Nuprl - Pf closed_rel

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

1. r: rel()
2. l: Term List
3. u: Term
4. v: Term List
5. i:. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil i < ||v|| term_free_vars(v[i]) = nil

i:. term_free_vars(u) = nil & reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil i < ||v||+1 term_free_vars([u / v][i]) = nil

By: Auto THEN CaseNat 0 `i'

Generated subgoals:

1 6. i:
7. term_free_vars(u) = nil
8. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil
9. i < ||v||+1
10. i = 0
term_free_vars([u / v][0]) = nil

2 6. i:
7. term_free_vars(u) = nil
8. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil
9. i < ||v||+1
10. i = 0
term_free_vars([u / v][i]) = nil

About:

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

1	6. `i:` 7. `term_free_vars(u) = nil` 8. `reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil` 9. `i < \|\|v\|\|+1` 10. `i = 0` `term_free_vars([u / v][0]) = nil`
2	6. `i:` 7. `term_free_vars(u) = nil` 8. `reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil` 9. `i < \|\|v\|\|+1` 10. `i = 0` `term_free_vars([u / v][i]) = nil`