prime_field_polynomial_convolution_shift_scale_aligned_equivalent

Exact expanded first-order arithmetic statement

forall p c ab ac L bb bc M pb pc N qb qc K rb rc T ub uc vb vc UPb UPc VPb VPc zb zc sb sc W eb ec fb fc EPb EPc FPb FPc yb yc. (~((p) = 1) /\ forall pfa_factor_left_step_helper_prime pfa_factor_right_step_helper_prime. (p) = pfa_factor_left_step_helper_prime * pfa_factor_right_step_helper_prime -> pfa_factor_left_step_helper_prime = 1 \/ pfa_factor_right_step_helper_prime = 1) -> (((forall fom_index_pfp_step_helper_ABleft. (exists fom_gap_pfp_step_helper_ABleft_index_bound. fom_gap_pfp_step_helper_ABleft_index_bound + S (fom_index_pfp_step_helper_ABleft) = L) -> exists fom_value_pfp_step_helper_ABleft. ((((exists fom_beta_height_pfp_step_helper_ABleft_entry. fom_beta_height_pfp_step_helper_ABleft_entry + S (fom_value_pfp_step_helper_ABleft) = S ((S (fom_index_pfp_step_helper_ABleft)) * ac)) /\ exists fom_beta_quotient_pfp_step_helper_ABleft_entry. ab = fom_beta_quotient_pfp_step_helper_ABleft_entry * S ((S (fom_index_pfp_step_helper_ABleft)) * ac) + (fom_value_pfp_step_helper_ABleft))) /\ (exists fom_gap_pfp_step_helper_ABleft_value_bound. fom_gap_pfp_step_helper_ABleft_value_bound + S (fom_value_pfp_step_helper_ABleft) = p))) /\ (((forall fom_index_pfp_step_helper_ABright. (exists fom_gap_pfp_step_helper_ABright_index_bound. fom_gap_pfp_step_helper_ABright_index_bound + S (fom_index_pfp_step_helper_ABright) = M) -> exists fom_value_pfp_step_helper_ABright. ((((exists fom_beta_height_pfp_step_helper_ABright_entry. fom_beta_height_pfp_step_helper_ABright_entry + S (fom_value_pfp_step_helper_ABright) = S ((S (fom_index_pfp_step_helper_ABright)) * bc)) /\ exists fom_beta_quotient_pfp_step_helper_ABright_entry. bb = fom_beta_quotient_pfp_step_helper_ABright_entry * S ((S (fom_index_pfp_step_helper_ABright)) * bc) + (fom_value_pfp_step_helper_ABright))) /\ (exists fom_gap_pfp_step_helper_ABright_value_bound. fom_gap_pfp_step_helper_ABright_value_bound + S (fom_value_pfp_step_helper_ABright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_step_helper_ABcoefficients. (exists pfa_gap_step_helper_ABcoefficientsbound. pfa_gap_step_helper_ABcoefficientsbound + S (pfc_index_step_helper_ABcoefficients) = (N)) -> exists pfc_value_step_helper_ABcoefficients. ((((exists ff_h_pfp_step_helper_ABcoefficientsentry. ff_h_pfp_step_helper_ABcoefficientsentry + S (pfc_value_step_helper_ABcoefficients) = S ((S (pfc_index_step_helper_ABcoefficients)) * pc)) /\ exists ff_q_pfp_step_helper_ABcoefficientsentry. pb = ff_q_pfp_step_helper_ABcoefficientsentry * S ((S (pfc_index_step_helper_ABcoefficients)) * pc) + (pfc_value_step_helper_ABcoefficients))) /\ ((exists pfc_terms_code_step_helper_ABcoefficientscoefficient pfc_terms_scale_step_helper_ABcoefficientscoefficient pfc_natural_sum_step_helper_ABcoefficientscoefficient. ((forall pfc_index_step_helper_ABcoefficientscoefficientdiagonal. (exists pfa_gap_step_helper_ABcoefficientscoefficientdiagonalbound. pfa_gap_step_helper_ABcoefficientscoefficientdiagonalbound + S (pfc_index_step_helper_ABcoefficientscoefficientdiagonal) = (S (pfc_index_step_helper_ABcoefficients))) -> exists pfc_value_step_helper_ABcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_step_helper_ABcoefficientscoefficientdiagonalentry. ff_h_pfp_step_helper_ABcoefficientscoefficientdiagonalentry + S (pfc_value_step_helper_ABcoefficientscoefficientdiagonal) = S ((S (pfc_index_step_helper_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_step_helper_ABcoefficientscoefficient)) /\ exists ff_q_pfp_step_helper_ABcoefficientscoefficientdiagonalentry. pfc_terms_code_step_helper_ABcoefficientscoefficient = ff_q_pfp_step_helper_ABcoefficientscoefficientdiagonalentry * S ((S (pfc_index_step_helper_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_step_helper_ABcoefficientscoefficient) + (pfc_value_step_helper_ABcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_step_helper_ABcoefficientscoefficientdiagonalterm pfc_left_step_helper_ABcoefficientscoefficientdiagonalterm pfc_right_step_helper_ABcoefficientscoefficientdiagonalterm. (((pfc_index_step_helper_ABcoefficientscoefficientdiagonal)+pfc_complement_step_helper_ABcoefficientscoefficientdiagonalterm=(pfc_index_step_helper_ABcoefficients)) /\ ((((((exists pfa_gap_step_helper_ABcoefficientscoefficientdiagonaltermleftinside. pfa_gap_step_helper_ABcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_step_helper_ABcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_step_helper_ABcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_step_helper_ABcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_step_helper_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_step_helper_ABcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_step_helper_ABcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_step_helper_ABcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_step_helper_ABcoefficientscoefficientdiagonal)) * ac) + (pfc_left_step_helper_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_step_helper_ABcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_step_helper_ABcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_step_helper_ABcoefficientscoefficientdiagonal)) /\ (((pfc_left_step_helper_ABcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_helper_ABcoefficientscoefficientdiagonaltermrightinside. pfa_gap_step_helper_ABcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_step_helper_ABcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_step_helper_ABcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_step_helper_ABcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_step_helper_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_step_helper_ABcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_step_helper_ABcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_step_helper_ABcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_step_helper_ABcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_step_helper_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_step_helper_ABcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_step_helper_ABcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_step_helper_ABcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_step_helper_ABcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_step_helper_ABcoefficientscoefficientdiagonal)=pfc_left_step_helper_ABcoefficientscoefficientdiagonalterm*pfc_right_step_helper_ABcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_helper_ABcoefficientscoefficientsum fs_v_pfc_step_helper_ABcoefficientscoefficientsum. ((((exists fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_start. fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_helper_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_start. fs_u_pfc_step_helper_ABcoefficientscoefficientsum = fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_step_helper_ABcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_terminal. fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_step_helper_ABcoefficientscoefficient) = S ((S (S (pfc_index_step_helper_ABcoefficients))) * fs_v_pfc_step_helper_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_terminal. fs_u_pfc_step_helper_ABcoefficientscoefficientsum = fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_step_helper_ABcoefficients))) * fs_v_pfc_step_helper_ABcoefficientscoefficientsum) + (pfc_natural_sum_step_helper_ABcoefficientscoefficient))) /\ forall fs_i_pfc_step_helper_ABcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_step_helper_ABcoefficientscoefficientsum_body_steps = S (pfc_index_step_helper_ABcoefficients)) -> exists fs_a_pfc_step_helper_ABcoefficientscoefficientsum_body_steps fs_r_pfc_step_helper_ABcoefficientscoefficientsum_body_steps fs_s_pfc_step_helper_ABcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_step_helper_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_step_helper_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_step_helper_ABcoefficientscoefficient)) /\ exists fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_step_helper_ABcoefficientscoefficient = fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_step_helper_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_step_helper_ABcoefficientscoefficient) + (fs_a_pfc_step_helper_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_step_helper_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_step_helper_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_step_helper_ABcoefficientscoefficientsum = fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_step_helper_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_ABcoefficientscoefficientsum) + (fs_r_pfc_step_helper_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_step_helper_ABcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_step_helper_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_step_helper_ABcoefficientscoefficientsum = fs_q_pfc_step_helper_ABcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_step_helper_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_ABcoefficientscoefficientsum) + (fs_s_pfc_step_helper_ABcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_step_helper_ABcoefficientscoefficientsum_body_steps = fs_r_pfc_step_helper_ABcoefficientscoefficientsum_body_steps + fs_a_pfc_step_helper_ABcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_step_helper_ABcoefficientscoefficientresiduebound. pfa_gap_step_helper_ABcoefficientscoefficientresiduebound + S (pfc_value_step_helper_ABcoefficients) = (p)) /\ ((exists pfa_offset_left_step_helper_ABcoefficientscoefficientresiduecongruence pfa_offset_right_step_helper_ABcoefficientscoefficientresiduecongruence. (pfc_natural_sum_step_helper_ABcoefficientscoefficient) + (p) * pfa_offset_left_step_helper_ABcoefficientscoefficientresiduecongruence = (pfc_value_step_helper_ABcoefficients) + (p) * pfa_offset_right_step_helper_ABcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_step_helper_AQleft. (exists fom_gap_pfp_step_helper_AQleft_index_bound. fom_gap_pfp_step_helper_AQleft_index_bound + S (fom_index_pfp_step_helper_AQleft) = L) -> exists fom_value_pfp_step_helper_AQleft. ((((exists fom_beta_height_pfp_step_helper_AQleft_entry. fom_beta_height_pfp_step_helper_AQleft_entry + S (fom_value_pfp_step_helper_AQleft) = S ((S (fom_index_pfp_step_helper_AQleft)) * ac)) /\ exists fom_beta_quotient_pfp_step_helper_AQleft_entry. ab = fom_beta_quotient_pfp_step_helper_AQleft_entry * S ((S (fom_index_pfp_step_helper_AQleft)) * ac) + (fom_value_pfp_step_helper_AQleft))) /\ (exists fom_gap_pfp_step_helper_AQleft_value_bound. fom_gap_pfp_step_helper_AQleft_value_bound + S (fom_value_pfp_step_helper_AQleft) = p))) /\ (((forall fom_index_pfp_step_helper_AQright. (exists fom_gap_pfp_step_helper_AQright_index_bound. fom_gap_pfp_step_helper_AQright_index_bound + S (fom_index_pfp_step_helper_AQright) = K) -> exists fom_value_pfp_step_helper_AQright. ((((exists fom_beta_height_pfp_step_helper_AQright_entry. fom_beta_height_pfp_step_helper_AQright_entry + S (fom_value_pfp_step_helper_AQright) = S ((S (fom_index_pfp_step_helper_AQright)) * qc)) /\ exists fom_beta_quotient_pfp_step_helper_AQright_entry. qb = fom_beta_quotient_pfp_step_helper_AQright_entry * S ((S (fom_index_pfp_step_helper_AQright)) * qc) + (fom_value_pfp_step_helper_AQright))) /\ (exists fom_gap_pfp_step_helper_AQright_value_bound. fom_gap_pfp_step_helper_AQright_value_bound + S (fom_value_pfp_step_helper_AQright) = p))) /\ (((((((L)=0 \/ (K)=0) /\ (((T)=0)))) \/ (((~((L)=0)) /\ (((~((K)=0)) /\ (((L)+(K)=S (T)))))))) /\ ((forall pfc_index_step_helper_AQcoefficients. (exists pfa_gap_step_helper_AQcoefficientsbound. pfa_gap_step_helper_AQcoefficientsbound + S (pfc_index_step_helper_AQcoefficients) = (T)) -> exists pfc_value_step_helper_AQcoefficients. ((((exists ff_h_pfp_step_helper_AQcoefficientsentry. ff_h_pfp_step_helper_AQcoefficientsentry + S (pfc_value_step_helper_AQcoefficients) = S ((S (pfc_index_step_helper_AQcoefficients)) * rc)) /\ exists ff_q_pfp_step_helper_AQcoefficientsentry. rb = ff_q_pfp_step_helper_AQcoefficientsentry * S ((S (pfc_index_step_helper_AQcoefficients)) * rc) + (pfc_value_step_helper_AQcoefficients))) /\ ((exists pfc_terms_code_step_helper_AQcoefficientscoefficient pfc_terms_scale_step_helper_AQcoefficientscoefficient pfc_natural_sum_step_helper_AQcoefficientscoefficient. ((forall pfc_index_step_helper_AQcoefficientscoefficientdiagonal. (exists pfa_gap_step_helper_AQcoefficientscoefficientdiagonalbound. pfa_gap_step_helper_AQcoefficientscoefficientdiagonalbound + S (pfc_index_step_helper_AQcoefficientscoefficientdiagonal) = (S (pfc_index_step_helper_AQcoefficients))) -> exists pfc_value_step_helper_AQcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_step_helper_AQcoefficientscoefficientdiagonalentry. ff_h_pfp_step_helper_AQcoefficientscoefficientdiagonalentry + S (pfc_value_step_helper_AQcoefficientscoefficientdiagonal) = S ((S (pfc_index_step_helper_AQcoefficientscoefficientdiagonal)) * pfc_terms_scale_step_helper_AQcoefficientscoefficient)) /\ exists ff_q_pfp_step_helper_AQcoefficientscoefficientdiagonalentry. pfc_terms_code_step_helper_AQcoefficientscoefficient = ff_q_pfp_step_helper_AQcoefficientscoefficientdiagonalentry * S ((S (pfc_index_step_helper_AQcoefficientscoefficientdiagonal)) * pfc_terms_scale_step_helper_AQcoefficientscoefficient) + (pfc_value_step_helper_AQcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_step_helper_AQcoefficientscoefficientdiagonalterm pfc_left_step_helper_AQcoefficientscoefficientdiagonalterm pfc_right_step_helper_AQcoefficientscoefficientdiagonalterm. (((pfc_index_step_helper_AQcoefficientscoefficientdiagonal)+pfc_complement_step_helper_AQcoefficientscoefficientdiagonalterm=(pfc_index_step_helper_AQcoefficients)) /\ ((((((exists pfa_gap_step_helper_AQcoefficientscoefficientdiagonaltermleftinside. pfa_gap_step_helper_AQcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_step_helper_AQcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_step_helper_AQcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_step_helper_AQcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_step_helper_AQcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_step_helper_AQcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_step_helper_AQcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_step_helper_AQcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_step_helper_AQcoefficientscoefficientdiagonal)) * ac) + (pfc_left_step_helper_AQcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_step_helper_AQcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_step_helper_AQcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_step_helper_AQcoefficientscoefficientdiagonal)) /\ (((pfc_left_step_helper_AQcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_helper_AQcoefficientscoefficientdiagonaltermrightinside. pfa_gap_step_helper_AQcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_step_helper_AQcoefficientscoefficientdiagonalterm) = (K)) /\ ((((exists ff_h_pfp_step_helper_AQcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_step_helper_AQcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_step_helper_AQcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_step_helper_AQcoefficientscoefficientdiagonalterm)) * qc)) /\ exists ff_q_pfp_step_helper_AQcoefficientscoefficientdiagonaltermrightentry. qb = ff_q_pfp_step_helper_AQcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_step_helper_AQcoefficientscoefficientdiagonalterm)) * qc) + (pfc_right_step_helper_AQcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_step_helper_AQcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_step_helper_AQcoefficientscoefficientdiagonaltermrightoutside+(K)=(pfc_complement_step_helper_AQcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_step_helper_AQcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_step_helper_AQcoefficientscoefficientdiagonal)=pfc_left_step_helper_AQcoefficientscoefficientdiagonalterm*pfc_right_step_helper_AQcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_helper_AQcoefficientscoefficientsum fs_v_pfc_step_helper_AQcoefficientscoefficientsum. ((((exists fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_start. fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_helper_AQcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_start. fs_u_pfc_step_helper_AQcoefficientscoefficientsum = fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_step_helper_AQcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_terminal. fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_step_helper_AQcoefficientscoefficient) = S ((S (S (pfc_index_step_helper_AQcoefficients))) * fs_v_pfc_step_helper_AQcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_terminal. fs_u_pfc_step_helper_AQcoefficientscoefficientsum = fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_step_helper_AQcoefficients))) * fs_v_pfc_step_helper_AQcoefficientscoefficientsum) + (pfc_natural_sum_step_helper_AQcoefficientscoefficient))) /\ forall fs_i_pfc_step_helper_AQcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_step_helper_AQcoefficientscoefficientsum_body_steps = S (pfc_index_step_helper_AQcoefficients)) -> exists fs_a_pfc_step_helper_AQcoefficientscoefficientsum_body_steps fs_r_pfc_step_helper_AQcoefficientscoefficientsum_body_steps fs_s_pfc_step_helper_AQcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_step_helper_AQcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_step_helper_AQcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_step_helper_AQcoefficientscoefficient)) /\ exists fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_step_helper_AQcoefficientscoefficient = fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_step_helper_AQcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_step_helper_AQcoefficientscoefficient) + (fs_a_pfc_step_helper_AQcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_step_helper_AQcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_step_helper_AQcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_AQcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_step_helper_AQcoefficientscoefficientsum = fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_step_helper_AQcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_AQcoefficientscoefficientsum) + (fs_r_pfc_step_helper_AQcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_step_helper_AQcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_step_helper_AQcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_AQcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_step_helper_AQcoefficientscoefficientsum = fs_q_pfc_step_helper_AQcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_step_helper_AQcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_AQcoefficientscoefficientsum) + (fs_s_pfc_step_helper_AQcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_step_helper_AQcoefficientscoefficientsum_body_steps = fs_r_pfc_step_helper_AQcoefficientscoefficientsum_body_steps + fs_a_pfc_step_helper_AQcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_step_helper_AQcoefficientscoefficientresiduebound. pfa_gap_step_helper_AQcoefficientscoefficientresiduebound + S (pfc_value_step_helper_AQcoefficients) = (p)) /\ ((exists pfa_offset_left_step_helper_AQcoefficientscoefficientresiduecongruence pfa_offset_right_step_helper_AQcoefficientscoefficientresiduecongruence. (pfc_natural_sum_step_helper_AQcoefficientscoefficient) + (p) * pfa_offset_left_step_helper_AQcoefficientscoefficientresiduecongruence = (pfc_value_step_helper_AQcoefficients) + (p) * pfa_offset_right_step_helper_AQcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall mdr_i_pfp_step_helper_left_shiftprefix mdr_a_pfp_step_helper_left_shiftprefix. (exists mdr_gap_pfp_step_helper_left_shiftprefixb. mdr_gap_pfp_step_helper_left_shiftprefixb + S (mdr_i_pfp_step_helper_left_shiftprefix) = (K)) -> (((exists ff_h_mdr_pfp_step_helper_left_shiftprefixo. ff_h_mdr_pfp_step_helper_left_shiftprefixo + S (mdr_a_pfp_step_helper_left_shiftprefix) = S ((S (mdr_i_pfp_step_helper_left_shiftprefix)) * qc)) /\ exists ff_q_mdr_pfp_step_helper_left_shiftprefixo. qb = ff_q_mdr_pfp_step_helper_left_shiftprefixo * S ((S (mdr_i_pfp_step_helper_left_shiftprefix)) * qc) + (mdr_a_pfp_step_helper_left_shiftprefix))) -> (((exists ff_h_mdr_pfp_step_helper_left_shiftprefixn. ff_h_mdr_pfp_step_helper_left_shiftprefixn + S (mdr_a_pfp_step_helper_left_shiftprefix) = S ((S (mdr_i_pfp_step_helper_left_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_step_helper_left_shiftprefixn. ub = ff_q_mdr_pfp_step_helper_left_shiftprefixn * S ((S (mdr_i_pfp_step_helper_left_shiftprefix)) * uc) + (mdr_a_pfp_step_helper_left_shiftprefix)))) /\ ((((exists ff_h_pfp_step_helper_left_shiftzero. ff_h_pfp_step_helper_left_shiftzero + S (0) = S ((S (K)) * uc)) /\ exists ff_q_pfp_step_helper_left_shiftzero. ub = ff_q_pfp_step_helper_left_shiftzero * S ((S (K)) * uc) + (0)))))) -> (((exists pfa_gap_step_helper_left_scalescalar. pfa_gap_step_helper_left_scalescalar + S (c) = (p)) /\ ((forall pfp_index_step_helper_left_scale. (exists pfa_gap_step_helper_left_scaleindex. pfa_gap_step_helper_left_scaleindex + S (pfp_index_step_helper_left_scale) = (M)) -> exists pfp_source_step_helper_left_scale pfp_value_step_helper_left_scale. ((((exists ff_h_pfp_step_helper_left_scalesource. ff_h_pfp_step_helper_left_scalesource + S (pfp_source_step_helper_left_scale) = S ((S (pfp_index_step_helper_left_scale)) * bc)) /\ exists ff_q_pfp_step_helper_left_scalesource. bb = ff_q_pfp_step_helper_left_scalesource * S ((S (pfp_index_step_helper_left_scale)) * bc) + (pfp_source_step_helper_left_scale))) /\ (((((exists ff_h_pfp_step_helper_left_scaletarget. ff_h_pfp_step_helper_left_scaletarget + S (pfp_value_step_helper_left_scale) = S ((S (pfp_index_step_helper_left_scale)) * vc)) /\ exists ff_q_pfp_step_helper_left_scaletarget. vb = ff_q_pfp_step_helper_left_scaletarget * S ((S (pfp_index_step_helper_left_scale)) * vc) + (pfp_value_step_helper_left_scale))) /\ ((((exists pfa_gap_step_helper_left_scaleoperationleft. pfa_gap_step_helper_left_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_step_helper_left_scaleoperationright. pfa_gap_step_helper_left_scaleoperationright + S (pfp_source_step_helper_left_scale) = (p)) /\ ((((exists pfa_gap_step_helper_left_scaleoperationresultbound. pfa_gap_step_helper_left_scaleoperationresultbound + S (pfp_value_step_helper_left_scale) = (p)) /\ ((exists pfa_offset_left_step_helper_left_scaleoperationresultcongruence pfa_offset_right_step_helper_left_scaleoperationresultcongruence. ((c) * (pfp_source_step_helper_left_scale)) + (p) * pfa_offset_left_step_helper_left_scaleoperationresultcongruence = (pfp_value_step_helper_left_scale) + (p) * pfa_offset_right_step_helper_left_scaleoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_step_helper_left_leftzeros. (exists pfa_gap_step_helper_left_leftzerosindex. pfa_gap_step_helper_left_leftzerosindex + S (pfp_repeat_index_step_helper_left_leftzeros) = (M)) -> (((exists ff_h_pfp_step_helper_left_leftzerosentry. ff_h_pfp_step_helper_left_leftzerosentry + S (0) = S ((S (pfp_repeat_index_step_helper_left_leftzeros)) * UPc)) /\ exists ff_q_pfp_step_helper_left_leftzerosentry. UPb = ff_q_pfp_step_helper_left_leftzerosentry * S ((S (pfp_repeat_index_step_helper_left_leftzeros)) * UPc) + (0)))) /\ ((forall pfrep_index_step_helper_left_left pfrep_value_step_helper_left_left. (exists pfa_gap_step_helper_left_leftbound. pfa_gap_step_helper_left_leftbound + S (pfrep_index_step_helper_left_left) = (S K)) -> (((exists ff_h_pfp_step_helper_left_leftinput. ff_h_pfp_step_helper_left_leftinput + S (pfrep_value_step_helper_left_left) = S ((S (pfrep_index_step_helper_left_left)) * uc)) /\ exists ff_q_pfp_step_helper_left_leftinput. ub = ff_q_pfp_step_helper_left_leftinput * S ((S (pfrep_index_step_helper_left_left)) * uc) + (pfrep_value_step_helper_left_left))) -> (((exists ff_h_pfp_step_helper_left_leftoutput. ff_h_pfp_step_helper_left_leftoutput + S (pfrep_value_step_helper_left_left) = S ((S ((M)+pfrep_index_step_helper_left_left)) * UPc)) /\ exists ff_q_pfp_step_helper_left_leftoutput. UPb = ff_q_pfp_step_helper_left_leftoutput * S ((S ((M)+pfrep_index_step_helper_left_left)) * UPc) + (pfrep_value_step_helper_left_left))))))) -> (((forall pfp_repeat_index_step_helper_left_rightzeros. (exists pfa_gap_step_helper_left_rightzerosindex. pfa_gap_step_helper_left_rightzerosindex + S (pfp_repeat_index_step_helper_left_rightzeros) = (S K)) -> (((exists ff_h_pfp_step_helper_left_rightzerosentry. ff_h_pfp_step_helper_left_rightzerosentry + S (0) = S ((S (pfp_repeat_index_step_helper_left_rightzeros)) * VPc)) /\ exists ff_q_pfp_step_helper_left_rightzerosentry. VPb = ff_q_pfp_step_helper_left_rightzerosentry * S ((S (pfp_repeat_index_step_helper_left_rightzeros)) * VPc) + (0)))) /\ ((forall pfrep_index_step_helper_left_right pfrep_value_step_helper_left_right. (exists pfa_gap_step_helper_left_rightbound. pfa_gap_step_helper_left_rightbound + S (pfrep_index_step_helper_left_right) = (M)) -> (((exists ff_h_pfp_step_helper_left_rightinput. ff_h_pfp_step_helper_left_rightinput + S (pfrep_value_step_helper_left_right) = S ((S (pfrep_index_step_helper_left_right)) * vc)) /\ exists ff_q_pfp_step_helper_left_rightinput. vb = ff_q_pfp_step_helper_left_rightinput * S ((S (pfrep_index_step_helper_left_right)) * vc) + (pfrep_value_step_helper_left_right))) -> (((exists ff_h_pfp_step_helper_left_rightoutput. ff_h_pfp_step_helper_left_rightoutput + S (pfrep_value_step_helper_left_right) = S ((S ((S K)+pfrep_index_step_helper_left_right)) * VPc)) /\ exists ff_q_pfp_step_helper_left_rightoutput. VPb = ff_q_pfp_step_helper_left_rightoutput * S ((S ((S K)+pfrep_index_step_helper_left_right)) * VPc) + (pfrep_value_step_helper_left_right))))))) -> (forall pfp_index_step_helper_left_sum. (exists pfa_gap_step_helper_left_sumindex. pfa_gap_step_helper_left_sumindex + S (pfp_index_step_helper_left_sum) = (M+S K)) -> exists pfp_left_step_helper_left_sum pfp_right_step_helper_left_sum pfp_value_step_helper_left_sum. ((((exists ff_h_pfp_step_helper_left_sumleft. ff_h_pfp_step_helper_left_sumleft + S (pfp_left_step_helper_left_sum) = S ((S (pfp_index_step_helper_left_sum)) * UPc)) /\ exists ff_q_pfp_step_helper_left_sumleft. UPb = ff_q_pfp_step_helper_left_sumleft * S ((S (pfp_index_step_helper_left_sum)) * UPc) + (pfp_left_step_helper_left_sum))) /\ (((((exists ff_h_pfp_step_helper_left_sumright. ff_h_pfp_step_helper_left_sumright + S (pfp_right_step_helper_left_sum) = S ((S (pfp_index_step_helper_left_sum)) * VPc)) /\ exists ff_q_pfp_step_helper_left_sumright. VPb = ff_q_pfp_step_helper_left_sumright * S ((S (pfp_index_step_helper_left_sum)) * VPc) + (pfp_right_step_helper_left_sum))) /\ (((((exists ff_h_pfp_step_helper_left_sumtarget. ff_h_pfp_step_helper_left_sumtarget + S (pfp_value_step_helper_left_sum) = S ((S (pfp_index_step_helper_left_sum)) * zc)) /\ exists ff_q_pfp_step_helper_left_sumtarget. zb = ff_q_pfp_step_helper_left_sumtarget * S ((S (pfp_index_step_helper_left_sum)) * zc) + (pfp_value_step_helper_left_sum))) /\ ((((exists pfa_gap_step_helper_left_sumoperationleft. pfa_gap_step_helper_left_sumoperationleft + S (pfp_left_step_helper_left_sum) = (p)) /\ (((exists pfa_gap_step_helper_left_sumoperationright. pfa_gap_step_helper_left_sumoperationright + S (pfp_right_step_helper_left_sum) = (p)) /\ ((((exists pfa_gap_step_helper_left_sumoperationresultbound. pfa_gap_step_helper_left_sumoperationresultbound + S (pfp_value_step_helper_left_sum) = (p)) /\ ((exists pfa_offset_left_step_helper_left_sumoperationresultcongruence pfa_offset_right_step_helper_left_sumoperationresultcongruence. ((pfp_left_step_helper_left_sum) + (pfp_right_step_helper_left_sum)) + (p) * pfa_offset_left_step_helper_left_sumoperationresultcongruence = (pfp_value_step_helper_left_sum) + (p) * pfa_offset_right_step_helper_left_sumoperationresultcongruence)))))))))))))))) -> (((forall fom_index_pfp_step_helper_AZleft. (exists fom_gap_pfp_step_helper_AZleft_index_bound. fom_gap_pfp_step_helper_AZleft_index_bound + S (fom_index_pfp_step_helper_AZleft) = L) -> exists fom_value_pfp_step_helper_AZleft. ((((exists fom_beta_height_pfp_step_helper_AZleft_entry. fom_beta_height_pfp_step_helper_AZleft_entry + S (fom_value_pfp_step_helper_AZleft) = S ((S (fom_index_pfp_step_helper_AZleft)) * ac)) /\ exists fom_beta_quotient_pfp_step_helper_AZleft_entry. ab = fom_beta_quotient_pfp_step_helper_AZleft_entry * S ((S (fom_index_pfp_step_helper_AZleft)) * ac) + (fom_value_pfp_step_helper_AZleft))) /\ (exists fom_gap_pfp_step_helper_AZleft_value_bound. fom_gap_pfp_step_helper_AZleft_value_bound + S (fom_value_pfp_step_helper_AZleft) = p))) /\ (((forall fom_index_pfp_step_helper_AZright. (exists fom_gap_pfp_step_helper_AZright_index_bound. fom_gap_pfp_step_helper_AZright_index_bound + S (fom_index_pfp_step_helper_AZright) = M+S K) -> exists fom_value_pfp_step_helper_AZright. ((((exists fom_beta_height_pfp_step_helper_AZright_entry. fom_beta_height_pfp_step_helper_AZright_entry + S (fom_value_pfp_step_helper_AZright) = S ((S (fom_index_pfp_step_helper_AZright)) * zc)) /\ exists fom_beta_quotient_pfp_step_helper_AZright_entry. zb = fom_beta_quotient_pfp_step_helper_AZright_entry * S ((S (fom_index_pfp_step_helper_AZright)) * zc) + (fom_value_pfp_step_helper_AZright))) /\ (exists fom_gap_pfp_step_helper_AZright_value_bound. fom_gap_pfp_step_helper_AZright_value_bound + S (fom_value_pfp_step_helper_AZright) = p))) /\ (((((((L)=0 \/ (M+S K)=0) /\ (((W)=0)))) \/ (((~((L)=0)) /\ (((~((M+S K)=0)) /\ (((L)+(M+S K)=S (W)))))))) /\ ((forall pfc_index_step_helper_AZcoefficients. (exists pfa_gap_step_helper_AZcoefficientsbound. pfa_gap_step_helper_AZcoefficientsbound + S (pfc_index_step_helper_AZcoefficients) = (W)) -> exists pfc_value_step_helper_AZcoefficients. ((((exists ff_h_pfp_step_helper_AZcoefficientsentry. ff_h_pfp_step_helper_AZcoefficientsentry + S (pfc_value_step_helper_AZcoefficients) = S ((S (pfc_index_step_helper_AZcoefficients)) * sc)) /\ exists ff_q_pfp_step_helper_AZcoefficientsentry. sb = ff_q_pfp_step_helper_AZcoefficientsentry * S ((S (pfc_index_step_helper_AZcoefficients)) * sc) + (pfc_value_step_helper_AZcoefficients))) /\ ((exists pfc_terms_code_step_helper_AZcoefficientscoefficient pfc_terms_scale_step_helper_AZcoefficientscoefficient pfc_natural_sum_step_helper_AZcoefficientscoefficient. ((forall pfc_index_step_helper_AZcoefficientscoefficientdiagonal. (exists pfa_gap_step_helper_AZcoefficientscoefficientdiagonalbound. pfa_gap_step_helper_AZcoefficientscoefficientdiagonalbound + S (pfc_index_step_helper_AZcoefficientscoefficientdiagonal) = (S (pfc_index_step_helper_AZcoefficients))) -> exists pfc_value_step_helper_AZcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_step_helper_AZcoefficientscoefficientdiagonalentry. ff_h_pfp_step_helper_AZcoefficientscoefficientdiagonalentry + S (pfc_value_step_helper_AZcoefficientscoefficientdiagonal) = S ((S (pfc_index_step_helper_AZcoefficientscoefficientdiagonal)) * pfc_terms_scale_step_helper_AZcoefficientscoefficient)) /\ exists ff_q_pfp_step_helper_AZcoefficientscoefficientdiagonalentry. pfc_terms_code_step_helper_AZcoefficientscoefficient = ff_q_pfp_step_helper_AZcoefficientscoefficientdiagonalentry * S ((S (pfc_index_step_helper_AZcoefficientscoefficientdiagonal)) * pfc_terms_scale_step_helper_AZcoefficientscoefficient) + (pfc_value_step_helper_AZcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_step_helper_AZcoefficientscoefficientdiagonalterm pfc_left_step_helper_AZcoefficientscoefficientdiagonalterm pfc_right_step_helper_AZcoefficientscoefficientdiagonalterm. (((pfc_index_step_helper_AZcoefficientscoefficientdiagonal)+pfc_complement_step_helper_AZcoefficientscoefficientdiagonalterm=(pfc_index_step_helper_AZcoefficients)) /\ ((((((exists pfa_gap_step_helper_AZcoefficientscoefficientdiagonaltermleftinside. pfa_gap_step_helper_AZcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_step_helper_AZcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_step_helper_AZcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_step_helper_AZcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_step_helper_AZcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_step_helper_AZcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_step_helper_AZcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_step_helper_AZcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_step_helper_AZcoefficientscoefficientdiagonal)) * ac) + (pfc_left_step_helper_AZcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_step_helper_AZcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_step_helper_AZcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_step_helper_AZcoefficientscoefficientdiagonal)) /\ (((pfc_left_step_helper_AZcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_helper_AZcoefficientscoefficientdiagonaltermrightinside. pfa_gap_step_helper_AZcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_step_helper_AZcoefficientscoefficientdiagonalterm) = (M+S K)) /\ ((((exists ff_h_pfp_step_helper_AZcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_step_helper_AZcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_step_helper_AZcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_step_helper_AZcoefficientscoefficientdiagonalterm)) * zc)) /\ exists ff_q_pfp_step_helper_AZcoefficientscoefficientdiagonaltermrightentry. zb = ff_q_pfp_step_helper_AZcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_step_helper_AZcoefficientscoefficientdiagonalterm)) * zc) + (pfc_right_step_helper_AZcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_step_helper_AZcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_step_helper_AZcoefficientscoefficientdiagonaltermrightoutside+(M+S K)=(pfc_complement_step_helper_AZcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_step_helper_AZcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_step_helper_AZcoefficientscoefficientdiagonal)=pfc_left_step_helper_AZcoefficientscoefficientdiagonalterm*pfc_right_step_helper_AZcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_helper_AZcoefficientscoefficientsum fs_v_pfc_step_helper_AZcoefficientscoefficientsum. ((((exists fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_start. fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_helper_AZcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_start. fs_u_pfc_step_helper_AZcoefficientscoefficientsum = fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_step_helper_AZcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_terminal. fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_step_helper_AZcoefficientscoefficient) = S ((S (S (pfc_index_step_helper_AZcoefficients))) * fs_v_pfc_step_helper_AZcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_terminal. fs_u_pfc_step_helper_AZcoefficientscoefficientsum = fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_step_helper_AZcoefficients))) * fs_v_pfc_step_helper_AZcoefficientscoefficientsum) + (pfc_natural_sum_step_helper_AZcoefficientscoefficient))) /\ forall fs_i_pfc_step_helper_AZcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_step_helper_AZcoefficientscoefficientsum_body_steps = S (pfc_index_step_helper_AZcoefficients)) -> exists fs_a_pfc_step_helper_AZcoefficientscoefficientsum_body_steps fs_r_pfc_step_helper_AZcoefficientscoefficientsum_body_steps fs_s_pfc_step_helper_AZcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_step_helper_AZcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_step_helper_AZcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_step_helper_AZcoefficientscoefficient)) /\ exists fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_step_helper_AZcoefficientscoefficient = fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_step_helper_AZcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_step_helper_AZcoefficientscoefficient) + (fs_a_pfc_step_helper_AZcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_step_helper_AZcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_step_helper_AZcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_AZcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_step_helper_AZcoefficientscoefficientsum = fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_step_helper_AZcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_AZcoefficientscoefficientsum) + (fs_r_pfc_step_helper_AZcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_step_helper_AZcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_step_helper_AZcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_AZcoefficientscoefficientsum)) /\ exists fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_step_helper_AZcoefficientscoefficientsum = fs_q_pfc_step_helper_AZcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_step_helper_AZcoefficientscoefficientsum_body_steps)) * fs_v_pfc_step_helper_AZcoefficientscoefficientsum) + (fs_s_pfc_step_helper_AZcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_step_helper_AZcoefficientscoefficientsum_body_steps = fs_r_pfc_step_helper_AZcoefficientscoefficientsum_body_steps + fs_a_pfc_step_helper_AZcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_step_helper_AZcoefficientscoefficientresiduebound. pfa_gap_step_helper_AZcoefficientscoefficientresiduebound + S (pfc_value_step_helper_AZcoefficients) = (p)) /\ ((exists pfa_offset_left_step_helper_AZcoefficientscoefficientresiduecongruence pfa_offset_right_step_helper_AZcoefficientscoefficientresiduecongruence. (pfc_natural_sum_step_helper_AZcoefficientscoefficient) + (p) * pfa_offset_left_step_helper_AZcoefficientscoefficientresiduecongruence = (pfc_value_step_helper_AZcoefficients) + (p) * pfa_offset_right_step_helper_AZcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall mdr_i_pfp_step_helper_right_shiftprefix mdr_a_pfp_step_helper_right_shiftprefix. (exists mdr_gap_pfp_step_helper_right_shiftprefixb. mdr_gap_pfp_step_helper_right_shiftprefixb + S (mdr_i_pfp_step_helper_right_shiftprefix) = (T)) -> (((exists ff_h_mdr_pfp_step_helper_right_shiftprefixo. ff_h_mdr_pfp_step_helper_right_shiftprefixo + S (mdr_a_pfp_step_helper_right_shiftprefix) = S ((S (mdr_i_pfp_step_helper_right_shiftprefix)) * rc)) /\ exists ff_q_mdr_pfp_step_helper_right_shiftprefixo. rb = ff_q_mdr_pfp_step_helper_right_shiftprefixo * S ((S (mdr_i_pfp_step_helper_right_shiftprefix)) * rc) + (mdr_a_pfp_step_helper_right_shiftprefix))) -> (((exists ff_h_mdr_pfp_step_helper_right_shiftprefixn. ff_h_mdr_pfp_step_helper_right_shiftprefixn + S (mdr_a_pfp_step_helper_right_shiftprefix) = S ((S (mdr_i_pfp_step_helper_right_shiftprefix)) * ec)) /\ exists ff_q_mdr_pfp_step_helper_right_shiftprefixn. eb = ff_q_mdr_pfp_step_helper_right_shiftprefixn * S ((S (mdr_i_pfp_step_helper_right_shiftprefix)) * ec) + (mdr_a_pfp_step_helper_right_shiftprefix)))) /\ ((((exists ff_h_pfp_step_helper_right_shiftzero. ff_h_pfp_step_helper_right_shiftzero + S (0) = S ((S (T)) * ec)) /\ exists ff_q_pfp_step_helper_right_shiftzero. eb = ff_q_pfp_step_helper_right_shiftzero * S ((S (T)) * ec) + (0)))))) -> (((exists pfa_gap_step_helper_right_scalescalar. pfa_gap_step_helper_right_scalescalar + S (c) = (p)) /\ ((forall pfp_index_step_helper_right_scale. (exists pfa_gap_step_helper_right_scaleindex. pfa_gap_step_helper_right_scaleindex + S (pfp_index_step_helper_right_scale) = (N)) -> exists pfp_source_step_helper_right_scale pfp_value_step_helper_right_scale. ((((exists ff_h_pfp_step_helper_right_scalesource. ff_h_pfp_step_helper_right_scalesource + S (pfp_source_step_helper_right_scale) = S ((S (pfp_index_step_helper_right_scale)) * pc)) /\ exists ff_q_pfp_step_helper_right_scalesource. pb = ff_q_pfp_step_helper_right_scalesource * S ((S (pfp_index_step_helper_right_scale)) * pc) + (pfp_source_step_helper_right_scale))) /\ (((((exists ff_h_pfp_step_helper_right_scaletarget. ff_h_pfp_step_helper_right_scaletarget + S (pfp_value_step_helper_right_scale) = S ((S (pfp_index_step_helper_right_scale)) * fc)) /\ exists ff_q_pfp_step_helper_right_scaletarget. fb = ff_q_pfp_step_helper_right_scaletarget * S ((S (pfp_index_step_helper_right_scale)) * fc) + (pfp_value_step_helper_right_scale))) /\ ((((exists pfa_gap_step_helper_right_scaleoperationleft. pfa_gap_step_helper_right_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_step_helper_right_scaleoperationright. pfa_gap_step_helper_right_scaleoperationright + S (pfp_source_step_helper_right_scale) = (p)) /\ ((((exists pfa_gap_step_helper_right_scaleoperationresultbound. pfa_gap_step_helper_right_scaleoperationresultbound + S (pfp_value_step_helper_right_scale) = (p)) /\ ((exists pfa_offset_left_step_helper_right_scaleoperationresultcongruence pfa_offset_right_step_helper_right_scaleoperationresultcongruence. ((c) * (pfp_source_step_helper_right_scale)) + (p) * pfa_offset_left_step_helper_right_scaleoperationresultcongruence = (pfp_value_step_helper_right_scale) + (p) * pfa_offset_right_step_helper_right_scaleoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_step_helper_right_leftzeros. (exists pfa_gap_step_helper_right_leftzerosindex. pfa_gap_step_helper_right_leftzerosindex + S (pfp_repeat_index_step_helper_right_leftzeros) = (N)) -> (((exists ff_h_pfp_step_helper_right_leftzerosentry. ff_h_pfp_step_helper_right_leftzerosentry + S (0) = S ((S (pfp_repeat_index_step_helper_right_leftzeros)) * EPc)) /\ exists ff_q_pfp_step_helper_right_leftzerosentry. EPb = ff_q_pfp_step_helper_right_leftzerosentry * S ((S (pfp_repeat_index_step_helper_right_leftzeros)) * EPc) + (0)))) /\ ((forall pfrep_index_step_helper_right_left pfrep_value_step_helper_right_left. (exists pfa_gap_step_helper_right_leftbound. pfa_gap_step_helper_right_leftbound + S (pfrep_index_step_helper_right_left) = (S T)) -> (((exists ff_h_pfp_step_helper_right_leftinput. ff_h_pfp_step_helper_right_leftinput + S (pfrep_value_step_helper_right_left) = S ((S (pfrep_index_step_helper_right_left)) * ec)) /\ exists ff_q_pfp_step_helper_right_leftinput. eb = ff_q_pfp_step_helper_right_leftinput * S ((S (pfrep_index_step_helper_right_left)) * ec) + (pfrep_value_step_helper_right_left))) -> (((exists ff_h_pfp_step_helper_right_leftoutput. ff_h_pfp_step_helper_right_leftoutput + S (pfrep_value_step_helper_right_left) = S ((S ((N)+pfrep_index_step_helper_right_left)) * EPc)) /\ exists ff_q_pfp_step_helper_right_leftoutput. EPb = ff_q_pfp_step_helper_right_leftoutput * S ((S ((N)+pfrep_index_step_helper_right_left)) * EPc) + (pfrep_value_step_helper_right_left))))))) -> (((forall pfp_repeat_index_step_helper_right_rightzeros. (exists pfa_gap_step_helper_right_rightzerosindex. pfa_gap_step_helper_right_rightzerosindex + S (pfp_repeat_index_step_helper_right_rightzeros) = (S T)) -> (((exists ff_h_pfp_step_helper_right_rightzerosentry. ff_h_pfp_step_helper_right_rightzerosentry + S (0) = S ((S (pfp_repeat_index_step_helper_right_rightzeros)) * FPc)) /\ exists ff_q_pfp_step_helper_right_rightzerosentry. FPb = ff_q_pfp_step_helper_right_rightzerosentry * S ((S (pfp_repeat_index_step_helper_right_rightzeros)) * FPc) + (0)))) /\ ((forall pfrep_index_step_helper_right_right pfrep_value_step_helper_right_right. (exists pfa_gap_step_helper_right_rightbound. pfa_gap_step_helper_right_rightbound + S (pfrep_index_step_helper_right_right) = (N)) -> (((exists ff_h_pfp_step_helper_right_rightinput. ff_h_pfp_step_helper_right_rightinput + S (pfrep_value_step_helper_right_right) = S ((S (pfrep_index_step_helper_right_right)) * fc)) /\ exists ff_q_pfp_step_helper_right_rightinput. fb = ff_q_pfp_step_helper_right_rightinput * S ((S (pfrep_index_step_helper_right_right)) * fc) + (pfrep_value_step_helper_right_right))) -> (((exists ff_h_pfp_step_helper_right_rightoutput. ff_h_pfp_step_helper_right_rightoutput + S (pfrep_value_step_helper_right_right) = S ((S ((S T)+pfrep_index_step_helper_right_right)) * FPc)) /\ exists ff_q_pfp_step_helper_right_rightoutput. FPb = ff_q_pfp_step_helper_right_rightoutput * S ((S ((S T)+pfrep_index_step_helper_right_right)) * FPc) + (pfrep_value_step_helper_right_right))))))) -> (forall pfp_index_step_helper_right_sum. (exists pfa_gap_step_helper_right_sumindex. pfa_gap_step_helper_right_sumindex + S (pfp_index_step_helper_right_sum) = (N+S T)) -> exists pfp_left_step_helper_right_sum pfp_right_step_helper_right_sum pfp_value_step_helper_right_sum. ((((exists ff_h_pfp_step_helper_right_sumleft. ff_h_pfp_step_helper_right_sumleft + S (pfp_left_step_helper_right_sum) = S ((S (pfp_index_step_helper_right_sum)) * EPc)) /\ exists ff_q_pfp_step_helper_right_sumleft. EPb = ff_q_pfp_step_helper_right_sumleft * S ((S (pfp_index_step_helper_right_sum)) * EPc) + (pfp_left_step_helper_right_sum))) /\ (((((exists ff_h_pfp_step_helper_right_sumright. ff_h_pfp_step_helper_right_sumright + S (pfp_right_step_helper_right_sum) = S ((S (pfp_index_step_helper_right_sum)) * FPc)) /\ exists ff_q_pfp_step_helper_right_sumright. FPb = ff_q_pfp_step_helper_right_sumright * S ((S (pfp_index_step_helper_right_sum)) * FPc) + (pfp_right_step_helper_right_sum))) /\ (((((exists ff_h_pfp_step_helper_right_sumtarget. ff_h_pfp_step_helper_right_sumtarget + S (pfp_value_step_helper_right_sum) = S ((S (pfp_index_step_helper_right_sum)) * yc)) /\ exists ff_q_pfp_step_helper_right_sumtarget. yb = ff_q_pfp_step_helper_right_sumtarget * S ((S (pfp_index_step_helper_right_sum)) * yc) + (pfp_value_step_helper_right_sum))) /\ ((((exists pfa_gap_step_helper_right_sumoperationleft. pfa_gap_step_helper_right_sumoperationleft + S (pfp_left_step_helper_right_sum) = (p)) /\ (((exists pfa_gap_step_helper_right_sumoperationright. pfa_gap_step_helper_right_sumoperationright + S (pfp_right_step_helper_right_sum) = (p)) /\ ((((exists pfa_gap_step_helper_right_sumoperationresultbound. pfa_gap_step_helper_right_sumoperationresultbound + S (pfp_value_step_helper_right_sum) = (p)) /\ ((exists pfa_offset_left_step_helper_right_sumoperationresultcongruence pfa_offset_right_step_helper_right_sumoperationresultcongruence. ((pfp_left_step_helper_right_sum) + (pfp_right_step_helper_right_sum)) + (p) * pfa_offset_left_step_helper_right_sumoperationresultcongruence = (pfp_value_step_helper_right_sum) + (p) * pfa_offset_right_step_helper_right_sumoperationresultcongruence)))))))))))))))) -> (forall pfrep_power_step_helper_result pfrep_left_step_helper_result pfrep_right_step_helper_result. ((exists pfrep_position_step_helper_resultfirst. ((pfrep_position_step_helper_resultfirst+S (pfrep_power_step_helper_result)=(W)) /\ ((((exists ff_h_pfp_step_helper_resultfirstentry. ff_h_pfp_step_helper_resultfirstentry + S (pfrep_left_step_helper_result) = S ((S (pfrep_position_step_helper_resultfirst)) * sc)) /\ exists ff_q_pfp_step_helper_resultfirstentry. sb = ff_q_pfp_step_helper_resultfirstentry * S ((S (pfrep_position_step_helper_resultfirst)) * sc) + (pfrep_left_step_helper_result)))))) \/ (((exists pfrep_gap_step_helper_resultfirstoutside. pfrep_gap_step_helper_resultfirstoutside+(W)=(pfrep_power_step_helper_result)) /\ (((pfrep_left_step_helper_result)=0))))) -> ((exists pfrep_position_step_helper_resultsecond. ((pfrep_position_step_helper_resultsecond+S (pfrep_power_step_helper_result)=(N+S T)) /\ ((((exists ff_h_pfp_step_helper_resultsecondentry. ff_h_pfp_step_helper_resultsecondentry + S (pfrep_right_step_helper_result) = S ((S (pfrep_position_step_helper_resultsecond)) * yc)) /\ exists ff_q_pfp_step_helper_resultsecondentry. yb = ff_q_pfp_step_helper_resultsecondentry * S ((S (pfrep_position_step_helper_resultsecond)) * yc) + (pfrep_right_step_helper_result)))))) \/ (((exists pfrep_gap_step_helper_resultsecondoutside. pfrep_gap_step_helper_resultsecondoutside+(N+S T)=(pfrep_power_step_helper_result)) /\ (((pfrep_right_step_helper_result)=0))))) -> pfrep_left_step_helper_result=pfrep_right_step_helper_result)