matrix_integer_cofactor_fold_balance

Exact expanded first-order arithmetic statement

forall ab ac bb bc cb cc db dc eb ec fb fc gb gc hb hc l p n P N. (forall ics_index_fold_rows_equal ics_value0_fold_rows_equal ics_value1_fold_rows_equal ics_value2_fold_rows_equal ics_value3_fold_rows_equal. (exists ics_gap_fold_rows_equal_bound. ics_gap_fold_rows_equal_bound + S (ics_index_fold_rows_equal) = (l)) -> (((exists fs_h_ics_fold_rows_equal_at0. fs_h_ics_fold_rows_equal_at0 + S (ics_value0_fold_rows_equal) = S ((S (ics_index_fold_rows_equal)) * ac)) /\ exists fs_q_ics_fold_rows_equal_at0. ab = fs_q_ics_fold_rows_equal_at0 * S ((S (ics_index_fold_rows_equal)) * ac) + (ics_value0_fold_rows_equal))) -> (((exists fs_h_ics_fold_rows_equal_at1. fs_h_ics_fold_rows_equal_at1 + S (ics_value1_fold_rows_equal) = S ((S (ics_index_fold_rows_equal)) * bc)) /\ exists fs_q_ics_fold_rows_equal_at1. bb = fs_q_ics_fold_rows_equal_at1 * S ((S (ics_index_fold_rows_equal)) * bc) + (ics_value1_fold_rows_equal))) -> (((exists fs_h_ics_fold_rows_equal_at2. fs_h_ics_fold_rows_equal_at2 + S (ics_value2_fold_rows_equal) = S ((S (ics_index_fold_rows_equal)) * ec)) /\ exists fs_q_ics_fold_rows_equal_at2. eb = fs_q_ics_fold_rows_equal_at2 * S ((S (ics_index_fold_rows_equal)) * ec) + (ics_value2_fold_rows_equal))) -> (((exists fs_h_ics_fold_rows_equal_at3. fs_h_ics_fold_rows_equal_at3 + S (ics_value3_fold_rows_equal) = S ((S (ics_index_fold_rows_equal)) * fc)) /\ exists fs_q_ics_fold_rows_equal_at3. fb = fs_q_ics_fold_rows_equal_at3 * S ((S (ics_index_fold_rows_equal)) * fc) + (ics_value3_fold_rows_equal))) -> ics_value0_fold_rows_equal + ics_value3_fold_rows_equal = ics_value2_fold_rows_equal + ics_value1_fold_rows_equal) -> (forall ics_index_fold_cofactors_equal ics_value0_fold_cofactors_equal ics_value1_fold_cofactors_equal ics_value2_fold_cofactors_equal ics_value3_fold_cofactors_equal. (exists ics_gap_fold_cofactors_equal_bound. ics_gap_fold_cofactors_equal_bound + S (ics_index_fold_cofactors_equal) = (l)) -> (((exists fs_h_ics_fold_cofactors_equal_at0. fs_h_ics_fold_cofactors_equal_at0 + S (ics_value0_fold_cofactors_equal) = S ((S (ics_index_fold_cofactors_equal)) * cc)) /\ exists fs_q_ics_fold_cofactors_equal_at0. cb = fs_q_ics_fold_cofactors_equal_at0 * S ((S (ics_index_fold_cofactors_equal)) * cc) + (ics_value0_fold_cofactors_equal))) -> (((exists fs_h_ics_fold_cofactors_equal_at1. fs_h_ics_fold_cofactors_equal_at1 + S (ics_value1_fold_cofactors_equal) = S ((S (ics_index_fold_cofactors_equal)) * dc)) /\ exists fs_q_ics_fold_cofactors_equal_at1. db = fs_q_ics_fold_cofactors_equal_at1 * S ((S (ics_index_fold_cofactors_equal)) * dc) + (ics_value1_fold_cofactors_equal))) -> (((exists fs_h_ics_fold_cofactors_equal_at2. fs_h_ics_fold_cofactors_equal_at2 + S (ics_value2_fold_cofactors_equal) = S ((S (ics_index_fold_cofactors_equal)) * gc)) /\ exists fs_q_ics_fold_cofactors_equal_at2. gb = fs_q_ics_fold_cofactors_equal_at2 * S ((S (ics_index_fold_cofactors_equal)) * gc) + (ics_value2_fold_cofactors_equal))) -> (((exists fs_h_ics_fold_cofactors_equal_at3. fs_h_ics_fold_cofactors_equal_at3 + S (ics_value3_fold_cofactors_equal) = S ((S (ics_index_fold_cofactors_equal)) * hc)) /\ exists fs_q_ics_fold_cofactors_equal_at3. hb = fs_q_ics_fold_cofactors_equal_at3 * S ((S (ics_index_fold_cofactors_equal)) * hc) + (ics_value3_fold_cofactors_equal))) -> ics_value0_fold_cofactors_equal + ics_value3_fold_cofactors_equal = ics_value2_fold_cofactors_equal + ics_value1_fold_cofactors_equal) -> (exists ff_ub_mce_fold_integer_fold_first ff_uc_mce_fold_integer_fold_first ff_vb_mce_fold_integer_fold_first ff_vc_mce_fold_integer_fold_first. ((forall ff_index_mce_alternating_integer_fold_first_prefix. (exists ff_gap_mce_integer_fold_first_prefix_index. ff_gap_mce_integer_fold_first_prefix_index + S (ff_index_mce_alternating_integer_fold_first_prefix) = (l)) -> exists ff_ap_mce_alternating_integer_fold_first_prefix ff_an_mce_alternating_integer_fold_first_prefix ff_bp_mce_alternating_integer_fold_first_prefix ff_bn_mce_alternating_integer_fold_first_prefix ff_p_mce_alternating_integer_fold_first_prefix ff_n_mce_alternating_integer_fold_first_prefix. ((((exists ff_h_mce_integer_fold_first_prefix_ap. ff_h_mce_integer_fold_first_prefix_ap + S (ff_ap_mce_alternating_integer_fold_first_prefix) = S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * ac)) /\ exists ff_q_mce_integer_fold_first_prefix_ap. ab = ff_q_mce_integer_fold_first_prefix_ap * S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * ac) + (ff_ap_mce_alternating_integer_fold_first_prefix))) /\ ((((exists ff_h_mce_integer_fold_first_prefix_an. ff_h_mce_integer_fold_first_prefix_an + S (ff_an_mce_alternating_integer_fold_first_prefix) = S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * bc)) /\ exists ff_q_mce_integer_fold_first_prefix_an. bb = ff_q_mce_integer_fold_first_prefix_an * S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * bc) + (ff_an_mce_alternating_integer_fold_first_prefix))) /\ ((((exists ff_h_mce_integer_fold_first_prefix_bp. ff_h_mce_integer_fold_first_prefix_bp + S (ff_bp_mce_alternating_integer_fold_first_prefix) = S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * cc)) /\ exists ff_q_mce_integer_fold_first_prefix_bp. cb = ff_q_mce_integer_fold_first_prefix_bp * S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * cc) + (ff_bp_mce_alternating_integer_fold_first_prefix))) /\ ((((exists ff_h_mce_integer_fold_first_prefix_bn. ff_h_mce_integer_fold_first_prefix_bn + S (ff_bn_mce_alternating_integer_fold_first_prefix) = S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * dc)) /\ exists ff_q_mce_integer_fold_first_prefix_bn. db = ff_q_mce_integer_fold_first_prefix_bn * S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * dc) + (ff_bn_mce_alternating_integer_fold_first_prefix))) /\ ((((exists ff_h_mce_integer_fold_first_prefix_positive. ff_h_mce_integer_fold_first_prefix_positive + S (ff_p_mce_alternating_integer_fold_first_prefix) = S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * ff_uc_mce_fold_integer_fold_first)) /\ exists ff_q_mce_integer_fold_first_prefix_positive. ff_ub_mce_fold_integer_fold_first = ff_q_mce_integer_fold_first_prefix_positive * S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * ff_uc_mce_fold_integer_fold_first) + (ff_p_mce_alternating_integer_fold_first_prefix))) /\ ((((exists ff_h_mce_integer_fold_first_prefix_negative. ff_h_mce_integer_fold_first_prefix_negative + S (ff_n_mce_alternating_integer_fold_first_prefix) = S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * ff_vc_mce_fold_integer_fold_first)) /\ exists ff_q_mce_integer_fold_first_prefix_negative. ff_vb_mce_fold_integer_fold_first = ff_q_mce_integer_fold_first_prefix_negative * S ((S (ff_index_mce_alternating_integer_fold_first_prefix)) * ff_vc_mce_fold_integer_fold_first) + (ff_n_mce_alternating_integer_fold_first_prefix))) /\ (((exists ff_even_mce_term_integer_fold_first_prefix_term. ff_index_mce_alternating_integer_fold_first_prefix = 2 * ff_even_mce_term_integer_fold_first_prefix_term) /\ (ff_p_mce_alternating_integer_fold_first_prefix = (ff_ap_mce_alternating_integer_fold_first_prefix) * (ff_bp_mce_alternating_integer_fold_first_prefix) + (ff_an_mce_alternating_integer_fold_first_prefix) * (ff_bn_mce_alternating_integer_fold_first_prefix) /\ ff_n_mce_alternating_integer_fold_first_prefix = (ff_ap_mce_alternating_integer_fold_first_prefix) * (ff_bn_mce_alternating_integer_fold_first_prefix) + (ff_an_mce_alternating_integer_fold_first_prefix) * (ff_bp_mce_alternating_integer_fold_first_prefix))) \/ ((exists ff_odd_mce_term_integer_fold_first_prefix_term. ff_index_mce_alternating_integer_fold_first_prefix = 2 * ff_odd_mce_term_integer_fold_first_prefix_term + 1) /\ (ff_p_mce_alternating_integer_fold_first_prefix = (ff_ap_mce_alternating_integer_fold_first_prefix) * (ff_bn_mce_alternating_integer_fold_first_prefix) + (ff_an_mce_alternating_integer_fold_first_prefix) * (ff_bp_mce_alternating_integer_fold_first_prefix) /\ ff_n_mce_alternating_integer_fold_first_prefix = (ff_ap_mce_alternating_integer_fold_first_prefix) * (ff_bp_mce_alternating_integer_fold_first_prefix) + (ff_an_mce_alternating_integer_fold_first_prefix) * (ff_bn_mce_alternating_integer_fold_first_prefix))))))))))) /\ ((exists ff_u_mce_integer_fold_first_positive ff_v_mce_integer_fold_first_positive. ((((exists ff_h_mce_integer_fold_first_positive_start. ff_h_mce_integer_fold_first_positive_start + S (0) = S ((S (0)) * ff_v_mce_integer_fold_first_positive)) /\ exists ff_q_mce_integer_fold_first_positive_start. ff_u_mce_integer_fold_first_positive = ff_q_mce_integer_fold_first_positive_start * S ((S (0)) * ff_v_mce_integer_fold_first_positive) + (0))) /\ ((((exists ff_h_mce_integer_fold_first_positive_terminal. ff_h_mce_integer_fold_first_positive_terminal + S (p) = S ((S (l)) * ff_v_mce_integer_fold_first_positive)) /\ exists ff_q_mce_integer_fold_first_positive_terminal. ff_u_mce_integer_fold_first_positive = ff_q_mce_integer_fold_first_positive_terminal * S ((S (l)) * ff_v_mce_integer_fold_first_positive) + (p))) /\ forall ff_i_mce_integer_fold_first_positive. (exists ff_lt_mce_integer_fold_first_positive_bound. ff_lt_mce_integer_fold_first_positive_bound + S ff_i_mce_integer_fold_first_positive = l) -> exists ff_a_mce_integer_fold_first_positive ff_r_mce_integer_fold_first_positive ff_s_mce_integer_fold_first_positive. ((((exists ff_h_mce_integer_fold_first_positive_summand. ff_h_mce_integer_fold_first_positive_summand + S (ff_a_mce_integer_fold_first_positive) = S ((S (ff_i_mce_integer_fold_first_positive)) * ff_uc_mce_fold_integer_fold_first)) /\ exists ff_q_mce_integer_fold_first_positive_summand. ff_ub_mce_fold_integer_fold_first = ff_q_mce_integer_fold_first_positive_summand * S ((S (ff_i_mce_integer_fold_first_positive)) * ff_uc_mce_fold_integer_fold_first) + (ff_a_mce_integer_fold_first_positive))) /\ ((((exists ff_h_mce_integer_fold_first_positive_partial. ff_h_mce_integer_fold_first_positive_partial + S (ff_r_mce_integer_fold_first_positive) = S ((S (ff_i_mce_integer_fold_first_positive)) * ff_v_mce_integer_fold_first_positive)) /\ exists ff_q_mce_integer_fold_first_positive_partial. ff_u_mce_integer_fold_first_positive = ff_q_mce_integer_fold_first_positive_partial * S ((S (ff_i_mce_integer_fold_first_positive)) * ff_v_mce_integer_fold_first_positive) + (ff_r_mce_integer_fold_first_positive))) /\ ((((exists ff_h_mce_integer_fold_first_positive_successor. ff_h_mce_integer_fold_first_positive_successor + S (ff_s_mce_integer_fold_first_positive) = S ((S (S ff_i_mce_integer_fold_first_positive)) * ff_v_mce_integer_fold_first_positive)) /\ exists ff_q_mce_integer_fold_first_positive_successor. ff_u_mce_integer_fold_first_positive = ff_q_mce_integer_fold_first_positive_successor * S ((S (S ff_i_mce_integer_fold_first_positive)) * ff_v_mce_integer_fold_first_positive) + (ff_s_mce_integer_fold_first_positive))) /\ ff_s_mce_integer_fold_first_positive = ff_r_mce_integer_fold_first_positive + ff_a_mce_integer_fold_first_positive)))))) /\ (exists ff_u_mce_integer_fold_first_negative ff_v_mce_integer_fold_first_negative. ((((exists ff_h_mce_integer_fold_first_negative_start. ff_h_mce_integer_fold_first_negative_start + S (0) = S ((S (0)) * ff_v_mce_integer_fold_first_negative)) /\ exists ff_q_mce_integer_fold_first_negative_start. ff_u_mce_integer_fold_first_negative = ff_q_mce_integer_fold_first_negative_start * S ((S (0)) * ff_v_mce_integer_fold_first_negative) + (0))) /\ ((((exists ff_h_mce_integer_fold_first_negative_terminal. ff_h_mce_integer_fold_first_negative_terminal + S (n) = S ((S (l)) * ff_v_mce_integer_fold_first_negative)) /\ exists ff_q_mce_integer_fold_first_negative_terminal. ff_u_mce_integer_fold_first_negative = ff_q_mce_integer_fold_first_negative_terminal * S ((S (l)) * ff_v_mce_integer_fold_first_negative) + (n))) /\ forall ff_i_mce_integer_fold_first_negative. (exists ff_lt_mce_integer_fold_first_negative_bound. ff_lt_mce_integer_fold_first_negative_bound + S ff_i_mce_integer_fold_first_negative = l) -> exists ff_a_mce_integer_fold_first_negative ff_r_mce_integer_fold_first_negative ff_s_mce_integer_fold_first_negative. ((((exists ff_h_mce_integer_fold_first_negative_summand. ff_h_mce_integer_fold_first_negative_summand + S (ff_a_mce_integer_fold_first_negative) = S ((S (ff_i_mce_integer_fold_first_negative)) * ff_vc_mce_fold_integer_fold_first)) /\ exists ff_q_mce_integer_fold_first_negative_summand. ff_vb_mce_fold_integer_fold_first = ff_q_mce_integer_fold_first_negative_summand * S ((S (ff_i_mce_integer_fold_first_negative)) * ff_vc_mce_fold_integer_fold_first) + (ff_a_mce_integer_fold_first_negative))) /\ ((((exists ff_h_mce_integer_fold_first_negative_partial. ff_h_mce_integer_fold_first_negative_partial + S (ff_r_mce_integer_fold_first_negative) = S ((S (ff_i_mce_integer_fold_first_negative)) * ff_v_mce_integer_fold_first_negative)) /\ exists ff_q_mce_integer_fold_first_negative_partial. ff_u_mce_integer_fold_first_negative = ff_q_mce_integer_fold_first_negative_partial * S ((S (ff_i_mce_integer_fold_first_negative)) * ff_v_mce_integer_fold_first_negative) + (ff_r_mce_integer_fold_first_negative))) /\ ((((exists ff_h_mce_integer_fold_first_negative_successor. ff_h_mce_integer_fold_first_negative_successor + S (ff_s_mce_integer_fold_first_negative) = S ((S (S ff_i_mce_integer_fold_first_negative)) * ff_v_mce_integer_fold_first_negative)) /\ exists ff_q_mce_integer_fold_first_negative_successor. ff_u_mce_integer_fold_first_negative = ff_q_mce_integer_fold_first_negative_successor * S ((S (S ff_i_mce_integer_fold_first_negative)) * ff_v_mce_integer_fold_first_negative) + (ff_s_mce_integer_fold_first_negative))) /\ ff_s_mce_integer_fold_first_negative = ff_r_mce_integer_fold_first_negative + ff_a_mce_integer_fold_first_negative))))))))) -> (exists ff_ub_mce_fold_integer_fold_second ff_uc_mce_fold_integer_fold_second ff_vb_mce_fold_integer_fold_second ff_vc_mce_fold_integer_fold_second. ((forall ff_index_mce_alternating_integer_fold_second_prefix. (exists ff_gap_mce_integer_fold_second_prefix_index. ff_gap_mce_integer_fold_second_prefix_index + S (ff_index_mce_alternating_integer_fold_second_prefix) = (l)) -> exists ff_ap_mce_alternating_integer_fold_second_prefix ff_an_mce_alternating_integer_fold_second_prefix ff_bp_mce_alternating_integer_fold_second_prefix ff_bn_mce_alternating_integer_fold_second_prefix ff_p_mce_alternating_integer_fold_second_prefix ff_n_mce_alternating_integer_fold_second_prefix. ((((exists ff_h_mce_integer_fold_second_prefix_ap. ff_h_mce_integer_fold_second_prefix_ap + S (ff_ap_mce_alternating_integer_fold_second_prefix) = S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * ec)) /\ exists ff_q_mce_integer_fold_second_prefix_ap. eb = ff_q_mce_integer_fold_second_prefix_ap * S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * ec) + (ff_ap_mce_alternating_integer_fold_second_prefix))) /\ ((((exists ff_h_mce_integer_fold_second_prefix_an. ff_h_mce_integer_fold_second_prefix_an + S (ff_an_mce_alternating_integer_fold_second_prefix) = S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * fc)) /\ exists ff_q_mce_integer_fold_second_prefix_an. fb = ff_q_mce_integer_fold_second_prefix_an * S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * fc) + (ff_an_mce_alternating_integer_fold_second_prefix))) /\ ((((exists ff_h_mce_integer_fold_second_prefix_bp. ff_h_mce_integer_fold_second_prefix_bp + S (ff_bp_mce_alternating_integer_fold_second_prefix) = S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * gc)) /\ exists ff_q_mce_integer_fold_second_prefix_bp. gb = ff_q_mce_integer_fold_second_prefix_bp * S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * gc) + (ff_bp_mce_alternating_integer_fold_second_prefix))) /\ ((((exists ff_h_mce_integer_fold_second_prefix_bn. ff_h_mce_integer_fold_second_prefix_bn + S (ff_bn_mce_alternating_integer_fold_second_prefix) = S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * hc)) /\ exists ff_q_mce_integer_fold_second_prefix_bn. hb = ff_q_mce_integer_fold_second_prefix_bn * S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * hc) + (ff_bn_mce_alternating_integer_fold_second_prefix))) /\ ((((exists ff_h_mce_integer_fold_second_prefix_positive. ff_h_mce_integer_fold_second_prefix_positive + S (ff_p_mce_alternating_integer_fold_second_prefix) = S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * ff_uc_mce_fold_integer_fold_second)) /\ exists ff_q_mce_integer_fold_second_prefix_positive. ff_ub_mce_fold_integer_fold_second = ff_q_mce_integer_fold_second_prefix_positive * S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * ff_uc_mce_fold_integer_fold_second) + (ff_p_mce_alternating_integer_fold_second_prefix))) /\ ((((exists ff_h_mce_integer_fold_second_prefix_negative. ff_h_mce_integer_fold_second_prefix_negative + S (ff_n_mce_alternating_integer_fold_second_prefix) = S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * ff_vc_mce_fold_integer_fold_second)) /\ exists ff_q_mce_integer_fold_second_prefix_negative. ff_vb_mce_fold_integer_fold_second = ff_q_mce_integer_fold_second_prefix_negative * S ((S (ff_index_mce_alternating_integer_fold_second_prefix)) * ff_vc_mce_fold_integer_fold_second) + (ff_n_mce_alternating_integer_fold_second_prefix))) /\ (((exists ff_even_mce_term_integer_fold_second_prefix_term. ff_index_mce_alternating_integer_fold_second_prefix = 2 * ff_even_mce_term_integer_fold_second_prefix_term) /\ (ff_p_mce_alternating_integer_fold_second_prefix = (ff_ap_mce_alternating_integer_fold_second_prefix) * (ff_bp_mce_alternating_integer_fold_second_prefix) + (ff_an_mce_alternating_integer_fold_second_prefix) * (ff_bn_mce_alternating_integer_fold_second_prefix) /\ ff_n_mce_alternating_integer_fold_second_prefix = (ff_ap_mce_alternating_integer_fold_second_prefix) * (ff_bn_mce_alternating_integer_fold_second_prefix) + (ff_an_mce_alternating_integer_fold_second_prefix) * (ff_bp_mce_alternating_integer_fold_second_prefix))) \/ ((exists ff_odd_mce_term_integer_fold_second_prefix_term. ff_index_mce_alternating_integer_fold_second_prefix = 2 * ff_odd_mce_term_integer_fold_second_prefix_term + 1) /\ (ff_p_mce_alternating_integer_fold_second_prefix = (ff_ap_mce_alternating_integer_fold_second_prefix) * (ff_bn_mce_alternating_integer_fold_second_prefix) + (ff_an_mce_alternating_integer_fold_second_prefix) * (ff_bp_mce_alternating_integer_fold_second_prefix) /\ ff_n_mce_alternating_integer_fold_second_prefix = (ff_ap_mce_alternating_integer_fold_second_prefix) * (ff_bp_mce_alternating_integer_fold_second_prefix) + (ff_an_mce_alternating_integer_fold_second_prefix) * (ff_bn_mce_alternating_integer_fold_second_prefix))))))))))) /\ ((exists ff_u_mce_integer_fold_second_positive ff_v_mce_integer_fold_second_positive. ((((exists ff_h_mce_integer_fold_second_positive_start. ff_h_mce_integer_fold_second_positive_start + S (0) = S ((S (0)) * ff_v_mce_integer_fold_second_positive)) /\ exists ff_q_mce_integer_fold_second_positive_start. ff_u_mce_integer_fold_second_positive = ff_q_mce_integer_fold_second_positive_start * S ((S (0)) * ff_v_mce_integer_fold_second_positive) + (0))) /\ ((((exists ff_h_mce_integer_fold_second_positive_terminal. ff_h_mce_integer_fold_second_positive_terminal + S (P) = S ((S (l)) * ff_v_mce_integer_fold_second_positive)) /\ exists ff_q_mce_integer_fold_second_positive_terminal. ff_u_mce_integer_fold_second_positive = ff_q_mce_integer_fold_second_positive_terminal * S ((S (l)) * ff_v_mce_integer_fold_second_positive) + (P))) /\ forall ff_i_mce_integer_fold_second_positive. (exists ff_lt_mce_integer_fold_second_positive_bound. ff_lt_mce_integer_fold_second_positive_bound + S ff_i_mce_integer_fold_second_positive = l) -> exists ff_a_mce_integer_fold_second_positive ff_r_mce_integer_fold_second_positive ff_s_mce_integer_fold_second_positive. ((((exists ff_h_mce_integer_fold_second_positive_summand. ff_h_mce_integer_fold_second_positive_summand + S (ff_a_mce_integer_fold_second_positive) = S ((S (ff_i_mce_integer_fold_second_positive)) * ff_uc_mce_fold_integer_fold_second)) /\ exists ff_q_mce_integer_fold_second_positive_summand. ff_ub_mce_fold_integer_fold_second = ff_q_mce_integer_fold_second_positive_summand * S ((S (ff_i_mce_integer_fold_second_positive)) * ff_uc_mce_fold_integer_fold_second) + (ff_a_mce_integer_fold_second_positive))) /\ ((((exists ff_h_mce_integer_fold_second_positive_partial. ff_h_mce_integer_fold_second_positive_partial + S (ff_r_mce_integer_fold_second_positive) = S ((S (ff_i_mce_integer_fold_second_positive)) * ff_v_mce_integer_fold_second_positive)) /\ exists ff_q_mce_integer_fold_second_positive_partial. ff_u_mce_integer_fold_second_positive = ff_q_mce_integer_fold_second_positive_partial * S ((S (ff_i_mce_integer_fold_second_positive)) * ff_v_mce_integer_fold_second_positive) + (ff_r_mce_integer_fold_second_positive))) /\ ((((exists ff_h_mce_integer_fold_second_positive_successor. ff_h_mce_integer_fold_second_positive_successor + S (ff_s_mce_integer_fold_second_positive) = S ((S (S ff_i_mce_integer_fold_second_positive)) * ff_v_mce_integer_fold_second_positive)) /\ exists ff_q_mce_integer_fold_second_positive_successor. ff_u_mce_integer_fold_second_positive = ff_q_mce_integer_fold_second_positive_successor * S ((S (S ff_i_mce_integer_fold_second_positive)) * ff_v_mce_integer_fold_second_positive) + (ff_s_mce_integer_fold_second_positive))) /\ ff_s_mce_integer_fold_second_positive = ff_r_mce_integer_fold_second_positive + ff_a_mce_integer_fold_second_positive)))))) /\ (exists ff_u_mce_integer_fold_second_negative ff_v_mce_integer_fold_second_negative. ((((exists ff_h_mce_integer_fold_second_negative_start. ff_h_mce_integer_fold_second_negative_start + S (0) = S ((S (0)) * ff_v_mce_integer_fold_second_negative)) /\ exists ff_q_mce_integer_fold_second_negative_start. ff_u_mce_integer_fold_second_negative = ff_q_mce_integer_fold_second_negative_start * S ((S (0)) * ff_v_mce_integer_fold_second_negative) + (0))) /\ ((((exists ff_h_mce_integer_fold_second_negative_terminal. ff_h_mce_integer_fold_second_negative_terminal + S (N) = S ((S (l)) * ff_v_mce_integer_fold_second_negative)) /\ exists ff_q_mce_integer_fold_second_negative_terminal. ff_u_mce_integer_fold_second_negative = ff_q_mce_integer_fold_second_negative_terminal * S ((S (l)) * ff_v_mce_integer_fold_second_negative) + (N))) /\ forall ff_i_mce_integer_fold_second_negative. (exists ff_lt_mce_integer_fold_second_negative_bound. ff_lt_mce_integer_fold_second_negative_bound + S ff_i_mce_integer_fold_second_negative = l) -> exists ff_a_mce_integer_fold_second_negative ff_r_mce_integer_fold_second_negative ff_s_mce_integer_fold_second_negative. ((((exists ff_h_mce_integer_fold_second_negative_summand. ff_h_mce_integer_fold_second_negative_summand + S (ff_a_mce_integer_fold_second_negative) = S ((S (ff_i_mce_integer_fold_second_negative)) * ff_vc_mce_fold_integer_fold_second)) /\ exists ff_q_mce_integer_fold_second_negative_summand. ff_vb_mce_fold_integer_fold_second = ff_q_mce_integer_fold_second_negative_summand * S ((S (ff_i_mce_integer_fold_second_negative)) * ff_vc_mce_fold_integer_fold_second) + (ff_a_mce_integer_fold_second_negative))) /\ ((((exists ff_h_mce_integer_fold_second_negative_partial. ff_h_mce_integer_fold_second_negative_partial + S (ff_r_mce_integer_fold_second_negative) = S ((S (ff_i_mce_integer_fold_second_negative)) * ff_v_mce_integer_fold_second_negative)) /\ exists ff_q_mce_integer_fold_second_negative_partial. ff_u_mce_integer_fold_second_negative = ff_q_mce_integer_fold_second_negative_partial * S ((S (ff_i_mce_integer_fold_second_negative)) * ff_v_mce_integer_fold_second_negative) + (ff_r_mce_integer_fold_second_negative))) /\ ((((exists ff_h_mce_integer_fold_second_negative_successor. ff_h_mce_integer_fold_second_negative_successor + S (ff_s_mce_integer_fold_second_negative) = S ((S (S ff_i_mce_integer_fold_second_negative)) * ff_v_mce_integer_fold_second_negative)) /\ exists ff_q_mce_integer_fold_second_negative_successor. ff_u_mce_integer_fold_second_negative = ff_q_mce_integer_fold_second_negative_successor * S ((S (S ff_i_mce_integer_fold_second_negative)) * ff_v_mce_integer_fold_second_negative) + (ff_s_mce_integer_fold_second_negative))) /\ ff_s_mce_integer_fold_second_negative = ff_r_mce_integer_fold_second_negative + ff_a_mce_integer_fold_second_negative))))))))) -> p + N = P + n