prime_field_polynomial_convolution_right_append_equivalent

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M c db dc pb pc N qb qc K ub uc vb vc UB UC VB VC rb rc. (~((p) = 1) /\ forall pfa_factor_left_append_recurrence_prime pfa_factor_right_append_recurrence_prime. (p) = pfa_factor_left_append_recurrence_prime * pfa_factor_right_append_recurrence_prime -> pfa_factor_left_append_recurrence_prime = 1 \/ pfa_factor_right_append_recurrence_prime = 1) -> (forall mdr_i_pfp_append_recurrence_preserve mdr_a_pfp_append_recurrence_preserve. (exists mdr_gap_pfp_append_recurrence_preserveb. mdr_gap_pfp_append_recurrence_preserveb + S (mdr_i_pfp_append_recurrence_preserve) = (M)) -> (((exists ff_h_mdr_pfp_append_recurrence_preserveo. ff_h_mdr_pfp_append_recurrence_preserveo + S (mdr_a_pfp_append_recurrence_preserve) = S ((S (mdr_i_pfp_append_recurrence_preserve)) * bc)) /\ exists ff_q_mdr_pfp_append_recurrence_preserveo. bb = ff_q_mdr_pfp_append_recurrence_preserveo * S ((S (mdr_i_pfp_append_recurrence_preserve)) * bc) + (mdr_a_pfp_append_recurrence_preserve))) -> (((exists ff_h_mdr_pfp_append_recurrence_preserven. ff_h_mdr_pfp_append_recurrence_preserven + S (mdr_a_pfp_append_recurrence_preserve) = S ((S (mdr_i_pfp_append_recurrence_preserve)) * dc)) /\ exists ff_q_mdr_pfp_append_recurrence_preserven. db = ff_q_mdr_pfp_append_recurrence_preserven * S ((S (mdr_i_pfp_append_recurrence_preserve)) * dc) + (mdr_a_pfp_append_recurrence_preserve)))) -> (((exists ff_h_pfp_append_recurrence_last. ff_h_pfp_append_recurrence_last + S (c) = S ((S (M)) * dc)) /\ exists ff_q_pfp_append_recurrence_last. db = ff_q_pfp_append_recurrence_last * S ((S (M)) * dc) + (c))) -> (((forall fom_index_pfp_append_recurrence_oldleft. (exists fom_gap_pfp_append_recurrence_oldleft_index_bound. fom_gap_pfp_append_recurrence_oldleft_index_bound + S (fom_index_pfp_append_recurrence_oldleft) = L) -> exists fom_value_pfp_append_recurrence_oldleft. ((((exists fom_beta_height_pfp_append_recurrence_oldleft_entry. fom_beta_height_pfp_append_recurrence_oldleft_entry + S (fom_value_pfp_append_recurrence_oldleft) = S ((S (fom_index_pfp_append_recurrence_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_recurrence_oldleft_entry. ab = fom_beta_quotient_pfp_append_recurrence_oldleft_entry * S ((S (fom_index_pfp_append_recurrence_oldleft)) * ac) + (fom_value_pfp_append_recurrence_oldleft))) /\ (exists fom_gap_pfp_append_recurrence_oldleft_value_bound. fom_gap_pfp_append_recurrence_oldleft_value_bound + S (fom_value_pfp_append_recurrence_oldleft) = p))) /\ (((forall fom_index_pfp_append_recurrence_oldright. (exists fom_gap_pfp_append_recurrence_oldright_index_bound. fom_gap_pfp_append_recurrence_oldright_index_bound + S (fom_index_pfp_append_recurrence_oldright) = M) -> exists fom_value_pfp_append_recurrence_oldright. ((((exists fom_beta_height_pfp_append_recurrence_oldright_entry. fom_beta_height_pfp_append_recurrence_oldright_entry + S (fom_value_pfp_append_recurrence_oldright) = S ((S (fom_index_pfp_append_recurrence_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_append_recurrence_oldright_entry. bb = fom_beta_quotient_pfp_append_recurrence_oldright_entry * S ((S (fom_index_pfp_append_recurrence_oldright)) * bc) + (fom_value_pfp_append_recurrence_oldright))) /\ (exists fom_gap_pfp_append_recurrence_oldright_value_bound. fom_gap_pfp_append_recurrence_oldright_value_bound + S (fom_value_pfp_append_recurrence_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_append_recurrence_oldcoefficients. (exists pfa_gap_append_recurrence_oldcoefficientsbound. pfa_gap_append_recurrence_oldcoefficientsbound + S (pfc_index_append_recurrence_oldcoefficients) = (N)) -> exists pfc_value_append_recurrence_oldcoefficients. ((((exists ff_h_pfp_append_recurrence_oldcoefficientsentry. ff_h_pfp_append_recurrence_oldcoefficientsentry + S (pfc_value_append_recurrence_oldcoefficients) = S ((S (pfc_index_append_recurrence_oldcoefficients)) * pc)) /\ exists ff_q_pfp_append_recurrence_oldcoefficientsentry. pb = ff_q_pfp_append_recurrence_oldcoefficientsentry * S ((S (pfc_index_append_recurrence_oldcoefficients)) * pc) + (pfc_value_append_recurrence_oldcoefficients))) /\ ((exists pfc_terms_code_append_recurrence_oldcoefficientscoefficient pfc_terms_scale_append_recurrence_oldcoefficientscoefficient pfc_natural_sum_append_recurrence_oldcoefficientscoefficient. ((forall pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal. (exists pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonalbound. pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonalbound + S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal) = (S (pfc_index_append_recurrence_oldcoefficients))) -> exists pfc_value_append_recurrence_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonalentry + S (pfc_value_append_recurrence_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_recurrence_oldcoefficientscoefficient)) /\ exists ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_append_recurrence_oldcoefficientscoefficient = ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_recurrence_oldcoefficientscoefficient) + (pfc_value_append_recurrence_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm. (((pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)+pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm=(pfc_index_append_recurrence_oldcoefficients)) /\ ((((((exists pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_recurrence_oldcoefficientscoefficientdiagonal)=pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm*pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_start. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_start. fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_recurrence_oldcoefficientscoefficient) = S ((S (S (pfc_index_append_recurrence_oldcoefficients))) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_recurrence_oldcoefficients))) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum) + (pfc_natural_sum_append_recurrence_oldcoefficientscoefficient))) /\ forall fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps = S (pfc_index_append_recurrence_oldcoefficients)) -> exists fs_a_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps fs_r_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps fs_s_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_recurrence_oldcoefficientscoefficient)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_recurrence_oldcoefficientscoefficient = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_recurrence_oldcoefficientscoefficient) + (fs_a_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum) + (fs_r_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum) + (fs_s_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_recurrence_oldcoefficientscoefficientresiduebound. pfa_gap_append_recurrence_oldcoefficientscoefficientresiduebound + S (pfc_value_append_recurrence_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_append_recurrence_oldcoefficientscoefficientresiduecongruence pfa_offset_right_append_recurrence_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_recurrence_oldcoefficientscoefficient) + (p) * pfa_offset_left_append_recurrence_oldcoefficientscoefficientresiduecongruence = (pfc_value_append_recurrence_oldcoefficients) + (p) * pfa_offset_right_append_recurrence_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_recurrence_newleft. (exists fom_gap_pfp_append_recurrence_newleft_index_bound. fom_gap_pfp_append_recurrence_newleft_index_bound + S (fom_index_pfp_append_recurrence_newleft) = L) -> exists fom_value_pfp_append_recurrence_newleft. ((((exists fom_beta_height_pfp_append_recurrence_newleft_entry. fom_beta_height_pfp_append_recurrence_newleft_entry + S (fom_value_pfp_append_recurrence_newleft) = S ((S (fom_index_pfp_append_recurrence_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_recurrence_newleft_entry. ab = fom_beta_quotient_pfp_append_recurrence_newleft_entry * S ((S (fom_index_pfp_append_recurrence_newleft)) * ac) + (fom_value_pfp_append_recurrence_newleft))) /\ (exists fom_gap_pfp_append_recurrence_newleft_value_bound. fom_gap_pfp_append_recurrence_newleft_value_bound + S (fom_value_pfp_append_recurrence_newleft) = p))) /\ (((forall fom_index_pfp_append_recurrence_newright. (exists fom_gap_pfp_append_recurrence_newright_index_bound. fom_gap_pfp_append_recurrence_newright_index_bound + S (fom_index_pfp_append_recurrence_newright) = S M) -> exists fom_value_pfp_append_recurrence_newright. ((((exists fom_beta_height_pfp_append_recurrence_newright_entry. fom_beta_height_pfp_append_recurrence_newright_entry + S (fom_value_pfp_append_recurrence_newright) = S ((S (fom_index_pfp_append_recurrence_newright)) * dc)) /\ exists fom_beta_quotient_pfp_append_recurrence_newright_entry. db = fom_beta_quotient_pfp_append_recurrence_newright_entry * S ((S (fom_index_pfp_append_recurrence_newright)) * dc) + (fom_value_pfp_append_recurrence_newright))) /\ (exists fom_gap_pfp_append_recurrence_newright_value_bound. fom_gap_pfp_append_recurrence_newright_value_bound + S (fom_value_pfp_append_recurrence_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_append_recurrence_newcoefficients. (exists pfa_gap_append_recurrence_newcoefficientsbound. pfa_gap_append_recurrence_newcoefficientsbound + S (pfc_index_append_recurrence_newcoefficients) = (K)) -> exists pfc_value_append_recurrence_newcoefficients. ((((exists ff_h_pfp_append_recurrence_newcoefficientsentry. ff_h_pfp_append_recurrence_newcoefficientsentry + S (pfc_value_append_recurrence_newcoefficients) = S ((S (pfc_index_append_recurrence_newcoefficients)) * qc)) /\ exists ff_q_pfp_append_recurrence_newcoefficientsentry. qb = ff_q_pfp_append_recurrence_newcoefficientsentry * S ((S (pfc_index_append_recurrence_newcoefficients)) * qc) + (pfc_value_append_recurrence_newcoefficients))) /\ ((exists pfc_terms_code_append_recurrence_newcoefficientscoefficient pfc_terms_scale_append_recurrence_newcoefficientscoefficient pfc_natural_sum_append_recurrence_newcoefficientscoefficient. ((forall pfc_index_append_recurrence_newcoefficientscoefficientdiagonal. (exists pfa_gap_append_recurrence_newcoefficientscoefficientdiagonalbound. pfa_gap_append_recurrence_newcoefficientscoefficientdiagonalbound + S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal) = (S (pfc_index_append_recurrence_newcoefficients))) -> exists pfc_value_append_recurrence_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonalentry. ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonalentry + S (pfc_value_append_recurrence_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_recurrence_newcoefficientscoefficient)) /\ exists ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonalentry. pfc_terms_code_append_recurrence_newcoefficientscoefficient = ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_recurrence_newcoefficientscoefficient) + (pfc_value_append_recurrence_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm. (((pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)+pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm=(pfc_index_append_recurrence_newcoefficients)) /\ ((((((exists pfa_gap_append_recurrence_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_recurrence_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_recurrence_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_recurrence_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_recurrence_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_recurrence_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_recurrence_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_recurrence_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_recurrence_newcoefficientscoefficientdiagonal)=pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm*pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_recurrence_newcoefficientscoefficientsum fs_v_pfc_append_recurrence_newcoefficientscoefficientsum. ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_start. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_start. fs_u_pfc_append_recurrence_newcoefficientscoefficientsum = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_recurrence_newcoefficientscoefficient) = S ((S (S (pfc_index_append_recurrence_newcoefficients))) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_recurrence_newcoefficientscoefficientsum = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_recurrence_newcoefficients))) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum) + (pfc_natural_sum_append_recurrence_newcoefficientscoefficient))) /\ forall fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps = S (pfc_index_append_recurrence_newcoefficients)) -> exists fs_a_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps fs_r_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps fs_s_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_recurrence_newcoefficientscoefficient)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_recurrence_newcoefficientscoefficient = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_recurrence_newcoefficientscoefficient) + (fs_a_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_recurrence_newcoefficientscoefficientsum = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum) + (fs_r_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_recurrence_newcoefficientscoefficientsum = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum) + (fs_s_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps = fs_r_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps + fs_a_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_recurrence_newcoefficientscoefficientresiduebound. pfa_gap_append_recurrence_newcoefficientscoefficientresiduebound + S (pfc_value_append_recurrence_newcoefficients) = (p)) /\ ((exists pfa_offset_left_append_recurrence_newcoefficientscoefficientresiduecongruence pfa_offset_right_append_recurrence_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_recurrence_newcoefficientscoefficient) + (p) * pfa_offset_left_append_recurrence_newcoefficientscoefficientresiduecongruence = (pfc_value_append_recurrence_newcoefficients) + (p) * pfa_offset_right_append_recurrence_newcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall mdr_i_pfp_append_recurrence_shiftprefix mdr_a_pfp_append_recurrence_shiftprefix. (exists mdr_gap_pfp_append_recurrence_shiftprefixb. mdr_gap_pfp_append_recurrence_shiftprefixb + S (mdr_i_pfp_append_recurrence_shiftprefix) = (N)) -> (((exists ff_h_mdr_pfp_append_recurrence_shiftprefixo. ff_h_mdr_pfp_append_recurrence_shiftprefixo + S (mdr_a_pfp_append_recurrence_shiftprefix) = S ((S (mdr_i_pfp_append_recurrence_shiftprefix)) * pc)) /\ exists ff_q_mdr_pfp_append_recurrence_shiftprefixo. pb = ff_q_mdr_pfp_append_recurrence_shiftprefixo * S ((S (mdr_i_pfp_append_recurrence_shiftprefix)) * pc) + (mdr_a_pfp_append_recurrence_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_recurrence_shiftprefixn. ff_h_mdr_pfp_append_recurrence_shiftprefixn + S (mdr_a_pfp_append_recurrence_shiftprefix) = S ((S (mdr_i_pfp_append_recurrence_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_append_recurrence_shiftprefixn. ub = ff_q_mdr_pfp_append_recurrence_shiftprefixn * S ((S (mdr_i_pfp_append_recurrence_shiftprefix)) * uc) + (mdr_a_pfp_append_recurrence_shiftprefix)))) /\ ((((exists ff_h_pfp_append_recurrence_shiftlast. ff_h_pfp_append_recurrence_shiftlast + S (0) = S ((S (N)) * uc)) /\ exists ff_q_pfp_append_recurrence_shiftlast. ub = ff_q_pfp_append_recurrence_shiftlast * S ((S (N)) * uc) + (0)))))) -> (((exists pfa_gap_append_recurrence_scalescalar. pfa_gap_append_recurrence_scalescalar + S (c) = (p)) /\ ((forall pfp_index_append_recurrence_scale. (exists pfa_gap_append_recurrence_scaleindex. pfa_gap_append_recurrence_scaleindex + S (pfp_index_append_recurrence_scale) = (L)) -> exists pfp_source_append_recurrence_scale pfp_value_append_recurrence_scale. ((((exists ff_h_pfp_append_recurrence_scalesource. ff_h_pfp_append_recurrence_scalesource + S (pfp_source_append_recurrence_scale) = S ((S (pfp_index_append_recurrence_scale)) * ac)) /\ exists ff_q_pfp_append_recurrence_scalesource. ab = ff_q_pfp_append_recurrence_scalesource * S ((S (pfp_index_append_recurrence_scale)) * ac) + (pfp_source_append_recurrence_scale))) /\ (((((exists ff_h_pfp_append_recurrence_scaletarget. ff_h_pfp_append_recurrence_scaletarget + S (pfp_value_append_recurrence_scale) = S ((S (pfp_index_append_recurrence_scale)) * vc)) /\ exists ff_q_pfp_append_recurrence_scaletarget. vb = ff_q_pfp_append_recurrence_scaletarget * S ((S (pfp_index_append_recurrence_scale)) * vc) + (pfp_value_append_recurrence_scale))) /\ ((((exists pfa_gap_append_recurrence_scaleoperationleft. pfa_gap_append_recurrence_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_append_recurrence_scaleoperationright. pfa_gap_append_recurrence_scaleoperationright + S (pfp_source_append_recurrence_scale) = (p)) /\ ((((exists pfa_gap_append_recurrence_scaleoperationresultbound. pfa_gap_append_recurrence_scaleoperationresultbound + S (pfp_value_append_recurrence_scale) = (p)) /\ ((exists pfa_offset_left_append_recurrence_scaleoperationresultcongruence pfa_offset_right_append_recurrence_scaleoperationresultcongruence. ((c) * (pfp_source_append_recurrence_scale)) + (p) * pfa_offset_left_append_recurrence_scaleoperationresultcongruence = (pfp_value_append_recurrence_scale) + (p) * pfa_offset_right_append_recurrence_scaleoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_append_recurrence_leftzeros. (exists pfa_gap_append_recurrence_leftzerosindex. pfa_gap_append_recurrence_leftzerosindex + S (pfp_repeat_index_append_recurrence_leftzeros) = (L)) -> (((exists ff_h_pfp_append_recurrence_leftzerosentry. ff_h_pfp_append_recurrence_leftzerosentry + S (0) = S ((S (pfp_repeat_index_append_recurrence_leftzeros)) * UC)) /\ exists ff_q_pfp_append_recurrence_leftzerosentry. UB = ff_q_pfp_append_recurrence_leftzerosentry * S ((S (pfp_repeat_index_append_recurrence_leftzeros)) * UC) + (0)))) /\ ((forall pfrep_index_append_recurrence_left pfrep_value_append_recurrence_left. (exists pfa_gap_append_recurrence_leftbound. pfa_gap_append_recurrence_leftbound + S (pfrep_index_append_recurrence_left) = (S N)) -> (((exists ff_h_pfp_append_recurrence_leftinput. ff_h_pfp_append_recurrence_leftinput + S (pfrep_value_append_recurrence_left) = S ((S (pfrep_index_append_recurrence_left)) * uc)) /\ exists ff_q_pfp_append_recurrence_leftinput. ub = ff_q_pfp_append_recurrence_leftinput * S ((S (pfrep_index_append_recurrence_left)) * uc) + (pfrep_value_append_recurrence_left))) -> (((exists ff_h_pfp_append_recurrence_leftoutput. ff_h_pfp_append_recurrence_leftoutput + S (pfrep_value_append_recurrence_left) = S ((S ((L)+pfrep_index_append_recurrence_left)) * UC)) /\ exists ff_q_pfp_append_recurrence_leftoutput. UB = ff_q_pfp_append_recurrence_leftoutput * S ((S ((L)+pfrep_index_append_recurrence_left)) * UC) + (pfrep_value_append_recurrence_left))))))) -> (((forall pfp_repeat_index_append_recurrence_rightzeros. (exists pfa_gap_append_recurrence_rightzerosindex. pfa_gap_append_recurrence_rightzerosindex + S (pfp_repeat_index_append_recurrence_rightzeros) = (S N)) -> (((exists ff_h_pfp_append_recurrence_rightzerosentry. ff_h_pfp_append_recurrence_rightzerosentry + S (0) = S ((S (pfp_repeat_index_append_recurrence_rightzeros)) * VC)) /\ exists ff_q_pfp_append_recurrence_rightzerosentry. VB = ff_q_pfp_append_recurrence_rightzerosentry * S ((S (pfp_repeat_index_append_recurrence_rightzeros)) * VC) + (0)))) /\ ((forall pfrep_index_append_recurrence_right pfrep_value_append_recurrence_right. (exists pfa_gap_append_recurrence_rightbound. pfa_gap_append_recurrence_rightbound + S (pfrep_index_append_recurrence_right) = (L)) -> (((exists ff_h_pfp_append_recurrence_rightinput. ff_h_pfp_append_recurrence_rightinput + S (pfrep_value_append_recurrence_right) = S ((S (pfrep_index_append_recurrence_right)) * vc)) /\ exists ff_q_pfp_append_recurrence_rightinput. vb = ff_q_pfp_append_recurrence_rightinput * S ((S (pfrep_index_append_recurrence_right)) * vc) + (pfrep_value_append_recurrence_right))) -> (((exists ff_h_pfp_append_recurrence_rightoutput. ff_h_pfp_append_recurrence_rightoutput + S (pfrep_value_append_recurrence_right) = S ((S ((S N)+pfrep_index_append_recurrence_right)) * VC)) /\ exists ff_q_pfp_append_recurrence_rightoutput. VB = ff_q_pfp_append_recurrence_rightoutput * S ((S ((S N)+pfrep_index_append_recurrence_right)) * VC) + (pfrep_value_append_recurrence_right))))))) -> (forall pfp_index_append_recurrence_sum. (exists pfa_gap_append_recurrence_sumindex. pfa_gap_append_recurrence_sumindex + S (pfp_index_append_recurrence_sum) = (L+S N)) -> exists pfp_left_append_recurrence_sum pfp_right_append_recurrence_sum pfp_value_append_recurrence_sum. ((((exists ff_h_pfp_append_recurrence_sumleft. ff_h_pfp_append_recurrence_sumleft + S (pfp_left_append_recurrence_sum) = S ((S (pfp_index_append_recurrence_sum)) * UC)) /\ exists ff_q_pfp_append_recurrence_sumleft. UB = ff_q_pfp_append_recurrence_sumleft * S ((S (pfp_index_append_recurrence_sum)) * UC) + (pfp_left_append_recurrence_sum))) /\ (((((exists ff_h_pfp_append_recurrence_sumright. ff_h_pfp_append_recurrence_sumright + S (pfp_right_append_recurrence_sum) = S ((S (pfp_index_append_recurrence_sum)) * VC)) /\ exists ff_q_pfp_append_recurrence_sumright. VB = ff_q_pfp_append_recurrence_sumright * S ((S (pfp_index_append_recurrence_sum)) * VC) + (pfp_right_append_recurrence_sum))) /\ (((((exists ff_h_pfp_append_recurrence_sumtarget. ff_h_pfp_append_recurrence_sumtarget + S (pfp_value_append_recurrence_sum) = S ((S (pfp_index_append_recurrence_sum)) * rc)) /\ exists ff_q_pfp_append_recurrence_sumtarget. rb = ff_q_pfp_append_recurrence_sumtarget * S ((S (pfp_index_append_recurrence_sum)) * rc) + (pfp_value_append_recurrence_sum))) /\ ((((exists pfa_gap_append_recurrence_sumoperationleft. pfa_gap_append_recurrence_sumoperationleft + S (pfp_left_append_recurrence_sum) = (p)) /\ (((exists pfa_gap_append_recurrence_sumoperationright. pfa_gap_append_recurrence_sumoperationright + S (pfp_right_append_recurrence_sum) = (p)) /\ ((((exists pfa_gap_append_recurrence_sumoperationresultbound. pfa_gap_append_recurrence_sumoperationresultbound + S (pfp_value_append_recurrence_sum) = (p)) /\ ((exists pfa_offset_left_append_recurrence_sumoperationresultcongruence pfa_offset_right_append_recurrence_sumoperationresultcongruence. ((pfp_left_append_recurrence_sum) + (pfp_right_append_recurrence_sum)) + (p) * pfa_offset_left_append_recurrence_sumoperationresultcongruence = (pfp_value_append_recurrence_sum) + (p) * pfa_offset_right_append_recurrence_sumoperationresultcongruence)))))))))))))))) -> (forall pfrep_power_append_recurrence_result pfrep_left_append_recurrence_result pfrep_right_append_recurrence_result. ((exists pfrep_position_append_recurrence_resultfirst. ((pfrep_position_append_recurrence_resultfirst+S (pfrep_power_append_recurrence_result)=(K)) /\ ((((exists ff_h_pfp_append_recurrence_resultfirstentry. ff_h_pfp_append_recurrence_resultfirstentry + S (pfrep_left_append_recurrence_result) = S ((S (pfrep_position_append_recurrence_resultfirst)) * qc)) /\ exists ff_q_pfp_append_recurrence_resultfirstentry. qb = ff_q_pfp_append_recurrence_resultfirstentry * S ((S (pfrep_position_append_recurrence_resultfirst)) * qc) + (pfrep_left_append_recurrence_result)))))) \/ (((exists pfrep_gap_append_recurrence_resultfirstoutside. pfrep_gap_append_recurrence_resultfirstoutside+(K)=(pfrep_power_append_recurrence_result)) /\ (((pfrep_left_append_recurrence_result)=0))))) -> ((exists pfrep_position_append_recurrence_resultsecond. ((pfrep_position_append_recurrence_resultsecond+S (pfrep_power_append_recurrence_result)=(L+S N)) /\ ((((exists ff_h_pfp_append_recurrence_resultsecondentry. ff_h_pfp_append_recurrence_resultsecondentry + S (pfrep_right_append_recurrence_result) = S ((S (pfrep_position_append_recurrence_resultsecond)) * rc)) /\ exists ff_q_pfp_append_recurrence_resultsecondentry. rb = ff_q_pfp_append_recurrence_resultsecondentry * S ((S (pfrep_position_append_recurrence_resultsecond)) * rc) + (pfrep_right_append_recurrence_result)))))) \/ (((exists pfrep_gap_append_recurrence_resultsecondoutside. pfrep_gap_append_recurrence_resultsecondoutside+(L+S N)=(pfrep_power_append_recurrence_result)) /\ (((pfrep_right_append_recurrence_result)=0))))) -> pfrep_left_append_recurrence_result=pfrep_right_append_recurrence_result)