prime_field_polynomial_convolution_shift_right_equivalent

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M cb cc N BB BC db dc K eb ec. (~(p=0)) -> (((forall mdr_i_pfp_shift_equivalent_factorprefix mdr_a_pfp_shift_equivalent_factorprefix. (exists mdr_gap_pfp_shift_equivalent_factorprefixb. mdr_gap_pfp_shift_equivalent_factorprefixb + S (mdr_i_pfp_shift_equivalent_factorprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_equivalent_factorprefixo. ff_h_mdr_pfp_shift_equivalent_factorprefixo + S (mdr_a_pfp_shift_equivalent_factorprefix) = S ((S (mdr_i_pfp_shift_equivalent_factorprefix)) * bc)) /\ exists ff_q_mdr_pfp_shift_equivalent_factorprefixo. bb = ff_q_mdr_pfp_shift_equivalent_factorprefixo * S ((S (mdr_i_pfp_shift_equivalent_factorprefix)) * bc) + (mdr_a_pfp_shift_equivalent_factorprefix))) -> (((exists ff_h_mdr_pfp_shift_equivalent_factorprefixn. ff_h_mdr_pfp_shift_equivalent_factorprefixn + S (mdr_a_pfp_shift_equivalent_factorprefix) = S ((S (mdr_i_pfp_shift_equivalent_factorprefix)) * BC)) /\ exists ff_q_mdr_pfp_shift_equivalent_factorprefixn. BB = ff_q_mdr_pfp_shift_equivalent_factorprefixn * S ((S (mdr_i_pfp_shift_equivalent_factorprefix)) * BC) + (mdr_a_pfp_shift_equivalent_factorprefix)))) /\ ((((exists ff_h_pfp_shift_equivalent_factorlast. ff_h_pfp_shift_equivalent_factorlast + S (0) = S ((S (M)) * BC)) /\ exists ff_q_pfp_shift_equivalent_factorlast. BB = ff_q_pfp_shift_equivalent_factorlast * S ((S (M)) * BC) + (0)))))) -> (((forall fom_index_pfp_shift_equivalent_oldleft. (exists fom_gap_pfp_shift_equivalent_oldleft_index_bound. fom_gap_pfp_shift_equivalent_oldleft_index_bound + S (fom_index_pfp_shift_equivalent_oldleft) = L) -> exists fom_value_pfp_shift_equivalent_oldleft. ((((exists fom_beta_height_pfp_shift_equivalent_oldleft_entry. fom_beta_height_pfp_shift_equivalent_oldleft_entry + S (fom_value_pfp_shift_equivalent_oldleft) = S ((S (fom_index_pfp_shift_equivalent_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_equivalent_oldleft_entry. ab = fom_beta_quotient_pfp_shift_equivalent_oldleft_entry * S ((S (fom_index_pfp_shift_equivalent_oldleft)) * ac) + (fom_value_pfp_shift_equivalent_oldleft))) /\ (exists fom_gap_pfp_shift_equivalent_oldleft_value_bound. fom_gap_pfp_shift_equivalent_oldleft_value_bound + S (fom_value_pfp_shift_equivalent_oldleft) = p))) /\ (((forall fom_index_pfp_shift_equivalent_oldright. (exists fom_gap_pfp_shift_equivalent_oldright_index_bound. fom_gap_pfp_shift_equivalent_oldright_index_bound + S (fom_index_pfp_shift_equivalent_oldright) = M) -> exists fom_value_pfp_shift_equivalent_oldright. ((((exists fom_beta_height_pfp_shift_equivalent_oldright_entry. fom_beta_height_pfp_shift_equivalent_oldright_entry + S (fom_value_pfp_shift_equivalent_oldright) = S ((S (fom_index_pfp_shift_equivalent_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_shift_equivalent_oldright_entry. bb = fom_beta_quotient_pfp_shift_equivalent_oldright_entry * S ((S (fom_index_pfp_shift_equivalent_oldright)) * bc) + (fom_value_pfp_shift_equivalent_oldright))) /\ (exists fom_gap_pfp_shift_equivalent_oldright_value_bound. fom_gap_pfp_shift_equivalent_oldright_value_bound + S (fom_value_pfp_shift_equivalent_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_shift_equivalent_oldcoefficients. (exists pfa_gap_shift_equivalent_oldcoefficientsbound. pfa_gap_shift_equivalent_oldcoefficientsbound + S (pfc_index_shift_equivalent_oldcoefficients) = (N)) -> exists pfc_value_shift_equivalent_oldcoefficients. ((((exists ff_h_pfp_shift_equivalent_oldcoefficientsentry. ff_h_pfp_shift_equivalent_oldcoefficientsentry + S (pfc_value_shift_equivalent_oldcoefficients) = S ((S (pfc_index_shift_equivalent_oldcoefficients)) * cc)) /\ exists ff_q_pfp_shift_equivalent_oldcoefficientsentry. cb = ff_q_pfp_shift_equivalent_oldcoefficientsentry * S ((S (pfc_index_shift_equivalent_oldcoefficients)) * cc) + (pfc_value_shift_equivalent_oldcoefficients))) /\ ((exists pfc_terms_code_shift_equivalent_oldcoefficientscoefficient pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient pfc_natural_sum_shift_equivalent_oldcoefficientscoefficient. ((forall pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal. (exists pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonalbound. pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonalbound + S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal) = (S (pfc_index_shift_equivalent_oldcoefficients))) -> exists pfc_value_shift_equivalent_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonalentry + S (pfc_value_shift_equivalent_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient)) /\ exists ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_equivalent_oldcoefficientscoefficient = ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient) + (pfc_value_shift_equivalent_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm. (((pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)+pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm=(pfc_index_shift_equivalent_oldcoefficients)) /\ ((((((exists pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_equivalent_oldcoefficientscoefficientdiagonal)=pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm*pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_start. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_start. fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_equivalent_oldcoefficientscoefficient) = S ((S (S (pfc_index_shift_equivalent_oldcoefficients))) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_equivalent_oldcoefficients))) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum) + (pfc_natural_sum_shift_equivalent_oldcoefficientscoefficient))) /\ forall fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps = S (pfc_index_shift_equivalent_oldcoefficients)) -> exists fs_a_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps fs_r_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps fs_s_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_equivalent_oldcoefficientscoefficient = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient) + (fs_a_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum) + (fs_r_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum) + (fs_s_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_equivalent_oldcoefficientscoefficientresiduebound. pfa_gap_shift_equivalent_oldcoefficientscoefficientresiduebound + S (pfc_value_shift_equivalent_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_equivalent_oldcoefficientscoefficientresiduecongruence pfa_offset_right_shift_equivalent_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_equivalent_oldcoefficientscoefficient) + (p) * pfa_offset_left_shift_equivalent_oldcoefficientscoefficientresiduecongruence = (pfc_value_shift_equivalent_oldcoefficients) + (p) * pfa_offset_right_shift_equivalent_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_shift_equivalent_newleft. (exists fom_gap_pfp_shift_equivalent_newleft_index_bound. fom_gap_pfp_shift_equivalent_newleft_index_bound + S (fom_index_pfp_shift_equivalent_newleft) = L) -> exists fom_value_pfp_shift_equivalent_newleft. ((((exists fom_beta_height_pfp_shift_equivalent_newleft_entry. fom_beta_height_pfp_shift_equivalent_newleft_entry + S (fom_value_pfp_shift_equivalent_newleft) = S ((S (fom_index_pfp_shift_equivalent_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_equivalent_newleft_entry. ab = fom_beta_quotient_pfp_shift_equivalent_newleft_entry * S ((S (fom_index_pfp_shift_equivalent_newleft)) * ac) + (fom_value_pfp_shift_equivalent_newleft))) /\ (exists fom_gap_pfp_shift_equivalent_newleft_value_bound. fom_gap_pfp_shift_equivalent_newleft_value_bound + S (fom_value_pfp_shift_equivalent_newleft) = p))) /\ (((forall fom_index_pfp_shift_equivalent_newright. (exists fom_gap_pfp_shift_equivalent_newright_index_bound. fom_gap_pfp_shift_equivalent_newright_index_bound + S (fom_index_pfp_shift_equivalent_newright) = S M) -> exists fom_value_pfp_shift_equivalent_newright. ((((exists fom_beta_height_pfp_shift_equivalent_newright_entry. fom_beta_height_pfp_shift_equivalent_newright_entry + S (fom_value_pfp_shift_equivalent_newright) = S ((S (fom_index_pfp_shift_equivalent_newright)) * BC)) /\ exists fom_beta_quotient_pfp_shift_equivalent_newright_entry. BB = fom_beta_quotient_pfp_shift_equivalent_newright_entry * S ((S (fom_index_pfp_shift_equivalent_newright)) * BC) + (fom_value_pfp_shift_equivalent_newright))) /\ (exists fom_gap_pfp_shift_equivalent_newright_value_bound. fom_gap_pfp_shift_equivalent_newright_value_bound + S (fom_value_pfp_shift_equivalent_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_shift_equivalent_newcoefficients. (exists pfa_gap_shift_equivalent_newcoefficientsbound. pfa_gap_shift_equivalent_newcoefficientsbound + S (pfc_index_shift_equivalent_newcoefficients) = (K)) -> exists pfc_value_shift_equivalent_newcoefficients. ((((exists ff_h_pfp_shift_equivalent_newcoefficientsentry. ff_h_pfp_shift_equivalent_newcoefficientsentry + S (pfc_value_shift_equivalent_newcoefficients) = S ((S (pfc_index_shift_equivalent_newcoefficients)) * dc)) /\ exists ff_q_pfp_shift_equivalent_newcoefficientsentry. db = ff_q_pfp_shift_equivalent_newcoefficientsentry * S ((S (pfc_index_shift_equivalent_newcoefficients)) * dc) + (pfc_value_shift_equivalent_newcoefficients))) /\ ((exists pfc_terms_code_shift_equivalent_newcoefficientscoefficient pfc_terms_scale_shift_equivalent_newcoefficientscoefficient pfc_natural_sum_shift_equivalent_newcoefficientscoefficient. ((forall pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal. (exists pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonalbound. pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonalbound + S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal) = (S (pfc_index_shift_equivalent_newcoefficients))) -> exists pfc_value_shift_equivalent_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonalentry + S (pfc_value_shift_equivalent_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_equivalent_newcoefficientscoefficient)) /\ exists ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_equivalent_newcoefficientscoefficient = ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_equivalent_newcoefficientscoefficient) + (pfc_value_shift_equivalent_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm. (((pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)+pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm=(pfc_index_shift_equivalent_newcoefficients)) /\ ((((((exists pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_equivalent_newcoefficientscoefficientdiagonal)=pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm*pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_start. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_start. fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_equivalent_newcoefficientscoefficient) = S ((S (S (pfc_index_shift_equivalent_newcoefficients))) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_equivalent_newcoefficients))) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum) + (pfc_natural_sum_shift_equivalent_newcoefficientscoefficient))) /\ forall fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps = S (pfc_index_shift_equivalent_newcoefficients)) -> exists fs_a_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps fs_r_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps fs_s_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_equivalent_newcoefficientscoefficient)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_equivalent_newcoefficientscoefficient = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_equivalent_newcoefficientscoefficient) + (fs_a_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum) + (fs_r_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum) + (fs_s_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_equivalent_newcoefficientscoefficientresiduebound. pfa_gap_shift_equivalent_newcoefficientscoefficientresiduebound + S (pfc_value_shift_equivalent_newcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_equivalent_newcoefficientscoefficientresiduecongruence pfa_offset_right_shift_equivalent_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_equivalent_newcoefficientscoefficient) + (p) * pfa_offset_left_shift_equivalent_newcoefficientscoefficientresiduecongruence = (pfc_value_shift_equivalent_newcoefficients) + (p) * pfa_offset_right_shift_equivalent_newcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall mdr_i_pfp_shift_equivalent_comparisonprefix mdr_a_pfp_shift_equivalent_comparisonprefix. (exists mdr_gap_pfp_shift_equivalent_comparisonprefixb. mdr_gap_pfp_shift_equivalent_comparisonprefixb + S (mdr_i_pfp_shift_equivalent_comparisonprefix) = (N)) -> (((exists ff_h_mdr_pfp_shift_equivalent_comparisonprefixo. ff_h_mdr_pfp_shift_equivalent_comparisonprefixo + S (mdr_a_pfp_shift_equivalent_comparisonprefix) = S ((S (mdr_i_pfp_shift_equivalent_comparisonprefix)) * cc)) /\ exists ff_q_mdr_pfp_shift_equivalent_comparisonprefixo. cb = ff_q_mdr_pfp_shift_equivalent_comparisonprefixo * S ((S (mdr_i_pfp_shift_equivalent_comparisonprefix)) * cc) + (mdr_a_pfp_shift_equivalent_comparisonprefix))) -> (((exists ff_h_mdr_pfp_shift_equivalent_comparisonprefixn. ff_h_mdr_pfp_shift_equivalent_comparisonprefixn + S (mdr_a_pfp_shift_equivalent_comparisonprefix) = S ((S (mdr_i_pfp_shift_equivalent_comparisonprefix)) * ec)) /\ exists ff_q_mdr_pfp_shift_equivalent_comparisonprefixn. eb = ff_q_mdr_pfp_shift_equivalent_comparisonprefixn * S ((S (mdr_i_pfp_shift_equivalent_comparisonprefix)) * ec) + (mdr_a_pfp_shift_equivalent_comparisonprefix)))) /\ ((((exists ff_h_pfp_shift_equivalent_comparisonlast. ff_h_pfp_shift_equivalent_comparisonlast + S (0) = S ((S (N)) * ec)) /\ exists ff_q_pfp_shift_equivalent_comparisonlast. eb = ff_q_pfp_shift_equivalent_comparisonlast * S ((S (N)) * ec) + (0)))))) -> (forall pfrep_power_shift_equivalent_result pfrep_left_shift_equivalent_result pfrep_right_shift_equivalent_result. ((exists pfrep_position_shift_equivalent_resultfirst. ((pfrep_position_shift_equivalent_resultfirst+S (pfrep_power_shift_equivalent_result)=(K)) /\ ((((exists ff_h_pfp_shift_equivalent_resultfirstentry. ff_h_pfp_shift_equivalent_resultfirstentry + S (pfrep_left_shift_equivalent_result) = S ((S (pfrep_position_shift_equivalent_resultfirst)) * dc)) /\ exists ff_q_pfp_shift_equivalent_resultfirstentry. db = ff_q_pfp_shift_equivalent_resultfirstentry * S ((S (pfrep_position_shift_equivalent_resultfirst)) * dc) + (pfrep_left_shift_equivalent_result)))))) \/ (((exists pfrep_gap_shift_equivalent_resultfirstoutside. pfrep_gap_shift_equivalent_resultfirstoutside+(K)=(pfrep_power_shift_equivalent_result)) /\ (((pfrep_left_shift_equivalent_result)=0))))) -> ((exists pfrep_position_shift_equivalent_resultsecond. ((pfrep_position_shift_equivalent_resultsecond+S (pfrep_power_shift_equivalent_result)=(S N)) /\ ((((exists ff_h_pfp_shift_equivalent_resultsecondentry. ff_h_pfp_shift_equivalent_resultsecondentry + S (pfrep_right_shift_equivalent_result) = S ((S (pfrep_position_shift_equivalent_resultsecond)) * ec)) /\ exists ff_q_pfp_shift_equivalent_resultsecondentry. eb = ff_q_pfp_shift_equivalent_resultsecondentry * S ((S (pfrep_position_shift_equivalent_resultsecond)) * ec) + (pfrep_right_shift_equivalent_result)))))) \/ (((exists pfrep_gap_shift_equivalent_resultsecondoutside. pfrep_gap_shift_equivalent_resultsecondoutside+(S N)=(pfrep_power_shift_equivalent_result)) /\ (((pfrep_right_shift_equivalent_result)=0))))) -> pfrep_left_shift_equivalent_result=pfrep_right_shift_equivalent_result)