Nuprl - Some Definitions

auto_oddeven	`Def OddEven#n == < (s:(2n). a:n. (s+(2a)) rem (2n)),0,(s:(2n). s=0 s=(2n)-1) >` `Thm* n:. OddEven#n Automata(n;(2n))`
automata	`Def Automata(Alph;States) == (StatesAlphStates)States(States)` `Thm* Alph,States:Type{i}. Automata(Alph;States) Type{i'}`
exp	`Def (basepower) == if power=0 1 else base(basepower-1) fi (recursive) Thm* n,k:. (nk)` `Thm* n,k:. (nk)`
int_seg	`Def {i..j} == {k:\| i k < j }` `Thm* m,n:. {m..n} Type`
nat_plus	`Def == {i:\| 0 < i }` `Thm* Type`
eq_int	`Def i=j == if i=j true ; false fi` `Thm* i,j:. i=j`
bor	`Def p q == if p true else q fi` `Thm* p,q:. (p q)`
tlambda	`Def (x:T. b(x))(x) == b(x)`
lelt	`Def i j < k == ij & j < k`
le	`Def AB == B < A` `Thm* i,j:. ij Prop`
not	`Def A == A False` `Thm* A:Prop. (A) Prop`

About: