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

At: member col subst2 1 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 < ||rel_primed_vars(r)||

s[i] c(rel_primed_vars(r)[i])

By:
InstHyp [i] -5
THEN
RWW "map_select" -1


Generated subgoals:

None


About:
productlistless_thanapplyfunctionequalimpliesall

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