PrintForm Definitions exponent Sections AutomataTheory Doc

At: en ubound 2 1 2 1 1

1. n:
2. l: n*
3. u: n
4. v: n*
5. en(v) < (n||v||)
6. ||v||+1 = 0
7. ||v||+1-1 = ||v||

u+en(v)n < n(n||v||)

By: RWH (LemmaC Thm* i,j:. i < j i+1j) 5

Generated subgoal:

15. en(v)+1(n||v||)
6. ||v||+1 = 0
7. ||v||+1-1 = ||v||
u+en(v)n < n(n||v||)


About:
less_thanaddmultiplylistnatural_numberequalintsubtract