matrix_recursive_alternating_fold_transport

Exact expanded first-order arithmetic statement

forall pb pc nb nc eb ec fb fc qb qc rb rc ub uc vb vc l p n. (forall mdr_i_fold_input_0 mdr_a_fold_input_0. (exists mdr_gap_fold_input_0b. mdr_gap_fold_input_0b + S (mdr_i_fold_input_0) = (l)) -> (((exists ff_h_mdr_fold_input_0o. ff_h_mdr_fold_input_0o + S (mdr_a_fold_input_0) = S ((S (mdr_i_fold_input_0)) * pc)) /\ exists ff_q_mdr_fold_input_0o. pb = ff_q_mdr_fold_input_0o * S ((S (mdr_i_fold_input_0)) * pc) + (mdr_a_fold_input_0))) -> (((exists ff_h_mdr_fold_input_0n. ff_h_mdr_fold_input_0n + S (mdr_a_fold_input_0) = S ((S (mdr_i_fold_input_0)) * qc)) /\ exists ff_q_mdr_fold_input_0n. qb = ff_q_mdr_fold_input_0n * S ((S (mdr_i_fold_input_0)) * qc) + (mdr_a_fold_input_0)))) -> (forall mdr_i_fold_input_1 mdr_a_fold_input_1. (exists mdr_gap_fold_input_1b. mdr_gap_fold_input_1b + S (mdr_i_fold_input_1) = (l)) -> (((exists ff_h_mdr_fold_input_1o. ff_h_mdr_fold_input_1o + S (mdr_a_fold_input_1) = S ((S (mdr_i_fold_input_1)) * nc)) /\ exists ff_q_mdr_fold_input_1o. nb = ff_q_mdr_fold_input_1o * S ((S (mdr_i_fold_input_1)) * nc) + (mdr_a_fold_input_1))) -> (((exists ff_h_mdr_fold_input_1n. ff_h_mdr_fold_input_1n + S (mdr_a_fold_input_1) = S ((S (mdr_i_fold_input_1)) * rc)) /\ exists ff_q_mdr_fold_input_1n. rb = ff_q_mdr_fold_input_1n * S ((S (mdr_i_fold_input_1)) * rc) + (mdr_a_fold_input_1)))) -> (forall mdr_i_fold_input_2 mdr_a_fold_input_2. (exists mdr_gap_fold_input_2b. mdr_gap_fold_input_2b + S (mdr_i_fold_input_2) = (l)) -> (((exists ff_h_mdr_fold_input_2o. ff_h_mdr_fold_input_2o + S (mdr_a_fold_input_2) = S ((S (mdr_i_fold_input_2)) * ec)) /\ exists ff_q_mdr_fold_input_2o. eb = ff_q_mdr_fold_input_2o * S ((S (mdr_i_fold_input_2)) * ec) + (mdr_a_fold_input_2))) -> (((exists ff_h_mdr_fold_input_2n. ff_h_mdr_fold_input_2n + S (mdr_a_fold_input_2) = S ((S (mdr_i_fold_input_2)) * uc)) /\ exists ff_q_mdr_fold_input_2n. ub = ff_q_mdr_fold_input_2n * S ((S (mdr_i_fold_input_2)) * uc) + (mdr_a_fold_input_2)))) -> (forall mdr_i_fold_input_3 mdr_a_fold_input_3. (exists mdr_gap_fold_input_3b. mdr_gap_fold_input_3b + S (mdr_i_fold_input_3) = (l)) -> (((exists ff_h_mdr_fold_input_3o. ff_h_mdr_fold_input_3o + S (mdr_a_fold_input_3) = S ((S (mdr_i_fold_input_3)) * fc)) /\ exists ff_q_mdr_fold_input_3o. fb = ff_q_mdr_fold_input_3o * S ((S (mdr_i_fold_input_3)) * fc) + (mdr_a_fold_input_3))) -> (((exists ff_h_mdr_fold_input_3n. ff_h_mdr_fold_input_3n + S (mdr_a_fold_input_3) = S ((S (mdr_i_fold_input_3)) * vc)) /\ exists ff_q_mdr_fold_input_3n. vb = ff_q_mdr_fold_input_3n * S ((S (mdr_i_fold_input_3)) * vc) + (mdr_a_fold_input_3)))) -> (exists ff_ub_mce_fold_mdre_fold_source ff_uc_mce_fold_mdre_fold_source ff_vb_mce_fold_mdre_fold_source ff_vc_mce_fold_mdre_fold_source. ((forall ff_index_mce_alternating_mdre_fold_source_prefix. (exists ff_gap_mce_mdre_fold_source_prefix_index. ff_gap_mce_mdre_fold_source_prefix_index + S (ff_index_mce_alternating_mdre_fold_source_prefix) = (l)) -> exists ff_ap_mce_alternating_mdre_fold_source_prefix ff_an_mce_alternating_mdre_fold_source_prefix ff_bp_mce_alternating_mdre_fold_source_prefix ff_bn_mce_alternating_mdre_fold_source_prefix ff_p_mce_alternating_mdre_fold_source_prefix ff_n_mce_alternating_mdre_fold_source_prefix. ((((exists ff_h_mce_mdre_fold_source_prefix_ap. ff_h_mce_mdre_fold_source_prefix_ap + S (ff_ap_mce_alternating_mdre_fold_source_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * pc)) /\ exists ff_q_mce_mdre_fold_source_prefix_ap. pb = ff_q_mce_mdre_fold_source_prefix_ap * S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * pc) + (ff_ap_mce_alternating_mdre_fold_source_prefix))) /\ ((((exists ff_h_mce_mdre_fold_source_prefix_an. ff_h_mce_mdre_fold_source_prefix_an + S (ff_an_mce_alternating_mdre_fold_source_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * nc)) /\ exists ff_q_mce_mdre_fold_source_prefix_an. nb = ff_q_mce_mdre_fold_source_prefix_an * S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * nc) + (ff_an_mce_alternating_mdre_fold_source_prefix))) /\ ((((exists ff_h_mce_mdre_fold_source_prefix_bp. ff_h_mce_mdre_fold_source_prefix_bp + S (ff_bp_mce_alternating_mdre_fold_source_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * ec)) /\ exists ff_q_mce_mdre_fold_source_prefix_bp. eb = ff_q_mce_mdre_fold_source_prefix_bp * S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * ec) + (ff_bp_mce_alternating_mdre_fold_source_prefix))) /\ ((((exists ff_h_mce_mdre_fold_source_prefix_bn. ff_h_mce_mdre_fold_source_prefix_bn + S (ff_bn_mce_alternating_mdre_fold_source_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * fc)) /\ exists ff_q_mce_mdre_fold_source_prefix_bn. fb = ff_q_mce_mdre_fold_source_prefix_bn * S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * fc) + (ff_bn_mce_alternating_mdre_fold_source_prefix))) /\ ((((exists ff_h_mce_mdre_fold_source_prefix_positive. ff_h_mce_mdre_fold_source_prefix_positive + S (ff_p_mce_alternating_mdre_fold_source_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * ff_uc_mce_fold_mdre_fold_source)) /\ exists ff_q_mce_mdre_fold_source_prefix_positive. ff_ub_mce_fold_mdre_fold_source = ff_q_mce_mdre_fold_source_prefix_positive * S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * ff_uc_mce_fold_mdre_fold_source) + (ff_p_mce_alternating_mdre_fold_source_prefix))) /\ ((((exists ff_h_mce_mdre_fold_source_prefix_negative. ff_h_mce_mdre_fold_source_prefix_negative + S (ff_n_mce_alternating_mdre_fold_source_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * ff_vc_mce_fold_mdre_fold_source)) /\ exists ff_q_mce_mdre_fold_source_prefix_negative. ff_vb_mce_fold_mdre_fold_source = ff_q_mce_mdre_fold_source_prefix_negative * S ((S (ff_index_mce_alternating_mdre_fold_source_prefix)) * ff_vc_mce_fold_mdre_fold_source) + (ff_n_mce_alternating_mdre_fold_source_prefix))) /\ (((exists ff_even_mce_term_mdre_fold_source_prefix_term. ff_index_mce_alternating_mdre_fold_source_prefix = 2 * ff_even_mce_term_mdre_fold_source_prefix_term) /\ (ff_p_mce_alternating_mdre_fold_source_prefix = (ff_ap_mce_alternating_mdre_fold_source_prefix) * (ff_bp_mce_alternating_mdre_fold_source_prefix) + (ff_an_mce_alternating_mdre_fold_source_prefix) * (ff_bn_mce_alternating_mdre_fold_source_prefix) /\ ff_n_mce_alternating_mdre_fold_source_prefix = (ff_ap_mce_alternating_mdre_fold_source_prefix) * (ff_bn_mce_alternating_mdre_fold_source_prefix) + (ff_an_mce_alternating_mdre_fold_source_prefix) * (ff_bp_mce_alternating_mdre_fold_source_prefix))) \/ ((exists ff_odd_mce_term_mdre_fold_source_prefix_term. ff_index_mce_alternating_mdre_fold_source_prefix = 2 * ff_odd_mce_term_mdre_fold_source_prefix_term + 1) /\ (ff_p_mce_alternating_mdre_fold_source_prefix = (ff_ap_mce_alternating_mdre_fold_source_prefix) * (ff_bn_mce_alternating_mdre_fold_source_prefix) + (ff_an_mce_alternating_mdre_fold_source_prefix) * (ff_bp_mce_alternating_mdre_fold_source_prefix) /\ ff_n_mce_alternating_mdre_fold_source_prefix = (ff_ap_mce_alternating_mdre_fold_source_prefix) * (ff_bp_mce_alternating_mdre_fold_source_prefix) + (ff_an_mce_alternating_mdre_fold_source_prefix) * (ff_bn_mce_alternating_mdre_fold_source_prefix))))))))))) /\ ((exists ff_u_mce_mdre_fold_source_positive ff_v_mce_mdre_fold_source_positive. ((((exists ff_h_mce_mdre_fold_source_positive_start. ff_h_mce_mdre_fold_source_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdre_fold_source_positive)) /\ exists ff_q_mce_mdre_fold_source_positive_start. ff_u_mce_mdre_fold_source_positive = ff_q_mce_mdre_fold_source_positive_start * S ((S (0)) * ff_v_mce_mdre_fold_source_positive) + (0))) /\ ((((exists ff_h_mce_mdre_fold_source_positive_terminal. ff_h_mce_mdre_fold_source_positive_terminal + S (p) = S ((S (l)) * ff_v_mce_mdre_fold_source_positive)) /\ exists ff_q_mce_mdre_fold_source_positive_terminal. ff_u_mce_mdre_fold_source_positive = ff_q_mce_mdre_fold_source_positive_terminal * S ((S (l)) * ff_v_mce_mdre_fold_source_positive) + (p))) /\ forall ff_i_mce_mdre_fold_source_positive. (exists ff_lt_mce_mdre_fold_source_positive_bound. ff_lt_mce_mdre_fold_source_positive_bound + S ff_i_mce_mdre_fold_source_positive = l) -> exists ff_a_mce_mdre_fold_source_positive ff_r_mce_mdre_fold_source_positive ff_s_mce_mdre_fold_source_positive. ((((exists ff_h_mce_mdre_fold_source_positive_summand. ff_h_mce_mdre_fold_source_positive_summand + S (ff_a_mce_mdre_fold_source_positive) = S ((S (ff_i_mce_mdre_fold_source_positive)) * ff_uc_mce_fold_mdre_fold_source)) /\ exists ff_q_mce_mdre_fold_source_positive_summand. ff_ub_mce_fold_mdre_fold_source = ff_q_mce_mdre_fold_source_positive_summand * S ((S (ff_i_mce_mdre_fold_source_positive)) * ff_uc_mce_fold_mdre_fold_source) + (ff_a_mce_mdre_fold_source_positive))) /\ ((((exists ff_h_mce_mdre_fold_source_positive_partial. ff_h_mce_mdre_fold_source_positive_partial + S (ff_r_mce_mdre_fold_source_positive) = S ((S (ff_i_mce_mdre_fold_source_positive)) * ff_v_mce_mdre_fold_source_positive)) /\ exists ff_q_mce_mdre_fold_source_positive_partial. ff_u_mce_mdre_fold_source_positive = ff_q_mce_mdre_fold_source_positive_partial * S ((S (ff_i_mce_mdre_fold_source_positive)) * ff_v_mce_mdre_fold_source_positive) + (ff_r_mce_mdre_fold_source_positive))) /\ ((((exists ff_h_mce_mdre_fold_source_positive_successor. ff_h_mce_mdre_fold_source_positive_successor + S (ff_s_mce_mdre_fold_source_positive) = S ((S (S ff_i_mce_mdre_fold_source_positive)) * ff_v_mce_mdre_fold_source_positive)) /\ exists ff_q_mce_mdre_fold_source_positive_successor. ff_u_mce_mdre_fold_source_positive = ff_q_mce_mdre_fold_source_positive_successor * S ((S (S ff_i_mce_mdre_fold_source_positive)) * ff_v_mce_mdre_fold_source_positive) + (ff_s_mce_mdre_fold_source_positive))) /\ ff_s_mce_mdre_fold_source_positive = ff_r_mce_mdre_fold_source_positive + ff_a_mce_mdre_fold_source_positive)))))) /\ (exists ff_u_mce_mdre_fold_source_negative ff_v_mce_mdre_fold_source_negative. ((((exists ff_h_mce_mdre_fold_source_negative_start. ff_h_mce_mdre_fold_source_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdre_fold_source_negative)) /\ exists ff_q_mce_mdre_fold_source_negative_start. ff_u_mce_mdre_fold_source_negative = ff_q_mce_mdre_fold_source_negative_start * S ((S (0)) * ff_v_mce_mdre_fold_source_negative) + (0))) /\ ((((exists ff_h_mce_mdre_fold_source_negative_terminal. ff_h_mce_mdre_fold_source_negative_terminal + S (n) = S ((S (l)) * ff_v_mce_mdre_fold_source_negative)) /\ exists ff_q_mce_mdre_fold_source_negative_terminal. ff_u_mce_mdre_fold_source_negative = ff_q_mce_mdre_fold_source_negative_terminal * S ((S (l)) * ff_v_mce_mdre_fold_source_negative) + (n))) /\ forall ff_i_mce_mdre_fold_source_negative. (exists ff_lt_mce_mdre_fold_source_negative_bound. ff_lt_mce_mdre_fold_source_negative_bound + S ff_i_mce_mdre_fold_source_negative = l) -> exists ff_a_mce_mdre_fold_source_negative ff_r_mce_mdre_fold_source_negative ff_s_mce_mdre_fold_source_negative. ((((exists ff_h_mce_mdre_fold_source_negative_summand. ff_h_mce_mdre_fold_source_negative_summand + S (ff_a_mce_mdre_fold_source_negative) = S ((S (ff_i_mce_mdre_fold_source_negative)) * ff_vc_mce_fold_mdre_fold_source)) /\ exists ff_q_mce_mdre_fold_source_negative_summand. ff_vb_mce_fold_mdre_fold_source = ff_q_mce_mdre_fold_source_negative_summand * S ((S (ff_i_mce_mdre_fold_source_negative)) * ff_vc_mce_fold_mdre_fold_source) + (ff_a_mce_mdre_fold_source_negative))) /\ ((((exists ff_h_mce_mdre_fold_source_negative_partial. ff_h_mce_mdre_fold_source_negative_partial + S (ff_r_mce_mdre_fold_source_negative) = S ((S (ff_i_mce_mdre_fold_source_negative)) * ff_v_mce_mdre_fold_source_negative)) /\ exists ff_q_mce_mdre_fold_source_negative_partial. ff_u_mce_mdre_fold_source_negative = ff_q_mce_mdre_fold_source_negative_partial * S ((S (ff_i_mce_mdre_fold_source_negative)) * ff_v_mce_mdre_fold_source_negative) + (ff_r_mce_mdre_fold_source_negative))) /\ ((((exists ff_h_mce_mdre_fold_source_negative_successor. ff_h_mce_mdre_fold_source_negative_successor + S (ff_s_mce_mdre_fold_source_negative) = S ((S (S ff_i_mce_mdre_fold_source_negative)) * ff_v_mce_mdre_fold_source_negative)) /\ exists ff_q_mce_mdre_fold_source_negative_successor. ff_u_mce_mdre_fold_source_negative = ff_q_mce_mdre_fold_source_negative_successor * S ((S (S ff_i_mce_mdre_fold_source_negative)) * ff_v_mce_mdre_fold_source_negative) + (ff_s_mce_mdre_fold_source_negative))) /\ ff_s_mce_mdre_fold_source_negative = ff_r_mce_mdre_fold_source_negative + ff_a_mce_mdre_fold_source_negative))))))))) -> (exists ff_ub_mce_fold_mdre_fold_target ff_uc_mce_fold_mdre_fold_target ff_vb_mce_fold_mdre_fold_target ff_vc_mce_fold_mdre_fold_target. ((forall ff_index_mce_alternating_mdre_fold_target_prefix. (exists ff_gap_mce_mdre_fold_target_prefix_index. ff_gap_mce_mdre_fold_target_prefix_index + S (ff_index_mce_alternating_mdre_fold_target_prefix) = (l)) -> exists ff_ap_mce_alternating_mdre_fold_target_prefix ff_an_mce_alternating_mdre_fold_target_prefix ff_bp_mce_alternating_mdre_fold_target_prefix ff_bn_mce_alternating_mdre_fold_target_prefix ff_p_mce_alternating_mdre_fold_target_prefix ff_n_mce_alternating_mdre_fold_target_prefix. ((((exists ff_h_mce_mdre_fold_target_prefix_ap. ff_h_mce_mdre_fold_target_prefix_ap + S (ff_ap_mce_alternating_mdre_fold_target_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * qc)) /\ exists ff_q_mce_mdre_fold_target_prefix_ap. qb = ff_q_mce_mdre_fold_target_prefix_ap * S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * qc) + (ff_ap_mce_alternating_mdre_fold_target_prefix))) /\ ((((exists ff_h_mce_mdre_fold_target_prefix_an. ff_h_mce_mdre_fold_target_prefix_an + S (ff_an_mce_alternating_mdre_fold_target_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * rc)) /\ exists ff_q_mce_mdre_fold_target_prefix_an. rb = ff_q_mce_mdre_fold_target_prefix_an * S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * rc) + (ff_an_mce_alternating_mdre_fold_target_prefix))) /\ ((((exists ff_h_mce_mdre_fold_target_prefix_bp. ff_h_mce_mdre_fold_target_prefix_bp + S (ff_bp_mce_alternating_mdre_fold_target_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * uc)) /\ exists ff_q_mce_mdre_fold_target_prefix_bp. ub = ff_q_mce_mdre_fold_target_prefix_bp * S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * uc) + (ff_bp_mce_alternating_mdre_fold_target_prefix))) /\ ((((exists ff_h_mce_mdre_fold_target_prefix_bn. ff_h_mce_mdre_fold_target_prefix_bn + S (ff_bn_mce_alternating_mdre_fold_target_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * vc)) /\ exists ff_q_mce_mdre_fold_target_prefix_bn. vb = ff_q_mce_mdre_fold_target_prefix_bn * S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * vc) + (ff_bn_mce_alternating_mdre_fold_target_prefix))) /\ ((((exists ff_h_mce_mdre_fold_target_prefix_positive. ff_h_mce_mdre_fold_target_prefix_positive + S (ff_p_mce_alternating_mdre_fold_target_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * ff_uc_mce_fold_mdre_fold_target)) /\ exists ff_q_mce_mdre_fold_target_prefix_positive. ff_ub_mce_fold_mdre_fold_target = ff_q_mce_mdre_fold_target_prefix_positive * S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * ff_uc_mce_fold_mdre_fold_target) + (ff_p_mce_alternating_mdre_fold_target_prefix))) /\ ((((exists ff_h_mce_mdre_fold_target_prefix_negative. ff_h_mce_mdre_fold_target_prefix_negative + S (ff_n_mce_alternating_mdre_fold_target_prefix) = S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * ff_vc_mce_fold_mdre_fold_target)) /\ exists ff_q_mce_mdre_fold_target_prefix_negative. ff_vb_mce_fold_mdre_fold_target = ff_q_mce_mdre_fold_target_prefix_negative * S ((S (ff_index_mce_alternating_mdre_fold_target_prefix)) * ff_vc_mce_fold_mdre_fold_target) + (ff_n_mce_alternating_mdre_fold_target_prefix))) /\ (((exists ff_even_mce_term_mdre_fold_target_prefix_term. ff_index_mce_alternating_mdre_fold_target_prefix = 2 * ff_even_mce_term_mdre_fold_target_prefix_term) /\ (ff_p_mce_alternating_mdre_fold_target_prefix = (ff_ap_mce_alternating_mdre_fold_target_prefix) * (ff_bp_mce_alternating_mdre_fold_target_prefix) + (ff_an_mce_alternating_mdre_fold_target_prefix) * (ff_bn_mce_alternating_mdre_fold_target_prefix) /\ ff_n_mce_alternating_mdre_fold_target_prefix = (ff_ap_mce_alternating_mdre_fold_target_prefix) * (ff_bn_mce_alternating_mdre_fold_target_prefix) + (ff_an_mce_alternating_mdre_fold_target_prefix) * (ff_bp_mce_alternating_mdre_fold_target_prefix))) \/ ((exists ff_odd_mce_term_mdre_fold_target_prefix_term. ff_index_mce_alternating_mdre_fold_target_prefix = 2 * ff_odd_mce_term_mdre_fold_target_prefix_term + 1) /\ (ff_p_mce_alternating_mdre_fold_target_prefix = (ff_ap_mce_alternating_mdre_fold_target_prefix) * (ff_bn_mce_alternating_mdre_fold_target_prefix) + (ff_an_mce_alternating_mdre_fold_target_prefix) * (ff_bp_mce_alternating_mdre_fold_target_prefix) /\ ff_n_mce_alternating_mdre_fold_target_prefix = (ff_ap_mce_alternating_mdre_fold_target_prefix) * (ff_bp_mce_alternating_mdre_fold_target_prefix) + (ff_an_mce_alternating_mdre_fold_target_prefix) * (ff_bn_mce_alternating_mdre_fold_target_prefix))))))))))) /\ ((exists ff_u_mce_mdre_fold_target_positive ff_v_mce_mdre_fold_target_positive. ((((exists ff_h_mce_mdre_fold_target_positive_start. ff_h_mce_mdre_fold_target_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdre_fold_target_positive)) /\ exists ff_q_mce_mdre_fold_target_positive_start. ff_u_mce_mdre_fold_target_positive = ff_q_mce_mdre_fold_target_positive_start * S ((S (0)) * ff_v_mce_mdre_fold_target_positive) + (0))) /\ ((((exists ff_h_mce_mdre_fold_target_positive_terminal. ff_h_mce_mdre_fold_target_positive_terminal + S (p) = S ((S (l)) * ff_v_mce_mdre_fold_target_positive)) /\ exists ff_q_mce_mdre_fold_target_positive_terminal. ff_u_mce_mdre_fold_target_positive = ff_q_mce_mdre_fold_target_positive_terminal * S ((S (l)) * ff_v_mce_mdre_fold_target_positive) + (p))) /\ forall ff_i_mce_mdre_fold_target_positive. (exists ff_lt_mce_mdre_fold_target_positive_bound. ff_lt_mce_mdre_fold_target_positive_bound + S ff_i_mce_mdre_fold_target_positive = l) -> exists ff_a_mce_mdre_fold_target_positive ff_r_mce_mdre_fold_target_positive ff_s_mce_mdre_fold_target_positive. ((((exists ff_h_mce_mdre_fold_target_positive_summand. ff_h_mce_mdre_fold_target_positive_summand + S (ff_a_mce_mdre_fold_target_positive) = S ((S (ff_i_mce_mdre_fold_target_positive)) * ff_uc_mce_fold_mdre_fold_target)) /\ exists ff_q_mce_mdre_fold_target_positive_summand. ff_ub_mce_fold_mdre_fold_target = ff_q_mce_mdre_fold_target_positive_summand * S ((S (ff_i_mce_mdre_fold_target_positive)) * ff_uc_mce_fold_mdre_fold_target) + (ff_a_mce_mdre_fold_target_positive))) /\ ((((exists ff_h_mce_mdre_fold_target_positive_partial. ff_h_mce_mdre_fold_target_positive_partial + S (ff_r_mce_mdre_fold_target_positive) = S ((S (ff_i_mce_mdre_fold_target_positive)) * ff_v_mce_mdre_fold_target_positive)) /\ exists ff_q_mce_mdre_fold_target_positive_partial. ff_u_mce_mdre_fold_target_positive = ff_q_mce_mdre_fold_target_positive_partial * S ((S (ff_i_mce_mdre_fold_target_positive)) * ff_v_mce_mdre_fold_target_positive) + (ff_r_mce_mdre_fold_target_positive))) /\ ((((exists ff_h_mce_mdre_fold_target_positive_successor. ff_h_mce_mdre_fold_target_positive_successor + S (ff_s_mce_mdre_fold_target_positive) = S ((S (S ff_i_mce_mdre_fold_target_positive)) * ff_v_mce_mdre_fold_target_positive)) /\ exists ff_q_mce_mdre_fold_target_positive_successor. ff_u_mce_mdre_fold_target_positive = ff_q_mce_mdre_fold_target_positive_successor * S ((S (S ff_i_mce_mdre_fold_target_positive)) * ff_v_mce_mdre_fold_target_positive) + (ff_s_mce_mdre_fold_target_positive))) /\ ff_s_mce_mdre_fold_target_positive = ff_r_mce_mdre_fold_target_positive + ff_a_mce_mdre_fold_target_positive)))))) /\ (exists ff_u_mce_mdre_fold_target_negative ff_v_mce_mdre_fold_target_negative. ((((exists ff_h_mce_mdre_fold_target_negative_start. ff_h_mce_mdre_fold_target_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdre_fold_target_negative)) /\ exists ff_q_mce_mdre_fold_target_negative_start. ff_u_mce_mdre_fold_target_negative = ff_q_mce_mdre_fold_target_negative_start * S ((S (0)) * ff_v_mce_mdre_fold_target_negative) + (0))) /\ ((((exists ff_h_mce_mdre_fold_target_negative_terminal. ff_h_mce_mdre_fold_target_negative_terminal + S (n) = S ((S (l)) * ff_v_mce_mdre_fold_target_negative)) /\ exists ff_q_mce_mdre_fold_target_negative_terminal. ff_u_mce_mdre_fold_target_negative = ff_q_mce_mdre_fold_target_negative_terminal * S ((S (l)) * ff_v_mce_mdre_fold_target_negative) + (n))) /\ forall ff_i_mce_mdre_fold_target_negative. (exists ff_lt_mce_mdre_fold_target_negative_bound. ff_lt_mce_mdre_fold_target_negative_bound + S ff_i_mce_mdre_fold_target_negative = l) -> exists ff_a_mce_mdre_fold_target_negative ff_r_mce_mdre_fold_target_negative ff_s_mce_mdre_fold_target_negative. ((((exists ff_h_mce_mdre_fold_target_negative_summand. ff_h_mce_mdre_fold_target_negative_summand + S (ff_a_mce_mdre_fold_target_negative) = S ((S (ff_i_mce_mdre_fold_target_negative)) * ff_vc_mce_fold_mdre_fold_target)) /\ exists ff_q_mce_mdre_fold_target_negative_summand. ff_vb_mce_fold_mdre_fold_target = ff_q_mce_mdre_fold_target_negative_summand * S ((S (ff_i_mce_mdre_fold_target_negative)) * ff_vc_mce_fold_mdre_fold_target) + (ff_a_mce_mdre_fold_target_negative))) /\ ((((exists ff_h_mce_mdre_fold_target_negative_partial. ff_h_mce_mdre_fold_target_negative_partial + S (ff_r_mce_mdre_fold_target_negative) = S ((S (ff_i_mce_mdre_fold_target_negative)) * ff_v_mce_mdre_fold_target_negative)) /\ exists ff_q_mce_mdre_fold_target_negative_partial. ff_u_mce_mdre_fold_target_negative = ff_q_mce_mdre_fold_target_negative_partial * S ((S (ff_i_mce_mdre_fold_target_negative)) * ff_v_mce_mdre_fold_target_negative) + (ff_r_mce_mdre_fold_target_negative))) /\ ((((exists ff_h_mce_mdre_fold_target_negative_successor. ff_h_mce_mdre_fold_target_negative_successor + S (ff_s_mce_mdre_fold_target_negative) = S ((S (S ff_i_mce_mdre_fold_target_negative)) * ff_v_mce_mdre_fold_target_negative)) /\ exists ff_q_mce_mdre_fold_target_negative_successor. ff_u_mce_mdre_fold_target_negative = ff_q_mce_mdre_fold_target_negative_successor * S ((S (S ff_i_mce_mdre_fold_target_negative)) * ff_v_mce_mdre_fold_target_negative) + (ff_s_mce_mdre_fold_target_negative))) /\ ff_s_mce_mdre_fold_target_negative = ff_r_mce_mdre_fold_target_negative + ff_a_mce_mdre_fold_target_negative)))))))))