Nuprl - GenAutomata Citations of trace consistent

Def trace_consistent(rho;da;R;t) ==

g:Label.

term_mentions_guard(g;t)

subtype_rel(({a:(

[[da]] rho)|

(R(g,kind(a))) } List); (rho(lbl_pr( < Trace, g > ))))

is mentioned

In prior sections: mb automata 3