PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
surj
1
1
1.
n:
2.
k:
(n
0)
l:
n*. ||l|| = 0 & en(l) = k
By:
RecUnfold `exp` 2
THEN
Reduce 2
Generated subgoal:
1
2.
k:
1
l:
n*. ||l|| = 0 & en(l) = k
About:
1
l:n*. ||l|| = 0 & en(l) = k
(n
0) l:n*. ||l|| = 0 & en(l) = k1 l:n*. ||l|| = 0 & en(l) = k
