numbering out of align with nested assumptions

[Jesper R]

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

[Dan Watkins (oddbloke)]

Hi Jesper,

Thanks for your bug report. I'm looking into what's going on right now.

Cheers,

Dan

[Dan Watkins (oddbloke)]

On a complete side note, you don't actually need the outer-most assumption box. If "$(p \to q) \to q$" is a premise then you can still reach the same conclusion.

The bug still happens even with that change.

[Jesper R (reenberg)]

Ok. Well technically there is one more error, but i guess it is related to the above;
When i write my conclusion at the bottom then it writes the line on top of the last line in the outer most assumption.

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

[Jesper R (reenberg)]

You are right, if it was a premise. But in this case it is not. I'm trying to prove the following

|- ((p -> q) -> q) -> (q -> p) -> p)

:)

[Jesper R (reenberg)]

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}