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