PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
ubound
2
1.
n:
2.
l:
n*
3.
u:
n
4.
v:
n*
5.
en(v) < (n
||v||)
en(u.v) < (n
||v||+1)
By:
RecUnfold `en` 0
THEN
Reduce 0
Generated subgoal:
1
u+en(v)
n < (n
||v||+1)
About:
u+en(v)
n < (n
||v||+1)
n*nn*||v||) en(u.v) < (n||v||+1) u+en(v)n < (n||v||+1)
