mb automata 3 Sections GenAutomata Doc

Def mentions_trace(t) == iterate(statevar x- > false statevar x'- > false funsymbol x- > false freevar x- > false trace(P)- > true x(y)- > x y over t)

is mentioned by

Thm* rho:Decl, t:Term, da:Collection(dec()) , R:(LabelLabel). mentions_trace(t) trace_consistent(rho;da;R;t)[no_mention_implies_consistent_term]
Thm* r:rel(). rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i]))[rel_mentions_trace_iff]
Thm* as:(LabelTerm) List. subst_mentions_trace(as) (i:||as||. mentions_trace(2of(as[i])))[assert_subst_mentions_trace]
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]
Def rel_mentions_trace(r) == reduce(x,y. mentions_trace(x) y;false;r.args)[rel_mentions_trace]
Def subst_mentions_trace(as) == reduce(a,b. mentions_trace(2of(a)) b;false;as)[subst_mentions_trace]

In prior sections: mb automata 2

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc