--- a/Paper/src/cbc-agda.agda.replaced	Tue Nov 02 06:58:39 2021 +0900
+++ b/Paper/src/cbc-agda.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -1,3 +1,22 @@
-plus : {l : Level} {t : Set l} @$\rightarrow$@ (x y : @$\mathbb{N}$@) @$\rightarrow$@ (next : @$\mathbb{N}$@ @$\rightarrow$@ t) @$\rightarrow$@ t
-plus x zero next = next x
-plus x (suc y) next = plus (suc x) y next
+module cbc-agda where
+
+open import Data.Nat
+open import Level renaming ( suc to succ ; zero to Zero )
+
+record Env : Set where
+  field
+    varx : @$\mathbb{N}$@
+    vary : @$\mathbb{N}$@
+open Env
+
+plus-com : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+plus-com env next exit with vary env
+... | zero  = exit (record { varx = varx env ; vary = vary env })
+... | suc y = next (record { varx = suc (varx env) ; vary = y })
+
+{-@$\#$@ TERMINATING @$\#$@-}
+plus-p : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+plus-p env exit = plus-com env ( @$\lambda$@ env @$\rightarrow$@ plus-p env exit ) exit
+
+plus : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Env
+plus x y = plus-p (record { varx = x ; vary = y }) (@$\lambda$@ env @$\rightarrow$@ env)