--- a/paper/src/gears-while.agda.replaced	Mon Feb 10 17:26:24 2020 +0900
+++ b/paper/src/gears-while.agda.replaced	Tue Feb 11 02:31:26 2020 +0900
@@ -1,13 +1,13 @@
 whileTest : {l : Level} {t : Set l}  @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env)  @$\rightarrow$@
-            ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
+            ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
 whileTest {_} {_} {c10} next = next env proof2
   where
     env : Env
     env = record {vari = 0 ; varn = c10}
-    proof2 : ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10)
+    proof2 : ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10)
     proof2 = record {pi1 = refl ; pi2 = refl}    
 
-conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10)
+conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10)
                @$\rightarrow$@ (Code : (env1 : Env) @$\rightarrow$@ (varn env1 + vari env1 @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
 conversion1 env {c10} p1 next = next env proof4
    where
@@ -23,7 +23,7 @@
             c10
           @$\blacksquare$@
 
-{-# TERMINATING #-}
+{-@$\#$@ TERMINATING @$\#$@-}
 whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((varn env) + (vari env) @$\equiv$@ c10) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t
 whileLoop env proof next with  ( suc zero  @$\leq$@? (varn  env) )
 whileLoop env proof next | no p = next env