c:(Label
Collection(Term)), r,r':rel().
r' 
col_subst(c;r)
(
as:(Label
Term) List.
1of(unzip(as)) = rel_vars(r)
& (i:
. i < ||as|| 
2of(as[i]) c(1of(as[i])))
& r' = rel_subst(as;r))
x.smts_eff(ss;x);r) col_list_prod(map(c;rel_vars(r))) > )
is mentioned by
|
Thm* c:(LabelCollection(Term)), r,r':rel().
r' col_subst(c;r)
(as:(LabelTerm) List.
1of(unzip(as)) = rel_vars(r)
& (i:. i < ||as|| 2of(as[i]) c(1of(as[i])))
& r' = rel_subst(as;r)) | [member_col_subst] |
|
Def smts_eff_rel(ss;r) == col_subst(x.smts_eff(ss;x);r) | [smts_eff_rel] |
Try larger context: GenAutomata