mb
automata
2
Sections
GenAutomata
Doc
Def
a
b == tree_node( < a, b > )
is mentioned by
Thm*
c1,c2:Collection(SimpleType), s:SimpleType. s
st_app(c1;c2)
(
a:SimpleType. a
c2 & a
s
c1)
[member_st_app]
Thm*
s1,s2,s:SimpleType. s
st_app1(s1;s2)
st_eq(s1;s2
s)
[member_st_app1]
Try larger context:
GenAutomata
mb
automata
2
Sections
GenAutomata
Doc