I have a question on how to "combine" substitutions in the sense that there is a dependency between two kinds of substitutions. I'll try to concretise this in an example.
I have a structure consisting of a pair:
is merely a set of labels composed from small letters.
Examples of are:
is the power set of
Moreover, there are two types of substitutions, A and B:
Substitutions of type A work on the first element of an element of , while substitutions of type B work on the second element of .
represents the dependency between substitutions of type A and B. That is, they are grouped in pairs.
What I wonder is how to define and apply these substitutions correctly to achieve the following:
| represents the action\operator that applies the substitutions correctly. That is, the substitutions of type B (second element of S) is only applied if the substitution of type A (first element of S) is applied.