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

At: member col subst 1
1. c: LabelCollection(Term)
2. r: rel()
3. r': rel()
4. as: (LabelTerm) List
5. s: Term List
6. ||s|| = ||rel_vars(r)||
7. i:. i < ||s|| s[i] map(c;rel_vars(r))[i]
8. as = zip(rel_vars(r);s)
9. r' = rel_subst(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_vars(r)||
s[i] c(rel_vars(r)[i])

About:
productlistless_thanapplyfunctionequalimpliesall

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