mb
automata
2
Sections
GenAutomata
Doc
Def
(
x
c.f(x))(y) ==
x:T. x
c & y
f(x)
is mentioned by
Def
st_app(c1;c2) == (
s2
c2.(
s1
c1.st_app1(s1;s2)))
[st_app]
In prior sections:
mb
collection
Try larger context:
GenAutomata
mb
automata
2
Sections
GenAutomata
Doc
s2
c2.(s1c1.st_app1(s1;s2)))xc.f(x))(y) == 
x:T. x c & y f(x)
s2c2.(s1c1.st_app1(s1;s2)))