matrix_integer_minor_cell_balance

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc q j r s a b c d. (forall ics_index_minor_parent_equal ics_value0_minor_parent_equal ics_value1_minor_parent_equal ics_value2_minor_parent_equal ics_value3_minor_parent_equal. (exists ics_gap_minor_parent_equal_bound. ics_gap_minor_parent_equal_bound + S (ics_index_minor_parent_equal) = ((S q) * (S q))) -> (((exists fs_h_ics_minor_parent_equal_at0. fs_h_ics_minor_parent_equal_at0 + S (ics_value0_minor_parent_equal) = S ((S (ics_index_minor_parent_equal)) * ac)) /\ exists fs_q_ics_minor_parent_equal_at0. ab = fs_q_ics_minor_parent_equal_at0 * S ((S (ics_index_minor_parent_equal)) * ac) + (ics_value0_minor_parent_equal))) -> (((exists fs_h_ics_minor_parent_equal_at1. fs_h_ics_minor_parent_equal_at1 + S (ics_value1_minor_parent_equal) = S ((S (ics_index_minor_parent_equal)) * bc)) /\ exists fs_q_ics_minor_parent_equal_at1. bb = fs_q_ics_minor_parent_equal_at1 * S ((S (ics_index_minor_parent_equal)) * bc) + (ics_value1_minor_parent_equal))) -> (((exists fs_h_ics_minor_parent_equal_at2. fs_h_ics_minor_parent_equal_at2 + S (ics_value2_minor_parent_equal) = S ((S (ics_index_minor_parent_equal)) * ec)) /\ exists fs_q_ics_minor_parent_equal_at2. eb = fs_q_ics_minor_parent_equal_at2 * S ((S (ics_index_minor_parent_equal)) * ec) + (ics_value2_minor_parent_equal))) -> (((exists fs_h_ics_minor_parent_equal_at3. fs_h_ics_minor_parent_equal_at3 + S (ics_value3_minor_parent_equal) = S ((S (ics_index_minor_parent_equal)) * fc)) /\ exists fs_q_ics_minor_parent_equal_at3. fb = fs_q_ics_minor_parent_equal_at3 * S ((S (ics_index_minor_parent_equal)) * fc) + (ics_value3_minor_parent_equal))) -> ics_value0_minor_parent_equal + ics_value3_minor_parent_equal = ics_value2_minor_parent_equal + ics_value1_minor_parent_equal) -> (exists mdr_gap_minor_row_bound. mdr_gap_minor_row_bound + S (r) = (q)) -> (exists mdr_gap_minor_col_bound. mdr_gap_minor_col_bound + S (s) = (q)) -> (exists ff_row_mdm_cell_mdre_minor_cell_ap ff_column_mdm_cell_mdre_minor_cell_ap. (((((exists ff_gap_mdm_lt_mdre_minor_cell_ap_row_before. ff_gap_mdm_lt_mdre_minor_cell_ap_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_minor_cell_ap = r) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_ap_row_after. ff_gap_mdm_le_mdre_minor_cell_ap_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_minor_cell_ap = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_cell_ap_column_before. ff_gap_mdm_lt_mdre_minor_cell_ap_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_minor_cell_ap = s) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_ap_column_after. ff_gap_mdm_le_mdre_minor_cell_ap_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_minor_cell_ap = S s))) /\ (((exists ff_h_mdm_mdre_minor_cell_ap_source. ff_h_mdm_mdre_minor_cell_ap_source + S (a) = S ((S ((ff_row_mdm_cell_mdre_minor_cell_ap) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_ap))) * ac)) /\ exists ff_q_mdm_mdre_minor_cell_ap_source. ab = ff_q_mdm_mdre_minor_cell_ap_source * S ((S ((ff_row_mdm_cell_mdre_minor_cell_ap) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_ap))) * ac) + (a)))))) -> (exists ff_row_mdm_cell_mdre_minor_cell_an ff_column_mdm_cell_mdre_minor_cell_an. (((((exists ff_gap_mdm_lt_mdre_minor_cell_an_row_before. ff_gap_mdm_lt_mdre_minor_cell_an_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_minor_cell_an = r) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_an_row_after. ff_gap_mdm_le_mdre_minor_cell_an_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_minor_cell_an = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_cell_an_column_before. ff_gap_mdm_lt_mdre_minor_cell_an_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_minor_cell_an = s) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_an_column_after. ff_gap_mdm_le_mdre_minor_cell_an_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_minor_cell_an = S s))) /\ (((exists ff_h_mdm_mdre_minor_cell_an_source. ff_h_mdm_mdre_minor_cell_an_source + S (b) = S ((S ((ff_row_mdm_cell_mdre_minor_cell_an) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_an))) * bc)) /\ exists ff_q_mdm_mdre_minor_cell_an_source. bb = ff_q_mdm_mdre_minor_cell_an_source * S ((S ((ff_row_mdm_cell_mdre_minor_cell_an) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_an))) * bc) + (b)))))) -> (exists ff_row_mdm_cell_mdre_minor_cell_bp ff_column_mdm_cell_mdre_minor_cell_bp. (((((exists ff_gap_mdm_lt_mdre_minor_cell_bp_row_before. ff_gap_mdm_lt_mdre_minor_cell_bp_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_minor_cell_bp = r) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_bp_row_after. ff_gap_mdm_le_mdre_minor_cell_bp_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_minor_cell_bp = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_cell_bp_column_before. ff_gap_mdm_lt_mdre_minor_cell_bp_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_minor_cell_bp = s) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_bp_column_after. ff_gap_mdm_le_mdre_minor_cell_bp_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_minor_cell_bp = S s))) /\ (((exists ff_h_mdm_mdre_minor_cell_bp_source. ff_h_mdm_mdre_minor_cell_bp_source + S (c) = S ((S ((ff_row_mdm_cell_mdre_minor_cell_bp) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_bp))) * ec)) /\ exists ff_q_mdm_mdre_minor_cell_bp_source. eb = ff_q_mdm_mdre_minor_cell_bp_source * S ((S ((ff_row_mdm_cell_mdre_minor_cell_bp) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_bp))) * ec) + (c)))))) -> (exists ff_row_mdm_cell_mdre_minor_cell_bn ff_column_mdm_cell_mdre_minor_cell_bn. (((((exists ff_gap_mdm_lt_mdre_minor_cell_bn_row_before. ff_gap_mdm_lt_mdre_minor_cell_bn_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_minor_cell_bn = r) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_bn_row_after. ff_gap_mdm_le_mdre_minor_cell_bn_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_minor_cell_bn = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_cell_bn_column_before. ff_gap_mdm_lt_mdre_minor_cell_bn_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_minor_cell_bn = s) \/ ((exists ff_gap_mdm_le_mdre_minor_cell_bn_column_after. ff_gap_mdm_le_mdre_minor_cell_bn_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_minor_cell_bn = S s))) /\ (((exists ff_h_mdm_mdre_minor_cell_bn_source. ff_h_mdm_mdre_minor_cell_bn_source + S (d) = S ((S ((ff_row_mdm_cell_mdre_minor_cell_bn) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_bn))) * fc)) /\ exists ff_q_mdm_mdre_minor_cell_bn_source. fb = ff_q_mdm_mdre_minor_cell_bn_source * S ((S ((ff_row_mdm_cell_mdre_minor_cell_bn) * (S (q)) + (ff_column_mdm_cell_mdre_minor_cell_bn))) * fc) + (d)))))) -> a + d = c + b