summaryrefslogtreecommitdiff
path: root/ss2016/lds/01/H1-2.md
diff options
context:
space:
mode:
Diffstat (limited to 'ss2016/lds/01/H1-2.md')
-rw-r--r--ss2016/lds/01/H1-2.md10
1 files changed, 10 insertions, 0 deletions
diff --git a/ss2016/lds/01/H1-2.md b/ss2016/lds/01/H1-2.md
new file mode 100644
index 0000000..43a35d1
--- /dev/null
+++ b/ss2016/lds/01/H1-2.md
@@ -0,0 +1,10 @@
1\begin{prooftree}
2\AxiomC{$A \seq A$}
3\RightLabel{\scriptsize $\lnot\ \text{R}$}
4\UnaryInfC{$\seq A, \lnot A$}
5\AxiomC{$A \seq A$}
6\RightLabel{\scriptsize $\limplies\ \text{L}$}
7\BinaryInfC{\lnot A \limplies A \seq A}
8\RightLabel{\scriptsize $\limplies\ \text{R}$}
9\UnaryInfC{$(\lnot A \limplies A) \seq A$}
10\end{prooftree}