matrix_integer_signed_minor_balance

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc ub uc vb vc Ub Uc Vb Vc q j. (forall ics_index_signed_minor_parent ics_value0_signed_minor_parent ics_value1_signed_minor_parent ics_value2_signed_minor_parent ics_value3_signed_minor_parent. (exists ics_gap_signed_minor_parent_bound. ics_gap_signed_minor_parent_bound + S (ics_index_signed_minor_parent) = ((S q) * (S q))) -> (((exists fs_h_ics_signed_minor_parent_at0. fs_h_ics_signed_minor_parent_at0 + S (ics_value0_signed_minor_parent) = S ((S (ics_index_signed_minor_parent)) * ac)) /\ exists fs_q_ics_signed_minor_parent_at0. ab = fs_q_ics_signed_minor_parent_at0 * S ((S (ics_index_signed_minor_parent)) * ac) + (ics_value0_signed_minor_parent))) -> (((exists fs_h_ics_signed_minor_parent_at1. fs_h_ics_signed_minor_parent_at1 + S (ics_value1_signed_minor_parent) = S ((S (ics_index_signed_minor_parent)) * bc)) /\ exists fs_q_ics_signed_minor_parent_at1. bb = fs_q_ics_signed_minor_parent_at1 * S ((S (ics_index_signed_minor_parent)) * bc) + (ics_value1_signed_minor_parent))) -> (((exists fs_h_ics_signed_minor_parent_at2. fs_h_ics_signed_minor_parent_at2 + S (ics_value2_signed_minor_parent) = S ((S (ics_index_signed_minor_parent)) * ec)) /\ exists fs_q_ics_signed_minor_parent_at2. eb = fs_q_ics_signed_minor_parent_at2 * S ((S (ics_index_signed_minor_parent)) * ec) + (ics_value2_signed_minor_parent))) -> (((exists fs_h_ics_signed_minor_parent_at3. fs_h_ics_signed_minor_parent_at3 + S (ics_value3_signed_minor_parent) = S ((S (ics_index_signed_minor_parent)) * fc)) /\ exists fs_q_ics_signed_minor_parent_at3. fb = fs_q_ics_signed_minor_parent_at3 * S ((S (ics_index_signed_minor_parent)) * fc) + (ics_value3_signed_minor_parent))) -> ics_value0_signed_minor_parent + ics_value3_signed_minor_parent = ics_value2_signed_minor_parent + ics_value1_signed_minor_parent) -> (((forall ff_index_mdm_prefix_mdr_signed_minor_first_positive. (exists ff_gap_mdm_lt_mdr_signed_minor_first_positive_index_bound. ff_gap_mdm_lt_mdr_signed_minor_first_positive_index_bound + S (ff_index_mdm_prefix_mdr_signed_minor_first_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_signed_minor_first_positive ff_column_mdm_prefix_mdr_signed_minor_first_positive ff_value_mdm_prefix_mdr_signed_minor_first_positive. (ff_index_mdm_prefix_mdr_signed_minor_first_positive = (q) * ff_row_mdm_prefix_mdr_signed_minor_first_positive + ff_column_mdm_prefix_mdr_signed_minor_first_positive /\ ((exists ff_gap_mdm_lt_mdr_signed_minor_first_positive_column_bound. ff_gap_mdm_lt_mdr_signed_minor_first_positive_column_bound + S (ff_column_mdm_prefix_mdr_signed_minor_first_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_signed_minor_first_positive_cell ff_column_mdm_cell_mdr_signed_minor_first_positive_cell. (((((exists ff_gap_mdm_lt_mdr_signed_minor_first_positive_cell_row_before. ff_gap_mdm_lt_mdr_signed_minor_first_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_signed_minor_first_positive) = (0)) /\ ff_row_mdm_cell_mdr_signed_minor_first_positive_cell = ff_row_mdm_prefix_mdr_signed_minor_first_positive) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_first_positive_cell_row_after. ff_gap_mdm_le_mdr_signed_minor_first_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_signed_minor_first_positive)) /\ ff_row_mdm_cell_mdr_signed_minor_first_positive_cell = S ff_row_mdm_prefix_mdr_signed_minor_first_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_signed_minor_first_positive_cell_column_before. ff_gap_mdm_lt_mdr_signed_minor_first_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_signed_minor_first_positive) = (j)) /\ ff_column_mdm_cell_mdr_signed_minor_first_positive_cell = ff_column_mdm_prefix_mdr_signed_minor_first_positive) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_first_positive_cell_column_after. ff_gap_mdm_le_mdr_signed_minor_first_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_signed_minor_first_positive)) /\ ff_column_mdm_cell_mdr_signed_minor_first_positive_cell = S ff_column_mdm_prefix_mdr_signed_minor_first_positive))) /\ (((exists ff_h_mdm_mdr_signed_minor_first_positive_cell_source. ff_h_mdm_mdr_signed_minor_first_positive_cell_source + S (ff_value_mdm_prefix_mdr_signed_minor_first_positive) = S ((S ((ff_row_mdm_cell_mdr_signed_minor_first_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_first_positive_cell))) * ac)) /\ exists ff_q_mdm_mdr_signed_minor_first_positive_cell_source. ab = ff_q_mdm_mdr_signed_minor_first_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_signed_minor_first_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_first_positive_cell))) * ac) + (ff_value_mdm_prefix_mdr_signed_minor_first_positive)))))) /\ (((exists ff_h_mdm_mdr_signed_minor_first_positive_target. ff_h_mdm_mdr_signed_minor_first_positive_target + S (ff_value_mdm_prefix_mdr_signed_minor_first_positive) = S ((S (ff_index_mdm_prefix_mdr_signed_minor_first_positive)) * uc)) /\ exists ff_q_mdm_mdr_signed_minor_first_positive_target. ub = ff_q_mdm_mdr_signed_minor_first_positive_target * S ((S (ff_index_mdm_prefix_mdr_signed_minor_first_positive)) * uc) + (ff_value_mdm_prefix_mdr_signed_minor_first_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_signed_minor_first_negative. (exists ff_gap_mdm_lt_mdr_signed_minor_first_negative_index_bound. ff_gap_mdm_lt_mdr_signed_minor_first_negative_index_bound + S (ff_index_mdm_prefix_mdr_signed_minor_first_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_signed_minor_first_negative ff_column_mdm_prefix_mdr_signed_minor_first_negative ff_value_mdm_prefix_mdr_signed_minor_first_negative. (ff_index_mdm_prefix_mdr_signed_minor_first_negative = (q) * ff_row_mdm_prefix_mdr_signed_minor_first_negative + ff_column_mdm_prefix_mdr_signed_minor_first_negative /\ ((exists ff_gap_mdm_lt_mdr_signed_minor_first_negative_column_bound. ff_gap_mdm_lt_mdr_signed_minor_first_negative_column_bound + S (ff_column_mdm_prefix_mdr_signed_minor_first_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_signed_minor_first_negative_cell ff_column_mdm_cell_mdr_signed_minor_first_negative_cell. (((((exists ff_gap_mdm_lt_mdr_signed_minor_first_negative_cell_row_before. ff_gap_mdm_lt_mdr_signed_minor_first_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_signed_minor_first_negative) = (0)) /\ ff_row_mdm_cell_mdr_signed_minor_first_negative_cell = ff_row_mdm_prefix_mdr_signed_minor_first_negative) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_first_negative_cell_row_after. ff_gap_mdm_le_mdr_signed_minor_first_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_signed_minor_first_negative)) /\ ff_row_mdm_cell_mdr_signed_minor_first_negative_cell = S ff_row_mdm_prefix_mdr_signed_minor_first_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_signed_minor_first_negative_cell_column_before. ff_gap_mdm_lt_mdr_signed_minor_first_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_signed_minor_first_negative) = (j)) /\ ff_column_mdm_cell_mdr_signed_minor_first_negative_cell = ff_column_mdm_prefix_mdr_signed_minor_first_negative) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_first_negative_cell_column_after. ff_gap_mdm_le_mdr_signed_minor_first_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_signed_minor_first_negative)) /\ ff_column_mdm_cell_mdr_signed_minor_first_negative_cell = S ff_column_mdm_prefix_mdr_signed_minor_first_negative))) /\ (((exists ff_h_mdm_mdr_signed_minor_first_negative_cell_source. ff_h_mdm_mdr_signed_minor_first_negative_cell_source + S (ff_value_mdm_prefix_mdr_signed_minor_first_negative) = S ((S ((ff_row_mdm_cell_mdr_signed_minor_first_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_first_negative_cell))) * bc)) /\ exists ff_q_mdm_mdr_signed_minor_first_negative_cell_source. bb = ff_q_mdm_mdr_signed_minor_first_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_signed_minor_first_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_first_negative_cell))) * bc) + (ff_value_mdm_prefix_mdr_signed_minor_first_negative)))))) /\ (((exists ff_h_mdm_mdr_signed_minor_first_negative_target. ff_h_mdm_mdr_signed_minor_first_negative_target + S (ff_value_mdm_prefix_mdr_signed_minor_first_negative) = S ((S (ff_index_mdm_prefix_mdr_signed_minor_first_negative)) * vc)) /\ exists ff_q_mdm_mdr_signed_minor_first_negative_target. vb = ff_q_mdm_mdr_signed_minor_first_negative_target * S ((S (ff_index_mdm_prefix_mdr_signed_minor_first_negative)) * vc) + (ff_value_mdm_prefix_mdr_signed_minor_first_negative))))))))) -> (((forall ff_index_mdm_prefix_mdr_signed_minor_second_positive. (exists ff_gap_mdm_lt_mdr_signed_minor_second_positive_index_bound. ff_gap_mdm_lt_mdr_signed_minor_second_positive_index_bound + S (ff_index_mdm_prefix_mdr_signed_minor_second_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_signed_minor_second_positive ff_column_mdm_prefix_mdr_signed_minor_second_positive ff_value_mdm_prefix_mdr_signed_minor_second_positive. (ff_index_mdm_prefix_mdr_signed_minor_second_positive = (q) * ff_row_mdm_prefix_mdr_signed_minor_second_positive + ff_column_mdm_prefix_mdr_signed_minor_second_positive /\ ((exists ff_gap_mdm_lt_mdr_signed_minor_second_positive_column_bound. ff_gap_mdm_lt_mdr_signed_minor_second_positive_column_bound + S (ff_column_mdm_prefix_mdr_signed_minor_second_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_signed_minor_second_positive_cell ff_column_mdm_cell_mdr_signed_minor_second_positive_cell. (((((exists ff_gap_mdm_lt_mdr_signed_minor_second_positive_cell_row_before. ff_gap_mdm_lt_mdr_signed_minor_second_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_signed_minor_second_positive) = (0)) /\ ff_row_mdm_cell_mdr_signed_minor_second_positive_cell = ff_row_mdm_prefix_mdr_signed_minor_second_positive) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_second_positive_cell_row_after. ff_gap_mdm_le_mdr_signed_minor_second_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_signed_minor_second_positive)) /\ ff_row_mdm_cell_mdr_signed_minor_second_positive_cell = S ff_row_mdm_prefix_mdr_signed_minor_second_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_signed_minor_second_positive_cell_column_before. ff_gap_mdm_lt_mdr_signed_minor_second_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_signed_minor_second_positive) = (j)) /\ ff_column_mdm_cell_mdr_signed_minor_second_positive_cell = ff_column_mdm_prefix_mdr_signed_minor_second_positive) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_second_positive_cell_column_after. ff_gap_mdm_le_mdr_signed_minor_second_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_signed_minor_second_positive)) /\ ff_column_mdm_cell_mdr_signed_minor_second_positive_cell = S ff_column_mdm_prefix_mdr_signed_minor_second_positive))) /\ (((exists ff_h_mdm_mdr_signed_minor_second_positive_cell_source. ff_h_mdm_mdr_signed_minor_second_positive_cell_source + S (ff_value_mdm_prefix_mdr_signed_minor_second_positive) = S ((S ((ff_row_mdm_cell_mdr_signed_minor_second_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_second_positive_cell))) * ec)) /\ exists ff_q_mdm_mdr_signed_minor_second_positive_cell_source. eb = ff_q_mdm_mdr_signed_minor_second_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_signed_minor_second_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_second_positive_cell))) * ec) + (ff_value_mdm_prefix_mdr_signed_minor_second_positive)))))) /\ (((exists ff_h_mdm_mdr_signed_minor_second_positive_target. ff_h_mdm_mdr_signed_minor_second_positive_target + S (ff_value_mdm_prefix_mdr_signed_minor_second_positive) = S ((S (ff_index_mdm_prefix_mdr_signed_minor_second_positive)) * Uc)) /\ exists ff_q_mdm_mdr_signed_minor_second_positive_target. Ub = ff_q_mdm_mdr_signed_minor_second_positive_target * S ((S (ff_index_mdm_prefix_mdr_signed_minor_second_positive)) * Uc) + (ff_value_mdm_prefix_mdr_signed_minor_second_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_signed_minor_second_negative. (exists ff_gap_mdm_lt_mdr_signed_minor_second_negative_index_bound. ff_gap_mdm_lt_mdr_signed_minor_second_negative_index_bound + S (ff_index_mdm_prefix_mdr_signed_minor_second_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_signed_minor_second_negative ff_column_mdm_prefix_mdr_signed_minor_second_negative ff_value_mdm_prefix_mdr_signed_minor_second_negative. (ff_index_mdm_prefix_mdr_signed_minor_second_negative = (q) * ff_row_mdm_prefix_mdr_signed_minor_second_negative + ff_column_mdm_prefix_mdr_signed_minor_second_negative /\ ((exists ff_gap_mdm_lt_mdr_signed_minor_second_negative_column_bound. ff_gap_mdm_lt_mdr_signed_minor_second_negative_column_bound + S (ff_column_mdm_prefix_mdr_signed_minor_second_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_signed_minor_second_negative_cell ff_column_mdm_cell_mdr_signed_minor_second_negative_cell. (((((exists ff_gap_mdm_lt_mdr_signed_minor_second_negative_cell_row_before. ff_gap_mdm_lt_mdr_signed_minor_second_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_signed_minor_second_negative) = (0)) /\ ff_row_mdm_cell_mdr_signed_minor_second_negative_cell = ff_row_mdm_prefix_mdr_signed_minor_second_negative) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_second_negative_cell_row_after. ff_gap_mdm_le_mdr_signed_minor_second_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_signed_minor_second_negative)) /\ ff_row_mdm_cell_mdr_signed_minor_second_negative_cell = S ff_row_mdm_prefix_mdr_signed_minor_second_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_signed_minor_second_negative_cell_column_before. ff_gap_mdm_lt_mdr_signed_minor_second_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_signed_minor_second_negative) = (j)) /\ ff_column_mdm_cell_mdr_signed_minor_second_negative_cell = ff_column_mdm_prefix_mdr_signed_minor_second_negative) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_second_negative_cell_column_after. ff_gap_mdm_le_mdr_signed_minor_second_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_signed_minor_second_negative)) /\ ff_column_mdm_cell_mdr_signed_minor_second_negative_cell = S ff_column_mdm_prefix_mdr_signed_minor_second_negative))) /\ (((exists ff_h_mdm_mdr_signed_minor_second_negative_cell_source. ff_h_mdm_mdr_signed_minor_second_negative_cell_source + S (ff_value_mdm_prefix_mdr_signed_minor_second_negative) = S ((S ((ff_row_mdm_cell_mdr_signed_minor_second_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_second_negative_cell))) * fc)) /\ exists ff_q_mdm_mdr_signed_minor_second_negative_cell_source. fb = ff_q_mdm_mdr_signed_minor_second_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_signed_minor_second_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_second_negative_cell))) * fc) + (ff_value_mdm_prefix_mdr_signed_minor_second_negative)))))) /\ (((exists ff_h_mdm_mdr_signed_minor_second_negative_target. ff_h_mdm_mdr_signed_minor_second_negative_target + S (ff_value_mdm_prefix_mdr_signed_minor_second_negative) = S ((S (ff_index_mdm_prefix_mdr_signed_minor_second_negative)) * Vc)) /\ exists ff_q_mdm_mdr_signed_minor_second_negative_target. Vb = ff_q_mdm_mdr_signed_minor_second_negative_target * S ((S (ff_index_mdm_prefix_mdr_signed_minor_second_negative)) * Vc) + (ff_value_mdm_prefix_mdr_signed_minor_second_negative))))))))) -> (forall ics_index_signed_minor_equal ics_value0_signed_minor_equal ics_value1_signed_minor_equal ics_value2_signed_minor_equal ics_value3_signed_minor_equal. (exists ics_gap_signed_minor_equal_bound. ics_gap_signed_minor_equal_bound + S (ics_index_signed_minor_equal) = ((q) * (q))) -> (((exists fs_h_ics_signed_minor_equal_at0. fs_h_ics_signed_minor_equal_at0 + S (ics_value0_signed_minor_equal) = S ((S (ics_index_signed_minor_equal)) * uc)) /\ exists fs_q_ics_signed_minor_equal_at0. ub = fs_q_ics_signed_minor_equal_at0 * S ((S (ics_index_signed_minor_equal)) * uc) + (ics_value0_signed_minor_equal))) -> (((exists fs_h_ics_signed_minor_equal_at1. fs_h_ics_signed_minor_equal_at1 + S (ics_value1_signed_minor_equal) = S ((S (ics_index_signed_minor_equal)) * vc)) /\ exists fs_q_ics_signed_minor_equal_at1. vb = fs_q_ics_signed_minor_equal_at1 * S ((S (ics_index_signed_minor_equal)) * vc) + (ics_value1_signed_minor_equal))) -> (((exists fs_h_ics_signed_minor_equal_at2. fs_h_ics_signed_minor_equal_at2 + S (ics_value2_signed_minor_equal) = S ((S (ics_index_signed_minor_equal)) * Uc)) /\ exists fs_q_ics_signed_minor_equal_at2. Ub = fs_q_ics_signed_minor_equal_at2 * S ((S (ics_index_signed_minor_equal)) * Uc) + (ics_value2_signed_minor_equal))) -> (((exists fs_h_ics_signed_minor_equal_at3. fs_h_ics_signed_minor_equal_at3 + S (ics_value3_signed_minor_equal) = S ((S (ics_index_signed_minor_equal)) * Vc)) /\ exists fs_q_ics_signed_minor_equal_at3. Vb = fs_q_ics_signed_minor_equal_at3 * S ((S (ics_index_signed_minor_equal)) * Vc) + (ics_value3_signed_minor_equal))) -> ics_value0_signed_minor_equal + ics_value3_signed_minor_equal = ics_value2_signed_minor_equal + ics_value1_signed_minor_equal)