PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
exp
wf2
1
2
1
1.
n:
2.
k:
3.
0 < k
4.
(n
k-1)
5.
k = 0
0
n
(n
k-1)
By:
Inst
Thm*
a,b:
, n:
. a
b
n
a
n
b [0;(n
k-1);n]
Generated subgoals:
1
0
(n
k-1)
2
6.
n
0
n
(n
k-1)
0
n
(n
k-1)
About:
0
(n
k-1)
0n(nk-1) 0n(nk-1)
k-1) 
k = 0 0n(nk-1)
a,b:, n:. ab 
nanb
[0;(nk-1);n] 0(nk-1)0n(nk-1) 0n(nk-1)
