(16steps)
PrintForm
Definitions
mb
automata
3
Sections
GenAutomata
Doc
At:
member
col
subst
2
1.
c:
Label
Collection(Term)
2.
r:
rel()
3.
r':
rel()
4.
as:
(Label
Term) 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)
s:Term List. ||s|| = ||map(c;rel_vars(r))||
& (
i:
. i < ||s||
s[i]
map(c;rel_vars(r))[i]) & as = zip(rel_vars(r);s)
By:
InstConcl [2of(unzip(as))]
Generated subgoals:
1
||2of(unzip(as))|| = ||map(c;rel_vars(r))||
2
8.
i:
9.
i < ||2of(unzip(as))||
2of(unzip(as))[i]
map(c;rel_vars(r))[i]
3
as = zip(rel_vars(r);2of(unzip(as)))
About:
(16steps)
PrintForm
Definitions
mb
automata
3
Sections
GenAutomata
Doc