PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
inj
1
2
1
2
1
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*
||u.v|| = m & ||nil|| = m
en(u.v) = en(nil)
u.v = nil
By:
Reduce 0
Generated subgoals:
None
About:
l1,l2:n*. ||l1|| = m-1 & ||l2|| = m-1 
en(l1) = en(l2) l1 = l2n*n*nn*
||u.v|| = m & ||nil|| = m en(u.v) = en(nil) u.v = nil
