ND0341 — PolynomialShift(b,c,L,d,e)

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Definition in prerequisite notation

BetaPrefixEqual(b,c,d,e,L) ∧ BetaAt(d,e,L,0)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition

((forall mdr_i_pfp_working_shift_definitionprefix mdr_a_pfp_working_shift_definitionprefix. (exists mdr_gap_pfp_working_shift_definitionprefixb. mdr_gap_pfp_working_shift_definitionprefixb + S (mdr_i_pfp_working_shift_definitionprefix) = ((L))) -> (((exists ff_h_mdr_pfp_working_shift_definitionprefixo. ff_h_mdr_pfp_working_shift_definitionprefixo + S (mdr_a_pfp_working_shift_definitionprefix) = S ((S (mdr_i_pfp_working_shift_definitionprefix)) * (c))) /\ exists ff_q_mdr_pfp_working_shift_definitionprefixo. (b) = ff_q_mdr_pfp_working_shift_definitionprefixo * S ((S (mdr_i_pfp_working_shift_definitionprefix)) * (c)) + (mdr_a_pfp_working_shift_definitionprefix))) -> (((exists ff_h_mdr_pfp_working_shift_definitionprefixn. ff_h_mdr_pfp_working_shift_definitionprefixn + S (mdr_a_pfp_working_shift_definitionprefix) = S ((S (mdr_i_pfp_working_shift_definitionprefix)) * (e))) /\ exists ff_q_mdr_pfp_working_shift_definitionprefixn. (d) = ff_q_mdr_pfp_working_shift_definitionprefixn * S ((S (mdr_i_pfp_working_shift_definitionprefix)) * (e)) + (mdr_a_pfp_working_shift_definitionprefix)))) /\ ((((exists ff_h_pfp_working_shift_definitionlast. ff_h_pfp_working_shift_definitionlast + S (0) = S ((S ((L))) * (e))) /\ exists ff_q_pfp_working_shift_definitionlast. (d) = ff_q_pfp_working_shift_definitionlast * S ((S ((L))) * (e)) + (0)))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

BetaPrefixEqual(b,c,d,e,l)BetaAt(b,c,i,x)

Definitions depending on this notation

none

Checked theorems using this definition