Mercurial > hg > Members > atton > agda > systemT

changeset 12:ce0c3af2c34e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Imporove proof
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 23 May 2014 12:10:42 +0900
parents 812de82556a2
children 5a81867278af
files int.agda
diffstat 1 files changed, 1 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/int.agda	Fri May 23 11:57:11 2014 +0900
+++ b/int.agda	Fri May 23 12:10:42 2014 +0900
@@ -135,11 +135,7 @@
     (S m) + (S n) + (S n * m)
   ≡⟨ sym (sum-assoc (S m) (S n) (S n * m)) ⟩
     (S m) + ((S n) + ((S n) * m))
-  ≡⟨ 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) ⟩
+  ≡⟨ cong (\x -> (S m) + x ) (sym (right-mult-distr-one (S n) m )) ⟩
     S m + S n * S m
   ∎