mb
automata
3
Sections
GenAutomata
Doc
Rank
Theorem
Name
3
Thm*
r:rel(), de:sig(), ds1,ds2:Collection(dec()) , da1,da2:Collection(SimpleType). ds1
ds2
da1
da2
tc(r;ds1;da1;de)
tc(r;ds2;da2;de)
[tc_monotone]
cites
2
Thm*
ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType) , de:sig(), t:Term. ds1
ds2
da1
da2
(
a:SimpleType. a
term_types(ds1;da1;de;t)
a
term_types(ds2;da2;de;t))
[term_types_monotone_member]
mb
automata
3
Sections
GenAutomata
Doc