diff --git a/tarea5/memoria.tex b/tarea5/memoria.tex
new file mode 100644
index 0000000..f7c9617
--- /dev/null
+++ b/tarea5/memoria.tex
@@ -0,0 +1,155 @@
+\documentclass[a4paper]{article}
+
+\usepackage[utf8]{inputenc}
+\usepackage[spanish]{babel}
+\usepackage{amsmath}
+\usepackage{amssymb}
+
+\author{Carlos S. Galindo Jiménez}
+\title{FLA - Tarea 5}
+
+\begin{document}
+\maketitle
+Las reglas que componen $E$ son las siguientes:
+
+\begin{align}
+&f(0) \rightarrow 0 \\
+&g(0) \rightarrow 0 \\
+&f(g(X)) \rightarrow g(X) \\
+&(X = X) \rightarrow \texttt{True}
+\end{align}
+
+Para diferenciar las variables, a cada nivel de profundidad cada variable $A$ se renombra a $A_i$, donde $i$ es el nivel actual de profundidad. El término inicial es:
+
+$$f(Z)=Z$$
+
+Desde aquí se pueden realizar varias combinaciones, con la siguiente nomenclatura: $p$ es la posición, $E_i: l_i \rightarrow r_i$ es la regla i-ésima y $\sigma$ es el unificador mediante el cual el término original $t$ se convierte  en $s=(t[r_i]_p)\sigma$. $\sigma$ es el mgu de $t|_p$ y $l_i$. La columna ``Hoja'' indica $\checkmark$ si es hoja y resulta en \texttt{True}, $\times$ si falla, `-' si tiene hijos y `$\sim$' si tiene hijos que resultan en \texttt{True} pero su exploración es simplemente reescritura.
+
+\begin{center}
+\begin{tabular}{| l | l | l | l | c | c |} \hline
+n & i & p & $\sigma$ & $s$ & Hoja \\ \hline
+1 & 1 & 1 & $Z/0$ & $0 = 0$ & $\checkmark$ \\
+2 & 1 & 1.1 & $Z/f(0)$ & $f(0) = f(0)$ & $\checkmark$ \\
+3 & 1 & 2 & $Z/f(0)$ & $f(0) = 0$ & $\sim$ \\ \hline
+4 & 2 & 1 & $\nexists$ & - & $\times$ \\
+5 & 2 & 1.1 & $Z/g(0)$ & $f(0)=g(0)$ & $\sim$ \\
+6 & 2 & 2 & $Z/g(0)$ & $f(g(0))=0$ & $\sim$ \\ \hline
+7 & 3 & 1 & $Z/g(X_1)$ & $g(X_1)=g(X_1)$ & $\checkmark$ \\
+8 & 3 & 1.1 & $Z/f(g(X_1))$ & $f(g(X_1))=f(g(X_1))$ & $\checkmark$ \\
+9 & 3 & 2 & $Z/f(g(X_1))$ & $f(f(g(X_1))) = g(X_1)$ & - \\ \hline
+\end{tabular}
+\end{center}
+
+Una vez desarrollado el primer nivel, todas aquellos estados que no hayan concluido de forma positiva o negativa tienen que sufrir el mismo procedimiento. Para simplificar el árbol, vamos a simplificar todos aquellos que no tengan variables en un solo paso, por lo que el número 3 sería $f(0)=0 \rightarrow 0=0 \rightarrow \texttt{True}$, y del mismo modo lo serían el 5 y 6. En las siguientes tablas vamos a omitir las posiciones para las cuales no existe un unificador $\sigma$ válido.
+
+En las siguientes tablas vamos a explorar las posibilidades que ofrece el caso 9. La nomenclatura para los casos hijos será $9.i$, para cada hijo de 9, y así sucesivamente.
+
+$$f(f(g(X_1)))=g(X_1)$$
+
+\begin{center}
+\begin{tabular}{| l | l | l | l | c | c |} \hline
+n & i & p & $\sigma$ & $s$ & Hoja \\ \hline
+9.1 & 1 & 1.1.1.1 & $X_1/f(0)$ & $f(f(g(0)))=g(f(0))$ & $\sim$ \\
+9.2 & 1 & 2.1 & $X_1/f(0)$ & $f(f(g(f(0))))=g(0)$ & $\sim$ \\ \hline
+9.3 & 2 & 1.1.1 & $X_1/0$ & $f(f(0))=g(0)$ & $\sim$ \\
+9.4 & 2 & 1.1.1.1 & $X_1/g(0)$ & $f(f(g(0)))=g(g(0))$ & $\sim$ \\
+9.5 & 2 & 2 & $X_1/0$ & $f(f(g(0)))=0$ & $\sim$ \\
+9.6 & 2 & 2.1 & $X_1/g(0)$ & $f(f(g(g(0))))=g(0)$ & $\sim$ \\ \hline
+9.7 & 3 & 1.1 & $X_1/X_2$ & $f(g(X_2))=g(X_2)$ & - \\
+9.8 & 3 & 1.1.1.1 & $X_1/f(g(X_2))$ & $f(f(g(g(X_2))))=g(f(g(X_2)))$ & - \\
+9.9 & 3 & 2.1 & $X_1/f(g(X_2))$ & $f(f(g(f(g(X_2)))))=g(g(X_2))$ & - \\ \hline
+\end{tabular}
+\end{center}
+
+Para el tercer nivel, la búsqueda se ramifica aún más, puesto que 9.7, 9.8 y 9.9 pueden continuar:
+
+\begin{center}
+\begin{tabular}{| l | l | l | l | c | c |} \hline
+n & i & p & $\sigma$ & $s$ & Hoja \\ \hline
+9.7.1 & 1 & 1.1.1 & $X_2/f(0)$ & $f(g(0))=g(f(0))$ & $\sim$ \\
+9.7.2 & 1 & 2.1 & $X_2/f(0)$ & $f(g(f(0)))=g(0)$ & $\sim$ \\ \hline
+9.7.3 & 2 & 1.1 & $X_2/0$ & $f(0)=g(0)$ & $\sim$ \\
+9.7.4 & 2 & 1.1.1 & $X_2/g(0)$ & $f(g(0))=g(g(0))$ & $\sim$ \\
+9.7.5 & 2 & 2 & $X_2/0$ & $f(g(0))=0$ & $\sim$ \\
+9.7.6 & 2 & 2.1 & $X_2/g(0)$ & $f(g(g(0)))=g(0)$ & $\sim$ \\ \hline
+9.7.7 & 3 & 1 & $X_2/X_3$ & $g(X_3)=g(X_3)$ & $\checkmark$ \\
+9.7.8 & 3 & 1.1.1 & $X_2/f(g(X_3))$ & $f(g(g(X_3)))=g(f(g(X_3)))$ & - \\
+9.7.9 & 3 & 2.1 & $X_2/f(g(X_3))$ & $f(g(f(g(X_3))))=g(g(X_3))$ & - \\ \hline
+9.8.1 & 1 & 1.1.1.1.1 & $X_2/f(0)$ & $f(f(g(g(0))))=g(f(g(f(0))))$ & $\sim$ \\
+9.8.2 & 1 & 2.1.1.1 & $X_2/f(0)$ & $f(f(g(g(f(0)))))=g(f(g(0)))$ & $\sim$ \\ \hline
+9.8.3 & 2 & 1.1.1.1 & $X_2/0$ & $f(f(g(0)))=g(f(g(0)))$ & $\sim$ \\
+9.8.4 & 2 & 1.1.1.1.1 & $X_2/g(0)$ & $f(f(g(0)))=g(f(g(g(0))))$ & $\sim$ \\
+9.8.5 & 2 & 2.1.1 & $X_2/0$ & $f(f(g(g(0))))=g(f(0))$ & $\sim$ \\
+9.8.6 & 2 & 2.1.1.1 & $X_2/g(0)$ & $f(f(g(g(g(0)))))=g(f(0))$ & $\sim$ \\ \hline
+9.8.7 & 3 & 1.1 & $X/g(X_3),X_2/X_3$ & $f(g(g(X_3)))=g(f(g(X_3)))$ & - \\
+9.8.8 & 3 & 1.1.1.1.1 & $X_2/f(g(X_3))$ & $f(f(g(g(g(X_3)))))=g(f(g(f(g(X_3)))))$ & - \\
+9.8.9 & 3 & 2.1 & $X_2/X_3$ & $f(f(g(g(X_3))))=g(g(X_3))$ & - \\
+9.8.10 & 3 & 2.1.1.1 & $X_2/f(g(X_3))$ & $f(f(g(g(f(g(X_3))))))=g(g(X_3))$ & - \\ \hline
+\end{tabular}
+\begin{tabular}{| l | l | l | l | c | c |} \hline
+9.9.1 & 1 & 1.1.1.1.1.1 & $X_2/f(0)$ & $f(f(g(f(g(0)))))=g(g(f(0)))$ & $\sim$ \\
+9.9.2 & 1 & 2.1.1 & $X_2/f(0)$ & $f(f(g(f(g(f(0))))))=g(g(0))$ & $\sim$ \\ \hline
+9.9.3 & 2 & 1.1.1.1.1 & $X_2/0$ & $f(f(g(f(0))))=g(g(0))$ & $\sim$ \\
+9.9.4 & 2 & 1.1.1.1.1.1 & $X_2/g(0)$ & $f(f(g(f(0))))=g(g(g(0)))$ & $\sim$ \\
+9.9.5 & 2 & 2.1 & $X_2/0$ & $f(f(g(f(g(0)))))=g(0)$ & $\sim$ \\
+9.9.6 & 2 & 2.1.1 & $X_2/g(0)$ & $f(f(g(f(g(g(0))))))=g(g(0))$ & $\sim$ \\ \hline
+9.9.7 & 3 & 1.1 & $X/f(g(X_3)),X_2/X_3$ & $f(g(f(g(X_3))))=g(g(X_3))$ & - \\
+9.9.8 & 3 & 1.1.1.1 & $X_2/X_3$ & $f(f(g(g(X_3))))=g(g(X_3))$ & - \\
+9.9.9 & 3 & 1.1.1.1.1.1 & $X_2/f(g(X_3))$ & $f(f(g(f(g(g(X_3))))))=g(g(f(g(X_3))))$ & - \\
+9.9.10 & 3 & 2.1.1 & $X_2/f(g(X_3))$ & $f(f(g(f(g(f(g(X_3)))))))=g(g(g(X_3)))$ & - \\ \hline
+\end{tabular}
+\end{center}
+
+Tras completar la tercera expansión, tenemos 10 ecuaciones, correspondientes a las generadas mediante la regla 3. Como la expansión no tiene fin, vamos a realizar una última expansión, considerando sólo la regla de reescritura 3.
+
+\begin{center}
+\begin{tabular}{| l | l | c | c |} \hline
+n & p & $s$ & Hoja \\ \hline
+9.7.8.1 & 1 & $g(g(X_4))=g(f(g(X_4)))$ & - \\
+9.7.8.2 & 1.1.1.1 & $f(g(g(g(X_4))))=g(f(g(f(g(X_4)))))$ & - \\
+9.7.8.3 & 2.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
+9.7.8.4 & 2.1.1.1 & $f(g(g(f(g(X_4)))))=g(f(g(g(X_4))))$ & - \\ \hline
+9.7.9.1 & 1 & $g(f(g(X_4)))=g(g(X_4))$ & - \\
+9.7.9.2 & 1.1.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
+9.7.9.3 & 1.1.1.1.1 & $f(g(f(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
+9.7.9.4 & 2.1.1 & $f(g(f(g(f(g(X_4))))))=g(g(g(X_4)))$ & - \\ \hline \hline
+9.8.7.1 & 1 & $g(g(X_4))=g(f(g(X_4)))$ & - \\
+9.8.7.2 & 1.1.1.1 & $(f(g(g(g(X_4)))))=g(f(g(f(g(X_4)))))$ & - \\
+9.8.7.3 & 2.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
+9.8.7.4 & 2.1.1.1 & $f(g(g(f(g(X_4)))))=g(f(g(g(X_4))))$ & - \\ \hline
+9.8.8.1 & 1.1 & $f(g(g(g(X_4))))=g(f(g(f(g(X_4)))))$ & - \\
+9.8.8.2 & 1.1.1.1.1.1 & $f(f(g(g(g(g(X_4))))))=g(f(g(f(g(f(g(X_4)))))))$ & - \\
+9.8.8.3 & 2.1 & $f(f(g(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
+9.8.8.4 & 2.1.1.1 & $f(f(g(g(g(X_4)))))=g(f(g(g(X_4))))$ & - \\
+9.8.8.5 & 2.1.1.1.1.1 & $f(f(g(g(g(f(g(X_4)))))))=g(f(g(f(g(g(X_4))))))$ & - \\ \hline
+9.8.9.1 & 1.1 & $f(g(g(g(X_4))))=g(g(X_4))$ & - \\
+9.8.9.2 & 1.1.1.1.1 & $f(f(g(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
+9.8.9.3 & 2.1.1 & $f(f(g(g(f(g(X_4))))))=g(g(g(X_4)))$ & - \\ \hline
+9.8.10.1 & 1.1 & $f(g^3(f(g(X_4))))=g(g(X_4))$ & - \\
+9.8.10.2 & 1.1.1.1.1 & $f(f(g^3(X_4)))=g(g(X_4))$ & - \\
+9.8.10.3 & 1.1.1.1.1.1.1 & $f(f(g(g(f(g(g(X_4)))))))=g(g(f(g(X_4))))$ & - \\
+9.8.10.4 & 2.1.1 & $f(f(g(g(f(g(f(g(X_4))))))))=g(g(g(X_4)))$ & - \\ \hline \hline
+9.9.7.1 & 1 & $g(f(g(X_4)))=g(g(X_4))$ & - \\
+9.9.7.2 & 1.1.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
+9.9.7.3 & 1.1.1.1.1 & $f(g(f(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
+9.9.7.4 & 2.1.1 & $f(g(f(g(f(g(X_4))))))=g(g(g(X_4)))$ & - \\ \hline
+9.9.8.1 & 1.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
+\end{tabular}
+\begin{tabular}{| l | l | c | c |}
+9.9.8.2 & 1.1.1.1.1 & $f(f(g^3(X_4)))=g(g(f(g(X_4))))$ & - \\
+9.9.8.3 & 2.1.1 & $f(f(g(g(f(g(X_4))))))=g(g(g(X_4)))$ & - \\ \hline
+9.9.9.1 & 1.1 & $f(g(f(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
+9.9.9.2 & 1.1.1.1 & $f(f(g^3(X_4)))=g(g(f(g(X_4))))$ & - \\
+9.9.9.3 & 1.1.1.1.1.1.1 & $f(f(g(f(g^3(X_4)))))=g(g(f(g(f(g(X_4))))))$ & - \\
+9.9.9.4 & 2.1.1 & $f(f(g(f(g(g(X_4))))))=g^3(X_4)$ & - \\
+9.9.9.5 & 2.1.1.1.1 & $f(f(g(f(g(g(f(g(X_4))))))))=g(g(f(g(g(X_4)))))$ & - \\ \hline
+9.9.10.1 & 1.1 & $f(g(f(g(f(g(X_4))))))=g^3(X_4)$ & - \\
+9.9.10.2 & 1.1.1.1 & $f(g(g(f(g(X_4)))))=g^3(X_4)$ & - \\
+9.9.10.3 & 1.1.1.1.1.1 & $f(f(g(f(g(g(X_4))))))=g^3(X_4)$ & - \\
+9.9.10.4 & 1.1.1.1.1.1.1.1 & $f(f(g(f(g(f(g(g(X_4))))))))=g^3(f(g(X_4)))$ & - \\
+9.9.10.5 & 2.1.1.1 & $f(f(g(f(g(f(g(f(g(X_4)))))))))=g^4(X_4)$ & - \\ \hline
+\end{tabular}
+\end{center}
+
+Como se puede observar, se van generando expresiones más complejas, a la vez que se van generanndo otras más simples, que en dos o tres niveles se instanciarán a $X_i/0$, $X_i/f(0)$ o $X_i/g(0)$ y generarán otra hoja con resultado \texttt{True}. Este ciclo continuará de forma infinita, y posiblemente a estas alturas se pudiera simplificar buscando repeticiones.
+\end{document}
\ No newline at end of file
diff --git a/tarea5/memoria_corregida.tex b/tarea5/memoria_corregida.tex
new file mode 100644
index 0000000..c5ac9ad
--- /dev/null
+++ b/tarea5/memoria_corregida.tex
@@ -0,0 +1,63 @@
+\documentclass[a4paper]{article}
+
+\usepackage[utf8]{inputenc}
+\usepackage[spanish]{babel}
+\usepackage{amsmath}
+\usepackage{amssymb}
+
+\author{Carlos S. Galindo Jiménez}
+\title{FLA - Tarea 5}
+
+\begin{document}
+\maketitle
+Las reglas que componen $E$ son las siguientes:
+
+\begin{align}
+&f(0) \rightarrow 0 \\
+&g(0) \rightarrow 0 \\
+&f(g(X)) \rightarrow g(X) \\
+&(X = X) \rightarrow \texttt{True}
+\end{align}
+
+Para diferenciar las variables, a cada nivel de profundidad cada variable $A$ se renombra a $A_i$, donde $i$ es el nivel actual de profundidad. El término inicial es:
+
+$$f(Z)=Z$$
+
+Desde aquí se pueden realizar varias combinaciones, con la siguiente nomenclatura:
+\begin{itemize}
+	\item $t\rightsquigarrow s$ es un paso de narrowing
+	\item $p$ es la posición del redex, y no puede ser una variable
+	\item $E_i: l_i \rightarrow r_i$ es la regla i-ésima
+	\item $\sigma$ es el $mgu(t|_p,l_i)$
+\end{itemize}
+
+$$s=(t[r_i]_p)\sigma$$
+
+% TODO: p no puede ser la de una variable
+% TODO: un final tiene que acabar en true, no en A = A
+\begin{center}
+\begin{tabular}{| l | l | l | l | c |} \hline
+n & i & p & $\sigma$ & $s$ \\ \hline
+1 & 1 & 1 & $Z/0$ & $0 = 0$ \\
+2 & 2 & 1 & $\nexists$ & - \\
+3 & 3 & 1 & $Z/g(X_1)$ & $g(X_1)=g(X_1)$ \\ \hline \hline
+1.1 & 4 & $\wedge$ & $X/0$ & \texttt{True} \\
+3.1 & 4 & $\wedge$ & $X/g(X_1)$ & \texttt{True} \\
+3.2 & 2 & 1 & $X_1/0$ & $0=g(0)$ \\
+3.3 & 2 & 2 & $X_1/0$ & $g(0)=0$ \\ \hline \hline
+3.2.1 & 2 & 2 & $\emptyset$ & $0=0$ \\
+3.2.1.1 & 4 & $\wedge$ & $X/0$ & \texttt{True} \\
+3.3.1 & 2 & 1 & $\emptyset$ & $0=0$ \\
+3.3.1.1 & 4 & $\wedge$ & $X/0$ & \texttt{True} \\ \hline
+\end{tabular}
+\end{center}
+
+De los 4 finales obtenidos (1.1, 3.1, 3.2.1.1 y 3.3.1.1) podemos obtener los cuatro unificadores:
+
+\begin{description}
+	\item [1.1] $\sigma_1=\{Z/0\}$
+	\item [3.1] $\sigma_2=\{Z/g(X_1)\}$
+	\item [3.2.1.1] $\sigma_3=\{Z/g(0)\}$
+	\item [3.3.1.1] $\sigma_4=\{Z/g(0)\}$
+\end{description}
+\end{document}
\ No newline at end of file