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

At: member col subst 2 2 3 1
1. c: LabelCollection(Term)
2. r: rel()
3. r': rel()
4. as: (LabelTerm) List
5. 1of(unzip(as)) = rel_vars(r)
6. i:. i < ||as|| 2of(as[i]) c(1of(as[i]))
7. r' = rel_subst(as;r)
8. i:
9. i < ||2of(unzip(as))||

rel_vars(r)[i] ~ 1of(as[i])
By:
Auto
THEN
Subst (rel_vars(r) ~ 1of(unzip(as))) 0
Generated subgoals:

110. rel_vars(r) = 1of(unzip(as))
11. x: Label List
12. y: Label List
13. x = y
x ~ y
2 1of(unzip(as))[i] = 1of(as[i])

About:
productlistless_thanapplyfunctionequalsqequalimpliesall

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