prime_field_polynomial_convolution_right_append_exists

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M c pb pc N. (~((p) = 1) /\ forall pfa_factor_left_append_exists_prime pfa_factor_right_append_exists_prime. (p) = pfa_factor_left_append_exists_prime * pfa_factor_right_append_exists_prime -> pfa_factor_left_append_exists_prime = 1 \/ pfa_factor_right_append_exists_prime = 1) -> (exists pfa_gap_append_exists_scalar. pfa_gap_append_exists_scalar + S (c) = (p)) -> (((forall fom_index_pfp_append_exists_oldleft. (exists fom_gap_pfp_append_exists_oldleft_index_bound. fom_gap_pfp_append_exists_oldleft_index_bound + S (fom_index_pfp_append_exists_oldleft) = L) -> exists fom_value_pfp_append_exists_oldleft. ((((exists fom_beta_height_pfp_append_exists_oldleft_entry. fom_beta_height_pfp_append_exists_oldleft_entry + S (fom_value_pfp_append_exists_oldleft) = S ((S (fom_index_pfp_append_exists_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_exists_oldleft_entry. ab = fom_beta_quotient_pfp_append_exists_oldleft_entry * S ((S (fom_index_pfp_append_exists_oldleft)) * ac) + (fom_value_pfp_append_exists_oldleft))) /\ (exists fom_gap_pfp_append_exists_oldleft_value_bound. fom_gap_pfp_append_exists_oldleft_value_bound + S (fom_value_pfp_append_exists_oldleft) = p))) /\ (((forall fom_index_pfp_append_exists_oldright. (exists fom_gap_pfp_append_exists_oldright_index_bound. fom_gap_pfp_append_exists_oldright_index_bound + S (fom_index_pfp_append_exists_oldright) = M) -> exists fom_value_pfp_append_exists_oldright. ((((exists fom_beta_height_pfp_append_exists_oldright_entry. fom_beta_height_pfp_append_exists_oldright_entry + S (fom_value_pfp_append_exists_oldright) = S ((S (fom_index_pfp_append_exists_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_append_exists_oldright_entry. bb = fom_beta_quotient_pfp_append_exists_oldright_entry * S ((S (fom_index_pfp_append_exists_oldright)) * bc) + (fom_value_pfp_append_exists_oldright))) /\ (exists fom_gap_pfp_append_exists_oldright_value_bound. fom_gap_pfp_append_exists_oldright_value_bound + S (fom_value_pfp_append_exists_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_append_exists_oldcoefficients. (exists pfa_gap_append_exists_oldcoefficientsbound. pfa_gap_append_exists_oldcoefficientsbound + S (pfc_index_append_exists_oldcoefficients) = (N)) -> exists pfc_value_append_exists_oldcoefficients. ((((exists ff_h_pfp_append_exists_oldcoefficientsentry. ff_h_pfp_append_exists_oldcoefficientsentry + S (pfc_value_append_exists_oldcoefficients) = S ((S (pfc_index_append_exists_oldcoefficients)) * pc)) /\ exists ff_q_pfp_append_exists_oldcoefficientsentry. pb = ff_q_pfp_append_exists_oldcoefficientsentry * S ((S (pfc_index_append_exists_oldcoefficients)) * pc) + (pfc_value_append_exists_oldcoefficients))) /\ ((exists pfc_terms_code_append_exists_oldcoefficientscoefficient pfc_terms_scale_append_exists_oldcoefficientscoefficient pfc_natural_sum_append_exists_oldcoefficientscoefficient. ((forall pfc_index_append_exists_oldcoefficientscoefficientdiagonal. (exists pfa_gap_append_exists_oldcoefficientscoefficientdiagonalbound. pfa_gap_append_exists_oldcoefficientscoefficientdiagonalbound + S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal) = (S (pfc_index_append_exists_oldcoefficients))) -> exists pfc_value_append_exists_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonalentry + S (pfc_value_append_exists_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_exists_oldcoefficientscoefficient)) /\ exists ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_append_exists_oldcoefficientscoefficient = ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_exists_oldcoefficientscoefficient) + (pfc_value_append_exists_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm. (((pfc_index_append_exists_oldcoefficientscoefficientdiagonal)+pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm=(pfc_index_append_exists_oldcoefficients)) /\ ((((((exists pfa_gap_append_exists_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_exists_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_exists_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_exists_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_exists_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_exists_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_exists_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_exists_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_exists_oldcoefficientscoefficientdiagonal)=pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm*pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_exists_oldcoefficientscoefficientsum fs_v_pfc_append_exists_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_start. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_start. fs_u_pfc_append_exists_oldcoefficientscoefficientsum = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_exists_oldcoefficientscoefficient) = S ((S (S (pfc_index_append_exists_oldcoefficients))) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_exists_oldcoefficientscoefficientsum = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_exists_oldcoefficients))) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum) + (pfc_natural_sum_append_exists_oldcoefficientscoefficient))) /\ forall fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps = S (pfc_index_append_exists_oldcoefficients)) -> exists fs_a_pfc_append_exists_oldcoefficientscoefficientsum_body_steps fs_r_pfc_append_exists_oldcoefficientscoefficientsum_body_steps fs_s_pfc_append_exists_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_exists_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_exists_oldcoefficientscoefficient)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_exists_oldcoefficientscoefficient = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_exists_oldcoefficientscoefficient) + (fs_a_pfc_append_exists_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_exists_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_exists_oldcoefficientscoefficientsum = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum) + (fs_r_pfc_append_exists_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_exists_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_exists_oldcoefficientscoefficientsum = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum) + (fs_s_pfc_append_exists_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_exists_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_append_exists_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_exists_oldcoefficientscoefficientresiduebound. pfa_gap_append_exists_oldcoefficientscoefficientresiduebound + S (pfc_value_append_exists_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_append_exists_oldcoefficientscoefficientresiduecongruence pfa_offset_right_append_exists_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_exists_oldcoefficientscoefficient) + (p) * pfa_offset_left_append_exists_oldcoefficientscoefficientresiduecongruence = (pfc_value_append_exists_oldcoefficients) + (p) * pfa_offset_right_append_exists_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (exists db dc K qb qc ub uc vb vc UB UC VB VC rb rc. ((forall mdr_i_pfp_append_exists_preserve mdr_a_pfp_append_exists_preserve. (exists mdr_gap_pfp_append_exists_preserveb. mdr_gap_pfp_append_exists_preserveb + S (mdr_i_pfp_append_exists_preserve) = (M)) -> (((exists ff_h_mdr_pfp_append_exists_preserveo. ff_h_mdr_pfp_append_exists_preserveo + S (mdr_a_pfp_append_exists_preserve) = S ((S (mdr_i_pfp_append_exists_preserve)) * bc)) /\ exists ff_q_mdr_pfp_append_exists_preserveo. bb = ff_q_mdr_pfp_append_exists_preserveo * S ((S (mdr_i_pfp_append_exists_preserve)) * bc) + (mdr_a_pfp_append_exists_preserve))) -> (((exists ff_h_mdr_pfp_append_exists_preserven. ff_h_mdr_pfp_append_exists_preserven + S (mdr_a_pfp_append_exists_preserve) = S ((S (mdr_i_pfp_append_exists_preserve)) * dc)) /\ exists ff_q_mdr_pfp_append_exists_preserven. db = ff_q_mdr_pfp_append_exists_preserven * S ((S (mdr_i_pfp_append_exists_preserve)) * dc) + (mdr_a_pfp_append_exists_preserve)))) /\ (((((exists ff_h_pfp_append_exists_last. ff_h_pfp_append_exists_last + S (c) = S ((S (M)) * dc)) /\ exists ff_q_pfp_append_exists_last. db = ff_q_pfp_append_exists_last * S ((S (M)) * dc) + (c))) /\ (((((forall fom_index_pfp_append_exists_newleft. (exists fom_gap_pfp_append_exists_newleft_index_bound. fom_gap_pfp_append_exists_newleft_index_bound + S (fom_index_pfp_append_exists_newleft) = L) -> exists fom_value_pfp_append_exists_newleft. ((((exists fom_beta_height_pfp_append_exists_newleft_entry. fom_beta_height_pfp_append_exists_newleft_entry + S (fom_value_pfp_append_exists_newleft) = S ((S (fom_index_pfp_append_exists_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_exists_newleft_entry. ab = fom_beta_quotient_pfp_append_exists_newleft_entry * S ((S (fom_index_pfp_append_exists_newleft)) * ac) + (fom_value_pfp_append_exists_newleft))) /\ (exists fom_gap_pfp_append_exists_newleft_value_bound. fom_gap_pfp_append_exists_newleft_value_bound + S (fom_value_pfp_append_exists_newleft) = p))) /\ (((forall fom_index_pfp_append_exists_newright. (exists fom_gap_pfp_append_exists_newright_index_bound. fom_gap_pfp_append_exists_newright_index_bound + S (fom_index_pfp_append_exists_newright) = S M) -> exists fom_value_pfp_append_exists_newright. ((((exists fom_beta_height_pfp_append_exists_newright_entry. fom_beta_height_pfp_append_exists_newright_entry + S (fom_value_pfp_append_exists_newright) = S ((S (fom_index_pfp_append_exists_newright)) * dc)) /\ exists fom_beta_quotient_pfp_append_exists_newright_entry. db = fom_beta_quotient_pfp_append_exists_newright_entry * S ((S (fom_index_pfp_append_exists_newright)) * dc) + (fom_value_pfp_append_exists_newright))) /\ (exists fom_gap_pfp_append_exists_newright_value_bound. fom_gap_pfp_append_exists_newright_value_bound + S (fom_value_pfp_append_exists_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_append_exists_newcoefficients. (exists pfa_gap_append_exists_newcoefficientsbound. pfa_gap_append_exists_newcoefficientsbound + S (pfc_index_append_exists_newcoefficients) = (K)) -> exists pfc_value_append_exists_newcoefficients. ((((exists ff_h_pfp_append_exists_newcoefficientsentry. ff_h_pfp_append_exists_newcoefficientsentry + S (pfc_value_append_exists_newcoefficients) = S ((S (pfc_index_append_exists_newcoefficients)) * qc)) /\ exists ff_q_pfp_append_exists_newcoefficientsentry. qb = ff_q_pfp_append_exists_newcoefficientsentry * S ((S (pfc_index_append_exists_newcoefficients)) * qc) + (pfc_value_append_exists_newcoefficients))) /\ ((exists pfc_terms_code_append_exists_newcoefficientscoefficient pfc_terms_scale_append_exists_newcoefficientscoefficient pfc_natural_sum_append_exists_newcoefficientscoefficient. ((forall pfc_index_append_exists_newcoefficientscoefficientdiagonal. (exists pfa_gap_append_exists_newcoefficientscoefficientdiagonalbound. pfa_gap_append_exists_newcoefficientscoefficientdiagonalbound + S (pfc_index_append_exists_newcoefficientscoefficientdiagonal) = (S (pfc_index_append_exists_newcoefficients))) -> exists pfc_value_append_exists_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_exists_newcoefficientscoefficientdiagonalentry. ff_h_pfp_append_exists_newcoefficientscoefficientdiagonalentry + S (pfc_value_append_exists_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_exists_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_exists_newcoefficientscoefficient)) /\ exists ff_q_pfp_append_exists_newcoefficientscoefficientdiagonalentry. pfc_terms_code_append_exists_newcoefficientscoefficient = ff_q_pfp_append_exists_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_exists_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_exists_newcoefficientscoefficient) + (pfc_value_append_exists_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm pfc_left_append_exists_newcoefficientscoefficientdiagonalterm pfc_right_append_exists_newcoefficientscoefficientdiagonalterm. (((pfc_index_append_exists_newcoefficientscoefficientdiagonal)+pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm=(pfc_index_append_exists_newcoefficients)) /\ ((((((exists pfa_gap_append_exists_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_exists_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_exists_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_exists_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_exists_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_exists_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_exists_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_exists_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_exists_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_exists_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_exists_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_exists_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_exists_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_exists_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_exists_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_exists_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_exists_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_append_exists_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_exists_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_exists_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_exists_newcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_exists_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_exists_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_exists_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_exists_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_exists_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_exists_newcoefficientscoefficientdiagonal)=pfc_left_append_exists_newcoefficientscoefficientdiagonalterm*pfc_right_append_exists_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_exists_newcoefficientscoefficientsum fs_v_pfc_append_exists_newcoefficientscoefficientsum. ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_start. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_start. fs_u_pfc_append_exists_newcoefficientscoefficientsum = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_exists_newcoefficientscoefficient) = S ((S (S (pfc_index_append_exists_newcoefficients))) * fs_v_pfc_append_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_exists_newcoefficientscoefficientsum = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_exists_newcoefficients))) * fs_v_pfc_append_exists_newcoefficientscoefficientsum) + (pfc_natural_sum_append_exists_newcoefficientscoefficient))) /\ forall fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_exists_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_exists_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps = S (pfc_index_append_exists_newcoefficients)) -> exists fs_a_pfc_append_exists_newcoefficientscoefficientsum_body_steps fs_r_pfc_append_exists_newcoefficientscoefficientsum_body_steps fs_s_pfc_append_exists_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_exists_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_exists_newcoefficientscoefficient)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_exists_newcoefficientscoefficient = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_exists_newcoefficientscoefficient) + (fs_a_pfc_append_exists_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_exists_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_exists_newcoefficientscoefficientsum = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum) + (fs_r_pfc_append_exists_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_exists_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_exists_newcoefficientscoefficientsum = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum) + (fs_s_pfc_append_exists_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_exists_newcoefficientscoefficientsum_body_steps = fs_r_pfc_append_exists_newcoefficientscoefficientsum_body_steps + fs_a_pfc_append_exists_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_exists_newcoefficientscoefficientresiduebound. pfa_gap_append_exists_newcoefficientscoefficientresiduebound + S (pfc_value_append_exists_newcoefficients) = (p)) /\ ((exists pfa_offset_left_append_exists_newcoefficientscoefficientresiduecongruence pfa_offset_right_append_exists_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_exists_newcoefficientscoefficient) + (p) * pfa_offset_left_append_exists_newcoefficientscoefficientresiduecongruence = (pfc_value_append_exists_newcoefficients) + (p) * pfa_offset_right_append_exists_newcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall mdr_i_pfp_append_exists_result_shiftprefix mdr_a_pfp_append_exists_result_shiftprefix. (exists mdr_gap_pfp_append_exists_result_shiftprefixb. mdr_gap_pfp_append_exists_result_shiftprefixb + S (mdr_i_pfp_append_exists_result_shiftprefix) = (N)) -> (((exists ff_h_mdr_pfp_append_exists_result_shiftprefixo. ff_h_mdr_pfp_append_exists_result_shiftprefixo + S (mdr_a_pfp_append_exists_result_shiftprefix) = S ((S (mdr_i_pfp_append_exists_result_shiftprefix)) * pc)) /\ exists ff_q_mdr_pfp_append_exists_result_shiftprefixo. pb = ff_q_mdr_pfp_append_exists_result_shiftprefixo * S ((S (mdr_i_pfp_append_exists_result_shiftprefix)) * pc) + (mdr_a_pfp_append_exists_result_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_exists_result_shiftprefixn. ff_h_mdr_pfp_append_exists_result_shiftprefixn + S (mdr_a_pfp_append_exists_result_shiftprefix) = S ((S (mdr_i_pfp_append_exists_result_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_append_exists_result_shiftprefixn. ub = ff_q_mdr_pfp_append_exists_result_shiftprefixn * S ((S (mdr_i_pfp_append_exists_result_shiftprefix)) * uc) + (mdr_a_pfp_append_exists_result_shiftprefix)))) /\ ((((exists ff_h_pfp_append_exists_result_shiftlast. ff_h_pfp_append_exists_result_shiftlast + S (0) = S ((S (N)) * uc)) /\ exists ff_q_pfp_append_exists_result_shiftlast. ub = ff_q_pfp_append_exists_result_shiftlast * S ((S (N)) * uc) + (0)))))) /\ (((((exists pfa_gap_append_exists_result_scalescalar. pfa_gap_append_exists_result_scalescalar + S (c) = (p)) /\ ((forall pfp_index_append_exists_result_scale. (exists pfa_gap_append_exists_result_scaleindex. pfa_gap_append_exists_result_scaleindex + S (pfp_index_append_exists_result_scale) = (L)) -> exists pfp_source_append_exists_result_scale pfp_value_append_exists_result_scale. ((((exists ff_h_pfp_append_exists_result_scalesource. ff_h_pfp_append_exists_result_scalesource + S (pfp_source_append_exists_result_scale) = S ((S (pfp_index_append_exists_result_scale)) * ac)) /\ exists ff_q_pfp_append_exists_result_scalesource. ab = ff_q_pfp_append_exists_result_scalesource * S ((S (pfp_index_append_exists_result_scale)) * ac) + (pfp_source_append_exists_result_scale))) /\ (((((exists ff_h_pfp_append_exists_result_scaletarget. ff_h_pfp_append_exists_result_scaletarget + S (pfp_value_append_exists_result_scale) = S ((S (pfp_index_append_exists_result_scale)) * vc)) /\ exists ff_q_pfp_append_exists_result_scaletarget. vb = ff_q_pfp_append_exists_result_scaletarget * S ((S (pfp_index_append_exists_result_scale)) * vc) + (pfp_value_append_exists_result_scale))) /\ ((((exists pfa_gap_append_exists_result_scaleoperationleft. pfa_gap_append_exists_result_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_append_exists_result_scaleoperationright. pfa_gap_append_exists_result_scaleoperationright + S (pfp_source_append_exists_result_scale) = (p)) /\ ((((exists pfa_gap_append_exists_result_scaleoperationresultbound. pfa_gap_append_exists_result_scaleoperationresultbound + S (pfp_value_append_exists_result_scale) = (p)) /\ ((exists pfa_offset_left_append_exists_result_scaleoperationresultcongruence pfa_offset_right_append_exists_result_scaleoperationresultcongruence. ((c) * (pfp_source_append_exists_result_scale)) + (p) * pfa_offset_left_append_exists_result_scaleoperationresultcongruence = (pfp_value_append_exists_result_scale) + (p) * pfa_offset_right_append_exists_result_scaleoperationresultcongruence))))))))))))))))) /\ (((((forall pfp_repeat_index_append_exists_result_leftzeros. (exists pfa_gap_append_exists_result_leftzerosindex. pfa_gap_append_exists_result_leftzerosindex + S (pfp_repeat_index_append_exists_result_leftzeros) = (L)) -> (((exists ff_h_pfp_append_exists_result_leftzerosentry. ff_h_pfp_append_exists_result_leftzerosentry + S (0) = S ((S (pfp_repeat_index_append_exists_result_leftzeros)) * UC)) /\ exists ff_q_pfp_append_exists_result_leftzerosentry. UB = ff_q_pfp_append_exists_result_leftzerosentry * S ((S (pfp_repeat_index_append_exists_result_leftzeros)) * UC) + (0)))) /\ ((forall pfrep_index_append_exists_result_left pfrep_value_append_exists_result_left. (exists pfa_gap_append_exists_result_leftbound. pfa_gap_append_exists_result_leftbound + S (pfrep_index_append_exists_result_left) = (S N)) -> (((exists ff_h_pfp_append_exists_result_leftinput. ff_h_pfp_append_exists_result_leftinput + S (pfrep_value_append_exists_result_left) = S ((S (pfrep_index_append_exists_result_left)) * uc)) /\ exists ff_q_pfp_append_exists_result_leftinput. ub = ff_q_pfp_append_exists_result_leftinput * S ((S (pfrep_index_append_exists_result_left)) * uc) + (pfrep_value_append_exists_result_left))) -> (((exists ff_h_pfp_append_exists_result_leftoutput. ff_h_pfp_append_exists_result_leftoutput + S (pfrep_value_append_exists_result_left) = S ((S ((L)+pfrep_index_append_exists_result_left)) * UC)) /\ exists ff_q_pfp_append_exists_result_leftoutput. UB = ff_q_pfp_append_exists_result_leftoutput * S ((S ((L)+pfrep_index_append_exists_result_left)) * UC) + (pfrep_value_append_exists_result_left))))))) /\ (((((forall pfp_repeat_index_append_exists_result_rightzeros. (exists pfa_gap_append_exists_result_rightzerosindex. pfa_gap_append_exists_result_rightzerosindex + S (pfp_repeat_index_append_exists_result_rightzeros) = (S N)) -> (((exists ff_h_pfp_append_exists_result_rightzerosentry. ff_h_pfp_append_exists_result_rightzerosentry + S (0) = S ((S (pfp_repeat_index_append_exists_result_rightzeros)) * VC)) /\ exists ff_q_pfp_append_exists_result_rightzerosentry. VB = ff_q_pfp_append_exists_result_rightzerosentry * S ((S (pfp_repeat_index_append_exists_result_rightzeros)) * VC) + (0)))) /\ ((forall pfrep_index_append_exists_result_right pfrep_value_append_exists_result_right. (exists pfa_gap_append_exists_result_rightbound. pfa_gap_append_exists_result_rightbound + S (pfrep_index_append_exists_result_right) = (L)) -> (((exists ff_h_pfp_append_exists_result_rightinput. ff_h_pfp_append_exists_result_rightinput + S (pfrep_value_append_exists_result_right) = S ((S (pfrep_index_append_exists_result_right)) * vc)) /\ exists ff_q_pfp_append_exists_result_rightinput. vb = ff_q_pfp_append_exists_result_rightinput * S ((S (pfrep_index_append_exists_result_right)) * vc) + (pfrep_value_append_exists_result_right))) -> (((exists ff_h_pfp_append_exists_result_rightoutput. ff_h_pfp_append_exists_result_rightoutput + S (pfrep_value_append_exists_result_right) = S ((S ((S N)+pfrep_index_append_exists_result_right)) * VC)) /\ exists ff_q_pfp_append_exists_result_rightoutput. VB = ff_q_pfp_append_exists_result_rightoutput * S ((S ((S N)+pfrep_index_append_exists_result_right)) * VC) + (pfrep_value_append_exists_result_right))))))) /\ (((forall pfp_index_append_exists_result_sum. (exists pfa_gap_append_exists_result_sumindex. pfa_gap_append_exists_result_sumindex + S (pfp_index_append_exists_result_sum) = (L+S N)) -> exists pfp_left_append_exists_result_sum pfp_right_append_exists_result_sum pfp_value_append_exists_result_sum. ((((exists ff_h_pfp_append_exists_result_sumleft. ff_h_pfp_append_exists_result_sumleft + S (pfp_left_append_exists_result_sum) = S ((S (pfp_index_append_exists_result_sum)) * UC)) /\ exists ff_q_pfp_append_exists_result_sumleft. UB = ff_q_pfp_append_exists_result_sumleft * S ((S (pfp_index_append_exists_result_sum)) * UC) + (pfp_left_append_exists_result_sum))) /\ (((((exists ff_h_pfp_append_exists_result_sumright. ff_h_pfp_append_exists_result_sumright + S (pfp_right_append_exists_result_sum) = S ((S (pfp_index_append_exists_result_sum)) * VC)) /\ exists ff_q_pfp_append_exists_result_sumright. VB = ff_q_pfp_append_exists_result_sumright * S ((S (pfp_index_append_exists_result_sum)) * VC) + (pfp_right_append_exists_result_sum))) /\ (((((exists ff_h_pfp_append_exists_result_sumtarget. ff_h_pfp_append_exists_result_sumtarget + S (pfp_value_append_exists_result_sum) = S ((S (pfp_index_append_exists_result_sum)) * rc)) /\ exists ff_q_pfp_append_exists_result_sumtarget. rb = ff_q_pfp_append_exists_result_sumtarget * S ((S (pfp_index_append_exists_result_sum)) * rc) + (pfp_value_append_exists_result_sum))) /\ ((((exists pfa_gap_append_exists_result_sumoperationleft. pfa_gap_append_exists_result_sumoperationleft + S (pfp_left_append_exists_result_sum) = (p)) /\ (((exists pfa_gap_append_exists_result_sumoperationright. pfa_gap_append_exists_result_sumoperationright + S (pfp_right_append_exists_result_sum) = (p)) /\ ((((exists pfa_gap_append_exists_result_sumoperationresultbound. pfa_gap_append_exists_result_sumoperationresultbound + S (pfp_value_append_exists_result_sum) = (p)) /\ ((exists pfa_offset_left_append_exists_result_sumoperationresultcongruence pfa_offset_right_append_exists_result_sumoperationresultcongruence. ((pfp_left_append_exists_result_sum) + (pfp_right_append_exists_result_sum)) + (p) * pfa_offset_left_append_exists_result_sumoperationresultcongruence = (pfp_value_append_exists_result_sum) + (p) * pfa_offset_right_append_exists_result_sumoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_append_exists_equivalence pfrep_left_append_exists_equivalence pfrep_right_append_exists_equivalence. ((exists pfrep_position_append_exists_equivalencefirst. ((pfrep_position_append_exists_equivalencefirst+S (pfrep_power_append_exists_equivalence)=(K)) /\ ((((exists ff_h_pfp_append_exists_equivalencefirstentry. ff_h_pfp_append_exists_equivalencefirstentry + S (pfrep_left_append_exists_equivalence) = S ((S (pfrep_position_append_exists_equivalencefirst)) * qc)) /\ exists ff_q_pfp_append_exists_equivalencefirstentry. qb = ff_q_pfp_append_exists_equivalencefirstentry * S ((S (pfrep_position_append_exists_equivalencefirst)) * qc) + (pfrep_left_append_exists_equivalence)))))) \/ (((exists pfrep_gap_append_exists_equivalencefirstoutside. pfrep_gap_append_exists_equivalencefirstoutside+(K)=(pfrep_power_append_exists_equivalence)) /\ (((pfrep_left_append_exists_equivalence)=0))))) -> ((exists pfrep_position_append_exists_equivalencesecond. ((pfrep_position_append_exists_equivalencesecond+S (pfrep_power_append_exists_equivalence)=(L+S N)) /\ ((((exists ff_h_pfp_append_exists_equivalencesecondentry. ff_h_pfp_append_exists_equivalencesecondentry + S (pfrep_right_append_exists_equivalence) = S ((S (pfrep_position_append_exists_equivalencesecond)) * rc)) /\ exists ff_q_pfp_append_exists_equivalencesecondentry. rb = ff_q_pfp_append_exists_equivalencesecondentry * S ((S (pfrep_position_append_exists_equivalencesecond)) * rc) + (pfrep_right_append_exists_equivalence)))))) \/ (((exists pfrep_gap_append_exists_equivalencesecondoutside. pfrep_gap_append_exists_equivalencesecondoutside+(L+S N)=(pfrep_power_append_exists_equivalence)) /\ (((pfrep_right_append_exists_equivalence)=0))))) -> pfrep_left_append_exists_equivalence=pfrep_right_append_exists_equivalence))))))))))))))))))