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