signed_alternating_cofactor_fold_exists_unique

Exact expanded first-order arithmetic statement

forall ab ac db dc eb ec fb fc l. exists p n. ((exists ff_ub_mce_fold_result ff_uc_mce_fold_result ff_vb_mce_fold_result ff_vc_mce_fold_result. ((forall ff_index_mce_alternating_result_prefix. (exists ff_gap_mce_result_prefix_index. ff_gap_mce_result_prefix_index + S (ff_index_mce_alternating_result_prefix) = (l)) -> exists ff_ap_mce_alternating_result_prefix ff_an_mce_alternating_result_prefix ff_bp_mce_alternating_result_prefix ff_bn_mce_alternating_result_prefix ff_p_mce_alternating_result_prefix ff_n_mce_alternating_result_prefix. ((((exists ff_h_mce_result_prefix_ap. ff_h_mce_result_prefix_ap + S (ff_ap_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * ac)) /\ exists ff_q_mce_result_prefix_ap. ab = ff_q_mce_result_prefix_ap * S ((S (ff_index_mce_alternating_result_prefix)) * ac) + (ff_ap_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_an. ff_h_mce_result_prefix_an + S (ff_an_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * dc)) /\ exists ff_q_mce_result_prefix_an. db = ff_q_mce_result_prefix_an * S ((S (ff_index_mce_alternating_result_prefix)) * dc) + (ff_an_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_bp. ff_h_mce_result_prefix_bp + S (ff_bp_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * ec)) /\ exists ff_q_mce_result_prefix_bp. eb = ff_q_mce_result_prefix_bp * S ((S (ff_index_mce_alternating_result_prefix)) * ec) + (ff_bp_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_bn. ff_h_mce_result_prefix_bn + S (ff_bn_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * fc)) /\ exists ff_q_mce_result_prefix_bn. fb = ff_q_mce_result_prefix_bn * S ((S (ff_index_mce_alternating_result_prefix)) * fc) + (ff_bn_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_positive. ff_h_mce_result_prefix_positive + S (ff_p_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * ff_uc_mce_fold_result)) /\ exists ff_q_mce_result_prefix_positive. ff_ub_mce_fold_result = ff_q_mce_result_prefix_positive * S ((S (ff_index_mce_alternating_result_prefix)) * ff_uc_mce_fold_result) + (ff_p_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_negative. ff_h_mce_result_prefix_negative + S (ff_n_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * ff_vc_mce_fold_result)) /\ exists ff_q_mce_result_prefix_negative. ff_vb_mce_fold_result = ff_q_mce_result_prefix_negative * S ((S (ff_index_mce_alternating_result_prefix)) * ff_vc_mce_fold_result) + (ff_n_mce_alternating_result_prefix))) /\ (((exists ff_even_mce_term_result_prefix_term. ff_index_mce_alternating_result_prefix = 2 * ff_even_mce_term_result_prefix_term) /\ (ff_p_mce_alternating_result_prefix = (ff_ap_mce_alternating_result_prefix) * (ff_bp_mce_alternating_result_prefix) + (ff_an_mce_alternating_result_prefix) * (ff_bn_mce_alternating_result_prefix) /\ ff_n_mce_alternating_result_prefix = (ff_ap_mce_alternating_result_prefix) * (ff_bn_mce_alternating_result_prefix) + (ff_an_mce_alternating_result_prefix) * (ff_bp_mce_alternating_result_prefix))) \/ ((exists ff_odd_mce_term_result_prefix_term. ff_index_mce_alternating_result_prefix = 2 * ff_odd_mce_term_result_prefix_term + 1) /\ (ff_p_mce_alternating_result_prefix = (ff_ap_mce_alternating_result_prefix) * (ff_bn_mce_alternating_result_prefix) + (ff_an_mce_alternating_result_prefix) * (ff_bp_mce_alternating_result_prefix) /\ ff_n_mce_alternating_result_prefix = (ff_ap_mce_alternating_result_prefix) * (ff_bp_mce_alternating_result_prefix) + (ff_an_mce_alternating_result_prefix) * (ff_bn_mce_alternating_result_prefix))))))))))) /\ ((exists ff_u_mce_result_positive ff_v_mce_result_positive. ((((exists ff_h_mce_result_positive_start. ff_h_mce_result_positive_start + S (0) = S ((S (0)) * ff_v_mce_result_positive)) /\ exists ff_q_mce_result_positive_start. ff_u_mce_result_positive = ff_q_mce_result_positive_start * S ((S (0)) * ff_v_mce_result_positive) + (0))) /\ ((((exists ff_h_mce_result_positive_terminal. ff_h_mce_result_positive_terminal + S (p) = S ((S (l)) * ff_v_mce_result_positive)) /\ exists ff_q_mce_result_positive_terminal. ff_u_mce_result_positive = ff_q_mce_result_positive_terminal * S ((S (l)) * ff_v_mce_result_positive) + (p))) /\ forall ff_i_mce_result_positive. (exists ff_lt_mce_result_positive_bound. ff_lt_mce_result_positive_bound + S ff_i_mce_result_positive = l) -> exists ff_a_mce_result_positive ff_r_mce_result_positive ff_s_mce_result_positive. ((((exists ff_h_mce_result_positive_summand. ff_h_mce_result_positive_summand + S (ff_a_mce_result_positive) = S ((S (ff_i_mce_result_positive)) * ff_uc_mce_fold_result)) /\ exists ff_q_mce_result_positive_summand. ff_ub_mce_fold_result = ff_q_mce_result_positive_summand * S ((S (ff_i_mce_result_positive)) * ff_uc_mce_fold_result) + (ff_a_mce_result_positive))) /\ ((((exists ff_h_mce_result_positive_partial. ff_h_mce_result_positive_partial + S (ff_r_mce_result_positive) = S ((S (ff_i_mce_result_positive)) * ff_v_mce_result_positive)) /\ exists ff_q_mce_result_positive_partial. ff_u_mce_result_positive = ff_q_mce_result_positive_partial * S ((S (ff_i_mce_result_positive)) * ff_v_mce_result_positive) + (ff_r_mce_result_positive))) /\ ((((exists ff_h_mce_result_positive_successor. ff_h_mce_result_positive_successor + S (ff_s_mce_result_positive) = S ((S (S ff_i_mce_result_positive)) * ff_v_mce_result_positive)) /\ exists ff_q_mce_result_positive_successor. ff_u_mce_result_positive = ff_q_mce_result_positive_successor * S ((S (S ff_i_mce_result_positive)) * ff_v_mce_result_positive) + (ff_s_mce_result_positive))) /\ ff_s_mce_result_positive = ff_r_mce_result_positive + ff_a_mce_result_positive)))))) /\ (exists ff_u_mce_result_negative ff_v_mce_result_negative. ((((exists ff_h_mce_result_negative_start. ff_h_mce_result_negative_start + S (0) = S ((S (0)) * ff_v_mce_result_negative)) /\ exists ff_q_mce_result_negative_start. ff_u_mce_result_negative = ff_q_mce_result_negative_start * S ((S (0)) * ff_v_mce_result_negative) + (0))) /\ ((((exists ff_h_mce_result_negative_terminal. ff_h_mce_result_negative_terminal + S (n) = S ((S (l)) * ff_v_mce_result_negative)) /\ exists ff_q_mce_result_negative_terminal. ff_u_mce_result_negative = ff_q_mce_result_negative_terminal * S ((S (l)) * ff_v_mce_result_negative) + (n))) /\ forall ff_i_mce_result_negative. (exists ff_lt_mce_result_negative_bound. ff_lt_mce_result_negative_bound + S ff_i_mce_result_negative = l) -> exists ff_a_mce_result_negative ff_r_mce_result_negative ff_s_mce_result_negative. ((((exists ff_h_mce_result_negative_summand. ff_h_mce_result_negative_summand + S (ff_a_mce_result_negative) = S ((S (ff_i_mce_result_negative)) * ff_vc_mce_fold_result)) /\ exists ff_q_mce_result_negative_summand. ff_vb_mce_fold_result = ff_q_mce_result_negative_summand * S ((S (ff_i_mce_result_negative)) * ff_vc_mce_fold_result) + (ff_a_mce_result_negative))) /\ ((((exists ff_h_mce_result_negative_partial. ff_h_mce_result_negative_partial + S (ff_r_mce_result_negative) = S ((S (ff_i_mce_result_negative)) * ff_v_mce_result_negative)) /\ exists ff_q_mce_result_negative_partial. ff_u_mce_result_negative = ff_q_mce_result_negative_partial * S ((S (ff_i_mce_result_negative)) * ff_v_mce_result_negative) + (ff_r_mce_result_negative))) /\ ((((exists ff_h_mce_result_negative_successor. ff_h_mce_result_negative_successor + S (ff_s_mce_result_negative) = S ((S (S ff_i_mce_result_negative)) * ff_v_mce_result_negative)) /\ exists ff_q_mce_result_negative_successor. ff_u_mce_result_negative = ff_q_mce_result_negative_successor * S ((S (S ff_i_mce_result_negative)) * ff_v_mce_result_negative) + (ff_s_mce_result_negative))) /\ ff_s_mce_result_negative = ff_r_mce_result_negative + ff_a_mce_result_negative))))))))) /\ forall r s. (exists ff_ub_mce_fold_other ff_uc_mce_fold_other ff_vb_mce_fold_other ff_vc_mce_fold_other. ((forall ff_index_mce_alternating_other_prefix. (exists ff_gap_mce_other_prefix_index. ff_gap_mce_other_prefix_index + S (ff_index_mce_alternating_other_prefix) = (l)) -> exists ff_ap_mce_alternating_other_prefix ff_an_mce_alternating_other_prefix ff_bp_mce_alternating_other_prefix ff_bn_mce_alternating_other_prefix ff_p_mce_alternating_other_prefix ff_n_mce_alternating_other_prefix. ((((exists ff_h_mce_other_prefix_ap. ff_h_mce_other_prefix_ap + S (ff_ap_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * ac)) /\ exists ff_q_mce_other_prefix_ap. ab = ff_q_mce_other_prefix_ap * S ((S (ff_index_mce_alternating_other_prefix)) * ac) + (ff_ap_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_an. ff_h_mce_other_prefix_an + S (ff_an_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * dc)) /\ exists ff_q_mce_other_prefix_an. db = ff_q_mce_other_prefix_an * S ((S (ff_index_mce_alternating_other_prefix)) * dc) + (ff_an_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_bp. ff_h_mce_other_prefix_bp + S (ff_bp_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * ec)) /\ exists ff_q_mce_other_prefix_bp. eb = ff_q_mce_other_prefix_bp * S ((S (ff_index_mce_alternating_other_prefix)) * ec) + (ff_bp_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_bn. ff_h_mce_other_prefix_bn + S (ff_bn_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * fc)) /\ exists ff_q_mce_other_prefix_bn. fb = ff_q_mce_other_prefix_bn * S ((S (ff_index_mce_alternating_other_prefix)) * fc) + (ff_bn_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_positive. ff_h_mce_other_prefix_positive + S (ff_p_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * ff_uc_mce_fold_other)) /\ exists ff_q_mce_other_prefix_positive. ff_ub_mce_fold_other = ff_q_mce_other_prefix_positive * S ((S (ff_index_mce_alternating_other_prefix)) * ff_uc_mce_fold_other) + (ff_p_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_negative. ff_h_mce_other_prefix_negative + S (ff_n_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * ff_vc_mce_fold_other)) /\ exists ff_q_mce_other_prefix_negative. ff_vb_mce_fold_other = ff_q_mce_other_prefix_negative * S ((S (ff_index_mce_alternating_other_prefix)) * ff_vc_mce_fold_other) + (ff_n_mce_alternating_other_prefix))) /\ (((exists ff_even_mce_term_other_prefix_term. ff_index_mce_alternating_other_prefix = 2 * ff_even_mce_term_other_prefix_term) /\ (ff_p_mce_alternating_other_prefix = (ff_ap_mce_alternating_other_prefix) * (ff_bp_mce_alternating_other_prefix) + (ff_an_mce_alternating_other_prefix) * (ff_bn_mce_alternating_other_prefix) /\ ff_n_mce_alternating_other_prefix = (ff_ap_mce_alternating_other_prefix) * (ff_bn_mce_alternating_other_prefix) + (ff_an_mce_alternating_other_prefix) * (ff_bp_mce_alternating_other_prefix))) \/ ((exists ff_odd_mce_term_other_prefix_term. ff_index_mce_alternating_other_prefix = 2 * ff_odd_mce_term_other_prefix_term + 1) /\ (ff_p_mce_alternating_other_prefix = (ff_ap_mce_alternating_other_prefix) * (ff_bn_mce_alternating_other_prefix) + (ff_an_mce_alternating_other_prefix) * (ff_bp_mce_alternating_other_prefix) /\ ff_n_mce_alternating_other_prefix = (ff_ap_mce_alternating_other_prefix) * (ff_bp_mce_alternating_other_prefix) + (ff_an_mce_alternating_other_prefix) * (ff_bn_mce_alternating_other_prefix))))))))))) /\ ((exists ff_u_mce_other_positive ff_v_mce_other_positive. ((((exists ff_h_mce_other_positive_start. ff_h_mce_other_positive_start + S (0) = S ((S (0)) * ff_v_mce_other_positive)) /\ exists ff_q_mce_other_positive_start. ff_u_mce_other_positive = ff_q_mce_other_positive_start * S ((S (0)) * ff_v_mce_other_positive) + (0))) /\ ((((exists ff_h_mce_other_positive_terminal. ff_h_mce_other_positive_terminal + S (r) = S ((S (l)) * ff_v_mce_other_positive)) /\ exists ff_q_mce_other_positive_terminal. ff_u_mce_other_positive = ff_q_mce_other_positive_terminal * S ((S (l)) * ff_v_mce_other_positive) + (r))) /\ forall ff_i_mce_other_positive. (exists ff_lt_mce_other_positive_bound. ff_lt_mce_other_positive_bound + S ff_i_mce_other_positive = l) -> exists ff_a_mce_other_positive ff_r_mce_other_positive ff_s_mce_other_positive. ((((exists ff_h_mce_other_positive_summand. ff_h_mce_other_positive_summand + S (ff_a_mce_other_positive) = S ((S (ff_i_mce_other_positive)) * ff_uc_mce_fold_other)) /\ exists ff_q_mce_other_positive_summand. ff_ub_mce_fold_other = ff_q_mce_other_positive_summand * S ((S (ff_i_mce_other_positive)) * ff_uc_mce_fold_other) + (ff_a_mce_other_positive))) /\ ((((exists ff_h_mce_other_positive_partial. ff_h_mce_other_positive_partial + S (ff_r_mce_other_positive) = S ((S (ff_i_mce_other_positive)) * ff_v_mce_other_positive)) /\ exists ff_q_mce_other_positive_partial. ff_u_mce_other_positive = ff_q_mce_other_positive_partial * S ((S (ff_i_mce_other_positive)) * ff_v_mce_other_positive) + (ff_r_mce_other_positive))) /\ ((((exists ff_h_mce_other_positive_successor. ff_h_mce_other_positive_successor + S (ff_s_mce_other_positive) = S ((S (S ff_i_mce_other_positive)) * ff_v_mce_other_positive)) /\ exists ff_q_mce_other_positive_successor. ff_u_mce_other_positive = ff_q_mce_other_positive_successor * S ((S (S ff_i_mce_other_positive)) * ff_v_mce_other_positive) + (ff_s_mce_other_positive))) /\ ff_s_mce_other_positive = ff_r_mce_other_positive + ff_a_mce_other_positive)))))) /\ (exists ff_u_mce_other_negative ff_v_mce_other_negative. ((((exists ff_h_mce_other_negative_start. ff_h_mce_other_negative_start + S (0) = S ((S (0)) * ff_v_mce_other_negative)) /\ exists ff_q_mce_other_negative_start. ff_u_mce_other_negative = ff_q_mce_other_negative_start * S ((S (0)) * ff_v_mce_other_negative) + (0))) /\ ((((exists ff_h_mce_other_negative_terminal. ff_h_mce_other_negative_terminal + S (s) = S ((S (l)) * ff_v_mce_other_negative)) /\ exists ff_q_mce_other_negative_terminal. ff_u_mce_other_negative = ff_q_mce_other_negative_terminal * S ((S (l)) * ff_v_mce_other_negative) + (s))) /\ forall ff_i_mce_other_negative. (exists ff_lt_mce_other_negative_bound. ff_lt_mce_other_negative_bound + S ff_i_mce_other_negative = l) -> exists ff_a_mce_other_negative ff_r_mce_other_negative ff_s_mce_other_negative. ((((exists ff_h_mce_other_negative_summand. ff_h_mce_other_negative_summand + S (ff_a_mce_other_negative) = S ((S (ff_i_mce_other_negative)) * ff_vc_mce_fold_other)) /\ exists ff_q_mce_other_negative_summand. ff_vb_mce_fold_other = ff_q_mce_other_negative_summand * S ((S (ff_i_mce_other_negative)) * ff_vc_mce_fold_other) + (ff_a_mce_other_negative))) /\ ((((exists ff_h_mce_other_negative_partial. ff_h_mce_other_negative_partial + S (ff_r_mce_other_negative) = S ((S (ff_i_mce_other_negative)) * ff_v_mce_other_negative)) /\ exists ff_q_mce_other_negative_partial. ff_u_mce_other_negative = ff_q_mce_other_negative_partial * S ((S (ff_i_mce_other_negative)) * ff_v_mce_other_negative) + (ff_r_mce_other_negative))) /\ ((((exists ff_h_mce_other_negative_successor. ff_h_mce_other_negative_successor + S (ff_s_mce_other_negative) = S ((S (S ff_i_mce_other_negative)) * ff_v_mce_other_negative)) /\ exists ff_q_mce_other_negative_successor. ff_u_mce_other_negative = ff_q_mce_other_negative_successor * S ((S (S ff_i_mce_other_negative)) * ff_v_mce_other_negative) + (ff_s_mce_other_negative))) /\ ff_s_mce_other_negative = ff_r_mce_other_negative + ff_a_mce_other_negative))))))))) -> (p = r /\ n = s))