matrix_integer_selected_point_balance

forall ab ac bb bc eb ec fb fc r w q rb rc cb cc i a b c d. (forall ics_index_selected_parent_equal ics_value0_selected_parent_equal ics_value1_selected_parent_equal ics_value2_selected_parent_equal ics_value3_selected_parent_equal. (exists ics_gap_selected_parent_equal_bound. ics_gap_selected_parent_equal_bound + S (ics_index_selected_parent_equal) = ((r) * (w))) -> (((exists fs_h_ics_selected_parent_equal_at0. fs_h_ics_selected_parent_equal_at0 + S (ics_value0_selected_parent_equal) = S ((S (ics_index_selected_parent_equal)) * ac)) /\ exists fs_q_ics_selected_parent_equal_at0. ab = fs_q_ics_selected_parent_equal_at0 * S ((S (ics_index_selected_parent_equal)) * ac) + (ics_value0_selected_parent_equal))) -> (((exists fs_h_ics_selected_parent_equal_at1. fs_h_ics_selected_parent_equal_at1 + S (ics_value1_selected_parent_equal) = S ((S (ics_index_selected_parent_equal)) * bc)) /\ exists fs_q_ics_selected_parent_equal_at1. bb = fs_q_ics_selected_parent_equal_at1 * S ((S (ics_index_selected_parent_equal)) * bc) + (ics_value1_selected_parent_equal))) -> (((exists fs_h_ics_selected_parent_equal_at2. fs_h_ics_selected_parent_equal_at2 + S (ics_value2_selected_parent_equal) = S ((S (ics_index_selected_parent_equal)) * ec)) /\ exists fs_q_ics_selected_parent_equal_at2. eb = fs_q_ics_selected_parent_equal_at2 * S ((S (ics_index_selected_parent_equal)) * ec) + (ics_value2_selected_parent_equal))) -> (((exists fs_h_ics_selected_parent_equal_at3. fs_h_ics_selected_parent_equal_at3 + S (ics_value3_selected_parent_equal) = S ((S (ics_index_selected_parent_equal)) * fc)) /\ exists fs_q_ics_selected_parent_equal_at3. fb = fs_q_ics_selected_parent_equal_at3 * S ((S (ics_index_selected_parent_equal)) * fc) + (ics_value3_selected_parent_equal))) -> ics_value0_selected_parent_equal + ics_value3_selected_parent_equal = ics_value2_selected_parent_equal + ics_value1_selected_parent_equal) -> (((forall fom_index_mrf_selected_rowsbound. (exists fom_gap_mrf_selected_rowsbound_index_bound. fom_gap_mrf_selected_rowsbound_index_bound + S (fom_index_mrf_selected_rowsbound) = q) -> exists fom_value_mrf_selected_rowsbound. ((((exists fom_beta_height_mrf_selected_rowsbound_entry. fom_beta_height_mrf_selected_rowsbound_entry + S (fom_value_mrf_selected_rowsbound) = S ((S (fom_index_mrf_selected_rowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_selected_rowsbound_entry. rb = fom_beta_quotient_mrf_selected_rowsbound_entry * S ((S (fom_index_mrf_selected_rowsbound)) * rc) + (fom_value_mrf_selected_rowsbound))) /\ (exists fom_gap_mrf_selected_rowsbound_value_bound. fom_gap_mrf_selected_rowsbound_value_bound + S (fom_value_mrf_selected_rowsbound) = r))) /\ (forall mdr_i_selected_rowsdistinct mdr_j_selected_rowsdistinct mdr_a_selected_rowsdistinct. (exists mdr_gap_selected_rowsdistincti. mdr_gap_selected_rowsdistincti + S (mdr_i_selected_rowsdistinct) = (q)) -> (exists mdr_gap_selected_rowsdistinctj. mdr_gap_selected_rowsdistinctj + S (mdr_j_selected_rowsdistinct) = (q)) -> (((exists ff_h_mdr_selected_rowsdistinctfirst. ff_h_mdr_selected_rowsdistinctfirst + S (mdr_a_selected_rowsdistinct) = S ((S (mdr_i_selected_rowsdistinct)) * rc)) /\ exists ff_q_mdr_selected_rowsdistinctfirst. rb = ff_q_mdr_selected_rowsdistinctfirst * S ((S (mdr_i_selected_rowsdistinct)) * rc) + (mdr_a_selected_rowsdistinct))) -> (((exists ff_h_mdr_selected_rowsdistinctsecond. ff_h_mdr_selected_rowsdistinctsecond + S (mdr_a_selected_rowsdistinct) = S ((S (mdr_j_selected_rowsdistinct)) * rc)) /\ exists ff_q_mdr_selected_rowsdistinctsecond. rb = ff_q_mdr_selected_rowsdistinctsecond * S ((S (mdr_j_selected_rowsdistinct)) * rc) + (mdr_a_selected_rowsdistinct))) -> mdr_i_selected_rowsdistinct = mdr_j_selected_rowsdistinct))) -> (((forall fom_index_mrf_selected_columnsbound. (exists fom_gap_mrf_selected_columnsbound_index_bound. fom_gap_mrf_selected_columnsbound_index_bound + S (fom_index_mrf_selected_columnsbound) = q) -> exists fom_value_mrf_selected_columnsbound. ((((exists fom_beta_height_mrf_selected_columnsbound_entry. fom_beta_height_mrf_selected_columnsbound_entry + S (fom_value_mrf_selected_columnsbound) = S ((S (fom_index_mrf_selected_columnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_selected_columnsbound_entry. cb = fom_beta_quotient_mrf_selected_columnsbound_entry * S ((S (fom_index_mrf_selected_columnsbound)) * cc) + (fom_value_mrf_selected_columnsbound))) /\ (exists fom_gap_mrf_selected_columnsbound_value_bound. fom_gap_mrf_selected_columnsbound_value_bound + S (fom_value_mrf_selected_columnsbound) = w))) /\ (forall mdr_i_selected_columnsdistinct mdr_j_selected_columnsdistinct mdr_a_selected_columnsdistinct. (exists mdr_gap_selected_columnsdistincti. mdr_gap_selected_columnsdistincti + S (mdr_i_selected_columnsdistinct) = (q)) -> (exists mdr_gap_selected_columnsdistinctj. mdr_gap_selected_columnsdistinctj + S (mdr_j_selected_columnsdistinct) = (q)) -> (((exists ff_h_mdr_selected_columnsdistinctfirst. ff_h_mdr_selected_columnsdistinctfirst + S (mdr_a_selected_columnsdistinct) = S ((S (mdr_i_selected_columnsdistinct)) * cc)) /\ exists ff_q_mdr_selected_columnsdistinctfirst. cb = ff_q_mdr_selected_columnsdistinctfirst * S ((S (mdr_i_selected_columnsdistinct)) * cc) + (mdr_a_selected_columnsdistinct))) -> (((exists ff_h_mdr_selected_columnsdistinctsecond. ff_h_mdr_selected_columnsdistinctsecond + S (mdr_a_selected_columnsdistinct) = S ((S (mdr_j_selected_columnsdistinct)) * cc)) /\ exists ff_q_mdr_selected_columnsdistinctsecond. cb = ff_q_mdr_selected_columnsdistinctsecond * S ((S (mdr_j_selected_columnsdistinct)) * cc) + (mdr_a_selected_columnsdistinct))) -> mdr_i_selected_columnsdistinct = mdr_j_selected_columnsdistinct))) -> (exists mdr_gap_selected_flat_bound. mdr_gap_selected_flat_bound + S (i) = (q * q)) -> (exists mdr_r_selected_point_ap mdr_s_selected_point_ap mdr_u_selected_point_ap mdr_v_selected_point_ap. ((i = (q) * mdr_r_selected_point_ap + mdr_s_selected_point_ap) /\ ((exists mdr_gap_selected_point_apcolumn. mdr_gap_selected_point_apcolumn + S (mdr_s_selected_point_ap) = (q)) /\ ((((exists ff_h_mdr_selected_point_aprow_index. ff_h_mdr_selected_point_aprow_index + S (mdr_u_selected_point_ap) = S ((S (mdr_r_selected_point_ap)) * rc)) /\ exists ff_q_mdr_selected_point_aprow_index. rb = ff_q_mdr_selected_point_aprow_index * S ((S (mdr_r_selected_point_ap)) * rc) + (mdr_u_selected_point_ap))) /\ ((((exists ff_h_mdr_selected_point_apcolumn_index. ff_h_mdr_selected_point_apcolumn_index + S (mdr_v_selected_point_ap) = S ((S (mdr_s_selected_point_ap)) * cc)) /\ exists ff_q_mdr_selected_point_apcolumn_index. cb = ff_q_mdr_selected_point_apcolumn_index * S ((S (mdr_s_selected_point_ap)) * cc) + (mdr_v_selected_point_ap))) /\ (((exists ff_h_mdr_selected_point_apsource. ff_h_mdr_selected_point_apsource + S (a) = S ((S ((mdr_u_selected_point_ap) * (w) + (mdr_v_selected_point_ap))) * ac)) /\ exists ff_q_mdr_selected_point_apsource. ab = ff_q_mdr_selected_point_apsource * S ((S ((mdr_u_selected_point_ap) * (w) + (mdr_v_selected_point_ap))) * ac) + (a)))))))) -> (exists mdr_r_selected_point_an mdr_s_selected_point_an mdr_u_selected_point_an mdr_v_selected_point_an. ((i = (q) * mdr_r_selected_point_an + mdr_s_selected_point_an) /\ ((exists mdr_gap_selected_point_ancolumn. mdr_gap_selected_point_ancolumn + S (mdr_s_selected_point_an) = (q)) /\ ((((exists ff_h_mdr_selected_point_anrow_index. ff_h_mdr_selected_point_anrow_index + S (mdr_u_selected_point_an) = S ((S (mdr_r_selected_point_an)) * rc)) /\ exists ff_q_mdr_selected_point_anrow_index. rb = ff_q_mdr_selected_point_anrow_index * S ((S (mdr_r_selected_point_an)) * rc) + (mdr_u_selected_point_an))) /\ ((((exists ff_h_mdr_selected_point_ancolumn_index. ff_h_mdr_selected_point_ancolumn_index + S (mdr_v_selected_point_an) = S ((S (mdr_s_selected_point_an)) * cc)) /\ exists ff_q_mdr_selected_point_ancolumn_index. cb = ff_q_mdr_selected_point_ancolumn_index * S ((S (mdr_s_selected_point_an)) * cc) + (mdr_v_selected_point_an))) /\ (((exists ff_h_mdr_selected_point_ansource. ff_h_mdr_selected_point_ansource + S (b) = S ((S ((mdr_u_selected_point_an) * (w) + (mdr_v_selected_point_an))) * bc)) /\ exists ff_q_mdr_selected_point_ansource. bb = ff_q_mdr_selected_point_ansource * S ((S ((mdr_u_selected_point_an) * (w) + (mdr_v_selected_point_an))) * bc) + (b)))))))) -> (exists mdr_r_selected_point_bp mdr_s_selected_point_bp mdr_u_selected_point_bp mdr_v_selected_point_bp. ((i = (q) * mdr_r_selected_point_bp + mdr_s_selected_point_bp) /\ ((exists mdr_gap_selected_point_bpcolumn. mdr_gap_selected_point_bpcolumn + S (mdr_s_selected_point_bp) = (q)) /\ ((((exists ff_h_mdr_selected_point_bprow_index. ff_h_mdr_selected_point_bprow_index + S (mdr_u_selected_point_bp) = S ((S (mdr_r_selected_point_bp)) * rc)) /\ exists ff_q_mdr_selected_point_bprow_index. rb = ff_q_mdr_selected_point_bprow_index * S ((S (mdr_r_selected_point_bp)) * rc) + (mdr_u_selected_point_bp))) /\ ((((exists ff_h_mdr_selected_point_bpcolumn_index. ff_h_mdr_selected_point_bpcolumn_index + S (mdr_v_selected_point_bp) = S ((S (mdr_s_selected_point_bp)) * cc)) /\ exists ff_q_mdr_selected_point_bpcolumn_index. cb = ff_q_mdr_selected_point_bpcolumn_index * S ((S (mdr_s_selected_point_bp)) * cc) + (mdr_v_selected_point_bp))) /\ (((exists ff_h_mdr_selected_point_bpsource. ff_h_mdr_selected_point_bpsource + S (c) = S ((S ((mdr_u_selected_point_bp) * (w) + (mdr_v_selected_point_bp))) * ec)) /\ exists ff_q_mdr_selected_point_bpsource. eb = ff_q_mdr_selected_point_bpsource * S ((S ((mdr_u_selected_point_bp) * (w) + (mdr_v_selected_point_bp))) * ec) + (c)))))))) -> (exists mdr_r_selected_point_bn mdr_s_selected_point_bn mdr_u_selected_point_bn mdr_v_selected_point_bn. ((i = (q) * mdr_r_selected_point_bn + mdr_s_selected_point_bn) /\ ((exists mdr_gap_selected_point_bncolumn. mdr_gap_selected_point_bncolumn + S (mdr_s_selected_point_bn) = (q)) /\ ((((exists ff_h_mdr_selected_point_bnrow_index. ff_h_mdr_selected_point_bnrow_index + S (mdr_u_selected_point_bn) = S ((S (mdr_r_selected_point_bn)) * rc)) /\ exists ff_q_mdr_selected_point_bnrow_index. rb = ff_q_mdr_selected_point_bnrow_index * S ((S (mdr_r_selected_point_bn)) * rc) + (mdr_u_selected_point_bn))) /\ ((((exists ff_h_mdr_selected_point_bncolumn_index. ff_h_mdr_selected_point_bncolumn_index + S (mdr_v_selected_point_bn) = S ((S (mdr_s_selected_point_bn)) * cc)) /\ exists ff_q_mdr_selected_point_bncolumn_index. cb = ff_q_mdr_selected_point_bncolumn_index * S ((S (mdr_s_selected_point_bn)) * cc) + (mdr_v_selected_point_bn))) /\ (((exists ff_h_mdr_selected_point_bnsource. ff_h_mdr_selected_point_bnsource + S (d) = S ((S ((mdr_u_selected_point_bn) * (w) + (mdr_v_selected_point_bn))) * fc)) /\ exists ff_q_mdr_selected_point_bnsource. fb = ff_q_mdr_selected_point_bnsource * S ((S ((mdr_u_selected_point_bn) * (w) + (mdr_v_selected_point_bn))) * fc) + (d)))))))) -> a + d = c + b