\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}