(2steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: mentions guard mentions trace

g:Label, t:Term. term_mentions_guard(g;t) mentions_trace(t)
By:
RepeatFor 2 (Analyze 0)
THEN
TermInd -1
THEN
Reduce 0
Generated subgoal:

11. g: Label
2. t: Term
3. u: TermType{i'}
4. w: t:{v:Term| u(v) }term_mentions_guard(g;t) mentions_trace(t)
5. y1: {v:Term| u(v) }
6. y2: {v:Term| u(v) }
7. term_mentions_guard(g;y1) term_mentions_guard(g;y2)
mentions_trace(y1) mentions_trace(y2)

About:
assertimpliesall

(2steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc