PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
inj
1
1
1.
n:
l1,l2:
n*. ||l1|| = 0 & ||l2|| = 0
en(l1) = en(l2)
l1 = l2
By:
UnivCD
Generated subgoal:
1
2.
l1:
n*
3.
l2:
n*
4.
||l1|| = 0 & ||l2|| = 0
5.
en(l1) = en(l2)
l1 = l2
About:
n*n*
l1 = l2
l1,l2:n*. ||l1|| = 0 & ||l2|| = 0 
en(l1) = en(l2) l1 = l2n*n* l1 = l2
