PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
inj
1
2
1
2
2
1
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.
u:
n
6.
v:
n*
7.
u1:
n
8.
v1:
n*
9.
||u.v|| = m & ||u1.v1|| = m
10.
en(u.v) = en(u1.v1)
u.v = u1.v1
By:
RecUnfold `en` 10
THEN
Reduce 10
Generated subgoal:
1
10.
u+en(v)
n = u1+en(v1)
n
u.v = u1.v1
About:
n = u1+en(v1)n
u.v = u1.v1
l1,l2:n*. ||l1|| = m-1 & ||l2|| = m-1 
en(l1) = en(l2) l1 = l2nn*nn* u.v = u1.v1n = u1+en(v1)n u.v = u1.v1
