PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
beq
wf
p,q:
. p =
q
By:
Unfold `beq` 0
THEN
RepD
Generated subgoal:
1
1.
p:
2.
q:
if p
q else
q fi
About:
if p
q else 
q fi 
p,q:. p =
q if p q else q fi 
