--- a/system-f.agda	Mon Mar 24 16:45:25 2014 +0700
+++ b/system-f.agda	Sat Mar 29 17:12:33 2014 +0900
@@ -149,6 +149,13 @@
 mul : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X
 mul {l} {X} x y = It Zero (add x) y
 
+--   λ x y → y y y y x
+--   λ x y → y y y x
+--   λ z t →   (λ x y → y y y y x) (λ x y → y y y y x) (λ x y → y y y y x) t
+--   λ z t →            t t t t             t t t t             t t t t    z
+-- mul : {l : Level } {X : Set l} → Int X → Int X → Int X
+-- mul {l} {X} x y = λ z t → x z ( λ w → y ? ? )
+
 fact : {l : Level} {X : Set l} → Int _ → Int X
 fact  {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w) ) n
 

--- a/system-t.agda	Mon Mar 24 16:45:25 2014 +0700
+++ b/system-t.agda	Sat Mar 29 17:12:33 2014 +0900
@@ -141,10 +141,90 @@
    ∎
 
 
--- lemma14 : (x y : Int) -> sum x y  ≡ sum y x
--- lemma14 zero zero = refl
--- lemma14 zero (S t) = cong (\x -> S x )( lemma14 zero t)
--- lemma14 (S t) t' = cong (\x -> {!!} ) (lemma14 t t')
+lemma13 : (x y : Int) -> sum x (S y)  ≡ S (sum x y )
+lemma13 zero y = refl
+lemma13 (S x) y = cong (\x -> S x ) (lemma13  x y )
+
+lemma14 : (x y : Int) -> sum x y  ≡ sum y x
+lemma14 zero zero = refl
+lemma14 zero (S t) = cong (\x -> S x )( lemma14 zero t)
+lemma14 (S t) zero = cong (\x -> S x ) ( lemma14 t zero )
+lemma14 (S t) (S t') =  let open ≡-Reasoning in 
+   begin 
+       sum (S t) (S t')
+   ≡⟨⟩
+       R (S t') ( λ z -> λ w -> S z ) (S t)
+   ≡⟨⟩
+       S ( R (S t') ( λ z -> λ w -> S z ) t) 
+   ≡⟨ cong ( \x -> S x ) ( lemma13 t t') ⟩
+       S ( S ( R t' ( λ z -> λ w -> S z ) t)) 
+   ≡⟨ cong ( \x -> S (S x ) ) ( lemma14 t t') ⟩
+       S ( S ( R t ( λ z -> λ w -> S z )  t'))
+   ≡⟨ sym ( cong ( \x -> S x ) ( lemma13 t' t)) ⟩
+       S ( R (S t) ( λ z -> λ w -> S z )  t')
+   ≡⟨⟩
+       R (S t) ( λ z -> λ w -> S z ) (S t')
+   ≡⟨⟩
+       sum (S t') (S t)
+   ∎
+
+lemma15assoc' : (x y : Int) -> S ( sum x y ) ≡ sum x (S y )
+lemma15assoc' zero _ = refl
+lemma15assoc' (S x) y = cong (\x -> S x ) ( lemma15assoc' x y  )
+
+lemma15assoc : (x y z : Int) -> sum x (sum y z ) ≡ sum y (sum x z )
+lemma15assoc zero y z  = refl
+lemma15assoc (S x) y z =  let open ≡-Reasoning in
+   begin
+     sum (S x) (sum y z)
+   ≡⟨⟩
+     S ( sum x (sum y z) )
+   ≡⟨ cong (\x -> S x ) ( lemma15assoc x y z ) ⟩
+     S ( sum y ( sum x z)  )
+   ≡⟨ lemma15assoc' y (sum x z )⟩
+     sum y (S ( sum x z) )
+   ≡⟨⟩
+     sum y (sum (S x) z)
+   ∎
 
 
-                   
+lemma15'' : (x y : Int) -> mul x (S y) ≡ sum x ( mul x y )
+lemma15'' zero y = refl
+lemma15'' (S x) y =   let open ≡-Reasoning in
+   begin
+     mul (S x) (S y)
+   ≡⟨⟩
+     sum (S y) (mul x (S y))
+   ≡⟨⟩
+     S (sum y (mul x (S y)  ))
+   ≡⟨ cong (\t -> S ( sum y t )) (lemma15'' x y ) ⟩
+     S (sum y (sum x (mul x y)))
+   ≡⟨ cong (\x -> S x ) (lemma15assoc y x (mul x y)) ⟩
+     S (sum x (sum y (mul x y) ))
+   ≡⟨⟩
+     S (sum x (mul (S x) y ) )
+   ≡⟨⟩
+     sum (S x) (mul (S x) y)
+   ∎
+
+lemma15' : (x : Int) -> mul zero x  ≡ mul x zero 
+lemma15' zero = refl
+lemma15' (S x) =  lemma15' x
+
+lemma15 : (x y : Int) -> mul x y  ≡ mul y x
+lemma15 zero x =  lemma15' x
+lemma15 (S x) y =  let open ≡-Reasoning in
+   begin
+      mul (S x) y
+   ≡⟨⟩
+     sum y (mul x y )
+   ≡⟨ cong ( \x -> sum y x ) (lemma15 x y ) ⟩
+     sum y (mul y x)
+   ≡⟨ sym ( lemma15'' y x ) ⟩
+     mul y (S x) 
+   ∎
+
+
+
+
+