From c188e082751a279577ce84702744618387721225 Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Fri, 22 Apr 2016 23:19:04 +0200
Subject: lds 01

---
 ss2016/lds/01/H1-2.md | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 ss2016/lds/01/H1-2.md

(limited to 'ss2016/lds/01/H1-2.md')

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 @@
+\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}
-- 
cgit v1.2.3