Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
BetaAt(sb,sc,0,0) ∧ (BetaAt(sb,sc,l,n) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ m. BetaAt(b,c,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (BetaAt(sb,sc,S x,m) ∧ m = z + y))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((((exists fs_h_secondwave_start. fs_h_secondwave_start + S (0) = S ((S (0)) * sc)) /\ exists fs_q_secondwave_start. sb = fs_q_secondwave_start * S ((S (0)) * sc) + (0))) /\ ((((exists fs_h_secondwave_terminal. fs_h_secondwave_terminal + S (n) = S ((S (l)) * sc)) /\ exists fs_q_secondwave_terminal. sb = fs_q_secondwave_terminal * S ((S (l)) * sc) + (n))) /\ forall fs_i_secondwave_steps. (exists fs_lt_secondwave_steps_bound. fs_lt_secondwave_steps_bound + S fs_i_secondwave_steps = l) -> exists fs_a_secondwave_steps fs_r_secondwave_steps fs_s_secondwave_steps. ((((exists fs_h_secondwave_steps_summand. fs_h_secondwave_steps_summand + S (fs_a_secondwave_steps) = S ((S (fs_i_secondwave_steps)) * c)) /\ exists fs_q_secondwave_steps_summand. b = fs_q_secondwave_steps_summand * S ((S (fs_i_secondwave_steps)) * c) + (fs_a_secondwave_steps))) /\ ((((exists fs_h_secondwave_steps_partial. fs_h_secondwave_steps_partial + S (fs_r_secondwave_steps) = S ((S (fs_i_secondwave_steps)) * sc)) /\ exists fs_q_secondwave_steps_partial. sb = fs_q_secondwave_steps_partial * S ((S (fs_i_secondwave_steps)) * sc) + (fs_r_secondwave_steps))) /\ ((((exists fs_h_secondwave_steps_successor. fs_h_secondwave_steps_successor + S (fs_s_secondwave_steps) = S ((S (S fs_i_secondwave_steps)) * sc)) /\ exists fs_q_secondwave_steps_successor. sb = fs_q_secondwave_steps_successor * S ((S (S fs_i_secondwave_steps)) * sc) + (fs_s_secondwave_steps))) /\ fs_s_secondwave_steps = fs_r_secondwave_steps + fs_a_secondwave_steps)))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
none directly; see definition consumers