prime_field_polynomial_trim_output_equal

Exact expanded first-order arithmetic statement

forall p b c L t d e M u f g N. ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_unique_firstinput. (exists fom_gap_pfp_unique_firstinput_index_bound. fom_gap_pfp_unique_firstinput_index_bound + S (fom_index_pfp_unique_firstinput) = L) -> exists fom_value_pfp_unique_firstinput. ((((exists fom_beta_height_pfp_unique_firstinput_entry. fom_beta_height_pfp_unique_firstinput_entry + S (fom_value_pfp_unique_firstinput) = S ((S (fom_index_pfp_unique_firstinput)) * c)) /\ exists fom_beta_quotient_pfp_unique_firstinput_entry. b = fom_beta_quotient_pfp_unique_firstinput_entry * S ((S (fom_index_pfp_unique_firstinput)) * c) + (fom_value_pfp_unique_firstinput))) /\ (exists fom_gap_pfp_unique_firstinput_value_bound. fom_gap_pfp_unique_firstinput_value_bound + S (fom_value_pfp_unique_firstinput) = p))) /\ (((forall pfp_repeat_index_unique_firstremoved. (exists pfa_gap_unique_firstremovedindex. pfa_gap_unique_firstremovedindex + S (pfp_repeat_index_unique_firstremoved) = (t)) -> (((exists ff_h_pfp_unique_firstremovedentry. ff_h_pfp_unique_firstremovedentry + S (0) = S ((S (pfp_repeat_index_unique_firstremoved)) * c)) /\ exists ff_q_pfp_unique_firstremovedentry. b = ff_q_pfp_unique_firstremovedentry * S ((S (pfp_repeat_index_unique_firstremoved)) * c) + (0)))) /\ (((forall pftrim_index_unique_firstsuffix pftrim_value_unique_firstsuffix. (exists pfa_gap_unique_firstsuffixbound. pfa_gap_unique_firstsuffixbound + S (pftrim_index_unique_firstsuffix) = (M)) -> (((exists ff_h_pfp_unique_firstsuffixsource. ff_h_pfp_unique_firstsuffixsource + S (pftrim_value_unique_firstsuffix) = S ((S ((t)+pftrim_index_unique_firstsuffix)) * c)) /\ exists ff_q_pfp_unique_firstsuffixsource. b = ff_q_pfp_unique_firstsuffixsource * S ((S ((t)+pftrim_index_unique_firstsuffix)) * c) + (pftrim_value_unique_firstsuffix))) -> (((exists ff_h_pfp_unique_firstsuffixoutput. ff_h_pfp_unique_firstsuffixoutput + S (pftrim_value_unique_firstsuffix) = S ((S (pftrim_index_unique_firstsuffix)) * e)) /\ exists ff_q_pfp_unique_firstsuffixoutput. d = ff_q_pfp_unique_firstsuffixoutput * S ((S (pftrim_index_unique_firstsuffix)) * e) + (pftrim_value_unique_firstsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_unique_firstnormal. ((((exists ff_h_pfp_unique_firstnormalentry. ff_h_pfp_unique_firstnormalentry + S (pftrim_leading_unique_firstnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_unique_firstnormalentry. d = ff_q_pfp_unique_firstnormalentry * S ((S (0)) * e) + (pftrim_leading_unique_firstnormal))) /\ ((~(pftrim_leading_unique_firstnormal=0))))))))))))))) -> ((((L)=(u)+(N)) /\ (((forall fom_index_pfp_unique_secondinput. (exists fom_gap_pfp_unique_secondinput_index_bound. fom_gap_pfp_unique_secondinput_index_bound + S (fom_index_pfp_unique_secondinput) = L) -> exists fom_value_pfp_unique_secondinput. ((((exists fom_beta_height_pfp_unique_secondinput_entry. fom_beta_height_pfp_unique_secondinput_entry + S (fom_value_pfp_unique_secondinput) = S ((S (fom_index_pfp_unique_secondinput)) * c)) /\ exists fom_beta_quotient_pfp_unique_secondinput_entry. b = fom_beta_quotient_pfp_unique_secondinput_entry * S ((S (fom_index_pfp_unique_secondinput)) * c) + (fom_value_pfp_unique_secondinput))) /\ (exists fom_gap_pfp_unique_secondinput_value_bound. fom_gap_pfp_unique_secondinput_value_bound + S (fom_value_pfp_unique_secondinput) = p))) /\ (((forall pfp_repeat_index_unique_secondremoved. (exists pfa_gap_unique_secondremovedindex. pfa_gap_unique_secondremovedindex + S (pfp_repeat_index_unique_secondremoved) = (u)) -> (((exists ff_h_pfp_unique_secondremovedentry. ff_h_pfp_unique_secondremovedentry + S (0) = S ((S (pfp_repeat_index_unique_secondremoved)) * c)) /\ exists ff_q_pfp_unique_secondremovedentry. b = ff_q_pfp_unique_secondremovedentry * S ((S (pfp_repeat_index_unique_secondremoved)) * c) + (0)))) /\ (((forall pftrim_index_unique_secondsuffix pftrim_value_unique_secondsuffix. (exists pfa_gap_unique_secondsuffixbound. pfa_gap_unique_secondsuffixbound + S (pftrim_index_unique_secondsuffix) = (N)) -> (((exists ff_h_pfp_unique_secondsuffixsource. ff_h_pfp_unique_secondsuffixsource + S (pftrim_value_unique_secondsuffix) = S ((S ((u)+pftrim_index_unique_secondsuffix)) * c)) /\ exists ff_q_pfp_unique_secondsuffixsource. b = ff_q_pfp_unique_secondsuffixsource * S ((S ((u)+pftrim_index_unique_secondsuffix)) * c) + (pftrim_value_unique_secondsuffix))) -> (((exists ff_h_pfp_unique_secondsuffixoutput. ff_h_pfp_unique_secondsuffixoutput + S (pftrim_value_unique_secondsuffix) = S ((S (pftrim_index_unique_secondsuffix)) * g)) /\ exists ff_q_pfp_unique_secondsuffixoutput. f = ff_q_pfp_unique_secondsuffixoutput * S ((S (pftrim_index_unique_secondsuffix)) * g) + (pftrim_value_unique_secondsuffix)))) /\ (((N)=0 \/ (exists pftrim_leading_unique_secondnormal. ((((exists ff_h_pfp_unique_secondnormalentry. ff_h_pfp_unique_secondnormalentry + S (pftrim_leading_unique_secondnormal) = S ((S (0)) * g)) /\ exists ff_q_pfp_unique_secondnormalentry. f = ff_q_pfp_unique_secondnormalentry * S ((S (0)) * g) + (pftrim_leading_unique_secondnormal))) /\ ((~(pftrim_leading_unique_secondnormal=0))))))))))))))) -> (forall mdr_i_pfp_unique_coefficients mdr_a_pfp_unique_coefficients. (exists mdr_gap_pfp_unique_coefficientsb. mdr_gap_pfp_unique_coefficientsb + S (mdr_i_pfp_unique_coefficients) = (M)) -> (((exists ff_h_mdr_pfp_unique_coefficientso. ff_h_mdr_pfp_unique_coefficientso + S (mdr_a_pfp_unique_coefficients) = S ((S (mdr_i_pfp_unique_coefficients)) * e)) /\ exists ff_q_mdr_pfp_unique_coefficientso. d = ff_q_mdr_pfp_unique_coefficientso * S ((S (mdr_i_pfp_unique_coefficients)) * e) + (mdr_a_pfp_unique_coefficients))) -> (((exists ff_h_mdr_pfp_unique_coefficientsn. ff_h_mdr_pfp_unique_coefficientsn + S (mdr_a_pfp_unique_coefficients) = S ((S (mdr_i_pfp_unique_coefficients)) * g)) /\ exists ff_q_mdr_pfp_unique_coefficientsn. f = ff_q_mdr_pfp_unique_coefficientsn * S ((S (mdr_i_pfp_unique_coefficients)) * g) + (mdr_a_pfp_unique_coefficients))))