Nuprl - Pf rel_mentions_trace_iff 1 2

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

At: rel mentions trace iff 1 2

1. r: rel()
2. L: Term List
3. u: Term
4. v: Term List
5. reduce(x,y. mentions_trace(x) y;false;v) (i:. i < ||v|| & mentions_trace(v[i]))
6. reduce(x,y. mentions_trace(x) y;false;v) (i:. i < ||v|| & mentions_trace(v[i]))
7. i:
8. i < ||v||+1
9. mentions_trace([u / v][i])

mentions_trace(u) reduce(x,y. mentions_trace(x) y;false;v)

By: (CaseNat 0 `i') THENL [Sel 1 (Analyze 0);Sel 2 (Analyze 0)]

Generated subgoals:

1 10. i = 0
mentions_trace(u)

2 10. i = 0
reduce(x,y. mentions_trace(x) y;false;v)

About:

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