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

At: member col subst2 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]))

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:

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


About:
productlistless_thanapplyfunctionequalimpliesall

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