prime_field_polynomial_aligned_add_associative

Exact expanded first-order arithmetic statement

forall p ab ac La bb bc Lb cb cc Lc ub uc Lu vb vc Lv rb rc Lr sb sc Ls. (~((p) = 1) /\ forall pfa_factor_left_associative_prime pfa_factor_right_associative_prime. (p) = pfa_factor_left_associative_prime * pfa_factor_right_associative_prime -> pfa_factor_left_associative_prime = 1 \/ pfa_factor_right_associative_prime = 1) -> (((forall fom_index_pfp_associative_0_left_bounded. (exists fom_gap_pfp_associative_0_left_bounded_index_bound. fom_gap_pfp_associative_0_left_bounded_index_bound + S (fom_index_pfp_associative_0_left_bounded) = La) -> exists fom_value_pfp_associative_0_left_bounded. ((((exists fom_beta_height_pfp_associative_0_left_bounded_entry. fom_beta_height_pfp_associative_0_left_bounded_entry + S (fom_value_pfp_associative_0_left_bounded) = S ((S (fom_index_pfp_associative_0_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_associative_0_left_bounded_entry. ab = fom_beta_quotient_pfp_associative_0_left_bounded_entry * S ((S (fom_index_pfp_associative_0_left_bounded)) * ac) + (fom_value_pfp_associative_0_left_bounded))) /\ (exists fom_gap_pfp_associative_0_left_bounded_value_bound. fom_gap_pfp_associative_0_left_bounded_value_bound + S (fom_value_pfp_associative_0_left_bounded) = p))) /\ (((forall fom_index_pfp_associative_0_right_bounded. (exists fom_gap_pfp_associative_0_right_bounded_index_bound. fom_gap_pfp_associative_0_right_bounded_index_bound + S (fom_index_pfp_associative_0_right_bounded) = Lb) -> exists fom_value_pfp_associative_0_right_bounded. ((((exists fom_beta_height_pfp_associative_0_right_bounded_entry. fom_beta_height_pfp_associative_0_right_bounded_entry + S (fom_value_pfp_associative_0_right_bounded) = S ((S (fom_index_pfp_associative_0_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_associative_0_right_bounded_entry. bb = fom_beta_quotient_pfp_associative_0_right_bounded_entry * S ((S (fom_index_pfp_associative_0_right_bounded)) * bc) + (fom_value_pfp_associative_0_right_bounded))) /\ (exists fom_gap_pfp_associative_0_right_bounded_value_bound. fom_gap_pfp_associative_0_right_bounded_value_bound + S (fom_value_pfp_associative_0_right_bounded) = p))) /\ (((forall fom_index_pfp_associative_0_result_bounded. (exists fom_gap_pfp_associative_0_result_bounded_index_bound. fom_gap_pfp_associative_0_result_bounded_index_bound + S (fom_index_pfp_associative_0_result_bounded) = Lu) -> exists fom_value_pfp_associative_0_result_bounded. ((((exists fom_beta_height_pfp_associative_0_result_bounded_entry. fom_beta_height_pfp_associative_0_result_bounded_entry + S (fom_value_pfp_associative_0_result_bounded) = S ((S (fom_index_pfp_associative_0_result_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_associative_0_result_bounded_entry. ub = fom_beta_quotient_pfp_associative_0_result_bounded_entry * S ((S (fom_index_pfp_associative_0_result_bounded)) * uc) + (fom_value_pfp_associative_0_result_bounded))) /\ (exists fom_gap_pfp_associative_0_result_bounded_value_bound. fom_gap_pfp_associative_0_result_bounded_value_bound + S (fom_value_pfp_associative_0_result_bounded) = p))) /\ ((exists pfaa_left_b_associative_0 pfaa_left_c_associative_0 pfaa_right_b_associative_0 pfaa_right_c_associative_0 pfaa_sum_b_associative_0 pfaa_sum_c_associative_0 pfaa_length_associative_0. ((((forall pfrep_power_associative_0_witness_common_left pfrep_left_associative_0_witness_common_left pfrep_right_associative_0_witness_common_left. ((exists pfrep_position_associative_0_witness_common_leftfirst. ((pfrep_position_associative_0_witness_common_leftfirst+S (pfrep_power_associative_0_witness_common_left)=(La)) /\ ((((exists ff_h_pfp_associative_0_witness_common_leftfirstentry. ff_h_pfp_associative_0_witness_common_leftfirstentry + S (pfrep_left_associative_0_witness_common_left) = S ((S (pfrep_position_associative_0_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_associative_0_witness_common_leftfirstentry. ab = ff_q_pfp_associative_0_witness_common_leftfirstentry * S ((S (pfrep_position_associative_0_witness_common_leftfirst)) * ac) + (pfrep_left_associative_0_witness_common_left)))))) \/ (((exists pfrep_gap_associative_0_witness_common_leftfirstoutside. pfrep_gap_associative_0_witness_common_leftfirstoutside+(La)=(pfrep_power_associative_0_witness_common_left)) /\ (((pfrep_left_associative_0_witness_common_left)=0))))) -> ((exists pfrep_position_associative_0_witness_common_leftsecond. ((pfrep_position_associative_0_witness_common_leftsecond+S (pfrep_power_associative_0_witness_common_left)=(pfaa_length_associative_0)) /\ ((((exists ff_h_pfp_associative_0_witness_common_leftsecondentry. ff_h_pfp_associative_0_witness_common_leftsecondentry + S (pfrep_right_associative_0_witness_common_left) = S ((S (pfrep_position_associative_0_witness_common_leftsecond)) * pfaa_left_c_associative_0)) /\ exists ff_q_pfp_associative_0_witness_common_leftsecondentry. pfaa_left_b_associative_0 = ff_q_pfp_associative_0_witness_common_leftsecondentry * S ((S (pfrep_position_associative_0_witness_common_leftsecond)) * pfaa_left_c_associative_0) + (pfrep_right_associative_0_witness_common_left)))))) \/ (((exists pfrep_gap_associative_0_witness_common_leftsecondoutside. pfrep_gap_associative_0_witness_common_leftsecondoutside+(pfaa_length_associative_0)=(pfrep_power_associative_0_witness_common_left)) /\ (((pfrep_right_associative_0_witness_common_left)=0))))) -> pfrep_left_associative_0_witness_common_left=pfrep_right_associative_0_witness_common_left) /\ ((forall pfrep_power_associative_0_witness_common_right pfrep_left_associative_0_witness_common_right pfrep_right_associative_0_witness_common_right. ((exists pfrep_position_associative_0_witness_common_rightfirst. ((pfrep_position_associative_0_witness_common_rightfirst+S (pfrep_power_associative_0_witness_common_right)=(Lb)) /\ ((((exists ff_h_pfp_associative_0_witness_common_rightfirstentry. ff_h_pfp_associative_0_witness_common_rightfirstentry + S (pfrep_left_associative_0_witness_common_right) = S ((S (pfrep_position_associative_0_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_associative_0_witness_common_rightfirstentry. bb = ff_q_pfp_associative_0_witness_common_rightfirstentry * S ((S (pfrep_position_associative_0_witness_common_rightfirst)) * bc) + (pfrep_left_associative_0_witness_common_right)))))) \/ (((exists pfrep_gap_associative_0_witness_common_rightfirstoutside. pfrep_gap_associative_0_witness_common_rightfirstoutside+(Lb)=(pfrep_power_associative_0_witness_common_right)) /\ (((pfrep_left_associative_0_witness_common_right)=0))))) -> ((exists pfrep_position_associative_0_witness_common_rightsecond. ((pfrep_position_associative_0_witness_common_rightsecond+S (pfrep_power_associative_0_witness_common_right)=(pfaa_length_associative_0)) /\ ((((exists ff_h_pfp_associative_0_witness_common_rightsecondentry. ff_h_pfp_associative_0_witness_common_rightsecondentry + S (pfrep_right_associative_0_witness_common_right) = S ((S (pfrep_position_associative_0_witness_common_rightsecond)) * pfaa_right_c_associative_0)) /\ exists ff_q_pfp_associative_0_witness_common_rightsecondentry. pfaa_right_b_associative_0 = ff_q_pfp_associative_0_witness_common_rightsecondentry * S ((S (pfrep_position_associative_0_witness_common_rightsecond)) * pfaa_right_c_associative_0) + (pfrep_right_associative_0_witness_common_right)))))) \/ (((exists pfrep_gap_associative_0_witness_common_rightsecondoutside. pfrep_gap_associative_0_witness_common_rightsecondoutside+(pfaa_length_associative_0)=(pfrep_power_associative_0_witness_common_right)) /\ (((pfrep_right_associative_0_witness_common_right)=0))))) -> pfrep_left_associative_0_witness_common_right=pfrep_right_associative_0_witness_common_right)))) /\ (((forall pfp_index_associative_0_witness_operation. (exists pfa_gap_associative_0_witness_operationindex. pfa_gap_associative_0_witness_operationindex + S (pfp_index_associative_0_witness_operation) = (pfaa_length_associative_0)) -> exists pfp_left_associative_0_witness_operation pfp_right_associative_0_witness_operation pfp_value_associative_0_witness_operation. ((((exists ff_h_pfp_associative_0_witness_operationleft. ff_h_pfp_associative_0_witness_operationleft + S (pfp_left_associative_0_witness_operation) = S ((S (pfp_index_associative_0_witness_operation)) * pfaa_left_c_associative_0)) /\ exists ff_q_pfp_associative_0_witness_operationleft. pfaa_left_b_associative_0 = ff_q_pfp_associative_0_witness_operationleft * S ((S (pfp_index_associative_0_witness_operation)) * pfaa_left_c_associative_0) + (pfp_left_associative_0_witness_operation))) /\ (((((exists ff_h_pfp_associative_0_witness_operationright. ff_h_pfp_associative_0_witness_operationright + S (pfp_right_associative_0_witness_operation) = S ((S (pfp_index_associative_0_witness_operation)) * pfaa_right_c_associative_0)) /\ exists ff_q_pfp_associative_0_witness_operationright. pfaa_right_b_associative_0 = ff_q_pfp_associative_0_witness_operationright * S ((S (pfp_index_associative_0_witness_operation)) * pfaa_right_c_associative_0) + (pfp_right_associative_0_witness_operation))) /\ (((((exists ff_h_pfp_associative_0_witness_operationtarget. ff_h_pfp_associative_0_witness_operationtarget + S (pfp_value_associative_0_witness_operation) = S ((S (pfp_index_associative_0_witness_operation)) * pfaa_sum_c_associative_0)) /\ exists ff_q_pfp_associative_0_witness_operationtarget. pfaa_sum_b_associative_0 = ff_q_pfp_associative_0_witness_operationtarget * S ((S (pfp_index_associative_0_witness_operation)) * pfaa_sum_c_associative_0) + (pfp_value_associative_0_witness_operation))) /\ ((((exists pfa_gap_associative_0_witness_operationoperationleft. pfa_gap_associative_0_witness_operationoperationleft + S (pfp_left_associative_0_witness_operation) = (p)) /\ (((exists pfa_gap_associative_0_witness_operationoperationright. pfa_gap_associative_0_witness_operationoperationright + S (pfp_right_associative_0_witness_operation) = (p)) /\ ((((exists pfa_gap_associative_0_witness_operationoperationresultbound. pfa_gap_associative_0_witness_operationoperationresultbound + S (pfp_value_associative_0_witness_operation) = (p)) /\ ((exists pfa_offset_left_associative_0_witness_operationoperationresultcongruence pfa_offset_right_associative_0_witness_operationoperationresultcongruence. ((pfp_left_associative_0_witness_operation) + (pfp_right_associative_0_witness_operation)) + (p) * pfa_offset_left_associative_0_witness_operationoperationresultcongruence = (pfp_value_associative_0_witness_operation) + (p) * pfa_offset_right_associative_0_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_associative_0_witness_output pfrep_left_associative_0_witness_output pfrep_right_associative_0_witness_output. ((exists pfrep_position_associative_0_witness_outputfirst. ((pfrep_position_associative_0_witness_outputfirst+S (pfrep_power_associative_0_witness_output)=(pfaa_length_associative_0)) /\ ((((exists ff_h_pfp_associative_0_witness_outputfirstentry. ff_h_pfp_associative_0_witness_outputfirstentry + S (pfrep_left_associative_0_witness_output) = S ((S (pfrep_position_associative_0_witness_outputfirst)) * pfaa_sum_c_associative_0)) /\ exists ff_q_pfp_associative_0_witness_outputfirstentry. pfaa_sum_b_associative_0 = ff_q_pfp_associative_0_witness_outputfirstentry * S ((S (pfrep_position_associative_0_witness_outputfirst)) * pfaa_sum_c_associative_0) + (pfrep_left_associative_0_witness_output)))))) \/ (((exists pfrep_gap_associative_0_witness_outputfirstoutside. pfrep_gap_associative_0_witness_outputfirstoutside+(pfaa_length_associative_0)=(pfrep_power_associative_0_witness_output)) /\ (((pfrep_left_associative_0_witness_output)=0))))) -> ((exists pfrep_position_associative_0_witness_outputsecond. ((pfrep_position_associative_0_witness_outputsecond+S (pfrep_power_associative_0_witness_output)=(Lu)) /\ ((((exists ff_h_pfp_associative_0_witness_outputsecondentry. ff_h_pfp_associative_0_witness_outputsecondentry + S (pfrep_right_associative_0_witness_output) = S ((S (pfrep_position_associative_0_witness_outputsecond)) * uc)) /\ exists ff_q_pfp_associative_0_witness_outputsecondentry. ub = ff_q_pfp_associative_0_witness_outputsecondentry * S ((S (pfrep_position_associative_0_witness_outputsecond)) * uc) + (pfrep_right_associative_0_witness_output)))))) \/ (((exists pfrep_gap_associative_0_witness_outputsecondoutside. pfrep_gap_associative_0_witness_outputsecondoutside+(Lu)=(pfrep_power_associative_0_witness_output)) /\ (((pfrep_right_associative_0_witness_output)=0))))) -> pfrep_left_associative_0_witness_output=pfrep_right_associative_0_witness_output))))))))))))) -> (((forall fom_index_pfp_associative_1_left_bounded. (exists fom_gap_pfp_associative_1_left_bounded_index_bound. fom_gap_pfp_associative_1_left_bounded_index_bound + S (fom_index_pfp_associative_1_left_bounded) = Lu) -> exists fom_value_pfp_associative_1_left_bounded. ((((exists fom_beta_height_pfp_associative_1_left_bounded_entry. fom_beta_height_pfp_associative_1_left_bounded_entry + S (fom_value_pfp_associative_1_left_bounded) = S ((S (fom_index_pfp_associative_1_left_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_associative_1_left_bounded_entry. ub = fom_beta_quotient_pfp_associative_1_left_bounded_entry * S ((S (fom_index_pfp_associative_1_left_bounded)) * uc) + (fom_value_pfp_associative_1_left_bounded))) /\ (exists fom_gap_pfp_associative_1_left_bounded_value_bound. fom_gap_pfp_associative_1_left_bounded_value_bound + S (fom_value_pfp_associative_1_left_bounded) = p))) /\ (((forall fom_index_pfp_associative_1_right_bounded. (exists fom_gap_pfp_associative_1_right_bounded_index_bound. fom_gap_pfp_associative_1_right_bounded_index_bound + S (fom_index_pfp_associative_1_right_bounded) = Lc) -> exists fom_value_pfp_associative_1_right_bounded. ((((exists fom_beta_height_pfp_associative_1_right_bounded_entry. fom_beta_height_pfp_associative_1_right_bounded_entry + S (fom_value_pfp_associative_1_right_bounded) = S ((S (fom_index_pfp_associative_1_right_bounded)) * cc)) /\ exists fom_beta_quotient_pfp_associative_1_right_bounded_entry. cb = fom_beta_quotient_pfp_associative_1_right_bounded_entry * S ((S (fom_index_pfp_associative_1_right_bounded)) * cc) + (fom_value_pfp_associative_1_right_bounded))) /\ (exists fom_gap_pfp_associative_1_right_bounded_value_bound. fom_gap_pfp_associative_1_right_bounded_value_bound + S (fom_value_pfp_associative_1_right_bounded) = p))) /\ (((forall fom_index_pfp_associative_1_result_bounded. (exists fom_gap_pfp_associative_1_result_bounded_index_bound. fom_gap_pfp_associative_1_result_bounded_index_bound + S (fom_index_pfp_associative_1_result_bounded) = Lr) -> exists fom_value_pfp_associative_1_result_bounded. ((((exists fom_beta_height_pfp_associative_1_result_bounded_entry. fom_beta_height_pfp_associative_1_result_bounded_entry + S (fom_value_pfp_associative_1_result_bounded) = S ((S (fom_index_pfp_associative_1_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_associative_1_result_bounded_entry. rb = fom_beta_quotient_pfp_associative_1_result_bounded_entry * S ((S (fom_index_pfp_associative_1_result_bounded)) * rc) + (fom_value_pfp_associative_1_result_bounded))) /\ (exists fom_gap_pfp_associative_1_result_bounded_value_bound. fom_gap_pfp_associative_1_result_bounded_value_bound + S (fom_value_pfp_associative_1_result_bounded) = p))) /\ ((exists pfaa_left_b_associative_1 pfaa_left_c_associative_1 pfaa_right_b_associative_1 pfaa_right_c_associative_1 pfaa_sum_b_associative_1 pfaa_sum_c_associative_1 pfaa_length_associative_1. ((((forall pfrep_power_associative_1_witness_common_left pfrep_left_associative_1_witness_common_left pfrep_right_associative_1_witness_common_left. ((exists pfrep_position_associative_1_witness_common_leftfirst. ((pfrep_position_associative_1_witness_common_leftfirst+S (pfrep_power_associative_1_witness_common_left)=(Lu)) /\ ((((exists ff_h_pfp_associative_1_witness_common_leftfirstentry. ff_h_pfp_associative_1_witness_common_leftfirstentry + S (pfrep_left_associative_1_witness_common_left) = S ((S (pfrep_position_associative_1_witness_common_leftfirst)) * uc)) /\ exists ff_q_pfp_associative_1_witness_common_leftfirstentry. ub = ff_q_pfp_associative_1_witness_common_leftfirstentry * S ((S (pfrep_position_associative_1_witness_common_leftfirst)) * uc) + (pfrep_left_associative_1_witness_common_left)))))) \/ (((exists pfrep_gap_associative_1_witness_common_leftfirstoutside. pfrep_gap_associative_1_witness_common_leftfirstoutside+(Lu)=(pfrep_power_associative_1_witness_common_left)) /\ (((pfrep_left_associative_1_witness_common_left)=0))))) -> ((exists pfrep_position_associative_1_witness_common_leftsecond. ((pfrep_position_associative_1_witness_common_leftsecond+S (pfrep_power_associative_1_witness_common_left)=(pfaa_length_associative_1)) /\ ((((exists ff_h_pfp_associative_1_witness_common_leftsecondentry. ff_h_pfp_associative_1_witness_common_leftsecondentry + S (pfrep_right_associative_1_witness_common_left) = S ((S (pfrep_position_associative_1_witness_common_leftsecond)) * pfaa_left_c_associative_1)) /\ exists ff_q_pfp_associative_1_witness_common_leftsecondentry. pfaa_left_b_associative_1 = ff_q_pfp_associative_1_witness_common_leftsecondentry * S ((S (pfrep_position_associative_1_witness_common_leftsecond)) * pfaa_left_c_associative_1) + (pfrep_right_associative_1_witness_common_left)))))) \/ (((exists pfrep_gap_associative_1_witness_common_leftsecondoutside. pfrep_gap_associative_1_witness_common_leftsecondoutside+(pfaa_length_associative_1)=(pfrep_power_associative_1_witness_common_left)) /\ (((pfrep_right_associative_1_witness_common_left)=0))))) -> pfrep_left_associative_1_witness_common_left=pfrep_right_associative_1_witness_common_left) /\ ((forall pfrep_power_associative_1_witness_common_right pfrep_left_associative_1_witness_common_right pfrep_right_associative_1_witness_common_right. ((exists pfrep_position_associative_1_witness_common_rightfirst. ((pfrep_position_associative_1_witness_common_rightfirst+S (pfrep_power_associative_1_witness_common_right)=(Lc)) /\ ((((exists ff_h_pfp_associative_1_witness_common_rightfirstentry. ff_h_pfp_associative_1_witness_common_rightfirstentry + S (pfrep_left_associative_1_witness_common_right) = S ((S (pfrep_position_associative_1_witness_common_rightfirst)) * cc)) /\ exists ff_q_pfp_associative_1_witness_common_rightfirstentry. cb = ff_q_pfp_associative_1_witness_common_rightfirstentry * S ((S (pfrep_position_associative_1_witness_common_rightfirst)) * cc) + (pfrep_left_associative_1_witness_common_right)))))) \/ (((exists pfrep_gap_associative_1_witness_common_rightfirstoutside. pfrep_gap_associative_1_witness_common_rightfirstoutside+(Lc)=(pfrep_power_associative_1_witness_common_right)) /\ (((pfrep_left_associative_1_witness_common_right)=0))))) -> ((exists pfrep_position_associative_1_witness_common_rightsecond. ((pfrep_position_associative_1_witness_common_rightsecond+S (pfrep_power_associative_1_witness_common_right)=(pfaa_length_associative_1)) /\ ((((exists ff_h_pfp_associative_1_witness_common_rightsecondentry. ff_h_pfp_associative_1_witness_common_rightsecondentry + S (pfrep_right_associative_1_witness_common_right) = S ((S (pfrep_position_associative_1_witness_common_rightsecond)) * pfaa_right_c_associative_1)) /\ exists ff_q_pfp_associative_1_witness_common_rightsecondentry. pfaa_right_b_associative_1 = ff_q_pfp_associative_1_witness_common_rightsecondentry * S ((S (pfrep_position_associative_1_witness_common_rightsecond)) * pfaa_right_c_associative_1) + (pfrep_right_associative_1_witness_common_right)))))) \/ (((exists pfrep_gap_associative_1_witness_common_rightsecondoutside. pfrep_gap_associative_1_witness_common_rightsecondoutside+(pfaa_length_associative_1)=(pfrep_power_associative_1_witness_common_right)) /\ (((pfrep_right_associative_1_witness_common_right)=0))))) -> pfrep_left_associative_1_witness_common_right=pfrep_right_associative_1_witness_common_right)))) /\ (((forall pfp_index_associative_1_witness_operation. (exists pfa_gap_associative_1_witness_operationindex. pfa_gap_associative_1_witness_operationindex + S (pfp_index_associative_1_witness_operation) = (pfaa_length_associative_1)) -> exists pfp_left_associative_1_witness_operation pfp_right_associative_1_witness_operation pfp_value_associative_1_witness_operation. ((((exists ff_h_pfp_associative_1_witness_operationleft. ff_h_pfp_associative_1_witness_operationleft + S (pfp_left_associative_1_witness_operation) = S ((S (pfp_index_associative_1_witness_operation)) * pfaa_left_c_associative_1)) /\ exists ff_q_pfp_associative_1_witness_operationleft. pfaa_left_b_associative_1 = ff_q_pfp_associative_1_witness_operationleft * S ((S (pfp_index_associative_1_witness_operation)) * pfaa_left_c_associative_1) + (pfp_left_associative_1_witness_operation))) /\ (((((exists ff_h_pfp_associative_1_witness_operationright. ff_h_pfp_associative_1_witness_operationright + S (pfp_right_associative_1_witness_operation) = S ((S (pfp_index_associative_1_witness_operation)) * pfaa_right_c_associative_1)) /\ exists ff_q_pfp_associative_1_witness_operationright. pfaa_right_b_associative_1 = ff_q_pfp_associative_1_witness_operationright * S ((S (pfp_index_associative_1_witness_operation)) * pfaa_right_c_associative_1) + (pfp_right_associative_1_witness_operation))) /\ (((((exists ff_h_pfp_associative_1_witness_operationtarget. ff_h_pfp_associative_1_witness_operationtarget + S (pfp_value_associative_1_witness_operation) = S ((S (pfp_index_associative_1_witness_operation)) * pfaa_sum_c_associative_1)) /\ exists ff_q_pfp_associative_1_witness_operationtarget. pfaa_sum_b_associative_1 = ff_q_pfp_associative_1_witness_operationtarget * S ((S (pfp_index_associative_1_witness_operation)) * pfaa_sum_c_associative_1) + (pfp_value_associative_1_witness_operation))) /\ ((((exists pfa_gap_associative_1_witness_operationoperationleft. pfa_gap_associative_1_witness_operationoperationleft + S (pfp_left_associative_1_witness_operation) = (p)) /\ (((exists pfa_gap_associative_1_witness_operationoperationright. pfa_gap_associative_1_witness_operationoperationright + S (pfp_right_associative_1_witness_operation) = (p)) /\ ((((exists pfa_gap_associative_1_witness_operationoperationresultbound. pfa_gap_associative_1_witness_operationoperationresultbound + S (pfp_value_associative_1_witness_operation) = (p)) /\ ((exists pfa_offset_left_associative_1_witness_operationoperationresultcongruence pfa_offset_right_associative_1_witness_operationoperationresultcongruence. ((pfp_left_associative_1_witness_operation) + (pfp_right_associative_1_witness_operation)) + (p) * pfa_offset_left_associative_1_witness_operationoperationresultcongruence = (pfp_value_associative_1_witness_operation) + (p) * pfa_offset_right_associative_1_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_associative_1_witness_output pfrep_left_associative_1_witness_output pfrep_right_associative_1_witness_output. ((exists pfrep_position_associative_1_witness_outputfirst. ((pfrep_position_associative_1_witness_outputfirst+S (pfrep_power_associative_1_witness_output)=(pfaa_length_associative_1)) /\ ((((exists ff_h_pfp_associative_1_witness_outputfirstentry. ff_h_pfp_associative_1_witness_outputfirstentry + S (pfrep_left_associative_1_witness_output) = S ((S (pfrep_position_associative_1_witness_outputfirst)) * pfaa_sum_c_associative_1)) /\ exists ff_q_pfp_associative_1_witness_outputfirstentry. pfaa_sum_b_associative_1 = ff_q_pfp_associative_1_witness_outputfirstentry * S ((S (pfrep_position_associative_1_witness_outputfirst)) * pfaa_sum_c_associative_1) + (pfrep_left_associative_1_witness_output)))))) \/ (((exists pfrep_gap_associative_1_witness_outputfirstoutside. pfrep_gap_associative_1_witness_outputfirstoutside+(pfaa_length_associative_1)=(pfrep_power_associative_1_witness_output)) /\ (((pfrep_left_associative_1_witness_output)=0))))) -> ((exists pfrep_position_associative_1_witness_outputsecond. ((pfrep_position_associative_1_witness_outputsecond+S (pfrep_power_associative_1_witness_output)=(Lr)) /\ ((((exists ff_h_pfp_associative_1_witness_outputsecondentry. ff_h_pfp_associative_1_witness_outputsecondentry + S (pfrep_right_associative_1_witness_output) = S ((S (pfrep_position_associative_1_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_associative_1_witness_outputsecondentry. rb = ff_q_pfp_associative_1_witness_outputsecondentry * S ((S (pfrep_position_associative_1_witness_outputsecond)) * rc) + (pfrep_right_associative_1_witness_output)))))) \/ (((exists pfrep_gap_associative_1_witness_outputsecondoutside. pfrep_gap_associative_1_witness_outputsecondoutside+(Lr)=(pfrep_power_associative_1_witness_output)) /\ (((pfrep_right_associative_1_witness_output)=0))))) -> pfrep_left_associative_1_witness_output=pfrep_right_associative_1_witness_output))))))))))))) -> (((forall fom_index_pfp_associative_2_left_bounded. (exists fom_gap_pfp_associative_2_left_bounded_index_bound. fom_gap_pfp_associative_2_left_bounded_index_bound + S (fom_index_pfp_associative_2_left_bounded) = Lb) -> exists fom_value_pfp_associative_2_left_bounded. ((((exists fom_beta_height_pfp_associative_2_left_bounded_entry. fom_beta_height_pfp_associative_2_left_bounded_entry + S (fom_value_pfp_associative_2_left_bounded) = S ((S (fom_index_pfp_associative_2_left_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_associative_2_left_bounded_entry. bb = fom_beta_quotient_pfp_associative_2_left_bounded_entry * S ((S (fom_index_pfp_associative_2_left_bounded)) * bc) + (fom_value_pfp_associative_2_left_bounded))) /\ (exists fom_gap_pfp_associative_2_left_bounded_value_bound. fom_gap_pfp_associative_2_left_bounded_value_bound + S (fom_value_pfp_associative_2_left_bounded) = p))) /\ (((forall fom_index_pfp_associative_2_right_bounded. (exists fom_gap_pfp_associative_2_right_bounded_index_bound. fom_gap_pfp_associative_2_right_bounded_index_bound + S (fom_index_pfp_associative_2_right_bounded) = Lc) -> exists fom_value_pfp_associative_2_right_bounded. ((((exists fom_beta_height_pfp_associative_2_right_bounded_entry. fom_beta_height_pfp_associative_2_right_bounded_entry + S (fom_value_pfp_associative_2_right_bounded) = S ((S (fom_index_pfp_associative_2_right_bounded)) * cc)) /\ exists fom_beta_quotient_pfp_associative_2_right_bounded_entry. cb = fom_beta_quotient_pfp_associative_2_right_bounded_entry * S ((S (fom_index_pfp_associative_2_right_bounded)) * cc) + (fom_value_pfp_associative_2_right_bounded))) /\ (exists fom_gap_pfp_associative_2_right_bounded_value_bound. fom_gap_pfp_associative_2_right_bounded_value_bound + S (fom_value_pfp_associative_2_right_bounded) = p))) /\ (((forall fom_index_pfp_associative_2_result_bounded. (exists fom_gap_pfp_associative_2_result_bounded_index_bound. fom_gap_pfp_associative_2_result_bounded_index_bound + S (fom_index_pfp_associative_2_result_bounded) = Lv) -> exists fom_value_pfp_associative_2_result_bounded. ((((exists fom_beta_height_pfp_associative_2_result_bounded_entry. fom_beta_height_pfp_associative_2_result_bounded_entry + S (fom_value_pfp_associative_2_result_bounded) = S ((S (fom_index_pfp_associative_2_result_bounded)) * vc)) /\ exists fom_beta_quotient_pfp_associative_2_result_bounded_entry. vb = fom_beta_quotient_pfp_associative_2_result_bounded_entry * S ((S (fom_index_pfp_associative_2_result_bounded)) * vc) + (fom_value_pfp_associative_2_result_bounded))) /\ (exists fom_gap_pfp_associative_2_result_bounded_value_bound. fom_gap_pfp_associative_2_result_bounded_value_bound + S (fom_value_pfp_associative_2_result_bounded) = p))) /\ ((exists pfaa_left_b_associative_2 pfaa_left_c_associative_2 pfaa_right_b_associative_2 pfaa_right_c_associative_2 pfaa_sum_b_associative_2 pfaa_sum_c_associative_2 pfaa_length_associative_2. ((((forall pfrep_power_associative_2_witness_common_left pfrep_left_associative_2_witness_common_left pfrep_right_associative_2_witness_common_left. ((exists pfrep_position_associative_2_witness_common_leftfirst. ((pfrep_position_associative_2_witness_common_leftfirst+S (pfrep_power_associative_2_witness_common_left)=(Lb)) /\ ((((exists ff_h_pfp_associative_2_witness_common_leftfirstentry. ff_h_pfp_associative_2_witness_common_leftfirstentry + S (pfrep_left_associative_2_witness_common_left) = S ((S (pfrep_position_associative_2_witness_common_leftfirst)) * bc)) /\ exists ff_q_pfp_associative_2_witness_common_leftfirstentry. bb = ff_q_pfp_associative_2_witness_common_leftfirstentry * S ((S (pfrep_position_associative_2_witness_common_leftfirst)) * bc) + (pfrep_left_associative_2_witness_common_left)))))) \/ (((exists pfrep_gap_associative_2_witness_common_leftfirstoutside. pfrep_gap_associative_2_witness_common_leftfirstoutside+(Lb)=(pfrep_power_associative_2_witness_common_left)) /\ (((pfrep_left_associative_2_witness_common_left)=0))))) -> ((exists pfrep_position_associative_2_witness_common_leftsecond. ((pfrep_position_associative_2_witness_common_leftsecond+S (pfrep_power_associative_2_witness_common_left)=(pfaa_length_associative_2)) /\ ((((exists ff_h_pfp_associative_2_witness_common_leftsecondentry. ff_h_pfp_associative_2_witness_common_leftsecondentry + S (pfrep_right_associative_2_witness_common_left) = S ((S (pfrep_position_associative_2_witness_common_leftsecond)) * pfaa_left_c_associative_2)) /\ exists ff_q_pfp_associative_2_witness_common_leftsecondentry. pfaa_left_b_associative_2 = ff_q_pfp_associative_2_witness_common_leftsecondentry * S ((S (pfrep_position_associative_2_witness_common_leftsecond)) * pfaa_left_c_associative_2) + (pfrep_right_associative_2_witness_common_left)))))) \/ (((exists pfrep_gap_associative_2_witness_common_leftsecondoutside. pfrep_gap_associative_2_witness_common_leftsecondoutside+(pfaa_length_associative_2)=(pfrep_power_associative_2_witness_common_left)) /\ (((pfrep_right_associative_2_witness_common_left)=0))))) -> pfrep_left_associative_2_witness_common_left=pfrep_right_associative_2_witness_common_left) /\ ((forall pfrep_power_associative_2_witness_common_right pfrep_left_associative_2_witness_common_right pfrep_right_associative_2_witness_common_right. ((exists pfrep_position_associative_2_witness_common_rightfirst. ((pfrep_position_associative_2_witness_common_rightfirst+S (pfrep_power_associative_2_witness_common_right)=(Lc)) /\ ((((exists ff_h_pfp_associative_2_witness_common_rightfirstentry. ff_h_pfp_associative_2_witness_common_rightfirstentry + S (pfrep_left_associative_2_witness_common_right) = S ((S (pfrep_position_associative_2_witness_common_rightfirst)) * cc)) /\ exists ff_q_pfp_associative_2_witness_common_rightfirstentry. cb = ff_q_pfp_associative_2_witness_common_rightfirstentry * S ((S (pfrep_position_associative_2_witness_common_rightfirst)) * cc) + (pfrep_left_associative_2_witness_common_right)))))) \/ (((exists pfrep_gap_associative_2_witness_common_rightfirstoutside. pfrep_gap_associative_2_witness_common_rightfirstoutside+(Lc)=(pfrep_power_associative_2_witness_common_right)) /\ (((pfrep_left_associative_2_witness_common_right)=0))))) -> ((exists pfrep_position_associative_2_witness_common_rightsecond. ((pfrep_position_associative_2_witness_common_rightsecond+S (pfrep_power_associative_2_witness_common_right)=(pfaa_length_associative_2)) /\ ((((exists ff_h_pfp_associative_2_witness_common_rightsecondentry. ff_h_pfp_associative_2_witness_common_rightsecondentry + S (pfrep_right_associative_2_witness_common_right) = S ((S (pfrep_position_associative_2_witness_common_rightsecond)) * pfaa_right_c_associative_2)) /\ exists ff_q_pfp_associative_2_witness_common_rightsecondentry. pfaa_right_b_associative_2 = ff_q_pfp_associative_2_witness_common_rightsecondentry * S ((S (pfrep_position_associative_2_witness_common_rightsecond)) * pfaa_right_c_associative_2) + (pfrep_right_associative_2_witness_common_right)))))) \/ (((exists pfrep_gap_associative_2_witness_common_rightsecondoutside. pfrep_gap_associative_2_witness_common_rightsecondoutside+(pfaa_length_associative_2)=(pfrep_power_associative_2_witness_common_right)) /\ (((pfrep_right_associative_2_witness_common_right)=0))))) -> pfrep_left_associative_2_witness_common_right=pfrep_right_associative_2_witness_common_right)))) /\ (((forall pfp_index_associative_2_witness_operation. (exists pfa_gap_associative_2_witness_operationindex. pfa_gap_associative_2_witness_operationindex + S (pfp_index_associative_2_witness_operation) = (pfaa_length_associative_2)) -> exists pfp_left_associative_2_witness_operation pfp_right_associative_2_witness_operation pfp_value_associative_2_witness_operation. ((((exists ff_h_pfp_associative_2_witness_operationleft. ff_h_pfp_associative_2_witness_operationleft + S (pfp_left_associative_2_witness_operation) = S ((S (pfp_index_associative_2_witness_operation)) * pfaa_left_c_associative_2)) /\ exists ff_q_pfp_associative_2_witness_operationleft. pfaa_left_b_associative_2 = ff_q_pfp_associative_2_witness_operationleft * S ((S (pfp_index_associative_2_witness_operation)) * pfaa_left_c_associative_2) + (pfp_left_associative_2_witness_operation))) /\ (((((exists ff_h_pfp_associative_2_witness_operationright. ff_h_pfp_associative_2_witness_operationright + S (pfp_right_associative_2_witness_operation) = S ((S (pfp_index_associative_2_witness_operation)) * pfaa_right_c_associative_2)) /\ exists ff_q_pfp_associative_2_witness_operationright. pfaa_right_b_associative_2 = ff_q_pfp_associative_2_witness_operationright * S ((S (pfp_index_associative_2_witness_operation)) * pfaa_right_c_associative_2) + (pfp_right_associative_2_witness_operation))) /\ (((((exists ff_h_pfp_associative_2_witness_operationtarget. ff_h_pfp_associative_2_witness_operationtarget + S (pfp_value_associative_2_witness_operation) = S ((S (pfp_index_associative_2_witness_operation)) * pfaa_sum_c_associative_2)) /\ exists ff_q_pfp_associative_2_witness_operationtarget. pfaa_sum_b_associative_2 = ff_q_pfp_associative_2_witness_operationtarget * S ((S (pfp_index_associative_2_witness_operation)) * pfaa_sum_c_associative_2) + (pfp_value_associative_2_witness_operation))) /\ ((((exists pfa_gap_associative_2_witness_operationoperationleft. pfa_gap_associative_2_witness_operationoperationleft + S (pfp_left_associative_2_witness_operation) = (p)) /\ (((exists pfa_gap_associative_2_witness_operationoperationright. pfa_gap_associative_2_witness_operationoperationright + S (pfp_right_associative_2_witness_operation) = (p)) /\ ((((exists pfa_gap_associative_2_witness_operationoperationresultbound. pfa_gap_associative_2_witness_operationoperationresultbound + S (pfp_value_associative_2_witness_operation) = (p)) /\ ((exists pfa_offset_left_associative_2_witness_operationoperationresultcongruence pfa_offset_right_associative_2_witness_operationoperationresultcongruence. ((pfp_left_associative_2_witness_operation) + (pfp_right_associative_2_witness_operation)) + (p) * pfa_offset_left_associative_2_witness_operationoperationresultcongruence = (pfp_value_associative_2_witness_operation) + (p) * pfa_offset_right_associative_2_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_associative_2_witness_output pfrep_left_associative_2_witness_output pfrep_right_associative_2_witness_output. ((exists pfrep_position_associative_2_witness_outputfirst. ((pfrep_position_associative_2_witness_outputfirst+S (pfrep_power_associative_2_witness_output)=(pfaa_length_associative_2)) /\ ((((exists ff_h_pfp_associative_2_witness_outputfirstentry. ff_h_pfp_associative_2_witness_outputfirstentry + S (pfrep_left_associative_2_witness_output) = S ((S (pfrep_position_associative_2_witness_outputfirst)) * pfaa_sum_c_associative_2)) /\ exists ff_q_pfp_associative_2_witness_outputfirstentry. pfaa_sum_b_associative_2 = ff_q_pfp_associative_2_witness_outputfirstentry * S ((S (pfrep_position_associative_2_witness_outputfirst)) * pfaa_sum_c_associative_2) + (pfrep_left_associative_2_witness_output)))))) \/ (((exists pfrep_gap_associative_2_witness_outputfirstoutside. pfrep_gap_associative_2_witness_outputfirstoutside+(pfaa_length_associative_2)=(pfrep_power_associative_2_witness_output)) /\ (((pfrep_left_associative_2_witness_output)=0))))) -> ((exists pfrep_position_associative_2_witness_outputsecond. ((pfrep_position_associative_2_witness_outputsecond+S (pfrep_power_associative_2_witness_output)=(Lv)) /\ ((((exists ff_h_pfp_associative_2_witness_outputsecondentry. ff_h_pfp_associative_2_witness_outputsecondentry + S (pfrep_right_associative_2_witness_output) = S ((S (pfrep_position_associative_2_witness_outputsecond)) * vc)) /\ exists ff_q_pfp_associative_2_witness_outputsecondentry. vb = ff_q_pfp_associative_2_witness_outputsecondentry * S ((S (pfrep_position_associative_2_witness_outputsecond)) * vc) + (pfrep_right_associative_2_witness_output)))))) \/ (((exists pfrep_gap_associative_2_witness_outputsecondoutside. pfrep_gap_associative_2_witness_outputsecondoutside+(Lv)=(pfrep_power_associative_2_witness_output)) /\ (((pfrep_right_associative_2_witness_output)=0))))) -> pfrep_left_associative_2_witness_output=pfrep_right_associative_2_witness_output))))))))))))) -> (((forall fom_index_pfp_associative_3_left_bounded. (exists fom_gap_pfp_associative_3_left_bounded_index_bound. fom_gap_pfp_associative_3_left_bounded_index_bound + S (fom_index_pfp_associative_3_left_bounded) = La) -> exists fom_value_pfp_associative_3_left_bounded. ((((exists fom_beta_height_pfp_associative_3_left_bounded_entry. fom_beta_height_pfp_associative_3_left_bounded_entry + S (fom_value_pfp_associative_3_left_bounded) = S ((S (fom_index_pfp_associative_3_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_associative_3_left_bounded_entry. ab = fom_beta_quotient_pfp_associative_3_left_bounded_entry * S ((S (fom_index_pfp_associative_3_left_bounded)) * ac) + (fom_value_pfp_associative_3_left_bounded))) /\ (exists fom_gap_pfp_associative_3_left_bounded_value_bound. fom_gap_pfp_associative_3_left_bounded_value_bound + S (fom_value_pfp_associative_3_left_bounded) = p))) /\ (((forall fom_index_pfp_associative_3_right_bounded. (exists fom_gap_pfp_associative_3_right_bounded_index_bound. fom_gap_pfp_associative_3_right_bounded_index_bound + S (fom_index_pfp_associative_3_right_bounded) = Lv) -> exists fom_value_pfp_associative_3_right_bounded. ((((exists fom_beta_height_pfp_associative_3_right_bounded_entry. fom_beta_height_pfp_associative_3_right_bounded_entry + S (fom_value_pfp_associative_3_right_bounded) = S ((S (fom_index_pfp_associative_3_right_bounded)) * vc)) /\ exists fom_beta_quotient_pfp_associative_3_right_bounded_entry. vb = fom_beta_quotient_pfp_associative_3_right_bounded_entry * S ((S (fom_index_pfp_associative_3_right_bounded)) * vc) + (fom_value_pfp_associative_3_right_bounded))) /\ (exists fom_gap_pfp_associative_3_right_bounded_value_bound. fom_gap_pfp_associative_3_right_bounded_value_bound + S (fom_value_pfp_associative_3_right_bounded) = p))) /\ (((forall fom_index_pfp_associative_3_result_bounded. (exists fom_gap_pfp_associative_3_result_bounded_index_bound. fom_gap_pfp_associative_3_result_bounded_index_bound + S (fom_index_pfp_associative_3_result_bounded) = Ls) -> exists fom_value_pfp_associative_3_result_bounded. ((((exists fom_beta_height_pfp_associative_3_result_bounded_entry. fom_beta_height_pfp_associative_3_result_bounded_entry + S (fom_value_pfp_associative_3_result_bounded) = S ((S (fom_index_pfp_associative_3_result_bounded)) * sc)) /\ exists fom_beta_quotient_pfp_associative_3_result_bounded_entry. sb = fom_beta_quotient_pfp_associative_3_result_bounded_entry * S ((S (fom_index_pfp_associative_3_result_bounded)) * sc) + (fom_value_pfp_associative_3_result_bounded))) /\ (exists fom_gap_pfp_associative_3_result_bounded_value_bound. fom_gap_pfp_associative_3_result_bounded_value_bound + S (fom_value_pfp_associative_3_result_bounded) = p))) /\ ((exists pfaa_left_b_associative_3 pfaa_left_c_associative_3 pfaa_right_b_associative_3 pfaa_right_c_associative_3 pfaa_sum_b_associative_3 pfaa_sum_c_associative_3 pfaa_length_associative_3. ((((forall pfrep_power_associative_3_witness_common_left pfrep_left_associative_3_witness_common_left pfrep_right_associative_3_witness_common_left. ((exists pfrep_position_associative_3_witness_common_leftfirst. ((pfrep_position_associative_3_witness_common_leftfirst+S (pfrep_power_associative_3_witness_common_left)=(La)) /\ ((((exists ff_h_pfp_associative_3_witness_common_leftfirstentry. ff_h_pfp_associative_3_witness_common_leftfirstentry + S (pfrep_left_associative_3_witness_common_left) = S ((S (pfrep_position_associative_3_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_associative_3_witness_common_leftfirstentry. ab = ff_q_pfp_associative_3_witness_common_leftfirstentry * S ((S (pfrep_position_associative_3_witness_common_leftfirst)) * ac) + (pfrep_left_associative_3_witness_common_left)))))) \/ (((exists pfrep_gap_associative_3_witness_common_leftfirstoutside. pfrep_gap_associative_3_witness_common_leftfirstoutside+(La)=(pfrep_power_associative_3_witness_common_left)) /\ (((pfrep_left_associative_3_witness_common_left)=0))))) -> ((exists pfrep_position_associative_3_witness_common_leftsecond. ((pfrep_position_associative_3_witness_common_leftsecond+S (pfrep_power_associative_3_witness_common_left)=(pfaa_length_associative_3)) /\ ((((exists ff_h_pfp_associative_3_witness_common_leftsecondentry. ff_h_pfp_associative_3_witness_common_leftsecondentry + S (pfrep_right_associative_3_witness_common_left) = S ((S (pfrep_position_associative_3_witness_common_leftsecond)) * pfaa_left_c_associative_3)) /\ exists ff_q_pfp_associative_3_witness_common_leftsecondentry. pfaa_left_b_associative_3 = ff_q_pfp_associative_3_witness_common_leftsecondentry * S ((S (pfrep_position_associative_3_witness_common_leftsecond)) * pfaa_left_c_associative_3) + (pfrep_right_associative_3_witness_common_left)))))) \/ (((exists pfrep_gap_associative_3_witness_common_leftsecondoutside. pfrep_gap_associative_3_witness_common_leftsecondoutside+(pfaa_length_associative_3)=(pfrep_power_associative_3_witness_common_left)) /\ (((pfrep_right_associative_3_witness_common_left)=0))))) -> pfrep_left_associative_3_witness_common_left=pfrep_right_associative_3_witness_common_left) /\ ((forall pfrep_power_associative_3_witness_common_right pfrep_left_associative_3_witness_common_right pfrep_right_associative_3_witness_common_right. ((exists pfrep_position_associative_3_witness_common_rightfirst. ((pfrep_position_associative_3_witness_common_rightfirst+S (pfrep_power_associative_3_witness_common_right)=(Lv)) /\ ((((exists ff_h_pfp_associative_3_witness_common_rightfirstentry. ff_h_pfp_associative_3_witness_common_rightfirstentry + S (pfrep_left_associative_3_witness_common_right) = S ((S (pfrep_position_associative_3_witness_common_rightfirst)) * vc)) /\ exists ff_q_pfp_associative_3_witness_common_rightfirstentry. vb = ff_q_pfp_associative_3_witness_common_rightfirstentry * S ((S (pfrep_position_associative_3_witness_common_rightfirst)) * vc) + (pfrep_left_associative_3_witness_common_right)))))) \/ (((exists pfrep_gap_associative_3_witness_common_rightfirstoutside. pfrep_gap_associative_3_witness_common_rightfirstoutside+(Lv)=(pfrep_power_associative_3_witness_common_right)) /\ (((pfrep_left_associative_3_witness_common_right)=0))))) -> ((exists pfrep_position_associative_3_witness_common_rightsecond. ((pfrep_position_associative_3_witness_common_rightsecond+S (pfrep_power_associative_3_witness_common_right)=(pfaa_length_associative_3)) /\ ((((exists ff_h_pfp_associative_3_witness_common_rightsecondentry. ff_h_pfp_associative_3_witness_common_rightsecondentry + S (pfrep_right_associative_3_witness_common_right) = S ((S (pfrep_position_associative_3_witness_common_rightsecond)) * pfaa_right_c_associative_3)) /\ exists ff_q_pfp_associative_3_witness_common_rightsecondentry. pfaa_right_b_associative_3 = ff_q_pfp_associative_3_witness_common_rightsecondentry * S ((S (pfrep_position_associative_3_witness_common_rightsecond)) * pfaa_right_c_associative_3) + (pfrep_right_associative_3_witness_common_right)))))) \/ (((exists pfrep_gap_associative_3_witness_common_rightsecondoutside. pfrep_gap_associative_3_witness_common_rightsecondoutside+(pfaa_length_associative_3)=(pfrep_power_associative_3_witness_common_right)) /\ (((pfrep_right_associative_3_witness_common_right)=0))))) -> pfrep_left_associative_3_witness_common_right=pfrep_right_associative_3_witness_common_right)))) /\ (((forall pfp_index_associative_3_witness_operation. (exists pfa_gap_associative_3_witness_operationindex. pfa_gap_associative_3_witness_operationindex + S (pfp_index_associative_3_witness_operation) = (pfaa_length_associative_3)) -> exists pfp_left_associative_3_witness_operation pfp_right_associative_3_witness_operation pfp_value_associative_3_witness_operation. ((((exists ff_h_pfp_associative_3_witness_operationleft. ff_h_pfp_associative_3_witness_operationleft + S (pfp_left_associative_3_witness_operation) = S ((S (pfp_index_associative_3_witness_operation)) * pfaa_left_c_associative_3)) /\ exists ff_q_pfp_associative_3_witness_operationleft. pfaa_left_b_associative_3 = ff_q_pfp_associative_3_witness_operationleft * S ((S (pfp_index_associative_3_witness_operation)) * pfaa_left_c_associative_3) + (pfp_left_associative_3_witness_operation))) /\ (((((exists ff_h_pfp_associative_3_witness_operationright. ff_h_pfp_associative_3_witness_operationright + S (pfp_right_associative_3_witness_operation) = S ((S (pfp_index_associative_3_witness_operation)) * pfaa_right_c_associative_3)) /\ exists ff_q_pfp_associative_3_witness_operationright. pfaa_right_b_associative_3 = ff_q_pfp_associative_3_witness_operationright * S ((S (pfp_index_associative_3_witness_operation)) * pfaa_right_c_associative_3) + (pfp_right_associative_3_witness_operation))) /\ (((((exists ff_h_pfp_associative_3_witness_operationtarget. ff_h_pfp_associative_3_witness_operationtarget + S (pfp_value_associative_3_witness_operation) = S ((S (pfp_index_associative_3_witness_operation)) * pfaa_sum_c_associative_3)) /\ exists ff_q_pfp_associative_3_witness_operationtarget. pfaa_sum_b_associative_3 = ff_q_pfp_associative_3_witness_operationtarget * S ((S (pfp_index_associative_3_witness_operation)) * pfaa_sum_c_associative_3) + (pfp_value_associative_3_witness_operation))) /\ ((((exists pfa_gap_associative_3_witness_operationoperationleft. pfa_gap_associative_3_witness_operationoperationleft + S (pfp_left_associative_3_witness_operation) = (p)) /\ (((exists pfa_gap_associative_3_witness_operationoperationright. pfa_gap_associative_3_witness_operationoperationright + S (pfp_right_associative_3_witness_operation) = (p)) /\ ((((exists pfa_gap_associative_3_witness_operationoperationresultbound. pfa_gap_associative_3_witness_operationoperationresultbound + S (pfp_value_associative_3_witness_operation) = (p)) /\ ((exists pfa_offset_left_associative_3_witness_operationoperationresultcongruence pfa_offset_right_associative_3_witness_operationoperationresultcongruence. ((pfp_left_associative_3_witness_operation) + (pfp_right_associative_3_witness_operation)) + (p) * pfa_offset_left_associative_3_witness_operationoperationresultcongruence = (pfp_value_associative_3_witness_operation) + (p) * pfa_offset_right_associative_3_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_associative_3_witness_output pfrep_left_associative_3_witness_output pfrep_right_associative_3_witness_output. ((exists pfrep_position_associative_3_witness_outputfirst. ((pfrep_position_associative_3_witness_outputfirst+S (pfrep_power_associative_3_witness_output)=(pfaa_length_associative_3)) /\ ((((exists ff_h_pfp_associative_3_witness_outputfirstentry. ff_h_pfp_associative_3_witness_outputfirstentry + S (pfrep_left_associative_3_witness_output) = S ((S (pfrep_position_associative_3_witness_outputfirst)) * pfaa_sum_c_associative_3)) /\ exists ff_q_pfp_associative_3_witness_outputfirstentry. pfaa_sum_b_associative_3 = ff_q_pfp_associative_3_witness_outputfirstentry * S ((S (pfrep_position_associative_3_witness_outputfirst)) * pfaa_sum_c_associative_3) + (pfrep_left_associative_3_witness_output)))))) \/ (((exists pfrep_gap_associative_3_witness_outputfirstoutside. pfrep_gap_associative_3_witness_outputfirstoutside+(pfaa_length_associative_3)=(pfrep_power_associative_3_witness_output)) /\ (((pfrep_left_associative_3_witness_output)=0))))) -> ((exists pfrep_position_associative_3_witness_outputsecond. ((pfrep_position_associative_3_witness_outputsecond+S (pfrep_power_associative_3_witness_output)=(Ls)) /\ ((((exists ff_h_pfp_associative_3_witness_outputsecondentry. ff_h_pfp_associative_3_witness_outputsecondentry + S (pfrep_right_associative_3_witness_output) = S ((S (pfrep_position_associative_3_witness_outputsecond)) * sc)) /\ exists ff_q_pfp_associative_3_witness_outputsecondentry. sb = ff_q_pfp_associative_3_witness_outputsecondentry * S ((S (pfrep_position_associative_3_witness_outputsecond)) * sc) + (pfrep_right_associative_3_witness_output)))))) \/ (((exists pfrep_gap_associative_3_witness_outputsecondoutside. pfrep_gap_associative_3_witness_outputsecondoutside+(Ls)=(pfrep_power_associative_3_witness_output)) /\ (((pfrep_right_associative_3_witness_output)=0))))) -> pfrep_left_associative_3_witness_output=pfrep_right_associative_3_witness_output))))))))))))) -> (forall pfrep_power_associative_result pfrep_left_associative_result pfrep_right_associative_result. ((exists pfrep_position_associative_resultfirst. ((pfrep_position_associative_resultfirst+S (pfrep_power_associative_result)=(Lr)) /\ ((((exists ff_h_pfp_associative_resultfirstentry. ff_h_pfp_associative_resultfirstentry + S (pfrep_left_associative_result) = S ((S (pfrep_position_associative_resultfirst)) * rc)) /\ exists ff_q_pfp_associative_resultfirstentry. rb = ff_q_pfp_associative_resultfirstentry * S ((S (pfrep_position_associative_resultfirst)) * rc) + (pfrep_left_associative_result)))))) \/ (((exists pfrep_gap_associative_resultfirstoutside. pfrep_gap_associative_resultfirstoutside+(Lr)=(pfrep_power_associative_result)) /\ (((pfrep_left_associative_result)=0))))) -> ((exists pfrep_position_associative_resultsecond. ((pfrep_position_associative_resultsecond+S (pfrep_power_associative_result)=(Ls)) /\ ((((exists ff_h_pfp_associative_resultsecondentry. ff_h_pfp_associative_resultsecondentry + S (pfrep_right_associative_result) = S ((S (pfrep_position_associative_resultsecond)) * sc)) /\ exists ff_q_pfp_associative_resultsecondentry. sb = ff_q_pfp_associative_resultsecondentry * S ((S (pfrep_position_associative_resultsecond)) * sc) + (pfrep_right_associative_result)))))) \/ (((exists pfrep_gap_associative_resultsecondoutside. pfrep_gap_associative_resultsecondoutside+(Ls)=(pfrep_power_associative_result)) /\ (((pfrep_right_associative_result)=0))))) -> pfrep_left_associative_result=pfrep_right_associative_result)