PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
ubound
2
1
2
1
1
1
1.
n:
2.
l:
n*
3.
u:
n
4.
v:
n*
5.
en(v)+1
(n
||v||)
6.
||v||+1 = 0
7.
||v||+1-1 = ||v||
u+en(v)
n < n
(n
||v||)
By:
Inst
Thm*
a,b:
, n:
. a
b
n
a
n
b [en(v)+1;(n
||v||);n]
Generated subgoal:
1
8.
n
(en(v)+1)
n
(n
||v||)
u+en(v)
n < n
(n
||v||)
About:
(en(v)+1)
n(n
||v||)
u+en(v)n < n(n||v||)
n*nn*(n||v||)
||v||+1 = 0 u+en(v)n < n(n||v||)
a,b:
, n:. ab 
nanb
[en(v)+1;(n||v||);n](en(v)+1)n(n||v||) u+en(v)n < n(n||v||)
