Nuprl - Pf member rel vars 3 1 1

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

At: member rel vars 3 1 1

1. x: Label
2. name: relname()
3. r1: 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:
8. i < ||v||+1
9. i = 0
10. (x term_vars([u / v][i]))

i:. i < ||v|| & (x term_vars(v[i]))

By: InstConcl [i-1]

Generated subgoal:

1 (x term_vars(v[(i-1)]))

About:

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