PrintForm Definitions exponent Sections AutomataTheory Doc

At: en inj 1 2 1 2 2
1. n:
2. m:
3. 0 < m
4. l1,l2:n*. ||l1|| = m-1 & ||l2|| = m-1 en(l1) = en(l2) l1 = l2
5. l1: n*
6. l2: n*
7. u: n
8. v: n*
9. u1: n
10. v1: n*

||u.v|| = m & ||u1.v1|| = m en(u.v) = en(u1.v1) u.v = u1.v1
By:
Thin 6
THEN
Thin 5
Generated subgoal:

15. u: n
6. v: n*
7. u1: n
8. v1: n*
||u.v|| = m & ||u1.v1|| = m en(u.v) = en(u1.v1) u.v = u1.v1

About:
impliesandequalintcons
listnatural_numberless_thanallsubtract