Mercurial > hg > Members > atton > agda > systemT

changeset 11:812de82556a2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof left-mult-distr-one
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 23 May 2014 11:57:11 +0900
parents c01d31399879
children ce0c3af2c34e
files int.agda
diffstat 1 files changed, 5 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/int.agda	Fri May 23 11:38:34 2014 +0900
+++ b/int.agda	Fri May 23 11:57:11 2014 +0900
@@ -135,12 +135,15 @@
     (S m) + (S n) + (S n * m)
   ≡⟨ sym (sum-assoc (S m) (S n) (S n * m)) ⟩
     (S m) + ((S n) + ((S n) * m))
-  ≡⟨ cong (\x -> (S m) + x) refl ⟩
+  ≡⟨ sum-sym (S m) (S n + S n * m) ⟩
+     ((S n) + ((S n) * m)) + S m
+  ≡⟨ cong (\x -> x + (S m)) (sym (right-mult-distr-one (S n) m )) ⟩
+    (S n) * (S m) + (S m)
+  ≡⟨ sum-sym (S n * S m) (S m) ⟩
     S m + S n * S m
   ∎
 
 
-
 mult-sym : (n m : Int) -> n * m ≡ m * n
 mult-sym n O     = begin
     n * O