PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
ubound
2
1
2
1
1
1.
n:
2.
l:
n*
3.
u:
n
4.
v:
n*
5.
en(v) < (n
||v||)
6.
||v||+1 = 0
7.
||v||+1-1 = ||v||
u+en(v)
n < n
(n
||v||)
By:
RWH (LemmaC
Thm*
i,j:
. i < j
i+1
j) 5
Generated subgoal:
1
5.
en(v)+1
(n
||v||)
6.
||v||+1 = 0
7.
||v||+1-1 = ||v||
u+en(v)
n < n
(n
||v||)
About:
(n
||v||)
||v||+1 = 0
u+en(v)
n < n(n||v||)
n*nn*||v||)||v||+1 = 0 u+en(v)n < n(n||v||)
i,j:
. i < j 
i+1j)
5(n||v||)||v||+1 = 0 u+en(v)n < n(n||v||)
