prime_field_polynomial_convolution_equivalent_congruent_right

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M cb cc N BB BC H CB CC K. (~(p=0)) -> (forall pfrep_power_congruent_factor_right pfrep_left_congruent_factor_right pfrep_right_congruent_factor_right. ((exists pfrep_position_congruent_factor_rightfirst. ((pfrep_position_congruent_factor_rightfirst+S (pfrep_power_congruent_factor_right)=(M)) /\ ((((exists ff_h_pfp_congruent_factor_rightfirstentry. ff_h_pfp_congruent_factor_rightfirstentry + S (pfrep_left_congruent_factor_right) = S ((S (pfrep_position_congruent_factor_rightfirst)) * bc)) /\ exists ff_q_pfp_congruent_factor_rightfirstentry. bb = ff_q_pfp_congruent_factor_rightfirstentry * S ((S (pfrep_position_congruent_factor_rightfirst)) * bc) + (pfrep_left_congruent_factor_right)))))) \/ (((exists pfrep_gap_congruent_factor_rightfirstoutside. pfrep_gap_congruent_factor_rightfirstoutside+(M)=(pfrep_power_congruent_factor_right)) /\ (((pfrep_left_congruent_factor_right)=0))))) -> ((exists pfrep_position_congruent_factor_rightsecond. ((pfrep_position_congruent_factor_rightsecond+S (pfrep_power_congruent_factor_right)=(H)) /\ ((((exists ff_h_pfp_congruent_factor_rightsecondentry. ff_h_pfp_congruent_factor_rightsecondentry + S (pfrep_right_congruent_factor_right) = S ((S (pfrep_position_congruent_factor_rightsecond)) * BC)) /\ exists ff_q_pfp_congruent_factor_rightsecondentry. BB = ff_q_pfp_congruent_factor_rightsecondentry * S ((S (pfrep_position_congruent_factor_rightsecond)) * BC) + (pfrep_right_congruent_factor_right)))))) \/ (((exists pfrep_gap_congruent_factor_rightsecondoutside. pfrep_gap_congruent_factor_rightsecondoutside+(H)=(pfrep_power_congruent_factor_right)) /\ (((pfrep_right_congruent_factor_right)=0))))) -> pfrep_left_congruent_factor_right=pfrep_right_congruent_factor_right) -> (((forall fom_index_pfp_congruent_original_rightleft. (exists fom_gap_pfp_congruent_original_rightleft_index_bound. fom_gap_pfp_congruent_original_rightleft_index_bound + S (fom_index_pfp_congruent_original_rightleft) = L) -> exists fom_value_pfp_congruent_original_rightleft. ((((exists fom_beta_height_pfp_congruent_original_rightleft_entry. fom_beta_height_pfp_congruent_original_rightleft_entry + S (fom_value_pfp_congruent_original_rightleft) = S ((S (fom_index_pfp_congruent_original_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_congruent_original_rightleft_entry. ab = fom_beta_quotient_pfp_congruent_original_rightleft_entry * S ((S (fom_index_pfp_congruent_original_rightleft)) * ac) + (fom_value_pfp_congruent_original_rightleft))) /\ (exists fom_gap_pfp_congruent_original_rightleft_value_bound. fom_gap_pfp_congruent_original_rightleft_value_bound + S (fom_value_pfp_congruent_original_rightleft) = p))) /\ (((forall fom_index_pfp_congruent_original_rightright. (exists fom_gap_pfp_congruent_original_rightright_index_bound. fom_gap_pfp_congruent_original_rightright_index_bound + S (fom_index_pfp_congruent_original_rightright) = M) -> exists fom_value_pfp_congruent_original_rightright. ((((exists fom_beta_height_pfp_congruent_original_rightright_entry. fom_beta_height_pfp_congruent_original_rightright_entry + S (fom_value_pfp_congruent_original_rightright) = S ((S (fom_index_pfp_congruent_original_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_congruent_original_rightright_entry. bb = fom_beta_quotient_pfp_congruent_original_rightright_entry * S ((S (fom_index_pfp_congruent_original_rightright)) * bc) + (fom_value_pfp_congruent_original_rightright))) /\ (exists fom_gap_pfp_congruent_original_rightright_value_bound. fom_gap_pfp_congruent_original_rightright_value_bound + S (fom_value_pfp_congruent_original_rightright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_congruent_original_rightcoefficients. (exists pfa_gap_congruent_original_rightcoefficientsbound. pfa_gap_congruent_original_rightcoefficientsbound + S (pfc_index_congruent_original_rightcoefficients) = (N)) -> exists pfc_value_congruent_original_rightcoefficients. ((((exists ff_h_pfp_congruent_original_rightcoefficientsentry. ff_h_pfp_congruent_original_rightcoefficientsentry + S (pfc_value_congruent_original_rightcoefficients) = S ((S (pfc_index_congruent_original_rightcoefficients)) * cc)) /\ exists ff_q_pfp_congruent_original_rightcoefficientsentry. cb = ff_q_pfp_congruent_original_rightcoefficientsentry * S ((S (pfc_index_congruent_original_rightcoefficients)) * cc) + (pfc_value_congruent_original_rightcoefficients))) /\ ((exists pfc_terms_code_congruent_original_rightcoefficientscoefficient pfc_terms_scale_congruent_original_rightcoefficientscoefficient pfc_natural_sum_congruent_original_rightcoefficientscoefficient. ((forall pfc_index_congruent_original_rightcoefficientscoefficientdiagonal. (exists pfa_gap_congruent_original_rightcoefficientscoefficientdiagonalbound. pfa_gap_congruent_original_rightcoefficientscoefficientdiagonalbound + S (pfc_index_congruent_original_rightcoefficientscoefficientdiagonal) = (S (pfc_index_congruent_original_rightcoefficients))) -> exists pfc_value_congruent_original_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_original_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_original_rightcoefficientscoefficientdiagonalentry + S (pfc_value_congruent_original_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_original_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_original_rightcoefficientscoefficient)) /\ exists ff_q_pfp_congruent_original_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_original_rightcoefficientscoefficient = ff_q_pfp_congruent_original_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_original_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_original_rightcoefficientscoefficient) + (pfc_value_congruent_original_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_original_rightcoefficientscoefficientdiagonalterm pfc_left_congruent_original_rightcoefficientscoefficientdiagonalterm pfc_right_congruent_original_rightcoefficientscoefficientdiagonalterm. (((pfc_index_congruent_original_rightcoefficientscoefficientdiagonal)+pfc_complement_congruent_original_rightcoefficientscoefficientdiagonalterm=(pfc_index_congruent_original_rightcoefficients)) /\ ((((((exists pfa_gap_congruent_original_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_original_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_original_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_congruent_original_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_original_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_original_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_original_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_congruent_original_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_congruent_original_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_original_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_congruent_original_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_original_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_original_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_congruent_original_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_original_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_original_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_original_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_original_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_congruent_original_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_original_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_original_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_original_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_congruent_original_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_congruent_original_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_original_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_congruent_original_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_original_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_original_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_congruent_original_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_original_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_original_rightcoefficientscoefficientdiagonal)=pfc_left_congruent_original_rightcoefficientscoefficientdiagonalterm*pfc_right_congruent_original_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_original_rightcoefficientscoefficientsum fs_v_pfc_congruent_original_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_start. fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_start. fs_u_pfc_congruent_original_rightcoefficientscoefficientsum = fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_original_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_original_rightcoefficientscoefficient) = S ((S (S (pfc_index_congruent_original_rightcoefficients))) * fs_v_pfc_congruent_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_original_rightcoefficientscoefficientsum = fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_original_rightcoefficients))) * fs_v_pfc_congruent_original_rightcoefficientscoefficientsum) + (pfc_natural_sum_congruent_original_rightcoefficientscoefficient))) /\ forall fs_i_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps = S (pfc_index_congruent_original_rightcoefficients)) -> exists fs_a_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps fs_r_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps fs_s_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_original_rightcoefficientscoefficient)) /\ exists fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_original_rightcoefficientscoefficient = fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_original_rightcoefficientscoefficient) + (fs_a_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_original_rightcoefficientscoefficientsum = fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_original_rightcoefficientscoefficientsum) + (fs_r_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_original_rightcoefficientscoefficientsum = fs_q_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_original_rightcoefficientscoefficientsum) + (fs_s_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_original_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_original_rightcoefficientscoefficientresiduebound. pfa_gap_congruent_original_rightcoefficientscoefficientresiduebound + S (pfc_value_congruent_original_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_original_rightcoefficientscoefficientresiduecongruence pfa_offset_right_congruent_original_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_original_rightcoefficientscoefficient) + (p) * pfa_offset_left_congruent_original_rightcoefficientscoefficientresiduecongruence = (pfc_value_congruent_original_rightcoefficients) + (p) * pfa_offset_right_congruent_original_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_congruent_other_rightleft. (exists fom_gap_pfp_congruent_other_rightleft_index_bound. fom_gap_pfp_congruent_other_rightleft_index_bound + S (fom_index_pfp_congruent_other_rightleft) = L) -> exists fom_value_pfp_congruent_other_rightleft. ((((exists fom_beta_height_pfp_congruent_other_rightleft_entry. fom_beta_height_pfp_congruent_other_rightleft_entry + S (fom_value_pfp_congruent_other_rightleft) = S ((S (fom_index_pfp_congruent_other_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_congruent_other_rightleft_entry. ab = fom_beta_quotient_pfp_congruent_other_rightleft_entry * S ((S (fom_index_pfp_congruent_other_rightleft)) * ac) + (fom_value_pfp_congruent_other_rightleft))) /\ (exists fom_gap_pfp_congruent_other_rightleft_value_bound. fom_gap_pfp_congruent_other_rightleft_value_bound + S (fom_value_pfp_congruent_other_rightleft) = p))) /\ (((forall fom_index_pfp_congruent_other_rightright. (exists fom_gap_pfp_congruent_other_rightright_index_bound. fom_gap_pfp_congruent_other_rightright_index_bound + S (fom_index_pfp_congruent_other_rightright) = H) -> exists fom_value_pfp_congruent_other_rightright. ((((exists fom_beta_height_pfp_congruent_other_rightright_entry. fom_beta_height_pfp_congruent_other_rightright_entry + S (fom_value_pfp_congruent_other_rightright) = S ((S (fom_index_pfp_congruent_other_rightright)) * BC)) /\ exists fom_beta_quotient_pfp_congruent_other_rightright_entry. BB = fom_beta_quotient_pfp_congruent_other_rightright_entry * S ((S (fom_index_pfp_congruent_other_rightright)) * BC) + (fom_value_pfp_congruent_other_rightright))) /\ (exists fom_gap_pfp_congruent_other_rightright_value_bound. fom_gap_pfp_congruent_other_rightright_value_bound + S (fom_value_pfp_congruent_other_rightright) = p))) /\ (((((((L)=0 \/ (H)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((H)=0)) /\ (((L)+(H)=S (K)))))))) /\ ((forall pfc_index_congruent_other_rightcoefficients. (exists pfa_gap_congruent_other_rightcoefficientsbound. pfa_gap_congruent_other_rightcoefficientsbound + S (pfc_index_congruent_other_rightcoefficients) = (K)) -> exists pfc_value_congruent_other_rightcoefficients. ((((exists ff_h_pfp_congruent_other_rightcoefficientsentry. ff_h_pfp_congruent_other_rightcoefficientsentry + S (pfc_value_congruent_other_rightcoefficients) = S ((S (pfc_index_congruent_other_rightcoefficients)) * CC)) /\ exists ff_q_pfp_congruent_other_rightcoefficientsentry. CB = ff_q_pfp_congruent_other_rightcoefficientsentry * S ((S (pfc_index_congruent_other_rightcoefficients)) * CC) + (pfc_value_congruent_other_rightcoefficients))) /\ ((exists pfc_terms_code_congruent_other_rightcoefficientscoefficient pfc_terms_scale_congruent_other_rightcoefficientscoefficient pfc_natural_sum_congruent_other_rightcoefficientscoefficient. ((forall pfc_index_congruent_other_rightcoefficientscoefficientdiagonal. (exists pfa_gap_congruent_other_rightcoefficientscoefficientdiagonalbound. pfa_gap_congruent_other_rightcoefficientscoefficientdiagonalbound + S (pfc_index_congruent_other_rightcoefficientscoefficientdiagonal) = (S (pfc_index_congruent_other_rightcoefficients))) -> exists pfc_value_congruent_other_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_other_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_other_rightcoefficientscoefficientdiagonalentry + S (pfc_value_congruent_other_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_other_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_other_rightcoefficientscoefficient)) /\ exists ff_q_pfp_congruent_other_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_other_rightcoefficientscoefficient = ff_q_pfp_congruent_other_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_other_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_other_rightcoefficientscoefficient) + (pfc_value_congruent_other_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_other_rightcoefficientscoefficientdiagonalterm pfc_left_congruent_other_rightcoefficientscoefficientdiagonalterm pfc_right_congruent_other_rightcoefficientscoefficientdiagonalterm. (((pfc_index_congruent_other_rightcoefficientscoefficientdiagonal)+pfc_complement_congruent_other_rightcoefficientscoefficientdiagonalterm=(pfc_index_congruent_other_rightcoefficients)) /\ ((((((exists pfa_gap_congruent_other_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_other_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_other_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_congruent_other_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_other_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_other_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_other_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_congruent_other_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_congruent_other_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_other_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_congruent_other_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_other_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_other_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_congruent_other_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_other_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_other_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_other_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_other_rightcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_congruent_other_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_other_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_other_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_other_rightcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_congruent_other_rightcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_congruent_other_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_other_rightcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_congruent_other_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_other_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_other_rightcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_congruent_other_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_other_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_other_rightcoefficientscoefficientdiagonal)=pfc_left_congruent_other_rightcoefficientscoefficientdiagonalterm*pfc_right_congruent_other_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_other_rightcoefficientscoefficientsum fs_v_pfc_congruent_other_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_start. fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_other_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_start. fs_u_pfc_congruent_other_rightcoefficientscoefficientsum = fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_other_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_other_rightcoefficientscoefficient) = S ((S (S (pfc_index_congruent_other_rightcoefficients))) * fs_v_pfc_congruent_other_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_other_rightcoefficientscoefficientsum = fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_other_rightcoefficients))) * fs_v_pfc_congruent_other_rightcoefficientscoefficientsum) + (pfc_natural_sum_congruent_other_rightcoefficientscoefficient))) /\ forall fs_i_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps = S (pfc_index_congruent_other_rightcoefficients)) -> exists fs_a_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps fs_r_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps fs_s_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_other_rightcoefficientscoefficient)) /\ exists fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_other_rightcoefficientscoefficient = fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_other_rightcoefficientscoefficient) + (fs_a_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_other_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_other_rightcoefficientscoefficientsum = fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_other_rightcoefficientscoefficientsum) + (fs_r_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_other_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_other_rightcoefficientscoefficientsum = fs_q_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_other_rightcoefficientscoefficientsum) + (fs_s_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_other_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_other_rightcoefficientscoefficientresiduebound. pfa_gap_congruent_other_rightcoefficientscoefficientresiduebound + S (pfc_value_congruent_other_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_other_rightcoefficientscoefficientresiduecongruence pfa_offset_right_congruent_other_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_other_rightcoefficientscoefficient) + (p) * pfa_offset_left_congruent_other_rightcoefficientscoefficientresiduecongruence = (pfc_value_congruent_other_rightcoefficients) + (p) * pfa_offset_right_congruent_other_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_congruent_output_right pfrep_left_congruent_output_right pfrep_right_congruent_output_right. ((exists pfrep_position_congruent_output_rightfirst. ((pfrep_position_congruent_output_rightfirst+S (pfrep_power_congruent_output_right)=(N)) /\ ((((exists ff_h_pfp_congruent_output_rightfirstentry. ff_h_pfp_congruent_output_rightfirstentry + S (pfrep_left_congruent_output_right) = S ((S (pfrep_position_congruent_output_rightfirst)) * cc)) /\ exists ff_q_pfp_congruent_output_rightfirstentry. cb = ff_q_pfp_congruent_output_rightfirstentry * S ((S (pfrep_position_congruent_output_rightfirst)) * cc) + (pfrep_left_congruent_output_right)))))) \/ (((exists pfrep_gap_congruent_output_rightfirstoutside. pfrep_gap_congruent_output_rightfirstoutside+(N)=(pfrep_power_congruent_output_right)) /\ (((pfrep_left_congruent_output_right)=0))))) -> ((exists pfrep_position_congruent_output_rightsecond. ((pfrep_position_congruent_output_rightsecond+S (pfrep_power_congruent_output_right)=(K)) /\ ((((exists ff_h_pfp_congruent_output_rightsecondentry. ff_h_pfp_congruent_output_rightsecondentry + S (pfrep_right_congruent_output_right) = S ((S (pfrep_position_congruent_output_rightsecond)) * CC)) /\ exists ff_q_pfp_congruent_output_rightsecondentry. CB = ff_q_pfp_congruent_output_rightsecondentry * S ((S (pfrep_position_congruent_output_rightsecond)) * CC) + (pfrep_right_congruent_output_right)))))) \/ (((exists pfrep_gap_congruent_output_rightsecondoutside. pfrep_gap_congruent_output_rightsecondoutside+(K)=(pfrep_power_congruent_output_right)) /\ (((pfrep_right_congruent_output_right)=0))))) -> pfrep_left_congruent_output_right=pfrep_right_congruent_output_right)