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
¬V = 0 ∧ (∀ x. ∀ y. ∀ z. Lt(x,L) → Lt(z,V) → x = V · y + z → BetaAt(r,s,x,y · z))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((~(((V))=0)) /\ (forall dpi_index_g009_definition dpi_row_g009_definition dpi_column_g009_definition. (exists pvs_gap_g009_definitionwindow. pvs_gap_g009_definitionwindow + S (dpi_index_g009_definition) = ((L))) -> (exists pvs_gap_g009_definitionremainder. pvs_gap_g009_definitionremainder + S (dpi_column_g009_definition) = ((V))) -> (dpi_index_g009_definition)=((V))*(dpi_row_g009_definition)+(dpi_column_g009_definition) -> (((exists ff_h_pvs_g009_definitionvalue. ff_h_pvs_g009_definitionvalue + S ((dpi_row_g009_definition)*(dpi_column_g009_definition)) = S ((S (dpi_index_g009_definition)) * (s))) /\ exists ff_q_pvs_g009_definitionvalue. (r) = ff_q_pvs_g009_definitionvalue * S ((S (dpi_index_g009_definition)) * (s)) + ((dpi_row_g009_definition)*(dpi_column_g009_definition))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.