Nuprl - Pf rel mentions iff 1

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

1. r: rel()
2. x: Label

(i:. i < ||r.args|| & (x term_vars(r.args[i]))) (x reduce(t,vs. term_vars(t) @ vs;nil;r.args))

By: GenConcl (r.args = l) THEN Thin -1 THEN ListInd -1 THEN Reduce 0

Generated subgoals:

1 3. l: Term List
(i:. i < 0 & (x term_vars(nil[i]))) (x nil)

2 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))
(i:. i < ||v||+1 & (x term_vars([u / v][i]))) (x term_vars(u) @ reduce(t,vs. term_vars(t) @ vs;nil;v))

About:

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

1	3. `l:` `Term List` `(i:. i < 0 & (x term_vars(nil[i]))) (x nil)`
2	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))` `(i:. i < \|\|v\|\|+1 & (x term_vars([u / v][i]))) (x term_vars(u) @ reduce(t,vs. term_vars(t) @ vs;nil;v))`