Nuprl - Some Definitions

NDA_init	`Def I(n) == 1of(2of(n))` `Thm* Alph,States:Type, n:NDA(Alph;States). I(n) States`
length	`Def \|\|as\|\| == Case of as; nil 0 ; a.as' \|\|as'\|\|+1 (recursive) Thm* A:Type, l:A. \|\|l\|\|` `Thm \|\|nil\|\|`
nd_automata	`Def NDA(Alph;States) == (StatesAlphStatesProp)States(States)` `Thm* Alph,States:Type{i}. nd_automata{i}(Alph;States) Type{i'}`
pi2	`Def 2of(t) == t.2` `Thm* A:Type, B:(AType), p:a:AB(a). 2of(p) B(1of(p))`
pi1	`Def 1of(t) == t.1` `Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A`

About: