## 4 Inverse Coupled Rewrite Systems
### ICORE Definitions  
**Definition 1**. : _Inverse coupled rewrite system._  
_Let \(k\) be a positive natural number. An ICORE of dimension \(k\) consists of_  
* _a set_ \(V\) _of variables,_
* \(a\) core _signature_ \(\zeta\)_, and_ \(k\) satellite _signatures_ \(\Sigma_{1},\ldots,\Sigma_{k}\)_, such that_ \(\zeta\cap(\Sigma_{1}\cup\ldots\cup\Sigma_{k})=\emptyset\)_. (Function symbols of_ \(\zeta\) _are disjoint from all_ \(\Sigma_{i}\)_, except for a possible shared alphabet. )_
* \(k\) _term rewrite systems with disjoint signatures,_ \(R_{1},\ldots,R_{k}\)_, which all have the same left-hand sides in_ \(T(\zeta,V)\)_. (Those systems are called the_ satellite rewrite systems_. )_
* _optionally a tree grammar_ \(\mathcal{G}\) _over the core signature_ \(\zeta\)_,_
* _an evaluation algebra_ \(A\) _for the core signature_ \(\zeta\)_, including an objective function_ \(\phi\)_._  
In the satellite rewrite systems, the multiple right-hand sides for the same left-hand side are also called _rule projections_ and are written in the form \(r_{1}\leftarrow\ell\to r_{2}\) for \(k=2\), or with a double arrow \(\ell\Rightarrow r_{1}\mid\ldots\mid r_{k}\) for any dimension \(k\). Since the core signature and the satellite signatures are disjoint, each rewrite step erases all operator symbols present in the left-hand side of the rewrite rules, and all satellite rewrite systems are terminating. No part of a term can be rewritten twice: Once an function symbol is read as part of a left-hand side, it is consumed. This ensures that a position in a term may take part in a rewrite only once, which corresponds to the classical edit model in string comparison: Each character in a string is to be edited at most once. This essential restriction compared to general term rewriting will be further discussed in Section 9.4. How to compute with an ICORE? We introduce the notion of _coupled rewriting_ which means in simple words that a core term is rewritten into \(k\) satellite terms by using the same rewrite rules in the same positions. Technically, this definition is a bit complicated as it requires to keep track of what are \"same\" positions over a series of rewrite steps. **Definition 2**. : _Coupled rewrite relation. Let \(c\) be a core term of \(T(\zeta,V)\), seen as a tree (This means that \(\sim\) symbols are omitted, and the position of a symbol is not modified when we apply associativity of \(\sim\)). We provide each operator symbol occuring in \(c\) with its initial position in \(c\) (for example using [PERSON]'s notation). A coupled rewrite of \(c\) is a sequence of \(k\) rewrite derivations \(c\rightarrow^{*}_{R_{1}}t_{1}\),..., \(c\rightarrow^{*}_{R_{k}}t_{k}\) such that there exist some number \(j\) and intermediate reducts \((t_{1}^{0},\ldots,t_{1}^{j}),\ldots,(t_{k}^{0},\ldots,t_{k}^{j})\) satisfying_  
1. \(c=t_{1}^{0}=\cdots=t_{k}^{0}\) _(start of a coupled derivation),_
2. \(t_{1}=t_{1}^{j}\)_,...,_ \(t_{k}=t_{k}^{j}\) _(end of a coupled derivation),_
3. _for each_ \(e\)_,_ \(0\leq e<j\) _(step in a coupled derivation), there exists a rule projection_ \(\ell\Rightarrow r_{1}\mid\ldots\mid r_{k}\) _such that_ \(t_{i}^{e}\) _rewrites modulo associativity to_ \(t_{i}^{e+1}\) _with the rule_ \(\ell\to r_{i}\) _and all rewrites apply simultaneously at the same place. In other words, for each_ \(i\)_, there is a term_ \(v_{i}\)_, a position_ \(p_{i}\) _in_ \(v_{i}\) _and a substitution_ \(\sigma_{i}\) _such that_ \(t_{i}^{e}=_{A}v_{i}\)_,_ \(v_{i}|_{p_{i}}=\ell\sigma_{i}\)_,_ \(t_{i}^{e+1}=v_{i}[r\sigma_{i}]_{p_{i}}\)_, and all operator symbols in_ \(\ell\) _have the same_ initial _position in_ \(c\)In the sequel, we shall write \(t_{1}\leftarrow^{*}c\rightarrow^{*}t_{2}\) to denote that \(c\rightarrow^{*}t_{1}\) and \(c\rightarrow^{*}t_{2}\) is a coupled derivation. We will use the double arrow symbol to designate a coupled rewrite of a core term \(c\) for any dimension \(k\), \(c\Rightarrow^{*}t_{1}\mid\ldots\mid t_{k}\). **Example 1**.