# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400650905 -32400
# Node ID 7138e79615b33deefe34b1f2e754bd424597db97
# Parent  ca2e9f7a7898e09342069feab842faab21dea990
Proof add-sym

diff -r ca2e9f7a7898 -r 7138e79615b3 int.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/int.agda	Wed May 21 14:41:45 2014 +0900
@@ -0,0 +1,35 @@
+open import systemT
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+module int where
+
+_+_ : Int -> Int -> Int
+n + O     = n
+n + (S m) = S (n + m)
+
+plus-one : (n m : Int) -> (S n) + m ≡ S (n + m)
+plus-one  n    O  = sym refl
+plus-one  n (S m) = cong S (plus-one n m)
+
+double : Int -> Int
+double O = O
+double (S n) = S (S (double n))
+
+sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n
+sum-sym    O     O  = refl
+sum-sym    O  (S m) = cong S (sum-sym O m)
+sum-sym (S n)    O  = cong S (sum-sym n O)
+sum-sym (S n) (S m) = begin
+    (S n) + (S m)  
+  ≡⟨ refl ⟩
+    S ((S n) + m)
+  ≡⟨ cong S (plus-one n m)⟩
+    S (S (n + m))
+  ≡⟨ cong (\x -> S (S x)) (sum-sym n m) ⟩
+    S (S (m + n))
+  ≡⟨ sym (cong S (plus-one m n)) ⟩
+    S ((S m) + n)
+  ≡⟨ refl ⟩
+    (S m) + (S n)
+  ∎
diff -r ca2e9f7a7898 -r 7138e79615b3 systemT.agda
--- a/systemT.agda	Tue May 13 11:14:49 2014 +0900
+++ b/systemT.agda	Wed May 21 14:41:45 2014 +0900
@@ -14,5 +14,4 @@
 
 D : {U : Set} -> U -> U -> Bool -> U
 D u v F = v
-D u v T = u
-
+D u v T = u
\ No newline at end of file