# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1396102332 -32400
# Node ID 1ff7b85e5bb28cbc105a717295da2655c433d467
# Parent  716f85bc7259cf564311350f928a7f3067083c97
ditr on system T

diff -r 716f85bc7259 -r 1ff7b85e5bb2 system-t.agda
--- 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