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