PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
inj
1
1
1
1.
n:
2.
l1:
n*
3.
l2:
n*
4.
||l1|| = 0 & ||l2|| = 0
5.
en(l1) = en(l2)
l1 = l2
By:
RWH (LemmaC
Thm*
l:T*. ||l|| = 0
l = nil) 0
Generated subgoals:
None
About:
n*n*
l1 = l2
l:T*. ||l|| = 0 
l = nil)
0
