Comment 5 for bug 266891

Revision history for this message
Jesper R (reenberg) wrote :

Hmm i fiddled around and found out that when there are not enough room for the name of the used rule then it fucks up the formatting of the proof. So by adding more space in \begin{proof}{2in}{1in} fixed the formatting problem.

I also found a fundamental flow in my proof so i had to redo it.. but as you see here there still are some problems with the formatting of the width of the assumptions. Its like when you open and close enough they get out of allign..

And also i think you are defining a bit to much space between the name of the used rule and margin of the box. It should be the same distance as on the left from the box to start of the line. If you understand what I'm saying.

Also there could be some more space between lines. When you close an assumption and open one again right after the boxes are like glued together. Not that prety :)

Anyway the latex code is below:

\subsubsection{a)}
$((p \to q) \to q) \to ((q \to p) \to p)$

\begin{center}
  \begin{proof}{2in}{1in}
    \assumption{19}{
      \assume{$(p \to q) \to q$}
      \assumption{17}{
        \assume{$q \to p$}
        \state{$q \lor \neg q$}{LEM}
        \assumption{2}{
          \assume{$q$}
          \state{$p$}{$\to e$ 2, 4}
        }
        \assumption{12}{
          \assume{$\neg q$}
          \state{$p \lor \neg p$}{LEM}
          \assumption{1}{
            \assume{$p$}
          }
          \assumption{8}{
            \assume{$\neg p$}
            \state{$\neg (p \to q)$}{MT 1, 6}
            \assumption{3}{
              \assume{p}
              \state{$\bot$}{$\neg e$ 11, 9}
              \state{$q$}{$\bot e$ 12}
            }
            \state{$p \to q$}{$\to i$ 11-13}
            \state{$\bot$}{$\neg e$ 14, 10}
            \state{$p$}{$\bot e$ 15}
          }
          \state{$p$}{$\lor e$ 7, 8, 9-16}
        }
        \state{$p$}{$\lor e$ 3, 4-5, 6-17}
      }
      \state{$(q \to p) \to p$}{$\to i$ 2-18}
    }
    \state{$((p \to q) \to q) \to ((q \to p) \to p)$}{$\to i$ 1-19}
  \end{proof}
 \end{center}