matrix_recursive_children_transport

forall b c u v l m pb pc nb nc q eb ec fb fc k. (forall mdr_i_source mdr_a_source. (exists mdr_gap_sourceb. mdr_gap_sourceb + S (mdr_i_source) = (l)) -> (((exists ff_h_mdr_sourceo. ff_h_mdr_sourceo + S (mdr_a_source) = S ((S (mdr_i_source)) * c)) /\ exists ff_q_mdr_sourceo. b = ff_q_mdr_sourceo * S ((S (mdr_i_source)) * c) + (mdr_a_source))) -> (((exists ff_h_mdr_sourcen. ff_h_mdr_sourcen + S (mdr_a_source) = S ((S (mdr_i_source)) * v)) /\ exists ff_q_mdr_sourcen. u = ff_q_mdr_sourcen * S ((S (mdr_i_source)) * v) + (mdr_a_source)))) -> (exists mdr_gap_transport. mdr_gap_transport + (l) = (m)) -> (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_j_new. (exists mdr_gap_newj. mdr_gap_newj + S (mdr_j_new) = (k)) -> exists mdr_i_new mdr_up_new mdr_us_new mdr_un_new mdr_ut_new mdr_p_new mdr_n_new. ((exists mdr_gap_newi. mdr_gap_newi + S (mdr_i_new) = (m)) /\ ((exists mdr_z_newr. ((exists mdr_a_newrc mdr_b_newrc mdr_c_newrc mdr_e_newrc mdr_f_newrc. ((mdr_a_newrc = ((q) + (mdr_up_new)) * S ((q) + (mdr_up_new)) + ((mdr_up_new) + (mdr_up_new))) /\ ((mdr_b_newrc = ((mdr_us_new) + (mdr_un_new)) * S ((mdr_us_new) + (mdr_un_new)) + ((mdr_un_new) + (mdr_un_new))) /\ ((mdr_c_newrc = ((mdr_a_newrc) + (mdr_b_newrc)) * S ((mdr_a_newrc) + (mdr_b_newrc)) + ((mdr_b_newrc) + (mdr_b_newrc))) /\ ((mdr_e_newrc = ((mdr_p_new) + (mdr_n_new)) * S ((mdr_p_new) + (mdr_n_new)) + ((mdr_n_new) + (mdr_n_new))) /\ ((mdr_f_newrc = ((mdr_ut_new) + (mdr_e_newrc)) * S ((mdr_ut_new) + (mdr_e_newrc)) + ((mdr_e_newrc) + (mdr_e_newrc))) /\ ((mdr_z_newr) = ((mdr_c_newrc) + (mdr_f_newrc)) * S ((mdr_c_newrc) + (mdr_f_newrc)) + ((mdr_f_newrc) + (mdr_f_newrc))))))))) /\ (((exists ff_h_mdr_newrb. ff_h_mdr_newrb + S (mdr_z_newr) = S ((S (mdr_i_new)) * v)) /\ exists ff_q_mdr_newrb. u = ff_q_mdr_newrb * S ((S (mdr_i_new)) * v) + (mdr_z_newr))))) /\ ((((forall ff_index_mdm_prefix_mdr_newm_positive. (exists ff_gap_mdm_lt_mdr_newm_positive_index_bound. ff_gap_mdm_lt_mdr_newm_positive_index_bound + S (ff_index_mdm_prefix_mdr_newm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_newm_positive ff_column_mdm_prefix_mdr_newm_positive ff_value_mdm_prefix_mdr_newm_positive. (ff_index_mdm_prefix_mdr_newm_positive = (q) * ff_row_mdm_prefix_mdr_newm_positive + ff_column_mdm_prefix_mdr_newm_positive /\ ((exists ff_gap_mdm_lt_mdr_newm_positive_column_bound. ff_gap_mdm_lt_mdr_newm_positive_column_bound + S (ff_column_mdm_prefix_mdr_newm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_newm_positive_cell ff_column_mdm_cell_mdr_newm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_newm_positive_cell_row_before. ff_gap_mdm_lt_mdr_newm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_newm_positive) = (0)) /\ ff_row_mdm_cell_mdr_newm_positive_cell = ff_row_mdm_prefix_mdr_newm_positive) \/ ((exists ff_gap_mdm_le_mdr_newm_positive_cell_row_after. ff_gap_mdm_le_mdr_newm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_newm_positive)) /\ ff_row_mdm_cell_mdr_newm_positive_cell = S ff_row_mdm_prefix_mdr_newm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_newm_positive_cell_column_before. ff_gap_mdm_lt_mdr_newm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_newm_positive) = (mdr_j_new)) /\ ff_column_mdm_cell_mdr_newm_positive_cell = ff_column_mdm_prefix_mdr_newm_positive) \/ ((exists ff_gap_mdm_le_mdr_newm_positive_cell_column_after. ff_gap_mdm_le_mdr_newm_positive_cell_column_after + (mdr_j_new) = (ff_column_mdm_prefix_mdr_newm_positive)) /\ ff_column_mdm_cell_mdr_newm_positive_cell = S ff_column_mdm_prefix_mdr_newm_positive))) /\ (((exists ff_h_mdm_mdr_newm_positive_cell_source. ff_h_mdm_mdr_newm_positive_cell_source + S (ff_value_mdm_prefix_mdr_newm_positive) = S ((S ((ff_row_mdm_cell_mdr_newm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_newm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_newm_positive_cell_source. pb = ff_q_mdm_mdr_newm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_newm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_newm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_newm_positive)))))) /\ (((exists ff_h_mdm_mdr_newm_positive_target. ff_h_mdm_mdr_newm_positive_target + S (ff_value_mdm_prefix_mdr_newm_positive) = S ((S (ff_index_mdm_prefix_mdr_newm_positive)) * mdr_us_new)) /\ exists ff_q_mdm_mdr_newm_positive_target. mdr_up_new = ff_q_mdm_mdr_newm_positive_target * S ((S (ff_index_mdm_prefix_mdr_newm_positive)) * mdr_us_new) + (ff_value_mdm_prefix_mdr_newm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_newm_negative. (exists ff_gap_mdm_lt_mdr_newm_negative_index_bound. ff_gap_mdm_lt_mdr_newm_negative_index_bound + S (ff_index_mdm_prefix_mdr_newm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_newm_negative ff_column_mdm_prefix_mdr_newm_negative ff_value_mdm_prefix_mdr_newm_negative. (ff_index_mdm_prefix_mdr_newm_negative = (q) * ff_row_mdm_prefix_mdr_newm_negative + ff_column_mdm_prefix_mdr_newm_negative /\ ((exists ff_gap_mdm_lt_mdr_newm_negative_column_bound. ff_gap_mdm_lt_mdr_newm_negative_column_bound + S (ff_column_mdm_prefix_mdr_newm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_newm_negative_cell ff_column_mdm_cell_mdr_newm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_newm_negative_cell_row_before. ff_gap_mdm_lt_mdr_newm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_newm_negative) = (0)) /\ ff_row_mdm_cell_mdr_newm_negative_cell = ff_row_mdm_prefix_mdr_newm_negative) \/ ((exists ff_gap_mdm_le_mdr_newm_negative_cell_row_after. ff_gap_mdm_le_mdr_newm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_newm_negative)) /\ ff_row_mdm_cell_mdr_newm_negative_cell = S ff_row_mdm_prefix_mdr_newm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_newm_negative_cell_column_before. ff_gap_mdm_lt_mdr_newm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_newm_negative) = (mdr_j_new)) /\ ff_column_mdm_cell_mdr_newm_negative_cell = ff_column_mdm_prefix_mdr_newm_negative) \/ ((exists ff_gap_mdm_le_mdr_newm_negative_cell_column_after. ff_gap_mdm_le_mdr_newm_negative_cell_column_after + (mdr_j_new) = (ff_column_mdm_prefix_mdr_newm_negative)) /\ ff_column_mdm_cell_mdr_newm_negative_cell = S ff_column_mdm_prefix_mdr_newm_negative))) /\ (((exists ff_h_mdm_mdr_newm_negative_cell_source. ff_h_mdm_mdr_newm_negative_cell_source + S (ff_value_mdm_prefix_mdr_newm_negative) = S ((S ((ff_row_mdm_cell_mdr_newm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_newm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_newm_negative_cell_source. nb = ff_q_mdm_mdr_newm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_newm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_newm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_newm_negative)))))) /\ (((exists ff_h_mdm_mdr_newm_negative_target. ff_h_mdm_mdr_newm_negative_target + S (ff_value_mdm_prefix_mdr_newm_negative) = S ((S (ff_index_mdm_prefix_mdr_newm_negative)) * mdr_ut_new)) /\ exists ff_q_mdm_mdr_newm_negative_target. mdr_un_new = ff_q_mdm_mdr_newm_negative_target * S ((S (ff_index_mdm_prefix_mdr_newm_negative)) * mdr_ut_new) + (ff_value_mdm_prefix_mdr_newm_negative))))))))) /\ ((((exists ff_h_mdr_newp. ff_h_mdr_newp + S (mdr_p_new) = S ((S (mdr_j_new)) * ec)) /\ exists ff_q_mdr_newp. eb = ff_q_mdr_newp * S ((S (mdr_j_new)) * ec) + (mdr_p_new))) /\ (((exists ff_h_mdr_newn. ff_h_mdr_newn + S (mdr_n_new) = S ((S (mdr_j_new)) * fc)) /\ exists ff_q_mdr_newn. fb = ff_q_mdr_newn * S ((S (mdr_j_new)) * fc) + (mdr_n_new))))))))