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