blob: 43a35d1c03a712a25738e85a970da4c11af102b2 (
plain)
1
2
3
4
5
6
7
8
9
10
|
\begin{prooftree}
\AxiomC{$A \seq A$}
\RightLabel{\scriptsize $\lnot\ \text{R}$}
\UnaryInfC{$\seq A, \lnot A$}
\AxiomC{$A \seq A$}
\RightLabel{\scriptsize $\limplies\ \text{L}$}
\BinaryInfC{\lnot A \limplies A \seq A}
\RightLabel{\scriptsize $\limplies\ \text{R}$}
\UnaryInfC{$(\lnot A \limplies A) \seq A$}
\end{prooftree}
|
