Nuprl - Pf member_col

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

c:(LabelCollection(Term)), r,r':rel(). r' col_subst2(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst2(as;r))

By: Unfold `col_subst2` 0 THEN Unfold `col_map_subst` 0 THEN RWW "member_col_map" 0 THEN RWW "member_col_list_prod" 0 THEN ExRepD THEN InstConcl [as] THEN AllHyps (RWW "map_length_nat") THEN Try ((((SubstFor as 0) THEN (RWW "unzip_zip" 0)) THEN (Reduce 0)) THEN (Complete Auto))

Generated subgoals:

1 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]))

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

About:

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

1	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]))`
2	1. `c:` `LabelCollection(Term)` 2. `r:` `rel()` 3. `r':` `rel()` 4. `as:` `(LabelTerm) List` 5. `1of(unzip(as)) = rel_primed_vars(r)` 6. `i:. i < \|\|as\|\| 2of(as[i]) c(1of(as[i]))` 7. `r' = rel_subst2(as;r)` `s:Term List. \|\|s\|\| = \|\|map(c;rel_primed_vars(r))\|\| & (i:. i < \|\|s\|\| s[i] map(c;rel_primed_vars(r))[i]) & as = zip(rel_primed_vars(r);s)`