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