--- a/whileTestGears.agda	Sat Dec 15 11:57:18 2018 +0900
+++ b/whileTestGears.agda	Sat Dec 15 16:59:52 2018 +0900
@@ -2,70 +2,13 @@
 
 open import Function
 open import Data.Nat
-open import Data.Bool hiding ( _≟_ ; _∧_)
+open import Data.Bool hiding ( _≟_ )
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
 
-
-record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
-  field
-    pi1 : a
-    pi2 : b
-
-open  _∧_
-
-_-_ : ℕ -> ℕ -> ℕ 
-x - zero  = x
-zero - _  = zero
-(suc x) - (suc y)  = x - y
-
-sym1 : { y : ℕ } -> y + zero  ≡ y
-sym1 {zero} = refl
-sym1 {suc y} = cong ( λ x → suc x ) ( sym1 {y} )
-
-+-sym : { x y : ℕ } -> x + y ≡ y + x
-+-sym {zero} {zero} = refl
-+-sym {zero} {suc y} = let open ≡-Reasoning  in
-          begin
-            zero + suc y 
-          ≡⟨⟩
-            suc y
-          ≡⟨ sym sym1 ⟩
-            suc y + zero
-          ∎
-+-sym {suc x} {zero} =  let open ≡-Reasoning  in
-          begin
-            suc x + zero
-          ≡⟨ sym1  ⟩
-            suc x
-          ≡⟨⟩
-            zero + suc x
-          ∎
-+-sym {suc x} {suc y} = cong ( λ z → suc z ) (  let open ≡-Reasoning  in
-          begin
-            x + suc y
-          ≡⟨ +-sym {x} {suc y} ⟩
-            suc (y + x)
-          ≡⟨ cong ( λ z → suc z )  (+-sym {y} {x}) ⟩
-            suc (x + y)
-          ≡⟨ sym ( +-sym {y} {suc x}) ⟩
-            y + suc x
-          ∎ )
-
-minus-plus : { x y : ℕ } -> (suc x - 1) + (y + 1) ≡ suc x + y
-minus-plus {zero} {y} = +-sym {y} {1}
-minus-plus {suc x} {y} =  cong ( λ z → suc z ) (minus-plus {x} {y})
-
-lt : ℕ -> ℕ -> Bool
-lt x y with (suc x ) ≤? y
-lt x y | yes p = true
-lt x y | no ¬p = false
-
-Equal : ℕ -> ℕ -> Bool
-Equal x y with x ≟ y
-Equal x y | yes p = true
-Equal x y | no ¬p = false
+open import utilities
+open  _/\_
 
 record Env  : Set where
   field
@@ -90,12 +33,12 @@
 proof1 : whileTest (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
 proof1 = refl
 
-whileTest' : {l : Level} {t : Set l}  -> (Code : (env : Env)  -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) -> t) -> t
+whileTest' : {l : Level} {t : Set l}  -> (Code : (env : Env)  -> ((vari env) ≡ 0) /\ ((varn env) ≡ 10) -> t) -> t
 whileTest' next = next env proof2
   where
     env : Env
     env = record {vari = 0 ; varn = 10}
-    proof2 : ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
+    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ 10)
     proof2 = record {pi1 = refl ; pi2 = refl}
     
 {-# TERMINATING #-}
@@ -111,7 +54,7 @@
       proof3 (s≤s lt) | suc n = {!!}
 
 
-conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
+conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) /\ ((varn env) ≡ 10)
                -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ 10) -> t) -> t
 conversion1 env p1 next = next env proof4
    where