prime_field_polynomial_convolution_equivalent_congruent_left

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M cb cc N AB AC H CB CC K. (~(p=0)) -> (forall pfrep_power_congruent_factor_left pfrep_left_congruent_factor_left pfrep_right_congruent_factor_left. ((exists pfrep_position_congruent_factor_leftfirst. ((pfrep_position_congruent_factor_leftfirst+S (pfrep_power_congruent_factor_left)=(L)) /\ ((((exists ff_h_pfp_congruent_factor_leftfirstentry. ff_h_pfp_congruent_factor_leftfirstentry + S (pfrep_left_congruent_factor_left) = S ((S (pfrep_position_congruent_factor_leftfirst)) * ac)) /\ exists ff_q_pfp_congruent_factor_leftfirstentry. ab = ff_q_pfp_congruent_factor_leftfirstentry * S ((S (pfrep_position_congruent_factor_leftfirst)) * ac) + (pfrep_left_congruent_factor_left)))))) \/ (((exists pfrep_gap_congruent_factor_leftfirstoutside. pfrep_gap_congruent_factor_leftfirstoutside+(L)=(pfrep_power_congruent_factor_left)) /\ (((pfrep_left_congruent_factor_left)=0))))) -> ((exists pfrep_position_congruent_factor_leftsecond. ((pfrep_position_congruent_factor_leftsecond+S (pfrep_power_congruent_factor_left)=(H)) /\ ((((exists ff_h_pfp_congruent_factor_leftsecondentry. ff_h_pfp_congruent_factor_leftsecondentry + S (pfrep_right_congruent_factor_left) = S ((S (pfrep_position_congruent_factor_leftsecond)) * AC)) /\ exists ff_q_pfp_congruent_factor_leftsecondentry. AB = ff_q_pfp_congruent_factor_leftsecondentry * S ((S (pfrep_position_congruent_factor_leftsecond)) * AC) + (pfrep_right_congruent_factor_left)))))) \/ (((exists pfrep_gap_congruent_factor_leftsecondoutside. pfrep_gap_congruent_factor_leftsecondoutside+(H)=(pfrep_power_congruent_factor_left)) /\ (((pfrep_right_congruent_factor_left)=0))))) -> pfrep_left_congruent_factor_left=pfrep_right_congruent_factor_left) -> (((forall fom_index_pfp_congruent_original_leftleft. (exists fom_gap_pfp_congruent_original_leftleft_index_bound. fom_gap_pfp_congruent_original_leftleft_index_bound + S (fom_index_pfp_congruent_original_leftleft) = L) -> exists fom_value_pfp_congruent_original_leftleft. ((((exists fom_beta_height_pfp_congruent_original_leftleft_entry. fom_beta_height_pfp_congruent_original_leftleft_entry + S (fom_value_pfp_congruent_original_leftleft) = S ((S (fom_index_pfp_congruent_original_leftleft)) * ac)) /\ exists fom_beta_quotient_pfp_congruent_original_leftleft_entry. ab = fom_beta_quotient_pfp_congruent_original_leftleft_entry * S ((S (fom_index_pfp_congruent_original_leftleft)) * ac) + (fom_value_pfp_congruent_original_leftleft))) /\ (exists fom_gap_pfp_congruent_original_leftleft_value_bound. fom_gap_pfp_congruent_original_leftleft_value_bound + S (fom_value_pfp_congruent_original_leftleft) = p))) /\ (((forall fom_index_pfp_congruent_original_leftright. (exists fom_gap_pfp_congruent_original_leftright_index_bound. fom_gap_pfp_congruent_original_leftright_index_bound + S (fom_index_pfp_congruent_original_leftright) = M) -> exists fom_value_pfp_congruent_original_leftright. ((((exists fom_beta_height_pfp_congruent_original_leftright_entry. fom_beta_height_pfp_congruent_original_leftright_entry + S (fom_value_pfp_congruent_original_leftright) = S ((S (fom_index_pfp_congruent_original_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_congruent_original_leftright_entry. bb = fom_beta_quotient_pfp_congruent_original_leftright_entry * S ((S (fom_index_pfp_congruent_original_leftright)) * bc) + (fom_value_pfp_congruent_original_leftright))) /\ (exists fom_gap_pfp_congruent_original_leftright_value_bound. fom_gap_pfp_congruent_original_leftright_value_bound + S (fom_value_pfp_congruent_original_leftright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_congruent_original_leftcoefficients. (exists pfa_gap_congruent_original_leftcoefficientsbound. pfa_gap_congruent_original_leftcoefficientsbound + S (pfc_index_congruent_original_leftcoefficients) = (N)) -> exists pfc_value_congruent_original_leftcoefficients. ((((exists ff_h_pfp_congruent_original_leftcoefficientsentry. ff_h_pfp_congruent_original_leftcoefficientsentry + S (pfc_value_congruent_original_leftcoefficients) = S ((S (pfc_index_congruent_original_leftcoefficients)) * cc)) /\ exists ff_q_pfp_congruent_original_leftcoefficientsentry. cb = ff_q_pfp_congruent_original_leftcoefficientsentry * S ((S (pfc_index_congruent_original_leftcoefficients)) * cc) + (pfc_value_congruent_original_leftcoefficients))) /\ ((exists pfc_terms_code_congruent_original_leftcoefficientscoefficient pfc_terms_scale_congruent_original_leftcoefficientscoefficient pfc_natural_sum_congruent_original_leftcoefficientscoefficient. ((forall pfc_index_congruent_original_leftcoefficientscoefficientdiagonal. (exists pfa_gap_congruent_original_leftcoefficientscoefficientdiagonalbound. pfa_gap_congruent_original_leftcoefficientscoefficientdiagonalbound + S (pfc_index_congruent_original_leftcoefficientscoefficientdiagonal) = (S (pfc_index_congruent_original_leftcoefficients))) -> exists pfc_value_congruent_original_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_original_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_original_leftcoefficientscoefficientdiagonalentry + S (pfc_value_congruent_original_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_original_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_original_leftcoefficientscoefficient)) /\ exists ff_q_pfp_congruent_original_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_original_leftcoefficientscoefficient = ff_q_pfp_congruent_original_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_original_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_original_leftcoefficientscoefficient) + (pfc_value_congruent_original_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_original_leftcoefficientscoefficientdiagonalterm pfc_left_congruent_original_leftcoefficientscoefficientdiagonalterm pfc_right_congruent_original_leftcoefficientscoefficientdiagonalterm. (((pfc_index_congruent_original_leftcoefficientscoefficientdiagonal)+pfc_complement_congruent_original_leftcoefficientscoefficientdiagonalterm=(pfc_index_congruent_original_leftcoefficients)) /\ ((((((exists pfa_gap_congruent_original_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_original_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_original_leftcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_congruent_original_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_original_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_original_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_original_leftcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_congruent_original_leftcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_congruent_original_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_original_leftcoefficientscoefficientdiagonal)) * ac) + (pfc_left_congruent_original_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_original_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_original_leftcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_congruent_original_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_original_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_original_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_original_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_original_leftcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_congruent_original_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_original_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_original_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_original_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_congruent_original_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_congruent_original_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_original_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_congruent_original_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_original_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_original_leftcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_congruent_original_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_original_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_original_leftcoefficientscoefficientdiagonal)=pfc_left_congruent_original_leftcoefficientscoefficientdiagonalterm*pfc_right_congruent_original_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_original_leftcoefficientscoefficientsum fs_v_pfc_congruent_original_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_start. fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_original_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_start. fs_u_pfc_congruent_original_leftcoefficientscoefficientsum = fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_original_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_original_leftcoefficientscoefficient) = S ((S (S (pfc_index_congruent_original_leftcoefficients))) * fs_v_pfc_congruent_original_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_original_leftcoefficientscoefficientsum = fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_original_leftcoefficients))) * fs_v_pfc_congruent_original_leftcoefficientscoefficientsum) + (pfc_natural_sum_congruent_original_leftcoefficientscoefficient))) /\ forall fs_i_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps = S (pfc_index_congruent_original_leftcoefficients)) -> exists fs_a_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps fs_r_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps fs_s_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_original_leftcoefficientscoefficient)) /\ exists fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_original_leftcoefficientscoefficient = fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_original_leftcoefficientscoefficient) + (fs_a_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_original_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_original_leftcoefficientscoefficientsum = fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_original_leftcoefficientscoefficientsum) + (fs_r_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_original_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_original_leftcoefficientscoefficientsum = fs_q_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_original_leftcoefficientscoefficientsum) + (fs_s_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_original_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_original_leftcoefficientscoefficientresiduebound. pfa_gap_congruent_original_leftcoefficientscoefficientresiduebound + S (pfc_value_congruent_original_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_original_leftcoefficientscoefficientresiduecongruence pfa_offset_right_congruent_original_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_original_leftcoefficientscoefficient) + (p) * pfa_offset_left_congruent_original_leftcoefficientscoefficientresiduecongruence = (pfc_value_congruent_original_leftcoefficients) + (p) * pfa_offset_right_congruent_original_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_congruent_other_leftleft. (exists fom_gap_pfp_congruent_other_leftleft_index_bound. fom_gap_pfp_congruent_other_leftleft_index_bound + S (fom_index_pfp_congruent_other_leftleft) = H) -> exists fom_value_pfp_congruent_other_leftleft. ((((exists fom_beta_height_pfp_congruent_other_leftleft_entry. fom_beta_height_pfp_congruent_other_leftleft_entry + S (fom_value_pfp_congruent_other_leftleft) = S ((S (fom_index_pfp_congruent_other_leftleft)) * AC)) /\ exists fom_beta_quotient_pfp_congruent_other_leftleft_entry. AB = fom_beta_quotient_pfp_congruent_other_leftleft_entry * S ((S (fom_index_pfp_congruent_other_leftleft)) * AC) + (fom_value_pfp_congruent_other_leftleft))) /\ (exists fom_gap_pfp_congruent_other_leftleft_value_bound. fom_gap_pfp_congruent_other_leftleft_value_bound + S (fom_value_pfp_congruent_other_leftleft) = p))) /\ (((forall fom_index_pfp_congruent_other_leftright. (exists fom_gap_pfp_congruent_other_leftright_index_bound. fom_gap_pfp_congruent_other_leftright_index_bound + S (fom_index_pfp_congruent_other_leftright) = M) -> exists fom_value_pfp_congruent_other_leftright. ((((exists fom_beta_height_pfp_congruent_other_leftright_entry. fom_beta_height_pfp_congruent_other_leftright_entry + S (fom_value_pfp_congruent_other_leftright) = S ((S (fom_index_pfp_congruent_other_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_congruent_other_leftright_entry. bb = fom_beta_quotient_pfp_congruent_other_leftright_entry * S ((S (fom_index_pfp_congruent_other_leftright)) * bc) + (fom_value_pfp_congruent_other_leftright))) /\ (exists fom_gap_pfp_congruent_other_leftright_value_bound. fom_gap_pfp_congruent_other_leftright_value_bound + S (fom_value_pfp_congruent_other_leftright) = p))) /\ (((((((H)=0 \/ (M)=0) /\ (((K)=0)))) \/ (((~((H)=0)) /\ (((~((M)=0)) /\ (((H)+(M)=S (K)))))))) /\ ((forall pfc_index_congruent_other_leftcoefficients. (exists pfa_gap_congruent_other_leftcoefficientsbound. pfa_gap_congruent_other_leftcoefficientsbound + S (pfc_index_congruent_other_leftcoefficients) = (K)) -> exists pfc_value_congruent_other_leftcoefficients. ((((exists ff_h_pfp_congruent_other_leftcoefficientsentry. ff_h_pfp_congruent_other_leftcoefficientsentry + S (pfc_value_congruent_other_leftcoefficients) = S ((S (pfc_index_congruent_other_leftcoefficients)) * CC)) /\ exists ff_q_pfp_congruent_other_leftcoefficientsentry. CB = ff_q_pfp_congruent_other_leftcoefficientsentry * S ((S (pfc_index_congruent_other_leftcoefficients)) * CC) + (pfc_value_congruent_other_leftcoefficients))) /\ ((exists pfc_terms_code_congruent_other_leftcoefficientscoefficient pfc_terms_scale_congruent_other_leftcoefficientscoefficient pfc_natural_sum_congruent_other_leftcoefficientscoefficient. ((forall pfc_index_congruent_other_leftcoefficientscoefficientdiagonal. (exists pfa_gap_congruent_other_leftcoefficientscoefficientdiagonalbound. pfa_gap_congruent_other_leftcoefficientscoefficientdiagonalbound + S (pfc_index_congruent_other_leftcoefficientscoefficientdiagonal) = (S (pfc_index_congruent_other_leftcoefficients))) -> exists pfc_value_congruent_other_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_other_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_other_leftcoefficientscoefficientdiagonalentry + S (pfc_value_congruent_other_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_other_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_other_leftcoefficientscoefficient)) /\ exists ff_q_pfp_congruent_other_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_other_leftcoefficientscoefficient = ff_q_pfp_congruent_other_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_other_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_other_leftcoefficientscoefficient) + (pfc_value_congruent_other_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_other_leftcoefficientscoefficientdiagonalterm pfc_left_congruent_other_leftcoefficientscoefficientdiagonalterm pfc_right_congruent_other_leftcoefficientscoefficientdiagonalterm. (((pfc_index_congruent_other_leftcoefficientscoefficientdiagonal)+pfc_complement_congruent_other_leftcoefficientscoefficientdiagonalterm=(pfc_index_congruent_other_leftcoefficients)) /\ ((((((exists pfa_gap_congruent_other_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_other_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_other_leftcoefficientscoefficientdiagonal) = (H)) /\ ((((exists ff_h_pfp_congruent_other_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_other_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_other_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_other_leftcoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_congruent_other_leftcoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_congruent_other_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_other_leftcoefficientscoefficientdiagonal)) * AC) + (pfc_left_congruent_other_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_other_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_other_leftcoefficientscoefficientdiagonaltermleftoutside+(H)=(pfc_index_congruent_other_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_other_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_other_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_other_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_other_leftcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_congruent_other_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_other_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_other_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_other_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_congruent_other_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_congruent_other_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_other_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_congruent_other_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_other_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_other_leftcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_congruent_other_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_other_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_other_leftcoefficientscoefficientdiagonal)=pfc_left_congruent_other_leftcoefficientscoefficientdiagonalterm*pfc_right_congruent_other_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_other_leftcoefficientscoefficientsum fs_v_pfc_congruent_other_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_start. fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_other_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_start. fs_u_pfc_congruent_other_leftcoefficientscoefficientsum = fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_other_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_other_leftcoefficientscoefficient) = S ((S (S (pfc_index_congruent_other_leftcoefficients))) * fs_v_pfc_congruent_other_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_other_leftcoefficientscoefficientsum = fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_other_leftcoefficients))) * fs_v_pfc_congruent_other_leftcoefficientscoefficientsum) + (pfc_natural_sum_congruent_other_leftcoefficientscoefficient))) /\ forall fs_i_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps = S (pfc_index_congruent_other_leftcoefficients)) -> exists fs_a_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps fs_r_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps fs_s_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_other_leftcoefficientscoefficient)) /\ exists fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_other_leftcoefficientscoefficient = fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_other_leftcoefficientscoefficient) + (fs_a_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_other_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_other_leftcoefficientscoefficientsum = fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_other_leftcoefficientscoefficientsum) + (fs_r_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_other_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_other_leftcoefficientscoefficientsum = fs_q_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_other_leftcoefficientscoefficientsum) + (fs_s_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_other_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_other_leftcoefficientscoefficientresiduebound. pfa_gap_congruent_other_leftcoefficientscoefficientresiduebound + S (pfc_value_congruent_other_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_other_leftcoefficientscoefficientresiduecongruence pfa_offset_right_congruent_other_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_other_leftcoefficientscoefficient) + (p) * pfa_offset_left_congruent_other_leftcoefficientscoefficientresiduecongruence = (pfc_value_congruent_other_leftcoefficients) + (p) * pfa_offset_right_congruent_other_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_congruent_output_left pfrep_left_congruent_output_left pfrep_right_congruent_output_left. ((exists pfrep_position_congruent_output_leftfirst. ((pfrep_position_congruent_output_leftfirst+S (pfrep_power_congruent_output_left)=(N)) /\ ((((exists ff_h_pfp_congruent_output_leftfirstentry. ff_h_pfp_congruent_output_leftfirstentry + S (pfrep_left_congruent_output_left) = S ((S (pfrep_position_congruent_output_leftfirst)) * cc)) /\ exists ff_q_pfp_congruent_output_leftfirstentry. cb = ff_q_pfp_congruent_output_leftfirstentry * S ((S (pfrep_position_congruent_output_leftfirst)) * cc) + (pfrep_left_congruent_output_left)))))) \/ (((exists pfrep_gap_congruent_output_leftfirstoutside. pfrep_gap_congruent_output_leftfirstoutside+(N)=(pfrep_power_congruent_output_left)) /\ (((pfrep_left_congruent_output_left)=0))))) -> ((exists pfrep_position_congruent_output_leftsecond. ((pfrep_position_congruent_output_leftsecond+S (pfrep_power_congruent_output_left)=(K)) /\ ((((exists ff_h_pfp_congruent_output_leftsecondentry. ff_h_pfp_congruent_output_leftsecondentry + S (pfrep_right_congruent_output_left) = S ((S (pfrep_position_congruent_output_leftsecond)) * CC)) /\ exists ff_q_pfp_congruent_output_leftsecondentry. CB = ff_q_pfp_congruent_output_leftsecondentry * S ((S (pfrep_position_congruent_output_leftsecond)) * CC) + (pfrep_right_congruent_output_left)))))) \/ (((exists pfrep_gap_congruent_output_leftsecondoutside. pfrep_gap_congruent_output_leftsecondoutside+(K)=(pfrep_power_congruent_output_left)) /\ (((pfrep_right_congruent_output_left)=0))))) -> pfrep_left_congruent_output_left=pfrep_right_congruent_output_left)