Nuprl - Pf rel_primed_vars_rel

(6steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1. name: relname()
2. r1: Term List
3. x: Label
4. (x reduce(t,vs. term_primed_vars(t) @ vs;nil;r1))

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

By: MoveToConcl -1 THEN ListInd 2 THEN Reduce 0

Generated subgoals:

1 (x nil) (x nil)

2 4. u: Term
5. v: Term List
6. (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) (x reduce(t,vs. term_vars(t) @ vs;nil;v))
(x term_primed_vars(u) @ reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) (x term_vars(u) @ reduce(t,vs. term_vars(t) @ vs;nil;v))

About:

(6steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1	`(x nil) (x nil)`
2	4. `u:` `Term` 5. `v:` `Term List` 6. `(x reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) (x reduce(t,vs. term_vars(t) @ vs;nil;v))` `(x term_primed_vars(u) @ reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) (x term_vars(u) @ reduce(t,vs. term_vars(t) @ vs;nil;v))`