Mercurial > hg > Members > kono > Proof > category

changeset 340:1ff7b85e5bb2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ditr on system T
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 29 Mar 2014 23:12:12 +0900
parents 716f85bc7259
children 33bc037319fa
files system-t.agda
diffstat 1 files changed, 5 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/system-t.agda	Sat Mar 29 23:00:22 2014 +0900
+++ b/system-t.agda	Sat Mar 29 23:12:12 2014 +0900
@@ -228,8 +228,8 @@
    ∎
 
 
-lemma15assoc' : (y z w : Int) -> sum (mul y z) ( mul w z ) ≡ mul (sum y w)  z
-lemma15assoc' y zero w =  let open ≡-Reasoning in
+lemma15distr : (y z w : Int) -> sum (mul y z) ( mul w z ) ≡ mul (sum y w)  z
+lemma15distr y zero w =  let open ≡-Reasoning in
    begin
       sum (mul y zero) ( mul w zero ) 
    ≡⟨ cong ( \t -> sum (mul y zero ) t ) (lemma15 w zero ) ⟩
@@ -241,7 +241,7 @@
    ≡⟨ lemma15 zero (sum y w) ⟩
       mul (sum y w)  zero
    ∎
-lemma15assoc' y (S z) w =  let open ≡-Reasoning in
+lemma15distr y (S z) w =  let open ≡-Reasoning in
    begin
       sum (mul y (S z)) ( mul w (S z) )
    ≡⟨ cong ( \t -> sum t ( mul w (S z ))) (lemma15'' y z) ⟩
@@ -256,7 +256,7 @@
       sum  y ( sum  w  (sum ( mul w z) ( mul y z)) )
    ≡⟨  cong ( \t -> sum  y (sum w t) ) ( lemma14sym (mul w z) (mul y z ))  ⟩
       sum  y ( sum  w  (sum ( mul y z) ( mul w z)) )
-   ≡⟨  cong ( \t -> sum  y (sum w t) ) ( lemma15assoc' y z w )  ⟩
+   ≡⟨  cong ( \t -> sum  y (sum w t) ) ( lemma15distr y z w )  ⟩
       sum  y ( sum  w  (mul (sum y w)  z) )
    ≡⟨ lemma16assoc y w (mul (sum y w)  z) ⟩
       sum (sum y w) ( mul (sum y w)  z )
@@ -274,7 +274,7 @@
       sum (mul y z) ( mul x ( mul y z ) )
    ≡⟨ cong (\t -> sum (mul y z) t ) (lemma15assoc x y z ) ⟩
       sum (mul y z) ( mul ( mul x y) z ) 
-   ≡⟨ lemma15assoc' y z (mul x y) ⟩
+   ≡⟨ lemma15distr y z (mul x y) ⟩
       mul (sum y (mul x y))  z
    ≡⟨⟩
       mul (mul (S x) y)  z