formatting; prevent orphaned header

Author: rzach

content/incompleteness/arithmetization-syntax/coding-formulas.tex

@@ -9,6 +9,10 @@
 \olfileid{inc}{art}{frm}
 \olsection{Coding \printtoken{P}{formula}}
 
+Once we have defined the relation $\fn{Term}(x)$ primitive
+recursively, we can use it to define the corresponding relation for
+!!{formula}s, $\fn{Frm}(x)$ primitive recursively.
+
 \begin{prop}
 The relation $\fn{Atom}(x)$ which holds iff $x$ is the G\"odel number
 of an atomic !!{formula}, is primitive recursive.

content/incompleteness/arithmetization-syntax/proofs-in-nd.tex

@@ -170,7 +170,8 @@
   $\fn{FollowsBy}_{\Intro\land}(d)$ as
   \begin{multline*}
     (d)_0 = 2 \land \fn{DischargeLabel}(d) = 0 \land \fn{LastRule}(d) = 1 \land {}\\
-    \fn{EndFmla}(d) = \Gn{(} \concat \fn{EndFmla}((d)_1) \concat \Gn{\land}
+    \fn{EndFmla}(d) = {}\\
+    \Gn{(} \concat \fn{EndFmla}((d)_1) \concat \Gn{\land}
     \concat \fn{EndFmla}((d)_2) \concat \Gn{)}.
   \end{multline*}
 
@@ -181,8 +182,8 @@
   \begin{multline*}
     (d)_0 = 1 \land (d)_1 = 0 \land \fn{DischargeLabel}(d) = 0 \land {}\\
     \bexists{t<d}{(\fn{ClTerm}(t) \land 
-      \fn{EndFmla}(d) = 
-      \Gn{{\eq}(} \concat t \concat \Gn{,} \concat t \concat \Gn{)})}
+      \fn{EndFmla}(d) = {}\\
+      \Gn{{\eq}(} \concat t \concat \Gn{,} \concat t \concat \Gn{)})}.
   \end{multline*}
 
   For a more complicated example, $\fn{FollowsBy}_{\Intro{\lif}}(d)$