prime_field_polynomial_euclidean_backward_coefficient_identity

forall p ab ac La bb bc Lb rb rc Lr qb qc Lq pb pc Lp ub uc Lu vb vc Lv gb gc Lg cb cc Lc db dc Ld wb wc Lw tb tc Lt xb xc Lx yb yc Ly zb zc Lz hb hc Lh. (~((p) = 1) /\ forall pfa_factor_left_backward_prime pfa_factor_right_backward_prime. (p) = pfa_factor_left_backward_prime * pfa_factor_right_backward_prime -> pfa_factor_left_backward_prime = 1 \/ pfa_factor_right_backward_prime = 1) -> (((forall fom_index_pfp_backward_division_productleft. (exists fom_gap_pfp_backward_division_productleft_index_bound. fom_gap_pfp_backward_division_productleft_index_bound + S (fom_index_pfp_backward_division_productleft) = Lq) -> exists fom_value_pfp_backward_division_productleft. ((((exists fom_beta_height_pfp_backward_division_productleft_entry. fom_beta_height_pfp_backward_division_productleft_entry + S (fom_value_pfp_backward_division_productleft) = S ((S (fom_index_pfp_backward_division_productleft)) * qc)) /\ exists fom_beta_quotient_pfp_backward_division_productleft_entry. qb = fom_beta_quotient_pfp_backward_division_productleft_entry * S ((S (fom_index_pfp_backward_division_productleft)) * qc) + (fom_value_pfp_backward_division_productleft))) /\ (exists fom_gap_pfp_backward_division_productleft_value_bound. fom_gap_pfp_backward_division_productleft_value_bound + S (fom_value_pfp_backward_division_productleft) = p))) /\ (((forall fom_index_pfp_backward_division_productright. (exists fom_gap_pfp_backward_division_productright_index_bound. fom_gap_pfp_backward_division_productright_index_bound + S (fom_index_pfp_backward_division_productright) = Lb) -> exists fom_value_pfp_backward_division_productright. ((((exists fom_beta_height_pfp_backward_division_productright_entry. fom_beta_height_pfp_backward_division_productright_entry + S (fom_value_pfp_backward_division_productright) = S ((S (fom_index_pfp_backward_division_productright)) * bc)) /\ exists fom_beta_quotient_pfp_backward_division_productright_entry. bb = fom_beta_quotient_pfp_backward_division_productright_entry * S ((S (fom_index_pfp_backward_division_productright)) * bc) + (fom_value_pfp_backward_division_productright))) /\ (exists fom_gap_pfp_backward_division_productright_value_bound. fom_gap_pfp_backward_division_productright_value_bound + S (fom_value_pfp_backward_division_productright) = p))) /\ (((((((Lq)=0 \/ (Lb)=0) /\ (((Lp)=0)))) \/ (((~((Lq)=0)) /\ (((~((Lb)=0)) /\ (((Lq)+(Lb)=S (Lp)))))))) /\ ((forall pfc_index_backward_division_productcoefficients. (exists pfa_gap_backward_division_productcoefficientsbound. pfa_gap_backward_division_productcoefficientsbound + S (pfc_index_backward_division_productcoefficients) = (Lp)) -> exists pfc_value_backward_division_productcoefficients. ((((exists ff_h_pfp_backward_division_productcoefficientsentry. ff_h_pfp_backward_division_productcoefficientsentry + S (pfc_value_backward_division_productcoefficients) = S ((S (pfc_index_backward_division_productcoefficients)) * pc)) /\ exists ff_q_pfp_backward_division_productcoefficientsentry. pb = ff_q_pfp_backward_division_productcoefficientsentry * S ((S (pfc_index_backward_division_productcoefficients)) * pc) + (pfc_value_backward_division_productcoefficients))) /\ ((exists pfc_terms_code_backward_division_productcoefficientscoefficient pfc_terms_scale_backward_division_productcoefficientscoefficient pfc_natural_sum_backward_division_productcoefficientscoefficient. ((forall pfc_index_backward_division_productcoefficientscoefficientdiagonal. (exists pfa_gap_backward_division_productcoefficientscoefficientdiagonalbound. pfa_gap_backward_division_productcoefficientscoefficientdiagonalbound + S (pfc_index_backward_division_productcoefficientscoefficientdiagonal) = (S (pfc_index_backward_division_productcoefficients))) -> exists pfc_value_backward_division_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_backward_division_productcoefficientscoefficientdiagonalentry. ff_h_pfp_backward_division_productcoefficientscoefficientdiagonalentry + S (pfc_value_backward_division_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_backward_division_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_division_productcoefficientscoefficient)) /\ exists ff_q_pfp_backward_division_productcoefficientscoefficientdiagonalentry. pfc_terms_code_backward_division_productcoefficientscoefficient = ff_q_pfp_backward_division_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_backward_division_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_division_productcoefficientscoefficient) + (pfc_value_backward_division_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_backward_division_productcoefficientscoefficientdiagonalterm pfc_left_backward_division_productcoefficientscoefficientdiagonalterm pfc_right_backward_division_productcoefficientscoefficientdiagonalterm. (((pfc_index_backward_division_productcoefficientscoefficientdiagonal)+pfc_complement_backward_division_productcoefficientscoefficientdiagonalterm=(pfc_index_backward_division_productcoefficients)) /\ ((((((exists pfa_gap_backward_division_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_backward_division_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_backward_division_productcoefficientscoefficientdiagonal) = (Lq)) /\ ((((exists ff_h_pfp_backward_division_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_backward_division_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_backward_division_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_backward_division_productcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_backward_division_productcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_backward_division_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_backward_division_productcoefficientscoefficientdiagonal)) * qc) + (pfc_left_backward_division_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_division_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_backward_division_productcoefficientscoefficientdiagonaltermleftoutside+(Lq)=(pfc_index_backward_division_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_backward_division_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_backward_division_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_backward_division_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_backward_division_productcoefficientscoefficientdiagonalterm) = (Lb)) /\ ((((exists ff_h_pfp_backward_division_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_backward_division_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_backward_division_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_backward_division_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_backward_division_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_backward_division_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_backward_division_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_backward_division_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_division_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_backward_division_productcoefficientscoefficientdiagonaltermrightoutside+(Lb)=(pfc_complement_backward_division_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_backward_division_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_backward_division_productcoefficientscoefficientdiagonal)=pfc_left_backward_division_productcoefficientscoefficientdiagonalterm*pfc_right_backward_division_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_backward_division_productcoefficientscoefficientsum fs_v_pfc_backward_division_productcoefficientscoefficientsum. ((((exists fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_start. fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_backward_division_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_start. fs_u_pfc_backward_division_productcoefficientscoefficientsum = fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_backward_division_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_backward_division_productcoefficientscoefficient) = S ((S (S (pfc_index_backward_division_productcoefficients))) * fs_v_pfc_backward_division_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_backward_division_productcoefficientscoefficientsum = fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_backward_division_productcoefficients))) * fs_v_pfc_backward_division_productcoefficientscoefficientsum) + (pfc_natural_sum_backward_division_productcoefficientscoefficient))) /\ forall fs_i_pfc_backward_division_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_backward_division_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_backward_division_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_backward_division_productcoefficientscoefficientsum_body_steps = S (pfc_index_backward_division_productcoefficients)) -> exists fs_a_pfc_backward_division_productcoefficientscoefficientsum_body_steps fs_r_pfc_backward_division_productcoefficientscoefficientsum_body_steps fs_s_pfc_backward_division_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_backward_division_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_division_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_division_productcoefficientscoefficient)) /\ exists fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_backward_division_productcoefficientscoefficient = fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_backward_division_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_division_productcoefficientscoefficient) + (fs_a_pfc_backward_division_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_backward_division_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_division_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_division_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_backward_division_productcoefficientscoefficientsum = fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_backward_division_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_division_productcoefficientscoefficientsum) + (fs_r_pfc_backward_division_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_backward_division_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_backward_division_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_backward_division_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_division_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_backward_division_productcoefficientscoefficientsum = fs_q_pfc_backward_division_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_backward_division_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_division_productcoefficientscoefficientsum) + (fs_s_pfc_backward_division_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_backward_division_productcoefficientscoefficientsum_body_steps = fs_r_pfc_backward_division_productcoefficientscoefficientsum_body_steps + fs_a_pfc_backward_division_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_backward_division_productcoefficientscoefficientresiduebound. pfa_gap_backward_division_productcoefficientscoefficientresiduebound + S (pfc_value_backward_division_productcoefficients) = (p)) /\ ((exists pfa_offset_left_backward_division_productcoefficientscoefficientresiduecongruence pfa_offset_right_backward_division_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_backward_division_productcoefficientscoefficient) + (p) * pfa_offset_left_backward_division_productcoefficientscoefficientresiduecongruence = (pfc_value_backward_division_productcoefficients) + (p) * pfa_offset_right_backward_division_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_backward_division_sum_left_bounded. (exists fom_gap_pfp_backward_division_sum_left_bounded_index_bound. fom_gap_pfp_backward_division_sum_left_bounded_index_bound + S (fom_index_pfp_backward_division_sum_left_bounded) = Lp) -> exists fom_value_pfp_backward_division_sum_left_bounded. ((((exists fom_beta_height_pfp_backward_division_sum_left_bounded_entry. fom_beta_height_pfp_backward_division_sum_left_bounded_entry + S (fom_value_pfp_backward_division_sum_left_bounded) = S ((S (fom_index_pfp_backward_division_sum_left_bounded)) * pc)) /\ exists fom_beta_quotient_pfp_backward_division_sum_left_bounded_entry. pb = fom_beta_quotient_pfp_backward_division_sum_left_bounded_entry * S ((S (fom_index_pfp_backward_division_sum_left_bounded)) * pc) + (fom_value_pfp_backward_division_sum_left_bounded))) /\ (exists fom_gap_pfp_backward_division_sum_left_bounded_value_bound. fom_gap_pfp_backward_division_sum_left_bounded_value_bound + S (fom_value_pfp_backward_division_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_backward_division_sum_right_bounded. (exists fom_gap_pfp_backward_division_sum_right_bounded_index_bound. fom_gap_pfp_backward_division_sum_right_bounded_index_bound + S (fom_index_pfp_backward_division_sum_right_bounded) = Lr) -> exists fom_value_pfp_backward_division_sum_right_bounded. ((((exists fom_beta_height_pfp_backward_division_sum_right_bounded_entry. fom_beta_height_pfp_backward_division_sum_right_bounded_entry + S (fom_value_pfp_backward_division_sum_right_bounded) = S ((S (fom_index_pfp_backward_division_sum_right_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_backward_division_sum_right_bounded_entry. rb = fom_beta_quotient_pfp_backward_division_sum_right_bounded_entry * S ((S (fom_index_pfp_backward_division_sum_right_bounded)) * rc) + (fom_value_pfp_backward_division_sum_right_bounded))) /\ (exists fom_gap_pfp_backward_division_sum_right_bounded_value_bound. fom_gap_pfp_backward_division_sum_right_bounded_value_bound + S (fom_value_pfp_backward_division_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_backward_division_sum_result_bounded. (exists fom_gap_pfp_backward_division_sum_result_bounded_index_bound. fom_gap_pfp_backward_division_sum_result_bounded_index_bound + S (fom_index_pfp_backward_division_sum_result_bounded) = La) -> exists fom_value_pfp_backward_division_sum_result_bounded. ((((exists fom_beta_height_pfp_backward_division_sum_result_bounded_entry. fom_beta_height_pfp_backward_division_sum_result_bounded_entry + S (fom_value_pfp_backward_division_sum_result_bounded) = S ((S (fom_index_pfp_backward_division_sum_result_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_backward_division_sum_result_bounded_entry. ab = fom_beta_quotient_pfp_backward_division_sum_result_bounded_entry * S ((S (fom_index_pfp_backward_division_sum_result_bounded)) * ac) + (fom_value_pfp_backward_division_sum_result_bounded))) /\ (exists fom_gap_pfp_backward_division_sum_result_bounded_value_bound. fom_gap_pfp_backward_division_sum_result_bounded_value_bound + S (fom_value_pfp_backward_division_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_backward_division_sum pfaa_left_c_backward_division_sum pfaa_right_b_backward_division_sum pfaa_right_c_backward_division_sum pfaa_sum_b_backward_division_sum pfaa_sum_c_backward_division_sum pfaa_length_backward_division_sum. ((((forall pfrep_power_backward_division_sum_witness_common_left pfrep_left_backward_division_sum_witness_common_left pfrep_right_backward_division_sum_witness_common_left. ((exists pfrep_position_backward_division_sum_witness_common_leftfirst. ((pfrep_position_backward_division_sum_witness_common_leftfirst+S (pfrep_power_backward_division_sum_witness_common_left)=(Lp)) /\ ((((exists ff_h_pfp_backward_division_sum_witness_common_leftfirstentry. ff_h_pfp_backward_division_sum_witness_common_leftfirstentry + S (pfrep_left_backward_division_sum_witness_common_left) = S ((S (pfrep_position_backward_division_sum_witness_common_leftfirst)) * pc)) /\ exists ff_q_pfp_backward_division_sum_witness_common_leftfirstentry. pb = ff_q_pfp_backward_division_sum_witness_common_leftfirstentry * S ((S (pfrep_position_backward_division_sum_witness_common_leftfirst)) * pc) + (pfrep_left_backward_division_sum_witness_common_left)))))) \/ (((exists pfrep_gap_backward_division_sum_witness_common_leftfirstoutside. pfrep_gap_backward_division_sum_witness_common_leftfirstoutside+(Lp)=(pfrep_power_backward_division_sum_witness_common_left)) /\ (((pfrep_left_backward_division_sum_witness_common_left)=0))))) -> ((exists pfrep_position_backward_division_sum_witness_common_leftsecond. ((pfrep_position_backward_division_sum_witness_common_leftsecond+S (pfrep_power_backward_division_sum_witness_common_left)=(pfaa_length_backward_division_sum)) /\ ((((exists ff_h_pfp_backward_division_sum_witness_common_leftsecondentry. ff_h_pfp_backward_division_sum_witness_common_leftsecondentry + S (pfrep_right_backward_division_sum_witness_common_left) = S ((S (pfrep_position_backward_division_sum_witness_common_leftsecond)) * pfaa_left_c_backward_division_sum)) /\ exists ff_q_pfp_backward_division_sum_witness_common_leftsecondentry. pfaa_left_b_backward_division_sum = ff_q_pfp_backward_division_sum_witness_common_leftsecondentry * S ((S (pfrep_position_backward_division_sum_witness_common_leftsecond)) * pfaa_left_c_backward_division_sum) + (pfrep_right_backward_division_sum_witness_common_left)))))) \/ (((exists pfrep_gap_backward_division_sum_witness_common_leftsecondoutside. pfrep_gap_backward_division_sum_witness_common_leftsecondoutside+(pfaa_length_backward_division_sum)=(pfrep_power_backward_division_sum_witness_common_left)) /\ (((pfrep_right_backward_division_sum_witness_common_left)=0))))) -> pfrep_left_backward_division_sum_witness_common_left=pfrep_right_backward_division_sum_witness_common_left) /\ ((forall pfrep_power_backward_division_sum_witness_common_right pfrep_left_backward_division_sum_witness_common_right pfrep_right_backward_division_sum_witness_common_right. ((exists pfrep_position_backward_division_sum_witness_common_rightfirst. ((pfrep_position_backward_division_sum_witness_common_rightfirst+S (pfrep_power_backward_division_sum_witness_common_right)=(Lr)) /\ ((((exists ff_h_pfp_backward_division_sum_witness_common_rightfirstentry. ff_h_pfp_backward_division_sum_witness_common_rightfirstentry + S (pfrep_left_backward_division_sum_witness_common_right) = S ((S (pfrep_position_backward_division_sum_witness_common_rightfirst)) * rc)) /\ exists ff_q_pfp_backward_division_sum_witness_common_rightfirstentry. rb = ff_q_pfp_backward_division_sum_witness_common_rightfirstentry * S ((S (pfrep_position_backward_division_sum_witness_common_rightfirst)) * rc) + (pfrep_left_backward_division_sum_witness_common_right)))))) \/ (((exists pfrep_gap_backward_division_sum_witness_common_rightfirstoutside. pfrep_gap_backward_division_sum_witness_common_rightfirstoutside+(Lr)=(pfrep_power_backward_division_sum_witness_common_right)) /\ (((pfrep_left_backward_division_sum_witness_common_right)=0))))) -> ((exists pfrep_position_backward_division_sum_witness_common_rightsecond. ((pfrep_position_backward_division_sum_witness_common_rightsecond+S (pfrep_power_backward_division_sum_witness_common_right)=(pfaa_length_backward_division_sum)) /\ ((((exists ff_h_pfp_backward_division_sum_witness_common_rightsecondentry. ff_h_pfp_backward_division_sum_witness_common_rightsecondentry + S (pfrep_right_backward_division_sum_witness_common_right) = S ((S (pfrep_position_backward_division_sum_witness_common_rightsecond)) * pfaa_right_c_backward_division_sum)) /\ exists ff_q_pfp_backward_division_sum_witness_common_rightsecondentry. pfaa_right_b_backward_division_sum = ff_q_pfp_backward_division_sum_witness_common_rightsecondentry * S ((S (pfrep_position_backward_division_sum_witness_common_rightsecond)) * pfaa_right_c_backward_division_sum) + (pfrep_right_backward_division_sum_witness_common_right)))))) \/ (((exists pfrep_gap_backward_division_sum_witness_common_rightsecondoutside. pfrep_gap_backward_division_sum_witness_common_rightsecondoutside+(pfaa_length_backward_division_sum)=(pfrep_power_backward_division_sum_witness_common_right)) /\ (((pfrep_right_backward_division_sum_witness_common_right)=0))))) -> pfrep_left_backward_division_sum_witness_common_right=pfrep_right_backward_division_sum_witness_common_right)))) /\ (((forall pfp_index_backward_division_sum_witness_operation. (exists pfa_gap_backward_division_sum_witness_operationindex. pfa_gap_backward_division_sum_witness_operationindex + S (pfp_index_backward_division_sum_witness_operation) = (pfaa_length_backward_division_sum)) -> exists pfp_left_backward_division_sum_witness_operation pfp_right_backward_division_sum_witness_operation pfp_value_backward_division_sum_witness_operation. ((((exists ff_h_pfp_backward_division_sum_witness_operationleft. ff_h_pfp_backward_division_sum_witness_operationleft + S (pfp_left_backward_division_sum_witness_operation) = S ((S (pfp_index_backward_division_sum_witness_operation)) * pfaa_left_c_backward_division_sum)) /\ exists ff_q_pfp_backward_division_sum_witness_operationleft. pfaa_left_b_backward_division_sum = ff_q_pfp_backward_division_sum_witness_operationleft * S ((S (pfp_index_backward_division_sum_witness_operation)) * pfaa_left_c_backward_division_sum) + (pfp_left_backward_division_sum_witness_operation))) /\ (((((exists ff_h_pfp_backward_division_sum_witness_operationright. ff_h_pfp_backward_division_sum_witness_operationright + S (pfp_right_backward_division_sum_witness_operation) = S ((S (pfp_index_backward_division_sum_witness_operation)) * pfaa_right_c_backward_division_sum)) /\ exists ff_q_pfp_backward_division_sum_witness_operationright. pfaa_right_b_backward_division_sum = ff_q_pfp_backward_division_sum_witness_operationright * S ((S (pfp_index_backward_division_sum_witness_operation)) * pfaa_right_c_backward_division_sum) + (pfp_right_backward_division_sum_witness_operation))) /\ (((((exists ff_h_pfp_backward_division_sum_witness_operationtarget. ff_h_pfp_backward_division_sum_witness_operationtarget + S (pfp_value_backward_division_sum_witness_operation) = S ((S (pfp_index_backward_division_sum_witness_operation)) * pfaa_sum_c_backward_division_sum)) /\ exists ff_q_pfp_backward_division_sum_witness_operationtarget. pfaa_sum_b_backward_division_sum = ff_q_pfp_backward_division_sum_witness_operationtarget * S ((S (pfp_index_backward_division_sum_witness_operation)) * pfaa_sum_c_backward_division_sum) + (pfp_value_backward_division_sum_witness_operation))) /\ ((((exists pfa_gap_backward_division_sum_witness_operationoperationleft. pfa_gap_backward_division_sum_witness_operationoperationleft + S (pfp_left_backward_division_sum_witness_operation) = (p)) /\ (((exists pfa_gap_backward_division_sum_witness_operationoperationright. pfa_gap_backward_division_sum_witness_operationoperationright + S (pfp_right_backward_division_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_backward_division_sum_witness_operationoperationresultbound. pfa_gap_backward_division_sum_witness_operationoperationresultbound + S (pfp_value_backward_division_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_backward_division_sum_witness_operationoperationresultcongruence pfa_offset_right_backward_division_sum_witness_operationoperationresultcongruence. ((pfp_left_backward_division_sum_witness_operation) + (pfp_right_backward_division_sum_witness_operation)) + (p) * pfa_offset_left_backward_division_sum_witness_operationoperationresultcongruence = (pfp_value_backward_division_sum_witness_operation) + (p) * pfa_offset_right_backward_division_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_backward_division_sum_witness_output pfrep_left_backward_division_sum_witness_output pfrep_right_backward_division_sum_witness_output. ((exists pfrep_position_backward_division_sum_witness_outputfirst. ((pfrep_position_backward_division_sum_witness_outputfirst+S (pfrep_power_backward_division_sum_witness_output)=(pfaa_length_backward_division_sum)) /\ ((((exists ff_h_pfp_backward_division_sum_witness_outputfirstentry. ff_h_pfp_backward_division_sum_witness_outputfirstentry + S (pfrep_left_backward_division_sum_witness_output) = S ((S (pfrep_position_backward_division_sum_witness_outputfirst)) * pfaa_sum_c_backward_division_sum)) /\ exists ff_q_pfp_backward_division_sum_witness_outputfirstentry. pfaa_sum_b_backward_division_sum = ff_q_pfp_backward_division_sum_witness_outputfirstentry * S ((S (pfrep_position_backward_division_sum_witness_outputfirst)) * pfaa_sum_c_backward_division_sum) + (pfrep_left_backward_division_sum_witness_output)))))) \/ (((exists pfrep_gap_backward_division_sum_witness_outputfirstoutside. pfrep_gap_backward_division_sum_witness_outputfirstoutside+(pfaa_length_backward_division_sum)=(pfrep_power_backward_division_sum_witness_output)) /\ (((pfrep_left_backward_division_sum_witness_output)=0))))) -> ((exists pfrep_position_backward_division_sum_witness_outputsecond. ((pfrep_position_backward_division_sum_witness_outputsecond+S (pfrep_power_backward_division_sum_witness_output)=(La)) /\ ((((exists ff_h_pfp_backward_division_sum_witness_outputsecondentry. ff_h_pfp_backward_division_sum_witness_outputsecondentry + S (pfrep_right_backward_division_sum_witness_output) = S ((S (pfrep_position_backward_division_sum_witness_outputsecond)) * ac)) /\ exists ff_q_pfp_backward_division_sum_witness_outputsecondentry. ab = ff_q_pfp_backward_division_sum_witness_outputsecondentry * S ((S (pfrep_position_backward_division_sum_witness_outputsecond)) * ac) + (pfrep_right_backward_division_sum_witness_output)))))) \/ (((exists pfrep_gap_backward_division_sum_witness_outputsecondoutside. pfrep_gap_backward_division_sum_witness_outputsecondoutside+(La)=(pfrep_power_backward_division_sum_witness_output)) /\ (((pfrep_right_backward_division_sum_witness_output)=0))))) -> pfrep_left_backward_division_sum_witness_output=pfrep_right_backward_division_sum_witness_output))))))))))))) -> (((forall fom_index_pfp_backward_old_leftleft. (exists fom_gap_pfp_backward_old_leftleft_index_bound. fom_gap_pfp_backward_old_leftleft_index_bound + S (fom_index_pfp_backward_old_leftleft) = Lu) -> exists fom_value_pfp_backward_old_leftleft. ((((exists fom_beta_height_pfp_backward_old_leftleft_entry. fom_beta_height_pfp_backward_old_leftleft_entry + S (fom_value_pfp_backward_old_leftleft) = S ((S (fom_index_pfp_backward_old_leftleft)) * uc)) /\ exists fom_beta_quotient_pfp_backward_old_leftleft_entry. ub = fom_beta_quotient_pfp_backward_old_leftleft_entry * S ((S (fom_index_pfp_backward_old_leftleft)) * uc) + (fom_value_pfp_backward_old_leftleft))) /\ (exists fom_gap_pfp_backward_old_leftleft_value_bound. fom_gap_pfp_backward_old_leftleft_value_bound + S (fom_value_pfp_backward_old_leftleft) = p))) /\ (((forall fom_index_pfp_backward_old_leftright. (exists fom_gap_pfp_backward_old_leftright_index_bound. fom_gap_pfp_backward_old_leftright_index_bound + S (fom_index_pfp_backward_old_leftright) = Lb) -> exists fom_value_pfp_backward_old_leftright. ((((exists fom_beta_height_pfp_backward_old_leftright_entry. fom_beta_height_pfp_backward_old_leftright_entry + S (fom_value_pfp_backward_old_leftright) = S ((S (fom_index_pfp_backward_old_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_backward_old_leftright_entry. bb = fom_beta_quotient_pfp_backward_old_leftright_entry * S ((S (fom_index_pfp_backward_old_leftright)) * bc) + (fom_value_pfp_backward_old_leftright))) /\ (exists fom_gap_pfp_backward_old_leftright_value_bound. fom_gap_pfp_backward_old_leftright_value_bound + S (fom_value_pfp_backward_old_leftright) = p))) /\ (((((((Lu)=0 \/ (Lb)=0) /\ (((Lc)=0)))) \/ (((~((Lu)=0)) /\ (((~((Lb)=0)) /\ (((Lu)+(Lb)=S (Lc)))))))) /\ ((forall pfc_index_backward_old_leftcoefficients. (exists pfa_gap_backward_old_leftcoefficientsbound. pfa_gap_backward_old_leftcoefficientsbound + S (pfc_index_backward_old_leftcoefficients) = (Lc)) -> exists pfc_value_backward_old_leftcoefficients. ((((exists ff_h_pfp_backward_old_leftcoefficientsentry. ff_h_pfp_backward_old_leftcoefficientsentry + S (pfc_value_backward_old_leftcoefficients) = S ((S (pfc_index_backward_old_leftcoefficients)) * cc)) /\ exists ff_q_pfp_backward_old_leftcoefficientsentry. cb = ff_q_pfp_backward_old_leftcoefficientsentry * S ((S (pfc_index_backward_old_leftcoefficients)) * cc) + (pfc_value_backward_old_leftcoefficients))) /\ ((exists pfc_terms_code_backward_old_leftcoefficientscoefficient pfc_terms_scale_backward_old_leftcoefficientscoefficient pfc_natural_sum_backward_old_leftcoefficientscoefficient. ((forall pfc_index_backward_old_leftcoefficientscoefficientdiagonal. (exists pfa_gap_backward_old_leftcoefficientscoefficientdiagonalbound. pfa_gap_backward_old_leftcoefficientscoefficientdiagonalbound + S (pfc_index_backward_old_leftcoefficientscoefficientdiagonal) = (S (pfc_index_backward_old_leftcoefficients))) -> exists pfc_value_backward_old_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_backward_old_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_backward_old_leftcoefficientscoefficientdiagonalentry + S (pfc_value_backward_old_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_backward_old_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_old_leftcoefficientscoefficient)) /\ exists ff_q_pfp_backward_old_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_backward_old_leftcoefficientscoefficient = ff_q_pfp_backward_old_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_backward_old_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_old_leftcoefficientscoefficient) + (pfc_value_backward_old_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_backward_old_leftcoefficientscoefficientdiagonalterm pfc_left_backward_old_leftcoefficientscoefficientdiagonalterm pfc_right_backward_old_leftcoefficientscoefficientdiagonalterm. (((pfc_index_backward_old_leftcoefficientscoefficientdiagonal)+pfc_complement_backward_old_leftcoefficientscoefficientdiagonalterm=(pfc_index_backward_old_leftcoefficients)) /\ ((((((exists pfa_gap_backward_old_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_backward_old_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_backward_old_leftcoefficientscoefficientdiagonal) = (Lu)) /\ ((((exists ff_h_pfp_backward_old_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_backward_old_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_backward_old_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_backward_old_leftcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_backward_old_leftcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_backward_old_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_backward_old_leftcoefficientscoefficientdiagonal)) * uc) + (pfc_left_backward_old_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_old_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_backward_old_leftcoefficientscoefficientdiagonaltermleftoutside+(Lu)=(pfc_index_backward_old_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_backward_old_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_backward_old_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_backward_old_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_backward_old_leftcoefficientscoefficientdiagonalterm) = (Lb)) /\ ((((exists ff_h_pfp_backward_old_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_backward_old_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_backward_old_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_backward_old_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_backward_old_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_backward_old_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_backward_old_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_backward_old_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_old_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_backward_old_leftcoefficientscoefficientdiagonaltermrightoutside+(Lb)=(pfc_complement_backward_old_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_backward_old_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_backward_old_leftcoefficientscoefficientdiagonal)=pfc_left_backward_old_leftcoefficientscoefficientdiagonalterm*pfc_right_backward_old_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_backward_old_leftcoefficientscoefficientsum fs_v_pfc_backward_old_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_start. fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_backward_old_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_start. fs_u_pfc_backward_old_leftcoefficientscoefficientsum = fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_backward_old_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_backward_old_leftcoefficientscoefficient) = S ((S (S (pfc_index_backward_old_leftcoefficients))) * fs_v_pfc_backward_old_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_backward_old_leftcoefficientscoefficientsum = fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_backward_old_leftcoefficients))) * fs_v_pfc_backward_old_leftcoefficientscoefficientsum) + (pfc_natural_sum_backward_old_leftcoefficientscoefficient))) /\ forall fs_i_pfc_backward_old_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_backward_old_leftcoefficientscoefficientsum_body_steps = S (pfc_index_backward_old_leftcoefficients)) -> exists fs_a_pfc_backward_old_leftcoefficientscoefficientsum_body_steps fs_r_pfc_backward_old_leftcoefficientscoefficientsum_body_steps fs_s_pfc_backward_old_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_backward_old_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_old_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_old_leftcoefficientscoefficient)) /\ exists fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_backward_old_leftcoefficientscoefficient = fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_backward_old_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_old_leftcoefficientscoefficient) + (fs_a_pfc_backward_old_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_backward_old_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_old_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_old_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_backward_old_leftcoefficientscoefficientsum = fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_backward_old_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_old_leftcoefficientscoefficientsum) + (fs_r_pfc_backward_old_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_backward_old_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_backward_old_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_old_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_backward_old_leftcoefficientscoefficientsum = fs_q_pfc_backward_old_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_backward_old_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_old_leftcoefficientscoefficientsum) + (fs_s_pfc_backward_old_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_backward_old_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_backward_old_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_backward_old_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_backward_old_leftcoefficientscoefficientresiduebound. pfa_gap_backward_old_leftcoefficientscoefficientresiduebound + S (pfc_value_backward_old_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_backward_old_leftcoefficientscoefficientresiduecongruence pfa_offset_right_backward_old_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_backward_old_leftcoefficientscoefficient) + (p) * pfa_offset_left_backward_old_leftcoefficientscoefficientresiduecongruence = (pfc_value_backward_old_leftcoefficients) + (p) * pfa_offset_right_backward_old_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_backward_old_rightleft. (exists fom_gap_pfp_backward_old_rightleft_index_bound. fom_gap_pfp_backward_old_rightleft_index_bound + S (fom_index_pfp_backward_old_rightleft) = Lv) -> exists fom_value_pfp_backward_old_rightleft. ((((exists fom_beta_height_pfp_backward_old_rightleft_entry. fom_beta_height_pfp_backward_old_rightleft_entry + S (fom_value_pfp_backward_old_rightleft) = S ((S (fom_index_pfp_backward_old_rightleft)) * vc)) /\ exists fom_beta_quotient_pfp_backward_old_rightleft_entry. vb = fom_beta_quotient_pfp_backward_old_rightleft_entry * S ((S (fom_index_pfp_backward_old_rightleft)) * vc) + (fom_value_pfp_backward_old_rightleft))) /\ (exists fom_gap_pfp_backward_old_rightleft_value_bound. fom_gap_pfp_backward_old_rightleft_value_bound + S (fom_value_pfp_backward_old_rightleft) = p))) /\ (((forall fom_index_pfp_backward_old_rightright. (exists fom_gap_pfp_backward_old_rightright_index_bound. fom_gap_pfp_backward_old_rightright_index_bound + S (fom_index_pfp_backward_old_rightright) = Lr) -> exists fom_value_pfp_backward_old_rightright. ((((exists fom_beta_height_pfp_backward_old_rightright_entry. fom_beta_height_pfp_backward_old_rightright_entry + S (fom_value_pfp_backward_old_rightright) = S ((S (fom_index_pfp_backward_old_rightright)) * rc)) /\ exists fom_beta_quotient_pfp_backward_old_rightright_entry. rb = fom_beta_quotient_pfp_backward_old_rightright_entry * S ((S (fom_index_pfp_backward_old_rightright)) * rc) + (fom_value_pfp_backward_old_rightright))) /\ (exists fom_gap_pfp_backward_old_rightright_value_bound. fom_gap_pfp_backward_old_rightright_value_bound + S (fom_value_pfp_backward_old_rightright) = p))) /\ (((((((Lv)=0 \/ (Lr)=0) /\ (((Ld)=0)))) \/ (((~((Lv)=0)) /\ (((~((Lr)=0)) /\ (((Lv)+(Lr)=S (Ld)))))))) /\ ((forall pfc_index_backward_old_rightcoefficients. (exists pfa_gap_backward_old_rightcoefficientsbound. pfa_gap_backward_old_rightcoefficientsbound + S (pfc_index_backward_old_rightcoefficients) = (Ld)) -> exists pfc_value_backward_old_rightcoefficients. ((((exists ff_h_pfp_backward_old_rightcoefficientsentry. ff_h_pfp_backward_old_rightcoefficientsentry + S (pfc_value_backward_old_rightcoefficients) = S ((S (pfc_index_backward_old_rightcoefficients)) * dc)) /\ exists ff_q_pfp_backward_old_rightcoefficientsentry. db = ff_q_pfp_backward_old_rightcoefficientsentry * S ((S (pfc_index_backward_old_rightcoefficients)) * dc) + (pfc_value_backward_old_rightcoefficients))) /\ ((exists pfc_terms_code_backward_old_rightcoefficientscoefficient pfc_terms_scale_backward_old_rightcoefficientscoefficient pfc_natural_sum_backward_old_rightcoefficientscoefficient. ((forall pfc_index_backward_old_rightcoefficientscoefficientdiagonal. (exists pfa_gap_backward_old_rightcoefficientscoefficientdiagonalbound. pfa_gap_backward_old_rightcoefficientscoefficientdiagonalbound + S (pfc_index_backward_old_rightcoefficientscoefficientdiagonal) = (S (pfc_index_backward_old_rightcoefficients))) -> exists pfc_value_backward_old_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_backward_old_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_backward_old_rightcoefficientscoefficientdiagonalentry + S (pfc_value_backward_old_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_backward_old_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_old_rightcoefficientscoefficient)) /\ exists ff_q_pfp_backward_old_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_backward_old_rightcoefficientscoefficient = ff_q_pfp_backward_old_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_backward_old_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_old_rightcoefficientscoefficient) + (pfc_value_backward_old_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_backward_old_rightcoefficientscoefficientdiagonalterm pfc_left_backward_old_rightcoefficientscoefficientdiagonalterm pfc_right_backward_old_rightcoefficientscoefficientdiagonalterm. (((pfc_index_backward_old_rightcoefficientscoefficientdiagonal)+pfc_complement_backward_old_rightcoefficientscoefficientdiagonalterm=(pfc_index_backward_old_rightcoefficients)) /\ ((((((exists pfa_gap_backward_old_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_backward_old_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_backward_old_rightcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_backward_old_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_backward_old_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_backward_old_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_backward_old_rightcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_backward_old_rightcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_backward_old_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_backward_old_rightcoefficientscoefficientdiagonal)) * vc) + (pfc_left_backward_old_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_old_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_backward_old_rightcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_backward_old_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_backward_old_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_backward_old_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_backward_old_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_backward_old_rightcoefficientscoefficientdiagonalterm) = (Lr)) /\ ((((exists ff_h_pfp_backward_old_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_backward_old_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_backward_old_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_backward_old_rightcoefficientscoefficientdiagonalterm)) * rc)) /\ exists ff_q_pfp_backward_old_rightcoefficientscoefficientdiagonaltermrightentry. rb = ff_q_pfp_backward_old_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_backward_old_rightcoefficientscoefficientdiagonalterm)) * rc) + (pfc_right_backward_old_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_old_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_backward_old_rightcoefficientscoefficientdiagonaltermrightoutside+(Lr)=(pfc_complement_backward_old_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_backward_old_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_backward_old_rightcoefficientscoefficientdiagonal)=pfc_left_backward_old_rightcoefficientscoefficientdiagonalterm*pfc_right_backward_old_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_backward_old_rightcoefficientscoefficientsum fs_v_pfc_backward_old_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_start. fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_backward_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_start. fs_u_pfc_backward_old_rightcoefficientscoefficientsum = fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_backward_old_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_backward_old_rightcoefficientscoefficient) = S ((S (S (pfc_index_backward_old_rightcoefficients))) * fs_v_pfc_backward_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_backward_old_rightcoefficientscoefficientsum = fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_backward_old_rightcoefficients))) * fs_v_pfc_backward_old_rightcoefficientscoefficientsum) + (pfc_natural_sum_backward_old_rightcoefficientscoefficient))) /\ forall fs_i_pfc_backward_old_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_backward_old_rightcoefficientscoefficientsum_body_steps = S (pfc_index_backward_old_rightcoefficients)) -> exists fs_a_pfc_backward_old_rightcoefficientscoefficientsum_body_steps fs_r_pfc_backward_old_rightcoefficientscoefficientsum_body_steps fs_s_pfc_backward_old_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_backward_old_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_old_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_old_rightcoefficientscoefficient)) /\ exists fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_backward_old_rightcoefficientscoefficient = fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_backward_old_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_old_rightcoefficientscoefficient) + (fs_a_pfc_backward_old_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_backward_old_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_backward_old_rightcoefficientscoefficientsum = fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_backward_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_old_rightcoefficientscoefficientsum) + (fs_r_pfc_backward_old_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_backward_old_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_backward_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_backward_old_rightcoefficientscoefficientsum = fs_q_pfc_backward_old_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_backward_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_old_rightcoefficientscoefficientsum) + (fs_s_pfc_backward_old_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_backward_old_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_backward_old_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_backward_old_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_backward_old_rightcoefficientscoefficientresiduebound. pfa_gap_backward_old_rightcoefficientscoefficientresiduebound + S (pfc_value_backward_old_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_backward_old_rightcoefficientscoefficientresiduecongruence pfa_offset_right_backward_old_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_backward_old_rightcoefficientscoefficient) + (p) * pfa_offset_left_backward_old_rightcoefficientscoefficientresiduecongruence = (pfc_value_backward_old_rightcoefficients) + (p) * pfa_offset_right_backward_old_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_backward_old_sum_left_bounded. (exists fom_gap_pfp_backward_old_sum_left_bounded_index_bound. fom_gap_pfp_backward_old_sum_left_bounded_index_bound + S (fom_index_pfp_backward_old_sum_left_bounded) = Lc) -> exists fom_value_pfp_backward_old_sum_left_bounded. ((((exists fom_beta_height_pfp_backward_old_sum_left_bounded_entry. fom_beta_height_pfp_backward_old_sum_left_bounded_entry + S (fom_value_pfp_backward_old_sum_left_bounded) = S ((S (fom_index_pfp_backward_old_sum_left_bounded)) * cc)) /\ exists fom_beta_quotient_pfp_backward_old_sum_left_bounded_entry. cb = fom_beta_quotient_pfp_backward_old_sum_left_bounded_entry * S ((S (fom_index_pfp_backward_old_sum_left_bounded)) * cc) + (fom_value_pfp_backward_old_sum_left_bounded))) /\ (exists fom_gap_pfp_backward_old_sum_left_bounded_value_bound. fom_gap_pfp_backward_old_sum_left_bounded_value_bound + S (fom_value_pfp_backward_old_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_backward_old_sum_right_bounded. (exists fom_gap_pfp_backward_old_sum_right_bounded_index_bound. fom_gap_pfp_backward_old_sum_right_bounded_index_bound + S (fom_index_pfp_backward_old_sum_right_bounded) = Ld) -> exists fom_value_pfp_backward_old_sum_right_bounded. ((((exists fom_beta_height_pfp_backward_old_sum_right_bounded_entry. fom_beta_height_pfp_backward_old_sum_right_bounded_entry + S (fom_value_pfp_backward_old_sum_right_bounded) = S ((S (fom_index_pfp_backward_old_sum_right_bounded)) * dc)) /\ exists fom_beta_quotient_pfp_backward_old_sum_right_bounded_entry. db = fom_beta_quotient_pfp_backward_old_sum_right_bounded_entry * S ((S (fom_index_pfp_backward_old_sum_right_bounded)) * dc) + (fom_value_pfp_backward_old_sum_right_bounded))) /\ (exists fom_gap_pfp_backward_old_sum_right_bounded_value_bound. fom_gap_pfp_backward_old_sum_right_bounded_value_bound + S (fom_value_pfp_backward_old_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_backward_old_sum_result_bounded. (exists fom_gap_pfp_backward_old_sum_result_bounded_index_bound. fom_gap_pfp_backward_old_sum_result_bounded_index_bound + S (fom_index_pfp_backward_old_sum_result_bounded) = Lg) -> exists fom_value_pfp_backward_old_sum_result_bounded. ((((exists fom_beta_height_pfp_backward_old_sum_result_bounded_entry. fom_beta_height_pfp_backward_old_sum_result_bounded_entry + S (fom_value_pfp_backward_old_sum_result_bounded) = S ((S (fom_index_pfp_backward_old_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_backward_old_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_backward_old_sum_result_bounded_entry * S ((S (fom_index_pfp_backward_old_sum_result_bounded)) * gc) + (fom_value_pfp_backward_old_sum_result_bounded))) /\ (exists fom_gap_pfp_backward_old_sum_result_bounded_value_bound. fom_gap_pfp_backward_old_sum_result_bounded_value_bound + S (fom_value_pfp_backward_old_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_backward_old_sum pfaa_left_c_backward_old_sum pfaa_right_b_backward_old_sum pfaa_right_c_backward_old_sum pfaa_sum_b_backward_old_sum pfaa_sum_c_backward_old_sum pfaa_length_backward_old_sum. ((((forall pfrep_power_backward_old_sum_witness_common_left pfrep_left_backward_old_sum_witness_common_left pfrep_right_backward_old_sum_witness_common_left. ((exists pfrep_position_backward_old_sum_witness_common_leftfirst. ((pfrep_position_backward_old_sum_witness_common_leftfirst+S (pfrep_power_backward_old_sum_witness_common_left)=(Lc)) /\ ((((exists ff_h_pfp_backward_old_sum_witness_common_leftfirstentry. ff_h_pfp_backward_old_sum_witness_common_leftfirstentry + S (pfrep_left_backward_old_sum_witness_common_left) = S ((S (pfrep_position_backward_old_sum_witness_common_leftfirst)) * cc)) /\ exists ff_q_pfp_backward_old_sum_witness_common_leftfirstentry. cb = ff_q_pfp_backward_old_sum_witness_common_leftfirstentry * S ((S (pfrep_position_backward_old_sum_witness_common_leftfirst)) * cc) + (pfrep_left_backward_old_sum_witness_common_left)))))) \/ (((exists pfrep_gap_backward_old_sum_witness_common_leftfirstoutside. pfrep_gap_backward_old_sum_witness_common_leftfirstoutside+(Lc)=(pfrep_power_backward_old_sum_witness_common_left)) /\ (((pfrep_left_backward_old_sum_witness_common_left)=0))))) -> ((exists pfrep_position_backward_old_sum_witness_common_leftsecond. ((pfrep_position_backward_old_sum_witness_common_leftsecond+S (pfrep_power_backward_old_sum_witness_common_left)=(pfaa_length_backward_old_sum)) /\ ((((exists ff_h_pfp_backward_old_sum_witness_common_leftsecondentry. ff_h_pfp_backward_old_sum_witness_common_leftsecondentry + S (pfrep_right_backward_old_sum_witness_common_left) = S ((S (pfrep_position_backward_old_sum_witness_common_leftsecond)) * pfaa_left_c_backward_old_sum)) /\ exists ff_q_pfp_backward_old_sum_witness_common_leftsecondentry. pfaa_left_b_backward_old_sum = ff_q_pfp_backward_old_sum_witness_common_leftsecondentry * S ((S (pfrep_position_backward_old_sum_witness_common_leftsecond)) * pfaa_left_c_backward_old_sum) + (pfrep_right_backward_old_sum_witness_common_left)))))) \/ (((exists pfrep_gap_backward_old_sum_witness_common_leftsecondoutside. pfrep_gap_backward_old_sum_witness_common_leftsecondoutside+(pfaa_length_backward_old_sum)=(pfrep_power_backward_old_sum_witness_common_left)) /\ (((pfrep_right_backward_old_sum_witness_common_left)=0))))) -> pfrep_left_backward_old_sum_witness_common_left=pfrep_right_backward_old_sum_witness_common_left) /\ ((forall pfrep_power_backward_old_sum_witness_common_right pfrep_left_backward_old_sum_witness_common_right pfrep_right_backward_old_sum_witness_common_right. ((exists pfrep_position_backward_old_sum_witness_common_rightfirst. ((pfrep_position_backward_old_sum_witness_common_rightfirst+S (pfrep_power_backward_old_sum_witness_common_right)=(Ld)) /\ ((((exists ff_h_pfp_backward_old_sum_witness_common_rightfirstentry. ff_h_pfp_backward_old_sum_witness_common_rightfirstentry + S (pfrep_left_backward_old_sum_witness_common_right) = S ((S (pfrep_position_backward_old_sum_witness_common_rightfirst)) * dc)) /\ exists ff_q_pfp_backward_old_sum_witness_common_rightfirstentry. db = ff_q_pfp_backward_old_sum_witness_common_rightfirstentry * S ((S (pfrep_position_backward_old_sum_witness_common_rightfirst)) * dc) + (pfrep_left_backward_old_sum_witness_common_right)))))) \/ (((exists pfrep_gap_backward_old_sum_witness_common_rightfirstoutside. pfrep_gap_backward_old_sum_witness_common_rightfirstoutside+(Ld)=(pfrep_power_backward_old_sum_witness_common_right)) /\ (((pfrep_left_backward_old_sum_witness_common_right)=0))))) -> ((exists pfrep_position_backward_old_sum_witness_common_rightsecond. ((pfrep_position_backward_old_sum_witness_common_rightsecond+S (pfrep_power_backward_old_sum_witness_common_right)=(pfaa_length_backward_old_sum)) /\ ((((exists ff_h_pfp_backward_old_sum_witness_common_rightsecondentry. ff_h_pfp_backward_old_sum_witness_common_rightsecondentry + S (pfrep_right_backward_old_sum_witness_common_right) = S ((S (pfrep_position_backward_old_sum_witness_common_rightsecond)) * pfaa_right_c_backward_old_sum)) /\ exists ff_q_pfp_backward_old_sum_witness_common_rightsecondentry. pfaa_right_b_backward_old_sum = ff_q_pfp_backward_old_sum_witness_common_rightsecondentry * S ((S (pfrep_position_backward_old_sum_witness_common_rightsecond)) * pfaa_right_c_backward_old_sum) + (pfrep_right_backward_old_sum_witness_common_right)))))) \/ (((exists pfrep_gap_backward_old_sum_witness_common_rightsecondoutside. pfrep_gap_backward_old_sum_witness_common_rightsecondoutside+(pfaa_length_backward_old_sum)=(pfrep_power_backward_old_sum_witness_common_right)) /\ (((pfrep_right_backward_old_sum_witness_common_right)=0))))) -> pfrep_left_backward_old_sum_witness_common_right=pfrep_right_backward_old_sum_witness_common_right)))) /\ (((forall pfp_index_backward_old_sum_witness_operation. (exists pfa_gap_backward_old_sum_witness_operationindex. pfa_gap_backward_old_sum_witness_operationindex + S (pfp_index_backward_old_sum_witness_operation) = (pfaa_length_backward_old_sum)) -> exists pfp_left_backward_old_sum_witness_operation pfp_right_backward_old_sum_witness_operation pfp_value_backward_old_sum_witness_operation. ((((exists ff_h_pfp_backward_old_sum_witness_operationleft. ff_h_pfp_backward_old_sum_witness_operationleft + S (pfp_left_backward_old_sum_witness_operation) = S ((S (pfp_index_backward_old_sum_witness_operation)) * pfaa_left_c_backward_old_sum)) /\ exists ff_q_pfp_backward_old_sum_witness_operationleft. pfaa_left_b_backward_old_sum = ff_q_pfp_backward_old_sum_witness_operationleft * S ((S (pfp_index_backward_old_sum_witness_operation)) * pfaa_left_c_backward_old_sum) + (pfp_left_backward_old_sum_witness_operation))) /\ (((((exists ff_h_pfp_backward_old_sum_witness_operationright. ff_h_pfp_backward_old_sum_witness_operationright + S (pfp_right_backward_old_sum_witness_operation) = S ((S (pfp_index_backward_old_sum_witness_operation)) * pfaa_right_c_backward_old_sum)) /\ exists ff_q_pfp_backward_old_sum_witness_operationright. pfaa_right_b_backward_old_sum = ff_q_pfp_backward_old_sum_witness_operationright * S ((S (pfp_index_backward_old_sum_witness_operation)) * pfaa_right_c_backward_old_sum) + (pfp_right_backward_old_sum_witness_operation))) /\ (((((exists ff_h_pfp_backward_old_sum_witness_operationtarget. ff_h_pfp_backward_old_sum_witness_operationtarget + S (pfp_value_backward_old_sum_witness_operation) = S ((S (pfp_index_backward_old_sum_witness_operation)) * pfaa_sum_c_backward_old_sum)) /\ exists ff_q_pfp_backward_old_sum_witness_operationtarget. pfaa_sum_b_backward_old_sum = ff_q_pfp_backward_old_sum_witness_operationtarget * S ((S (pfp_index_backward_old_sum_witness_operation)) * pfaa_sum_c_backward_old_sum) + (pfp_value_backward_old_sum_witness_operation))) /\ ((((exists pfa_gap_backward_old_sum_witness_operationoperationleft. pfa_gap_backward_old_sum_witness_operationoperationleft + S (pfp_left_backward_old_sum_witness_operation) = (p)) /\ (((exists pfa_gap_backward_old_sum_witness_operationoperationright. pfa_gap_backward_old_sum_witness_operationoperationright + S (pfp_right_backward_old_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_backward_old_sum_witness_operationoperationresultbound. pfa_gap_backward_old_sum_witness_operationoperationresultbound + S (pfp_value_backward_old_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_backward_old_sum_witness_operationoperationresultcongruence pfa_offset_right_backward_old_sum_witness_operationoperationresultcongruence. ((pfp_left_backward_old_sum_witness_operation) + (pfp_right_backward_old_sum_witness_operation)) + (p) * pfa_offset_left_backward_old_sum_witness_operationoperationresultcongruence = (pfp_value_backward_old_sum_witness_operation) + (p) * pfa_offset_right_backward_old_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_backward_old_sum_witness_output pfrep_left_backward_old_sum_witness_output pfrep_right_backward_old_sum_witness_output. ((exists pfrep_position_backward_old_sum_witness_outputfirst. ((pfrep_position_backward_old_sum_witness_outputfirst+S (pfrep_power_backward_old_sum_witness_output)=(pfaa_length_backward_old_sum)) /\ ((((exists ff_h_pfp_backward_old_sum_witness_outputfirstentry. ff_h_pfp_backward_old_sum_witness_outputfirstentry + S (pfrep_left_backward_old_sum_witness_output) = S ((S (pfrep_position_backward_old_sum_witness_outputfirst)) * pfaa_sum_c_backward_old_sum)) /\ exists ff_q_pfp_backward_old_sum_witness_outputfirstentry. pfaa_sum_b_backward_old_sum = ff_q_pfp_backward_old_sum_witness_outputfirstentry * S ((S (pfrep_position_backward_old_sum_witness_outputfirst)) * pfaa_sum_c_backward_old_sum) + (pfrep_left_backward_old_sum_witness_output)))))) \/ (((exists pfrep_gap_backward_old_sum_witness_outputfirstoutside. pfrep_gap_backward_old_sum_witness_outputfirstoutside+(pfaa_length_backward_old_sum)=(pfrep_power_backward_old_sum_witness_output)) /\ (((pfrep_left_backward_old_sum_witness_output)=0))))) -> ((exists pfrep_position_backward_old_sum_witness_outputsecond. ((pfrep_position_backward_old_sum_witness_outputsecond+S (pfrep_power_backward_old_sum_witness_output)=(Lg)) /\ ((((exists ff_h_pfp_backward_old_sum_witness_outputsecondentry. ff_h_pfp_backward_old_sum_witness_outputsecondentry + S (pfrep_right_backward_old_sum_witness_output) = S ((S (pfrep_position_backward_old_sum_witness_outputsecond)) * gc)) /\ exists ff_q_pfp_backward_old_sum_witness_outputsecondentry. gb = ff_q_pfp_backward_old_sum_witness_outputsecondentry * S ((S (pfrep_position_backward_old_sum_witness_outputsecond)) * gc) + (pfrep_right_backward_old_sum_witness_output)))))) \/ (((exists pfrep_gap_backward_old_sum_witness_outputsecondoutside. pfrep_gap_backward_old_sum_witness_outputsecondoutside+(Lg)=(pfrep_power_backward_old_sum_witness_output)) /\ (((pfrep_right_backward_old_sum_witness_output)=0))))) -> pfrep_left_backward_old_sum_witness_output=pfrep_right_backward_old_sum_witness_output))))))))))))) -> (((forall fom_index_pfp_backward_coefficient_productleft. (exists fom_gap_pfp_backward_coefficient_productleft_index_bound. fom_gap_pfp_backward_coefficient_productleft_index_bound + S (fom_index_pfp_backward_coefficient_productleft) = Lv) -> exists fom_value_pfp_backward_coefficient_productleft. ((((exists fom_beta_height_pfp_backward_coefficient_productleft_entry. fom_beta_height_pfp_backward_coefficient_productleft_entry + S (fom_value_pfp_backward_coefficient_productleft) = S ((S (fom_index_pfp_backward_coefficient_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_backward_coefficient_productleft_entry. vb = fom_beta_quotient_pfp_backward_coefficient_productleft_entry * S ((S (fom_index_pfp_backward_coefficient_productleft)) * vc) + (fom_value_pfp_backward_coefficient_productleft))) /\ (exists fom_gap_pfp_backward_coefficient_productleft_value_bound. fom_gap_pfp_backward_coefficient_productleft_value_bound + S (fom_value_pfp_backward_coefficient_productleft) = p))) /\ (((forall fom_index_pfp_backward_coefficient_productright. (exists fom_gap_pfp_backward_coefficient_productright_index_bound. fom_gap_pfp_backward_coefficient_productright_index_bound + S (fom_index_pfp_backward_coefficient_productright) = Lq) -> exists fom_value_pfp_backward_coefficient_productright. ((((exists fom_beta_height_pfp_backward_coefficient_productright_entry. fom_beta_height_pfp_backward_coefficient_productright_entry + S (fom_value_pfp_backward_coefficient_productright) = S ((S (fom_index_pfp_backward_coefficient_productright)) * qc)) /\ exists fom_beta_quotient_pfp_backward_coefficient_productright_entry. qb = fom_beta_quotient_pfp_backward_coefficient_productright_entry * S ((S (fom_index_pfp_backward_coefficient_productright)) * qc) + (fom_value_pfp_backward_coefficient_productright))) /\ (exists fom_gap_pfp_backward_coefficient_productright_value_bound. fom_gap_pfp_backward_coefficient_productright_value_bound + S (fom_value_pfp_backward_coefficient_productright) = p))) /\ (((((((Lv)=0 \/ (Lq)=0) /\ (((Lw)=0)))) \/ (((~((Lv)=0)) /\ (((~((Lq)=0)) /\ (((Lv)+(Lq)=S (Lw)))))))) /\ ((forall pfc_index_backward_coefficient_productcoefficients. (exists pfa_gap_backward_coefficient_productcoefficientsbound. pfa_gap_backward_coefficient_productcoefficientsbound + S (pfc_index_backward_coefficient_productcoefficients) = (Lw)) -> exists pfc_value_backward_coefficient_productcoefficients. ((((exists ff_h_pfp_backward_coefficient_productcoefficientsentry. ff_h_pfp_backward_coefficient_productcoefficientsentry + S (pfc_value_backward_coefficient_productcoefficients) = S ((S (pfc_index_backward_coefficient_productcoefficients)) * wc)) /\ exists ff_q_pfp_backward_coefficient_productcoefficientsentry. wb = ff_q_pfp_backward_coefficient_productcoefficientsentry * S ((S (pfc_index_backward_coefficient_productcoefficients)) * wc) + (pfc_value_backward_coefficient_productcoefficients))) /\ ((exists pfc_terms_code_backward_coefficient_productcoefficientscoefficient pfc_terms_scale_backward_coefficient_productcoefficientscoefficient pfc_natural_sum_backward_coefficient_productcoefficientscoefficient. ((forall pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal. (exists pfa_gap_backward_coefficient_productcoefficientscoefficientdiagonalbound. pfa_gap_backward_coefficient_productcoefficientscoefficientdiagonalbound + S (pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal) = (S (pfc_index_backward_coefficient_productcoefficients))) -> exists pfc_value_backward_coefficient_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_backward_coefficient_productcoefficientscoefficientdiagonalentry. ff_h_pfp_backward_coefficient_productcoefficientscoefficientdiagonalentry + S (pfc_value_backward_coefficient_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_coefficient_productcoefficientscoefficient)) /\ exists ff_q_pfp_backward_coefficient_productcoefficientscoefficientdiagonalentry. pfc_terms_code_backward_coefficient_productcoefficientscoefficient = ff_q_pfp_backward_coefficient_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_coefficient_productcoefficientscoefficient) + (pfc_value_backward_coefficient_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_backward_coefficient_productcoefficientscoefficientdiagonalterm pfc_left_backward_coefficient_productcoefficientscoefficientdiagonalterm pfc_right_backward_coefficient_productcoefficientscoefficientdiagonalterm. (((pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal)+pfc_complement_backward_coefficient_productcoefficientscoefficientdiagonalterm=(pfc_index_backward_coefficient_productcoefficients)) /\ ((((((exists pfa_gap_backward_coefficient_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_backward_coefficient_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_backward_coefficient_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_backward_coefficient_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_backward_coefficient_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_backward_coefficient_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_backward_coefficient_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_backward_coefficient_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_coefficient_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_backward_coefficient_productcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_backward_coefficient_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_backward_coefficient_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_backward_coefficient_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_backward_coefficient_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_backward_coefficient_productcoefficientscoefficientdiagonalterm) = (Lq)) /\ ((((exists ff_h_pfp_backward_coefficient_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_backward_coefficient_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_backward_coefficient_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_backward_coefficient_productcoefficientscoefficientdiagonalterm)) * qc)) /\ exists ff_q_pfp_backward_coefficient_productcoefficientscoefficientdiagonaltermrightentry. qb = ff_q_pfp_backward_coefficient_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_backward_coefficient_productcoefficientscoefficientdiagonalterm)) * qc) + (pfc_right_backward_coefficient_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_coefficient_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_backward_coefficient_productcoefficientscoefficientdiagonaltermrightoutside+(Lq)=(pfc_complement_backward_coefficient_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_backward_coefficient_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_backward_coefficient_productcoefficientscoefficientdiagonal)=pfc_left_backward_coefficient_productcoefficientscoefficientdiagonalterm*pfc_right_backward_coefficient_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_backward_coefficient_productcoefficientscoefficientsum fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum. ((((exists fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_start. fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_start. fs_u_pfc_backward_coefficient_productcoefficientscoefficientsum = fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_backward_coefficient_productcoefficientscoefficient) = S ((S (S (pfc_index_backward_coefficient_productcoefficients))) * fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_backward_coefficient_productcoefficientscoefficientsum = fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_backward_coefficient_productcoefficients))) * fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum) + (pfc_natural_sum_backward_coefficient_productcoefficientscoefficient))) /\ forall fs_i_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps = S (pfc_index_backward_coefficient_productcoefficients)) -> exists fs_a_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps fs_r_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps fs_s_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_coefficient_productcoefficientscoefficient)) /\ exists fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_backward_coefficient_productcoefficientscoefficient = fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_coefficient_productcoefficientscoefficient) + (fs_a_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_backward_coefficient_productcoefficientscoefficientsum = fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum) + (fs_r_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_backward_coefficient_productcoefficientscoefficientsum = fs_q_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_coefficient_productcoefficientscoefficientsum) + (fs_s_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps = fs_r_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps + fs_a_pfc_backward_coefficient_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_backward_coefficient_productcoefficientscoefficientresiduebound. pfa_gap_backward_coefficient_productcoefficientscoefficientresiduebound + S (pfc_value_backward_coefficient_productcoefficients) = (p)) /\ ((exists pfa_offset_left_backward_coefficient_productcoefficientscoefficientresiduecongruence pfa_offset_right_backward_coefficient_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_backward_coefficient_productcoefficientscoefficient) + (p) * pfa_offset_left_backward_coefficient_productcoefficientscoefficientresiduecongruence = (pfc_value_backward_coefficient_productcoefficients) + (p) * pfa_offset_right_backward_coefficient_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_backward_coefficient_difference_left_bounded. (exists fom_gap_pfp_backward_coefficient_difference_left_bounded_index_bound. fom_gap_pfp_backward_coefficient_difference_left_bounded_index_bound + S (fom_index_pfp_backward_coefficient_difference_left_bounded) = Lw) -> exists fom_value_pfp_backward_coefficient_difference_left_bounded. ((((exists fom_beta_height_pfp_backward_coefficient_difference_left_bounded_entry. fom_beta_height_pfp_backward_coefficient_difference_left_bounded_entry + S (fom_value_pfp_backward_coefficient_difference_left_bounded) = S ((S (fom_index_pfp_backward_coefficient_difference_left_bounded)) * wc)) /\ exists fom_beta_quotient_pfp_backward_coefficient_difference_left_bounded_entry. wb = fom_beta_quotient_pfp_backward_coefficient_difference_left_bounded_entry * S ((S (fom_index_pfp_backward_coefficient_difference_left_bounded)) * wc) + (fom_value_pfp_backward_coefficient_difference_left_bounded))) /\ (exists fom_gap_pfp_backward_coefficient_difference_left_bounded_value_bound. fom_gap_pfp_backward_coefficient_difference_left_bounded_value_bound + S (fom_value_pfp_backward_coefficient_difference_left_bounded) = p))) /\ (((forall fom_index_pfp_backward_coefficient_difference_right_bounded. (exists fom_gap_pfp_backward_coefficient_difference_right_bounded_index_bound. fom_gap_pfp_backward_coefficient_difference_right_bounded_index_bound + S (fom_index_pfp_backward_coefficient_difference_right_bounded) = Lt) -> exists fom_value_pfp_backward_coefficient_difference_right_bounded. ((((exists fom_beta_height_pfp_backward_coefficient_difference_right_bounded_entry. fom_beta_height_pfp_backward_coefficient_difference_right_bounded_entry + S (fom_value_pfp_backward_coefficient_difference_right_bounded) = S ((S (fom_index_pfp_backward_coefficient_difference_right_bounded)) * tc)) /\ exists fom_beta_quotient_pfp_backward_coefficient_difference_right_bounded_entry. tb = fom_beta_quotient_pfp_backward_coefficient_difference_right_bounded_entry * S ((S (fom_index_pfp_backward_coefficient_difference_right_bounded)) * tc) + (fom_value_pfp_backward_coefficient_difference_right_bounded))) /\ (exists fom_gap_pfp_backward_coefficient_difference_right_bounded_value_bound. fom_gap_pfp_backward_coefficient_difference_right_bounded_value_bound + S (fom_value_pfp_backward_coefficient_difference_right_bounded) = p))) /\ (((forall fom_index_pfp_backward_coefficient_difference_result_bounded. (exists fom_gap_pfp_backward_coefficient_difference_result_bounded_index_bound. fom_gap_pfp_backward_coefficient_difference_result_bounded_index_bound + S (fom_index_pfp_backward_coefficient_difference_result_bounded) = Lu) -> exists fom_value_pfp_backward_coefficient_difference_result_bounded. ((((exists fom_beta_height_pfp_backward_coefficient_difference_result_bounded_entry. fom_beta_height_pfp_backward_coefficient_difference_result_bounded_entry + S (fom_value_pfp_backward_coefficient_difference_result_bounded) = S ((S (fom_index_pfp_backward_coefficient_difference_result_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_backward_coefficient_difference_result_bounded_entry. ub = fom_beta_quotient_pfp_backward_coefficient_difference_result_bounded_entry * S ((S (fom_index_pfp_backward_coefficient_difference_result_bounded)) * uc) + (fom_value_pfp_backward_coefficient_difference_result_bounded))) /\ (exists fom_gap_pfp_backward_coefficient_difference_result_bounded_value_bound. fom_gap_pfp_backward_coefficient_difference_result_bounded_value_bound + S (fom_value_pfp_backward_coefficient_difference_result_bounded) = p))) /\ ((exists pfaa_left_b_backward_coefficient_difference pfaa_left_c_backward_coefficient_difference pfaa_right_b_backward_coefficient_difference pfaa_right_c_backward_coefficient_difference pfaa_sum_b_backward_coefficient_difference pfaa_sum_c_backward_coefficient_difference pfaa_length_backward_coefficient_difference. ((((forall pfrep_power_backward_coefficient_difference_witness_common_left pfrep_left_backward_coefficient_difference_witness_common_left pfrep_right_backward_coefficient_difference_witness_common_left. ((exists pfrep_position_backward_coefficient_difference_witness_common_leftfirst. ((pfrep_position_backward_coefficient_difference_witness_common_leftfirst+S (pfrep_power_backward_coefficient_difference_witness_common_left)=(Lw)) /\ ((((exists ff_h_pfp_backward_coefficient_difference_witness_common_leftfirstentry. ff_h_pfp_backward_coefficient_difference_witness_common_leftfirstentry + S (pfrep_left_backward_coefficient_difference_witness_common_left) = S ((S (pfrep_position_backward_coefficient_difference_witness_common_leftfirst)) * wc)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_common_leftfirstentry. wb = ff_q_pfp_backward_coefficient_difference_witness_common_leftfirstentry * S ((S (pfrep_position_backward_coefficient_difference_witness_common_leftfirst)) * wc) + (pfrep_left_backward_coefficient_difference_witness_common_left)))))) \/ (((exists pfrep_gap_backward_coefficient_difference_witness_common_leftfirstoutside. pfrep_gap_backward_coefficient_difference_witness_common_leftfirstoutside+(Lw)=(pfrep_power_backward_coefficient_difference_witness_common_left)) /\ (((pfrep_left_backward_coefficient_difference_witness_common_left)=0))))) -> ((exists pfrep_position_backward_coefficient_difference_witness_common_leftsecond. ((pfrep_position_backward_coefficient_difference_witness_common_leftsecond+S (pfrep_power_backward_coefficient_difference_witness_common_left)=(pfaa_length_backward_coefficient_difference)) /\ ((((exists ff_h_pfp_backward_coefficient_difference_witness_common_leftsecondentry. ff_h_pfp_backward_coefficient_difference_witness_common_leftsecondentry + S (pfrep_right_backward_coefficient_difference_witness_common_left) = S ((S (pfrep_position_backward_coefficient_difference_witness_common_leftsecond)) * pfaa_left_c_backward_coefficient_difference)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_common_leftsecondentry. pfaa_left_b_backward_coefficient_difference = ff_q_pfp_backward_coefficient_difference_witness_common_leftsecondentry * S ((S (pfrep_position_backward_coefficient_difference_witness_common_leftsecond)) * pfaa_left_c_backward_coefficient_difference) + (pfrep_right_backward_coefficient_difference_witness_common_left)))))) \/ (((exists pfrep_gap_backward_coefficient_difference_witness_common_leftsecondoutside. pfrep_gap_backward_coefficient_difference_witness_common_leftsecondoutside+(pfaa_length_backward_coefficient_difference)=(pfrep_power_backward_coefficient_difference_witness_common_left)) /\ (((pfrep_right_backward_coefficient_difference_witness_common_left)=0))))) -> pfrep_left_backward_coefficient_difference_witness_common_left=pfrep_right_backward_coefficient_difference_witness_common_left) /\ ((forall pfrep_power_backward_coefficient_difference_witness_common_right pfrep_left_backward_coefficient_difference_witness_common_right pfrep_right_backward_coefficient_difference_witness_common_right. ((exists pfrep_position_backward_coefficient_difference_witness_common_rightfirst. ((pfrep_position_backward_coefficient_difference_witness_common_rightfirst+S (pfrep_power_backward_coefficient_difference_witness_common_right)=(Lt)) /\ ((((exists ff_h_pfp_backward_coefficient_difference_witness_common_rightfirstentry. ff_h_pfp_backward_coefficient_difference_witness_common_rightfirstentry + S (pfrep_left_backward_coefficient_difference_witness_common_right) = S ((S (pfrep_position_backward_coefficient_difference_witness_common_rightfirst)) * tc)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_common_rightfirstentry. tb = ff_q_pfp_backward_coefficient_difference_witness_common_rightfirstentry * S ((S (pfrep_position_backward_coefficient_difference_witness_common_rightfirst)) * tc) + (pfrep_left_backward_coefficient_difference_witness_common_right)))))) \/ (((exists pfrep_gap_backward_coefficient_difference_witness_common_rightfirstoutside. pfrep_gap_backward_coefficient_difference_witness_common_rightfirstoutside+(Lt)=(pfrep_power_backward_coefficient_difference_witness_common_right)) /\ (((pfrep_left_backward_coefficient_difference_witness_common_right)=0))))) -> ((exists pfrep_position_backward_coefficient_difference_witness_common_rightsecond. ((pfrep_position_backward_coefficient_difference_witness_common_rightsecond+S (pfrep_power_backward_coefficient_difference_witness_common_right)=(pfaa_length_backward_coefficient_difference)) /\ ((((exists ff_h_pfp_backward_coefficient_difference_witness_common_rightsecondentry. ff_h_pfp_backward_coefficient_difference_witness_common_rightsecondentry + S (pfrep_right_backward_coefficient_difference_witness_common_right) = S ((S (pfrep_position_backward_coefficient_difference_witness_common_rightsecond)) * pfaa_right_c_backward_coefficient_difference)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_common_rightsecondentry. pfaa_right_b_backward_coefficient_difference = ff_q_pfp_backward_coefficient_difference_witness_common_rightsecondentry * S ((S (pfrep_position_backward_coefficient_difference_witness_common_rightsecond)) * pfaa_right_c_backward_coefficient_difference) + (pfrep_right_backward_coefficient_difference_witness_common_right)))))) \/ (((exists pfrep_gap_backward_coefficient_difference_witness_common_rightsecondoutside. pfrep_gap_backward_coefficient_difference_witness_common_rightsecondoutside+(pfaa_length_backward_coefficient_difference)=(pfrep_power_backward_coefficient_difference_witness_common_right)) /\ (((pfrep_right_backward_coefficient_difference_witness_common_right)=0))))) -> pfrep_left_backward_coefficient_difference_witness_common_right=pfrep_right_backward_coefficient_difference_witness_common_right)))) /\ (((forall pfp_index_backward_coefficient_difference_witness_operation. (exists pfa_gap_backward_coefficient_difference_witness_operationindex. pfa_gap_backward_coefficient_difference_witness_operationindex + S (pfp_index_backward_coefficient_difference_witness_operation) = (pfaa_length_backward_coefficient_difference)) -> exists pfp_left_backward_coefficient_difference_witness_operation pfp_right_backward_coefficient_difference_witness_operation pfp_value_backward_coefficient_difference_witness_operation. ((((exists ff_h_pfp_backward_coefficient_difference_witness_operationleft. ff_h_pfp_backward_coefficient_difference_witness_operationleft + S (pfp_left_backward_coefficient_difference_witness_operation) = S ((S (pfp_index_backward_coefficient_difference_witness_operation)) * pfaa_left_c_backward_coefficient_difference)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_operationleft. pfaa_left_b_backward_coefficient_difference = ff_q_pfp_backward_coefficient_difference_witness_operationleft * S ((S (pfp_index_backward_coefficient_difference_witness_operation)) * pfaa_left_c_backward_coefficient_difference) + (pfp_left_backward_coefficient_difference_witness_operation))) /\ (((((exists ff_h_pfp_backward_coefficient_difference_witness_operationright. ff_h_pfp_backward_coefficient_difference_witness_operationright + S (pfp_right_backward_coefficient_difference_witness_operation) = S ((S (pfp_index_backward_coefficient_difference_witness_operation)) * pfaa_right_c_backward_coefficient_difference)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_operationright. pfaa_right_b_backward_coefficient_difference = ff_q_pfp_backward_coefficient_difference_witness_operationright * S ((S (pfp_index_backward_coefficient_difference_witness_operation)) * pfaa_right_c_backward_coefficient_difference) + (pfp_right_backward_coefficient_difference_witness_operation))) /\ (((((exists ff_h_pfp_backward_coefficient_difference_witness_operationtarget. ff_h_pfp_backward_coefficient_difference_witness_operationtarget + S (pfp_value_backward_coefficient_difference_witness_operation) = S ((S (pfp_index_backward_coefficient_difference_witness_operation)) * pfaa_sum_c_backward_coefficient_difference)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_operationtarget. pfaa_sum_b_backward_coefficient_difference = ff_q_pfp_backward_coefficient_difference_witness_operationtarget * S ((S (pfp_index_backward_coefficient_difference_witness_operation)) * pfaa_sum_c_backward_coefficient_difference) + (pfp_value_backward_coefficient_difference_witness_operation))) /\ ((((exists pfa_gap_backward_coefficient_difference_witness_operationoperationleft. pfa_gap_backward_coefficient_difference_witness_operationoperationleft + S (pfp_left_backward_coefficient_difference_witness_operation) = (p)) /\ (((exists pfa_gap_backward_coefficient_difference_witness_operationoperationright. pfa_gap_backward_coefficient_difference_witness_operationoperationright + S (pfp_right_backward_coefficient_difference_witness_operation) = (p)) /\ ((((exists pfa_gap_backward_coefficient_difference_witness_operationoperationresultbound. pfa_gap_backward_coefficient_difference_witness_operationoperationresultbound + S (pfp_value_backward_coefficient_difference_witness_operation) = (p)) /\ ((exists pfa_offset_left_backward_coefficient_difference_witness_operationoperationresultcongruence pfa_offset_right_backward_coefficient_difference_witness_operationoperationresultcongruence. ((pfp_left_backward_coefficient_difference_witness_operation) + (pfp_right_backward_coefficient_difference_witness_operation)) + (p) * pfa_offset_left_backward_coefficient_difference_witness_operationoperationresultcongruence = (pfp_value_backward_coefficient_difference_witness_operation) + (p) * pfa_offset_right_backward_coefficient_difference_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_backward_coefficient_difference_witness_output pfrep_left_backward_coefficient_difference_witness_output pfrep_right_backward_coefficient_difference_witness_output. ((exists pfrep_position_backward_coefficient_difference_witness_outputfirst. ((pfrep_position_backward_coefficient_difference_witness_outputfirst+S (pfrep_power_backward_coefficient_difference_witness_output)=(pfaa_length_backward_coefficient_difference)) /\ ((((exists ff_h_pfp_backward_coefficient_difference_witness_outputfirstentry. ff_h_pfp_backward_coefficient_difference_witness_outputfirstentry + S (pfrep_left_backward_coefficient_difference_witness_output) = S ((S (pfrep_position_backward_coefficient_difference_witness_outputfirst)) * pfaa_sum_c_backward_coefficient_difference)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_outputfirstentry. pfaa_sum_b_backward_coefficient_difference = ff_q_pfp_backward_coefficient_difference_witness_outputfirstentry * S ((S (pfrep_position_backward_coefficient_difference_witness_outputfirst)) * pfaa_sum_c_backward_coefficient_difference) + (pfrep_left_backward_coefficient_difference_witness_output)))))) \/ (((exists pfrep_gap_backward_coefficient_difference_witness_outputfirstoutside. pfrep_gap_backward_coefficient_difference_witness_outputfirstoutside+(pfaa_length_backward_coefficient_difference)=(pfrep_power_backward_coefficient_difference_witness_output)) /\ (((pfrep_left_backward_coefficient_difference_witness_output)=0))))) -> ((exists pfrep_position_backward_coefficient_difference_witness_outputsecond. ((pfrep_position_backward_coefficient_difference_witness_outputsecond+S (pfrep_power_backward_coefficient_difference_witness_output)=(Lu)) /\ ((((exists ff_h_pfp_backward_coefficient_difference_witness_outputsecondentry. ff_h_pfp_backward_coefficient_difference_witness_outputsecondentry + S (pfrep_right_backward_coefficient_difference_witness_output) = S ((S (pfrep_position_backward_coefficient_difference_witness_outputsecond)) * uc)) /\ exists ff_q_pfp_backward_coefficient_difference_witness_outputsecondentry. ub = ff_q_pfp_backward_coefficient_difference_witness_outputsecondentry * S ((S (pfrep_position_backward_coefficient_difference_witness_outputsecond)) * uc) + (pfrep_right_backward_coefficient_difference_witness_output)))))) \/ (((exists pfrep_gap_backward_coefficient_difference_witness_outputsecondoutside. pfrep_gap_backward_coefficient_difference_witness_outputsecondoutside+(Lu)=(pfrep_power_backward_coefficient_difference_witness_output)) /\ (((pfrep_right_backward_coefficient_difference_witness_output)=0))))) -> pfrep_left_backward_coefficient_difference_witness_output=pfrep_right_backward_coefficient_difference_witness_output))))))))))))) -> (((forall fom_index_pfp_backward_new_leftleft. (exists fom_gap_pfp_backward_new_leftleft_index_bound. fom_gap_pfp_backward_new_leftleft_index_bound + S (fom_index_pfp_backward_new_leftleft) = Lv) -> exists fom_value_pfp_backward_new_leftleft. ((((exists fom_beta_height_pfp_backward_new_leftleft_entry. fom_beta_height_pfp_backward_new_leftleft_entry + S (fom_value_pfp_backward_new_leftleft) = S ((S (fom_index_pfp_backward_new_leftleft)) * vc)) /\ exists fom_beta_quotient_pfp_backward_new_leftleft_entry. vb = fom_beta_quotient_pfp_backward_new_leftleft_entry * S ((S (fom_index_pfp_backward_new_leftleft)) * vc) + (fom_value_pfp_backward_new_leftleft))) /\ (exists fom_gap_pfp_backward_new_leftleft_value_bound. fom_gap_pfp_backward_new_leftleft_value_bound + S (fom_value_pfp_backward_new_leftleft) = p))) /\ (((forall fom_index_pfp_backward_new_leftright. (exists fom_gap_pfp_backward_new_leftright_index_bound. fom_gap_pfp_backward_new_leftright_index_bound + S (fom_index_pfp_backward_new_leftright) = La) -> exists fom_value_pfp_backward_new_leftright. ((((exists fom_beta_height_pfp_backward_new_leftright_entry. fom_beta_height_pfp_backward_new_leftright_entry + S (fom_value_pfp_backward_new_leftright) = S ((S (fom_index_pfp_backward_new_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_backward_new_leftright_entry. ab = fom_beta_quotient_pfp_backward_new_leftright_entry * S ((S (fom_index_pfp_backward_new_leftright)) * ac) + (fom_value_pfp_backward_new_leftright))) /\ (exists fom_gap_pfp_backward_new_leftright_value_bound. fom_gap_pfp_backward_new_leftright_value_bound + S (fom_value_pfp_backward_new_leftright) = p))) /\ (((((((Lv)=0 \/ (La)=0) /\ (((Lx)=0)))) \/ (((~((Lv)=0)) /\ (((~((La)=0)) /\ (((Lv)+(La)=S (Lx)))))))) /\ ((forall pfc_index_backward_new_leftcoefficients. (exists pfa_gap_backward_new_leftcoefficientsbound. pfa_gap_backward_new_leftcoefficientsbound + S (pfc_index_backward_new_leftcoefficients) = (Lx)) -> exists pfc_value_backward_new_leftcoefficients. ((((exists ff_h_pfp_backward_new_leftcoefficientsentry. ff_h_pfp_backward_new_leftcoefficientsentry + S (pfc_value_backward_new_leftcoefficients) = S ((S (pfc_index_backward_new_leftcoefficients)) * xc)) /\ exists ff_q_pfp_backward_new_leftcoefficientsentry. xb = ff_q_pfp_backward_new_leftcoefficientsentry * S ((S (pfc_index_backward_new_leftcoefficients)) * xc) + (pfc_value_backward_new_leftcoefficients))) /\ ((exists pfc_terms_code_backward_new_leftcoefficientscoefficient pfc_terms_scale_backward_new_leftcoefficientscoefficient pfc_natural_sum_backward_new_leftcoefficientscoefficient. ((forall pfc_index_backward_new_leftcoefficientscoefficientdiagonal. (exists pfa_gap_backward_new_leftcoefficientscoefficientdiagonalbound. pfa_gap_backward_new_leftcoefficientscoefficientdiagonalbound + S (pfc_index_backward_new_leftcoefficientscoefficientdiagonal) = (S (pfc_index_backward_new_leftcoefficients))) -> exists pfc_value_backward_new_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_backward_new_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_backward_new_leftcoefficientscoefficientdiagonalentry + S (pfc_value_backward_new_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_backward_new_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_new_leftcoefficientscoefficient)) /\ exists ff_q_pfp_backward_new_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_backward_new_leftcoefficientscoefficient = ff_q_pfp_backward_new_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_backward_new_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_new_leftcoefficientscoefficient) + (pfc_value_backward_new_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_backward_new_leftcoefficientscoefficientdiagonalterm pfc_left_backward_new_leftcoefficientscoefficientdiagonalterm pfc_right_backward_new_leftcoefficientscoefficientdiagonalterm. (((pfc_index_backward_new_leftcoefficientscoefficientdiagonal)+pfc_complement_backward_new_leftcoefficientscoefficientdiagonalterm=(pfc_index_backward_new_leftcoefficients)) /\ ((((((exists pfa_gap_backward_new_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_backward_new_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_backward_new_leftcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_backward_new_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_backward_new_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_backward_new_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_backward_new_leftcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_backward_new_leftcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_backward_new_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_backward_new_leftcoefficientscoefficientdiagonal)) * vc) + (pfc_left_backward_new_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_new_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_backward_new_leftcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_backward_new_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_backward_new_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_backward_new_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_backward_new_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_backward_new_leftcoefficientscoefficientdiagonalterm) = (La)) /\ ((((exists ff_h_pfp_backward_new_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_backward_new_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_backward_new_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_backward_new_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_backward_new_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_backward_new_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_backward_new_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_backward_new_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_new_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_backward_new_leftcoefficientscoefficientdiagonaltermrightoutside+(La)=(pfc_complement_backward_new_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_backward_new_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_backward_new_leftcoefficientscoefficientdiagonal)=pfc_left_backward_new_leftcoefficientscoefficientdiagonalterm*pfc_right_backward_new_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_backward_new_leftcoefficientscoefficientsum fs_v_pfc_backward_new_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_start. fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_backward_new_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_start. fs_u_pfc_backward_new_leftcoefficientscoefficientsum = fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_backward_new_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_backward_new_leftcoefficientscoefficient) = S ((S (S (pfc_index_backward_new_leftcoefficients))) * fs_v_pfc_backward_new_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_backward_new_leftcoefficientscoefficientsum = fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_backward_new_leftcoefficients))) * fs_v_pfc_backward_new_leftcoefficientscoefficientsum) + (pfc_natural_sum_backward_new_leftcoefficientscoefficient))) /\ forall fs_i_pfc_backward_new_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_backward_new_leftcoefficientscoefficientsum_body_steps = S (pfc_index_backward_new_leftcoefficients)) -> exists fs_a_pfc_backward_new_leftcoefficientscoefficientsum_body_steps fs_r_pfc_backward_new_leftcoefficientscoefficientsum_body_steps fs_s_pfc_backward_new_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_backward_new_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_new_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_new_leftcoefficientscoefficient)) /\ exists fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_backward_new_leftcoefficientscoefficient = fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_backward_new_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_new_leftcoefficientscoefficient) + (fs_a_pfc_backward_new_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_backward_new_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_new_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_new_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_backward_new_leftcoefficientscoefficientsum = fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_backward_new_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_new_leftcoefficientscoefficientsum) + (fs_r_pfc_backward_new_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_backward_new_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_backward_new_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_new_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_backward_new_leftcoefficientscoefficientsum = fs_q_pfc_backward_new_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_backward_new_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_new_leftcoefficientscoefficientsum) + (fs_s_pfc_backward_new_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_backward_new_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_backward_new_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_backward_new_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_backward_new_leftcoefficientscoefficientresiduebound. pfa_gap_backward_new_leftcoefficientscoefficientresiduebound + S (pfc_value_backward_new_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_backward_new_leftcoefficientscoefficientresiduecongruence pfa_offset_right_backward_new_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_backward_new_leftcoefficientscoefficient) + (p) * pfa_offset_left_backward_new_leftcoefficientscoefficientresiduecongruence = (pfc_value_backward_new_leftcoefficients) + (p) * pfa_offset_right_backward_new_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_backward_new_rightleft. (exists fom_gap_pfp_backward_new_rightleft_index_bound. fom_gap_pfp_backward_new_rightleft_index_bound + S (fom_index_pfp_backward_new_rightleft) = Lt) -> exists fom_value_pfp_backward_new_rightleft. ((((exists fom_beta_height_pfp_backward_new_rightleft_entry. fom_beta_height_pfp_backward_new_rightleft_entry + S (fom_value_pfp_backward_new_rightleft) = S ((S (fom_index_pfp_backward_new_rightleft)) * tc)) /\ exists fom_beta_quotient_pfp_backward_new_rightleft_entry. tb = fom_beta_quotient_pfp_backward_new_rightleft_entry * S ((S (fom_index_pfp_backward_new_rightleft)) * tc) + (fom_value_pfp_backward_new_rightleft))) /\ (exists fom_gap_pfp_backward_new_rightleft_value_bound. fom_gap_pfp_backward_new_rightleft_value_bound + S (fom_value_pfp_backward_new_rightleft) = p))) /\ (((forall fom_index_pfp_backward_new_rightright. (exists fom_gap_pfp_backward_new_rightright_index_bound. fom_gap_pfp_backward_new_rightright_index_bound + S (fom_index_pfp_backward_new_rightright) = Lb) -> exists fom_value_pfp_backward_new_rightright. ((((exists fom_beta_height_pfp_backward_new_rightright_entry. fom_beta_height_pfp_backward_new_rightright_entry + S (fom_value_pfp_backward_new_rightright) = S ((S (fom_index_pfp_backward_new_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_backward_new_rightright_entry. bb = fom_beta_quotient_pfp_backward_new_rightright_entry * S ((S (fom_index_pfp_backward_new_rightright)) * bc) + (fom_value_pfp_backward_new_rightright))) /\ (exists fom_gap_pfp_backward_new_rightright_value_bound. fom_gap_pfp_backward_new_rightright_value_bound + S (fom_value_pfp_backward_new_rightright) = p))) /\ (((((((Lt)=0 \/ (Lb)=0) /\ (((Ly)=0)))) \/ (((~((Lt)=0)) /\ (((~((Lb)=0)) /\ (((Lt)+(Lb)=S (Ly)))))))) /\ ((forall pfc_index_backward_new_rightcoefficients. (exists pfa_gap_backward_new_rightcoefficientsbound. pfa_gap_backward_new_rightcoefficientsbound + S (pfc_index_backward_new_rightcoefficients) = (Ly)) -> exists pfc_value_backward_new_rightcoefficients. ((((exists ff_h_pfp_backward_new_rightcoefficientsentry. ff_h_pfp_backward_new_rightcoefficientsentry + S (pfc_value_backward_new_rightcoefficients) = S ((S (pfc_index_backward_new_rightcoefficients)) * yc)) /\ exists ff_q_pfp_backward_new_rightcoefficientsentry. yb = ff_q_pfp_backward_new_rightcoefficientsentry * S ((S (pfc_index_backward_new_rightcoefficients)) * yc) + (pfc_value_backward_new_rightcoefficients))) /\ ((exists pfc_terms_code_backward_new_rightcoefficientscoefficient pfc_terms_scale_backward_new_rightcoefficientscoefficient pfc_natural_sum_backward_new_rightcoefficientscoefficient. ((forall pfc_index_backward_new_rightcoefficientscoefficientdiagonal. (exists pfa_gap_backward_new_rightcoefficientscoefficientdiagonalbound. pfa_gap_backward_new_rightcoefficientscoefficientdiagonalbound + S (pfc_index_backward_new_rightcoefficientscoefficientdiagonal) = (S (pfc_index_backward_new_rightcoefficients))) -> exists pfc_value_backward_new_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_backward_new_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_backward_new_rightcoefficientscoefficientdiagonalentry + S (pfc_value_backward_new_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_backward_new_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_new_rightcoefficientscoefficient)) /\ exists ff_q_pfp_backward_new_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_backward_new_rightcoefficientscoefficient = ff_q_pfp_backward_new_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_backward_new_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_new_rightcoefficientscoefficient) + (pfc_value_backward_new_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_backward_new_rightcoefficientscoefficientdiagonalterm pfc_left_backward_new_rightcoefficientscoefficientdiagonalterm pfc_right_backward_new_rightcoefficientscoefficientdiagonalterm. (((pfc_index_backward_new_rightcoefficientscoefficientdiagonal)+pfc_complement_backward_new_rightcoefficientscoefficientdiagonalterm=(pfc_index_backward_new_rightcoefficients)) /\ ((((((exists pfa_gap_backward_new_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_backward_new_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_backward_new_rightcoefficientscoefficientdiagonal) = (Lt)) /\ ((((exists ff_h_pfp_backward_new_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_backward_new_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_backward_new_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_backward_new_rightcoefficientscoefficientdiagonal)) * tc)) /\ exists ff_q_pfp_backward_new_rightcoefficientscoefficientdiagonaltermleftentry. tb = ff_q_pfp_backward_new_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_backward_new_rightcoefficientscoefficientdiagonal)) * tc) + (pfc_left_backward_new_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_new_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_backward_new_rightcoefficientscoefficientdiagonaltermleftoutside+(Lt)=(pfc_index_backward_new_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_backward_new_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_backward_new_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_backward_new_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_backward_new_rightcoefficientscoefficientdiagonalterm) = (Lb)) /\ ((((exists ff_h_pfp_backward_new_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_backward_new_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_backward_new_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_backward_new_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_backward_new_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_backward_new_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_backward_new_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_backward_new_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_new_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_backward_new_rightcoefficientscoefficientdiagonaltermrightoutside+(Lb)=(pfc_complement_backward_new_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_backward_new_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_backward_new_rightcoefficientscoefficientdiagonal)=pfc_left_backward_new_rightcoefficientscoefficientdiagonalterm*pfc_right_backward_new_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_backward_new_rightcoefficientscoefficientsum fs_v_pfc_backward_new_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_start. fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_backward_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_start. fs_u_pfc_backward_new_rightcoefficientscoefficientsum = fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_backward_new_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_backward_new_rightcoefficientscoefficient) = S ((S (S (pfc_index_backward_new_rightcoefficients))) * fs_v_pfc_backward_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_backward_new_rightcoefficientscoefficientsum = fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_backward_new_rightcoefficients))) * fs_v_pfc_backward_new_rightcoefficientscoefficientsum) + (pfc_natural_sum_backward_new_rightcoefficientscoefficient))) /\ forall fs_i_pfc_backward_new_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_backward_new_rightcoefficientscoefficientsum_body_steps = S (pfc_index_backward_new_rightcoefficients)) -> exists fs_a_pfc_backward_new_rightcoefficientscoefficientsum_body_steps fs_r_pfc_backward_new_rightcoefficientscoefficientsum_body_steps fs_s_pfc_backward_new_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_backward_new_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_new_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_new_rightcoefficientscoefficient)) /\ exists fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_backward_new_rightcoefficientscoefficient = fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_backward_new_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_new_rightcoefficientscoefficient) + (fs_a_pfc_backward_new_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_backward_new_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_backward_new_rightcoefficientscoefficientsum = fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_backward_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_new_rightcoefficientscoefficientsum) + (fs_r_pfc_backward_new_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_backward_new_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_backward_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_backward_new_rightcoefficientscoefficientsum = fs_q_pfc_backward_new_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_backward_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_new_rightcoefficientscoefficientsum) + (fs_s_pfc_backward_new_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_backward_new_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_backward_new_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_backward_new_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_backward_new_rightcoefficientscoefficientresiduebound. pfa_gap_backward_new_rightcoefficientscoefficientresiduebound + S (pfc_value_backward_new_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_backward_new_rightcoefficientscoefficientresiduecongruence pfa_offset_right_backward_new_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_backward_new_rightcoefficientscoefficient) + (p) * pfa_offset_left_backward_new_rightcoefficientscoefficientresiduecongruence = (pfc_value_backward_new_rightcoefficients) + (p) * pfa_offset_right_backward_new_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_backward_associated_productleft. (exists fom_gap_pfp_backward_associated_productleft_index_bound. fom_gap_pfp_backward_associated_productleft_index_bound + S (fom_index_pfp_backward_associated_productleft) = Lw) -> exists fom_value_pfp_backward_associated_productleft. ((((exists fom_beta_height_pfp_backward_associated_productleft_entry. fom_beta_height_pfp_backward_associated_productleft_entry + S (fom_value_pfp_backward_associated_productleft) = S ((S (fom_index_pfp_backward_associated_productleft)) * wc)) /\ exists fom_beta_quotient_pfp_backward_associated_productleft_entry. wb = fom_beta_quotient_pfp_backward_associated_productleft_entry * S ((S (fom_index_pfp_backward_associated_productleft)) * wc) + (fom_value_pfp_backward_associated_productleft))) /\ (exists fom_gap_pfp_backward_associated_productleft_value_bound. fom_gap_pfp_backward_associated_productleft_value_bound + S (fom_value_pfp_backward_associated_productleft) = p))) /\ (((forall fom_index_pfp_backward_associated_productright. (exists fom_gap_pfp_backward_associated_productright_index_bound. fom_gap_pfp_backward_associated_productright_index_bound + S (fom_index_pfp_backward_associated_productright) = Lb) -> exists fom_value_pfp_backward_associated_productright. ((((exists fom_beta_height_pfp_backward_associated_productright_entry. fom_beta_height_pfp_backward_associated_productright_entry + S (fom_value_pfp_backward_associated_productright) = S ((S (fom_index_pfp_backward_associated_productright)) * bc)) /\ exists fom_beta_quotient_pfp_backward_associated_productright_entry. bb = fom_beta_quotient_pfp_backward_associated_productright_entry * S ((S (fom_index_pfp_backward_associated_productright)) * bc) + (fom_value_pfp_backward_associated_productright))) /\ (exists fom_gap_pfp_backward_associated_productright_value_bound. fom_gap_pfp_backward_associated_productright_value_bound + S (fom_value_pfp_backward_associated_productright) = p))) /\ (((((((Lw)=0 \/ (Lb)=0) /\ (((Lz)=0)))) \/ (((~((Lw)=0)) /\ (((~((Lb)=0)) /\ (((Lw)+(Lb)=S (Lz)))))))) /\ ((forall pfc_index_backward_associated_productcoefficients. (exists pfa_gap_backward_associated_productcoefficientsbound. pfa_gap_backward_associated_productcoefficientsbound + S (pfc_index_backward_associated_productcoefficients) = (Lz)) -> exists pfc_value_backward_associated_productcoefficients. ((((exists ff_h_pfp_backward_associated_productcoefficientsentry. ff_h_pfp_backward_associated_productcoefficientsentry + S (pfc_value_backward_associated_productcoefficients) = S ((S (pfc_index_backward_associated_productcoefficients)) * zc)) /\ exists ff_q_pfp_backward_associated_productcoefficientsentry. zb = ff_q_pfp_backward_associated_productcoefficientsentry * S ((S (pfc_index_backward_associated_productcoefficients)) * zc) + (pfc_value_backward_associated_productcoefficients))) /\ ((exists pfc_terms_code_backward_associated_productcoefficientscoefficient pfc_terms_scale_backward_associated_productcoefficientscoefficient pfc_natural_sum_backward_associated_productcoefficientscoefficient. ((forall pfc_index_backward_associated_productcoefficientscoefficientdiagonal. (exists pfa_gap_backward_associated_productcoefficientscoefficientdiagonalbound. pfa_gap_backward_associated_productcoefficientscoefficientdiagonalbound + S (pfc_index_backward_associated_productcoefficientscoefficientdiagonal) = (S (pfc_index_backward_associated_productcoefficients))) -> exists pfc_value_backward_associated_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_backward_associated_productcoefficientscoefficientdiagonalentry. ff_h_pfp_backward_associated_productcoefficientscoefficientdiagonalentry + S (pfc_value_backward_associated_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_backward_associated_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_associated_productcoefficientscoefficient)) /\ exists ff_q_pfp_backward_associated_productcoefficientscoefficientdiagonalentry. pfc_terms_code_backward_associated_productcoefficientscoefficient = ff_q_pfp_backward_associated_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_backward_associated_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_associated_productcoefficientscoefficient) + (pfc_value_backward_associated_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_backward_associated_productcoefficientscoefficientdiagonalterm pfc_left_backward_associated_productcoefficientscoefficientdiagonalterm pfc_right_backward_associated_productcoefficientscoefficientdiagonalterm. (((pfc_index_backward_associated_productcoefficientscoefficientdiagonal)+pfc_complement_backward_associated_productcoefficientscoefficientdiagonalterm=(pfc_index_backward_associated_productcoefficients)) /\ ((((((exists pfa_gap_backward_associated_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_backward_associated_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_backward_associated_productcoefficientscoefficientdiagonal) = (Lw)) /\ ((((exists ff_h_pfp_backward_associated_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_backward_associated_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_backward_associated_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_backward_associated_productcoefficientscoefficientdiagonal)) * wc)) /\ exists ff_q_pfp_backward_associated_productcoefficientscoefficientdiagonaltermleftentry. wb = ff_q_pfp_backward_associated_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_backward_associated_productcoefficientscoefficientdiagonal)) * wc) + (pfc_left_backward_associated_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_associated_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_backward_associated_productcoefficientscoefficientdiagonaltermleftoutside+(Lw)=(pfc_index_backward_associated_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_backward_associated_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_backward_associated_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_backward_associated_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_backward_associated_productcoefficientscoefficientdiagonalterm) = (Lb)) /\ ((((exists ff_h_pfp_backward_associated_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_backward_associated_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_backward_associated_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_backward_associated_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_backward_associated_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_backward_associated_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_backward_associated_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_backward_associated_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_associated_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_backward_associated_productcoefficientscoefficientdiagonaltermrightoutside+(Lb)=(pfc_complement_backward_associated_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_backward_associated_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_backward_associated_productcoefficientscoefficientdiagonal)=pfc_left_backward_associated_productcoefficientscoefficientdiagonalterm*pfc_right_backward_associated_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_backward_associated_productcoefficientscoefficientsum fs_v_pfc_backward_associated_productcoefficientscoefficientsum. ((((exists fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_start. fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_backward_associated_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_start. fs_u_pfc_backward_associated_productcoefficientscoefficientsum = fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_backward_associated_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_backward_associated_productcoefficientscoefficient) = S ((S (S (pfc_index_backward_associated_productcoefficients))) * fs_v_pfc_backward_associated_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_backward_associated_productcoefficientscoefficientsum = fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_backward_associated_productcoefficients))) * fs_v_pfc_backward_associated_productcoefficientscoefficientsum) + (pfc_natural_sum_backward_associated_productcoefficientscoefficient))) /\ forall fs_i_pfc_backward_associated_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_backward_associated_productcoefficientscoefficientsum_body_steps = S (pfc_index_backward_associated_productcoefficients)) -> exists fs_a_pfc_backward_associated_productcoefficientscoefficientsum_body_steps fs_r_pfc_backward_associated_productcoefficientscoefficientsum_body_steps fs_s_pfc_backward_associated_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_backward_associated_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_associated_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_associated_productcoefficientscoefficient)) /\ exists fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_backward_associated_productcoefficientscoefficient = fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_backward_associated_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_associated_productcoefficientscoefficient) + (fs_a_pfc_backward_associated_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_backward_associated_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_associated_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_associated_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_backward_associated_productcoefficientscoefficientsum = fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_backward_associated_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_associated_productcoefficientscoefficientsum) + (fs_r_pfc_backward_associated_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_backward_associated_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_backward_associated_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_associated_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_backward_associated_productcoefficientscoefficientsum = fs_q_pfc_backward_associated_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_backward_associated_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_associated_productcoefficientscoefficientsum) + (fs_s_pfc_backward_associated_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_backward_associated_productcoefficientscoefficientsum_body_steps = fs_r_pfc_backward_associated_productcoefficientscoefficientsum_body_steps + fs_a_pfc_backward_associated_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_backward_associated_productcoefficientscoefficientresiduebound. pfa_gap_backward_associated_productcoefficientscoefficientresiduebound + S (pfc_value_backward_associated_productcoefficients) = (p)) /\ ((exists pfa_offset_left_backward_associated_productcoefficientscoefficientresiduecongruence pfa_offset_right_backward_associated_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_backward_associated_productcoefficientscoefficient) + (p) * pfa_offset_left_backward_associated_productcoefficientscoefficientresiduecongruence = (pfc_value_backward_associated_productcoefficients) + (p) * pfa_offset_right_backward_associated_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_backward_distributed_productleft. (exists fom_gap_pfp_backward_distributed_productleft_index_bound. fom_gap_pfp_backward_distributed_productleft_index_bound + S (fom_index_pfp_backward_distributed_productleft) = Lv) -> exists fom_value_pfp_backward_distributed_productleft. ((((exists fom_beta_height_pfp_backward_distributed_productleft_entry. fom_beta_height_pfp_backward_distributed_productleft_entry + S (fom_value_pfp_backward_distributed_productleft) = S ((S (fom_index_pfp_backward_distributed_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_backward_distributed_productleft_entry. vb = fom_beta_quotient_pfp_backward_distributed_productleft_entry * S ((S (fom_index_pfp_backward_distributed_productleft)) * vc) + (fom_value_pfp_backward_distributed_productleft))) /\ (exists fom_gap_pfp_backward_distributed_productleft_value_bound. fom_gap_pfp_backward_distributed_productleft_value_bound + S (fom_value_pfp_backward_distributed_productleft) = p))) /\ (((forall fom_index_pfp_backward_distributed_productright. (exists fom_gap_pfp_backward_distributed_productright_index_bound. fom_gap_pfp_backward_distributed_productright_index_bound + S (fom_index_pfp_backward_distributed_productright) = Lp) -> exists fom_value_pfp_backward_distributed_productright. ((((exists fom_beta_height_pfp_backward_distributed_productright_entry. fom_beta_height_pfp_backward_distributed_productright_entry + S (fom_value_pfp_backward_distributed_productright) = S ((S (fom_index_pfp_backward_distributed_productright)) * pc)) /\ exists fom_beta_quotient_pfp_backward_distributed_productright_entry. pb = fom_beta_quotient_pfp_backward_distributed_productright_entry * S ((S (fom_index_pfp_backward_distributed_productright)) * pc) + (fom_value_pfp_backward_distributed_productright))) /\ (exists fom_gap_pfp_backward_distributed_productright_value_bound. fom_gap_pfp_backward_distributed_productright_value_bound + S (fom_value_pfp_backward_distributed_productright) = p))) /\ (((((((Lv)=0 \/ (Lp)=0) /\ (((Lh)=0)))) \/ (((~((Lv)=0)) /\ (((~((Lp)=0)) /\ (((Lv)+(Lp)=S (Lh)))))))) /\ ((forall pfc_index_backward_distributed_productcoefficients. (exists pfa_gap_backward_distributed_productcoefficientsbound. pfa_gap_backward_distributed_productcoefficientsbound + S (pfc_index_backward_distributed_productcoefficients) = (Lh)) -> exists pfc_value_backward_distributed_productcoefficients. ((((exists ff_h_pfp_backward_distributed_productcoefficientsentry. ff_h_pfp_backward_distributed_productcoefficientsentry + S (pfc_value_backward_distributed_productcoefficients) = S ((S (pfc_index_backward_distributed_productcoefficients)) * hc)) /\ exists ff_q_pfp_backward_distributed_productcoefficientsentry. hb = ff_q_pfp_backward_distributed_productcoefficientsentry * S ((S (pfc_index_backward_distributed_productcoefficients)) * hc) + (pfc_value_backward_distributed_productcoefficients))) /\ ((exists pfc_terms_code_backward_distributed_productcoefficientscoefficient pfc_terms_scale_backward_distributed_productcoefficientscoefficient pfc_natural_sum_backward_distributed_productcoefficientscoefficient. ((forall pfc_index_backward_distributed_productcoefficientscoefficientdiagonal. (exists pfa_gap_backward_distributed_productcoefficientscoefficientdiagonalbound. pfa_gap_backward_distributed_productcoefficientscoefficientdiagonalbound + S (pfc_index_backward_distributed_productcoefficientscoefficientdiagonal) = (S (pfc_index_backward_distributed_productcoefficients))) -> exists pfc_value_backward_distributed_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_backward_distributed_productcoefficientscoefficientdiagonalentry. ff_h_pfp_backward_distributed_productcoefficientscoefficientdiagonalentry + S (pfc_value_backward_distributed_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_backward_distributed_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_distributed_productcoefficientscoefficient)) /\ exists ff_q_pfp_backward_distributed_productcoefficientscoefficientdiagonalentry. pfc_terms_code_backward_distributed_productcoefficientscoefficient = ff_q_pfp_backward_distributed_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_backward_distributed_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_backward_distributed_productcoefficientscoefficient) + (pfc_value_backward_distributed_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_backward_distributed_productcoefficientscoefficientdiagonalterm pfc_left_backward_distributed_productcoefficientscoefficientdiagonalterm pfc_right_backward_distributed_productcoefficientscoefficientdiagonalterm. (((pfc_index_backward_distributed_productcoefficientscoefficientdiagonal)+pfc_complement_backward_distributed_productcoefficientscoefficientdiagonalterm=(pfc_index_backward_distributed_productcoefficients)) /\ ((((((exists pfa_gap_backward_distributed_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_backward_distributed_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_backward_distributed_productcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_backward_distributed_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_backward_distributed_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_backward_distributed_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_backward_distributed_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_backward_distributed_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_backward_distributed_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_backward_distributed_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_backward_distributed_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_distributed_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_backward_distributed_productcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_backward_distributed_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_backward_distributed_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_backward_distributed_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_backward_distributed_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_backward_distributed_productcoefficientscoefficientdiagonalterm) = (Lp)) /\ ((((exists ff_h_pfp_backward_distributed_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_backward_distributed_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_backward_distributed_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_backward_distributed_productcoefficientscoefficientdiagonalterm)) * pc)) /\ exists ff_q_pfp_backward_distributed_productcoefficientscoefficientdiagonaltermrightentry. pb = ff_q_pfp_backward_distributed_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_backward_distributed_productcoefficientscoefficientdiagonalterm)) * pc) + (pfc_right_backward_distributed_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_backward_distributed_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_backward_distributed_productcoefficientscoefficientdiagonaltermrightoutside+(Lp)=(pfc_complement_backward_distributed_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_backward_distributed_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_backward_distributed_productcoefficientscoefficientdiagonal)=pfc_left_backward_distributed_productcoefficientscoefficientdiagonalterm*pfc_right_backward_distributed_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_backward_distributed_productcoefficientscoefficientsum fs_v_pfc_backward_distributed_productcoefficientscoefficientsum. ((((exists fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_start. fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_backward_distributed_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_start. fs_u_pfc_backward_distributed_productcoefficientscoefficientsum = fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_backward_distributed_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_backward_distributed_productcoefficientscoefficient) = S ((S (S (pfc_index_backward_distributed_productcoefficients))) * fs_v_pfc_backward_distributed_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_backward_distributed_productcoefficientscoefficientsum = fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_backward_distributed_productcoefficients))) * fs_v_pfc_backward_distributed_productcoefficientscoefficientsum) + (pfc_natural_sum_backward_distributed_productcoefficientscoefficient))) /\ forall fs_i_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps = S (pfc_index_backward_distributed_productcoefficients)) -> exists fs_a_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps fs_r_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps fs_s_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_distributed_productcoefficientscoefficient)) /\ exists fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_backward_distributed_productcoefficientscoefficient = fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_backward_distributed_productcoefficientscoefficient) + (fs_a_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_distributed_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_backward_distributed_productcoefficientscoefficientsum = fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_distributed_productcoefficientscoefficientsum) + (fs_r_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_distributed_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_backward_distributed_productcoefficientscoefficientsum = fs_q_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_backward_distributed_productcoefficientscoefficientsum) + (fs_s_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps = fs_r_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps + fs_a_pfc_backward_distributed_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_backward_distributed_productcoefficientscoefficientresiduebound. pfa_gap_backward_distributed_productcoefficientscoefficientresiduebound + S (pfc_value_backward_distributed_productcoefficients) = (p)) /\ ((exists pfa_offset_left_backward_distributed_productcoefficientscoefficientresiduecongruence pfa_offset_right_backward_distributed_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_backward_distributed_productcoefficientscoefficient) + (p) * pfa_offset_left_backward_distributed_productcoefficientscoefficientresiduecongruence = (pfc_value_backward_distributed_productcoefficients) + (p) * pfa_offset_right_backward_distributed_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_backward_result_left_bounded. (exists fom_gap_pfp_backward_result_left_bounded_index_bound. fom_gap_pfp_backward_result_left_bounded_index_bound + S (fom_index_pfp_backward_result_left_bounded) = Lx) -> exists fom_value_pfp_backward_result_left_bounded. ((((exists fom_beta_height_pfp_backward_result_left_bounded_entry. fom_beta_height_pfp_backward_result_left_bounded_entry + S (fom_value_pfp_backward_result_left_bounded) = S ((S (fom_index_pfp_backward_result_left_bounded)) * xc)) /\ exists fom_beta_quotient_pfp_backward_result_left_bounded_entry. xb = fom_beta_quotient_pfp_backward_result_left_bounded_entry * S ((S (fom_index_pfp_backward_result_left_bounded)) * xc) + (fom_value_pfp_backward_result_left_bounded))) /\ (exists fom_gap_pfp_backward_result_left_bounded_value_bound. fom_gap_pfp_backward_result_left_bounded_value_bound + S (fom_value_pfp_backward_result_left_bounded) = p))) /\ (((forall fom_index_pfp_backward_result_right_bounded. (exists fom_gap_pfp_backward_result_right_bounded_index_bound. fom_gap_pfp_backward_result_right_bounded_index_bound + S (fom_index_pfp_backward_result_right_bounded) = Ly) -> exists fom_value_pfp_backward_result_right_bounded. ((((exists fom_beta_height_pfp_backward_result_right_bounded_entry. fom_beta_height_pfp_backward_result_right_bounded_entry + S (fom_value_pfp_backward_result_right_bounded) = S ((S (fom_index_pfp_backward_result_right_bounded)) * yc)) /\ exists fom_beta_quotient_pfp_backward_result_right_bounded_entry. yb = fom_beta_quotient_pfp_backward_result_right_bounded_entry * S ((S (fom_index_pfp_backward_result_right_bounded)) * yc) + (fom_value_pfp_backward_result_right_bounded))) /\ (exists fom_gap_pfp_backward_result_right_bounded_value_bound. fom_gap_pfp_backward_result_right_bounded_value_bound + S (fom_value_pfp_backward_result_right_bounded) = p))) /\ (((forall fom_index_pfp_backward_result_result_bounded. (exists fom_gap_pfp_backward_result_result_bounded_index_bound. fom_gap_pfp_backward_result_result_bounded_index_bound + S (fom_index_pfp_backward_result_result_bounded) = Lg) -> exists fom_value_pfp_backward_result_result_bounded. ((((exists fom_beta_height_pfp_backward_result_result_bounded_entry. fom_beta_height_pfp_backward_result_result_bounded_entry + S (fom_value_pfp_backward_result_result_bounded) = S ((S (fom_index_pfp_backward_result_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_backward_result_result_bounded_entry. gb = fom_beta_quotient_pfp_backward_result_result_bounded_entry * S ((S (fom_index_pfp_backward_result_result_bounded)) * gc) + (fom_value_pfp_backward_result_result_bounded))) /\ (exists fom_gap_pfp_backward_result_result_bounded_value_bound. fom_gap_pfp_backward_result_result_bounded_value_bound + S (fom_value_pfp_backward_result_result_bounded) = p))) /\ ((exists pfaa_left_b_backward_result pfaa_left_c_backward_result pfaa_right_b_backward_result pfaa_right_c_backward_result pfaa_sum_b_backward_result pfaa_sum_c_backward_result pfaa_length_backward_result. ((((forall pfrep_power_backward_result_witness_common_left pfrep_left_backward_result_witness_common_left pfrep_right_backward_result_witness_common_left. ((exists pfrep_position_backward_result_witness_common_leftfirst. ((pfrep_position_backward_result_witness_common_leftfirst+S (pfrep_power_backward_result_witness_common_left)=(Lx)) /\ ((((exists ff_h_pfp_backward_result_witness_common_leftfirstentry. ff_h_pfp_backward_result_witness_common_leftfirstentry + S (pfrep_left_backward_result_witness_common_left) = S ((S (pfrep_position_backward_result_witness_common_leftfirst)) * xc)) /\ exists ff_q_pfp_backward_result_witness_common_leftfirstentry. xb = ff_q_pfp_backward_result_witness_common_leftfirstentry * S ((S (pfrep_position_backward_result_witness_common_leftfirst)) * xc) + (pfrep_left_backward_result_witness_common_left)))))) \/ (((exists pfrep_gap_backward_result_witness_common_leftfirstoutside. pfrep_gap_backward_result_witness_common_leftfirstoutside+(Lx)=(pfrep_power_backward_result_witness_common_left)) /\ (((pfrep_left_backward_result_witness_common_left)=0))))) -> ((exists pfrep_position_backward_result_witness_common_leftsecond. ((pfrep_position_backward_result_witness_common_leftsecond+S (pfrep_power_backward_result_witness_common_left)=(pfaa_length_backward_result)) /\ ((((exists ff_h_pfp_backward_result_witness_common_leftsecondentry. ff_h_pfp_backward_result_witness_common_leftsecondentry + S (pfrep_right_backward_result_witness_common_left) = S ((S (pfrep_position_backward_result_witness_common_leftsecond)) * pfaa_left_c_backward_result)) /\ exists ff_q_pfp_backward_result_witness_common_leftsecondentry. pfaa_left_b_backward_result = ff_q_pfp_backward_result_witness_common_leftsecondentry * S ((S (pfrep_position_backward_result_witness_common_leftsecond)) * pfaa_left_c_backward_result) + (pfrep_right_backward_result_witness_common_left)))))) \/ (((exists pfrep_gap_backward_result_witness_common_leftsecondoutside. pfrep_gap_backward_result_witness_common_leftsecondoutside+(pfaa_length_backward_result)=(pfrep_power_backward_result_witness_common_left)) /\ (((pfrep_right_backward_result_witness_common_left)=0))))) -> pfrep_left_backward_result_witness_common_left=pfrep_right_backward_result_witness_common_left) /\ ((forall pfrep_power_backward_result_witness_common_right pfrep_left_backward_result_witness_common_right pfrep_right_backward_result_witness_common_right. ((exists pfrep_position_backward_result_witness_common_rightfirst. ((pfrep_position_backward_result_witness_common_rightfirst+S (pfrep_power_backward_result_witness_common_right)=(Ly)) /\ ((((exists ff_h_pfp_backward_result_witness_common_rightfirstentry. ff_h_pfp_backward_result_witness_common_rightfirstentry + S (pfrep_left_backward_result_witness_common_right) = S ((S (pfrep_position_backward_result_witness_common_rightfirst)) * yc)) /\ exists ff_q_pfp_backward_result_witness_common_rightfirstentry. yb = ff_q_pfp_backward_result_witness_common_rightfirstentry * S ((S (pfrep_position_backward_result_witness_common_rightfirst)) * yc) + (pfrep_left_backward_result_witness_common_right)))))) \/ (((exists pfrep_gap_backward_result_witness_common_rightfirstoutside. pfrep_gap_backward_result_witness_common_rightfirstoutside+(Ly)=(pfrep_power_backward_result_witness_common_right)) /\ (((pfrep_left_backward_result_witness_common_right)=0))))) -> ((exists pfrep_position_backward_result_witness_common_rightsecond. ((pfrep_position_backward_result_witness_common_rightsecond+S (pfrep_power_backward_result_witness_common_right)=(pfaa_length_backward_result)) /\ ((((exists ff_h_pfp_backward_result_witness_common_rightsecondentry. ff_h_pfp_backward_result_witness_common_rightsecondentry + S (pfrep_right_backward_result_witness_common_right) = S ((S (pfrep_position_backward_result_witness_common_rightsecond)) * pfaa_right_c_backward_result)) /\ exists ff_q_pfp_backward_result_witness_common_rightsecondentry. pfaa_right_b_backward_result = ff_q_pfp_backward_result_witness_common_rightsecondentry * S ((S (pfrep_position_backward_result_witness_common_rightsecond)) * pfaa_right_c_backward_result) + (pfrep_right_backward_result_witness_common_right)))))) \/ (((exists pfrep_gap_backward_result_witness_common_rightsecondoutside. pfrep_gap_backward_result_witness_common_rightsecondoutside+(pfaa_length_backward_result)=(pfrep_power_backward_result_witness_common_right)) /\ (((pfrep_right_backward_result_witness_common_right)=0))))) -> pfrep_left_backward_result_witness_common_right=pfrep_right_backward_result_witness_common_right)))) /\ (((forall pfp_index_backward_result_witness_operation. (exists pfa_gap_backward_result_witness_operationindex. pfa_gap_backward_result_witness_operationindex + S (pfp_index_backward_result_witness_operation) = (pfaa_length_backward_result)) -> exists pfp_left_backward_result_witness_operation pfp_right_backward_result_witness_operation pfp_value_backward_result_witness_operation. ((((exists ff_h_pfp_backward_result_witness_operationleft. ff_h_pfp_backward_result_witness_operationleft + S (pfp_left_backward_result_witness_operation) = S ((S (pfp_index_backward_result_witness_operation)) * pfaa_left_c_backward_result)) /\ exists ff_q_pfp_backward_result_witness_operationleft. pfaa_left_b_backward_result = ff_q_pfp_backward_result_witness_operationleft * S ((S (pfp_index_backward_result_witness_operation)) * pfaa_left_c_backward_result) + (pfp_left_backward_result_witness_operation))) /\ (((((exists ff_h_pfp_backward_result_witness_operationright. ff_h_pfp_backward_result_witness_operationright + S (pfp_right_backward_result_witness_operation) = S ((S (pfp_index_backward_result_witness_operation)) * pfaa_right_c_backward_result)) /\ exists ff_q_pfp_backward_result_witness_operationright. pfaa_right_b_backward_result = ff_q_pfp_backward_result_witness_operationright * S ((S (pfp_index_backward_result_witness_operation)) * pfaa_right_c_backward_result) + (pfp_right_backward_result_witness_operation))) /\ (((((exists ff_h_pfp_backward_result_witness_operationtarget. ff_h_pfp_backward_result_witness_operationtarget + S (pfp_value_backward_result_witness_operation) = S ((S (pfp_index_backward_result_witness_operation)) * pfaa_sum_c_backward_result)) /\ exists ff_q_pfp_backward_result_witness_operationtarget. pfaa_sum_b_backward_result = ff_q_pfp_backward_result_witness_operationtarget * S ((S (pfp_index_backward_result_witness_operation)) * pfaa_sum_c_backward_result) + (pfp_value_backward_result_witness_operation))) /\ ((((exists pfa_gap_backward_result_witness_operationoperationleft. pfa_gap_backward_result_witness_operationoperationleft + S (pfp_left_backward_result_witness_operation) = (p)) /\ (((exists pfa_gap_backward_result_witness_operationoperationright. pfa_gap_backward_result_witness_operationoperationright + S (pfp_right_backward_result_witness_operation) = (p)) /\ ((((exists pfa_gap_backward_result_witness_operationoperationresultbound. pfa_gap_backward_result_witness_operationoperationresultbound + S (pfp_value_backward_result_witness_operation) = (p)) /\ ((exists pfa_offset_left_backward_result_witness_operationoperationresultcongruence pfa_offset_right_backward_result_witness_operationoperationresultcongruence. ((pfp_left_backward_result_witness_operation) + (pfp_right_backward_result_witness_operation)) + (p) * pfa_offset_left_backward_result_witness_operationoperationresultcongruence = (pfp_value_backward_result_witness_operation) + (p) * pfa_offset_right_backward_result_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_backward_result_witness_output pfrep_left_backward_result_witness_output pfrep_right_backward_result_witness_output. ((exists pfrep_position_backward_result_witness_outputfirst. ((pfrep_position_backward_result_witness_outputfirst+S (pfrep_power_backward_result_witness_output)=(pfaa_length_backward_result)) /\ ((((exists ff_h_pfp_backward_result_witness_outputfirstentry. ff_h_pfp_backward_result_witness_outputfirstentry + S (pfrep_left_backward_result_witness_output) = S ((S (pfrep_position_backward_result_witness_outputfirst)) * pfaa_sum_c_backward_result)) /\ exists ff_q_pfp_backward_result_witness_outputfirstentry. pfaa_sum_b_backward_result = ff_q_pfp_backward_result_witness_outputfirstentry * S ((S (pfrep_position_backward_result_witness_outputfirst)) * pfaa_sum_c_backward_result) + (pfrep_left_backward_result_witness_output)))))) \/ (((exists pfrep_gap_backward_result_witness_outputfirstoutside. pfrep_gap_backward_result_witness_outputfirstoutside+(pfaa_length_backward_result)=(pfrep_power_backward_result_witness_output)) /\ (((pfrep_left_backward_result_witness_output)=0))))) -> ((exists pfrep_position_backward_result_witness_outputsecond. ((pfrep_position_backward_result_witness_outputsecond+S (pfrep_power_backward_result_witness_output)=(Lg)) /\ ((((exists ff_h_pfp_backward_result_witness_outputsecondentry. ff_h_pfp_backward_result_witness_outputsecondentry + S (pfrep_right_backward_result_witness_output) = S ((S (pfrep_position_backward_result_witness_outputsecond)) * gc)) /\ exists ff_q_pfp_backward_result_witness_outputsecondentry. gb = ff_q_pfp_backward_result_witness_outputsecondentry * S ((S (pfrep_position_backward_result_witness_outputsecond)) * gc) + (pfrep_right_backward_result_witness_output)))))) \/ (((exists pfrep_gap_backward_result_witness_outputsecondoutside. pfrep_gap_backward_result_witness_outputsecondoutside+(Lg)=(pfrep_power_backward_result_witness_output)) /\ (((pfrep_right_backward_result_witness_output)=0))))) -> pfrep_left_backward_result_witness_output=pfrep_right_backward_result_witness_output)))))))))))))