u:Term, e,s,a,tr,tr':Top. 
mentions_trace(u) 
([[u]] e s a tr' ~ [[u]] e s a tr)g:Label, t:Term. term_mentions_guard(g;t) mentions_trace(t)
statevar x'- > false
funsymbol x- > false
freevar x- > false
trace(P)- > true
x(y)- > x 
y
over t)
is mentioned by
| Thm* u:Term, e,s,a,tr,tr':Top. mentions_trace(u) ([[u]] e s a tr' ~ [[u]] e s a tr) | [term_mng_static] |
| Thm* g:Label, t:Term. term_mentions_guard(g;t) mentions_trace(t) | [mentions_guard_mentions_trace] |
Try larger context:
GenAutomata