automata
6
Sections
AutomataTheory
Doc
Def
(base
power) == if power=
0
1 else base
(base
power-1) fi (recursive)
Thm*
n:
. OddEven#n
Automata(
n;
(2
n)) auto_oddeven_wf
In prior sections:
exponent
n:
. OddEven#n 
Automata(n;(2
n)) auto_oddeven_wf
power) == if power=
0
1 else base
(basepower-1) fi (recursive)
n:. OddEven#n Automata(n;(2n)) auto_oddeven_wf