Nuprl - Pf member_col

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

1. c: LabelCollection(Term)
2. r: rel()
3. r': rel()
4. as: (LabelTerm) List
5. s: Term List
6. ||s|| = ||rel_primed_vars(r)||
7. i:. i < ||s|| s[i] map(c;rel_primed_vars(r))[i]
8. as = zip(rel_primed_vars(r);s)
9. r' = rel_subst2(as;r)
10. i:
11. i < ||as||

2of(as[i]) c(1of(as[i]))

By: MoveToConcl -1 THEN SubstFor as 0 THEN RWW "select_zip" 0 THEN Reduce 0 THEN Analyze 0 THEN RWW "length_zip" -1

Generated subgoal:

1 11. i < ||rel_primed_vars(r)||
s[i] c(rel_primed_vars(r)[i])

About:

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