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

\begin{document}

\bigskip

\begin{center}
{\Large Assignment 10}

\medskip

due Wednesday, November 30
\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 (7 points)}

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

\subsection*{Problem 2 (3 points)}

\noindent In this problem, $x$, $y$, $z$, and $w$ denote variables. For each pair of expressions, present an assignment that unifies them, or explain why no such assignment exists.

\begin{enumerate}
\item $R(f(x), g(x))$ and $R(f(f(a)), g(f(y)))$
\item $f(x, h(x), y)$ and $f(g(z), w, z)$
\item $f(x, g(h(z)), y)$ and $f(g(y), x, z)$
\end{enumerate}

\subsection*{Problem 3 (7 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 4 (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}
