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