# numbering out of align with nested assumptions

Bug #266891 reported by Jesper R
Affects Status Importance Assigned to Milestone
Triaged
High
Unassigned

### Bug Description

\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}

Revision history for this message
 Dan Watkins (oddbloke) wrote on 2008-09-05: #1

Hi Jesper,

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

Cheers,

Dan

 Changed in naturaldeduction: assignee: nobody → daniel-thewatkins importance: Undecided → High status: New → Triaged
Revision history for this message
 Dan Watkins (oddbloke) wrote on 2008-09-05: #2

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.

Revision history for this message
 Jesper R (reenberg) wrote on 2008-09-05: #3

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}

Revision history for this message
 Jesper R (reenberg) wrote on 2008-09-05: #4

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)

:)

Revision history for this message
 Jesper R (reenberg) wrote on 2008-09-07: #5

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}

Dan Watkins (oddbloke)
 Changed in naturaldeduction: assignee: Daniel Watkins (daniel-thewatkins) → nobody
To post a comment you must log in.
This report contains Public information
Everyone can see this information.
Subscribing...

## Remote bug watches

Bug watches keep track of this bug in other bug trackers.