GenAutomata
Sections
NuprlLIB
Doc
Def
ioa_mentions_trace(A) == (
e:eff(). e
A.eff &
mentions_trace(e.smt.term))
(
p:pre(). p
A.pre &
rel_mentions_trace(p.rel))
(
r:rel(). r
A.init &
rel_mentions_trace(r))
is mentioned
In prior sections:
mb
automata
3
mb
automata
4
GenAutomata
Sections
NuprlLIB
Doc
e:eff(). e 
A.eff & 
mentions_trace(e.smt.term)) 
(p:pre(). p A.pre & rel_mentions_trace(p.rel)) (r:rel(). r A.init & rel_mentions_trace(r))