prime_field_polynomial_convolution_associativity_append_step

forall p ab ac L bb bc M pb pc N cb cc J q0b q0c K0 r0b r0c U0 s0b s0c V0 c db dc q1b q1c K1 r1b r1c U1 s1b s1c V1. (~((p) = 1) /\ forall pfa_factor_left_append_step_prime pfa_factor_right_append_step_prime. (p) = pfa_factor_left_append_step_prime * pfa_factor_right_append_step_prime -> pfa_factor_left_append_step_prime = 1 \/ pfa_factor_right_append_step_prime = 1) -> (((forall fom_index_pfp_append_step_ABleft. (exists fom_gap_pfp_append_step_ABleft_index_bound. fom_gap_pfp_append_step_ABleft_index_bound + S (fom_index_pfp_append_step_ABleft) = L) -> exists fom_value_pfp_append_step_ABleft. ((((exists fom_beta_height_pfp_append_step_ABleft_entry. fom_beta_height_pfp_append_step_ABleft_entry + S (fom_value_pfp_append_step_ABleft) = S ((S (fom_index_pfp_append_step_ABleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_step_ABleft_entry. ab = fom_beta_quotient_pfp_append_step_ABleft_entry * S ((S (fom_index_pfp_append_step_ABleft)) * ac) + (fom_value_pfp_append_step_ABleft))) /\ (exists fom_gap_pfp_append_step_ABleft_value_bound. fom_gap_pfp_append_step_ABleft_value_bound + S (fom_value_pfp_append_step_ABleft) = p))) /\ (((forall fom_index_pfp_append_step_ABright. (exists fom_gap_pfp_append_step_ABright_index_bound. fom_gap_pfp_append_step_ABright_index_bound + S (fom_index_pfp_append_step_ABright) = M) -> exists fom_value_pfp_append_step_ABright. ((((exists fom_beta_height_pfp_append_step_ABright_entry. fom_beta_height_pfp_append_step_ABright_entry + S (fom_value_pfp_append_step_ABright) = S ((S (fom_index_pfp_append_step_ABright)) * bc)) /\ exists fom_beta_quotient_pfp_append_step_ABright_entry. bb = fom_beta_quotient_pfp_append_step_ABright_entry * S ((S (fom_index_pfp_append_step_ABright)) * bc) + (fom_value_pfp_append_step_ABright))) /\ (exists fom_gap_pfp_append_step_ABright_value_bound. fom_gap_pfp_append_step_ABright_value_bound + S (fom_value_pfp_append_step_ABright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_append_step_ABcoefficients. (exists pfa_gap_append_step_ABcoefficientsbound. pfa_gap_append_step_ABcoefficientsbound + S (pfc_index_append_step_ABcoefficients) = (N)) -> exists pfc_value_append_step_ABcoefficients. ((((exists ff_h_pfp_append_step_ABcoefficientsentry. ff_h_pfp_append_step_ABcoefficientsentry + S (pfc_value_append_step_ABcoefficients) = S ((S (pfc_index_append_step_ABcoefficients)) * pc)) /\ exists ff_q_pfp_append_step_ABcoefficientsentry. pb = ff_q_pfp_append_step_ABcoefficientsentry * S ((S (pfc_index_append_step_ABcoefficients)) * pc) + (pfc_value_append_step_ABcoefficients))) /\ ((exists pfc_terms_code_append_step_ABcoefficientscoefficient pfc_terms_scale_append_step_ABcoefficientscoefficient pfc_natural_sum_append_step_ABcoefficientscoefficient. ((forall pfc_index_append_step_ABcoefficientscoefficientdiagonal. (exists pfa_gap_append_step_ABcoefficientscoefficientdiagonalbound. pfa_gap_append_step_ABcoefficientscoefficientdiagonalbound + S (pfc_index_append_step_ABcoefficientscoefficientdiagonal) = (S (pfc_index_append_step_ABcoefficients))) -> exists pfc_value_append_step_ABcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonalentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonalentry + S (pfc_value_append_step_ABcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_ABcoefficientscoefficient)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonalentry. pfc_terms_code_append_step_ABcoefficientscoefficient = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_ABcoefficientscoefficient) + (pfc_value_append_step_ABcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm pfc_left_append_step_ABcoefficientscoefficientdiagonalterm pfc_right_append_step_ABcoefficientscoefficientdiagonalterm. (((pfc_index_append_step_ABcoefficientscoefficientdiagonal)+pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm=(pfc_index_append_step_ABcoefficients)) /\ ((((((exists pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_ABcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_step_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_step_ABcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_ABcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_append_step_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_ABcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_ABcoefficientscoefficientdiagonal)=pfc_left_append_step_ABcoefficientscoefficientdiagonalterm*pfc_right_append_step_ABcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_ABcoefficientscoefficientsum fs_v_pfc_append_step_ABcoefficientscoefficientsum. ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_start. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_start. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_ABcoefficientscoefficient) = S ((S (S (pfc_index_append_step_ABcoefficients))) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_ABcoefficients))) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (pfc_natural_sum_append_step_ABcoefficientscoefficient))) /\ forall fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_ABcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_ABcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps = S (pfc_index_append_step_ABcoefficients)) -> exists fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_ABcoefficientscoefficient)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_ABcoefficientscoefficient = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_ABcoefficientscoefficient) + (fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps = fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps + fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_ABcoefficientscoefficientresiduebound. pfa_gap_append_step_ABcoefficientscoefficientresiduebound + S (pfc_value_append_step_ABcoefficients) = (p)) /\ ((exists pfa_offset_left_append_step_ABcoefficientscoefficientresiduecongruence pfa_offset_right_append_step_ABcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_ABcoefficientscoefficient) + (p) * pfa_offset_left_append_step_ABcoefficientscoefficientresiduecongruence = (pfc_value_append_step_ABcoefficients) + (p) * pfa_offset_right_append_step_ABcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_Q0left. (exists fom_gap_pfp_append_step_Q0left_index_bound. fom_gap_pfp_append_step_Q0left_index_bound + S (fom_index_pfp_append_step_Q0left) = M) -> exists fom_value_pfp_append_step_Q0left. ((((exists fom_beta_height_pfp_append_step_Q0left_entry. fom_beta_height_pfp_append_step_Q0left_entry + S (fom_value_pfp_append_step_Q0left) = S ((S (fom_index_pfp_append_step_Q0left)) * bc)) /\ exists fom_beta_quotient_pfp_append_step_Q0left_entry. bb = fom_beta_quotient_pfp_append_step_Q0left_entry * S ((S (fom_index_pfp_append_step_Q0left)) * bc) + (fom_value_pfp_append_step_Q0left))) /\ (exists fom_gap_pfp_append_step_Q0left_value_bound. fom_gap_pfp_append_step_Q0left_value_bound + S (fom_value_pfp_append_step_Q0left) = p))) /\ (((forall fom_index_pfp_append_step_Q0right. (exists fom_gap_pfp_append_step_Q0right_index_bound. fom_gap_pfp_append_step_Q0right_index_bound + S (fom_index_pfp_append_step_Q0right) = J) -> exists fom_value_pfp_append_step_Q0right. ((((exists fom_beta_height_pfp_append_step_Q0right_entry. fom_beta_height_pfp_append_step_Q0right_entry + S (fom_value_pfp_append_step_Q0right) = S ((S (fom_index_pfp_append_step_Q0right)) * cc)) /\ exists fom_beta_quotient_pfp_append_step_Q0right_entry. cb = fom_beta_quotient_pfp_append_step_Q0right_entry * S ((S (fom_index_pfp_append_step_Q0right)) * cc) + (fom_value_pfp_append_step_Q0right))) /\ (exists fom_gap_pfp_append_step_Q0right_value_bound. fom_gap_pfp_append_step_Q0right_value_bound + S (fom_value_pfp_append_step_Q0right) = p))) /\ (((((((M)=0 \/ (J)=0) /\ (((K0)=0)))) \/ (((~((M)=0)) /\ (((~((J)=0)) /\ (((M)+(J)=S (K0)))))))) /\ ((forall pfc_index_append_step_Q0coefficients. (exists pfa_gap_append_step_Q0coefficientsbound. pfa_gap_append_step_Q0coefficientsbound + S (pfc_index_append_step_Q0coefficients) = (K0)) -> exists pfc_value_append_step_Q0coefficients. ((((exists ff_h_pfp_append_step_Q0coefficientsentry. ff_h_pfp_append_step_Q0coefficientsentry + S (pfc_value_append_step_Q0coefficients) = S ((S (pfc_index_append_step_Q0coefficients)) * q0c)) /\ exists ff_q_pfp_append_step_Q0coefficientsentry. q0b = ff_q_pfp_append_step_Q0coefficientsentry * S ((S (pfc_index_append_step_Q0coefficients)) * q0c) + (pfc_value_append_step_Q0coefficients))) /\ ((exists pfc_terms_code_append_step_Q0coefficientscoefficient pfc_terms_scale_append_step_Q0coefficientscoefficient pfc_natural_sum_append_step_Q0coefficientscoefficient. ((forall pfc_index_append_step_Q0coefficientscoefficientdiagonal. (exists pfa_gap_append_step_Q0coefficientscoefficientdiagonalbound. pfa_gap_append_step_Q0coefficientscoefficientdiagonalbound + S (pfc_index_append_step_Q0coefficientscoefficientdiagonal) = (S (pfc_index_append_step_Q0coefficients))) -> exists pfc_value_append_step_Q0coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_Q0coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_Q0coefficientscoefficientdiagonalentry + S (pfc_value_append_step_Q0coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_Q0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q0coefficientscoefficient)) /\ exists ff_q_pfp_append_step_Q0coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_Q0coefficientscoefficient = ff_q_pfp_append_step_Q0coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_Q0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q0coefficientscoefficient) + (pfc_value_append_step_Q0coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm pfc_left_append_step_Q0coefficientscoefficientdiagonalterm pfc_right_append_step_Q0coefficientscoefficientdiagonalterm. (((pfc_index_append_step_Q0coefficientscoefficientdiagonal)+pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm=(pfc_index_append_step_Q0coefficients)) /\ ((((((exists pfa_gap_append_step_Q0coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_Q0coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_Q0coefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_append_step_Q0coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_Q0coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_Q0coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_Q0coefficientscoefficientdiagonal)) * bc)) /\ exists ff_q_pfp_append_step_Q0coefficientscoefficientdiagonaltermleftentry. bb = ff_q_pfp_append_step_Q0coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_Q0coefficientscoefficientdiagonal)) * bc) + (pfc_left_append_step_Q0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q0coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_Q0coefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_append_step_Q0coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_Q0coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_Q0coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_Q0coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_append_step_Q0coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_Q0coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_Q0coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_append_step_Q0coefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_append_step_Q0coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm)) * cc) + (pfc_right_append_step_Q0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q0coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_Q0coefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_Q0coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_Q0coefficientscoefficientdiagonal)=pfc_left_append_step_Q0coefficientscoefficientdiagonalterm*pfc_right_append_step_Q0coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_Q0coefficientscoefficientsum fs_v_pfc_append_step_Q0coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_start. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_start. fs_u_pfc_append_step_Q0coefficientscoefficientsum = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_Q0coefficientscoefficient) = S ((S (S (pfc_index_append_step_Q0coefficients))) * fs_v_pfc_append_step_Q0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_Q0coefficientscoefficientsum = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_Q0coefficients))) * fs_v_pfc_append_step_Q0coefficientscoefficientsum) + (pfc_natural_sum_append_step_Q0coefficientscoefficient))) /\ forall fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_Q0coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_Q0coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps = S (pfc_index_append_step_Q0coefficients)) -> exists fs_a_pfc_append_step_Q0coefficientscoefficientsum_body_steps fs_r_pfc_append_step_Q0coefficientscoefficientsum_body_steps fs_s_pfc_append_step_Q0coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_Q0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q0coefficientscoefficient)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_Q0coefficientscoefficient = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q0coefficientscoefficient) + (fs_a_pfc_append_step_Q0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_Q0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_Q0coefficientscoefficientsum = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum) + (fs_r_pfc_append_step_Q0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_Q0coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_Q0coefficientscoefficientsum = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum) + (fs_s_pfc_append_step_Q0coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_Q0coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_Q0coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_Q0coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_Q0coefficientscoefficientresiduebound. pfa_gap_append_step_Q0coefficientscoefficientresiduebound + S (pfc_value_append_step_Q0coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_Q0coefficientscoefficientresiduecongruence pfa_offset_right_append_step_Q0coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_Q0coefficientscoefficient) + (p) * pfa_offset_left_append_step_Q0coefficientscoefficientresiduecongruence = (pfc_value_append_step_Q0coefficients) + (p) * pfa_offset_right_append_step_Q0coefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_R0left. (exists fom_gap_pfp_append_step_R0left_index_bound. fom_gap_pfp_append_step_R0left_index_bound + S (fom_index_pfp_append_step_R0left) = N) -> exists fom_value_pfp_append_step_R0left. ((((exists fom_beta_height_pfp_append_step_R0left_entry. fom_beta_height_pfp_append_step_R0left_entry + S (fom_value_pfp_append_step_R0left) = S ((S (fom_index_pfp_append_step_R0left)) * pc)) /\ exists fom_beta_quotient_pfp_append_step_R0left_entry. pb = fom_beta_quotient_pfp_append_step_R0left_entry * S ((S (fom_index_pfp_append_step_R0left)) * pc) + (fom_value_pfp_append_step_R0left))) /\ (exists fom_gap_pfp_append_step_R0left_value_bound. fom_gap_pfp_append_step_R0left_value_bound + S (fom_value_pfp_append_step_R0left) = p))) /\ (((forall fom_index_pfp_append_step_R0right. (exists fom_gap_pfp_append_step_R0right_index_bound. fom_gap_pfp_append_step_R0right_index_bound + S (fom_index_pfp_append_step_R0right) = J) -> exists fom_value_pfp_append_step_R0right. ((((exists fom_beta_height_pfp_append_step_R0right_entry. fom_beta_height_pfp_append_step_R0right_entry + S (fom_value_pfp_append_step_R0right) = S ((S (fom_index_pfp_append_step_R0right)) * cc)) /\ exists fom_beta_quotient_pfp_append_step_R0right_entry. cb = fom_beta_quotient_pfp_append_step_R0right_entry * S ((S (fom_index_pfp_append_step_R0right)) * cc) + (fom_value_pfp_append_step_R0right))) /\ (exists fom_gap_pfp_append_step_R0right_value_bound. fom_gap_pfp_append_step_R0right_value_bound + S (fom_value_pfp_append_step_R0right) = p))) /\ (((((((N)=0 \/ (J)=0) /\ (((U0)=0)))) \/ (((~((N)=0)) /\ (((~((J)=0)) /\ (((N)+(J)=S (U0)))))))) /\ ((forall pfc_index_append_step_R0coefficients. (exists pfa_gap_append_step_R0coefficientsbound. pfa_gap_append_step_R0coefficientsbound + S (pfc_index_append_step_R0coefficients) = (U0)) -> exists pfc_value_append_step_R0coefficients. ((((exists ff_h_pfp_append_step_R0coefficientsentry. ff_h_pfp_append_step_R0coefficientsentry + S (pfc_value_append_step_R0coefficients) = S ((S (pfc_index_append_step_R0coefficients)) * r0c)) /\ exists ff_q_pfp_append_step_R0coefficientsentry. r0b = ff_q_pfp_append_step_R0coefficientsentry * S ((S (pfc_index_append_step_R0coefficients)) * r0c) + (pfc_value_append_step_R0coefficients))) /\ ((exists pfc_terms_code_append_step_R0coefficientscoefficient pfc_terms_scale_append_step_R0coefficientscoefficient pfc_natural_sum_append_step_R0coefficientscoefficient. ((forall pfc_index_append_step_R0coefficientscoefficientdiagonal. (exists pfa_gap_append_step_R0coefficientscoefficientdiagonalbound. pfa_gap_append_step_R0coefficientscoefficientdiagonalbound + S (pfc_index_append_step_R0coefficientscoefficientdiagonal) = (S (pfc_index_append_step_R0coefficients))) -> exists pfc_value_append_step_R0coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_R0coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_R0coefficientscoefficientdiagonalentry + S (pfc_value_append_step_R0coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_R0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_R0coefficientscoefficient)) /\ exists ff_q_pfp_append_step_R0coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_R0coefficientscoefficient = ff_q_pfp_append_step_R0coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_R0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_R0coefficientscoefficient) + (pfc_value_append_step_R0coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_R0coefficientscoefficientdiagonalterm pfc_left_append_step_R0coefficientscoefficientdiagonalterm pfc_right_append_step_R0coefficientscoefficientdiagonalterm. (((pfc_index_append_step_R0coefficientscoefficientdiagonal)+pfc_complement_append_step_R0coefficientscoefficientdiagonalterm=(pfc_index_append_step_R0coefficients)) /\ ((((((exists pfa_gap_append_step_R0coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_R0coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_R0coefficientscoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_append_step_R0coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_R0coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_R0coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_R0coefficientscoefficientdiagonal)) * pc)) /\ exists ff_q_pfp_append_step_R0coefficientscoefficientdiagonaltermleftentry. pb = ff_q_pfp_append_step_R0coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_R0coefficientscoefficientdiagonal)) * pc) + (pfc_left_append_step_R0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_R0coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_R0coefficientscoefficientdiagonaltermleftoutside+(N)=(pfc_index_append_step_R0coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_R0coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_R0coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_R0coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_R0coefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_append_step_R0coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_R0coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_R0coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_R0coefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_append_step_R0coefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_append_step_R0coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_R0coefficientscoefficientdiagonalterm)) * cc) + (pfc_right_append_step_R0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_R0coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_R0coefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_append_step_R0coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_R0coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_R0coefficientscoefficientdiagonal)=pfc_left_append_step_R0coefficientscoefficientdiagonalterm*pfc_right_append_step_R0coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_R0coefficientscoefficientsum fs_v_pfc_append_step_R0coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_start. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_R0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_start. fs_u_pfc_append_step_R0coefficientscoefficientsum = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_R0coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_R0coefficientscoefficient) = S ((S (S (pfc_index_append_step_R0coefficients))) * fs_v_pfc_append_step_R0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_R0coefficientscoefficientsum = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_R0coefficients))) * fs_v_pfc_append_step_R0coefficientscoefficientsum) + (pfc_natural_sum_append_step_R0coefficientscoefficient))) /\ forall fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_R0coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_R0coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps = S (pfc_index_append_step_R0coefficients)) -> exists fs_a_pfc_append_step_R0coefficientscoefficientsum_body_steps fs_r_pfc_append_step_R0coefficientscoefficientsum_body_steps fs_s_pfc_append_step_R0coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_R0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_R0coefficientscoefficient)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_R0coefficientscoefficient = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_R0coefficientscoefficient) + (fs_a_pfc_append_step_R0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_R0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_R0coefficientscoefficientsum = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R0coefficientscoefficientsum) + (fs_r_pfc_append_step_R0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_R0coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_R0coefficientscoefficientsum = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R0coefficientscoefficientsum) + (fs_s_pfc_append_step_R0coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_R0coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_R0coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_R0coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_R0coefficientscoefficientresiduebound. pfa_gap_append_step_R0coefficientscoefficientresiduebound + S (pfc_value_append_step_R0coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_R0coefficientscoefficientresiduecongruence pfa_offset_right_append_step_R0coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_R0coefficientscoefficient) + (p) * pfa_offset_left_append_step_R0coefficientscoefficientresiduecongruence = (pfc_value_append_step_R0coefficients) + (p) * pfa_offset_right_append_step_R0coefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_S0left. (exists fom_gap_pfp_append_step_S0left_index_bound. fom_gap_pfp_append_step_S0left_index_bound + S (fom_index_pfp_append_step_S0left) = L) -> exists fom_value_pfp_append_step_S0left. ((((exists fom_beta_height_pfp_append_step_S0left_entry. fom_beta_height_pfp_append_step_S0left_entry + S (fom_value_pfp_append_step_S0left) = S ((S (fom_index_pfp_append_step_S0left)) * ac)) /\ exists fom_beta_quotient_pfp_append_step_S0left_entry. ab = fom_beta_quotient_pfp_append_step_S0left_entry * S ((S (fom_index_pfp_append_step_S0left)) * ac) + (fom_value_pfp_append_step_S0left))) /\ (exists fom_gap_pfp_append_step_S0left_value_bound. fom_gap_pfp_append_step_S0left_value_bound + S (fom_value_pfp_append_step_S0left) = p))) /\ (((forall fom_index_pfp_append_step_S0right. (exists fom_gap_pfp_append_step_S0right_index_bound. fom_gap_pfp_append_step_S0right_index_bound + S (fom_index_pfp_append_step_S0right) = K0) -> exists fom_value_pfp_append_step_S0right. ((((exists fom_beta_height_pfp_append_step_S0right_entry. fom_beta_height_pfp_append_step_S0right_entry + S (fom_value_pfp_append_step_S0right) = S ((S (fom_index_pfp_append_step_S0right)) * q0c)) /\ exists fom_beta_quotient_pfp_append_step_S0right_entry. q0b = fom_beta_quotient_pfp_append_step_S0right_entry * S ((S (fom_index_pfp_append_step_S0right)) * q0c) + (fom_value_pfp_append_step_S0right))) /\ (exists fom_gap_pfp_append_step_S0right_value_bound. fom_gap_pfp_append_step_S0right_value_bound + S (fom_value_pfp_append_step_S0right) = p))) /\ (((((((L)=0 \/ (K0)=0) /\ (((V0)=0)))) \/ (((~((L)=0)) /\ (((~((K0)=0)) /\ (((L)+(K0)=S (V0)))))))) /\ ((forall pfc_index_append_step_S0coefficients. (exists pfa_gap_append_step_S0coefficientsbound. pfa_gap_append_step_S0coefficientsbound + S (pfc_index_append_step_S0coefficients) = (V0)) -> exists pfc_value_append_step_S0coefficients. ((((exists ff_h_pfp_append_step_S0coefficientsentry. ff_h_pfp_append_step_S0coefficientsentry + S (pfc_value_append_step_S0coefficients) = S ((S (pfc_index_append_step_S0coefficients)) * s0c)) /\ exists ff_q_pfp_append_step_S0coefficientsentry. s0b = ff_q_pfp_append_step_S0coefficientsentry * S ((S (pfc_index_append_step_S0coefficients)) * s0c) + (pfc_value_append_step_S0coefficients))) /\ ((exists pfc_terms_code_append_step_S0coefficientscoefficient pfc_terms_scale_append_step_S0coefficientscoefficient pfc_natural_sum_append_step_S0coefficientscoefficient. ((forall pfc_index_append_step_S0coefficientscoefficientdiagonal. (exists pfa_gap_append_step_S0coefficientscoefficientdiagonalbound. pfa_gap_append_step_S0coefficientscoefficientdiagonalbound + S (pfc_index_append_step_S0coefficientscoefficientdiagonal) = (S (pfc_index_append_step_S0coefficients))) -> exists pfc_value_append_step_S0coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_S0coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_S0coefficientscoefficientdiagonalentry + S (pfc_value_append_step_S0coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_S0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_S0coefficientscoefficient)) /\ exists ff_q_pfp_append_step_S0coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_S0coefficientscoefficient = ff_q_pfp_append_step_S0coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_S0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_S0coefficientscoefficient) + (pfc_value_append_step_S0coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_S0coefficientscoefficientdiagonalterm pfc_left_append_step_S0coefficientscoefficientdiagonalterm pfc_right_append_step_S0coefficientscoefficientdiagonalterm. (((pfc_index_append_step_S0coefficientscoefficientdiagonal)+pfc_complement_append_step_S0coefficientscoefficientdiagonalterm=(pfc_index_append_step_S0coefficients)) /\ ((((((exists pfa_gap_append_step_S0coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_S0coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_S0coefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_step_S0coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_S0coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_S0coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_S0coefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_step_S0coefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_step_S0coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_S0coefficientscoefficientdiagonal)) * ac) + (pfc_left_append_step_S0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_S0coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_S0coefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_step_S0coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_S0coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_S0coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_S0coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_S0coefficientscoefficientdiagonalterm) = (K0)) /\ ((((exists ff_h_pfp_append_step_S0coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_S0coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_S0coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_S0coefficientscoefficientdiagonalterm)) * q0c)) /\ exists ff_q_pfp_append_step_S0coefficientscoefficientdiagonaltermrightentry. q0b = ff_q_pfp_append_step_S0coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_S0coefficientscoefficientdiagonalterm)) * q0c) + (pfc_right_append_step_S0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_S0coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_S0coefficientscoefficientdiagonaltermrightoutside+(K0)=(pfc_complement_append_step_S0coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_S0coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_S0coefficientscoefficientdiagonal)=pfc_left_append_step_S0coefficientscoefficientdiagonalterm*pfc_right_append_step_S0coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_S0coefficientscoefficientsum fs_v_pfc_append_step_S0coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_start. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_S0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_start. fs_u_pfc_append_step_S0coefficientscoefficientsum = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_S0coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_S0coefficientscoefficient) = S ((S (S (pfc_index_append_step_S0coefficients))) * fs_v_pfc_append_step_S0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_S0coefficientscoefficientsum = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_S0coefficients))) * fs_v_pfc_append_step_S0coefficientscoefficientsum) + (pfc_natural_sum_append_step_S0coefficientscoefficient))) /\ forall fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_S0coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_S0coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps = S (pfc_index_append_step_S0coefficients)) -> exists fs_a_pfc_append_step_S0coefficientscoefficientsum_body_steps fs_r_pfc_append_step_S0coefficientscoefficientsum_body_steps fs_s_pfc_append_step_S0coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_S0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_S0coefficientscoefficient)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_S0coefficientscoefficient = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_S0coefficientscoefficient) + (fs_a_pfc_append_step_S0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_S0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_S0coefficientscoefficientsum = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S0coefficientscoefficientsum) + (fs_r_pfc_append_step_S0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_S0coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_S0coefficientscoefficientsum = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S0coefficientscoefficientsum) + (fs_s_pfc_append_step_S0coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_S0coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_S0coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_S0coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_S0coefficientscoefficientresiduebound. pfa_gap_append_step_S0coefficientscoefficientresiduebound + S (pfc_value_append_step_S0coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_S0coefficientscoefficientresiduecongruence pfa_offset_right_append_step_S0coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_S0coefficientscoefficient) + (p) * pfa_offset_left_append_step_S0coefficientscoefficientresiduecongruence = (pfc_value_append_step_S0coefficients) + (p) * pfa_offset_right_append_step_S0coefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_append_step_actual_induction_hypothesis pfrep_left_append_step_actual_induction_hypothesis pfrep_right_append_step_actual_induction_hypothesis. ((exists pfrep_position_append_step_actual_induction_hypothesisfirst. ((pfrep_position_append_step_actual_induction_hypothesisfirst+S (pfrep_power_append_step_actual_induction_hypothesis)=(U0)) /\ ((((exists ff_h_pfp_append_step_actual_induction_hypothesisfirstentry. ff_h_pfp_append_step_actual_induction_hypothesisfirstentry + S (pfrep_left_append_step_actual_induction_hypothesis) = S ((S (pfrep_position_append_step_actual_induction_hypothesisfirst)) * r0c)) /\ exists ff_q_pfp_append_step_actual_induction_hypothesisfirstentry. r0b = ff_q_pfp_append_step_actual_induction_hypothesisfirstentry * S ((S (pfrep_position_append_step_actual_induction_hypothesisfirst)) * r0c) + (pfrep_left_append_step_actual_induction_hypothesis)))))) \/ (((exists pfrep_gap_append_step_actual_induction_hypothesisfirstoutside. pfrep_gap_append_step_actual_induction_hypothesisfirstoutside+(U0)=(pfrep_power_append_step_actual_induction_hypothesis)) /\ (((pfrep_left_append_step_actual_induction_hypothesis)=0))))) -> ((exists pfrep_position_append_step_actual_induction_hypothesissecond. ((pfrep_position_append_step_actual_induction_hypothesissecond+S (pfrep_power_append_step_actual_induction_hypothesis)=(V0)) /\ ((((exists ff_h_pfp_append_step_actual_induction_hypothesissecondentry. ff_h_pfp_append_step_actual_induction_hypothesissecondentry + S (pfrep_right_append_step_actual_induction_hypothesis) = S ((S (pfrep_position_append_step_actual_induction_hypothesissecond)) * s0c)) /\ exists ff_q_pfp_append_step_actual_induction_hypothesissecondentry. s0b = ff_q_pfp_append_step_actual_induction_hypothesissecondentry * S ((S (pfrep_position_append_step_actual_induction_hypothesissecond)) * s0c) + (pfrep_right_append_step_actual_induction_hypothesis)))))) \/ (((exists pfrep_gap_append_step_actual_induction_hypothesissecondoutside. pfrep_gap_append_step_actual_induction_hypothesissecondoutside+(V0)=(pfrep_power_append_step_actual_induction_hypothesis)) /\ (((pfrep_right_append_step_actual_induction_hypothesis)=0))))) -> pfrep_left_append_step_actual_induction_hypothesis=pfrep_right_append_step_actual_induction_hypothesis) -> (forall mdr_i_pfp_append_step_prefix mdr_a_pfp_append_step_prefix. (exists mdr_gap_pfp_append_step_prefixb. mdr_gap_pfp_append_step_prefixb + S (mdr_i_pfp_append_step_prefix) = (J)) -> (((exists ff_h_mdr_pfp_append_step_prefixo. ff_h_mdr_pfp_append_step_prefixo + S (mdr_a_pfp_append_step_prefix) = S ((S (mdr_i_pfp_append_step_prefix)) * cc)) /\ exists ff_q_mdr_pfp_append_step_prefixo. cb = ff_q_mdr_pfp_append_step_prefixo * S ((S (mdr_i_pfp_append_step_prefix)) * cc) + (mdr_a_pfp_append_step_prefix))) -> (((exists ff_h_mdr_pfp_append_step_prefixn. ff_h_mdr_pfp_append_step_prefixn + S (mdr_a_pfp_append_step_prefix) = S ((S (mdr_i_pfp_append_step_prefix)) * dc)) /\ exists ff_q_mdr_pfp_append_step_prefixn. db = ff_q_mdr_pfp_append_step_prefixn * S ((S (mdr_i_pfp_append_step_prefix)) * dc) + (mdr_a_pfp_append_step_prefix)))) -> (((exists ff_h_pfp_append_step_last. ff_h_pfp_append_step_last + S (c) = S ((S (J)) * dc)) /\ exists ff_q_pfp_append_step_last. db = ff_q_pfp_append_step_last * S ((S (J)) * dc) + (c))) -> (((forall fom_index_pfp_append_step_Q1left. (exists fom_gap_pfp_append_step_Q1left_index_bound. fom_gap_pfp_append_step_Q1left_index_bound + S (fom_index_pfp_append_step_Q1left) = M) -> exists fom_value_pfp_append_step_Q1left. ((((exists fom_beta_height_pfp_append_step_Q1left_entry. fom_beta_height_pfp_append_step_Q1left_entry + S (fom_value_pfp_append_step_Q1left) = S ((S (fom_index_pfp_append_step_Q1left)) * bc)) /\ exists fom_beta_quotient_pfp_append_step_Q1left_entry. bb = fom_beta_quotient_pfp_append_step_Q1left_entry * S ((S (fom_index_pfp_append_step_Q1left)) * bc) + (fom_value_pfp_append_step_Q1left))) /\ (exists fom_gap_pfp_append_step_Q1left_value_bound. fom_gap_pfp_append_step_Q1left_value_bound + S (fom_value_pfp_append_step_Q1left) = p))) /\ (((forall fom_index_pfp_append_step_Q1right. (exists fom_gap_pfp_append_step_Q1right_index_bound. fom_gap_pfp_append_step_Q1right_index_bound + S (fom_index_pfp_append_step_Q1right) = S J) -> exists fom_value_pfp_append_step_Q1right. ((((exists fom_beta_height_pfp_append_step_Q1right_entry. fom_beta_height_pfp_append_step_Q1right_entry + S (fom_value_pfp_append_step_Q1right) = S ((S (fom_index_pfp_append_step_Q1right)) * dc)) /\ exists fom_beta_quotient_pfp_append_step_Q1right_entry. db = fom_beta_quotient_pfp_append_step_Q1right_entry * S ((S (fom_index_pfp_append_step_Q1right)) * dc) + (fom_value_pfp_append_step_Q1right))) /\ (exists fom_gap_pfp_append_step_Q1right_value_bound. fom_gap_pfp_append_step_Q1right_value_bound + S (fom_value_pfp_append_step_Q1right) = p))) /\ (((((((M)=0 \/ (S J)=0) /\ (((K1)=0)))) \/ (((~((M)=0)) /\ (((~((S J)=0)) /\ (((M)+(S J)=S (K1)))))))) /\ ((forall pfc_index_append_step_Q1coefficients. (exists pfa_gap_append_step_Q1coefficientsbound. pfa_gap_append_step_Q1coefficientsbound + S (pfc_index_append_step_Q1coefficients) = (K1)) -> exists pfc_value_append_step_Q1coefficients. ((((exists ff_h_pfp_append_step_Q1coefficientsentry. ff_h_pfp_append_step_Q1coefficientsentry + S (pfc_value_append_step_Q1coefficients) = S ((S (pfc_index_append_step_Q1coefficients)) * q1c)) /\ exists ff_q_pfp_append_step_Q1coefficientsentry. q1b = ff_q_pfp_append_step_Q1coefficientsentry * S ((S (pfc_index_append_step_Q1coefficients)) * q1c) + (pfc_value_append_step_Q1coefficients))) /\ ((exists pfc_terms_code_append_step_Q1coefficientscoefficient pfc_terms_scale_append_step_Q1coefficientscoefficient pfc_natural_sum_append_step_Q1coefficientscoefficient. ((forall pfc_index_append_step_Q1coefficientscoefficientdiagonal. (exists pfa_gap_append_step_Q1coefficientscoefficientdiagonalbound. pfa_gap_append_step_Q1coefficientscoefficientdiagonalbound + S (pfc_index_append_step_Q1coefficientscoefficientdiagonal) = (S (pfc_index_append_step_Q1coefficients))) -> exists pfc_value_append_step_Q1coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonalentry + S (pfc_value_append_step_Q1coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q1coefficientscoefficient)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_Q1coefficientscoefficient = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q1coefficientscoefficient) + (pfc_value_append_step_Q1coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm pfc_left_append_step_Q1coefficientscoefficientdiagonalterm pfc_right_append_step_Q1coefficientscoefficientdiagonalterm. (((pfc_index_append_step_Q1coefficientscoefficientdiagonal)+pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm=(pfc_index_append_step_Q1coefficients)) /\ ((((((exists pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_Q1coefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_Q1coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * bc)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry. bb = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * bc) + (pfc_left_append_step_Q1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_append_step_Q1coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_Q1coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm) = (S J)) /\ ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_Q1coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_step_Q1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermrightoutside+(S J)=(pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_Q1coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_Q1coefficientscoefficientdiagonal)=pfc_left_append_step_Q1coefficientscoefficientdiagonalterm*pfc_right_append_step_Q1coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_Q1coefficientscoefficientsum fs_v_pfc_append_step_Q1coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_start. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_start. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_Q1coefficientscoefficient) = S ((S (S (pfc_index_append_step_Q1coefficients))) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_Q1coefficients))) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (pfc_natural_sum_append_step_Q1coefficientscoefficient))) /\ forall fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_Q1coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_Q1coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps = S (pfc_index_append_step_Q1coefficients)) -> exists fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q1coefficientscoefficient)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_Q1coefficientscoefficient = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q1coefficientscoefficient) + (fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_Q1coefficientscoefficientresiduebound. pfa_gap_append_step_Q1coefficientscoefficientresiduebound + S (pfc_value_append_step_Q1coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_Q1coefficientscoefficientresiduecongruence pfa_offset_right_append_step_Q1coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_Q1coefficientscoefficient) + (p) * pfa_offset_left_append_step_Q1coefficientscoefficientresiduecongruence = (pfc_value_append_step_Q1coefficients) + (p) * pfa_offset_right_append_step_Q1coefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_R1left. (exists fom_gap_pfp_append_step_R1left_index_bound. fom_gap_pfp_append_step_R1left_index_bound + S (fom_index_pfp_append_step_R1left) = N) -> exists fom_value_pfp_append_step_R1left. ((((exists fom_beta_height_pfp_append_step_R1left_entry. fom_beta_height_pfp_append_step_R1left_entry + S (fom_value_pfp_append_step_R1left) = S ((S (fom_index_pfp_append_step_R1left)) * pc)) /\ exists fom_beta_quotient_pfp_append_step_R1left_entry. pb = fom_beta_quotient_pfp_append_step_R1left_entry * S ((S (fom_index_pfp_append_step_R1left)) * pc) + (fom_value_pfp_append_step_R1left))) /\ (exists fom_gap_pfp_append_step_R1left_value_bound. fom_gap_pfp_append_step_R1left_value_bound + S (fom_value_pfp_append_step_R1left) = p))) /\ (((forall fom_index_pfp_append_step_R1right. (exists fom_gap_pfp_append_step_R1right_index_bound. fom_gap_pfp_append_step_R1right_index_bound + S (fom_index_pfp_append_step_R1right) = S J) -> exists fom_value_pfp_append_step_R1right. ((((exists fom_beta_height_pfp_append_step_R1right_entry. fom_beta_height_pfp_append_step_R1right_entry + S (fom_value_pfp_append_step_R1right) = S ((S (fom_index_pfp_append_step_R1right)) * dc)) /\ exists fom_beta_quotient_pfp_append_step_R1right_entry. db = fom_beta_quotient_pfp_append_step_R1right_entry * S ((S (fom_index_pfp_append_step_R1right)) * dc) + (fom_value_pfp_append_step_R1right))) /\ (exists fom_gap_pfp_append_step_R1right_value_bound. fom_gap_pfp_append_step_R1right_value_bound + S (fom_value_pfp_append_step_R1right) = p))) /\ (((((((N)=0 \/ (S J)=0) /\ (((U1)=0)))) \/ (((~((N)=0)) /\ (((~((S J)=0)) /\ (((N)+(S J)=S (U1)))))))) /\ ((forall pfc_index_append_step_R1coefficients. (exists pfa_gap_append_step_R1coefficientsbound. pfa_gap_append_step_R1coefficientsbound + S (pfc_index_append_step_R1coefficients) = (U1)) -> exists pfc_value_append_step_R1coefficients. ((((exists ff_h_pfp_append_step_R1coefficientsentry. ff_h_pfp_append_step_R1coefficientsentry + S (pfc_value_append_step_R1coefficients) = S ((S (pfc_index_append_step_R1coefficients)) * r1c)) /\ exists ff_q_pfp_append_step_R1coefficientsentry. r1b = ff_q_pfp_append_step_R1coefficientsentry * S ((S (pfc_index_append_step_R1coefficients)) * r1c) + (pfc_value_append_step_R1coefficients))) /\ ((exists pfc_terms_code_append_step_R1coefficientscoefficient pfc_terms_scale_append_step_R1coefficientscoefficient pfc_natural_sum_append_step_R1coefficientscoefficient. ((forall pfc_index_append_step_R1coefficientscoefficientdiagonal. (exists pfa_gap_append_step_R1coefficientscoefficientdiagonalbound. pfa_gap_append_step_R1coefficientscoefficientdiagonalbound + S (pfc_index_append_step_R1coefficientscoefficientdiagonal) = (S (pfc_index_append_step_R1coefficients))) -> exists pfc_value_append_step_R1coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_R1coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_R1coefficientscoefficientdiagonalentry + S (pfc_value_append_step_R1coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_R1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_R1coefficientscoefficient)) /\ exists ff_q_pfp_append_step_R1coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_R1coefficientscoefficient = ff_q_pfp_append_step_R1coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_R1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_R1coefficientscoefficient) + (pfc_value_append_step_R1coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_R1coefficientscoefficientdiagonalterm pfc_left_append_step_R1coefficientscoefficientdiagonalterm pfc_right_append_step_R1coefficientscoefficientdiagonalterm. (((pfc_index_append_step_R1coefficientscoefficientdiagonal)+pfc_complement_append_step_R1coefficientscoefficientdiagonalterm=(pfc_index_append_step_R1coefficients)) /\ ((((((exists pfa_gap_append_step_R1coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_R1coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_R1coefficientscoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_append_step_R1coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_R1coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_R1coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_R1coefficientscoefficientdiagonal)) * pc)) /\ exists ff_q_pfp_append_step_R1coefficientscoefficientdiagonaltermleftentry. pb = ff_q_pfp_append_step_R1coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_R1coefficientscoefficientdiagonal)) * pc) + (pfc_left_append_step_R1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_R1coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_R1coefficientscoefficientdiagonaltermleftoutside+(N)=(pfc_index_append_step_R1coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_R1coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_R1coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_R1coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_R1coefficientscoefficientdiagonalterm) = (S J)) /\ ((((exists ff_h_pfp_append_step_R1coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_R1coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_R1coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_R1coefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_step_R1coefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_step_R1coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_R1coefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_step_R1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_R1coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_R1coefficientscoefficientdiagonaltermrightoutside+(S J)=(pfc_complement_append_step_R1coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_R1coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_R1coefficientscoefficientdiagonal)=pfc_left_append_step_R1coefficientscoefficientdiagonalterm*pfc_right_append_step_R1coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_R1coefficientscoefficientsum fs_v_pfc_append_step_R1coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_start. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_R1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_start. fs_u_pfc_append_step_R1coefficientscoefficientsum = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_R1coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_R1coefficientscoefficient) = S ((S (S (pfc_index_append_step_R1coefficients))) * fs_v_pfc_append_step_R1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_R1coefficientscoefficientsum = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_R1coefficients))) * fs_v_pfc_append_step_R1coefficientscoefficientsum) + (pfc_natural_sum_append_step_R1coefficientscoefficient))) /\ forall fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_R1coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_R1coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps = S (pfc_index_append_step_R1coefficients)) -> exists fs_a_pfc_append_step_R1coefficientscoefficientsum_body_steps fs_r_pfc_append_step_R1coefficientscoefficientsum_body_steps fs_s_pfc_append_step_R1coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_R1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_R1coefficientscoefficient)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_R1coefficientscoefficient = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_R1coefficientscoefficient) + (fs_a_pfc_append_step_R1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_R1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_R1coefficientscoefficientsum = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R1coefficientscoefficientsum) + (fs_r_pfc_append_step_R1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_R1coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_R1coefficientscoefficientsum = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R1coefficientscoefficientsum) + (fs_s_pfc_append_step_R1coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_R1coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_R1coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_R1coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_R1coefficientscoefficientresiduebound. pfa_gap_append_step_R1coefficientscoefficientresiduebound + S (pfc_value_append_step_R1coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_R1coefficientscoefficientresiduecongruence pfa_offset_right_append_step_R1coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_R1coefficientscoefficient) + (p) * pfa_offset_left_append_step_R1coefficientscoefficientresiduecongruence = (pfc_value_append_step_R1coefficients) + (p) * pfa_offset_right_append_step_R1coefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_S1left. (exists fom_gap_pfp_append_step_S1left_index_bound. fom_gap_pfp_append_step_S1left_index_bound + S (fom_index_pfp_append_step_S1left) = L) -> exists fom_value_pfp_append_step_S1left. ((((exists fom_beta_height_pfp_append_step_S1left_entry. fom_beta_height_pfp_append_step_S1left_entry + S (fom_value_pfp_append_step_S1left) = S ((S (fom_index_pfp_append_step_S1left)) * ac)) /\ exists fom_beta_quotient_pfp_append_step_S1left_entry. ab = fom_beta_quotient_pfp_append_step_S1left_entry * S ((S (fom_index_pfp_append_step_S1left)) * ac) + (fom_value_pfp_append_step_S1left))) /\ (exists fom_gap_pfp_append_step_S1left_value_bound. fom_gap_pfp_append_step_S1left_value_bound + S (fom_value_pfp_append_step_S1left) = p))) /\ (((forall fom_index_pfp_append_step_S1right. (exists fom_gap_pfp_append_step_S1right_index_bound. fom_gap_pfp_append_step_S1right_index_bound + S (fom_index_pfp_append_step_S1right) = K1) -> exists fom_value_pfp_append_step_S1right. ((((exists fom_beta_height_pfp_append_step_S1right_entry. fom_beta_height_pfp_append_step_S1right_entry + S (fom_value_pfp_append_step_S1right) = S ((S (fom_index_pfp_append_step_S1right)) * q1c)) /\ exists fom_beta_quotient_pfp_append_step_S1right_entry. q1b = fom_beta_quotient_pfp_append_step_S1right_entry * S ((S (fom_index_pfp_append_step_S1right)) * q1c) + (fom_value_pfp_append_step_S1right))) /\ (exists fom_gap_pfp_append_step_S1right_value_bound. fom_gap_pfp_append_step_S1right_value_bound + S (fom_value_pfp_append_step_S1right) = p))) /\ (((((((L)=0 \/ (K1)=0) /\ (((V1)=0)))) \/ (((~((L)=0)) /\ (((~((K1)=0)) /\ (((L)+(K1)=S (V1)))))))) /\ ((forall pfc_index_append_step_S1coefficients. (exists pfa_gap_append_step_S1coefficientsbound. pfa_gap_append_step_S1coefficientsbound + S (pfc_index_append_step_S1coefficients) = (V1)) -> exists pfc_value_append_step_S1coefficients. ((((exists ff_h_pfp_append_step_S1coefficientsentry. ff_h_pfp_append_step_S1coefficientsentry + S (pfc_value_append_step_S1coefficients) = S ((S (pfc_index_append_step_S1coefficients)) * s1c)) /\ exists ff_q_pfp_append_step_S1coefficientsentry. s1b = ff_q_pfp_append_step_S1coefficientsentry * S ((S (pfc_index_append_step_S1coefficients)) * s1c) + (pfc_value_append_step_S1coefficients))) /\ ((exists pfc_terms_code_append_step_S1coefficientscoefficient pfc_terms_scale_append_step_S1coefficientscoefficient pfc_natural_sum_append_step_S1coefficientscoefficient. ((forall pfc_index_append_step_S1coefficientscoefficientdiagonal. (exists pfa_gap_append_step_S1coefficientscoefficientdiagonalbound. pfa_gap_append_step_S1coefficientscoefficientdiagonalbound + S (pfc_index_append_step_S1coefficientscoefficientdiagonal) = (S (pfc_index_append_step_S1coefficients))) -> exists pfc_value_append_step_S1coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_S1coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_S1coefficientscoefficientdiagonalentry + S (pfc_value_append_step_S1coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_S1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_S1coefficientscoefficient)) /\ exists ff_q_pfp_append_step_S1coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_S1coefficientscoefficient = ff_q_pfp_append_step_S1coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_S1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_S1coefficientscoefficient) + (pfc_value_append_step_S1coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_S1coefficientscoefficientdiagonalterm pfc_left_append_step_S1coefficientscoefficientdiagonalterm pfc_right_append_step_S1coefficientscoefficientdiagonalterm. (((pfc_index_append_step_S1coefficientscoefficientdiagonal)+pfc_complement_append_step_S1coefficientscoefficientdiagonalterm=(pfc_index_append_step_S1coefficients)) /\ ((((((exists pfa_gap_append_step_S1coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_S1coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_S1coefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_step_S1coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_S1coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_S1coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_S1coefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_step_S1coefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_step_S1coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_S1coefficientscoefficientdiagonal)) * ac) + (pfc_left_append_step_S1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_S1coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_S1coefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_step_S1coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_S1coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_S1coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_S1coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_S1coefficientscoefficientdiagonalterm) = (K1)) /\ ((((exists ff_h_pfp_append_step_S1coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_S1coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_S1coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_S1coefficientscoefficientdiagonalterm)) * q1c)) /\ exists ff_q_pfp_append_step_S1coefficientscoefficientdiagonaltermrightentry. q1b = ff_q_pfp_append_step_S1coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_S1coefficientscoefficientdiagonalterm)) * q1c) + (pfc_right_append_step_S1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_S1coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_S1coefficientscoefficientdiagonaltermrightoutside+(K1)=(pfc_complement_append_step_S1coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_S1coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_S1coefficientscoefficientdiagonal)=pfc_left_append_step_S1coefficientscoefficientdiagonalterm*pfc_right_append_step_S1coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_S1coefficientscoefficientsum fs_v_pfc_append_step_S1coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_start. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_S1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_start. fs_u_pfc_append_step_S1coefficientscoefficientsum = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_S1coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_S1coefficientscoefficient) = S ((S (S (pfc_index_append_step_S1coefficients))) * fs_v_pfc_append_step_S1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_S1coefficientscoefficientsum = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_S1coefficients))) * fs_v_pfc_append_step_S1coefficientscoefficientsum) + (pfc_natural_sum_append_step_S1coefficientscoefficient))) /\ forall fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_S1coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_S1coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps = S (pfc_index_append_step_S1coefficients)) -> exists fs_a_pfc_append_step_S1coefficientscoefficientsum_body_steps fs_r_pfc_append_step_S1coefficientscoefficientsum_body_steps fs_s_pfc_append_step_S1coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_S1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_S1coefficientscoefficient)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_S1coefficientscoefficient = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_S1coefficientscoefficient) + (fs_a_pfc_append_step_S1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_S1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_S1coefficientscoefficientsum = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S1coefficientscoefficientsum) + (fs_r_pfc_append_step_S1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_S1coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_S1coefficientscoefficientsum = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S1coefficientscoefficientsum) + (fs_s_pfc_append_step_S1coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_S1coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_S1coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_S1coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_S1coefficientscoefficientresiduebound. pfa_gap_append_step_S1coefficientscoefficientresiduebound + S (pfc_value_append_step_S1coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_S1coefficientscoefficientresiduecongruence pfa_offset_right_append_step_S1coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_S1coefficientscoefficient) + (p) * pfa_offset_left_append_step_S1coefficientscoefficientresiduecongruence = (pfc_value_append_step_S1coefficients) + (p) * pfa_offset_right_append_step_S1coefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_append_step_result pfrep_left_append_step_result pfrep_right_append_step_result. ((exists pfrep_position_append_step_resultfirst. ((pfrep_position_append_step_resultfirst+S (pfrep_power_append_step_result)=(U1)) /\ ((((exists ff_h_pfp_append_step_resultfirstentry. ff_h_pfp_append_step_resultfirstentry + S (pfrep_left_append_step_result) = S ((S (pfrep_position_append_step_resultfirst)) * r1c)) /\ exists ff_q_pfp_append_step_resultfirstentry. r1b = ff_q_pfp_append_step_resultfirstentry * S ((S (pfrep_position_append_step_resultfirst)) * r1c) + (pfrep_left_append_step_result)))))) \/ (((exists pfrep_gap_append_step_resultfirstoutside. pfrep_gap_append_step_resultfirstoutside+(U1)=(pfrep_power_append_step_result)) /\ (((pfrep_left_append_step_result)=0))))) -> ((exists pfrep_position_append_step_resultsecond. ((pfrep_position_append_step_resultsecond+S (pfrep_power_append_step_result)=(V1)) /\ ((((exists ff_h_pfp_append_step_resultsecondentry. ff_h_pfp_append_step_resultsecondentry + S (pfrep_right_append_step_result) = S ((S (pfrep_position_append_step_resultsecond)) * s1c)) /\ exists ff_q_pfp_append_step_resultsecondentry. s1b = ff_q_pfp_append_step_resultsecondentry * S ((S (pfrep_position_append_step_resultsecond)) * s1c) + (pfrep_right_append_step_result)))))) \/ (((exists pfrep_gap_append_step_resultsecondoutside. pfrep_gap_append_step_resultsecondoutside+(V1)=(pfrep_power_append_step_result)) /\ (((pfrep_right_append_step_result)=0))))) -> pfrep_left_append_step_result=pfrep_right_append_step_result)