Nuprl - Some Definitions

NDA_act	`Def n == 1of(n)` `Thm* Alph,States:Type, n:NDA(Alph;States). n StatesAlphStatesProp`
NDA_fin	`Def F(n) == 2of(2of(n))` `Thm* Alph,States:Type, n:NDA(Alph;States). F(n) States`
NDA_init	`Def I(n) == 1of(2of(n))` `Thm* Alph,States:Type, n:NDA(Alph;States). I(n) States`
nd_automata	`Def NDA(Alph;States) == (StatesAlphStatesProp)States(States)` `Thm* Alph,States:Type{i}. nd_automata{i}(Alph;States) Type{i'}`
pi1	`Def 1of(t) == t.1` `Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A`
pi2	`Def 2of(t) == t.2` `Thm* A:Type, B:(AType), p:a:AB(a). 2of(p) B(1of(p))`

About: