mb
events
Sections
GenAutomata
Doc
Def
tr | P == filter(
x.P(kind(x));tr)
is mentioned by
Thm*
a,tr,P:Top. [a / tr] | P ~ if P(kind(a))
[a / tr | P] else tr | P fi
[trace_projection_cons]
Thm*
P:Top. nil | P ~ nil
[trace_projection_nil]
Thm*
d:Decl, t1,t2:(
d) List, P:(Label
). t1 @ t2 | P ~ (t1 | P @ t2 | P)
[trace_projection_append]
Try larger context:
GenAutomata
mb
events
Sections
GenAutomata
Doc