Binary file Paper/.DS_Store has changed

--- a/Paper/escape_agda.rb	Tue Nov 02 06:58:39 2021 +0900
+++ b/Paper/escape_agda.rb	Fri Nov 05 15:19:08 2021 +0900
@@ -28,7 +28,8 @@
   '⊥' => 'bot',
   '∀' => 'forall',
   '#' => '\#',
-  '⊤' => '\top'
+  '⊤' => '\top',
+  '\'' => '\prime'
 }
 
 code = File.read(FileName)

Binary file Paper/soto.pdf has changed

--- a/Paper/soto.tex	Tue Nov 02 06:58:39 2021 +0900
+++ b/Paper/soto.tex	Fri Nov 05 15:19:08 2021 +0900
@@ -74,21 +74,20 @@
 \end{abstract}
 
 \begin{jkeyword}
-プログラミング言語, Perl6, サーバー, Raku 
+プログラミング言語, CbC, Gears OS, Agda, 検証
 \end{jkeyword}
 
 \maketitle
 
 % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \input{tex/intro.tex} % はじめに
-\input{tex/cbc.tex} % cbcの説明
-\input{tex/agda.tex} % agdaの説明
-\input{tex/cbc_agda.tex}% cbcとagda(gearsagda)
-\input{tex/hoare.tex} % hoare logicの説明
-% while loopの実装(簡単に)
-% while loopの検証
-% red black treeの実装(こいつも簡単に)
-% red black treeの検証
+\input{tex/cbc.tex} % cbc の説明
+\input{tex/agda.tex} % agda の説明
+\input{tex/cbc_agda.tex}% cbc と agda(gearsagda)
+\input{tex/hoare.tex} % hoare logic の説明
+\input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
+% red black tree の実装(こいつも簡単に)
+% red black tree の検証
 % まとめ
 
 \nocite{*}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/And.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,4 @@
+record _@$\wedge$@_ (A B : Set) : Set where
+  field
+    p1 : A
+    p2 : B

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/Nat.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,3 @@
+data @$\mathbb{N}$@ : Set where
+  zero : @$\mathbb{N}$@
+  suc  : (n : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/_Fresh.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,211 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Fresh lists, a proof relevant variant of Catarina Coquand's contexts in
+-- "A Formalised Proof of the Soundness and Completeness of a Simply Typed
+-- Lambda-Calculus with Explicit Substitutions"
+------------------------------------------------------------------------
+
+-- See README.Data.List.Fresh and README.Data.Trie.NonDependent for
+-- examples of how to use fresh lists.
+
+{-@$\#$@ OPTIONS --without-K --safe @$\#$@-}
+
+module Data.List.Fresh where
+
+open import Level using (Level; _@$\sqcup$@_)
+open import Data.Bool.Base using (true; false)
+open import Data.Unit.Polymorphic.Base using (@$\top$@)
+open import Data.Product using (∃; _@$\times$@_; _,_; -,_; proj@$\_{1}$@; proj@$\_{2}$@)
+open import Data.List.Relation.Unary.All using (All; []; _@$\text{::}$@_)
+open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _@$\text{::}$@_)
+open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
+open import Data.Nat.Base using (@$\mathbb{N}$@; zero; suc)
+open import Function using (_∘′_; flip; id; _on_)
+open import Relation.Nullary      using (does)
+open import Relation.Unary   as U using (Pred)
+open import Relation.Binary  as B using (Rel)
+open import Relation.Nary
+
+private
+  variable
+    a b p r s : Level
+    A : Set a
+    B : Set b
+
+------------------------------------------------------------------------
+-- Basic type
+
+-- If we pick an R such that (R a b) means that a is different from b
+-- then we have a list of distinct values.
+
+module _ {a} (A : Set a) (R : Rel A r) where
+
+  data List@$\#$@ : Set (a @$\sqcup$@ r)
+  fresh : (a : A) (as : List@$\#$@) @$\rightarrow$@ Set r
+
+  data List@$\#$@ where
+    []   : List@$\#$@
+    cons : (a : A) (as : List@$\#$@) @$\rightarrow$@ fresh a as @$\rightarrow$@ List@$\#$@
+
+  -- Whenever R can be reconstructed by η-expansion (e.g. because it is
+  -- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we
+  -- do not care about the proof, it is convenient to get back list syntax.
+
+  -- We use a different symbol to avoid conflict when importing both Data.List
+  -- and Data.List.Fresh.
+  infixr 5 _@$\text{::}$@@$\#$@_
+  pattern _@$\text{::}$@@$\#$@_ x xs = cons x xs _
+
+  fresh a []        = @$\top$@
+  fresh a (x @$\text{::}$@@$\#$@ xs) = R a x @$\times$@ fresh a xs
+
+-- Convenient notation for freshness making A and R implicit parameters
+infix 5 _@$\#$@_
+_@$\#$@_ : {R : Rel A r} (a : A) (as : List@$\#$@ A R) @$\rightarrow$@ Set r
+_@$\#$@_ = fresh _ _
+
+------------------------------------------------------------------------
+-- Operations for modifying fresh lists
+
+module _ {R : Rel A r} {S : Rel B s} (f : A @$\rightarrow$@ B) (R@$\Rightarrow$@S : @$\forall$@[ R @$\Rightarrow$@ (S on f) ]) where
+
+  map   : List@$\#$@ A R @$\rightarrow$@ List@$\#$@ B S
+  map-@$\#$@ : @$\forall$@ {a} as @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ f a @$\#$@ map as
+
+  map []             = []
+  map (cons a as ps) = cons (f a) (map as) (map-@$\#$@ as ps)
+
+  map-@$\#$@ []        _        = _
+  map-@$\#$@ (a @$\text{::}$@@$\#$@ as) (p , ps) = R@$\Rightarrow$@S p , map-@$\#$@ as ps
+
+module _ {R : Rel B r} (f : A @$\rightarrow$@ B) where
+
+  map@$\_{1}$@ : List@$\#$@ A (R on f) @$\rightarrow$@ List@$\#$@ B R
+  map@$\_{1}$@ = map f id
+
+module _ {R : Rel A r} {S : Rel A s} (R@$\Rightarrow$@S : @$\forall$@[ R @$\Rightarrow$@ S ]) where
+
+  map@$\_{2}$@ : List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A S
+  map@$\_{2}$@ = map id R@$\Rightarrow$@S
+
+------------------------------------------------------------------------
+-- Views
+
+data Empty {A : Set a} {R : Rel A r} : List@$\#$@ A R @$\rightarrow$@ Set (a @$\sqcup$@ r) where
+  [] : Empty []
+
+data NonEmpty {A : Set a} {R : Rel A r} : List@$\#$@ A R @$\rightarrow$@ Set (a @$\sqcup$@ r) where
+  cons : @$\forall$@ x xs pr @$\rightarrow$@ NonEmpty (cons x xs pr)
+
+------------------------------------------------------------------------
+-- Operations for reducing fresh lists
+
+length : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ @$\mathbb{N}$@
+length []        = 0
+length (_ @$\text{::}$@@$\#$@ xs) = suc (length xs)
+
+------------------------------------------------------------------------
+-- Operations for constructing fresh lists
+
+pattern [_] a = a @$\text{::}$@@$\#$@ []
+
+fromMaybe : {R : Rel A r} @$\rightarrow$@ Maybe A @$\rightarrow$@ List@$\#$@ A R
+fromMaybe nothing  = []
+fromMaybe (just a) = [ a ]
+
+module _ {R : Rel A r} (R-refl : B.Reflexive R) where
+
+  replicate   : @$\mathbb{N}$@ @$\rightarrow$@ A @$\rightarrow$@ List@$\#$@ A R
+  replicate-@$\#$@ : (n : @$\mathbb{N}$@) (a : A) @$\rightarrow$@ a @$\#$@ replicate n a
+
+  replicate zero    a = []
+  replicate (suc n) a = cons a (replicate n a) (replicate-@$\#$@ n a)
+
+  replicate-@$\#$@ zero    a = _
+  replicate-@$\#$@ (suc n) a = R-refl , replicate-@$\#$@ n a
+
+------------------------------------------------------------------------
+-- Operations for deconstructing fresh lists
+
+uncons : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe (A @$\times$@ List@$\#$@ A R)
+uncons []        = nothing
+uncons (a @$\text{::}$@@$\#$@ as) = just (a , as)
+
+head : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe A
+head = Maybe.map proj@$\_{1}$@ ∘′ uncons
+
+tail : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe (List@$\#$@ A R)
+tail = Maybe.map proj@$\_{2}$@ ∘′ uncons
+
+take   : {R : Rel A r} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R
+take-@$\#$@ : {R : Rel A r} @$\rightarrow$@ @$\forall$@ n a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ take n as
+
+take zero    xs             = []
+take (suc n) []             = []
+take (suc n) (cons a as ps) = cons a (take n as) (take-@$\#$@ n a as ps)
+
+take-@$\#$@ zero    a xs        _        = _
+take-@$\#$@ (suc n) a []        ps       = _
+take-@$\#$@ (suc n) a (x @$\text{::}$@@$\#$@ xs) (p , ps) = p , take-@$\#$@ n a xs ps
+
+drop : {R : Rel A r} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R
+drop zero    as        = as
+drop (suc n) []        = []
+drop (suc n) (a @$\text{::}$@@$\#$@ as) = drop n as
+
+module _ {P : Pred A p} (P? : U.Decidable P) where
+
+  takeWhile   : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R
+  takeWhile-@$\#$@ : @$\forall$@ {R : Rel A r} a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ takeWhile as
+
+  takeWhile []             = []
+  takeWhile (cons a as ps) with does (P? a)
+  ... | true  = cons a (takeWhile as) (takeWhile-@$\#$@ a as ps)
+  ... | false = []
+
+  takeWhile-@$\#$@ a []        _        = _
+  takeWhile-@$\#$@ a (x @$\text{::}$@@$\#$@ xs) (p , ps) with does (P? x)
+  ... | true  = p , takeWhile-@$\#$@ a xs ps
+  ... | false = _
+
+  dropWhile : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R
+  dropWhile []            = []
+  dropWhile aas@(a @$\text{::}$@@$\#$@ as) with does (P? a)
+  ... | true  = dropWhile as
+  ... | false = aas
+
+  filter   : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R
+  filter-@$\#$@ : @$\forall$@ {R : Rel A r} a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ filter as
+
+  filter []             = []
+  filter (cons a as ps) with does (P? a)
+  ... | true  = cons a (filter as) (filter-@$\#$@ a as ps)
+  ... | false = filter as
+
+  filter-@$\#$@ a []        _        = _
+  filter-@$\#$@ a (x @$\text{::}$@@$\#$@ xs) (p , ps) with does (P? x)
+  ... | true  = p , filter-@$\#$@ a xs ps
+  ... | false = filter-@$\#$@ a xs ps
+
+------------------------------------------------------------------------
+-- Relationship to List and AllPairs
+
+toList : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ ∃ (AllPairs R)
+toAll  : @$\forall$@ {R : Rel A r} {a} as @$\rightarrow$@ fresh A R a as @$\rightarrow$@ All (R a) (proj@$\_{1}$@ (toList as))
+
+toList []             = -, []
+toList (cons x xs ps) = -, toAll xs ps @$\text{::}$@ proj@$\_{2}$@ (toList xs)
+
+toAll []        ps       = []
+toAll (a @$\text{::}$@@$\#$@ as) (p , ps) = p @$\text{::}$@ toAll as ps
+
+fromList   : @$\forall$@ {R : Rel A r} {xs} @$\rightarrow$@ AllPairs R xs @$\rightarrow$@ List@$\#$@ A R
+fromList-@$\#$@ : @$\forall$@ {R : Rel A r} {x xs} (ps : AllPairs R xs) @$\rightarrow$@
+             All (R x) xs @$\rightarrow$@ x @$\#$@ fromList ps
+
+fromList []       = []
+fromList (r @$\text{::}$@ rs) = cons _ (fromList rs) (fromList-@$\#$@ rs r)
+
+fromList-@$\#$@ []       _        = _
+fromList-@$\#$@ (p @$\text{::}$@ ps) (r @$\text{::}$@ rs) = r , fromList-@$\#$@ ps rs

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/abridgement.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,22 @@
+module abridgement where
+
+open import Data.Nat
+
+record env : Set where
+  field
+    a : @$\mathbb{N}$@
+    b : @$\mathbb{N}$@
+    c : @$\mathbb{N}$@
+open env
+
+patternmatch-default : env @$\rightarrow$@ @$\mathbb{N}$@
+patternmatch-default record { a = a ; b = b ; c = c } = c
+
+patternmatch-extraction : env @$\rightarrow$@ @$\mathbb{N}$@
+patternmatch-extraction env with c env
+patternmatch-extraction env | c = c
+
+patternmatch-extraction' : env @$\rightarrow$@ @$\mathbb{N}$@
+patternmatch-extraction' env with c env
+... | c = c
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/cbc-agda.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,22 @@
+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)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/cmp.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,15 @@
+module cmp where
+
+open import Data.Nat
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+
+compare_test : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@
+compare_test x y with <-cmp x y
+... | tri< a @$\neg$@b @$\neg$@c = y
+... | tri≈ @$\neg$@a b @$\neg$@c = x
+... | tri> @$\neg$@a @$\neg$@b c = x
+
+-- test = compare_test 7 2
+-- 7
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/fresh_test.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,14 @@
+module fresh_test where
+
+open import Data.Nat
+open import Data.List.Base
+open import Data.List.Fresh
+open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
+open import Data.Product
+open import Relation.Nary using (⌊_⌋; fromWitness)
+
+ISortedList : Set
+ISortedList = List@$\#$@ @$\mathbb{N}$@ ⌊ _>?_ ⌋
+
+ins : ISortedList
+ins = 8 @$\text{::}$@@$\#$@ 4 @$\text{::}$@@$\#$@ 2 @$\text{::}$@@$\#$@ 0 @$\text{::}$@@$\#$@ []

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/hoare-test.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,103 @@
+module hoare-test where
+
+open import Data.Nat hiding (_@$\sqcup$@_)
+open import Level renaming ( suc to succ ; zero to Zero )
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+
+open import Relation.Nullary hiding (proof)
+
+open import Data.Nat.Properties as NatProp -- <-cmp
+
+record Env : Set where
+  field
+    var-init-x : @$\mathbb{N}$@
+    var-init-y : @$\mathbb{N}$@
+    var-x : @$\mathbb{N}$@
+    var-y : @$\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 var-y env
+... | zero  = exit record env{var-x = var-x env ; var-y = zero}
+... | suc y = next record env{var-x = suc (var-x env) ; var-y = y}
+
+plus-init : {l : Level} {t : Set l} @$\rightarrow$@ ( x y : @$\mathbb{N}$@ ) @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+plus-init x y next = next (record { var-init-x = x ; var-init-y = y ; var-x = x ; var-y = 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-init x y (@$\lambda$@ env @$\rightarrow$@  plus-p env (@$\lambda$@ env @$\rightarrow$@ env))
+--(record { varx = x ; vary = y }) (@$\lambda$@ env @$\rightarrow$@ env)
+
+-- ここまでplusの定義
+
+-- mdg (meta code gear)
+data mdg-state : Set where
+  s-init  : mdg-state
+  s-doing : mdg-state
+  s-fin   : mdg-state
+
+record  _@$\wedge$@_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+-- mcg (meta code gear)
+plus-mdg : mdg-state @$\rightarrow$@ Env @$\rightarrow$@ Set
+plus-mdg s-init  env = (var-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-y env @$\equiv$@ var-init-y env)
+plus-mdg s-doing env = (var-init-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-init-y env @$\equiv$@ var-init-y env) -- よくないmdg
+plus-mdg s-fin   env = (var-init-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-init-y env @$\equiv$@ var-init-y env) -- よくないmdg
+
+-- 実行のwrapperを作って、そこでmcgが適切に選ばれて接続をしたい。多分できる気がする。
+plus-init-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (x y : @$\mathbb{N}$@) @$\rightarrow$@  ((env : Env ) @$\rightarrow$@ plus-mdg s-init env @$\rightarrow$@ t) @$\rightarrow$@ t
+plus-init-mcg x y next = next ( plus-init x y ( @$\lambda$@ env @$\rightarrow$@ env ) ) record { proj1 = refl ; proj2 = refl } where
+
+plus-com-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env ) @$\rightarrow$@ (next : (env : Env ) @$\rightarrow$@ plus-mdg s-doing env  @$\rightarrow$@ t) @$\rightarrow$@ (exit : (env : Env ) @$\rightarrow$@ plus-mdg s-fin env @$\rightarrow$@ t) @$\rightarrow$@ t
+plus-com-mcg env-in next exit with (var-y env-in)
+... | suc y = next ( plus-com env-in ( @$\lambda$@ env @$\rightarrow$@ env ) ( @$\lambda$@ env @$\rightarrow$@ env ) ) (record { proj1 = refl ; proj2 = refl }) where
+... | zero = exit env-in (record { proj1 = refl ; proj2 = refl })
+
+--plus-com-mcg
+{-@$\#$@ TERMINATING @$\#$@-}
+plus-p-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : (env : Env ) @$\rightarrow$@ plus-mdg s-fin env @$\rightarrow$@ t) @$\rightarrow$@ t
+plus-p-mcg env exit = plus-com-mcg env (@$\lambda$@ env s @$\rightarrow$@ plus-p-mcg env exit ) exit
+
+plus-mcg : (x y : @$\mathbb{N}$@) @$\rightarrow$@ Env
+plus-mcg x y = plus-init-mcg x y (@$\lambda$@ env s @$\rightarrow$@ plus-p-mcg env (@$\lambda$@ env s @$\rightarrow$@ env))
+
+test1 = plus-mcg 3 4
+
+{-
+next env ? where
+   env : Env
+   env = plus-com env-in {!!} {!!}
+-}
+--plus-mdg s-init (plus-p record env{var-x = var-init-x env ; var-y = var-init-y env} (@$\lambda$@ env @$\rightarrow$@ env))
+
+
+
+{-
+whileTestPwP  : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
+   env : Envc
+   env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env )
+-}
+
+data hoare-cond : Set where
+  p : hoare-cond
+  q : hoare-cond
+
+
+{-
+continuation-hoare-triple : {l : Level} {t : Set l} @$\rightarrow$@ hoare-cond @$\rightarrow$@ (next : Env @$\rightarrow$@ t) Set
+continuation-hoare-triple p next = continuation-hoare-triple q
+continuation-hoare-triple q next = continuation-hoare-triple p
+-}
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/hoare-while.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,98 @@
+module hoare-while where
+
+open import Data.Nat
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+
+record Envc : Set (succ Zero) where
+  field
+    c10 : @$\mathbb{N}$@
+    varn : @$\mathbb{N}$@
+    vari : @$\mathbb{N}$@
+open Envc
+
+whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+
+whileLoopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
+whileLoopP env next exit with (varn env)
+... | zero = exit env
+... | suc n = exit (record env { varn = n ; vari = (suc n) })
+
+
+{-@$\#$@ TERMINATING @$\#$@-}
+loopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
+loopP env exit = whileLoopP env (@$\lambda$@ env @$\rightarrow$@ loopP env exit ) exit
+
+whileTestPCall : (c10 :  @$\mathbb{N}$@ ) @$\rightarrow$@ Envc
+whileTestPCall c10 = whileTestP {_} {_} c10 (@$\lambda$@ env @$\rightarrow$@ loopP env (@$\lambda$@ env @$\rightarrow$@  env))
+
+---
+open import Data.Empty
+--open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)
+
+--open import Agda.Builtin.Unit
+open import utilities
+
+open import Relation.Binary.PropositionalEquality
+
+open _@$\wedge$@_
+
+data whileTestState  : Set where
+  s1 : whileTestState
+  s2 : whileTestState
+  sf : whileTestState
+
+whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@  Set
+whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env)
+whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env)
+whileTestStateP sf env = (vari env @$\equiv$@ c10 env)
+
+whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
+   env : Envc
+   env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env )
+
+whileLoopPwP : {l : Level} {t : Set l}   @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env
+    @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env  @$\rightarrow$@ t)
+    @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env  @$\rightarrow$@ t) @$\rightarrow$@ t
+whileLoopPwP env s next exit with <-cmp 0 (varn env)
+whileLoopPwP env s next exit | tri≈ @$\neg$@a b @$\neg$@c = exit env (lem (sym b) s)
+  where
+    lem : (varn env @$\equiv$@ 0) @$\rightarrow$@ (varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ vari env @$\equiv$@ c10 env
+    lem refl refl = refl
+whileLoopPwP env s next exit | tri< a @$\neg$@b @$\neg$@c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
+  where
+    1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@
+    1<0 ()
+    proof5 : (suc zero  @$\leq$@ (varn  env))  @$\rightarrow$@ ((varn env ) - 1) + (vari env + 1) @$\equiv$@ c10 env
+    proof5 (s@$\leq$@s lt) with varn  env
+    proof5 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 a)
+    proof5 (s@$\leq$@s (z@$\leq$@n {n'}) ) | suc n = let open @$\equiv$@-Reasoning in
+      begin
+        n' + (vari env + 1)
+      @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ n' + z ) ( +-sym  {vari env} {1} )  @$\rangle$@
+        n' + (1 + vari env )
+      @$\equiv$@@$\langle$@ sym ( +-assoc (n')  1 (vari env) ) @$\rangle$@
+        (n' + 1) + vari env
+      @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env )  +1@$\equiv$@suc  @$\rangle$@
+        (suc n' ) + vari env
+      @$\equiv$@@$\langle$@@$\rangle$@
+        varn env + vari env
+      @$\equiv$@@$\langle$@ s  @$\rangle$@
+         c10 env
+      @$\blacksquare$@
+
+
+whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env
+  @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env  @$\rightarrow$@ t)
+  @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env  @$\rightarrow$@ t) @$\rightarrow$@ t
+whileLoopPwP' zero env refl refl next exit = exit env refl
+whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
+
+
+
+whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) @$\rightarrow$@ @$\top$@ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c))
+whileTestPSemSound c output refl = whileTestPSem c
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/hoare-while1.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,41 @@
+module hoare-while1 where
+
+open import Level renaming (suc to Suc ; zero to Zero )
+module WhileTest  where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat hiding (compare)
+open import Data.Maybe
+open import Data.List
+open import Function
+open import logic
+
+record Env : Set (Suc Zero) where
+  field
+    varn : @$\mathbb{N}$@
+    vari : @$\mathbb{N}$@
+open Env
+
+record WhileTest {m : Level }  {t : Set m }  : Set (Suc m) where
+  field
+    env : Env
+  whileInit : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Env @$\rightarrow$@ t) @$\rightarrow$@ t
+  whileInit c10 next = next (record {varn = c10 ; vari = 0 } )
+  whileLoop : Env @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+  whileLoop env next = whileLoop1 (varn env) env where
+      whileLoop1 : @$\mathbb{N}$@ @$\rightarrow$@ Env @$\rightarrow$@ t
+      whileLoop1 zero env =  next env
+      whileLoop1 (suc t ) env = 
+          whileLoop1 t (record env {varn = t ; vari = (vari env) + 1}) 
+  whileTest : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Env @$\rightarrow$@ t) @$\rightarrow$@ t
+  whileTest c10 next = whileInit c10 $ @$\lambda$@ env @$\rightarrow$@ whileLoop env next
+
+open WhileTest
+
+createWhileTest : {m : Level} {t : Set m }  @$\rightarrow$@ WhileTest {m} {t}
+createWhileTest  = record { env = record { varn = 0; vari = 0 } }
+
+test2 : @$\mathbb{N}$@
+test2 = whileTest createWhileTest 10 $ @$\lambda$@ e @$\rightarrow$@ vari e
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/lambda.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,28 @@
+module lambda where
+
+open import Data.Nat
+
+ll+_ : (x y : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@
+ll+ zero = @$\lambda$@ y @$\rightarrow$@ y
+ll+ suc x = @$\lambda$@ y @$\rightarrow$@ (ll+ x) (suc y)
+
+test =  (ll+ 5) 7
+
+-- +1をしたのち、もう一度+1をする関数を定義する場合
+
++1 : (x : @$\mathbb{N}$@ )@$\rightarrow$@ @$\mathbb{N}$@
++1 x = suc x
+
++n : (a : @$\mathbb{N}$@) @$\rightarrow$@ (x : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@
++n a x = x a
+
+test*2 : (a : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@
+test*2 a = +n a (@$\lambda$@ z @$\rightarrow$@ z + 2)
+
+test*2' : (a : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@
+test*2' a = +n a (@$\lambda$@ z @$\rightarrow$@ +n z (@$\lambda$@ z @$\rightarrow$@ z))
+
+
+@$\lambda$@'+2 : (x : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@
+@$\lambda$@'+2 d = {!!} -- (@$\lambda$@ x @$\rightarrow$@ x +1)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/list-any.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,73 @@
+module list-any where
+
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_@$\equiv$@_; refl; sym; trans; cong)
+open Eq.@$\equiv$@-Reasoning
+open import Data.Bool using (Bool; true; false; T; _@$\wedge$@_; _∨_; not)
+open import Data.Nat using (@$\mathbb{N}$@; zero; suc; _+_; _*_; _∸_; _@$\leq$@_; s@$\leq$@s; z@$\leq$@n)
+open import Data.Nat.Properties using
+  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
+open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)
+open import Data.Product using (_@$\times$@_; ∃; ∃-syntax) renaming (_,_ to @$\langle$@_,_@$\rangle$@)
+open import Function using (_∘_)
+open import Level using (Level)
+--open import plfa.part1.Isomorphism using (_≃_; _⇔_)
+
+open import Data.List
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+
+open import rbt_t
+
+-- infix 4 _∈_ _∉_
+
+test-l : List @$\mathbb{N}$@
+test-l = 1 @$\text{::}$@ 2 @$\text{::}$@ []
+
+data Any-test {A : Set} (P : A @$\rightarrow$@ Set) : List A @$\rightarrow$@ Set where
+  here  : @$\forall$@ {x : A} {xs : List A} @$\rightarrow$@ P x @$\rightarrow$@ Any-test P (x @$\text{::}$@ xs)
+  there : @$\forall$@ {x : A} {xs : List A} @$\rightarrow$@ Any-test P xs @$\rightarrow$@ Any-test P (x @$\text{::}$@ xs)
+
+{-
+_∈_ : @$\forall$@ {A : Set} (x : A) (xs : List A) @$\rightarrow$@ Set
+x ∈ xs = Any (x @$\equiv$@_) xs
+-}
+
+_∈1_ : @$\forall$@ (n : @$\mathbb{N}$@) (xs : List @$\mathbb{N}$@) @$\rightarrow$@ Set
+n ∈1 [] = Any-test (n @$\equiv$@_) []
+n ∈1 l@(x @$\text{::}$@ xs) with <-cmp n x
+... | tri< a @$\neg$@b @$\neg$@c = Any-test (n @$\equiv$@_) xs
+... | tri≈ @$\neg$@a b @$\neg$@c = Any-test (n @$\equiv$@_) l
+... | tri> @$\neg$@a @$\neg$@b c = Any-test (n @$\equiv$@_) xs
+
+test : 1 ∈1 test-l
+test = here refl
+
+data Any (P : @$\mathbb{N}$@ @$\rightarrow$@ Set) : rbt @$\rightarrow$@ Set where
+  here  : @$\forall$@ {x : @$\mathbb{N}$@} {xs : rbt} @$\rightarrow$@ P x @$\rightarrow$@ Any P xs
+  there : @$\forall$@ {x : @$\mathbb{N}$@} {xs : rbt} @$\rightarrow$@ Any P (get-rbt xs) @$\rightarrow$@ Any P xs
+
+_∈_ : @$\forall$@ (n : @$\mathbb{N}$@) (xs : rbt) @$\rightarrow$@ Bool
+n ∈ bt-empty = false
+n ∈ bt-node node with <-cmp n (node.number (tree.key node))
+... | tri< a @$\neg$@b @$\neg$@c = n ∈ (tree.ltree node)
+... | tri≈ @$\neg$@a b @$\neg$@c = true
+... | tri> @$\neg$@a @$\neg$@b c = n ∈ (tree.rtree node)
+
+
+
+testany1 : rbt @$\rightarrow$@ Set
+testany1 bt-empty = {!!}
+testany1 (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) = {!!}
+
+testrbt1 = whileTestPCall' bt-empty 0
+testrbt2 = whileTestPCall' (Env.vart testrbt1) 1
+testrbt3 = whileTestPCall' (Env.vart testrbt2) 2
+testrbt4 = whileTestPCall' (Env.vart testrbt3) 3
+testrbt5 = whileTestPCall' (Env.vart testrbt4) 4
+testrbt6 = whileTestPCall' (Env.vart testrbt5) 5
+testrbt7 = whileTestPCall' (Env.vart testrbt6) 6
+
+
+test1kk = 100 ∈ (Env.vart testrbt6)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/logic.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,152 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary hiding(_⇔_)
+open import Data.Empty
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _@$\wedge$@_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where
+   case1 : A @$\rightarrow$@ A ∨ B
+   case2 : B @$\rightarrow$@ A ∨ B
+
+_⇔_ : {n m : Level } @$\rightarrow$@ ( A : Set n ) ( B : Set m )  @$\rightarrow$@ Set (n @$\sqcup$@ m)
+_⇔_ A B =  ( A @$\rightarrow$@ B ) @$\wedge$@ ( B @$\rightarrow$@ A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} @$\rightarrow$@ (A @$\rightarrow$@ B) @$\rightarrow$@ @$\neg$@ B @$\rightarrow$@ @$\neg$@ A
+contra-position {n} {m} {A} {B}  f @$\neg$@b a = @$\neg$@b ( f a )
+
+double-neg : {n  : Level } {A : Set n} @$\rightarrow$@ A @$\rightarrow$@ @$\neg$@ @$\neg$@ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} @$\rightarrow$@ @$\neg$@ @$\neg$@ @$\neg$@ A @$\rightarrow$@ @$\neg$@ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} @$\rightarrow$@  A @$\wedge$@ B  @$\rightarrow$@ @$\neg$@ ( (@$\neg$@ A ) ∨ (@$\neg$@ B ) )
+de-morgan {n} {A} {B} and (case1 @$\neg$@A) = @$\bot$@-elim ( @$\neg$@A ( _@$\wedge$@_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 @$\neg$@B) = @$\bot$@-elim ( @$\neg$@B ( _@$\wedge$@_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } @$\rightarrow$@  A ∨ B @$\rightarrow$@ @$\neg$@ A @$\rightarrow$@ B
+dont-or {A} {B} (case1 a) @$\neg$@A = @$\bot$@-elim ( @$\neg$@A a )
+dont-or {A} {B} (case2 b) @$\neg$@A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } @$\rightarrow$@  A ∨ B @$\rightarrow$@ @$\neg$@ B @$\rightarrow$@ A
+dont-orb {A} {B} (case2 b) @$\neg$@B = @$\bot$@-elim ( @$\neg$@B b )
+dont-orb {A} {B} (case1 a) @$\neg$@B = a
+
+
+
+infixr  130 _@$\wedge$@_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_@$\wedge$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool 
+true @$\wedge$@ true = true
+_ @$\wedge$@ _ = false
+
+_\/_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool @$\rightarrow$@ Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _@$\wedge$@_
+
+open import Relation.Binary.PropositionalEquality
+
+
+@$\equiv$@-Bool-func : {A B : Bool } @$\rightarrow$@ ( A @$\equiv$@ true @$\rightarrow$@ B @$\equiv$@ true ) @$\rightarrow$@ ( B @$\equiv$@ true @$\rightarrow$@ A @$\equiv$@ true ) @$\rightarrow$@ A @$\equiv$@ B
+@$\equiv$@-Bool-func {true} {true} a@$\rightarrow$@b b@$\rightarrow$@a = refl
+@$\equiv$@-Bool-func {false} {true} a@$\rightarrow$@b b@$\rightarrow$@a with b@$\rightarrow$@a refl
+... | ()
+@$\equiv$@-Bool-func {true} {false} a@$\rightarrow$@b b@$\rightarrow$@a with a@$\rightarrow$@b refl
+... | ()
+@$\equiv$@-Bool-func {false} {false} a@$\rightarrow$@b b@$\rightarrow$@a = refl
+
+bool-@$\equiv$@-? : (a b : Bool) @$\rightarrow$@ Dec ( a @$\equiv$@ b )
+bool-@$\equiv$@-? true true = yes refl
+bool-@$\equiv$@-? true false = no (@$\lambda$@ ())
+bool-@$\equiv$@-? false true = no (@$\lambda$@ ())
+bool-@$\equiv$@-? false false = yes refl
+
+@$\neg$@-bool-t : {a : Bool} @$\rightarrow$@  @$\neg$@ ( a @$\equiv$@ true ) @$\rightarrow$@ a @$\equiv$@ false
+@$\neg$@-bool-t {true} ne = @$\bot$@-elim ( ne refl )
+@$\neg$@-bool-t {false} ne = refl
+
+@$\neg$@-bool-f : {a : Bool} @$\rightarrow$@  @$\neg$@ ( a @$\equiv$@ false ) @$\rightarrow$@ a @$\equiv$@ true
+@$\neg$@-bool-f {true} ne = refl
+@$\neg$@-bool-f {false} ne = @$\bot$@-elim ( ne refl )
+
+@$\neg$@-bool : {a : Bool} @$\rightarrow$@  a @$\equiv$@ false  @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ @$\bot$@
+@$\neg$@-bool refl ()
+
+lemma-@$\wedge$@-0 : {a b : Bool} @$\rightarrow$@ a @$\wedge$@ b @$\equiv$@ true @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ @$\bot$@
+lemma-@$\wedge$@-0 {true} {true} refl ()
+lemma-@$\wedge$@-0 {true} {false} ()
+lemma-@$\wedge$@-0 {false} {true} ()
+lemma-@$\wedge$@-0 {false} {false} ()
+
+lemma-@$\wedge$@-1 : {a b : Bool} @$\rightarrow$@ a @$\wedge$@ b @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ @$\bot$@
+lemma-@$\wedge$@-1 {true} {true} refl ()
+lemma-@$\wedge$@-1 {true} {false} ()
+lemma-@$\wedge$@-1 {false} {true} ()
+lemma-@$\wedge$@-1 {false} {false} ()
+
+bool-and-tt : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ true @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true
+bool-and-tt refl refl = refl
+
+bool-@$\wedge$@@$\rightarrow$@tt-0 : {a b : Bool} @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true @$\rightarrow$@ a @$\equiv$@ true 
+bool-@$\wedge$@@$\rightarrow$@tt-0 {true} {true} refl = refl
+bool-@$\wedge$@@$\rightarrow$@tt-0 {false} {_} ()
+
+bool-@$\wedge$@@$\rightarrow$@tt-1 : {a b : Bool} @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ true 
+bool-@$\wedge$@@$\rightarrow$@tt-1 {true} {true} refl = refl
+bool-@$\wedge$@@$\rightarrow$@tt-1 {true} {false} ()
+bool-@$\wedge$@@$\rightarrow$@tt-1 {false} {false} ()
+
+bool-or-1 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ ( a \/ b ) @$\equiv$@ b 
+bool-or-1 {false} {true} refl = refl
+bool-or-1 {false} {false} refl = refl
+bool-or-2 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ (a \/ b ) @$\equiv$@ a 
+bool-or-2 {true} {false} refl = refl
+bool-or-2 {false} {false} refl = refl
+
+bool-or-3 : {a : Bool} @$\rightarrow$@ ( a \/ true ) @$\equiv$@ true 
+bool-or-3 {true} = refl
+bool-or-3 {false} = refl
+
+bool-or-31 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ true  @$\rightarrow$@ ( a \/ b ) @$\equiv$@ true 
+bool-or-31 {true} {true} refl = refl
+bool-or-31 {false} {true} refl = refl
+
+bool-or-4 : {a : Bool} @$\rightarrow$@ ( true \/ a ) @$\equiv$@ true 
+bool-or-4 {true} = refl
+bool-or-4 {false} = refl
+
+bool-or-41 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ true  @$\rightarrow$@ ( a \/ b ) @$\equiv$@ true 
+bool-or-41 {true} {b} refl = refl
+
+bool-and-1 : {a b : Bool} @$\rightarrow$@  a @$\equiv$@ false @$\rightarrow$@ (a @$\wedge$@ b ) @$\equiv$@ false
+bool-and-1 {false} {b} refl = refl
+bool-and-2 : {a b : Bool} @$\rightarrow$@  b @$\equiv$@ false @$\rightarrow$@ (a @$\wedge$@ b ) @$\equiv$@ false
+bool-and-2 {true} {false} refl = refl
+bool-and-2 {false} {false} refl = refl
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/plus.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,6 @@
+plus : (x y : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@
+plus x zero  = x
+plus x (suc y) = plus (suc x) y
+
+-- plus 10 20
+-- 30

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/plus2.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,10 @@
+module plus2 where
+
+open import Data.Nat hiding (_+_)
+
+_+_ : (x y : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@
+x + zero = x
+x + suc y = (suc x) + y
+
+-- 10 + 20
+-- 30

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/rbt_imple.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,140 @@
+module rbt_imple where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Binary
+open import Data.Nat hiding (_@$\leq$@_  ; _@$\leq$@?_)
+open import Data.List hiding ([_])
+open import Data.Product
+open import Data.Nat.Properties as NP
+
+open import rbt_t
+
+--このmutalの部分は別場所に書いてimportしたい。その方が綺麗に検証できそう
+mutual
+  data  right-List : Set where
+    [] : right-List
+    [_] : @$\mathbb{N}$@ @$\rightarrow$@ right-List
+    _@$\text{::}$@>_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : right-List ) @$\rightarrow$@ (p : x Data.Nat.> top-r xs) @$\rightarrow$@ right-List
+
+  top-r : right-List @$\rightarrow$@ @$\mathbb{N}$@
+  top-r [] = {!!}
+  top-r [ x ] = x
+  top-r (x @$\text{::}$@> l Cond x@$\_{1}$@) = x
+
+  insert-r : @$\mathbb{N}$@ @$\rightarrow$@ right-List @$\rightarrow$@ right-List
+  insert-r x l with l
+  ... | [] = {!!}
+  ... | [ y ] = ?
+  ... | y @$\text{::}$@> ys Cond p with <-cmp x y
+  ... | tri< a @$\neg$@b @$\neg$@c = l
+  ... | tri≈ @$\neg$@a b @$\neg$@c = l
+  ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@> l Cond c
+
+  data  left-List : Set where
+    [] : left-List
+    [_] : @$\mathbb{N}$@ @$\rightarrow$@ left-List
+    _<@$\text{::}$@_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : left-List ) @$\rightarrow$@ (p : x Data.Nat.< top-l xs) @$\rightarrow$@ left-List
+
+  top-l : left-List @$\rightarrow$@ @$\mathbb{N}$@
+  top-l [] = {!!}
+  top-l [ x ] = x
+  top-l (x <@$\text{::}$@ l Cond x@$\_{1}$@) = x
+
+  insert-l : @$\mathbb{N}$@ @$\rightarrow$@ left-List @$\rightarrow$@ left-List
+  insert-l x [] = [ x ]
+  insert-l x l@([ y ]) with <-cmp x y
+  ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a
+  ... | tri≈ @$\neg$@a b @$\neg$@c = l
+  ... | tri> @$\neg$@a @$\neg$@b c = l
+  insert-l x l@(y <@$\text{::}$@ ys Cond p) with <-cmp x y
+  ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a
+  ... | tri≈ @$\neg$@a b @$\neg$@c = l
+  ... | tri> @$\neg$@a @$\neg$@b c = l
+
+
+record meta : Set where
+  field
+    deeps : @$\mathbb{N}$@
+    black-nodes : @$\mathbb{N}$@
+    l-list : left-List
+    r-list : right-List
+open meta
+
+record tree-meta (A B C D : Set) : Set where
+  field
+    key : A
+    meta-data : B
+    ltree : C
+    rtree : D
+open tree
+
+{-
+
+data rbt-meta : Set where
+  bt-empty : rbt-meta
+  bt-node  : (node : tree-meta (node col @$\mathbb{N}$@ ) meta rbt-meta rbt-meta ) @$\rightarrow$@ rbt-meta
+
+test'1 = whileTestPCall' bt-empty 0
+test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1
+test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2
+test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3
+test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4
+test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5
+test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6
+test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7
+test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8
+test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9
+test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10
+test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11
+test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12
+test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13
+test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14
+
+testdata = rbt_t.Env.vart test'7
+
+-- ここからmetaの作成
+
+makemeta-comm : rbt_t.rbt @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ meta @$\rightarrow$@ rbt-meta
+
+--make meta black nodes
+makemeta-black-nodes :  rbt_t.rbt @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ meta @$\rightarrow$@ rbt-meta
+makemeta-black-nodes = {!!}
+
+-- make meta deeps
+set-black-nodes : rbt_t.rbt @$\rightarrow$@ meta @$\rightarrow$@ @$\mathbb{N}$@
+set-black-nodes rbt fls with rbt
+... | bt-empty = (suc (black-nodes fls) )
+... | bt-node node with (node.coler (key node))
+... | black = (suc (black-nodes fls) )
+... | red = (black-nodes fls)
+
+--make meta list
+makemeta-comm rbt num fls with rbt
+... | bt-empty = bt-empty
+... | bt-node node = bt-node ( record { key = key node
+  ; meta-data = ( record {deeps = (deeps fls)
+    ; black-nodes = set-black-nodes rbt fls
+    ; l-list = insert-l (node.number (key node)) (l-list fls)
+    ; r-list = insert-r (node.number (key node))  (r-list fls) } )
+  ; ltree = makemeta-comm (ltree node) (node.number (key node)) ( record { deeps = (suc (deeps fls))
+    ; black-nodes = set-black-nodes rbt fls
+    ; l-list = insert-l (node.number (key node)) (l-list fls)
+    ; r-list = (r-list fls) } )
+  ; rtree = makemeta-comm (rtree node) (node.number (key node)) ( record { deeps = (suc (deeps fls))
+    ; black-nodes = set-black-nodes rbt fls
+    ; l-list = (l-list fls)
+    ; r-list = insert-r (node.number (key node)) (r-list fls) } ) })
+
+-- init
+makemeta : rbt @$\rightarrow$@ rbt-meta
+makemeta rbt with rbt
+... | bt-empty = bt-empty
+... | bt-node node = bt-node ( record { key = key node
+  ; meta-data =  ( record { deeps = 0 ; black-nodes = 1; l-list = [] ; r-list = [] } )
+  ; ltree = makemeta-comm (ltree node) (node.number (key node))
+    ( record { deeps = 1 ; black-nodes = 1 ; l-list = insert-l (node.number (key node)) [] ; r-list = [] } )
+  ; rtree = makemeta-comm (rtree node) (node.number (key node))
+    ( record { deeps = 1 ; black-nodes = 1 ; l-list = [] ; r-list = insert-r (node.number (key node)) [] } ) })
+
+---test11 = makemeta (rbt_t.Env.vart test'11)
+-}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/rbt_t.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,283 @@
+module rbt_t where
+
+open import Data.Nat hiding (compare)
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+open import Data.List
+
+-- @$\rightarrow$@ t を適用するために必要だった
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Level
+
+
+data col : Set where
+  black : col
+  red : col
+
+record node (A B : Set) : Set where
+  field
+    coler : A
+    number : B
+open node
+
+record tree (A B C : Set) : Set where
+  field
+    key : A
+    ltree : B
+    rtree : C
+open tree
+
+data rbt : Set where
+  bt-empty : rbt
+  bt-node  : (node : tree (node col @$\mathbb{N}$@) rbt rbt ) @$\rightarrow$@ rbt
+
+record Env : Set (succ Zero) where
+  field
+    vart : rbt
+    varn : @$\mathbb{N}$@
+    varl : List rbt
+open Env
+
+
+whileTest-next : {l : Level} {t : Set l}  @$\rightarrow$@ (c10 : rbt) @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (list : List rbt) @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTest-next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} )
+
+merge-tree :  {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+
+-- 全てmerge-treeへ
+split : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+split node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+split node@record { vart = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit node
+split node@record { vart = (bt-node record { key = key ; ltree = (bt-node node@$\_{1}$@) ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
+split record { vart = (bt-node record { key = record { coler = coler@$\_{1}$@ ; number = number@$\_{1}$@ }
+  ; ltree = (bt-node record { key = record { coler = ly ; number = ln } ; ltree = ll ; rtree = lr })
+  ; rtree = (bt-node record { key = record { coler = ry ; number = rn } ; ltree = rl ; rtree = rr }) })
+  ; varn = varn ; varl = varl } next exit
+  = next record { vart = (bt-node record { key = record { coler = red ; number = number@$\_{1}$@ }
+    ; ltree = (bt-node record { key = record { coler = black ; number = ln } ; ltree = ll ; rtree = lr })
+    ; rtree = (bt-node record { key = record { coler = black ; number = rn } ; ltree = rl ; rtree = rr }) })
+    ; varn = varn ; varl = varl }
+
+
+-- 右回転
+-- 実行時splitへ、それ以外はmerge-treeへ
+merge-rotate-right : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate-right record { vart = bt-node record { key = record { coler = y ; number = x }
+  ; ltree = (bt-node record { key =  record { coler = ly ; number = lx } ; ltree = ll ; rtree = lr })
+  ; rtree = r }
+  ; varn = varn ; varl = varl } next exit
+    = next record { vart = bt-node record { key = record { coler = y ; number = lx }
+      ; ltree = ll
+      ; rtree = (bt-node record { key = record { coler = red ; number = x } ; ltree = lr; rtree = r }) }
+      ; varn = varn ; varl = varl }
+
+
+-- split
+split-branch : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+split-branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key@$\_{1}$@ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key@$\_{1}$@ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node@$\_{1}$@) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key@$\_{1}$@ ; ltree = (bt-node record { key = record { coler = red ; number = number@$\_{1}$@ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree@$\_{1}$@ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key@$\_{1}$@
+  ; ltree = (bt-node record { key = record { coler = red ; number = number@$\_{1}$@ }
+    ; ltree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree@$\_{1}$@ })
+    ; rtree = lr })
+  ; rtree = rtree }
+  ; varn = varn ; varl = varl } next exit
+  = next node
+
+
+-- 左回転、exitはsplit_branchへ　nextもsplit_branchへ
+merge-rotate-left : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl }  next exit = exit node
+merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate-left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit
+  = next record { vart = bt-node record { key = record { coler = y ; number = rx }
+  　　; ltree = (bt-node record { key = record { coler = red ; number = x } ; ltree = l ; rtree = rl })
+  　　; rtree = rr}
+  　　; varn = varn ; varl = varl }
+
+
+-- skew exitがsplitへ　nextが左回転
+skew-bt : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+skew-bt node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit =  exit node
+skew-bt node@record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
+skew-bt node@record { vart = (bt-node record { key = key@$\_{1}$@
+  ; ltree = ltree@$\_{1}$@
+  ; rtree = (bt-node record { key = record { coler = black ; number = number }
+  ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit
+    = exit node
+skew-bt node@record { vart = (bt-node record { key = key@$\_{1}$@
+  ; ltree = ltree@$\_{1}$@
+  ; rtree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree }) })
+  ; varn = varn ; varl = varl } next exit
+    = next node
+
+
+set-node-coler : Env @$\rightarrow$@ Env
+set-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node
+set-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+  = record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+
+init-node-coler : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+init-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit
+  = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+
+--修正前
+merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node
+merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty @$\text{::}$@ varl@$\_{1}$@) } next exit = exit node
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } @$\text{::}$@ varl@$\_{1}$@) } next exit with <-cmp varn number
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } @$\text{::}$@ varl@$\_{1}$@) } next exit | tri≈ @$\neg$@a b @$\neg$@c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl@$\_{1}$@ }
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } @$\text{::}$@ varl@$\_{1}$@) } next exit | tri> @$\neg$@a @$\neg$@b c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = vart }) ; varn = number ; varl = varl@$\_{1}$@ }
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } @$\text{::}$@ varl@$\_{1}$@) } next exit | tri< a @$\neg$@b @$\neg$@c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl@$\_{1}$@ }
+
+-- do marge-tree
+-- next merge-tree-c
+-- exit fin
+merge-tree-c :  {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+merge-tree-c env next exit with varl env
+... | [] = exit env
+... | bt-empty @$\text{::}$@ nl = exit env
+... | bt-node xtree @$\text{::}$@ varl with <-cmp (varn env) (number ( key xtree ))
+... | tri≈ @$\neg$@a b @$\neg$@c = next (record env { vart = bt-node xtree ; varn = number (key xtree) ; varl = varl })
+... | tri> @$\neg$@a @$\neg$@b c = next (record env { vart = (bt-node record xtree{rtree = Env.vart env}) ; varn = number (key xtree) ; varl = varl })
+... | tri< a @$\neg$@b @$\neg$@c = next (record env { vart = (bt-node record xtree{ltree = Env.vart env}) ; varn = number (key xtree) ; varl = varl })
+
+-- do brandh
+-- next insert-c
+-- exit merge-tree
+insert-c : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+insert-c env next exit with Env.vart env
+... | bt-empty = exit record env{vart = (bt-node (record { key = record { coler = red ; number = Env.varn env }; ltree = bt-empty; rtree = bt-empty }))}
+... | bt-node node with <-cmp (Env.varn env) (node.number (tree.key node))
+... | tri≈ @$\neg$@a b @$\neg$@c = exit env
+... | tri> @$\neg$@a @$\neg$@b c = next record env{vart = (tree.ltree node) ; varl = (bt-node record node{ltree = bt-empty}) @$\text{::}$@ (Env.varl env) }
+... | tri< a @$\neg$@b @$\neg$@c = next record env{vart = (tree.rtree node) ; varl = (bt-node record node{rtree = bt-empty}) @$\text{::}$@ (Env.varl env) }
+
+-- insert
+bt-insert : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+-- mergeへ遷移する
+bt-insert (record { vart = bt-empty ; varn = varn ; varl = varl }) next exit
+  = exit (record { vart = (bt-node (record { key = record { coler = red ; number = varn }; ltree = bt-empty; rtree = bt-empty })) ; varn = varn ; varl = varl })
+
+-- 場合分けを行う
+bt-insert record {vart = (bt-node record { key = record { coler = y; number = x } ; ltree = ltree ; rtree = rtree }) ; varn = n ; varl = varl } next exit with <-cmp x n
+bt-insert node@(record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } ) next exit | tri≈ @$\neg$@a b @$\neg$@c
+  = exit node
+
+bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri> @$\neg$@a @$\neg$@b c
+  = next (record {vart = ltree ; varn = varn ; varl = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) @$\text{::}$@ varl })
+
+bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a @$\neg$@b @$\neg$@c
+  = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) @$\text{::}$@ varl })
+
+-- normal loop without termination
+{-@$\#$@ TERMINATING @$\#$@-}
+insert : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+insert env exit = bt-insert env (@$\lambda$@ env @$\rightarrow$@ insert env exit ) exit
+
+init-col : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+init-col env exit = init-node-coler env exit exit
+
+{-
+{-@$\#$@ TERMINATING @$\#$@-}
+merge : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+
+{-@$\#$@ TERMINATING @$\#$@-}
+split-p : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+split-p env exit = split env (@$\lambda$@ env @$\rightarrow$@ merge env (@$\lambda$@ env @$\rightarrow$@ merge env exit ) ) exit
+
+{-@$\#$@ TERMINATING @$\#$@-}
+rotate_right : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+rotate_right env exit = merge-rotate-right env (@$\lambda$@ env @$\rightarrow$@ split-p env (@$\lambda$@ env @$\rightarrow$@ merge env exit ) ) exit
+
+{-@$\#$@ TERMINATING @$\#$@-}
+split-b : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+split-b env exit = split-branch env (@$\lambda$@ env @$\rightarrow$@ rotate_right env exit ) @$\lambda$@ env @$\rightarrow$@ merge env exit
+
+{-@$\#$@ TERMINATING @$\#$@-}
+rotate_left : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+rotate_left env exit = merge-rotate-left env (@$\lambda$@ env @$\rightarrow$@ split-b env exit ) exit
+
+{-@$\#$@ TERMINATING @$\#$@-}
+skew : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+skew env exit = skew-bt env (@$\lambda$@ env @$\rightarrow$@ rotate_left env (@$\lambda$@ env @$\rightarrow$@ split-b env exit ) ) exit
+
+merge env exit = merge-tree env (@$\lambda$@ env @$\rightarrow$@ skew env exit ) exit
+-}
+-- skewはnextがrotate-right。exitはsplitとなる
+-- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する
+-- それはskewのexitと等しいので同時に記述してやる。
+skew' : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+skew' env exit = skew-bt env (@$\lambda$@ env @$\rightarrow$@ merge-rotate-left env exit exit ) exit
+
+split' : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+split' env exit = split-branch env (@$\lambda$@ env @$\rightarrow$@ merge-rotate-right env (@$\lambda$@ env @$\rightarrow$@ split env exit exit ) (@$\lambda$@ env @$\rightarrow$@ split env exit exit ) ) exit
+
+
+{-
+merge' : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node
+merge' node@record { vart = vart ; varn = varn ; varl = (x @$\text{::}$@ varl@$\_{1}$@) } exit = merge' (merge-tree node (@$\lambda$@ env @$\rightarrow$@ skew' env (@$\lambda$@ env @$\rightarrow$@ split' env (@$\lambda$@ env @$\rightarrow$@ env) ) ) (@$\lambda$@ env @$\rightarrow$@ env) ) exit
+-}
+
+whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (tree : rbt) @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } )
+
+
+
+{-@$\#$@ TERMINATING @$\#$@-}
+mergeP : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+mergeP env exit = merge-tree env (@$\lambda$@ env @$\rightarrow$@ skew' env (@$\lambda$@ env @$\rightarrow$@ split' env (@$\lambda$@ env @$\rightarrow$@ mergeP env exit)) ) exit
+
+{-
+mergeP1 : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!}
+mergeP1 record { vart = vart ; varn = varn ; varl = (x @$\text{::}$@ varl@$\_{1}$@) } exit = {!!}
+-}
+
+{-
+merge-tree env
+  (@$\lambda$@ env @$\rightarrow$@ skew-bt env
+    (@$\lambda$@ env @$\rightarrow$@ merge-rotate-left env
+      (@$\lambda$@ env @$\rightarrow$@ split-branch env
+        (@$\lambda$@ env @$\rightarrow$@  merge-rotate-right env
+          (@$\lambda$@ env @$\rightarrow$@ split env (@$\lambda$@ env @$\rightarrow$@ mergeP env exit ) (@$\lambda$@ env @$\rightarrow$@ mergeP env exit ) ) exit)
+      (@$\lambda$@ env @$\rightarrow$@ mergeP env exit ) )
+    exit )
+  exit ) exit
+-}
+
+--whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (c11 : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
+--whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+
+--whileTestPCall : (tree : rbt) @$\rightarrow$@ (n : @$\mathbb{N}$@)  @$\rightarrow$@ Env
+--whileTestPCall tree n = whileTestP {_} {_} tree n (@$\lambda$@ env @$\rightarrow$@ insert env (@$\lambda$@ env @$\rightarrow$@ merge env (@$\lambda$@ env @$\rightarrow$@ init-col env (@$\lambda$@ env @$\rightarrow$@ env ) ) ) )
+
+whileTestPCall' : (tree : rbt) @$\rightarrow$@ (n : @$\mathbb{N}$@)  @$\rightarrow$@ Env
+whileTestPCall' tree n = whileTestP {_} {_} tree n (@$\lambda$@ env @$\rightarrow$@ insert env (@$\lambda$@ env @$\rightarrow$@ mergeP env (@$\lambda$@ env @$\rightarrow$@ init-col env (@$\lambda$@ env @$\rightarrow$@ env ) ) ) )
+
+-- 以下test部分
+test1 = whileTestPCall' bt-empty 8
+test2 = whileTestPCall' (vart test1) 10
+test3 = whileTestPCall' (vart test2) 24
+test4 = whileTestPCall' (vart test3) 31
+test5 = whileTestPCall' (vart test4) 41
+test6 = whileTestPCall' (vart test5) 45
+test7 = whileTestPCall' (vart test6) 50
+test8 = whileTestPCall' (vart test7) 59
+test9 = whileTestPCall' (vart test8) 73
+test10 = whileTestPCall' (vart test9) 74
+test11 = whileTestPCall' (vart test10) 79
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/rbt_varif.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,54 @@
+module rbt_varif where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Binary
+open import Data.Nat hiding (_@$\leq$@_  ; _@$\leq$@?_)
+open import Data.List hiding ([_])
+open import Data.Product
+open import Data.Nat.Properties as NP
+
+
+
+mutual
+  data  right-List : Set where
+    [] : right-List
+    [_] : @$\mathbb{N}$@ @$\rightarrow$@ right-List
+    _@$\text{::}$@>_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : right-List ) @$\rightarrow$@ (p : x Data.Nat.> top-r xs) @$\rightarrow$@ right-List
+
+  top-r : right-List @$\rightarrow$@ @$\mathbb{N}$@
+  top-r [] = {!!}
+  top-r [ x ] = x
+  top-r (x @$\text{::}$@> l Cond x@$\_{1}$@) = x
+
+  insert-r : @$\mathbb{N}$@ @$\rightarrow$@ right-List @$\rightarrow$@ right-List
+  insert-r x [] = {!!}
+  insert-r x [ y ] with <-cmp x y
+  ... | tri< a @$\neg$@b @$\neg$@c = [ y ]
+  ... | tri≈ @$\neg$@a b @$\neg$@c = [ y ]
+  ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@>  [ y ] Cond c
+  insert-r x (y @$\text{::}$@> ys Cond p) with <-cmp x y
+  ... | tri< a @$\neg$@b @$\neg$@c = (y @$\text{::}$@> ys Cond p)
+  ... | tri≈ @$\neg$@a b @$\neg$@c = (y @$\text{::}$@> ys Cond p)
+  ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@> (y @$\text{::}$@> ys Cond p) Cond c
+
+  data  left-List : Set where
+    [] : left-List
+    [_] : @$\mathbb{N}$@ @$\rightarrow$@ left-List
+    _<@$\text{::}$@_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : left-List ) @$\rightarrow$@ (p : x Data.Nat.< top-l xs) @$\rightarrow$@ left-List
+
+  top-l : left-List @$\rightarrow$@ @$\mathbb{N}$@
+  top-l [] = {!!}
+  top-l [ x ] = x
+  top-l (x <@$\text{::}$@ l Cond x@$\_{1}$@) = x
+
+  insert-l : @$\mathbb{N}$@ @$\rightarrow$@ left-List @$\rightarrow$@ left-List
+  insert-l x [] = [ x ]
+  insert-l x l@([ y ]) with <-cmp x y
+  ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a
+  ... | tri≈ @$\neg$@a b @$\neg$@c = l
+  ... | tri> @$\neg$@a @$\neg$@b c = l
+  insert-l x l@(y <@$\text{::}$@ ys Cond p) with <-cmp x y
+  ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a
+  ... | tri≈ @$\neg$@a b @$\neg$@c = l
+
+  ... | tri> @$\neg$@a @$\neg$@b c = l

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/syllogism.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,2 @@
+syllogism : {A B C : Set} @$\rightarrow$@ ((A @$\rightarrow$@ B) @$\wedge$@ (B @$\rightarrow$@ C)) @$\rightarrow$@ (A @$\rightarrow$@ C)
+syllogism x a = _@$\wedge$@_.p2 x (_@$\wedge$@_.p1 x a)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/utilities.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,171 @@
+{-@$\#$@ OPTIONS --allow-unsolved-metas @$\#$@-}
+module utilities where
+
+open import Function
+open import Data.Nat
+open import Data.Product
+open import Data.Bool hiding ( _≟_  ; _@$\leq$@?_)
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+
+Pred : Set @$\rightarrow$@ Set@$\_{1}$@
+Pred X = X @$\rightarrow$@ Set
+
+Imply : Set @$\rightarrow$@ Set @$\rightarrow$@ Set
+Imply X Y = X @$\rightarrow$@ Y
+
+Iff : Set @$\rightarrow$@ Set @$\rightarrow$@ Set
+Iff X Y = Imply X Y @$\times$@ Imply Y X
+
+record _@$\wedge$@_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+
+open  _@$\wedge$@_
+
+_-_ : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ 
+x - zero  = x
+zero - _  = zero
+(suc x) - (suc y)  = x - y
+
++zero : { y : @$\mathbb{N}$@ } @$\rightarrow$@ y + zero  @$\equiv$@ y
++zero {zero} = refl
++zero {suc y} = cong ( @$\lambda$@ x @$\rightarrow$@ suc x ) ( +zero {y} )
+
+
++-sym : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ x + y @$\equiv$@ y + x
++-sym {zero} {zero} = refl
++-sym {zero} {suc y} = let open @$\equiv$@-Reasoning  in
+          begin
+            zero + suc y 
+          @$\equiv$@@$\langle$@@$\rangle$@
+            suc y
+          @$\equiv$@@$\langle$@ sym +zero @$\rangle$@
+            suc y + zero
+          @$\blacksquare$@
++-sym {suc x} {zero} =  let open @$\equiv$@-Reasoning  in
+          begin
+            suc x + zero
+          @$\equiv$@@$\langle$@ +zero  @$\rangle$@
+            suc x
+          @$\equiv$@@$\langle$@@$\rangle$@
+            zero + suc x
+          @$\blacksquare$@
++-sym {suc x} {suc y} = cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) (  let open @$\equiv$@-Reasoning  in
+          begin
+            x + suc y
+          @$\equiv$@@$\langle$@ +-sym {x} {suc y} @$\rangle$@
+            suc (y + x)
+          @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ suc z )  (+-sym {y} {x}) @$\rangle$@
+            suc (x + y)
+          @$\equiv$@@$\langle$@ sym ( +-sym {y} {suc x}) @$\rangle$@
+            y + suc x
+          @$\blacksquare$@ )
+
+
+minus-plus : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ (suc x - 1) + (y + 1) @$\equiv$@ suc x + y
+minus-plus {zero} {y} = +-sym {y} {1}
+minus-plus {suc x} {y} =  cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) (minus-plus {x} {y})
+
++1@$\equiv$@suc : { x : @$\mathbb{N}$@ } @$\rightarrow$@ x + 1 @$\equiv$@ suc x
++1@$\equiv$@suc {zero} = refl
++1@$\equiv$@suc {suc x} = cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) ( +1@$\equiv$@suc {x} )
+
+lt : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool
+lt x y with (suc x ) @$\leq$@? y
+lt x y | yes p = true
+lt x y | no @$\neg$@p = false
+
+pred@$\mathbb{N}$@ : {n :  @$\mathbb{N}$@ } @$\rightarrow$@ lt 0 n @$\equiv$@ true  @$\rightarrow$@  @$\mathbb{N}$@
+pred@$\mathbb{N}$@ {zero} ()
+pred@$\mathbb{N}$@ {suc n} refl = n
+
+pred@$\mathbb{N}$@+1=n : {n :  @$\mathbb{N}$@ } @$\rightarrow$@ (less : lt 0 n @$\equiv$@ true ) @$\rightarrow$@ (pred@$\mathbb{N}$@ less) + 1 @$\equiv$@ n
+pred@$\mathbb{N}$@+1=n {zero} ()
+pred@$\mathbb{N}$@+1=n {suc n} refl = +1@$\equiv$@suc
+
+suc-pred@$\mathbb{N}$@=n : {n :  @$\mathbb{N}$@ } @$\rightarrow$@ (less : lt 0 n @$\equiv$@ true ) @$\rightarrow$@ suc (pred@$\mathbb{N}$@ less) @$\equiv$@ n
+suc-pred@$\mathbb{N}$@=n {zero} ()
+suc-pred@$\mathbb{N}$@=n {suc n} refl = refl
+
+Equal : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool
+Equal x y with x ≟ y
+Equal x y | yes p = true
+Equal x y | no @$\neg$@p = false
+
+_@$\Rightarrow$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool
+false  @$\Rightarrow$@  _ = true
+true  @$\Rightarrow$@  true = true
+true  @$\Rightarrow$@  false = false
+
+@$\Rightarrow$@t : {x : Bool} @$\rightarrow$@ x  @$\Rightarrow$@ true  @$\equiv$@ true
+@$\Rightarrow$@t {x} with x
+@$\Rightarrow$@t {x} | false = refl
+@$\Rightarrow$@t {x} | true = refl
+
+f@$\Rightarrow$@ : {x : Bool} @$\rightarrow$@ false  @$\Rightarrow$@ x  @$\equiv$@ true
+f@$\Rightarrow$@ {x} with x
+f@$\Rightarrow$@ {x} | false = refl
+f@$\Rightarrow$@ {x} | true = refl
+
+@$\wedge$@-pi1 : { x y : Bool } @$\rightarrow$@ x  @$\wedge$@  y  @$\equiv$@ true  @$\rightarrow$@ x  @$\equiv$@ true
+@$\wedge$@-pi1 {x} {y} eq with x | y | eq
+@$\wedge$@-pi1 {x} {y} eq | false | b | ()
+@$\wedge$@-pi1 {x} {y} eq | true | false | ()
+@$\wedge$@-pi1 {x} {y} eq | true | true | refl = refl
+
+@$\wedge$@-pi2 : { x y : Bool } @$\rightarrow$@  x  @$\wedge$@  y  @$\equiv$@ true  @$\rightarrow$@ y  @$\equiv$@ true
+@$\wedge$@-pi2 {x} {y} eq with x | y | eq
+@$\wedge$@-pi2 {x} {y} eq | false | b | ()
+@$\wedge$@-pi2 {x} {y} eq | true | false | ()
+@$\wedge$@-pi2 {x} {y} eq | true | true | refl = refl
+
+@$\wedge$@true : { x : Bool } @$\rightarrow$@  x  @$\wedge$@  true  @$\equiv$@ x
+@$\wedge$@true {x} with x
+@$\wedge$@true {x} | false = refl
+@$\wedge$@true {x} | true = refl
+
+true@$\wedge$@ : { x : Bool } @$\rightarrow$@  true  @$\wedge$@  x  @$\equiv$@ x
+true@$\wedge$@ {x} with x
+true@$\wedge$@ {x} | false = refl
+true@$\wedge$@ {x} | true = refl
+bool-case : ( x : Bool ) { p : Set } @$\rightarrow$@ ( x @$\equiv$@ true  @$\rightarrow$@ p ) @$\rightarrow$@ ( x @$\equiv$@ false  @$\rightarrow$@ p ) @$\rightarrow$@ p
+bool-case x T F with x
+bool-case x T F | false = F refl
+bool-case x T F | true = T refl
+
+impl@$\Rightarrow$@ :  {x y : Bool} @$\rightarrow$@ (x  @$\equiv$@ true @$\rightarrow$@ y  @$\equiv$@ true ) @$\rightarrow$@ x  @$\Rightarrow$@ y  @$\equiv$@ true
+impl@$\Rightarrow$@ {x} {y} p = bool-case x (@$\lambda$@ x=t @$\rightarrow$@   let open @$\equiv$@-Reasoning  in
+          begin
+            x  @$\Rightarrow$@ y
+          @$\equiv$@@$\langle$@  cong ( @$\lambda$@ z @$\rightarrow$@ x  @$\Rightarrow$@ z ) (p x=t ) @$\rangle$@
+            x  @$\Rightarrow$@  true
+          @$\equiv$@@$\langle$@ @$\Rightarrow$@t @$\rangle$@
+            true
+          @$\blacksquare$@
+    ) ( @$\lambda$@ x=f @$\rightarrow$@  let open @$\equiv$@-Reasoning  in
+          begin
+            x  @$\Rightarrow$@  y
+          @$\equiv$@@$\langle$@  cong ( @$\lambda$@ z @$\rightarrow$@ z  @$\Rightarrow$@  y ) x=f @$\rangle$@
+            true
+          @$\blacksquare$@
+  )
+ 
+Equal@$\rightarrow$@@$\equiv$@ : { x y : @$\mathbb{N}$@ } @$\rightarrow$@  Equal x y @$\equiv$@ true @$\rightarrow$@ x @$\equiv$@ y
+Equal@$\rightarrow$@@$\equiv$@ {x} {y} eq with x ≟ y
+Equal@$\rightarrow$@@$\equiv$@ {x} {y} refl | yes refl = refl
+Equal@$\rightarrow$@@$\equiv$@ {x} {y} () | no @$\neg$@p 
+
+Equal+1 : { x y : @$\mathbb{N}$@ } @$\rightarrow$@  Equal x y @$\equiv$@ Equal (suc x) (suc y)
+Equal+1 {x} {y} with  x ≟ y
+Equal+1 {x} {.x} | yes refl = {!!}
+Equal+1 {x} {y} | no @$\neg$@p = {!!}
+
+open import Data.Empty 
+
+@$\equiv$@@$\rightarrow$@Equal : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ x @$\equiv$@ y @$\rightarrow$@  Equal x y @$\equiv$@ true 
+@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl with x ≟ x
+@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl | yes refl = refl
+@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl | no @$\neg$@p = @$\bot$@-elim ( @$\neg$@p refl )

--- 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)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_impl/init_cg.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,2 @@
+whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
+whileTest c10 next = next (record {varn = c10 ; vari = 0} )
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_impl/init_cg.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,2 @@
+whileTest : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTest c10 next = next (record {varn = c10 ; vari = 0} )
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_impl/while_loop.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,5 @@
+{-# TERMINATING #-}
+whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_impl/while_loop.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,5 @@
+{-@$\#$@ TERMINATING @$\#$@-}
+whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_impl/while_loop_c.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,2 @@
+whileLoopC : ℕ → Env
+whileLoopC n = whileTest n (λ env → whileLoop env (λ env1 → env1 ))
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_impl/while_loop_c.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,2 @@
+whileLoopC : @$\mathbb{N}$@ @$\rightarrow$@ Env
+whileLoopC n = whileTest n (@$\lambda$@ env @$\rightarrow$@ whileLoop env (@$\lambda$@ env1 @$\rightarrow$@ env1 ))
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_impl/while_loop_dg.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,5 @@
+record Env  : Set where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_impl/while_loop_dg.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,5 @@
+record Env  : Set where
+  field
+    varn : @$\mathbb{N}$@
+    vari : @$\mathbb{N}$@
+open Env
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/conversion.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,10 @@
+conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+               → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
+conversion1 env {c10} p1 next = next env proof4 where
+      proof4 : varn env + vari env ≡ c10
+      proof4 = let open ≡-Reasoning  in begin
+            varn env + vari env ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
+            c10 + vari env      ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
+            c10 + 0             ≡⟨ +-sym {c10} {0} ⟩
+            c10
+          ∎
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/conversion.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,10 @@
+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
+      proof4 : varn env + vari env @$\equiv$@ c10
+      proof4 = let open @$\equiv$@-Reasoning  in begin
+            varn env + vari env @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ n + vari env ) (pi2 p1 ) @$\rangle$@
+            c10 + vari env      @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ c10 + n ) (pi1 p1 ) @$\rangle$@
+            c10 + 0             @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@
+            c10
+          @$\blacksquare$@
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/init_cg.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,7 @@
+whileTest' : {l : Level} {t : Set l}  → {c10 :  ℕ } → (Code : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+whileTest' {_} {_} {c10} next = next env proof2
+  where
+    env : Env
+    env = record {vari = 0 ; varn = c10}
+    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
+    proof2 = record {pi1 = refl ; pi2 = refl}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/init_cg.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,7 @@
+whileTest@$\prime$@ : {l : Level} {t : Set l}  @$\rightarrow$@ {c10 :  @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env)  @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTest@$\prime$@ {_} {_} {c10} next = next env proof2
+  where
+    env : Env
+    env = record {vari = 0 ; varn = c10}
+    proof2 : ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) -- PostCondition
+    proof2 = record {pi1 = refl ; pi2 = refl}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/verif.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,4 @@
+proofGearsTermS : {c10 :  ℕ } → ⊤
+proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
+    TerminatingLoopS Env (λ env → varn env)
+        (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/verif.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,4 @@
+proofGearsTermS : {c10 :  @$\mathbb{N}$@ } @$\rightarrow$@ @$\top$@
+proofGearsTermS {c10} = whileTest@$\prime$@ {_} {_}  {c10} (@$\lambda$@ n p @$\rightarrow$@  conversion1 n p (@$\lambda$@ n1 p1 @$\rightarrow$@
+    TerminatingLoopS Env (@$\lambda$@ env @$\rightarrow$@ varn env)
+        (@$\lambda$@ n2 p2 loop @$\rightarrow$@ whileLoopSeg {_} {_} {c10} n2 p2 loop (@$\lambda$@ ne pe @$\rightarrow$@ whileTestSpec1 c10 ne pe)) n1 p1 )) 
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/verif_loop.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,12 @@
+TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ)
+   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t)
+   → (r : Index) → (p : Invraiant r)  → t 
+TerminatingLoopS {_} {t} Index {Invraiant} reduce loop  r p with <-cmp 0 (reduce r)
+... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) 
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where 
+    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
+    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) 
+    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 
+    ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
+    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/verif_loop.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,12 @@
+TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) @$\rightarrow$@ {Invraiant : Index @$\rightarrow$@ Set } @$\rightarrow$@ ( reduce : Index @$\rightarrow$@ @$\mathbb{N}$@)
+   @$\rightarrow$@ (loop : (r : Index)  @$\rightarrow$@ Invraiant r @$\rightarrow$@ (next : (r1 : Index)  @$\rightarrow$@ Invraiant r1 @$\rightarrow$@ reduce r1 < reduce r  @$\rightarrow$@ t ) @$\rightarrow$@ t)
+   @$\rightarrow$@ (r : Index) @$\rightarrow$@ (p : Invraiant r)  @$\rightarrow$@ t 
+TerminatingLoopS {_} {t} Index {Invraiant} reduce loop  r p with <-cmp 0 (reduce r)
+... | tri≈ @$\neg$@a b @$\neg$@c = loop r p (@$\lambda$@ r1 p1 lt @$\rightarrow$@ @$\bot$@-elim (lemma3 b lt) ) 
+... | tri< a @$\neg$@b @$\neg$@c = loop r p (@$\lambda$@ r1 p1 lt1 @$\rightarrow$@ TerminatingLoop1 (reduce r) r r1 (@$\leq$@-step lt1) p1 lt1 ) where 
+    TerminatingLoop1 : (j : @$\mathbb{N}$@) @$\rightarrow$@ (r r1 : Index) @$\rightarrow$@ reduce r1 < suc j  @$\rightarrow$@ Invraiant r1 @$\rightarrow$@  reduce r1 < reduce r @$\rightarrow$@ t
+    TerminatingLoop1 zero r r1 n@$\leq$@j p1 lt = loop r1 p1 (@$\lambda$@ r2 p1 lt1 @$\rightarrow$@ @$\bot$@-elim (lemma5 n@$\leq$@j lt1)) 
+    TerminatingLoop1 (suc j) r r1  n@$\leq$@j p1 lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a @$\neg$@b @$\neg$@c = TerminatingLoop1 j r r1 a p1 lt 
+    ... | tri≈ @$\neg$@a b @$\neg$@c = loop r1 p1 (@$\lambda$@ r2 p2 lt1 @$\rightarrow$@ TerminatingLoop1 j r1 r2 (subst (@$\lambda$@ k @$\rightarrow$@ reduce r2 < k ) b lt1 ) p2 lt1 )
+    ... | tri> @$\neg$@a @$\neg$@b c =  @$\bot$@-elim ( nat-@$\leq$@> c n@$\leq$@j )   
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/verif_term.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,5 @@
+whileTestSpec1 : (c10 : ℕ) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
+whileTestSpec1 _ _ x = tt
+
+proofGears : {c10 :  ℕ } → ⊤
+proofGears {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/verif_term.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,5 @@
+whileTestSpec1 : (c10 : @$\mathbb{N}$@) @$\rightarrow$@  (e1 : Env ) @$\rightarrow$@ vari e1 @$\equiv$@ c10 @$\rightarrow$@ @$\top$@
+whileTestSpec1 _ _ x = tt
+
+proofGears : {c10 :  @$\mathbb{N}$@ } @$\rightarrow$@ @$\top$@
+proofGears {c10} = whileTest@$\prime$@ {_} {_}  {c10} (@$\lambda$@ n p1 @$\rightarrow$@  conversion1 n p1 (@$\lambda$@ n1 p2 @$\rightarrow$@ whileLoop@$\prime$@ n1 p2 (@$\lambda$@ n2 p3 @$\rightarrow$@ whileTestSpec1 c10 n2 p3 ))) 
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/while_loop.agda	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,24 @@
+{-# TERMINATING #-}
+whileLoop' : {l : Level} {t : Set l} → (env : Env) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10)
+   → (Code : (e1 : Env )→ vari e1 ≡ c10 → t) → t
+whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
+whileLoop' env {c10} proof next | no p = next env ( begin
+       vari env            ≡⟨ refl ⟩
+       0 + vari env        ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩
+       varn env + vari env ≡⟨ proof ⟩
+       c10 ∎ ) where open ≡-Reasoning  
+whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next where
+      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
+      1<0 : 1 ≤ zero → ⊥
+      1<0 ()
+      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
+      proof3 (s≤s lt) with varn  env
+      proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
+      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in begin
+             n' + (vari env + 1)  ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+             n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+             (n' + 1) + vari env  ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+             (suc n' ) + vari env ≡⟨⟩
+             varn env + vari env  ≡⟨ proof  ⟩
+             c10
+          ∎
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/while_loop_verif/while_loop.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,24 @@
+{-@$\#$@ TERMINATING @$\#$@-}
+whileLoop@$\prime$@ : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 :  @$\mathbb{N}$@ } @$\rightarrow$@ ((varn env) + (vari env) @$\equiv$@ c10)
+   @$\rightarrow$@ (Code : (e1 : Env )@$\rightarrow$@ vari e1 @$\equiv$@ c10 @$\rightarrow$@ t) @$\rightarrow$@ t
+whileLoop@$\prime$@ env proof next with  ( suc zero  @$\leq$@? (varn  env) )
+whileLoop@$\prime$@ env {c10} proof next | no p = next env ( begin
+       vari env            @$\equiv$@@$\langle$@ refl @$\rangle$@
+       0 + vari env        @$\equiv$@@$\langle$@ cong (@$\lambda$@ k @$\rightarrow$@ k + vari env) (sym (lemma1 p )) @$\rangle$@
+       varn env + vari env @$\equiv$@@$\langle$@ proof @$\rangle$@
+       c10 @$\blacksquare$@ ) where open @$\equiv$@-Reasoning  
+whileLoop@$\prime$@ env {c10} proof next | yes p = whileLoop@$\prime$@ env1 (proof3 p ) next where
+      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
+      1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@
+      1<0 ()
+      proof3 : (suc zero  @$\leq$@ (varn  env))  @$\rightarrow$@ varn env1 + vari env1 @$\equiv$@ c10
+      proof3 (s@$\leq$@s lt) with varn  env
+      proof3 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 p)
+      proof3 (s@$\leq$@s (z@$\leq$@n {n@$\prime$@}) ) | suc n =  let open @$\equiv$@-Reasoning  in begin
+             n@$\prime$@ + (vari env + 1)  @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ n@$\prime$@ + z ) ( +-sym  {vari env} {1} )  @$\rangle$@
+             n@$\prime$@ + (1 + vari env ) @$\equiv$@@$\langle$@ sym ( +-assoc (n@$\prime$@)  1 (vari env) ) @$\rangle$@
+             (n@$\prime$@ + 1) + vari env  @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env )  +1@$\equiv$@suc  @$\rangle$@
+             (suc n@$\prime$@ ) + vari env @$\equiv$@@$\langle$@@$\rangle$@
+             varn env + vari env  @$\equiv$@@$\langle$@ proof  @$\rangle$@
+             c10
+          @$\blacksquare$@
\ No newline at end of file

--- a/Paper/tex/hoare.tex	Tue Nov 02 06:58:39 2021 +0900
+++ b/Paper/tex/hoare.tex	Fri Nov 05 15:19:08 2021 +0900
@@ -16,7 +16,7 @@
 これらを満たし、
 事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
 
-\section{Hoare Logic による Code Gear の検証手法 }
+\subsection{Hoare Logic による Code Gear の検証手法 }
 
 \figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。
 input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/tex/while_loop.tex	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,86 @@
+\section{Gears Agda にて Hoare Logic を用いた検証の例}
+ここでは Gears Agda にて Hoare Logic を用いた検証の例として、
+ While Loop プログラムを実装・検証する。
+
+\subsection{While Loop の実装}
+まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する。
+実装はまず、 Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う。
+\lstinputlisting[label=while-loop-dg, caption=Data Gearの定義] {src/while_loop_impl/while_loop_dg.agda.replaced}
+
+そのため最初の Code Gear は引数を受け取り、Envを作成する Code Gear となる Code \ref{while_init_cg}。
+
+\lstinputlisting[label=while_init_cg, caption=Data Gear の定義を行う Code Gear] {src/while_loop_impl/init_cg.agda.replaced}
+
+次に、目的である While Loop の実装を行う。ソースコードは Code \ref{while-loop} のようになる。
+
+\lstinputlisting[label=while-loop, caption=Loop の部分を担う Code Gears] {src/while_loop_impl/while_loop.agda.replaced}
+
+また Agda では停止性の検出機能が存在し、
+プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る。
+その場合は関数定義の直前に
+\{-$\#$ TERMINATING $\#$-\} のタグを付けると
+停止しないプログラムをコンパイルすることができる
+
+これまでの Code Gear を繋げることで、 While Loop　を行う Code を実装することができる。
+
+\lstinputlisting[label=while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced}
+
+\subsection{While Loop の検証}
+
+Gears Agda にて行なった While Loop の実装コードを元に、
+5章にて述べた Pre / Post Condition を記述していくことで
+Hoare Logic を用いた検証を行う。
+
+検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear の定義から行う。Code \ref{while_verif_init_cg} がそれに当たる。
+
+\lstinputlisting[label=while_verif_init_cg, caption=While Loop を行う Code Gear] {src/while_loop_verif/init_cg.agda.replaced}
+
+今回は検証を行いたいため 5.1 で述べたように、実装に加えて Pre / Post Condition を持つ必要がある。
+init時の Pre Condition のみ特殊で　Agda での関数定義の際に記述し、
+「Data Gear に正しく初期値が設定される」という条件を使用する。これが
+((vari env) $\equiv$ 0) $\wedge$ ((varn env) $\equiv$ c10)
+に当たる。
+そしてinit時以外の、Pre Condition と Post Condition には実行開始から実行終了までの間で不変の条件を記述する。
+今回は While Loop の不変条件として、
+$今回loopさせたい回数(c10) = 残りのloopする回数(vern) + 今回loopした回数(vari)$
+を設定した。これがinit時の Post Condition となる。
+
+また、init時の Pre Condition と同じ値で
+Post Condition を設定しなければならない。
+init時の Pre Condition を Post Condition に変換する Code \ref{conversion} を記載する。
+
+\lstinputlisting[label=conversion, caption=init時の Pre Condition を Post Condition に変換する Code Gear] {src/while_loop_verif/conversion.agda.replaced}
+
+ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため、
+この後の Pre / Post Condition は停止するまでこれを用いる。
+
+以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが、 Wile Loop の Loop 部分の検証を行う Code Gear となる。
+
+\lstinputlisting[label=loop_verif_cg, caption=停止性以外の Loop の検証も行う Code Gear] {src/while_loop_verif/while_loop.agda.replaced}
+
+Loop が停止することを示していないため、関数定義の直前に \{-\# TERMINATING \#-\} が記述されている。
+こちらも Loop の実装以外に、Pre / Post Condition を満たしているか検証を行い、次の Code Gear に渡している。
+
+ここまでで定義した Pre / Post Consition が付いている Code Gear を繋げることで、
+停止性以外の While Loop の検証を行う Code Gear を実装できる。
+
+\lstinputlisting[label=loop_verif_cg, caption=停止性以外の While Loop の検証を行う Code Gear] {src/while_loop_verif/verif_term.agda.replaced}
+
+停止性の検証も行う While Loop の検証を行う Code Gear を実装する
+
+\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う Loop 部分の Code Gear] {src/while_loop_verif/verif_loop.agda.replaced}
+
+停止することを Agda が理解できるように記述すると良い。
+そのため引数に減少していく変数 reduce を追加し、
+loop するとデクリメントするように実装する。
+
+loop には先ほど実装した loop の部分を担う Code Gear が次の関数遷移先を引数に受け取れるようにした
+whileLoopSeg を使用する。
+
+そしてこれらを繋げて While Loop の検証を行うことができる Code ref を実装できた。
+
+\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced}
+
+
+
+