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

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

By: InstConcl [2of(unzip(as))]

Generated subgoals:

1 ||2of(unzip(as))|| = ||map(c;rel_primed_vars(r))||
28. i:
9. i < ||2of(unzip(as))||
2of(unzip(as))[i] map(c;rel_primed_vars(r))[i]
3 as = zip(rel_primed_vars(r);2of(unzip(as)))


About:
productlistless_thanapplyfunctionequalimpliesandallexists

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