# Adding Matrix Control: Insertion-Deletion Systems with Substitutions III
## 2 Definitions
### Adding Appearance Checking  
We have previously shown that there are even regular languages not included in \(\text{MAT}_{*}INS_{2}^{0,0}DEL_{2}^{0,0}SUB^{0,0}\). We now show that expanding these systems with appearance checking yields computational completeness. More precisely, we show that the expanded systems can simulate type-0 grammars in Penttonen normal form, which means that all of the production rules are of the form  
\[AB \to AC\text{ or }\] \[A \to BC\text{ or }\] \[A \to a\text{ or }\] \[A \to\lambda,\]  
where \(A,B,C\) are nonterminal symbols and \(a\) is a terminal symbol. Theorem 3.3: \(MAT_{*}^{\text{ac}}INS_{1}^{0,0}DEL_{2}^{0,0}SUB^{0,0}=RE\)  
**Proof. ** Because the inclusion \(\mathrm{MAT}_{*}^{\mathrm{ac}}\mathrm{NS}_{2}^{0,0}\mathrm{DEL}_{2}^{0,0}\mathrm{ SUB}^{0,0}\subseteq\mathrm{RE}\) is clear, we now proceed to prove the converse by simulating a type-0 grammar \(G=(N,T,P,S)\) in Penttonen normal form. The matrix ins-del-sub systems with appearance checking simulating \(G\) is defined as \(MID_{\zeta,\mathrm{ac}}=(V,T,\{\$S\$},M_{\zeta},F)\), with \(V=N\cup T\cup\{X,X_{1},X_{2},\$,\$^{\prime}\}\) and \((N\cup T)\cap\{X,X_{1},X_{2},\$,\$^{\prime}\}=\emptyset\). The nonterminal \(\$\) is an auxiliary symbol that marks the beginning of a sentential form, and it is eventually deleted by the matrix \([(\lambda,\$,\lambda)_{\mathrm{del}}]\). We now describe how the rules of \(G\) are simulated. For every rule of \(G\) of the form \(A\to a\), we add a matrix \([(\lambda,A\to a,\lambda)]\) to \(M_{\zeta}\), and, for every rule \(A\to\lambda\), we add the matrix \([(\lambda,A,\lambda)_{\mathrm{del}}]\) to \(M_{\zeta}\). We remark that the following matrices that are introduced to \(M_{\zeta}\) require the sentential form to have \(\$\) as the leftmost symbol. Hence, these rules cannot be applied if \(\$\) is absent. For every rule of the form \(AB\to AC\), to \(M_{\zeta}\), we add a matrix  
\[[(\lambda,\$\to\$^{\prime},\lambda),(\lambda,B\to X,\lambda),\] \[A \to BC\text{ or }\]0 \[A \to BC\text{ or }\]1  
with \(V\setminus\{A\}=\{A_{1},\ldots,A_{n}\}\). Add \(\{(\lambda,A_{1}X,\lambda)_{\mathrm{del}},\ldots,(\lambda,A_{n}X,\lambda)_{ \mathrm{del}}\}\) to \(F\). These deletion rules are used to check whether the left context of the \(B\), which is substituted by \(X\), has been \(A\). The basic idea is as follows: consider the application of the matrix above to \(\\[A \to BC\text{ or }\]2,\\[A \to BC\text{ or }\]3\to\\[A \to BC\text{ or }\]4^{\prime},\lambda)_{\mathrm{del}}),\] \[A \to BC\text{ or }\]5  
with \(\{A_{1}^{\prime},\ldots,A_{n}^{\prime}\}=V\setminus\{X_{1}\}\) to \(M_{\zeta}\). The deletion rules \((\lambda,A_{1}^{\prime}X_{1},\lambda),\ldots,(\lambda,A_{n}^{\prime}X_{1},\lambda)\) and \((\lambda,X_{2}\\[A \to BC\text{ or }\]6,\\[A \to BC\text{ or }\]7w\). Using the same argumentation as before, \((\lambda,A_{1}^{\prime}X_{2},\lambda),\ldots,(\lambda,A_{n}^{\prime}X_{2},\lambda)\) in \(F\) ensure that the left context of the inserted \(X_{2}\) is not an element of \(\{A_{1}^{\prime},\ldots,A_{n}^{\prime}\}=V\setminus\{X_{1}\}\). Additionally, if the matrix above has been successfully applied, then the deletion rule \((\lambda,X_{2}\\[A \to BC\text{ or }\]8^{\prime}\). This in turn means that \(X_{2}\) must have been inserted left of \(X_{1}\) and, therefore, it is clear that the above matrix simulates \(A\to BC\). We remark that applying any of the matrices, which simulate a production rule of \(G\), to a sentential form of \(MID_{\zeta,\mathrm{ac}}\), whose leftmost symbol is \(\\[A \to BC\text{ or }\]9\). By induction, we can show that \(S\Rightarrow_{G}^{*}w\) iff \(\\[A \to a\text{ or }\]0w\). \(\Box\)  
Additionally, we can show that \(\mathrm{MAT}_{*}^{\mathrm{ac}}\mathrm{INS}_{1}^{0,0}\mathrm{DEL}_{1}^{1,0} \mathrm{SUB}^{0,0}\) is also computationally complete. Theorem 3.2: \(\mathrm{MAT}_{*}^{\mathrm{ac}}\mathrm{INS}_{1}^{0,0}\mathrm{DEL}_{1}^{1,0} \mathrm{SUB}^{0,0}=RE\)_._Proof. : The idea is the same as in Theorem 9.