Nuprl - Pf rel mentions iff 1 2 1

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

At: rel mentions iff 1 2 1

1. r: rel()
2. x: Label
3. l: Term List
4. u: Term
5. v: Term List
6. (i:. i < ||v|| & (x term_vars(v[i]))) (x reduce(t,vs. term_vars(t) @ vs;nil;v))
7. (i:. i < ||v|| & (x term_vars(v[i]))) (x reduce(t,vs. term_vars(t) @ vs;nil;v))
8. i:
9. i < ||v||+1
10. (x term_vars([u / v][i]))

(x term_vars(u)) (x reduce(t,vs. term_vars(t) @ vs;nil;v))

By: MoveToConcl -1 THEN CaseNat 0 `i' THEN Reduce 0

Generated subgoals:

1 10. i = 0
11. (x term_vars(u))
(x term_vars(u)) (x reduce(t,vs. term_vars(t) @ vs;nil;v))

2 10. i = 0
11. (x term_vars([u / v][i]))
(x term_vars(u)) (x reduce(t,vs. term_vars(t) @ vs;nil;v))

3 10. i = 0
i < ||[u / v]||

About:

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