Nuprl - Pf member_rel_primed

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

1. x: Label
2. name: relname()
3. r1: Term List
4. u: Term
5. v: Term List
6. (i:. i < ||v|| & (x term_primed_vars(v[i]))) (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v))
7. i:
8. i < ||v||+1
9. (x term_primed_vars([u / v][i]))

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

By: MoveToConcl -1 THEN CaseNat 0 `i' THEN Reduce 0 THEN RWW "member_append" 0 THEN Reduce 0 THEN TrivialOr

Generated subgoal:

1 9. i = 0
10. (x term_primed_vars([u / v][i]))
(x term_primed_vars(u)) (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v))

About:

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