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))

Def (basepower) == if power=0 1 else base(basepower-1) fi (recursive)

Thm* n,k:. (nk)

Thm* n,k:. (nk)

Def i=j == if i=j true ; false fi

Thm* i,j:. i=j

Def p q == if p true else q fi

Thm* p,q:. (p q)

Def {i..j} == {k:| i k < j }

Thm* m,n:. {m..n} Type

Def AB == B < A

Thm* i,j:. ij Prop

Def A == A False

Thm* A:Prop. (A) Prop