prime_field_polynomial_trim_from_cut

Exact expanded first-order arithmetic statement

forall p b c L t d e M. (forall fom_index_pfp_cut_to_trim_coefficients. (exists fom_gap_pfp_cut_to_trim_coefficients_index_bound. fom_gap_pfp_cut_to_trim_coefficients_index_bound + S (fom_index_pfp_cut_to_trim_coefficients) = L) -> exists fom_value_pfp_cut_to_trim_coefficients. ((((exists fom_beta_height_pfp_cut_to_trim_coefficients_entry. fom_beta_height_pfp_cut_to_trim_coefficients_entry + S (fom_value_pfp_cut_to_trim_coefficients) = S ((S (fom_index_pfp_cut_to_trim_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_cut_to_trim_coefficients_entry. b = fom_beta_quotient_pfp_cut_to_trim_coefficients_entry * S ((S (fom_index_pfp_cut_to_trim_coefficients)) * c) + (fom_value_pfp_cut_to_trim_coefficients))) /\ (exists fom_gap_pfp_cut_to_trim_coefficients_value_bound. fom_gap_pfp_cut_to_trim_coefficients_value_bound + S (fom_value_pfp_cut_to_trim_coefficients) = p))) -> ((((L)=(t)+(M)) /\ (((forall pfp_repeat_index_cut_to_trim_sourcezero. (exists pfa_gap_cut_to_trim_sourcezeroindex. pfa_gap_cut_to_trim_sourcezeroindex + S (pfp_repeat_index_cut_to_trim_sourcezero) = (t)) -> (((exists ff_h_pfp_cut_to_trim_sourcezeroentry. ff_h_pfp_cut_to_trim_sourcezeroentry + S (0) = S ((S (pfp_repeat_index_cut_to_trim_sourcezero)) * c)) /\ exists ff_q_pfp_cut_to_trim_sourcezeroentry. b = ff_q_pfp_cut_to_trim_sourcezeroentry * S ((S (pfp_repeat_index_cut_to_trim_sourcezero)) * c) + (0)))) /\ (((M)=0 \/ (((~((M)=0)) /\ ((exists pftrim_leading_cut_to_trim_sourcehead. ((((exists ff_h_pfp_cut_to_trim_sourceheadentry. ff_h_pfp_cut_to_trim_sourceheadentry + S (pftrim_leading_cut_to_trim_sourcehead) = S ((S (t)) * c)) /\ exists ff_q_pfp_cut_to_trim_sourceheadentry. b = ff_q_pfp_cut_to_trim_sourceheadentry * S ((S (t)) * c) + (pftrim_leading_cut_to_trim_sourcehead))) /\ ((~(pftrim_leading_cut_to_trim_sourcehead=0)))))))))))))) -> (forall pftrim_index_cut_to_trim_suffix pftrim_value_cut_to_trim_suffix. (exists pfa_gap_cut_to_trim_suffixbound. pfa_gap_cut_to_trim_suffixbound + S (pftrim_index_cut_to_trim_suffix) = (M)) -> (((exists ff_h_pfp_cut_to_trim_suffixsource. ff_h_pfp_cut_to_trim_suffixsource + S (pftrim_value_cut_to_trim_suffix) = S ((S ((t)+pftrim_index_cut_to_trim_suffix)) * c)) /\ exists ff_q_pfp_cut_to_trim_suffixsource. b = ff_q_pfp_cut_to_trim_suffixsource * S ((S ((t)+pftrim_index_cut_to_trim_suffix)) * c) + (pftrim_value_cut_to_trim_suffix))) -> (((exists ff_h_pfp_cut_to_trim_suffixoutput. ff_h_pfp_cut_to_trim_suffixoutput + S (pftrim_value_cut_to_trim_suffix) = S ((S (pftrim_index_cut_to_trim_suffix)) * e)) /\ exists ff_q_pfp_cut_to_trim_suffixoutput. d = ff_q_pfp_cut_to_trim_suffixoutput * S ((S (pftrim_index_cut_to_trim_suffix)) * e) + (pftrim_value_cut_to_trim_suffix)))) -> ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_cut_to_trim_resultinput. (exists fom_gap_pfp_cut_to_trim_resultinput_index_bound. fom_gap_pfp_cut_to_trim_resultinput_index_bound + S (fom_index_pfp_cut_to_trim_resultinput) = L) -> exists fom_value_pfp_cut_to_trim_resultinput. ((((exists fom_beta_height_pfp_cut_to_trim_resultinput_entry. fom_beta_height_pfp_cut_to_trim_resultinput_entry + S (fom_value_pfp_cut_to_trim_resultinput) = S ((S (fom_index_pfp_cut_to_trim_resultinput)) * c)) /\ exists fom_beta_quotient_pfp_cut_to_trim_resultinput_entry. b = fom_beta_quotient_pfp_cut_to_trim_resultinput_entry * S ((S (fom_index_pfp_cut_to_trim_resultinput)) * c) + (fom_value_pfp_cut_to_trim_resultinput))) /\ (exists fom_gap_pfp_cut_to_trim_resultinput_value_bound. fom_gap_pfp_cut_to_trim_resultinput_value_bound + S (fom_value_pfp_cut_to_trim_resultinput) = p))) /\ (((forall pfp_repeat_index_cut_to_trim_resultremoved. (exists pfa_gap_cut_to_trim_resultremovedindex. pfa_gap_cut_to_trim_resultremovedindex + S (pfp_repeat_index_cut_to_trim_resultremoved) = (t)) -> (((exists ff_h_pfp_cut_to_trim_resultremovedentry. ff_h_pfp_cut_to_trim_resultremovedentry + S (0) = S ((S (pfp_repeat_index_cut_to_trim_resultremoved)) * c)) /\ exists ff_q_pfp_cut_to_trim_resultremovedentry. b = ff_q_pfp_cut_to_trim_resultremovedentry * S ((S (pfp_repeat_index_cut_to_trim_resultremoved)) * c) + (0)))) /\ (((forall pftrim_index_cut_to_trim_resultsuffix pftrim_value_cut_to_trim_resultsuffix. (exists pfa_gap_cut_to_trim_resultsuffixbound. pfa_gap_cut_to_trim_resultsuffixbound + S (pftrim_index_cut_to_trim_resultsuffix) = (M)) -> (((exists ff_h_pfp_cut_to_trim_resultsuffixsource. ff_h_pfp_cut_to_trim_resultsuffixsource + S (pftrim_value_cut_to_trim_resultsuffix) = S ((S ((t)+pftrim_index_cut_to_trim_resultsuffix)) * c)) /\ exists ff_q_pfp_cut_to_trim_resultsuffixsource. b = ff_q_pfp_cut_to_trim_resultsuffixsource * S ((S ((t)+pftrim_index_cut_to_trim_resultsuffix)) * c) + (pftrim_value_cut_to_trim_resultsuffix))) -> (((exists ff_h_pfp_cut_to_trim_resultsuffixoutput. ff_h_pfp_cut_to_trim_resultsuffixoutput + S (pftrim_value_cut_to_trim_resultsuffix) = S ((S (pftrim_index_cut_to_trim_resultsuffix)) * e)) /\ exists ff_q_pfp_cut_to_trim_resultsuffixoutput. d = ff_q_pfp_cut_to_trim_resultsuffixoutput * S ((S (pftrim_index_cut_to_trim_resultsuffix)) * e) + (pftrim_value_cut_to_trim_resultsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_cut_to_trim_resultnormal. ((((exists ff_h_pfp_cut_to_trim_resultnormalentry. ff_h_pfp_cut_to_trim_resultnormalentry + S (pftrim_leading_cut_to_trim_resultnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_cut_to_trim_resultnormalentry. d = ff_q_pfp_cut_to_trim_resultnormalentry * S ((S (0)) * e) + (pftrim_leading_cut_to_trim_resultnormal))) /\ ((~(pftrim_leading_cut_to_trim_resultnormal=0)))))))))))))))