(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: assert subst mentions trace 2 1 1 1
1. True
2. u: LabelTerm
3. v: (LabelTerm) List
4. subst_mentions_trace(v) (i:||v||. mentions_trace(2of(v[i])))
5. subst_mentions_trace(v) (i:||v||. mentions_trace(2of(v[i])))
6. i: (||v||+1)
7. mentions_trace(2of(v[(i-1)]))
8. i = 0

subst_mentions_trace(v)
By:
BackThruSomeHyp
THEN
AutoInstConcl []
Generated subgoals:

None

About:
productlistassertintnatural_numberaddsubtractequalimpliestrueexists

(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc