\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=black,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}
\usepackage{amsmath,amssymb}
\usepackage{stmaryrd}   % for the tval symbol
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{trees}

\newcommand{\fn}[1]{\mathrm{#1}}
\newcommand{\append}{\mathbin{+\mkern-10mu+}}
\newcommand{\cons}{\mathbin{::}}
\newcommand{\tval}[1]{\llbracket #1 \rrbracket}
% If you don't have the stmaryrd package, the following substitute will do.
%\newcommand{\tval}[1]{[\![ #1 ]\!]}
\newcommand{\liff}{\leftrightarrow}
\newcommand{\fa}[1]{\forall #1. \, }
\newcommand{\ex}[1]{\exists #1. \, }
\newcommand{\mdl}[1]{\mathfrak{#1}}

\pagestyle{fancy}
\fancyhf{}
\renewcommand{\headrulewidth}{0pt}

\lhead{\sf Logic and Mechanized Reasoning}
\rhead{\sf Fall 2021}

\begin{document}

\bigskip

\begin{center}
{\Large Assignment 10}

\medskip

due 6pm Thursday, November 18, 2021
\end{center}

\medskip

\thispagestyle{fancy}

\noindent These problems rely on the latest version of the github lamr repository,
so be sure to use a new Gitpod image or update your repository following the instructions
in the README.


\subsection*{Problem 1 (6 points)}

Build the Tarski's World models that meet the specifications in {\tt assignment10a.lean}.

\subsection*{Problem 2 (1 point)}

\noindent In this problem and the next, $x$, $y$, and $z$ denote variables.

\medskip

\noindent Present a substitution that unifies $R(f(x), g(x))$ and $R(f(f(a)), g(f(y)))$.

\subsection*{Problem 3 (1 point)}

\noindent Present a substitution that unifies $f(x, h(x), y)$ and $f(g(z), w, z)$.

\subsection*{Problem 4 (6 points)}

Replace the definitions of of the functions {\tt sortGtConstraints} and {\tt elimVarGtConstraints}
in the file {\tt assignment10b.lean}
to meet the specifications indicated in that file.

\subsection*{Problem 5 (3 points)}

Present an equational proof of $f(a) = a$ from $f^5(a) = a$ and $f^8(a) = a$, where $f^n(a)$ abbreviates $n$-fold application $f(f(\cdots f(a)))$.
At each line indicate whether you are applying congruence to a previous line or some combination of symmetry and transitivity.
You can chain together as many instances of symmetry and transitivity as you like; just indicate which lines you are using.
For example, your proof might begin like this:
\begin{enumerate}
  \item $f^5(a) = a$, given
  \item $f^8(a) = a$, given
  \item $f^6(a) = f(a)$, congruence 1
  \item \ldots
\end{enumerate}

\end{document}