mb automata 2 Sections GenAutomata Doc

Def st_app(c1;c2) == (s2c2.(s1c1.st_app1(s1;s2)))

is mentioned by

Thm* a1,a2,b1,b2:Collection(SimpleType). a1 = a2 b1 = b2 st_app(a1;b1) = st_app(a2;b2)[st_app_functionality]
Thm* a1,a2,b1,b2:Collection(SimpleType). a1 a2 b1 b2 st_app(a1;b1) st_app(a2;b2)[st_app_monotone]
Thm* c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1)[member_st_app]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc