ND0334 — PolynomialLeftPad(b,c,L,t,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

(∀ x. Lt(x,t) → BetaAt(d,e,x,0)) ∧ (∀ x. ∀ y. Lt(x,L) → BetaAt(b,c,x,y) → BetaAt(d,e,t + x,y))

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

Hygienic expanded first-order definition

((forall pfp_repeat_index_working_euclidean_definitionzeros. (exists pfa_gap_working_euclidean_definitionzerosindex. pfa_gap_working_euclidean_definitionzerosindex + S (pfp_repeat_index_working_euclidean_definitionzeros) = ((t))) -> (((exists ff_h_pfp_working_euclidean_definitionzerosentry. ff_h_pfp_working_euclidean_definitionzerosentry + S (0) = S ((S (pfp_repeat_index_working_euclidean_definitionzeros)) * (e))) /\ exists ff_q_pfp_working_euclidean_definitionzerosentry. (d) = ff_q_pfp_working_euclidean_definitionzerosentry * S ((S (pfp_repeat_index_working_euclidean_definitionzeros)) * (e)) + (0)))) /\ ((forall pfrep_index_working_euclidean_definition pfrep_value_working_euclidean_definition. (exists pfa_gap_working_euclidean_definitionbound. pfa_gap_working_euclidean_definitionbound + S (pfrep_index_working_euclidean_definition) = ((L))) -> (((exists ff_h_pfp_working_euclidean_definitioninput. ff_h_pfp_working_euclidean_definitioninput + S (pfrep_value_working_euclidean_definition) = S ((S (pfrep_index_working_euclidean_definition)) * (c))) /\ exists ff_q_pfp_working_euclidean_definitioninput. (b) = ff_q_pfp_working_euclidean_definitioninput * S ((S (pfrep_index_working_euclidean_definition)) * (c)) + (pfrep_value_working_euclidean_definition))) -> (((exists ff_h_pfp_working_euclidean_definitionoutput. ff_h_pfp_working_euclidean_definitionoutput + S (pfrep_value_working_euclidean_definition) = S ((S (((t))+pfrep_index_working_euclidean_definition)) * (e))) /\ exists ff_q_pfp_working_euclidean_definitionoutput. (d) = ff_q_pfp_working_euclidean_definitionoutput * S ((S (((t))+pfrep_index_working_euclidean_definition)) * (e)) + (pfrep_value_working_euclidean_definition))))))

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

Direct definition dependencies

Lt(a,b)BetaAt(b,c,i,x)

Definitions depending on this notation

none

Checked theorems using this definition