mb
automata
3
Sections
GenAutomata
Doc
Def
t.pre == 1of(2of(2of(2of(t))))
is mentioned by
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))
[ioa_mentions_trace]
In prior sections:
mb
automata
1
Try larger context:
GenAutomata
mb
automata
3
Sections
GenAutomata
Doc