mb
automata
2
Sections
GenAutomata
Doc
Def
c1
c2 ==
x:T. x
c1
x
c2
is mentioned by
Thm*
a1,a2,b1,b2:Collection(SimpleType). a1
a2
b1
b2
st_app(a1;b1)
st_app(a2;b2)
[st_app_monotone]
Thm*
x:Label, a1,a2:Collection(dec()). a1
a2
dec_lookup(a1;x)
dec_lookup(a2;x)
[dec_lookup_monotone]
In prior sections:
mb
collection
Try larger context:
GenAutomata
mb
automata
2
Sections
GenAutomata
Doc