Compare commits

..

No commits in common. "73b8fb0dd13d12e75a420edf9eb8fa4df2fefc08" and "173015ffc9113346199c3de347713b7dd86e5d83" have entirely different histories.

View file

@ -134,7 +134,7 @@ Applications of induction and recursion:
on a class $A$.
Then there is a function $F\colon A \to \OR$,
such that for all $x,y \in A$
\[(x,y) \in R \implies F(x) < F(y).\]
\[(x,y) \in R \implies F(x) < F(y) F(x) < F(y).\]
\end{lemma}
\begin{proof}
By the recursion theorem,