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:

$\displaystyle \mathcal{X} := \langle \mathcal{L} \times 2^\mathcal{L} \rangle $ where

$\displaystyle \mathcal{L} := \{a,b,c...,z,aa,bb,...,ab,ac,...\}$

$\displaystyle \mathcal{L}$ is merely a set of labels composed from small letters.

Examples of $\displaystyle \mathcal{X}$ are:

$\displaystyle x_1 = \langle a, \{ b, c, d\}\rangle $

$\displaystyle x_2 = \langle e, \{ f, g, h\}\rangle $

$\displaystyle x_3 = \langle i, \{ j, k, l\}\rangle $

$\displaystyle x_1, x_2, x_3 \in \mathcal{X}$

$\displaystyle \mathcal{Y}$ is the power set of $\displaystyle \mathcal{X}$

$\displaystyle \mathcal{Y} := 2^\mathcal{X}$

$\displaystyle y = \{ x_1\} \cup \{ x_2\} \cup \{x_3\} $

$\displaystyle y \in \mathcal{Y}$

Moreover, there are two types of substitutions, A and B:

$\displaystyle a_1 = \{ a \mapsto aa\}$

$\displaystyle a_2 = \{ e \mapsto ee\}$

$\displaystyle a_3 = \{ i \mapsto ii\}$

$\displaystyle a_1, a_2, a_2 \in \mathcal{A}$

$\displaystyle b_1 = \{ b \mapsto bb, c \mapsto cc, d \mapsto dd \}$

$\displaystyle b_2 = \{ f \mapsto ff, g \mapsto gg, h \mapsto hh \}$

$\displaystyle b_3 = \{ j \mapsto jj, k \mapsto kk, l \mapsto ll \}$

$\displaystyle b_1, b_2, b_3 \in \mathcal{B}$

Substitutions of type A work on the first element of an element of $\displaystyle \mathcal{X}$, while substitutions of type B work on the second element of $\displaystyle \mathcal{X}$.

$\displaystyle \mathcal{S} := 2^{\mathcal{A} \times \mathcal{B}}$

$\displaystyle \mathcal{S}$ represents the dependency between substitutions of type A and B. That is, they are grouped in pairs.

$\displaystyle s = \{ \langle a_1, b_1\rangle, \langle a_2, b_2\rangle, \langle a_3, b_3\rangle \} , s \in \mathcal{S}$

What I wonder is how to define and apply these substitutions correctly to achieve the following:

$\displaystyle y | s \equiv \{ \langle aa, \{ bb, cc, dd \} \rangle\ , \langle ee, \{ ff, gg, hh \} \rangle\ , \langle ii, \{ jj, kk, kk \} \rangle\}$

$\displaystyle y \in \mathcal{Y} , s \in \mathcal{S}$

| 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?