partially unbreak innperseqs diagram

1 files changed, 1 insertions, 1 deletions

diff --git a/essays/post_formalism_memories.otx b/essays/post_formalism_memories.otx
index f5885d4..74f4377 100644
--- a/essays/post_formalism_memories.otx
+++ b/essays/post_formalism_memories.otx
@@ -126,7 +126,7 @@ An \term{innperseq} is a sequence of sequences of sentences on one radius satisf
 * The last sequence has one member. 
 \enditems}
 
-% \input innperseqs.diag.otx
+\input essays/innperseqs.diag.otx
 
 In diagram \ref[innperdiag], different positions of the vague outer ring at different times are suggested by different shadings. The outer segment moves \dq{down the page.} The figure is by no means an innperseq, but is supposed to help explain the definition. In \sysname{Innperseqs,} a conventional proof would be redundant unless all the statements were on the same radius. And even if the weakest axiom were chosen (the initial outer endpoint), this axiom would imply the initial inner endpoint, and from there the theorem could be reached immediately. In other words, to use the standard definition of \dq{\term{proof}} in \sysname{Innperseqs} would result in an uninteresting derivation structure. Thus, a more interesting derivation structure is defined, the \dq{\term{innperseq.}} The interest of an \dq{\term{innperseq}} is to be as elaborate as the many restrictions in its definition will allow. Proofs are either disregarded in \sysname{Innperseqs}; or else they are identified with innperseqs, and lack Property 8. \sysname{Innperseqs} makes the break with the proof-theorem structure of formalist mathematics.