PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
inj
1
1
7
1.
q:
2.
l1:
q*
3.
l2:
q*
4.
(q
||l1||
)+en(l1) =
(q
||l2||
)+en(l2)
5.
||l1|| = ||l2||
& en(l1) = en(l2)
l1 = l2
By:
Inst
Thm*
n:
, m:
, l1,l2:
n*. ||l1|| = m & ||l2|| = m
en(l1) = en(l2)
l1 = l2 [q;||l1||;l1;l2]
Generated subgoals:
None
About:
q*q*
(q
||l1||
)+en(l1) = (q||l2||)+en(l2)
& en(l1) = en(l2)
l1 = l2
n:, m:, l1,l2:n*. ||l1|| = m & ||l2|| = m 
en(l1) = en(l2) l1 = l2
[q;||l1||;l1;l2]