Finished TMAM hanout

Advanced/Mock a Mockingbird/main.tex

@@ -7,6 +7,9 @@
 
 \usepackage{mathtools} % for \coloneqq
 
+%\usepackage{lua-visual-debug}
+
+\usepackage{censor}
 \usepackage{alltt}
 
 
@@ -37,10 +40,24 @@
 }
 
 % Logic block comment
-\newcommand{\cmnt}[1]{
+\newcommand{\cmnt}[1]{\textcolor{gray}{\# #1}}
-	\textcolor{gray}{\# #1}
+
+\newcounter{allttLineCounter}
+\setcounter{allttLineCounter}{0}
+
+\newcommand{\linenoref}[1]{\colorbox{gray!30!white}{#1}}
+\newcommand{\lineno}{
+	\stepcounter{allttLineCounter}%
+	\linenoref{\ifnum\value{allttLineCounter}<10 0\fi\arabic{allttLineCounter}}%
 }
 
+% Redefine alltt so it automatically
+% resets allttLineCounter
+\let\oldalltt\alltt
+\renewenvironment{alltt}
+	{\setcounter{allttLineCounter}{0}\begin{oldalltt}}
+	{\end{oldalltt}}
+
 
 \newcommand{\thus}{\(\Rightarrow\)}
 \newcommand{\qed}{\(\blacksquare\)}
@@ -59,5 +76,5 @@
 
 	\input{parts/00 intro}
 	\input{parts/01 tmam}
-
+	\input{parts/02 kestrel}
 \end{document}

Advanced/Mock a Mockingbird/parts/00 intro.tex

@@ -38,7 +38,9 @@ We say a bird $C$ \textit{composes} $A$ with $B$ if for any bird $x$,
 $$
 	Cx = A(Bx)
 $$
-In other words, this means that $C$'s response to $x$ is the same as $A$'s response to $B$'s response to $x$.
+In other words, this means that $C$'s response to $x$ is the same as $A$'s response to $B$'s response to $x$. \\
+Note that $C$ is exactly the kind of bird $L_1$ guarantees.
+
 
 \vfill
 \pagebreak

Advanced/Mock a Mockingbird/parts/01 tmam.tex

@@ -1,11 +1,11 @@
 \section{To Mock a Mockingbird}
 
 \problem{}
-The bear, a lifelong resident of the forest, tells you that any bird $A$ is fond of at least one other bird. \\
+Mark tells you that any bird $A$ is fond of at least one other bird. \\
 Complete his proof.
 \begin{alltt}
 	let A           \cmnt{Let A be any any bird.}
-	let Cx := A(Mx) \cmnt{Define C as the composition of A and M}
+	let Cx = A(Mx)  \cmnt{Define C as the composition of A and M}
 
 	\cmnt{The rest is up to you.}
 	CC = ??
@@ -20,17 +20,16 @@ Complete his proof.
 
 \begin{solution}
 	\begin{alltt}
-		let A           \cmnt{Let A be any any bird.}
+		\lineno{} let A           \cmnt{Let A be any any bird.}
-		let Cx := A(Mx) \cmnt{Define C as the composition of A and M}
+		\lineno{} let Cx = A(Mx)  \cmnt{Define C as the composition of A and M}
-		CC = A(MC)
+		\lineno{} CC = A(MC)
-		   = A(CC)  \qed{}
+		\lineno{}    = A(CC)  \qed{}
 	\end{alltt}
 \end{solution}
 
 \vfill
 \problem{}
-We say a bird $A$ is \textit{egocentric} if it is fond if itself.
+We say a bird $A$ is \textit{egocentric} if it is fond if itself. \\
-
 Show that the laws of the forest guarantee that at least one bird is egocentric.
 
 
@@ -42,12 +41,12 @@ Show that the laws of the forest guarantee that at least one bird is egocentric.
 
 \begin{solution}
 	\begin{alltt}
-		\cmnt{We know M is fond of at least one bird.}
+		\lineno{} \cmnt{We know M is fond of at least one bird.}
-		let E so that ME = E
+		\lineno{} let E so that ME = E
-
+		\lineno{}
-		ME = E     \cmnt{By definition of fondness}
+		\lineno{} ME = E     \cmnt{By definition of fondness}
-		ME = EE    \cmnt{By definition of M}
+		\lineno{} ME = EE    \cmnt{By definition of M}
-		\thus{} EE = E  \qed{}
+		\lineno{} \thus{} EE = E  \qed{}
 	\end{alltt}
 \end{solution}
 
@@ -57,7 +56,7 @@ Show that the laws of the forest guarantee that at least one bird is egocentric.
 
 \problem{}
 We say a bird $A$ is \textit{agreeable} if for all birds $B$, there is at least one bird $x$ on which $A$ and $B$ agree. \\
-This means that $Ax = Bx$.
+In other words, $A$ is agreeable if $Ax = Bx$ for some $x$ for all $B$.
 
 \begin{helpbox}
 	\texttt{Def:} $Mx := xx$
@@ -73,15 +72,14 @@ This means that $Ax = Bx$.
 
 \problem{}
 Take two birds $A$ and $B$. Let $C$ be their composition. \\
-Show that $A$ must be agreeable if $C$ is agreeable. \\
+Show that $A$ must be agreeable if $C$ is agreeable.
-The bear has again given you a hint.
 \begin{alltt}
 	\cmnt{Given information}
 	let A, B
-	let Cx := A(Bx)
+	let Cx = A(Bx)
 
 	let D            \cmnt{Arbitrary bird}
-	let Ex := D(Bx)  \cmnt{Define E as the composition of D and B}
+	let Ex = D(Bx)   \cmnt{Define E as the composition of D and B}
 	Cy = ??
 \end{alltt}
 
@@ -93,15 +91,16 @@ The bear has again given you a hint.
 
 \begin{solution}
 	\begin{alltt}
-		\cmnt{Given information}
+		\lineno{} \cmnt{Given information}
-		let A, B
+		\lineno{} let A, B
-		let Cx := A(Bx)
+		\lineno{} let Cx = A(Bx)
-
+		\lineno{}
-		let D           \cmnt{Arbitrary bird}
+		\lineno{} let D                  \cmnt{Arbitrary bird}
-		let Ex := D(Bx) \cmnt{Define E as the composition of D and B}
+		\lineno{} let Ex = D(Bx)         \cmnt{Define E as the composition of D and B}
-		Cy = Ey         \cmnt{For some y, because C is agreeable}
+		\lineno{} let y so that Cy = Ey  \cmnt{Such a y must exist because C is agreeable}
-		\thus{} A(By) = Ey
+		\lineno{}
-		\thus{} A(By) = D(By)  \qed{}
+		\lineno{} A(By) = Ey
+		\lineno{}       = D(By)  \qed{}
 	\end{alltt}
 \end{solution}
 
@@ -109,18 +108,18 @@ The bear has again given you a hint.
 \pagebreak
 
 \problem{}
-Given three arbitrary birds $A$, $B$, and $C$, show that there exists a bird $D$ defined by $Dx = A(B(Cx))$
+Given three arbitrary birds $A$, $B$, and $C$, show that there exists a bird $D$ satisfying $Dx = A(B(Cx))$
 
 \begin{solution}
 	\begin{alltt}
-		let A, B, C
+		\lineno{} let A, B, C
-
+		\lineno{}
-		\cmnt{Invoke the Law of Composition:}
+		\lineno{} \cmnt{Invoke the Law of Composition:}
-		let Q := BC
+		\lineno{} let Q = BC
-		let D := AQ
+		\lineno{} let D = AQ
-
+		\lineno{}
-		D = AQ
+		\lineno{} D = AQ
-		  = A(BC)  \qed{}
+		\lineno{}   = A(BC)  \qed{}
 	\end{alltt}
 \end{solution}
 
@@ -133,7 +132,7 @@ Note that $x$ and $y$ may be the same bird. \\
 Show that any two birds in this forest are compatible. \\
 \begin{alltt}
 	let A, B
-	let Cx := A(Bx)
+	let Cx = A(Bx)
 \end{alltt}
 
 \begin{helpbox}
@@ -143,16 +142,16 @@ Show that any two birds in this forest are compatible. \\
 
 \begin{solution}
 	\begin{alltt}
-		let A, B
+		\lineno{} let A, B
-
+		\lineno{}
-		let Cx := A(Bx)  \cmnt{Composition}
+		\lineno{} let Cx = A(Bx)  \cmnt{Composition}
-		let y := Cy      \cmnt{Let C be fond of y}
+		\lineno{} let y = Cy      \cmnt{Let C be fond of y}
-
+		\lineno{}
-		Cy = y
+		\lineno{} Cy = y
-		\thus{} A(By) = y
+		\lineno{}    = A(By)
-
+		\lineno{}
-		let x := By  \cmnt{Rename By to x}
+		\lineno{} let x = By  \cmnt{Rename By to x}
-		Ax = y  \qed{}
+		\lineno{} Ax = y  \qed{}
 	\end{alltt}
 \end{solution}
 
@@ -163,13 +162,13 @@ Show that any bird that is fond of at least one bird is compatible with itself.
 
 \begin{solution}
 	\begin{alltt}
-		let A
+		\lineno{} let A
-		let x so that Ax = x
+		\lineno{} let x so that Ax = x  \cmnt{A is fond of at least one other bird}
-		Ax = x  \qed{}
+		\lineno{} Ax = x  \qed{}
 	\end{alltt}
+
 	That's it.
 \end{solution}
 
-
 \vfill
 \pagebreak

Advanced/Mock a Mockingbird/parts/02 kestrel.tex

@@ -0,0 +1,137 @@
+\section{The Curious Kestrel}
+
+\definition{}
+Recall that a bird is \textit{egocenteric} if it is fond of itself. \\
+A bird is \textit{hopelessly egocentric} if $Bx = B$ for all birds $x$.
+
+\definition{}
+More generally, we say that a bird $A$ is \textit{fixated} on a bird $B$ if $Ax = B$ for all $x$. \\
+Convince yourself that a hopelessly egocentric bird is fixated on itself.
+
+
+
+\problem{}
+Say $A$ is fixated on $B$. Is $A$ fond of $B$?
+
+\begin{solution}
+	Yes! See the following proof.
+	\begin{alltt}
+		\lineno{} let B
+		\lineno{} let B
+		\lineno{} let A so that Ax = B
+		\lineno{} \thus{} AB = B \qed{}
+	\end{alltt}
+\end{solution}
+\vfill
+
+
+
+\definition{}
+The \textit{Kestrel} $K$ is defined by the following relationship:
+$$
+	(Kx)y = x
+$$
+In other words, this means that for every bird $x$, the bird $Kx$ is fixated on $x$.
+
+\problem{}
+Show that an egocenteric Kestrel is hopelessly egocentric
+
+\begin{solution}
+	\begin{alltt}
+		\lineno{} KK = K
+		\lineno{} \thus{} (KK)y = K
+		\lineno{} \thus{} Ky = K \qed{}
+	\end{alltt}
+\end{solution}
+
+\vfill
+\pagebreak
+
+
+\problem{}
+Assume the forest contains a Kestrel. \\
+Given $L_1$ and $L_2$, show that at least one bird is hopelessly egocentric.
+
+\begin{helpbox}[0.75]
+	\texttt{Def:} $K$ is defined by $(Kx)y = x$ \\
+	\texttt{Def:} $A$ is fond of $B$ if $AB = B$ \\
+	\texttt{???:} You'll need one more result from the previous section. Good luck!
+\end{helpbox}
+
+\begin{solution}
+	The final piece is a lemma we proved earler: \\
+	Any bird is fond of at least one bird
+
+	\begin{alltt}
+		\lineno{} let A so that KA = A   \cmnt{Any bird is fond of at least one bird}
+		\lineno{} (KA)y = y              \cmnt{By definition of the kestrel}
+		\lineno{} \thus{} Ay = A \qed{}  \cmnt{By 01}
+	\end{alltt}
+\end{solution}
+
+\vfill
+
+\problem{Kestrel Left-Cancellation}<leftcancel>
+In general, $Ax = Ay$ does not imply $x = y$. However, this is true if $A$ is $K$. \\
+Show that $Kx = Ky \implies x = y$.
+
+\begin{alltt}
+	\cmnt{This is a hint.}
+	let x, y so that Kx = Ky
+\end{alltt}
+
+\begin{solution}
+	\begin{alltt}
+		\lineno{} let x, y so that Kx = Ky
+		\lineno{} let z
+		\lineno{}
+		\lineno{} (Kx)z = (Ky)z  \cmnt{By 01}
+		\lineno{}
+		\lineno{} \cmnt{By the definition of K}
+		\lineno{} (Kx)z = x
+		\lineno{} (Ky)z = y
+		\lineno{}
+		\lineno{} \thus{} x = (Kx)z = (Ky)z = y \qed{}
+	\end{alltt}
+\end{solution}
+
+\vfill
+\pagebreak
+
+\problem{}
+Show that if $K$ is fond of $Kx$, $K$ is fond of $x$.
+
+\begin{solution}
+	\begin{alltt}
+		\lineno{} let x so that K(Kx) = Kx
+		\lineno{} (K(Kx))y = (Kx)y
+		\lineno{}          = Kx  \cmnt{By definition of K}
+		\lineno{} x = Kx  \cmnt{By 03 and definition of K}
+	\end{alltt}
+\end{solution}
+
+\vfill
+
+\problem{}
+An egocentric Kestrel must be extremely lonely. Why is this?
+
+\begin{solution}
+	If a Kestrel is egocenteric, it must be the only bird in the forest:
+
+	\begin{alltt}
+		\lineno{} \cmnt{Given}
+		\lineno{} Kx = K for some x
+		\lineno{} \cmnt{We have shown that an egocentric kestrel is hopelessly egocentric}
+		\lineno{} Kx = K for all x
+		\lineno{}
+		\lineno{} let x, y
+		\lineno{} Kx = K
+		\lineno{} Ky = K
+		\lineno{} Kx = Ky
+		\lineno{} x = y for all x, y  \cmnt{By \ref{leftcancel}}
+		\lineno{} x = y = K \qed{}  \cmnt{By 10, and since K exists}
+	\end{alltt}
+\end{solution}
+
+\vfill
+\pagebreak