Let $T \subseteq \Sigma^* \times \Sigma^*$ be a regular relation. We define the obligatory rewrite relation over $T$ as follows: $$ R^{obl}(T) := N(T) \cdot (T \cdot N(T))^* $$ $$ N(T) := Id(\Sigma^* \setminus (\Sigma^* \cdot dom(T) \cdot \Sigma^*)) \cup \{ \langle \epsilon, \epsilon \rangle \} $$ $N(T)$ is the identity relation of the set of all words that don't contain an infix in $dom(T)$ including the pair $\langle \epsilon, \epsilon \rangle$.
The idea is the following - we have an input string $t \in \Sigma^*$ and $R^{obl}(T)(t)$ will result in the translation of the substrings of $t$ which $\in dom(T)$ via $Т$, and the ones $\notin dom(T)$ via identity.
Example 1: $T = \{ \langle ab, d \rangle, \langle bc, d \rangle \}$, the input text $t = babacbca$ is decomposed as $t = b \cdot ab \cdot ac \cdot bc \cdot a$ and the substrings $\{ b,ac,a \} \subseteq dom(N(T))$, whereas, $\{ab, bc\} \subseteq dom(T)$. So $R^{obl}(T)(t) = b \cdot d \cdot ac \cdot d \cdot a = bdacda$
Example 2: $T = \{ \langle ab, d \rangle, \langle bc, d \rangle \}, t = abcc$. This time we have two possible decompositions due to overlapping. $t = ab \cdot cc = a \cdot bc \cdot c$, therefore, two possible translations $\langle abcc, dcc \rangle \in R^{obl}(T), \langle abcc, adc \rangle \in R^{obl}(T)$.
My questions is - how do we formulate a proof of correctness for such a construction? That it indeed translates the words as described
A bit of a context. I've studying rewrite systems based on regular relations (implemented as finite-state transducers) and more specifically the papers "Regular Models of Phonological Rule Systems" by Kaplan & Kay (1994) and "Directed Replacement" by Karttunnen (1996). They construct complex rewrite relations by using only the regular set and relation algebra, however, the papers do not provide formal proofs that their method is correct. If anyone has experience in this field and can provide some guidance, I'll greatly appreciate it.
