Mercurial > hg > Members > atton > agda > systemT

changeset 10:c01d31399879

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update left-mult-distr-one. but has yellow...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 23 May 2014 11:38:34 +0900
parents 8ad92d830679
children 812de82556a2
files int.agda
diffstat 1 files changed, 10 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/int.agda	Thu May 22 21:53:48 2014 +0900
+++ b/int.agda	Fri May 23 11:38:34 2014 +0900
@@ -126,12 +126,16 @@
   ≡⟨ sum-assoc ((S O) + (S n)) m (S n * m)  ⟩
     (S O) + (S n) + m + S n * m
   ≡⟨ cong (\x -> x + m + S n * m) (sum-sym (S O) (S n)) ⟩
-    (S n) + (S O) + m + S n * m
-  ≡⟨ cong (\x -> (S n) + x + (S n * m)) refl ⟩
-    (S n) + (S m) + S n * m
-  ≡⟨ cong (\x -> x + S n * m) (sum-sym (S n) (S m)) ⟩
-    (S m) + (S n) + S n * m
-  ≡⟨ cong (\x -> (S m + x)) refl ⟩
+    ((((S n) + (S O)) + m) + S n * m)
+  ≡⟨ cong (\x -> x + (S n * m)) (sym (sum-assoc (S n) (S O) m))⟩
+    (((S n) + ((S O) + m)) + S n * m)
+  ≡⟨ cong (\x -> (S n + x + S n * m)) (sym (left-add-one m)) ⟩
+    ((S n) + (S m) + S n * m)
+  ≡⟨ cong (\x -> x + (S n * m)) (sum-sym (S n) (S m)) ⟩
+    (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 ⟩
     S m + S n * S m
   ∎