PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
ubound
n:
, l:
n*. en(l) < (n
||l||)
By:
UnivCD
THEN
ListInd 2
THEN
Reduce 0
Generated subgoals:
1
1.
n:
2.
l:
n*
en(nil) < (n
0)
2
1.
n:
2.
l:
n*
3.
u:
n
4.
v:
n*
5.
en(v) < (n
||v||)
en(u.v) < (n
||v||+1)
About:
n*
en(nil) < (n
0)n*nn*||v||) en(u.v) < (n||v||+1) 
n:, l:n*. en(l) < (n||l||)n* en(nil) < (n0)n*nn*||v||) en(u.v) < (n||v||+1)
