Any smart guys here (substitutions)?

Hi,

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:

where

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.

Any ideas?