Fin ejercicio reescritura

ej-csr/memoria.tex

@@ -224,15 +224,35 @@ Como todos los pares críticos tienen como posición $p=\wedge$, todos son pares
 
 \subsection{$\mu$-confluencia}
 
+De los pares $\mu$-críticos, el 1, 4 y 7 son triviales, por lo que $\mathcal{R}_{173}$ no es $\mu$-ortogonal. El resto de los pares son $\mu$-convergentes:
 
-\section{SRT $\mathcal{R}_{i}$}
+\begin{enumerate}
-\subsection{Función de reemplazamiento $\mu_{i}$}
+	\item[2.] $\texttt{max}(0,x) \hookrightarrow x$
-\subsection{Pares $\mu$-críticos}
+	\item[3.] $\texttt{max}(y,0) \hookrightarrow y$
-\subsection{$\mu$-confluencia}
+	\item[5.] $\texttt{max}(s(y),s(x)) \hookrightarrow s(\texttt{max}(y,x)) \hookleftarrow s(\texttt{max}(x,y))$
+	\item[6.] $x \hookleftarrow \texttt{max}(x,x)$
+\end{enumerate}
 
-\section{SRT $\mathcal{R}_{i}$}
+Por tanto ya sólo quedaría comprobar la $\mu$-terminación de $\mathcal{R}_{173}$ en la herramienta \textsc{MuTerm}, que indica que no es $\mu$-terminante. Por lo tanto, $\mathcal{R}_{173}$ es localmente $\mu$-confluente.
-\subsection{Función de reemplazamiento $\mu_{i}$}
+
+\section{SRT $\mathcal{R}_{163}$}
+\begin{lstlisting}
+(VAR x y z)
+(RULES
+  +(+(x, y), z) -> +(x, +(y, z))
+  +(x, +(y, z)) -> +(+(x, y), z)
+)
+\end{lstlisting}
+\subsection{Función de reemplazamiento $\mu_{163}$}
+Este SRT ha sido escogido por ser uno de los pocos en el rango 151-175 que no define la propiedad conmutativa para sus operaciones. Desafortunadamente, define la propiedad asociativa para la operación $+$, lo cual limita de forma similar las opciones disponibles de $\mu_{163}(+)$. Para intentar obtener un SRT que NO sea $\mu$-confluente, vamos a limitar $\mu_{163}(+)$ a $\emptyset$.
 \subsection{Pares $\mu$-críticos}
+Puesto que $\mathcal{R}_{163}$ se compone únicamente de 2 reglas, sólo existe una posibilidad dada la función $\mu_{163}$ escogida. El par crítico resultante es:
+$$(x' + (y' + y)) + z, (x'+y')+(y+z)$$
 \subsection{$\mu$-confluencia}
+La $\mu$-confluencia de nuevo requiere de la $\mu$-congruencia del par $\mu$-crítico y la $\mu$-terminación del sistema de reescritura.
+
+Respecto a la $\mu$-congruencia del par $\mu$-crítico, no se puede llegar a un término común $u$ que pueda ser $\mu$-derivado de $l$ y $r$ ($l \hookrightarrow^* u \wedge r \hookrightarrow^* u$), puesto que $r$ no es derivable y $l$ sólo se podría derivar a $x' + ((y' + y) + z)$.
+
+Por tanto, podemos determinar que el sistema de reescritura $\mathcal{R}_{163}$ no es $\mu$-confluente.
 
 \end{document}