Fix definition of OpenAssum(z,d).

As written, a discharge of the assumption by the final inference (0)
would be ignored. This commit fixes that.

Author: beastaugh

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

@@ -297,7 +297,7 @@
       \land (s)_0 = d \land {}} \\
     \bexists{n<d}{((s)_{\len{s} \tsub 1} = \tuple{0, z, n} \land {}}\\
       \bforall{i<(\len{s} \tsub 1)}{(\fn{Subderiv}((s)_{i+1}, (s)_i) \land {}}\\
-      \fn{DischargeLabel}((s)_{i+1}) \neq n))).
+      \fn{DischargeLabel}((s)_i) \neq n))).
   \end{multline*}
 \end{proof}