matrix_recursive_children_recode

Exact expanded first-order arithmetic statement

forall b c l pb pc nb nc q eb ec fb fc k ub uc vb vc. (forall mdr_j_old. (exists mdr_gap_oldj. mdr_gap_oldj + S (mdr_j_old) = (k)) -> exists mdr_i_old mdr_up_old mdr_us_old mdr_un_old mdr_ut_old mdr_p_old mdr_n_old. ((exists mdr_gap_oldi. mdr_gap_oldi + S (mdr_i_old) = (l)) /\ ((exists mdr_z_oldr. ((exists mdr_a_oldrc mdr_b_oldrc mdr_c_oldrc mdr_e_oldrc mdr_f_oldrc. ((mdr_a_oldrc = ((q) + (mdr_up_old)) * S ((q) + (mdr_up_old)) + ((mdr_up_old) + (mdr_up_old))) /\ ((mdr_b_oldrc = ((mdr_us_old) + (mdr_un_old)) * S ((mdr_us_old) + (mdr_un_old)) + ((mdr_un_old) + (mdr_un_old))) /\ ((mdr_c_oldrc = ((mdr_a_oldrc) + (mdr_b_oldrc)) * S ((mdr_a_oldrc) + (mdr_b_oldrc)) + ((mdr_b_oldrc) + (mdr_b_oldrc))) /\ ((mdr_e_oldrc = ((mdr_p_old) + (mdr_n_old)) * S ((mdr_p_old) + (mdr_n_old)) + ((mdr_n_old) + (mdr_n_old))) /\ ((mdr_f_oldrc = ((mdr_ut_old) + (mdr_e_oldrc)) * S ((mdr_ut_old) + (mdr_e_oldrc)) + ((mdr_e_oldrc) + (mdr_e_oldrc))) /\ ((mdr_z_oldr) = ((mdr_c_oldrc) + (mdr_f_oldrc)) * S ((mdr_c_oldrc) + (mdr_f_oldrc)) + ((mdr_f_oldrc) + (mdr_f_oldrc))))))))) /\ (((exists ff_h_mdr_oldrb. ff_h_mdr_oldrb + S (mdr_z_oldr) = S ((S (mdr_i_old)) * c)) /\ exists ff_q_mdr_oldrb. b = ff_q_mdr_oldrb * S ((S (mdr_i_old)) * c) + (mdr_z_oldr))))) /\ ((((forall ff_index_mdm_prefix_mdr_oldm_positive. (exists ff_gap_mdm_lt_mdr_oldm_positive_index_bound. ff_gap_mdm_lt_mdr_oldm_positive_index_bound + S (ff_index_mdm_prefix_mdr_oldm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_oldm_positive ff_column_mdm_prefix_mdr_oldm_positive ff_value_mdm_prefix_mdr_oldm_positive. (ff_index_mdm_prefix_mdr_oldm_positive = (q) * ff_row_mdm_prefix_mdr_oldm_positive + ff_column_mdm_prefix_mdr_oldm_positive /\ ((exists ff_gap_mdm_lt_mdr_oldm_positive_column_bound. ff_gap_mdm_lt_mdr_oldm_positive_column_bound + S (ff_column_mdm_prefix_mdr_oldm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_oldm_positive_cell ff_column_mdm_cell_mdr_oldm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_oldm_positive_cell_row_before. ff_gap_mdm_lt_mdr_oldm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_oldm_positive) = (0)) /\ ff_row_mdm_cell_mdr_oldm_positive_cell = ff_row_mdm_prefix_mdr_oldm_positive) \/ ((exists ff_gap_mdm_le_mdr_oldm_positive_cell_row_after. ff_gap_mdm_le_mdr_oldm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_oldm_positive)) /\ ff_row_mdm_cell_mdr_oldm_positive_cell = S ff_row_mdm_prefix_mdr_oldm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_oldm_positive_cell_column_before. ff_gap_mdm_lt_mdr_oldm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_oldm_positive) = (mdr_j_old)) /\ ff_column_mdm_cell_mdr_oldm_positive_cell = ff_column_mdm_prefix_mdr_oldm_positive) \/ ((exists ff_gap_mdm_le_mdr_oldm_positive_cell_column_after. ff_gap_mdm_le_mdr_oldm_positive_cell_column_after + (mdr_j_old) = (ff_column_mdm_prefix_mdr_oldm_positive)) /\ ff_column_mdm_cell_mdr_oldm_positive_cell = S ff_column_mdm_prefix_mdr_oldm_positive))) /\ (((exists ff_h_mdm_mdr_oldm_positive_cell_source. ff_h_mdm_mdr_oldm_positive_cell_source + S (ff_value_mdm_prefix_mdr_oldm_positive) = S ((S ((ff_row_mdm_cell_mdr_oldm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_oldm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_oldm_positive_cell_source. pb = ff_q_mdm_mdr_oldm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_oldm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_oldm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_oldm_positive)))))) /\ (((exists ff_h_mdm_mdr_oldm_positive_target. ff_h_mdm_mdr_oldm_positive_target + S (ff_value_mdm_prefix_mdr_oldm_positive) = S ((S (ff_index_mdm_prefix_mdr_oldm_positive)) * mdr_us_old)) /\ exists ff_q_mdm_mdr_oldm_positive_target. mdr_up_old = ff_q_mdm_mdr_oldm_positive_target * S ((S (ff_index_mdm_prefix_mdr_oldm_positive)) * mdr_us_old) + (ff_value_mdm_prefix_mdr_oldm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_oldm_negative. (exists ff_gap_mdm_lt_mdr_oldm_negative_index_bound. ff_gap_mdm_lt_mdr_oldm_negative_index_bound + S (ff_index_mdm_prefix_mdr_oldm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_oldm_negative ff_column_mdm_prefix_mdr_oldm_negative ff_value_mdm_prefix_mdr_oldm_negative. (ff_index_mdm_prefix_mdr_oldm_negative = (q) * ff_row_mdm_prefix_mdr_oldm_negative + ff_column_mdm_prefix_mdr_oldm_negative /\ ((exists ff_gap_mdm_lt_mdr_oldm_negative_column_bound. ff_gap_mdm_lt_mdr_oldm_negative_column_bound + S (ff_column_mdm_prefix_mdr_oldm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_oldm_negative_cell ff_column_mdm_cell_mdr_oldm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_oldm_negative_cell_row_before. ff_gap_mdm_lt_mdr_oldm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_oldm_negative) = (0)) /\ ff_row_mdm_cell_mdr_oldm_negative_cell = ff_row_mdm_prefix_mdr_oldm_negative) \/ ((exists ff_gap_mdm_le_mdr_oldm_negative_cell_row_after. ff_gap_mdm_le_mdr_oldm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_oldm_negative)) /\ ff_row_mdm_cell_mdr_oldm_negative_cell = S ff_row_mdm_prefix_mdr_oldm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_oldm_negative_cell_column_before. ff_gap_mdm_lt_mdr_oldm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_oldm_negative) = (mdr_j_old)) /\ ff_column_mdm_cell_mdr_oldm_negative_cell = ff_column_mdm_prefix_mdr_oldm_negative) \/ ((exists ff_gap_mdm_le_mdr_oldm_negative_cell_column_after. ff_gap_mdm_le_mdr_oldm_negative_cell_column_after + (mdr_j_old) = (ff_column_mdm_prefix_mdr_oldm_negative)) /\ ff_column_mdm_cell_mdr_oldm_negative_cell = S ff_column_mdm_prefix_mdr_oldm_negative))) /\ (((exists ff_h_mdm_mdr_oldm_negative_cell_source. ff_h_mdm_mdr_oldm_negative_cell_source + S (ff_value_mdm_prefix_mdr_oldm_negative) = S ((S ((ff_row_mdm_cell_mdr_oldm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_oldm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_oldm_negative_cell_source. nb = ff_q_mdm_mdr_oldm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_oldm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_oldm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_oldm_negative)))))) /\ (((exists ff_h_mdm_mdr_oldm_negative_target. ff_h_mdm_mdr_oldm_negative_target + S (ff_value_mdm_prefix_mdr_oldm_negative) = S ((S (ff_index_mdm_prefix_mdr_oldm_negative)) * mdr_ut_old)) /\ exists ff_q_mdm_mdr_oldm_negative_target. mdr_un_old = ff_q_mdm_mdr_oldm_negative_target * S ((S (ff_index_mdm_prefix_mdr_oldm_negative)) * mdr_ut_old) + (ff_value_mdm_prefix_mdr_oldm_negative))))))))) /\ ((((exists ff_h_mdr_oldp. ff_h_mdr_oldp + S (mdr_p_old) = S ((S (mdr_j_old)) * ec)) /\ exists ff_q_mdr_oldp. eb = ff_q_mdr_oldp * S ((S (mdr_j_old)) * ec) + (mdr_p_old))) /\ (((exists ff_h_mdr_oldn. ff_h_mdr_oldn + S (mdr_n_old) = S ((S (mdr_j_old)) * fc)) /\ exists ff_q_mdr_oldn. fb = ff_q_mdr_oldn * S ((S (mdr_j_old)) * fc) + (mdr_n_old)))))))) -> (forall mdr_i_recode_p mdr_a_recode_p. (exists mdr_gap_recode_pb. mdr_gap_recode_pb + S (mdr_i_recode_p) = (k)) -> (((exists ff_h_mdr_recode_po. ff_h_mdr_recode_po + S (mdr_a_recode_p) = S ((S (mdr_i_recode_p)) * ec)) /\ exists ff_q_mdr_recode_po. eb = ff_q_mdr_recode_po * S ((S (mdr_i_recode_p)) * ec) + (mdr_a_recode_p))) -> (((exists ff_h_mdr_recode_pn. ff_h_mdr_recode_pn + S (mdr_a_recode_p) = S ((S (mdr_i_recode_p)) * uc)) /\ exists ff_q_mdr_recode_pn. ub = ff_q_mdr_recode_pn * S ((S (mdr_i_recode_p)) * uc) + (mdr_a_recode_p)))) -> (forall mdr_i_recode_n mdr_a_recode_n. (exists mdr_gap_recode_nb. mdr_gap_recode_nb + S (mdr_i_recode_n) = (k)) -> (((exists ff_h_mdr_recode_no. ff_h_mdr_recode_no + S (mdr_a_recode_n) = S ((S (mdr_i_recode_n)) * fc)) /\ exists ff_q_mdr_recode_no. fb = ff_q_mdr_recode_no * S ((S (mdr_i_recode_n)) * fc) + (mdr_a_recode_n))) -> (((exists ff_h_mdr_recode_nn. ff_h_mdr_recode_nn + S (mdr_a_recode_n) = S ((S (mdr_i_recode_n)) * vc)) /\ exists ff_q_mdr_recode_nn. vb = ff_q_mdr_recode_nn * S ((S (mdr_i_recode_n)) * vc) + (mdr_a_recode_n)))) -> (forall mdr_j_recoded. (exists mdr_gap_recodedj. mdr_gap_recodedj + S (mdr_j_recoded) = (k)) -> exists mdr_i_recoded mdr_up_recoded mdr_us_recoded mdr_un_recoded mdr_ut_recoded mdr_p_recoded mdr_n_recoded. ((exists mdr_gap_recodedi. mdr_gap_recodedi + S (mdr_i_recoded) = (l)) /\ ((exists mdr_z_recodedr. ((exists mdr_a_recodedrc mdr_b_recodedrc mdr_c_recodedrc mdr_e_recodedrc mdr_f_recodedrc. ((mdr_a_recodedrc = ((q) + (mdr_up_recoded)) * S ((q) + (mdr_up_recoded)) + ((mdr_up_recoded) + (mdr_up_recoded))) /\ ((mdr_b_recodedrc = ((mdr_us_recoded) + (mdr_un_recoded)) * S ((mdr_us_recoded) + (mdr_un_recoded)) + ((mdr_un_recoded) + (mdr_un_recoded))) /\ ((mdr_c_recodedrc = ((mdr_a_recodedrc) + (mdr_b_recodedrc)) * S ((mdr_a_recodedrc) + (mdr_b_recodedrc)) + ((mdr_b_recodedrc) + (mdr_b_recodedrc))) /\ ((mdr_e_recodedrc = ((mdr_p_recoded) + (mdr_n_recoded)) * S ((mdr_p_recoded) + (mdr_n_recoded)) + ((mdr_n_recoded) + (mdr_n_recoded))) /\ ((mdr_f_recodedrc = ((mdr_ut_recoded) + (mdr_e_recodedrc)) * S ((mdr_ut_recoded) + (mdr_e_recodedrc)) + ((mdr_e_recodedrc) + (mdr_e_recodedrc))) /\ ((mdr_z_recodedr) = ((mdr_c_recodedrc) + (mdr_f_recodedrc)) * S ((mdr_c_recodedrc) + (mdr_f_recodedrc)) + ((mdr_f_recodedrc) + (mdr_f_recodedrc))))))))) /\ (((exists ff_h_mdr_recodedrb. ff_h_mdr_recodedrb + S (mdr_z_recodedr) = S ((S (mdr_i_recoded)) * c)) /\ exists ff_q_mdr_recodedrb. b = ff_q_mdr_recodedrb * S ((S (mdr_i_recoded)) * c) + (mdr_z_recodedr))))) /\ ((((forall ff_index_mdm_prefix_mdr_recodedm_positive. (exists ff_gap_mdm_lt_mdr_recodedm_positive_index_bound. ff_gap_mdm_lt_mdr_recodedm_positive_index_bound + S (ff_index_mdm_prefix_mdr_recodedm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_recodedm_positive ff_column_mdm_prefix_mdr_recodedm_positive ff_value_mdm_prefix_mdr_recodedm_positive. (ff_index_mdm_prefix_mdr_recodedm_positive = (q) * ff_row_mdm_prefix_mdr_recodedm_positive + ff_column_mdm_prefix_mdr_recodedm_positive /\ ((exists ff_gap_mdm_lt_mdr_recodedm_positive_column_bound. ff_gap_mdm_lt_mdr_recodedm_positive_column_bound + S (ff_column_mdm_prefix_mdr_recodedm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_recodedm_positive_cell ff_column_mdm_cell_mdr_recodedm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_recodedm_positive_cell_row_before. ff_gap_mdm_lt_mdr_recodedm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_recodedm_positive) = (0)) /\ ff_row_mdm_cell_mdr_recodedm_positive_cell = ff_row_mdm_prefix_mdr_recodedm_positive) \/ ((exists ff_gap_mdm_le_mdr_recodedm_positive_cell_row_after. ff_gap_mdm_le_mdr_recodedm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_recodedm_positive)) /\ ff_row_mdm_cell_mdr_recodedm_positive_cell = S ff_row_mdm_prefix_mdr_recodedm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_recodedm_positive_cell_column_before. ff_gap_mdm_lt_mdr_recodedm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_recodedm_positive) = (mdr_j_recoded)) /\ ff_column_mdm_cell_mdr_recodedm_positive_cell = ff_column_mdm_prefix_mdr_recodedm_positive) \/ ((exists ff_gap_mdm_le_mdr_recodedm_positive_cell_column_after. ff_gap_mdm_le_mdr_recodedm_positive_cell_column_after + (mdr_j_recoded) = (ff_column_mdm_prefix_mdr_recodedm_positive)) /\ ff_column_mdm_cell_mdr_recodedm_positive_cell = S ff_column_mdm_prefix_mdr_recodedm_positive))) /\ (((exists ff_h_mdm_mdr_recodedm_positive_cell_source. ff_h_mdm_mdr_recodedm_positive_cell_source + S (ff_value_mdm_prefix_mdr_recodedm_positive) = S ((S ((ff_row_mdm_cell_mdr_recodedm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_recodedm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_recodedm_positive_cell_source. pb = ff_q_mdm_mdr_recodedm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_recodedm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_recodedm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_recodedm_positive)))))) /\ (((exists ff_h_mdm_mdr_recodedm_positive_target. ff_h_mdm_mdr_recodedm_positive_target + S (ff_value_mdm_prefix_mdr_recodedm_positive) = S ((S (ff_index_mdm_prefix_mdr_recodedm_positive)) * mdr_us_recoded)) /\ exists ff_q_mdm_mdr_recodedm_positive_target. mdr_up_recoded = ff_q_mdm_mdr_recodedm_positive_target * S ((S (ff_index_mdm_prefix_mdr_recodedm_positive)) * mdr_us_recoded) + (ff_value_mdm_prefix_mdr_recodedm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_recodedm_negative. (exists ff_gap_mdm_lt_mdr_recodedm_negative_index_bound. ff_gap_mdm_lt_mdr_recodedm_negative_index_bound + S (ff_index_mdm_prefix_mdr_recodedm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_recodedm_negative ff_column_mdm_prefix_mdr_recodedm_negative ff_value_mdm_prefix_mdr_recodedm_negative. (ff_index_mdm_prefix_mdr_recodedm_negative = (q) * ff_row_mdm_prefix_mdr_recodedm_negative + ff_column_mdm_prefix_mdr_recodedm_negative /\ ((exists ff_gap_mdm_lt_mdr_recodedm_negative_column_bound. ff_gap_mdm_lt_mdr_recodedm_negative_column_bound + S (ff_column_mdm_prefix_mdr_recodedm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_recodedm_negative_cell ff_column_mdm_cell_mdr_recodedm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_recodedm_negative_cell_row_before. ff_gap_mdm_lt_mdr_recodedm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_recodedm_negative) = (0)) /\ ff_row_mdm_cell_mdr_recodedm_negative_cell = ff_row_mdm_prefix_mdr_recodedm_negative) \/ ((exists ff_gap_mdm_le_mdr_recodedm_negative_cell_row_after. ff_gap_mdm_le_mdr_recodedm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_recodedm_negative)) /\ ff_row_mdm_cell_mdr_recodedm_negative_cell = S ff_row_mdm_prefix_mdr_recodedm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_recodedm_negative_cell_column_before. ff_gap_mdm_lt_mdr_recodedm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_recodedm_negative) = (mdr_j_recoded)) /\ ff_column_mdm_cell_mdr_recodedm_negative_cell = ff_column_mdm_prefix_mdr_recodedm_negative) \/ ((exists ff_gap_mdm_le_mdr_recodedm_negative_cell_column_after. ff_gap_mdm_le_mdr_recodedm_negative_cell_column_after + (mdr_j_recoded) = (ff_column_mdm_prefix_mdr_recodedm_negative)) /\ ff_column_mdm_cell_mdr_recodedm_negative_cell = S ff_column_mdm_prefix_mdr_recodedm_negative))) /\ (((exists ff_h_mdm_mdr_recodedm_negative_cell_source. ff_h_mdm_mdr_recodedm_negative_cell_source + S (ff_value_mdm_prefix_mdr_recodedm_negative) = S ((S ((ff_row_mdm_cell_mdr_recodedm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_recodedm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_recodedm_negative_cell_source. nb = ff_q_mdm_mdr_recodedm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_recodedm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_recodedm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_recodedm_negative)))))) /\ (((exists ff_h_mdm_mdr_recodedm_negative_target. ff_h_mdm_mdr_recodedm_negative_target + S (ff_value_mdm_prefix_mdr_recodedm_negative) = S ((S (ff_index_mdm_prefix_mdr_recodedm_negative)) * mdr_ut_recoded)) /\ exists ff_q_mdm_mdr_recodedm_negative_target. mdr_un_recoded = ff_q_mdm_mdr_recodedm_negative_target * S ((S (ff_index_mdm_prefix_mdr_recodedm_negative)) * mdr_ut_recoded) + (ff_value_mdm_prefix_mdr_recodedm_negative))))))))) /\ ((((exists ff_h_mdr_recodedp. ff_h_mdr_recodedp + S (mdr_p_recoded) = S ((S (mdr_j_recoded)) * uc)) /\ exists ff_q_mdr_recodedp. ub = ff_q_mdr_recodedp * S ((S (mdr_j_recoded)) * uc) + (mdr_p_recoded))) /\ (((exists ff_h_mdr_recodedn. ff_h_mdr_recodedn + S (mdr_n_recoded) = S ((S (mdr_j_recoded)) * vc)) /\ exists ff_q_mdr_recodedn. vb = ff_q_mdr_recodedn * S ((S (mdr_j_recoded)) * vc) + (mdr_n_recoded))))))))