matrix_integer_alternating_prefix_balance

forall ab ac bb bc cb cc db dc eb ec fb fc gb gc hb hc ub uc vb vc Ub Uc Vb Vc l. (forall ics_index_prefix_rows_equal ics_value0_prefix_rows_equal ics_value1_prefix_rows_equal ics_value2_prefix_rows_equal ics_value3_prefix_rows_equal. (exists ics_gap_prefix_rows_equal_bound. ics_gap_prefix_rows_equal_bound + S (ics_index_prefix_rows_equal) = (l)) -> (((exists fs_h_ics_prefix_rows_equal_at0. fs_h_ics_prefix_rows_equal_at0 + S (ics_value0_prefix_rows_equal) = S ((S (ics_index_prefix_rows_equal)) * ac)) /\ exists fs_q_ics_prefix_rows_equal_at0. ab = fs_q_ics_prefix_rows_equal_at0 * S ((S (ics_index_prefix_rows_equal)) * ac) + (ics_value0_prefix_rows_equal))) -> (((exists fs_h_ics_prefix_rows_equal_at1. fs_h_ics_prefix_rows_equal_at1 + S (ics_value1_prefix_rows_equal) = S ((S (ics_index_prefix_rows_equal)) * bc)) /\ exists fs_q_ics_prefix_rows_equal_at1. bb = fs_q_ics_prefix_rows_equal_at1 * S ((S (ics_index_prefix_rows_equal)) * bc) + (ics_value1_prefix_rows_equal))) -> (((exists fs_h_ics_prefix_rows_equal_at2. fs_h_ics_prefix_rows_equal_at2 + S (ics_value2_prefix_rows_equal) = S ((S (ics_index_prefix_rows_equal)) * ec)) /\ exists fs_q_ics_prefix_rows_equal_at2. eb = fs_q_ics_prefix_rows_equal_at2 * S ((S (ics_index_prefix_rows_equal)) * ec) + (ics_value2_prefix_rows_equal))) -> (((exists fs_h_ics_prefix_rows_equal_at3. fs_h_ics_prefix_rows_equal_at3 + S (ics_value3_prefix_rows_equal) = S ((S (ics_index_prefix_rows_equal)) * fc)) /\ exists fs_q_ics_prefix_rows_equal_at3. fb = fs_q_ics_prefix_rows_equal_at3 * S ((S (ics_index_prefix_rows_equal)) * fc) + (ics_value3_prefix_rows_equal))) -> ics_value0_prefix_rows_equal + ics_value3_prefix_rows_equal = ics_value2_prefix_rows_equal + ics_value1_prefix_rows_equal) -> (forall ics_index_prefix_cofactors_equal ics_value0_prefix_cofactors_equal ics_value1_prefix_cofactors_equal ics_value2_prefix_cofactors_equal ics_value3_prefix_cofactors_equal. (exists ics_gap_prefix_cofactors_equal_bound. ics_gap_prefix_cofactors_equal_bound + S (ics_index_prefix_cofactors_equal) = (l)) -> (((exists fs_h_ics_prefix_cofactors_equal_at0. fs_h_ics_prefix_cofactors_equal_at0 + S (ics_value0_prefix_cofactors_equal) = S ((S (ics_index_prefix_cofactors_equal)) * cc)) /\ exists fs_q_ics_prefix_cofactors_equal_at0. cb = fs_q_ics_prefix_cofactors_equal_at0 * S ((S (ics_index_prefix_cofactors_equal)) * cc) + (ics_value0_prefix_cofactors_equal))) -> (((exists fs_h_ics_prefix_cofactors_equal_at1. fs_h_ics_prefix_cofactors_equal_at1 + S (ics_value1_prefix_cofactors_equal) = S ((S (ics_index_prefix_cofactors_equal)) * dc)) /\ exists fs_q_ics_prefix_cofactors_equal_at1. db = fs_q_ics_prefix_cofactors_equal_at1 * S ((S (ics_index_prefix_cofactors_equal)) * dc) + (ics_value1_prefix_cofactors_equal))) -> (((exists fs_h_ics_prefix_cofactors_equal_at2. fs_h_ics_prefix_cofactors_equal_at2 + S (ics_value2_prefix_cofactors_equal) = S ((S (ics_index_prefix_cofactors_equal)) * gc)) /\ exists fs_q_ics_prefix_cofactors_equal_at2. gb = fs_q_ics_prefix_cofactors_equal_at2 * S ((S (ics_index_prefix_cofactors_equal)) * gc) + (ics_value2_prefix_cofactors_equal))) -> (((exists fs_h_ics_prefix_cofactors_equal_at3. fs_h_ics_prefix_cofactors_equal_at3 + S (ics_value3_prefix_cofactors_equal) = S ((S (ics_index_prefix_cofactors_equal)) * hc)) /\ exists fs_q_ics_prefix_cofactors_equal_at3. hb = fs_q_ics_prefix_cofactors_equal_at3 * S ((S (ics_index_prefix_cofactors_equal)) * hc) + (ics_value3_prefix_cofactors_equal))) -> ics_value0_prefix_cofactors_equal + ics_value3_prefix_cofactors_equal = ics_value2_prefix_cofactors_equal + ics_value1_prefix_cofactors_equal) -> (forall ff_index_mce_alternating_integer_prefix_first. (exists ff_gap_mce_integer_prefix_first_index. ff_gap_mce_integer_prefix_first_index + S (ff_index_mce_alternating_integer_prefix_first) = (l)) -> exists ff_ap_mce_alternating_integer_prefix_first ff_an_mce_alternating_integer_prefix_first ff_bp_mce_alternating_integer_prefix_first ff_bn_mce_alternating_integer_prefix_first ff_p_mce_alternating_integer_prefix_first ff_n_mce_alternating_integer_prefix_first. ((((exists ff_h_mce_integer_prefix_first_ap. ff_h_mce_integer_prefix_first_ap + S (ff_ap_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * ac)) /\ exists ff_q_mce_integer_prefix_first_ap. ab = ff_q_mce_integer_prefix_first_ap * S ((S (ff_index_mce_alternating_integer_prefix_first)) * ac) + (ff_ap_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_an. ff_h_mce_integer_prefix_first_an + S (ff_an_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * bc)) /\ exists ff_q_mce_integer_prefix_first_an. bb = ff_q_mce_integer_prefix_first_an * S ((S (ff_index_mce_alternating_integer_prefix_first)) * bc) + (ff_an_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_bp. ff_h_mce_integer_prefix_first_bp + S (ff_bp_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * cc)) /\ exists ff_q_mce_integer_prefix_first_bp. cb = ff_q_mce_integer_prefix_first_bp * S ((S (ff_index_mce_alternating_integer_prefix_first)) * cc) + (ff_bp_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_bn. ff_h_mce_integer_prefix_first_bn + S (ff_bn_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * dc)) /\ exists ff_q_mce_integer_prefix_first_bn. db = ff_q_mce_integer_prefix_first_bn * S ((S (ff_index_mce_alternating_integer_prefix_first)) * dc) + (ff_bn_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_positive. ff_h_mce_integer_prefix_first_positive + S (ff_p_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * uc)) /\ exists ff_q_mce_integer_prefix_first_positive. ub = ff_q_mce_integer_prefix_first_positive * S ((S (ff_index_mce_alternating_integer_prefix_first)) * uc) + (ff_p_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_negative. ff_h_mce_integer_prefix_first_negative + S (ff_n_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * vc)) /\ exists ff_q_mce_integer_prefix_first_negative. vb = ff_q_mce_integer_prefix_first_negative * S ((S (ff_index_mce_alternating_integer_prefix_first)) * vc) + (ff_n_mce_alternating_integer_prefix_first))) /\ (((exists ff_even_mce_term_integer_prefix_first_term. ff_index_mce_alternating_integer_prefix_first = 2 * ff_even_mce_term_integer_prefix_first_term) /\ (ff_p_mce_alternating_integer_prefix_first = (ff_ap_mce_alternating_integer_prefix_first) * (ff_bp_mce_alternating_integer_prefix_first) + (ff_an_mce_alternating_integer_prefix_first) * (ff_bn_mce_alternating_integer_prefix_first) /\ ff_n_mce_alternating_integer_prefix_first = (ff_ap_mce_alternating_integer_prefix_first) * (ff_bn_mce_alternating_integer_prefix_first) + (ff_an_mce_alternating_integer_prefix_first) * (ff_bp_mce_alternating_integer_prefix_first))) \/ ((exists ff_odd_mce_term_integer_prefix_first_term. ff_index_mce_alternating_integer_prefix_first = 2 * ff_odd_mce_term_integer_prefix_first_term + 1) /\ (ff_p_mce_alternating_integer_prefix_first = (ff_ap_mce_alternating_integer_prefix_first) * (ff_bn_mce_alternating_integer_prefix_first) + (ff_an_mce_alternating_integer_prefix_first) * (ff_bp_mce_alternating_integer_prefix_first) /\ ff_n_mce_alternating_integer_prefix_first = (ff_ap_mce_alternating_integer_prefix_first) * (ff_bp_mce_alternating_integer_prefix_first) + (ff_an_mce_alternating_integer_prefix_first) * (ff_bn_mce_alternating_integer_prefix_first))))))))))) -> (forall ff_index_mce_alternating_integer_prefix_second. (exists ff_gap_mce_integer_prefix_second_index. ff_gap_mce_integer_prefix_second_index + S (ff_index_mce_alternating_integer_prefix_second) = (l)) -> exists ff_ap_mce_alternating_integer_prefix_second ff_an_mce_alternating_integer_prefix_second ff_bp_mce_alternating_integer_prefix_second ff_bn_mce_alternating_integer_prefix_second ff_p_mce_alternating_integer_prefix_second ff_n_mce_alternating_integer_prefix_second. ((((exists ff_h_mce_integer_prefix_second_ap. ff_h_mce_integer_prefix_second_ap + S (ff_ap_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * ec)) /\ exists ff_q_mce_integer_prefix_second_ap. eb = ff_q_mce_integer_prefix_second_ap * S ((S (ff_index_mce_alternating_integer_prefix_second)) * ec) + (ff_ap_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_an. ff_h_mce_integer_prefix_second_an + S (ff_an_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * fc)) /\ exists ff_q_mce_integer_prefix_second_an. fb = ff_q_mce_integer_prefix_second_an * S ((S (ff_index_mce_alternating_integer_prefix_second)) * fc) + (ff_an_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_bp. ff_h_mce_integer_prefix_second_bp + S (ff_bp_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * gc)) /\ exists ff_q_mce_integer_prefix_second_bp. gb = ff_q_mce_integer_prefix_second_bp * S ((S (ff_index_mce_alternating_integer_prefix_second)) * gc) + (ff_bp_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_bn. ff_h_mce_integer_prefix_second_bn + S (ff_bn_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * hc)) /\ exists ff_q_mce_integer_prefix_second_bn. hb = ff_q_mce_integer_prefix_second_bn * S ((S (ff_index_mce_alternating_integer_prefix_second)) * hc) + (ff_bn_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_positive. ff_h_mce_integer_prefix_second_positive + S (ff_p_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * Uc)) /\ exists ff_q_mce_integer_prefix_second_positive. Ub = ff_q_mce_integer_prefix_second_positive * S ((S (ff_index_mce_alternating_integer_prefix_second)) * Uc) + (ff_p_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_negative. ff_h_mce_integer_prefix_second_negative + S (ff_n_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * Vc)) /\ exists ff_q_mce_integer_prefix_second_negative. Vb = ff_q_mce_integer_prefix_second_negative * S ((S (ff_index_mce_alternating_integer_prefix_second)) * Vc) + (ff_n_mce_alternating_integer_prefix_second))) /\ (((exists ff_even_mce_term_integer_prefix_second_term. ff_index_mce_alternating_integer_prefix_second = 2 * ff_even_mce_term_integer_prefix_second_term) /\ (ff_p_mce_alternating_integer_prefix_second = (ff_ap_mce_alternating_integer_prefix_second) * (ff_bp_mce_alternating_integer_prefix_second) + (ff_an_mce_alternating_integer_prefix_second) * (ff_bn_mce_alternating_integer_prefix_second) /\ ff_n_mce_alternating_integer_prefix_second = (ff_ap_mce_alternating_integer_prefix_second) * (ff_bn_mce_alternating_integer_prefix_second) + (ff_an_mce_alternating_integer_prefix_second) * (ff_bp_mce_alternating_integer_prefix_second))) \/ ((exists ff_odd_mce_term_integer_prefix_second_term. ff_index_mce_alternating_integer_prefix_second = 2 * ff_odd_mce_term_integer_prefix_second_term + 1) /\ (ff_p_mce_alternating_integer_prefix_second = (ff_ap_mce_alternating_integer_prefix_second) * (ff_bn_mce_alternating_integer_prefix_second) + (ff_an_mce_alternating_integer_prefix_second) * (ff_bp_mce_alternating_integer_prefix_second) /\ ff_n_mce_alternating_integer_prefix_second = (ff_ap_mce_alternating_integer_prefix_second) * (ff_bp_mce_alternating_integer_prefix_second) + (ff_an_mce_alternating_integer_prefix_second) * (ff_bn_mce_alternating_integer_prefix_second))))))))))) -> (forall ics_index_prefix_outputs_equal ics_value0_prefix_outputs_equal ics_value1_prefix_outputs_equal ics_value2_prefix_outputs_equal ics_value3_prefix_outputs_equal. (exists ics_gap_prefix_outputs_equal_bound. ics_gap_prefix_outputs_equal_bound + S (ics_index_prefix_outputs_equal) = (l)) -> (((exists fs_h_ics_prefix_outputs_equal_at0. fs_h_ics_prefix_outputs_equal_at0 + S (ics_value0_prefix_outputs_equal) = S ((S (ics_index_prefix_outputs_equal)) * uc)) /\ exists fs_q_ics_prefix_outputs_equal_at0. ub = fs_q_ics_prefix_outputs_equal_at0 * S ((S (ics_index_prefix_outputs_equal)) * uc) + (ics_value0_prefix_outputs_equal))) -> (((exists fs_h_ics_prefix_outputs_equal_at1. fs_h_ics_prefix_outputs_equal_at1 + S (ics_value1_prefix_outputs_equal) = S ((S (ics_index_prefix_outputs_equal)) * vc)) /\ exists fs_q_ics_prefix_outputs_equal_at1. vb = fs_q_ics_prefix_outputs_equal_at1 * S ((S (ics_index_prefix_outputs_equal)) * vc) + (ics_value1_prefix_outputs_equal))) -> (((exists fs_h_ics_prefix_outputs_equal_at2. fs_h_ics_prefix_outputs_equal_at2 + S (ics_value2_prefix_outputs_equal) = S ((S (ics_index_prefix_outputs_equal)) * Uc)) /\ exists fs_q_ics_prefix_outputs_equal_at2. Ub = fs_q_ics_prefix_outputs_equal_at2 * S ((S (ics_index_prefix_outputs_equal)) * Uc) + (ics_value2_prefix_outputs_equal))) -> (((exists fs_h_ics_prefix_outputs_equal_at3. fs_h_ics_prefix_outputs_equal_at3 + S (ics_value3_prefix_outputs_equal) = S ((S (ics_index_prefix_outputs_equal)) * Vc)) /\ exists fs_q_ics_prefix_outputs_equal_at3. Vb = fs_q_ics_prefix_outputs_equal_at3 * S ((S (ics_index_prefix_outputs_equal)) * Vc) + (ics_value3_prefix_outputs_equal))) -> ics_value0_prefix_outputs_equal + ics_value3_prefix_outputs_equal = ics_value2_prefix_outputs_equal + ics_value1_prefix_outputs_equal)