(7steps)
PrintForm
Definitions
Lemmas
mb
label
Sections
GenAutomata
Doc
At:
lbl
pair
wf2
1
2
1.
x:
Label
2.
y:
Label
ground_ptn(lbl_pr( < x, y > ))
By:
RecUnfold `ground_ptn` 0
THEN
Reduce 0
Generated subgoal:
1
ground_ptn(x)
ground_ptn(y)
About:
(7steps)
PrintForm
Definitions
Lemmas
mb
label
Sections
GenAutomata
Doc