PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
inj
1
1
5
1.
q:
2.
l1:
q*
3.
l2:
q*
4.
(q
||l1||
)+en(l1) =
(q
||l2||
)+en(l2)
en(l2)
(q
||l2||)
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(l2) 
(q||l2||)
n:, l:n*. en(l) (n||l||)