PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
inj
1
1
4
1.
q:
2.
l1:
q*
3.
l2:
q*
4.
(q
||l1||
)+en(l1) =
(q
||l2||
)+en(l2)
en(l1)
(q
||l1||)
By:
BackThru
Thm*
n:
, l:
n*. en(l)
(n
||l||)
Generated subgoals:
None
About:
q*q*
(q
||l1||
)+en(l1) = (q||l2||)+en(l2)
en(l1) 
(q||l1||)
n:, l:n*. en(l) (n||l||)