matrix_recursive_children_extend

Exact expanded first-order arithmetic statement

forall b c l pb pc nb nc q eb ec fb fc k i up us un ut a z. (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)))))))) -> (exists mdr_gap_append_child_bound. mdr_gap_append_child_bound + S (i) = (l)) -> (exists mdr_z_append_child_record. ((exists mdr_a_append_child_recordc mdr_b_append_child_recordc mdr_c_append_child_recordc mdr_e_append_child_recordc mdr_f_append_child_recordc. ((mdr_a_append_child_recordc = ((q) + (up)) * S ((q) + (up)) + ((up) + (up))) /\ ((mdr_b_append_child_recordc = ((us) + (un)) * S ((us) + (un)) + ((un) + (un))) /\ ((mdr_c_append_child_recordc = ((mdr_a_append_child_recordc) + (mdr_b_append_child_recordc)) * S ((mdr_a_append_child_recordc) + (mdr_b_append_child_recordc)) + ((mdr_b_append_child_recordc) + (mdr_b_append_child_recordc))) /\ ((mdr_e_append_child_recordc = ((a) + (z)) * S ((a) + (z)) + ((z) + (z))) /\ ((mdr_f_append_child_recordc = ((ut) + (mdr_e_append_child_recordc)) * S ((ut) + (mdr_e_append_child_recordc)) + ((mdr_e_append_child_recordc) + (mdr_e_append_child_recordc))) /\ ((mdr_z_append_child_record) = ((mdr_c_append_child_recordc) + (mdr_f_append_child_recordc)) * S ((mdr_c_append_child_recordc) + (mdr_f_append_child_recordc)) + ((mdr_f_append_child_recordc) + (mdr_f_append_child_recordc))))))))) /\ (((exists ff_h_mdr_append_child_recordb. ff_h_mdr_append_child_recordb + S (mdr_z_append_child_record) = S ((S (i)) * c)) /\ exists ff_q_mdr_append_child_recordb. b = ff_q_mdr_append_child_recordb * S ((S (i)) * c) + (mdr_z_append_child_record))))) -> (((forall ff_index_mdm_prefix_mdr_append_child_minor_positive. (exists ff_gap_mdm_lt_mdr_append_child_minor_positive_index_bound. ff_gap_mdm_lt_mdr_append_child_minor_positive_index_bound + S (ff_index_mdm_prefix_mdr_append_child_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_append_child_minor_positive ff_column_mdm_prefix_mdr_append_child_minor_positive ff_value_mdm_prefix_mdr_append_child_minor_positive. (ff_index_mdm_prefix_mdr_append_child_minor_positive = (q) * ff_row_mdm_prefix_mdr_append_child_minor_positive + ff_column_mdm_prefix_mdr_append_child_minor_positive /\ ((exists ff_gap_mdm_lt_mdr_append_child_minor_positive_column_bound. ff_gap_mdm_lt_mdr_append_child_minor_positive_column_bound + S (ff_column_mdm_prefix_mdr_append_child_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_append_child_minor_positive_cell ff_column_mdm_cell_mdr_append_child_minor_positive_cell. (((((exists ff_gap_mdm_lt_mdr_append_child_minor_positive_cell_row_before. ff_gap_mdm_lt_mdr_append_child_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_append_child_minor_positive) = (0)) /\ ff_row_mdm_cell_mdr_append_child_minor_positive_cell = ff_row_mdm_prefix_mdr_append_child_minor_positive) \/ ((exists ff_gap_mdm_le_mdr_append_child_minor_positive_cell_row_after. ff_gap_mdm_le_mdr_append_child_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_append_child_minor_positive)) /\ ff_row_mdm_cell_mdr_append_child_minor_positive_cell = S ff_row_mdm_prefix_mdr_append_child_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_append_child_minor_positive_cell_column_before. ff_gap_mdm_lt_mdr_append_child_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_append_child_minor_positive) = (k)) /\ ff_column_mdm_cell_mdr_append_child_minor_positive_cell = ff_column_mdm_prefix_mdr_append_child_minor_positive) \/ ((exists ff_gap_mdm_le_mdr_append_child_minor_positive_cell_column_after. ff_gap_mdm_le_mdr_append_child_minor_positive_cell_column_after + (k) = (ff_column_mdm_prefix_mdr_append_child_minor_positive)) /\ ff_column_mdm_cell_mdr_append_child_minor_positive_cell = S ff_column_mdm_prefix_mdr_append_child_minor_positive))) /\ (((exists ff_h_mdm_mdr_append_child_minor_positive_cell_source. ff_h_mdm_mdr_append_child_minor_positive_cell_source + S (ff_value_mdm_prefix_mdr_append_child_minor_positive) = S ((S ((ff_row_mdm_cell_mdr_append_child_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_append_child_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_append_child_minor_positive_cell_source. pb = ff_q_mdm_mdr_append_child_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_append_child_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_append_child_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_append_child_minor_positive)))))) /\ (((exists ff_h_mdm_mdr_append_child_minor_positive_target. ff_h_mdm_mdr_append_child_minor_positive_target + S (ff_value_mdm_prefix_mdr_append_child_minor_positive) = S ((S (ff_index_mdm_prefix_mdr_append_child_minor_positive)) * us)) /\ exists ff_q_mdm_mdr_append_child_minor_positive_target. up = ff_q_mdm_mdr_append_child_minor_positive_target * S ((S (ff_index_mdm_prefix_mdr_append_child_minor_positive)) * us) + (ff_value_mdm_prefix_mdr_append_child_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_append_child_minor_negative. (exists ff_gap_mdm_lt_mdr_append_child_minor_negative_index_bound. ff_gap_mdm_lt_mdr_append_child_minor_negative_index_bound + S (ff_index_mdm_prefix_mdr_append_child_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_append_child_minor_negative ff_column_mdm_prefix_mdr_append_child_minor_negative ff_value_mdm_prefix_mdr_append_child_minor_negative. (ff_index_mdm_prefix_mdr_append_child_minor_negative = (q) * ff_row_mdm_prefix_mdr_append_child_minor_negative + ff_column_mdm_prefix_mdr_append_child_minor_negative /\ ((exists ff_gap_mdm_lt_mdr_append_child_minor_negative_column_bound. ff_gap_mdm_lt_mdr_append_child_minor_negative_column_bound + S (ff_column_mdm_prefix_mdr_append_child_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_append_child_minor_negative_cell ff_column_mdm_cell_mdr_append_child_minor_negative_cell. (((((exists ff_gap_mdm_lt_mdr_append_child_minor_negative_cell_row_before. ff_gap_mdm_lt_mdr_append_child_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_append_child_minor_negative) = (0)) /\ ff_row_mdm_cell_mdr_append_child_minor_negative_cell = ff_row_mdm_prefix_mdr_append_child_minor_negative) \/ ((exists ff_gap_mdm_le_mdr_append_child_minor_negative_cell_row_after. ff_gap_mdm_le_mdr_append_child_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_append_child_minor_negative)) /\ ff_row_mdm_cell_mdr_append_child_minor_negative_cell = S ff_row_mdm_prefix_mdr_append_child_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_append_child_minor_negative_cell_column_before. ff_gap_mdm_lt_mdr_append_child_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_append_child_minor_negative) = (k)) /\ ff_column_mdm_cell_mdr_append_child_minor_negative_cell = ff_column_mdm_prefix_mdr_append_child_minor_negative) \/ ((exists ff_gap_mdm_le_mdr_append_child_minor_negative_cell_column_after. ff_gap_mdm_le_mdr_append_child_minor_negative_cell_column_after + (k) = (ff_column_mdm_prefix_mdr_append_child_minor_negative)) /\ ff_column_mdm_cell_mdr_append_child_minor_negative_cell = S ff_column_mdm_prefix_mdr_append_child_minor_negative))) /\ (((exists ff_h_mdm_mdr_append_child_minor_negative_cell_source. ff_h_mdm_mdr_append_child_minor_negative_cell_source + S (ff_value_mdm_prefix_mdr_append_child_minor_negative) = S ((S ((ff_row_mdm_cell_mdr_append_child_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_append_child_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_append_child_minor_negative_cell_source. nb = ff_q_mdm_mdr_append_child_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_append_child_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_append_child_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_append_child_minor_negative)))))) /\ (((exists ff_h_mdm_mdr_append_child_minor_negative_target. ff_h_mdm_mdr_append_child_minor_negative_target + S (ff_value_mdm_prefix_mdr_append_child_minor_negative) = S ((S (ff_index_mdm_prefix_mdr_append_child_minor_negative)) * ut)) /\ exists ff_q_mdm_mdr_append_child_minor_negative_target. un = ff_q_mdm_mdr_append_child_minor_negative_target * S ((S (ff_index_mdm_prefix_mdr_append_child_minor_negative)) * ut) + (ff_value_mdm_prefix_mdr_append_child_minor_negative))))))))) -> exists ub uc vb vc. (forall mdr_j_append_children. (exists mdr_gap_append_childrenj. mdr_gap_append_childrenj + S (mdr_j_append_children) = (S k)) -> exists mdr_i_append_children mdr_up_append_children mdr_us_append_children mdr_un_append_children mdr_ut_append_children mdr_p_append_children mdr_n_append_children. ((exists mdr_gap_append_childreni. mdr_gap_append_childreni + S (mdr_i_append_children) = (l)) /\ ((exists mdr_z_append_childrenr. ((exists mdr_a_append_childrenrc mdr_b_append_childrenrc mdr_c_append_childrenrc mdr_e_append_childrenrc mdr_f_append_childrenrc. ((mdr_a_append_childrenrc = ((q) + (mdr_up_append_children)) * S ((q) + (mdr_up_append_children)) + ((mdr_up_append_children) + (mdr_up_append_children))) /\ ((mdr_b_append_childrenrc = ((mdr_us_append_children) + (mdr_un_append_children)) * S ((mdr_us_append_children) + (mdr_un_append_children)) + ((mdr_un_append_children) + (mdr_un_append_children))) /\ ((mdr_c_append_childrenrc = ((mdr_a_append_childrenrc) + (mdr_b_append_childrenrc)) * S ((mdr_a_append_childrenrc) + (mdr_b_append_childrenrc)) + ((mdr_b_append_childrenrc) + (mdr_b_append_childrenrc))) /\ ((mdr_e_append_childrenrc = ((mdr_p_append_children) + (mdr_n_append_children)) * S ((mdr_p_append_children) + (mdr_n_append_children)) + ((mdr_n_append_children) + (mdr_n_append_children))) /\ ((mdr_f_append_childrenrc = ((mdr_ut_append_children) + (mdr_e_append_childrenrc)) * S ((mdr_ut_append_children) + (mdr_e_append_childrenrc)) + ((mdr_e_append_childrenrc) + (mdr_e_append_childrenrc))) /\ ((mdr_z_append_childrenr) = ((mdr_c_append_childrenrc) + (mdr_f_append_childrenrc)) * S ((mdr_c_append_childrenrc) + (mdr_f_append_childrenrc)) + ((mdr_f_append_childrenrc) + (mdr_f_append_childrenrc))))))))) /\ (((exists ff_h_mdr_append_childrenrb. ff_h_mdr_append_childrenrb + S (mdr_z_append_childrenr) = S ((S (mdr_i_append_children)) * c)) /\ exists ff_q_mdr_append_childrenrb. b = ff_q_mdr_append_childrenrb * S ((S (mdr_i_append_children)) * c) + (mdr_z_append_childrenr))))) /\ ((((forall ff_index_mdm_prefix_mdr_append_childrenm_positive. (exists ff_gap_mdm_lt_mdr_append_childrenm_positive_index_bound. ff_gap_mdm_lt_mdr_append_childrenm_positive_index_bound + S (ff_index_mdm_prefix_mdr_append_childrenm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_append_childrenm_positive ff_column_mdm_prefix_mdr_append_childrenm_positive ff_value_mdm_prefix_mdr_append_childrenm_positive. (ff_index_mdm_prefix_mdr_append_childrenm_positive = (q) * ff_row_mdm_prefix_mdr_append_childrenm_positive + ff_column_mdm_prefix_mdr_append_childrenm_positive /\ ((exists ff_gap_mdm_lt_mdr_append_childrenm_positive_column_bound. ff_gap_mdm_lt_mdr_append_childrenm_positive_column_bound + S (ff_column_mdm_prefix_mdr_append_childrenm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_append_childrenm_positive_cell ff_column_mdm_cell_mdr_append_childrenm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_append_childrenm_positive_cell_row_before. ff_gap_mdm_lt_mdr_append_childrenm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_append_childrenm_positive) = (0)) /\ ff_row_mdm_cell_mdr_append_childrenm_positive_cell = ff_row_mdm_prefix_mdr_append_childrenm_positive) \/ ((exists ff_gap_mdm_le_mdr_append_childrenm_positive_cell_row_after. ff_gap_mdm_le_mdr_append_childrenm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_append_childrenm_positive)) /\ ff_row_mdm_cell_mdr_append_childrenm_positive_cell = S ff_row_mdm_prefix_mdr_append_childrenm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_append_childrenm_positive_cell_column_before. ff_gap_mdm_lt_mdr_append_childrenm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_append_childrenm_positive) = (mdr_j_append_children)) /\ ff_column_mdm_cell_mdr_append_childrenm_positive_cell = ff_column_mdm_prefix_mdr_append_childrenm_positive) \/ ((exists ff_gap_mdm_le_mdr_append_childrenm_positive_cell_column_after. ff_gap_mdm_le_mdr_append_childrenm_positive_cell_column_after + (mdr_j_append_children) = (ff_column_mdm_prefix_mdr_append_childrenm_positive)) /\ ff_column_mdm_cell_mdr_append_childrenm_positive_cell = S ff_column_mdm_prefix_mdr_append_childrenm_positive))) /\ (((exists ff_h_mdm_mdr_append_childrenm_positive_cell_source. ff_h_mdm_mdr_append_childrenm_positive_cell_source + S (ff_value_mdm_prefix_mdr_append_childrenm_positive) = S ((S ((ff_row_mdm_cell_mdr_append_childrenm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_append_childrenm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_append_childrenm_positive_cell_source. pb = ff_q_mdm_mdr_append_childrenm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_append_childrenm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_append_childrenm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_append_childrenm_positive)))))) /\ (((exists ff_h_mdm_mdr_append_childrenm_positive_target. ff_h_mdm_mdr_append_childrenm_positive_target + S (ff_value_mdm_prefix_mdr_append_childrenm_positive) = S ((S (ff_index_mdm_prefix_mdr_append_childrenm_positive)) * mdr_us_append_children)) /\ exists ff_q_mdm_mdr_append_childrenm_positive_target. mdr_up_append_children = ff_q_mdm_mdr_append_childrenm_positive_target * S ((S (ff_index_mdm_prefix_mdr_append_childrenm_positive)) * mdr_us_append_children) + (ff_value_mdm_prefix_mdr_append_childrenm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_append_childrenm_negative. (exists ff_gap_mdm_lt_mdr_append_childrenm_negative_index_bound. ff_gap_mdm_lt_mdr_append_childrenm_negative_index_bound + S (ff_index_mdm_prefix_mdr_append_childrenm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_append_childrenm_negative ff_column_mdm_prefix_mdr_append_childrenm_negative ff_value_mdm_prefix_mdr_append_childrenm_negative. (ff_index_mdm_prefix_mdr_append_childrenm_negative = (q) * ff_row_mdm_prefix_mdr_append_childrenm_negative + ff_column_mdm_prefix_mdr_append_childrenm_negative /\ ((exists ff_gap_mdm_lt_mdr_append_childrenm_negative_column_bound. ff_gap_mdm_lt_mdr_append_childrenm_negative_column_bound + S (ff_column_mdm_prefix_mdr_append_childrenm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_append_childrenm_negative_cell ff_column_mdm_cell_mdr_append_childrenm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_append_childrenm_negative_cell_row_before. ff_gap_mdm_lt_mdr_append_childrenm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_append_childrenm_negative) = (0)) /\ ff_row_mdm_cell_mdr_append_childrenm_negative_cell = ff_row_mdm_prefix_mdr_append_childrenm_negative) \/ ((exists ff_gap_mdm_le_mdr_append_childrenm_negative_cell_row_after. ff_gap_mdm_le_mdr_append_childrenm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_append_childrenm_negative)) /\ ff_row_mdm_cell_mdr_append_childrenm_negative_cell = S ff_row_mdm_prefix_mdr_append_childrenm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_append_childrenm_negative_cell_column_before. ff_gap_mdm_lt_mdr_append_childrenm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_append_childrenm_negative) = (mdr_j_append_children)) /\ ff_column_mdm_cell_mdr_append_childrenm_negative_cell = ff_column_mdm_prefix_mdr_append_childrenm_negative) \/ ((exists ff_gap_mdm_le_mdr_append_childrenm_negative_cell_column_after. ff_gap_mdm_le_mdr_append_childrenm_negative_cell_column_after + (mdr_j_append_children) = (ff_column_mdm_prefix_mdr_append_childrenm_negative)) /\ ff_column_mdm_cell_mdr_append_childrenm_negative_cell = S ff_column_mdm_prefix_mdr_append_childrenm_negative))) /\ (((exists ff_h_mdm_mdr_append_childrenm_negative_cell_source. ff_h_mdm_mdr_append_childrenm_negative_cell_source + S (ff_value_mdm_prefix_mdr_append_childrenm_negative) = S ((S ((ff_row_mdm_cell_mdr_append_childrenm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_append_childrenm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_append_childrenm_negative_cell_source. nb = ff_q_mdm_mdr_append_childrenm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_append_childrenm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_append_childrenm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_append_childrenm_negative)))))) /\ (((exists ff_h_mdm_mdr_append_childrenm_negative_target. ff_h_mdm_mdr_append_childrenm_negative_target + S (ff_value_mdm_prefix_mdr_append_childrenm_negative) = S ((S (ff_index_mdm_prefix_mdr_append_childrenm_negative)) * mdr_ut_append_children)) /\ exists ff_q_mdm_mdr_append_childrenm_negative_target. mdr_un_append_children = ff_q_mdm_mdr_append_childrenm_negative_target * S ((S (ff_index_mdm_prefix_mdr_append_childrenm_negative)) * mdr_ut_append_children) + (ff_value_mdm_prefix_mdr_append_childrenm_negative))))))))) /\ ((((exists ff_h_mdr_append_childrenp. ff_h_mdr_append_childrenp + S (mdr_p_append_children) = S ((S (mdr_j_append_children)) * uc)) /\ exists ff_q_mdr_append_childrenp. ub = ff_q_mdr_append_childrenp * S ((S (mdr_j_append_children)) * uc) + (mdr_p_append_children))) /\ (((exists ff_h_mdr_append_childrenn. ff_h_mdr_append_childrenn + S (mdr_n_append_children) = S ((S (mdr_j_append_children)) * vc)) /\ exists ff_q_mdr_append_childrenn. vb = ff_q_mdr_append_childrenn * S ((S (mdr_j_append_children)) * vc) + (mdr_n_append_children))))))))