mb
label
Sections
GenAutomata
Doc
Def
Label == {p:Pattern|
ground_ptn(p) }
is mentioned by
Thm*
x,y:Label. Dec(x = y)
[decidable__equal_lbl]
Thm*
x:Label, ls:Label List. x
ls
(x
ls)
[assert_lbls_member]
Thm*
l1,l2:Label. l1 =
l2
l1 = l2
[eq_lbl_iff]
Thm*
SQType(Label)
[lbl_sq]
Thm*
x,y:Label. lbl_pr( < x, y > )
Label
[lbl_pair_wf2]
Thm*
l1,l2:Label. l1 =
l2
l1 = l2
[assert_eq_label]
Thm*
x:Atom. ptn_atom(x)
Label
[ptn_atom_wf3]
Try larger context:
GenAutomata
mb
label
Sections
GenAutomata
Doc