PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
beq
sym
p,q:
. p =
q = q =
p
By:
Unfold `beq` 0
THEN
RepD
THEN
BoolCases 1
THEN
BoolCases 1
THEN
Reduce 0
Generated subgoals:
None
About:
p,q:
. p =
q = q = p
