Mercurial > hg > Papers > 2018 > ryokka-sigos

--- a/Paper/auto/sigos.el	Fri Apr 13 18:07:04 2018 +0900
+++ b/Paper/auto/sigos.el	Fri Apr 13 19:47:50 2018 +0900
@@ -22,7 +22,21 @@
     "listings"
     "jlisting"
     "enumitem"
+    "bussproofs"
+    "amsmath"
+    "multirow"
+    "here"
+    "cite"
+    "amssymb"
     "caption")
+   (LaTeX-add-labels
+    "fig:csds"
+    "fig:code_simple"
+    "fig:factorial"
+    "agda-interface-stack"
+    "hoare-logic"
+    "fig:hoare"
+    "fig:cbc-hoare")
    (LaTeX-add-bibliographies))
  :latex)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaBasics.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,1 @@
+module AgdaBasics where
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaInterface.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,35 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module AgdaInterface where
+
+data Maybe {n : Level } (a : Set n) : Set n where
+  Nothing : Maybe a
+  Just    : a @$\rightarrow$@ Maybe a
+
+record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    push : stackImpl @$\rightarrow$@ a @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop  : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    get  : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    get2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    clear : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+open StackMethods
+
+record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    stack : si
+    stackMethods : StackMethods {n} {m} a {t} si
+  pushStack :  a @$\rightarrow$@ (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
+  pushStack d next = push (stackMethods ) (stack ) d (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
+  popStack : (Stack a si @$\rightarrow$@ Maybe a  @$\rightarrow$@ t) @$\rightarrow$@ t
+  popStack next = pop (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  pop2Stack :  (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  getStack :  (Stack a si @$\rightarrow$@ Maybe a  @$\rightarrow$@ t) @$\rightarrow$@ t
+  getStack next = get (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  get2Stack :  (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  clearStack : (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
+  clearStack next = clear (stackMethods ) (stack ) (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
+
+open Stack
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaSingleLinkedStack.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,63 @@
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+push = pushSingleLinkedStack
+; pop  = popSingleLinkedStack
+; pop2 = pop2SingleLinkedStack
+; get  = getSingleLinkedStack
+; get2 = get2SingleLinkedStack
+; clear = clearSingleLinkedStack
+}
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+stack = emptySingleLinkedStack ;
+stackMethods = singleLinkedStackSpec
+}
+
+-- Implementation
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+popSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+
+pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
+  where
+    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
+
+
+getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+getSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack (Just data1)
+  where
+    data1  = datum d
+
+get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
+  where
+    get2SingleLinkedStack' : {n m : Level} {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+    get2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
+
+clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\rightarrow$@ t) @$\rightarrow$@ t
+clearSingleLinkedStack stack next = next (record {top = Nothing})
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaStackImpl.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,28 @@
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+  top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+-- Basic stack implementations are specifications of a Stack
+
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                               }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                            stack = emptySingleLinkedStack ;
+                            stackMethods = singleLinkedStackSpec
+                          }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaStackSomeState.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,6 @@
+stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) @$\rightarrow$@ Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+
+push@$\rightarrow$@push@$\rightarrow$@pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) @$\rightarrow$@ pushStack (stackInSomeState s)  x (\s1 @$\rightarrow$@ pushStack s1 y (\s2 @$\rightarrow$@ pop2Stack s2 (\s3 y1 x1 @$\rightarrow$@
+   (Just x @$\equiv$@ x1) ∧ (Just y @$\equiv$@ y1))))
+push@$\rightarrow$@push@$\rightarrow$@pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaStackTest.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,22 @@
+-- after push 1 and 2, pop2 get 1 and 2
+
+testStack02 : {m : Level } @$\rightarrow$@  ( Stack  @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m}
+testStack02 cs = pushStack createSingleLinkedStack 1 (\s @$\rightarrow$@ pushStack s 2 cs)
+
+
+testStack031 : (d1 d2 : $\mathbb{N}$ ) @$\rightarrow$@ Bool {Zero}
+testStack031 2 1 = True
+testStack031 _ _ = False
+
+testStack032 : (d1 d2 : Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {Zero}
+testStack032  (Just d1) (Just d2) = testStack031 d1 d2
+testStack032  _ _ = False
+
+testStack03 : {m : Level } @$\rightarrow$@ Stack  @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ ((Maybe @$\mathbb{N}$@) @$\rightarrow$@ (Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m}
+testStack03 s cs = pop2Stack s (\s d1 d2 @$\rightarrow$@ cs d1 d2 )
+
+testStack04 : Bool
+testStack04 = testStack02 (\s @$\rightarrow$@ testStack03 s testStack032)
+
+testStack05 : testStack04 @$\equiv$@ True
+testStack05 = refl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaTree.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,17 @@
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    getImpl  : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+    putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
+    getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+
+open Tree
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaTreeDebug.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,15 @@
+test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1
+  $ \t @$\rightarrow$@ putTree1 t 2 2
+  $ \t @$\rightarrow$@ putTree1 t 3 3
+  $ \t @$\rightarrow$@ putTree1 t 4 4
+  $ \t @$\rightarrow$@ getRedBlackTree t 4
+  $ \t x @$\rightarrow$@ x
+
+-- Just
+-- (record
+-- { key = 4
+-- ; value = 4
+-- ; right = Nothing
+-- ; left = Nothing
+-- ; color = Red
+-- })
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaTreeImpl.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,47 @@
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    getImpl  : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+    putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
+    getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+open Tree
+
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+  field
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+leafNode : {n : Level } {a k : Set n}  @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k
+leafNode k1 value = record {
+  key   = k1 ;
+  value = value ;
+  right = Nothing ;
+  left  = Nothing ;
+  color = Red
+  }
+record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where
+  field
+    root : Maybe (Node a k)
+    nodeStack : SingleLinkedStack  (Node a k)
+    compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n}
+open RedBlackTree
+
+putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
+putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next))
+
+-- 以下省略
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/AgdaTreeProof.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,34 @@
+redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@
+redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
+
+putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@))
+         @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@)
+         @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x
+         (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True))
+putTest1 n k x with n
+...  | Just n1 = lemma2 ( record { top = Nothing } )
+   where
+     lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
+         GetRedBlackTree.checkNode t k (λ t@$\text{1}$@ x1 → check2 x1 x @$\equiv$@ True) (root t))
+     lemma2 s with compare2 k (key n1)
+     ... |  EQ = lemma3 {!!}
+        where
+           lemma3 : compare2 k (key n1) @$\equiv$@  EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record {  root = Just ( record {
+               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
+               } ) ; nodeStack = s ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y  } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True)
+           lemma3 eq with compare2 x x | putTest1Lemma2 x
+           ... | EQ | refl with compare2 k (key n1)  | eq
+           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
+           ...                    | EQ | refl = refl
+     ... |  GT = {!!}
+     ... |  LT = {!!}
+
+...  | Nothing =  lemma1
+   where
+     lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record {  root = Just ( record {
+               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red
+        } ) ; nodeStack = record { top = Nothing } ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y  } ) k
+        ( \ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True)
+     lemma1 with compare2 k k | putTest1Lemma2 k
+     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
+     ...              | EQ | refl = refl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/CodeSegment.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,2 @@
+data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l @$\sqcup$@ l1 @$\sqcup$@ l2) where
+  cs : (I @$\rightarrow$@ O) @$\rightarrow$@ CodeSegment I O
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/DataSegment.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
+record ds1 : Set where
+  field
+    c : Int
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/Goto.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,4 @@
+goto : {l1 l2 : Level} {I : Set l1} {O : Set l2}
+   @$\rightarrow$@ CodeSegment I O @$\rightarrow$@ I @$\rightarrow$@ O
+goto (cs b) i = b i
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/MetaGear.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: MetaGear.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 792 532
+%%HiResBoundingBox: 0.000000 0.000000 792.000000 532.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/cbc-hoare.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/cbc-hoare.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: cbc-hoare.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 580 175
+%%HiResBoundingBox: 0.000000 0.000000 580.000000 175.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/cbc-subtype.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/cbc-subtype.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: cbc-subtype.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 1084 281
+%%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/cbc_goto.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: cbc_goto.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 393 201
+%%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/codeGear_dataGear.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: codeGear_dataGear.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 535 427
+%%HiResBoundingBox: 0.000000 0.000000 535.000000 427.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/codeGear_dataGear_dependency.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: codeGear_dataGear_dependency.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 535 247
+%%HiResBoundingBox: 0.000000 0.000000 535.000000 247.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/codesegment.pdf has changed
--- a/Paper/pic/codesegment.xbb	Fri Apr 13 18:07:04 2018 +0900
+++ b/Paper/pic/codesegment.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: ./pic/codesegment.pdf
-%%Creator: extractbb 20140317
-%%BoundingBox: 0 0 393 201
-%%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000
+%%Title: codesegment.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 305 85
+%%HiResBoundingBox: 0.000000 0.000000 305.000000 85.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Fri Nov 24 17:30:26 2017
+%%CreationDate: Fri Apr 13 18:34:25 2018
Binary file Paper/pic/codesegment2.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/codesegment2.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: codesegment2.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 393 201
+%%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/csds.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/csds.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: csds.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 580 76
+%%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/factorial.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/factorial.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: factorial.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 296 220
+%%HiResBoundingBox: 0.000000 0.000000 296.000000 220.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/gears-meta.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/gears-meta.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: gears-meta.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 653 243
+%%HiResBoundingBox: 0.000000 0.000000 653.000000 243.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- a/Paper/pic/gears_structure.xbb	Fri Apr 13 18:07:04 2018 +0900
+++ b/Paper/pic/gears_structure.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: ./pic/gears_structure.pdf
-%%Creator: extractbb 20140317
+%%Title: gears_structure.pdf
+%%Creator: extractbb 20160307
 %%BoundingBox: 0 0 713 418
 %%HiResBoundingBox: 0.000000 0.000000 713.000000 418.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Fri Nov 24 17:30:26 2017
+%%CreationDate: Fri Apr 13 18:34:25 2018
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/gearsos.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: gearsos.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 1174 1004
+%%HiResBoundingBox: 0.000000 0.000000 1174.000000 1004.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/generate_context.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: generate_context.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 508 408
+%%HiResBoundingBox: 0.000000 0.000000 508.000000 408.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/generate_context2.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: generate_context2.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 706 355
+%%HiResBoundingBox: 0.000000 0.000000 706.000000 355.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- a/Paper/pic/generate_context3.xbb	Fri Apr 13 18:07:04 2018 +0900
+++ b/Paper/pic/generate_context3.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: ./pic/generate_context3.pdf
-%%Creator: extractbb 20140317
-%%BoundingBox: 0 0 706 265
-%%HiResBoundingBox: 0.000000 0.000000 706.000000 265.000000
+%%Title: generate_context3.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 706 274
+%%HiResBoundingBox: 0.000000 0.000000 706.000000 274.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Fri Nov 24 17:30:33 2017
+%%CreationDate: Fri Apr 13 18:34:25 2018
Binary file Paper/pic/goto.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/goto.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: goto.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 305 85
+%%HiResBoundingBox: 0.000000 0.000000 305.000000 85.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/hoare-logic.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/hoare-logic.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: hoare-logic.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 580 76
+%%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/meta-hierarchy.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/meta-hierarchy.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: meta-hierarchy.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 832 283
+%%HiResBoundingBox: 0.000000 0.000000 832.000000 283.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/meta.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/meta.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: meta.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 958 148
+%%HiResBoundingBox: 0.000000 0.000000 958.000000 148.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- a/Paper/pic/metaCS.xbb	Fri Apr 13 18:07:04 2018 +0900
+++ b/Paper/pic/metaCS.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: ./fig/metaCS.pdf
-%%Creator: extractbb 20140317
+%%Title: metaCS.pdf
+%%Creator: extractbb 20160307
 %%BoundingBox: 31 511 515 732
 %%HiResBoundingBox: 30.601520 511.100000 515.413800 732.012800
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb 15 05:21:55 2016
+%%CreationDate: Fri Apr 13 18:34:25 2018
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/meta_cg_dg.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: meta_cg_dg.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 608 522
+%%HiResBoundingBox: 0.000000 0.000000 608.000000 522.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/meta_gear.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: meta_gear.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 788 229
+%%HiResBoundingBox: 0.000000 0.000000 788.000000 229.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/metameta.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/metameta.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: metameta.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 472 184
+%%HiResBoundingBox: 0.000000 0.000000 472.000000 184.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/modus-ponens.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/modus-ponens.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: modus-ponens.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 96 684 500 799
+%%HiResBoundingBox: 96.082030 683.554700 499.886700 799.296900
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Mon Jan 29 15:58:01 2018
+
Binary file Paper/pic/non-destructive-rbtree.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/non-destructive-rbtree.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: non-destructive-rbtree.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 559 248
+%%HiResBoundingBox: 0.000000 0.000000 559.000000 248.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/persistent_date_tree.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: persistent_date_tree.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 773 374
+%%HiResBoundingBox: 0.000000 0.000000 773.000000 374.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/persistent_date_tree_2.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: persistent_date_tree_2.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 736 271
+%%HiResBoundingBox: 0.000000 0.000000 736.000000 271.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/put.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/put.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: put.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 868 130
+%%HiResBoundingBox: 0.000000 0.000000 868.000000 130.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/rbtree.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/rbtree.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: rbtree.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 562 274
+%%HiResBoundingBox: 0.000000 0.000000 562.000000 274.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/ryukyu.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/ryukyu.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: ryukyu.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 595 842
+%%HiResBoundingBox: 0.000000 0.000000 595.000000 842.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/subtype-arg.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/subtype-arg.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: subtype-arg.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 1084 281
+%%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
Binary file Paper/pic/subtype-return.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/subtype-return.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: subtype-return.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 1084 281
+%%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/taskManager.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: taskManager.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 1021 459
+%%HiResBoundingBox: 0.000000 0.000000 1021.000000 459.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/twice_640.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: twice_640.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 360 216
+%%HiResBoundingBox: 0.000000 0.000000 360.000000 216.000000
+%%PDFVersion: 1.4
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/verification.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: verification.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 478 204
+%%HiResBoundingBox: 0.000000 0.000000 478.000000 204.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/pic/worker.xbb	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+%%Title: worker.pdf
+%%Creator: extractbb 20160307
+%%BoundingBox: 0 0 901 644
+%%HiResBoundingBox: 0.000000 0.000000 901.000000 644.000000
+%%PDFVersion: 1.3
+%%Pages: 1
+%%CreationDate: Fri Apr 13 18:34:25 2018
+
--- a/Paper/sigos.tex	Fri Apr 13 18:07:04 2018 +0900
+++ b/Paper/sigos.tex	Fri Apr 13 19:47:50 2018 +0900
@@ -3,6 +3,13 @@
 \usepackage{url}
 \usepackage{listings,jlisting}
 \usepackage{enumitem}
+\usepackage{bussproofs}
+\usepackage{amsmath}
+\usepackage{multirow}
+\usepackage{here}
+\usepackage{cite}
+\usepackage{listings}
+\usepackage{amssymb}

 \lstset{
     language=C,
@@ -87,8 +94,939 @@

 % 信頼性の高いOS

-\section{OS での信頼性の保証}
-test
+\section{ソフトウェアの信頼性の保証}
+
+動作するソフトウェアは高い信頼性を持つことが望ましい。
+そのためにはソフトウェアが期待される動作をすることを保証する必要がある。
+期待される動作は仕様と呼ばれ、自然言語や論理によって記述される。
+また、ソフトウェアのが期待される動作をすることを保証するためには検証をする必要が
+ある。
+
+ソフトウェアの検証手法には定理証明とモデル検査がある。
+定理証明では。ソフトウェアが満たすべき仕様を論理式で記述し、その論理式が常に正し
+いことを証明する。
+定理証明支援系には依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} などが存
+在する。
+
+モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が正し
+いことを確認する。モデル検査器には Spin\cite{spin} や、モデルを状態遷移系で記述
+する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
+
+当研究室では検証の単位として CodeGear、DataGear という単位を用いてソフトウェアを記述する手法を提案している。
+また、 CodeGear 、 DataGear という単位を用いてプログラミングする言語としてCountinuation based C\cite{kaito:2015}を開発している。Continuation based C (CbC)はC言語と似た構文を持つ言語である。
+
+本論文では CbC で Interface と呼ばれる記述方法を Agda で表現し、その記述を通した
+実装の仕様の一部に対して証明を行なった。
+
+\section{CodeGear, DataGear}
+
+CodeGear、 DataGear は当研究室で提案している検証の単位である。
+処理の単位を CodeGear、処理に使うデータの単位を DataGear とし、
+CodeGear を他の CodeGear と継続することでプログラムを構成する。
+図\ref{fig:csds}のように Input DataGear を受け取り、 CodeGear で Output
+DataGear に変更を加えることでプログラムを記述していく。
+% CS,DSの図
+\begin{figure}[htpb]
+ \begin{center}
+  \scalebox{0.25}{\includegraphics{pic/csds.pdf}}
+ \end{center}
+ \caption{CodeGear と DataGear}
+ \label{fig:csds}
+\end{figure}
+
+
+\section{ CbC での CodeGear、 DataGear}
+CbC での簡単な記述例をソースコード\ref{code_simple}、流れを図\ref{fig:code_simple}に示
+す。CbC では CodeGear を$\_\_$code キーワードを指定する。その際、Input
+DataGear は関数の引数として定義される。 CodeGear は継続で次の CodeGear
+に遷移するために関数末尾で goto キーワードの後に CodeGear 名と Input
+DataGear を指定する必要がある。
+
+ソースコード\ref{code_simple}では　cs0、 cs1 が CodeGear で a+b が cs0 の Output DataGear であり、
+cs1 の Input DataGear である。
+
+\begin{lstlisting}[frame=lrbt,label=code_simple,caption={CodeGear の継続の例}]
+__code cg0(int a, int b){
+  goto cg1(a+b);
+}
+
+__code cg1(int c){
+  goto cg2(c);
+}
+\end{lstlisting}
+
+
+\begin{figure}[htpb]
+ \begin{center}
+  \scalebox{0.6}{\includegraphics{pic/codesegment.pdf}}
+ \end{center}
+ \caption{ソースコード\ref{code_simple}の流れ}
+ \label{fig:code_simple}
+\end{figure}
+
+CbC の継続は、呼び出し元の情報を持たずに処理を続ける。この継続を軽量継続と呼ぶ。
+ソースコード\ref{code_simple}は cs0 から cs1 へ継続した後、 cs0 には戻らずに次の継
+続に指定された CodeGear へ継続する。
+
+CbC でのループ処理の記述例をソースコード\ref{factorial}、流れを図\ref{fig:factorial}に示
+す。
+軽量継続では関数呼び出しのスタックは存在しないが、ソースコード\ref{factorial}の
+ように計算中の値を DataGear で持つことでループ処理を行なうこともできる。
+
+\begin{lstlisting}[frame=lrbt,label=factorial,caption={階乗を求め
+る CbC プログラムの例}]
+__code print_factorial(int prod)
+{
+  printf("factorial = %d\n",prod);
+  exit(0);
+}
+
+__code factorial0(int prod, int x)
+{
+  if ( x >= 1) {
+    goto factorial0(prod*x, x-1);
+  }else{
+    goto print_factorial(prod);
+  }
+
+}
+
+__code factorial(int x)
+{
+  goto factorial0(1, x);
+}
+
+int main(int argc, char **argv)
+{
+  int i;
+  i = atoi(argv[1]);
+
+  goto factorial(i);
+}
+\end{lstlisting}
+
+\begin{figure}[htpb]
+ \begin{center}
+  \scalebox{0.6}{\includegraphics{pic/factorial.pdf}}
+ \end{center}
+ \caption{階乗を求める CbC プログラムの流れ}
+ \label{fig:factorial}
+\end{figure}
+
+\section{メタ計算}
+% メタ計算の論文引用どうするかな…
+% メタプログラミング~系の本とかもいれていいのかな
+
+メタ計算(リフレクション)とは、対象とするレベルとメタなレベルを分離し、対象レベルでの推論や計算に
+関するメタな情報をメタレベルで明示的に記述し操作する。
+
+メタ計算(自己反映計算)\cite{weko_5056_1} とはプログラムを記述する際に通常の処理
+と分離し、他に記述しなければならない処理である。例えばプログラム実行時のメモリ管
+理やスレッド管理、資源管理等の計算がこれに当たる。
+
+
+
+% \section{Meta CodeGear とMeta DataGear}
+
+% CbC
+
+
+% \section{Interface}
+
+% Interface では使用する DataGear とそれに対する処理を行う CodeGear の集合をま
+% とめて定義する。
+
+% \lstinputlisting[label=interface, caption=CbCでのStack-Interfaceの記述] {src/interface.cbc}
+
+% DataGear に対して何らかの操作(API)を行う CodeGear とその
+% CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
+% として定義される。
+
+% Interface を記述することでデータ構造の api と DataGear の結びつきを高め、呼び出しが容易になる。
+
+
+\section{Context}
+CbC で DataGear を扱う際、 Context と呼ばれる接続可能な CodeGear、 DataGear のリ
+スト、Temporal DataGear のためのメモリ空間等を持っている Meta DataGearである。
+CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする必
+要がある。
+
+\section{stub CodeGear}
+CodeGear が必要とする DataGear を取り出す際、 Context を通す必要がある。
+しかし、 Context を直接扱えるようにするのは信頼性を損なう。そのため CbC では
+Context を通して必要なデータを取り出して次の Code Gear に接続する stub CodeGear
+を定義している。CodeGear は stub CodeGear を介してのみ必要な DataGear へアクセス
+することができる。 stub CodeGear は CodeGear 毎に生成され、次の CodeGear へと接
+続される。
+stub CodeGear は CodeGear の Meta CodeGear に当たる。
+
+
+\section{CbCによる Interface の記述と継続}
+
+CodeGear は通常の関数と比べ、細かく分割されるためメタ計算をより柔軟に記述でき
+る。 CodeGear 、 DataGear にはそれぞれメタレベルとして、 Meta CodeGear
+、 Meta DataGear が存在する。
+
+CbC で実装していくうちに、stub CodeGear の記述が煩雑になることが分かった。
+そのため 既存の実装を モジュールとして扱うため Interface を導入した。
+
+Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその
+CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
+として定義される。
+
+例として CbC による Stack Interface \ref{interface-define},
+\ref{interface}がある。Stack への push 操作に注目すると、
+実態は SingleLinkedStack の push であることが\ref{interface}で分
+かる。実際の SingleLinkedStack の push では Stack を指定する必要があるが、
+Interface で実装した Stack では push 先の Stack が stackImpl として扱
+われている。この stackImpl は$ Stack->push $で呼ばれた時の Stack と同じになる。
+これにより、 ユーザーは実行時に Stack を指定する必要がなくなる。
+
+このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出
+しが容易になる。
+
+\lstinputlisting[label=interface-define, caption=CbCでのStack-Interfaceの定義] {src/interface.cbc}
+
+\lstinputlisting[label=interface, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc}
+
+\section{定理証明支援器 Agda での証明}
+
+型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。
+Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ
+ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる
+。
+型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。
+
+\section{Agda の文法}
+
+Agda はインデントに意味を持つため、きちんと揃える必要がある。
+また、スペースの有無は厳格にチェックされる。
+なお、 \verb/--/ の後はコメントである。
+
+Agda のプログラムでは全てモジュール内部に記述されるため、まずはトップレベルにモ
+ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一になる。
+
+通常のモジュールをインポートする時は \verb/import/ キーワードを指定する。
+また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。
+モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードの後に
+関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠
+す場合は \verb/hiding/ キーワードを用いる。
+なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/opestack に対する操作を定義しており、n/ キーワードを使うことで展開できる。
+モジュールをインポートする例をリスト~\ref{agda-import}に示す。
+
+\lstinputlisting[label=agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda}
+
+Agda における型指定は $:$ を用いて行う。
+
+例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。
+
+データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
+\verb/data/キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
+例えば Bool 型を定義するとリスト~\ref{agda-bool}のようになる。
+Bool はコンストラクタ \verb/true/ と \verb/false/ を持つデータ型である。
+Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
+Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く。
+
+\lstinputlisting[label=agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}
+
+関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。
+関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。
+
+例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書
+ける。
+また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この
+時の型は \verb/A -> (A -> B)/のように考えられる。
+Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{agda-function}のようになる。
+
+\lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda}
+
+引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
+これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
+例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{agda-not}のようになる。
+
+\lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}
+
+パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
+例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
+なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
+例えばリスト~\ref{agda-pattern}の not は x には true しか入ることは無い。
+なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。
+
+\lstinputlisting[label=agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
+
+Agda にはラムダ式が存在している。ラムダ式とは関数内で生成できる無名の関数であり、
+\verb/\arg1 arg2 -> function body/ のように書くことができる。
+例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{agda-lambda}のようになる。
+関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。
+
+\lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}
+
+Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。
+スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
+例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{agda-where} のように書ける。
+これは \verb/f'/ と同様の動作をする。
+\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
+
+\lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}
+
+データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{agda-nat})。
+自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
+例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。
+
+\lstinputlisting[label=agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}
+
+自然数に対する演算は再帰関数として定義できる。
+例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{agda-plus}のように書ける。
+
+この二項演算子は中置関数として振る舞う。
+前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくと、関数を呼ぶ
+時にあたかも前置や後置演算子のように振る舞うことができる。
+例えば \verb/!_/ を定義すると \verb/! true/ のように利用でき、\verb/_~/ を定義すると \verb/false ~/ のように利用できる。
+
+また、Agda は再帰関数が停止するかを判別できる。
+この加算の二項演算子は左側がゼロに対しては明らかに停止する。
+左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
+もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。
+
+\lstinputlisting[label=agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}
+
+次に依存型について見ていく。
+依存型で最も基本的なものは関数型である。
+依存型を利用した関数は引数の型に依存して返す型を決定できる。
+なお、依存型の解決はモジュールのインポート時に行なわれる。
+
+Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つ x を受け取り、Bを返す。
+ここで B の中で x を扱っても良い。
+例えば任意の型に対する恒等関数はリスト~\ref{agda-id}のように書ける。
+
+\lstinputlisting[label=agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}
+
+この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
+実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。
+
+多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。
+Agda はこのような推論をサポートしており、推論可能な引数は省略できる。
+推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、変数を
+\verb/{}/ でくくることで表す。
+
+例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{agda-implicit-id}のようになる。
+この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。
+よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。
+なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
+適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。
+
+\lstinputlisting[label=agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}
+
+Agda のデータには C における構造体に相当するレコード型も存在する。
+定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
+例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{agda-record}のようになる。
+レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
+複数の値を列挙する際は \verb/;/ で区切る。
+
+\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}
+
+構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{agda-record-proj} 内2行目) 。
+なお、レコードにもパターンマッチが利用できる(リスト~\ref{agda-record-proj} 内5行目)。
+レコード内の値は \verb/record oldRecord {field = value ; ... }/ という構文を利用し更新することができる。
+Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{agda-record-proj}の 7,8行目のように書ける。
+
+\lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}
+
+
+% \section{Natural Deduction}
+% % Natural Deduction のお話。細かい規則は…書かなきゃいけないよね…
+% % いらない規則は省略しようと、少なくとも3段論法を証明できるだけ置く。。。？
+% % とりあえず証明に使えるやつは全部書いて必要あるやつを詳しく。
+
+% Natural Deduction (自然演繹)は Gentzen によって作られた論理及びその証明システムである。
+% % ~\cite{Girard:1989:PT:64805}。
+% 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。
+
+% Natural Deduction では次のように
+
+% \begin{eqnarray}
+%     \vdots \\ \nonumber
+%     A \\ \nonumber
+% \end{eqnarray}
+
+% と書いた時、命題Aを証明したことを意味する。証明は木構造で表わされ、葉の命題は仮
+% 定となる。
+
+% \begin{eqnarray}
+%     \label{exp:a_implies_b}
+%     A \\ \nonumber
+%     \vdots \\ \nonumber
+%     B \\ \nonumber
+% \end{eqnarray}
+
+% 式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。
+% この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。
+
+% ここで、推論規則により記号 $ \Rightarrow $ を導入する。
+
+% \begin{prooftree}
+%     \AxiomC{[$ A $]}
+%     \noLine
+%     \UnaryInfC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ B $ }
+%     \RightLabel{ $ \Rightarrow \mathcal{I} $}
+%     \UnaryInfC{$ A \Rightarrow B $}
+% \end{prooftree}
+
+% $ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
+% A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
+% このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
+% なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。
+
+% alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。
+% それを踏まえ、 natural deduction には以下のような規則が存在する。
+
+% \begin{itemize}
+%     \item Hypothesis
+
+%         仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。
+
+%         $ A $
+
+%     \item Introductions
+
+%         導入。証明された論理式に対して記号を導入することで新たな証明を導く。
+
+
+% \begin{prooftree}
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ A $ }
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ B $ }
+%     \RightLabel{ $ \land \mathcal{I} $}
+%     \BinaryInfC{$ A \land B $}
+%   \end{prooftree}
+
+% \begin{prooftree}
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ A $ }
+%     \RightLabel{ $ \lor 1 \mathcal{I} $}
+%     \UnaryInfC{$ A \lor B $}
+%   \end{prooftree}
+
+% \begin{prooftree}
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ B $ }
+%     \RightLabel{ $ \lor 2 \mathcal{I} $}
+%     \UnaryInfC{$ A \lor B $}
+%   \end{prooftree}
+
+% \begin{prooftree}
+%     \AxiomC{[$ A $]}
+%     \noLine
+%     \UnaryInfC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ B $ }
+%     \RightLabel{ $ \Rightarrow \mathcal{I} $}
+%     \UnaryInfC{$ A \Rightarrow B $}
+%   \end{prooftree}
+
+% \item Eliminations
+
+%     除去。ある論理記号で構成された証明から別の証明を導く。
+
+% \begin{prooftree}
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ A \land B $ }
+%     \RightLabel{ $ \land 1 \mathcal{E} $}
+%     \UnaryInfC{$ A $}
+%   \end{prooftree}
+
+% \begin{prooftree}
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ A \land B $ }
+%     \RightLabel{ $ \land 2 \mathcal{E} $}
+%     \UnaryInfC{$ B $}
+%   \end{prooftree}
+
+% \begin{prooftree}
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ A \lor B $ }
+
+%     \AxiomC{[$A$]}
+%     \noLine
+%     \UnaryInfC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ C $ }
+
+%     \AxiomC{[$B$]}
+%     \noLine
+%     \UnaryInfC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ C $ }
+
+%     \RightLabel{ $ \lor \mathcal{E} $}
+%     \TrinaryInfC{ $ C $ }
+%   \end{prooftree}
+
+% \begin{prooftree}
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ A $ }
+
+%     \AxiomC{ $ \vdots $}
+%     \noLine
+%     \UnaryInfC{ $ A \Rightarrow B $ }
+
+%     \RightLabel{ $ \Rightarrow \mathcal{E} $}
+%     \BinaryInfC{$ B $}
+%   \end{prooftree}
+
+% \end{itemize}
+
+% 記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。
+% natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。
+
+% それぞれの記号は以下のような意味を持つ
+% \begin{itemize}
+%     \item $ \land $
+%         conjunction。2つの命題が成り立つことを示す。
+%         $ A \land B $ と記述すると、 A かつ B と考えることができる。
+
+%     \item $ \lor $
+%         disjunction。2つの命題のうちどちらかが成り立つことを示す。
+%         $ A \lor B $ と記述すると、 A または B と考えることができる。
+
+%     \item $ \Rightarrow $
+%         implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
+%         $ A \Rightarrow B $ と記述すると、 A ならば B と考えることができる。
+% \end{itemize}
+
+% Natural Deduction では、これまでで説明したような規則を使い証明を行うことができる。
+
+% 例として Natural Deduction で三段論法の証明を行う。
+% このとき、「A は B であり、 B は C である。よって A は C である」 が証明するべき
+% 命題である。
+
+% この命題では 「A は B であり」と 「B は C である」の二つの小さい命題に分けられる。
+% この「A は B であり」から、AからBが導出できることが分かり、これは $ A \Rightarrow B $ と表せる。
+% また、「B は C である」から、BからCが導出できることが分かる。これも「A は B であ
+% り」の時と同様に $ B \Rightarrow C $ と表せる。
+
+
+% \begin{prooftree}
+%     \AxiomC{ $ [A] $ $_{(1)}$}
+%     \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
+%     \RightLabel{ $ \land 1 \mathcal{E} $ }
+%     \UnaryInfC{ $ (A \Rightarrow B) $ }
+%     \RightLabel{ $ \Rightarrow \mathcal{E} $}
+%     \BinaryInfC{ $ B $ }
+
+%     \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
+%     \RightLabel{ $ \land 2 \mathcal{E} $ }
+%     \UnaryInfC{ $ (B \Rightarrow C) $ }
+
+%     \RightLabel{ $ \Rightarrow \mathcal{E} $}
+%     \BinaryInfC{ $ C $ }
+%     \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$}
+%     \UnaryInfC{ $ A \Rightarrow C $}
+%     \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$}
+%     \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $}
+% \end{prooftree}
+
+
+% Natural Deductionでは次のような証明木になる。
+
+
+% \begin{figure}[htpb]
+%    \begin{center}
+%      \scalebox{0.25}{\includegraphics{pic/modus-ponens.pdf}}
+%    \end{center}
+%    \caption{自然演繹での三段論法の証明}
+%    \label{fig:modus-ponens}
+% \end{figure}
+
+% これにより自然演繹を使って三段論法が証明できた。
+% %%%%%%%%%%%%%%%%%%%%%%
+
+
+% \section{Natural Deduction と 型付き $ \lambda $  計算}
+
+% ここでは、 Natural Deduction と型付き$ \lambda $ 計算の対応を定義する。
+% 対応は以下の表\ref{table:curry-howard}のようになる。
+
+% \begin{center}
+%   \begin{table}[h]
+%     \scalebox{0.5}{
+%       \begin{tabular}{|c|c|} \hline
+%         Natural Deduction           & 型付き $ \lambda $ 計算  \\ \hline \hline
+%         $ A $                       & 型 A を持つ変数 x \\ \hline
+%         $ A \Rightarrow B $         & 型 A を取り型 B の変数を返す関数 f \\ \hline
+%         $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline
+%         $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline
+%         $ A \land B $               & 型 A と型 B の直積型 を持つ変数 x \\ \hline
+%         $ \land \mathcal{I} $       & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline
+%         $ \land 1 \mathcal{E} $     & 直積型からの型Aを取り出す射影fst \\ \hline
+%         $ \land 2 \mathcal{E} $     & 直積型からの型Bを取り出す射影snd \\ \hline
+%       \end{tabular}
+%     }
+%     \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)}
+%     \label{table:curry-howard}
+%   \end{table}
+% \end{center}
+
+% この対応をもとに Agda で型付き $\lambda$ 計算による証明を示す。
+% % ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。
+% ここでも先程 Natural Deduction で証明した三段論法を例とする。
+% % この三段論法は自然演繹では\ref{fig:modus-ponens}のようになっていた。
+
+% % \begin{figure}[htpb]
+% %    \begin{center}
+% %        \includegraphics{pic/modus-ponens.pdf}
+% %    \end{center}
+% %    \caption{自然演繹での三段論法の証明}
+% %    \label{fig:modus-ponens}
+% % \end{figure}
+
+% %McCこの証明木に対応するAgdaによる証明はリスト\ref{agda-moduse-ponens}のようになる。
+
+% \begin{lstlisting}[frame=lrbt,label=agda-moduse-ponens,caption={ Agda による
+%     三段論法の定義と証明}]
+% data _×_ (A B : Set) : Set where
+%   <_,_> : A → B → A × B
+
+% fst : {A B : Set} → A × B → A
+% fst < a , _ > = a
+
+% snd : {A B : Set} → A × B → B
+% snd < _ , b > = b
+
+
+% f : {A B C : Set} → ((A → B) × (B → C)) → (A → C)
+% f = λ p x → (snd p) ((fst p) x)
+% \end{lstlisting}
+
+% 自然演繹での三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。
+
+% ここで $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。
+% よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。
+% これをラムダ式で書くとリスト~\ref{agda-modus-ponens}のようになる。
+% 仮定 $ (A \rightarrow B) \times (B \rightarrow C) $  と仮定 A から A $ \rightarrow $ C を導いている。
+
+% 仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。
+% fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。
+% もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。
+% 得られた B を snd p に適用することで最終的に C が導ける。
+
+% \lstinputlisting[label=agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda}
+
+% このように Agda でも自然演繹と同様に証明を記述できる。
+
+\section{Agda での CodeGear 、 DataGear 、 継続の表現}
+Agda と CbC を対応して CodeGear、 DataGear、 継続を Agda で表現する。
+また、 Agda で継続を記述することで得た知見を示す。
+
+DataGear はレコード型で表現できるため、 Agda のレコード型をそのまま利用して定義
+していく。記述は~\ref{agda-ds}のようになる。
+
+\lstinputlisting[label=agda-ds, caption=Agda における DataGear の定義]
+{src/DataSegment.agda}
+
+CodeGear は DataGear を受け取って DataGear を返すという定義であるため、
+$ I \rightarrow O $ を内包する CodeGear 型のデータ型(~\ref{agda-cs})を定義する。
+
+\lstinputlisting[label=agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda}
+
+CodeGear 型を定義することで、 Agda での CodeGear の本体は Agda での関数そのもの
+と対応する。
+
+CodeGear の実行は CodeGear 型から関数本体を取り出し、レコード型を持つ値を適用す
+ることに相当する。
+
+CbC での軽量継続は
+
+\begin{itemize}
+ \item 次に実行する CodeGear を指定する
+ \item CodeGear に渡す DataGear を指定する
+ \item 現在実行している CodeGear から制御を指定された CodeGear へと移す
+\end{itemize}
+
+の機能を持っている。
+
+この機能を満たす関数はソースコード\ref{agda-goto} として定義されている。
+
+\lstinputlisting[label=agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda}
+
+goto は CodeGear よりも一つ Level が上の Meta CodeGear にあたり、次に実行する
+CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。
+
+
+\section{Agda での Stack、 Tree の実装}
+
+ここでは Agda での Stack 、 Tree の実装を示す。
+
+Stack の実装を以下のソースコード\ref{stack-impl}で示す。
+実装は SingleLinkedStack という名前で定義されている。
+定義されている API は push を例に残りは省略する。残りのの実装は付録に示す。 %~\
+
+\lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装] {src/AgdaStackImpl.agda}
+
+
+Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー
+タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。
+Maybe 型では値が存在する場合は Just 、 存在しない場合は　Nothing を返す。
+
+SingleLinkedStack 型では、この Element の top 部分のみを定義している。
+
+Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum
+の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい
+stack を返すというような実装をしている。
+
+Tree の実装(以下のソースコード\ref{tree-impl})は RedBlackTree という名前で定義されている。
+定義されている API は put 以後省略する。残りのの実装は付録に示す。 %~\
+
+\lstinputlisting[label=tree-impl, caption=Agdaにおける Tree の実装] {src/AgdaTreeImpl.agda}
+
+Node 型は key と value 、 Color と Node の rihgt 、 left の情報を持っている。
+Tree を構成する末端の Node は leafNode 型で定義されている。
+
+RedBlackTree 型は root の Node 情報と Tree に関する計算をする際に、そこまでの
+Node の経路情報を保持するための nodeStack と 比較するための compare を持っている。
+
+Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け
+取り、Tree の root に Node が存在しているかどうかで場合分けしている。
+Nothing が返ってきたときは RedBlackTree 型の tree 内に定義されている root に受け
+取ったキーと値を新しいノードとして追加する。
+Just が返ってきたときは root が存在するので、経路情報を積むために nodeStack を初
+期化し、受け取ったキーと値で新たなノードを作成した後、ノードが追加されるべき位置
+までキーの値を比べて新しい Tree を返すというような実装になっている。
+
+\section{Agda における Interface の実装}
+
+%% 書くこと
+% stack の Interface部分と redBlackTree の Interface部分。
+% interfaceとは?->cbcのとこに突っ込んでこっちは同様に〜で済ませたい
+
+Agda 側でも CbC 側と同様に interface を実装した。
+interface は record で列挙し、ソースコード~\ref{agda-interface}のように紐付けることができる。
+CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を記述している。
+
+例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface})を見る。
+Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側から
+interface を通して呼び出している。
+
+ここでの interface の型は Stack の record 内にある pushStack や popStack などで、
+実際に使われる Stack の操作は StackMethods にある push や popである。この push
+や pop は SingleLinkedStack で実装されている。
+
+% \lstinputlisting[label=agda-single-linked-stack, caption=Agda における Stack
+% の実装] {src/AgdaSingleLinkedStack.agda}
+
+\lstinputlisting[label=agda-interface, caption=Agda における Interface の定義] {src/AgdaInterface.agda}
+
+interface を通すことで、実際には Stack の push では stackImpl と何らかのデータ a を取
+り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更
+して継続を返す型に変わっている。
+
+また、 Tree でも interface を記述した。
+
+\lstinputlisting[label=agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda}
+
+interface を記述することによって、データを push する際に予め決まっている引数を省
+略することができた。
+また、 Agda で interface を記述することで CbC 側では意識していなかった型が、明確
+化された。
+
+% 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push
+% する可能性があったが、 pushStack では紐付けた Stack に push することになり
+
+\section{継続を使った Agda における Test , Debug}
+
+Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず
+しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動
+作をしているかを確認するために行なった手法を幾つか示す。
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+今回は実験中にソースコード\ref{agda-stack-test}のような Test を書いた。
+この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー
+タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の
+定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。
+
+\lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda}
+
+上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2
+を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動
+作が正しく行われていれば 04 は True を返し、 05 で記述された型通りに互いに等しくなる
+ため 05 が refl でコンパイルが通るようになる。
+今回は、 pop2 で取れた値を確認するため 03 の後に 031、 032 の二つの作成した。
+032 では 03 で扱っている値が Maybe であるため、 031 のような比較をする前に値が確
+実に存在していることを示す補題である。 032 を通すことで 031 では 2つの値があり、
+かつ$\mathbb{N}$型である事がわかる。 031 では直接取れた値が 2、 1 の順番で入って
+いるかを確認している。
+
+この Test でエラーが出なかったことから、 Stack に1、2の二つのデータを pushする
+と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分
+かる。
+
+
+また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ
+とができた。
+
+ここでの \$ は \( \) をまとめる糖衣構文で、 \$ が書かれた一行を\(\)でくくること
+ができる。
+% \ref{sintax}のようなコードを
+% \begin{lstlisting}[frame=lrbt,label=sintax,caption={ 通常の継続の
+%     コード}]
+
+% \end{lstlisting}
+
+% \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={ 糖衣構文
+%     を用いた継続のコード}]
+
+% \end{lstlisting}
+
+ソースコード~\ref{agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n
+(Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。
+また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ
+とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。
+
+ \lstinputlisting[label=agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda}
+
+今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ
+とが分かった。
+
+
+%getRedBlackTree の関数に
+% \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda}
+% Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう
+
+
+\section{Agda による Interface 部分を含めた Stack の部分的な証明}
+\label{agda-interface-stack}
+
+% Stack の仕様記述
+Stack や Tree の Interface を使い、 Agda で Interface を 経由した証明が可能であ
+ることを示す。
+ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。
+
+Stack の処理として様々な性質が存在する。例えば、
+
+\begin{itemize}
+ \item Stack に push した値は存在する
+ \item Stack に push した値は取り出すことができる
+ \item Stack に push した値を pop した時、その値は Stack から消える
+ \item どのような状態の Stack に値を push しても中に入っているデータの順序は変わらない
+ \item どのような状態の Stack でも、値を push した後 pop した値は直前に入れた値と一致する
+\end{itemize}
+
+などの性質がある。
+
+ここでは「どのような状態の Stack でも、値を push した後 pop した値は直前
+に入れた値と一致する」という性質を証明する。
+
+まず始めに不定状態の Stack を定義する。ソースコード~\ref{agda-in-some-state}
+の stackInSomeState 型は中身の分からない抽象的な Stack を表現している。ソースコー
+ド~\ref{agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を
+2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明す
+る。
+
+ \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda}
+
+この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー
+タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
+Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
+型に書かれている。
+
+この関数本体で返ってくる値は$ x \equiv x1 と y \equiv y1$　のため record でまと
+めて refl で推論が通る。
+これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
+のを受け取れることが証明できた。
+
+
+% \lstinputlisting[label=agda-Test, caption=]{src/AgdaStackTest.agda}
+
+\section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題}
+ここでは Binary Tree の性質の一部に対して証明を行う。
+Binary Tree の性質として挙げられるのは次のようなものである
+% 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる
+
+\begin{itemize}
+ \item Tree に対して Node を Put することができる。
+ \item Tree に Put された Node は Delete されるまでなくならない。
+ \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。
+ \item どのような状態の Tree に値を put しても Node と子の関係は保たれる
+ \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。
+\end{itemize}
+
+ここで証明する性質は
+
+${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。
+
+\lstinputlisting[label=agda-tree-proof, caption=Tree Interface の証
+明]{src/AgdaTreeProof.agda}
+
+この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree
+に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの
+である。
+
+しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した
+Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、
+key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が
+あった。今回この証明では Put した Node と Get した
+Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合
+同であることを示すことが困難であった。
+
+今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を
+行おうと考えている。
+
+\section{Hoare Logic}
+\label{hoare-logic}
+
+Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
+しさを推論する手法である。図\ref{fig:hoare}のように、 P を前状態(Pre Condition)
+、C を処理(Command) 、 Q を後状態(Post Condition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
+プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といった形で考える事ができる。
+
+\begin{figure}[htpb]
+ \begin{center}
+  \scalebox{0.3}[0.3]{\includegraphics{pic/hoare-logic.pdf}}
+ \end{center}
+ \caption{hoare logicの流れ}
+ \label{fig:hoare}
+\end{figure}
+
+
+このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
+動きをすることを証明することができる。
+
+この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表
+\ref{fig:cbc-hoare} のように表せるのではないか考えている。
+
+\begin{figure}[htpb]
+ \begin{center}
+  \scalebox{0.3}[0.3]{\includegraphics{pic/cbc-hoare.pdf}}
+ \end{center}
+ \caption{cbc と hoare logic}
+ \label{fig:cbc-hoare}
+\end{figure}
+
+この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
+Pre Condition が CodeGear に入力として与えられる Input DataGear、Command が
+CodeGear、 Post Condition を Output DataGear として当てはめることができると考えて
+いる。
+
+今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ Agda に
+当てはめ、幾つかの実装を証明していく。
+
+% Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
+% 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
+%%
+% 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
+% 入した。
+%%

 \nocite{*}
 \bibliographystyle{ipsjunsrt}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaBasics.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,1 @@
+module AgdaBasics where
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaBasics.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,1 @@
+module AgdaBasics where
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaBool.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+data Bool : Set where
+  true  : Bool
+  false : Bool
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaDebug.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,32 @@
+open import Level renaming (suc to succ ; zero to Zero )
+
+module AgdaDebug where
+
+open import stack
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat
+open import Function
+
+
+open SingleLinkedStack
+open Stack
+
+testStack07 : {m : Level } -> Maybe (Element ℕ)
+testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s -> pushSingleLinkedStack s 2 (\s -> top s))
+
+testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
+  $ \s -> pushSingleLinkedStack s 2
+  $ \s -> pushSingleLinkedStack s 3
+  $ \s -> pushSingleLinkedStack s 4
+  $ \s -> pushSingleLinkedStack s 5
+  $ \s -> top s
+
+
+testStack10 = pushStack emptySingleLinkedStack 1
+  $ \s -> pushStack 2
+  $ \s -> pushStack 3
+  $ \s -> pushStack 4
+  $ \s -> pushStack 5
+  $ \s -> top s
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaElem.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool
+elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs)
+elem         x []        = false
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaElemApply.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+listHas4 : Bool
+listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaFunction.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,2 @@
+f : Bool -> Bool
+f x = true
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaId.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,5 @@
+identity : (A : Set) -> A -> A
+identity A x = x
+
+identity-zero : Nat
+identity-zero = identity Nat zero
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaImplicitId.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,11 @@
+id : {A : Set} -> A -> A
+id x = x
+
+id-zero : Nat
+id-zero = id zero
+
+id' : {A : Set} -> A -> A
+id' {A} x = x
+
+id-true : Bool
+id-true = id {Bool} true
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaImport.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,6 @@
+import Data.Nat                  -- import module
+import Data.Bool as B            -- renamed module
+import Data.List using (head)    -- import Data.head function
+import Level renaming (suc to S) -- import module with rename suc to S
+import Data.String hiding (_++_) -- import module without _++_
+open import Data.List            -- import and expand Data.List
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaInstance.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,9 @@
+_==Nat_ : Nat -> Nat -> Bool
+zero    ==Nat zero    = true
+(suc n) ==Nat zero    = false
+zero    ==Nat (suc m) = false
+(suc n) ==Nat (suc m) = n ==Nat m
+
+instance
+  natHas== : Eq Nat
+  natHas== = record { _==_ = _==Nat_}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaInterface.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,35 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module AgdaInterface where
+
+data Maybe {n : Level } (a : Set n) : Set n where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+
+record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    push : stackImpl -> a -> (stackImpl -> t) -> t
+    pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
+    pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
+    get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
+    get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
+    clear : stackImpl -> (stackImpl -> t) -> t
+open StackMethods
+
+record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
+  field
+    stack : si
+    stackMethods : StackMethods {n} {m} a {t} si
+  pushStack :  a -> (Stack a si -> t) -> t
+  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
+  popStack : (Stack a si -> Maybe a  -> t) -> t
+  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  pop2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
+  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  getStack :  (Stack a si -> Maybe a  -> t) -> t
+  getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  get2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
+  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  clearStack : (Stack a si -> t) -> t
+  clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
+
+open Stack
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaInterface.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,35 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module AgdaInterface where
+
+data Maybe {n : Level } (a : Set n) : Set n where
+  Nothing : Maybe a
+  Just    : a @$\rightarrow$@ Maybe a
+
+record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    push : stackImpl @$\rightarrow$@ a @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop  : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    get  : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    get2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    clear : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+open StackMethods
+
+record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    stack : si
+    stackMethods : StackMethods {n} {m} a {t} si
+  pushStack :  a @$\rightarrow$@ (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
+  pushStack d next = push (stackMethods ) (stack ) d (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
+  popStack : (Stack a si @$\rightarrow$@ Maybe a  @$\rightarrow$@ t) @$\rightarrow$@ t
+  popStack next = pop (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  pop2Stack :  (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  getStack :  (Stack a si @$\rightarrow$@ Maybe a  @$\rightarrow$@ t) @$\rightarrow$@ t
+  getStack next = get (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  get2Stack :  (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  clearStack : (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
+  clearStack next = clear (stackMethods ) (stack ) (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
+
+open Stack
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaLambda.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,5 @@
+not-apply : Bool -> Bool
+not-apply = (\b -> not b)   -- use lambda
+
+not-apply : Bool -> Bool
+not-appy b = not b          -- not use lambda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaModusPonens.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,2 @@
+f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C)
+f = \p x -> (snd p) ((fst p) x)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaNPushNPop.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,13 @@
+n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-push {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m))
+
+n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-pop {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m))
+
+pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
+pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta
+                         ≡ M.exec (n-push {meta} n) meta
+  where
+    meta = id-meta cn ce s
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaNPushNPopProof.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,58 @@
+pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
+pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta
+                         ≡ M.exec (n-push n) meta
+  where
+    meta = id-meta cn ce s
+
+pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s
+pop-n-push zero cn ce s    = refl
+pop-n-push (suc n) cn ce s = begin
+  M.exec (M.csComp  (M.cs popOnce) (n-push  (suc (suc n)))) (id-meta cn ce s)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.cs popOnce) (M.csComp  (n-push  (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
+  ≡⟨ exec-comp (M.cs popOnce) (M.csComp  (n-push  (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩
+  M.exec (M.cs popOnce) (M.exec (M.csComp  (n-push  (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
+  ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩
+  M.exec (M.cs popOnce) (M.exec (n-push  (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
+  ≡⟨ refl ⟩
+  M.exec (M.cs popOnce) (M.exec (n-push  (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
+  ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩
+  M.exec (M.csComp  (M.cs popOnce) (n-push  (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩
+  M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  ≡⟨ refl ⟩
+  M.exec (n-push n) (pushOnce (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-push (suc n)) (id-meta cn ce s)
+  ∎
+
+
+
+n-push-pop-type : ℕ ->  ℕ  -> ℕ -> SingleLinkedStack ℕ -> Set₁
+n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta ≡ meta
+  where
+    meta = id-meta cn ce st
+
+n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s
+n-push-pop zero    cn ce s = refl
+n-push-pop (suc n) cn ce s = begin
+  M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s)
+  ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))  (id-meta cn ce s) ⟩
+  M.exec (M.cs (\m -> M.exec (n-pop  n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s)))
+  ≡⟨ refl ⟩
+  M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s)))
+  ≡⟨ cong (\x -> M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) ⟩
+  M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s))
+  ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩
+  M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
+  ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩
+  M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
+  ≡⟨ n-push-pop n cn ce s ⟩
+  id-meta cn ce s
+  ∎
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaNat.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+data Nat : Set where
+  zero : Nat
+  suc  : Nat -> Nat
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaNot.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+not : Bool -> Bool
+not  true = false
+not false = true
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaParameterizedModule.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,7 @@
+module Sort (A : Set) (_<_ : A -> A -> Bool) where
+sort : List A -> List A
+sort = -- 実装は省略 ...
+
+-- Parameterized Module により N.sort や B.sort が可能
+open import Sort Nat  Nat._<_  as N
+open import Sort Bool Bool._<_ as B
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaPattern.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+not : Bool -> Bool
+not false = true
+not x     = false
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaPlus.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+_+_ : Nat -> Nat -> Nat
+zero  + m = m
+suc n + m = suc (n + m)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaProduct.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+data _×_ (A B : Set) : Set where
+  <_,_> : A -> B -> A × B
+
+fst : {A B : Set} -> A × B -> A
+fst < a , _ > = a
+
+snd : {A B : Set} -> A × B -> B
+snd < _ , b > = b
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaProp.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,2 @@
+prop : Bool
+prop = true
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaPushPop.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,28 @@
+pushSingleLinkedStack : Meta -> Meta
+pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
+  where
+    n = Meta.nextCS m
+    s = Meta.stack  m
+    e = Context.element (Meta.context m)
+    push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
+    push s nothing  = s
+    push s (just x) = record {top = just (cons x (top s))}
+
+popSingleLinkedStack : Meta -> Meta
+popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
+  where
+    n = Meta.nextCS m
+    con  = Meta.context m
+    elem : Meta -> Maybe A
+    elem record {stack = record { top = (just (cons x _)) }} = just x
+    elem record {stack = record { top = nothing           }} = nothing
+    st : Meta -> SingleLinkedStack A
+    st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
+    st record {stack = record { top = nothing           }} = record {top = nothing}
+
+
+pushSingleLinkedStackCS : M.CodeSegment Meta Meta
+pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
+
+popSingleLinkedStackCS : M.CodeSegment Meta Meta
+popSingleLinkedStackCS = M.cs popSingleLinkedStack
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaPushPopProof.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,11 @@
+id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta
+id-meta n e s = record { context = record {n = n ; element = just e}
+                       ; nextCS = (N.cs id) ; stack = s}
+
+push-pop-type : ℕ -> ℕ  -> ℕ -> Element ℕ -> Set₁
+push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
+  where
+    meta = id-meta n e record {top = just (cons x (just s))}
+
+push-pop : (n e x : ℕ) -> (s : Element ℕ) ->  push-pop-type n e x s
+push-pop n e x s = refl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaRecord.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,7 @@
+record Point : Set where
+  field
+    x : Nat
+    y : Nat
+
+makePoint : Nat -> Nat -> Point
+makePoint a b = record { x = a ; y = b }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaRecordProj.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+getX : Point -> Nat
+getX p = Point.x p
+
+getY : Point -> Nat
+getY record { x = a ; y = b} = b
+
+xPlus5 : Point -> Point
+xPlus5 p = record p { x = (Point.x p) + 5}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaSingleLinkedStack.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,63 @@
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+push = pushSingleLinkedStack
+; pop  = popSingleLinkedStack
+; pop2 = pop2SingleLinkedStack
+; get  = getSingleLinkedStack
+; get2 = get2SingleLinkedStack
+; clear = clearSingleLinkedStack
+}
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+stack = emptySingleLinkedStack ;
+stackMethods = singleLinkedStackSpec
+}
+
+-- Implementation
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+
+pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
+  where
+    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    pop2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
+
+
+getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+getSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack (Just data1)
+  where
+    data1  = datum d
+
+get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
+  where
+    get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    get2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
+
+clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t
+clearSingleLinkedStack stack next = next (record {top = Nothing})
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaSingleLinkedStack.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,63 @@
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+push = pushSingleLinkedStack
+; pop  = popSingleLinkedStack
+; pop2 = pop2SingleLinkedStack
+; get  = getSingleLinkedStack
+; get2 = get2SingleLinkedStack
+; clear = clearSingleLinkedStack
+}
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+stack = emptySingleLinkedStack ;
+stackMethods = singleLinkedStackSpec
+}
+
+-- Implementation
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+popSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+
+pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
+  where
+    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
+
+
+getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+getSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack (Just data1)
+  where
+    data1  = datum d
+
+get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
+  where
+    get2SingleLinkedStack' : {n m : Level} {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+    get2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
+
+clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\rightarrow$@ t) @$\rightarrow$@ t
+clearSingleLinkedStack stack next = next (record {top = Nothing})
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStack.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,13 @@
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStackDS.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,17 @@
+record Context : Set where
+  field
+    -- fields for stack
+    element : Maybe A
+
+
+open import subtype Context as N
+
+record Meta  : Set₁ where
+  field
+    -- context as set of data segments
+    context : Context
+    stack   : SingleLinkedStack A
+    nextCS  : N.CodeSegment Context Context
+
+open import subtype Meta as M
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStackImpl.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,28 @@
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+  top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+-- Basic stack implementations are specifications of a Stack
+
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                           push = pushSingleLinkedStack
+                         ; pop  = popSingleLinkedStack
+                         ; pop2 = pop2SingleLinkedStack
+                         ; get  = getSingleLinkedStack
+                         ; get2 = get2SingleLinkedStack
+                         ; clear = clearSingleLinkedStack
+                         }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                        stack = emptySingleLinkedStack ;
+                        tackMethods = singleLinkedStackSpec
+                        }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStackImpl.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,28 @@
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+  top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} $\rightarrow$ SingleLinkedStack Data $\rightarrow$ Data $\rightarrow$ (Code : SingleLinkedStack Data $\rightarrow$ t) $\rightarrow$ t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+-- Basic stack implementations are specifications of a Stack
+
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} $\rightarrow$ StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                               }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} $\rightarrow$ Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                            stack = emptySingleLinkedStack ;
+                            stackMethods = singleLinkedStackSpec
+                          }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStackSomeState.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,6 @@
+stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+
+push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStackSomeState.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,6 @@
+stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) @$\rightarrow$@ Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+
+push@$\rightarrow$@push@$\rightarrow$@pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) @$\rightarrow$@ pushStack (stackInSomeState s)  x (\s1 @$\rightarrow$@ pushStack s1 y (\s2 @$\rightarrow$@ pop2Stack s2 (\s3 y1 x1 @$\rightarrow$@
+   (Just x @$\equiv$@ x1) ∧ (Just y @$\equiv$@ y1))))
+push@$\rightarrow$@push@$\rightarrow$@pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStackTest.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,37 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module AgdaStackTest where
+
+open import stack
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat
+open import Function
+
+
+open SingleLinkedStack
+open Stack
+
+
+-- after push 1 and 2, pop2 get 1 and 2
+
+testStack02 : {m : Level } ->  ( Stack  ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
+testStack02 cs = pushStack createSingleLinkedStack 1 (\s -> pushStack s 2 cs)
+
+
+testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
+testStack031 2 1 = True
+testStack031 _ _ = False
+
+testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
+testStack032  (Just d1) (Just d2) = testStack031 d1 d2
+testStack032  _ _ = False
+
+testStack03 : {m : Level } -> Stack  ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
+testStack03 s cs = pop2Stack s (\s d1 d2 -> cs d1 d2 )
+
+testStack04 : Bool
+testStack04 = testStack02 (\s -> testStack03 s testStack032)
+
+testStack05 : testStack04 ≡ True
+testStack05 = refl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaStackTest.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,22 @@
+-- after push 1 and 2, pop2 get 1 and 2
+
+testStack02 : {m : Level } @$\rightarrow$@  ( Stack  @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m}
+testStack02 cs = pushStack createSingleLinkedStack 1 (\s @$\rightarrow$@ pushStack s 2 cs)
+
+
+testStack031 : (d1 d2 : $\mathbb{N}$ ) @$\rightarrow$@ Bool {Zero}
+testStack031 2 1 = True
+testStack031 _ _ = False
+
+testStack032 : (d1 d2 : Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {Zero}
+testStack032  (Just d1) (Just d2) = testStack031 d1 d2
+testStack032  _ _ = False
+
+testStack03 : {m : Level } @$\rightarrow$@ Stack  @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ ((Maybe @$\mathbb{N}$@) @$\rightarrow$@ (Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m}
+testStack03 s cs = pop2Stack s (\s d1 d2 @$\rightarrow$@ cs d1 d2 )
+
+testStack04 : Bool
+testStack04 = testStack02 (\s @$\rightarrow$@ testStack03 s testStack032)
+
+testStack05 : testStack04 @$\equiv$@ True
+testStack05 = refl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTree.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,17 @@
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    getImpl  : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+    putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
+    getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+
+open Tree
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeDebug.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,15 @@
+test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
+  $ \t -> putTree1 t 2 2
+  $ \t -> putTree1 t 3 3
+  $ \t -> putTree1 t 4 4
+  $ \t -> getRedBlackTree t 4
+  $ \t x -> x
+
+-- Just
+-- (record
+-- { key = 4
+-- ; value = 4
+-- ; right = Nothing
+-- ; left = Nothing
+-- ; color = Red
+-- })
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeDebug.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,15 @@
+test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1
+  $ \t @$\rightarrow$@ putTree1 t 2 2
+  $ \t @$\rightarrow$@ putTree1 t 3 3
+  $ \t @$\rightarrow$@ putTree1 t 4 4
+  $ \t @$\rightarrow$@ getRedBlackTree t 4
+  $ \t x @$\rightarrow$@ x
+
+-- Just
+-- (record
+-- { key = 4
+-- ; value = 4
+-- ; right = Nothing
+-- ; left = Nothing
+-- ; color = Red
+-- })
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeDebugReturnNode4.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,16 @@
+test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
+$ \t -> putTree1 t 2 2
+$ \t -> putTree1 t 3 3
+$ \t -> putTree1 t 4 4
+$ \t -> getRedBlackTree t 4
+$ \t x -> x
+
+-- C-c C-n test31 return
+  -- Just
+  -- (record
+  -- { key = 4
+  -- ; value = 4
+  -- ; right = Nothing
+  -- ; left = Nothing
+  -- ; color = Red
+  -- })
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeImpl.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,33 @@
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+  field
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
+leafNode k1 value = record {
+  key   = k1 ;
+  value = value ;
+  right = Nothing ;
+  left  = Nothing ;
+  color = Red
+  }
+open leafNode
+
+record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
+  field
+    root : Maybe (Node a k)
+    nodeStack : SingleLinkedStack  (Node a k)
+    compare : k -> k -> CompareResult {n}
+open RedBlackTree
+
+putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))
+
+-- 以下省略
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeImpl.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,47 @@
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    getImpl  : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+    putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
+    getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+open Tree
+
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+  field
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+leafNode : {n : Level } {a k : Set n}  @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k
+leafNode k1 value = record {
+  key   = k1 ;
+  value = value ;
+  right = Nothing ;
+  left  = Nothing ;
+  color = Red
+  }
+record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where
+  field
+    root : Maybe (Node a k)
+    nodeStack : SingleLinkedStack  (Node a k)
+    compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n}
+open RedBlackTree
+
+putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
+putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next))
+
+-- 以下省略
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeProof.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,34 @@
+redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
+redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
+
+putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
+         -> (k : ℕ) (x : ℕ)
+         -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
+         (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x  ≡ True))
+putTest1 n k x with n
+...  | Just n1 = lemma2 ( record { top = Nothing } )
+   where
+     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
+         GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
+     lemma2 s with compare2 k (key n1)
+     ... |  EQ = lemma3 {!!}
+        where
+           lemma3 : compare2 k (key n1) ≡  EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
+               } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y  } ) k ( \ t x1 -> check2 x1 x  ≡ True)
+           lemma3 eq with compare2 x x | putTest1Lemma2 x
+           ... | EQ | refl with compare2 k (key n1)  | eq
+           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
+           ...                    | EQ | refl = refl
+     ... |  GT = {!!}
+     ... |  LT = {!!}
+
+...  | Nothing =  lemma1
+   where
+     lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red
+        } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k
+        ( \ t x1 -> check2 x1 x  ≡ True)
+     lemma1 with compare2 k k | putTest1Lemma2 k
+     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
+     ...              | EQ | refl = refl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeProof.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,34 @@
+redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@
+redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
+
+putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@))
+         @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@)
+         @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x
+         (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True))
+putTest1 n k x with n
+...  | Just n1 = lemma2 ( record { top = Nothing } )
+   where
+     lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
+         GetRedBlackTree.checkNode t k (λ t@$\text{1}$@ x1 → check2 x1 x @$\equiv$@ True) (root t))
+     lemma2 s with compare2 k (key n1)
+     ... |  EQ = lemma3 {!!}
+        where
+           lemma3 : compare2 k (key n1) @$\equiv$@  EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record {  root = Just ( record {
+               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
+               } ) ; nodeStack = s ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y  } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True)
+           lemma3 eq with compare2 x x | putTest1Lemma2 x
+           ... | EQ | refl with compare2 k (key n1)  | eq
+           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
+           ...                    | EQ | refl = refl
+     ... |  GT = {!!}
+     ... |  LT = {!!}
+
+...  | Nothing =  lemma1
+   where
+     lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record {  root = Just ( record {
+               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red
+        } ) ; nodeStack = record { top = Nothing } ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y  } ) k
+        ( \ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True)
+     lemma1 with compare2 k k | putTest1Lemma2 k
+     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
+     ...              | EQ | refl = refl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeTest.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,6 @@
+test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
+$ \t -> putTree1 t 2 2
+$ \t -> putTree1 t 3 3
+$ \t -> putTree1 t 4 4
+$ \t -> getRedBlackTree t 4
+$ \t x -> x
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTypeClass.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+record Eq (A : Set) : Set where
+  field
+    _==_ : A -> A -> Bool
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaWhere.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,7 @@
+f : Int -> Int -> Int
+f a b c = (t a) + (t b) + (t c)
+  where
+    t x = x + x + x
+
+f' : Int -> Int -> Int
+f' a b c = (a + a + a) + (b + b + b) + (c + c + c)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/CodeSegment.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,2 @@
+data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l ⊔ l1 ⊔ l2) where
+  cs : (I -> O) -> CodeSegment I O
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/CodeSegment.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,2 @@
+data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l @$\sqcup$@ l1 @$\sqcup$@ l2) where
+  cs : (I @$\rightarrow$@ O) @$\rightarrow$@ CodeSegment I O
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/CodeSegments.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,12 @@
+cs2 : CodeSegment ds1 ds1
+cs2 = cs id
+
+cs1 : CodeSegment ds1 ds1
+cs1 = cs (\d -> goto cs2 d)
+
+cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+main : ds1
+main = goto cs0 (record {a = 100 ; b = 50})
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/DataSegment.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
+record ds1 : Set where
+  field
+    c : Int
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/DataSegment.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
+record ds1 : Set where
+  field
+    c : Int
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/Equiv.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,1 @@
+data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/Exec.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,5 @@
+exec : {l1 l2 : Level} {I : Set l1} {O : Set l2}
+       {{_ : DataSegment I}} {{_ : DataSegment O}}
+       -> CodeSegment I O -> Context -> Context
+exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/Goto.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,4 @@
+goto : {l1 l2 : Level} {I : Set l1} {O : Set l2}
+   -> CodeSegment I O -> I -> O
+goto (cs b) i = b i
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/Goto.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,4 @@
+goto : {l1 l2 : Level} {I : Set l1} {O : Set l2}
+   @$\rightarrow$@ CodeSegment I O @$\rightarrow$@ I @$\rightarrow$@ O
+goto (cs b) i = b i
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/Maybe.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,3 @@
+data Maybe {a} (A : Set a) : Set a where
+  just    : (x : A) -> Maybe A
+  nothing : Maybe A
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/MetaCodeSegment.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,4 @@
+data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where
+  cs : {{_ : DataSegment A}} {{_ : DataSegment B}}
+        -> (A -> B) -> CodeSegment A B
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/MetaDataSegment.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,7 @@
+module subtype {l : Level} (Context : Set l) where
+
+record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
+  field
+    get : Context -> A
+    set : Context -> A -> Context
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/MetaMetaCodeSegment.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,29 @@
+-- meta level
+liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
+liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
+
+liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
+liftMeta (N.cs f) = M.cs f
+
+gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta
+gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)})
+
+push : M.CodeSegment Meta Meta
+push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)}))
+
+-- normal level
+
+cs2 : N.CodeSegment ds1 ds1
+cs2 = N.cs id
+
+cs1 : N.CodeSegment ds1 ds1
+cs1 = N.cs (\d -> N.goto cs2 d)
+
+cs0 : N.CodeSegment ds0 ds1
+cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+-- meta level (with extended normal)
+main : Meta
+main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
+-- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/MetaMetaDataSegment.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,12 @@
+-- 上で各 DataSegement の定義を行なっているとする
+open import subtype Context as N    -- Meta Datasegment を定義
+
+-- Meta DataSegment を持つ Meta Meta DataSegment を定義できる
+record Meta : Set where
+  field
+    context : Context
+    c'      : Int
+    next    : N.CodeSegment Context Context
+
+open import subtype Meta as M
+-- 以下よりメタメタレベルのプログラムを記述できる
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/Nat.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,5 @@
+module nat where
+
+data Nat : Set where
+  O : Nat
+  S : Nat -> Nat
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/NatAdd.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,6 @@
+open import nat
+module nat_add where
+
+_+_ : Nat -> Nat -> Nat
+O + m     = m
+(S n) + m = S (n + m)
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/NatAddSym.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,12 @@
+open import Relation.Binary.PropositionalEquality
+open import nat
+open import nat_add
+open ≡-Reasoning
+
+module nat_add_sym where
+
+addSym : (n m : Nat) -> n + m ≡ m + n
+addSym O       O   = refl
+addSym O    (S m)  = cong S (addSym O m)
+addSym (S n)   O   = cong S (addSym n O)
+addSym (S n) (S m) = {!!} -- 後述
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/PushPopType.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,9 @@
+pushOnce : Meta -> Meta
+pushOnce m = M.exec pushSingleLinkedStackCS m
+
+popOnce : Meta -> Meta
+popOnce m = M.exec popSingleLinkedStackCS m
+
+push-pop-type : Meta -> Set₁
+push-pop-type meta =
+    M.exec (M.csComp  (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/Reasoning.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,21 @@
+open import Relation.Binary.PropositionalEquality
+open import nat
+open import nat_add
+open ≡-Reasoning
+
+module nat_add_sym_reasoning where
+
+addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m)
+addToRight O m     = refl
+addToRight (S n) m = cong S (addToRight n m)
+
+addSym : (n m : Nat) -> n + m ≡ m + n
+addSym O       O   = refl
+addSym O    (S m)  = cong S (addSym O m)
+addSym (S n)   O   = cong S (addSym n O)
+addSym (S n) (S m) = begin
+  (S n) + (S m)  ≡⟨ refl ⟩
+  S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
+  S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
+  S (m + S n)    ≡⟨ refl ⟩
+  (S m) + (S n)  ∎
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/RedBlackTree.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,231 @@
+module RedBlackTree where
+
+open import stack
+open import Level hiding (zero)
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
+    getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+  putTree : a -> (Tree treeImpl -> t) -> t
+  putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
+  getTree : (Tree treeImpl -> Maybe a -> t) -> t
+  getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+
+open Tree
+
+data Color {n : Level } : Set n where
+  Red   : Color
+  Black : Color
+
+data CompareResult {n : Level } : Set n where
+  LT : CompareResult
+  GT : CompareResult
+  EQ : CompareResult
+
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+  field
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
+  field
+    root : Maybe (Node a k)
+    nodeStack : SingleLinkedStack  (Node a k)
+    compare : k -> k -> CompareResult {n}
+
+open RedBlackTree
+
+open SingleLinkedStack
+
+--
+-- put new node at parent node, and rebuild tree to the top
+--
+{-# TERMINATING #-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
+replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) ->  Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s (
+      \s parent -> replaceNode1 s parent)
+        where
+          replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t
+          replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } )
+          replaceNode1 s (Just n1) with compare tree (key n1) (key n0)
+          ... | EQ =  replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next
+          ... | GT =  replaceNode tree s ( record n1 { left = Just n0 } ) next
+          ... | LT =  replaceNode tree s ( record n1 { right = Just n0 } ) next
+
+
+rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
+  (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
+rotateRight {n} {m} {t} {a} {k}  tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateRight1 tree s n0 parent rotateNext)
+  where
+        rotateRight1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k)  -> Maybe (Node a k) -> Maybe (Node a k) ->
+          (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k)  -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
+        rotateRight1 {n} {m} {t} {a} {k}  tree s n0 parent rotateNext with n0
+        ... | Nothing  = rotateNext tree s Nothing n0
+        ... | Just n1 with parent
+        ...           | Nothing = rotateNext tree s (Just n1 ) n0
+        ...           | Just parent1 with left parent1
+        ...                | Nothing = rotateNext tree s (Just n1) Nothing
+        ...                | Just leftParent with compare tree (key n1) (key leftParent)
+        ...                                    | EQ = rotateNext tree s (Just n1) parent
+        ...                                    | _ = rotateNext tree s (Just n1) parent
+
+
+rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
+  (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) ->  t) -> t
+rotateLeft {n} {m} {t} {a} {k}  tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 -> rotateLeft1 tree s n0 parent rotateNext)
+  where
+        rotateLeft1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) ->
+          (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node  a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t) -> t
+        rotateLeft1 {n} {m} {t} {a} {k}  tree s n0 parent rotateNext with n0
+        ... | Nothing  = rotateNext tree s Nothing n0
+        ... | Just n1 with parent
+        ...           | Nothing = rotateNext tree s (Just n1) Nothing
+        ...           | Just parent1 with right parent1
+        ...                | Nothing = rotateNext tree s (Just n1) Nothing
+        ...                | Just rightParent with compare tree (key n1) (key rightParent)
+        ...                                    | EQ = rotateNext tree s (Just n1) parent
+        ...                                    | _ = rotateNext tree s (Just n1) parent
+
+{-# TERMINATING #-}
+insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+insertCase5 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent -> insertCase51 tree s n0 parent grandParent next)
+  where
+    insertCase51 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+    insertCase51 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next with n0
+    ...     | Nothing = next tree
+    ...     | Just n1  with  parent | grandParent
+    ...                 | Nothing | _  = next tree
+    ...                 | _ | Nothing  = next tree
+    ...                 | Just parent1 | Just grandParent1 with left parent1 | left grandParent1
+    ...                                                     | Nothing | _  = next tree
+    ...                                                     | _ | Nothing  = next tree
+    ...                                                     | Just leftParent1 | Just leftGrandParent1
+      with compare tree (key n1) (key leftParent1) | compare tree (key leftParent1) (key leftGrandParent1)
+    ...     | EQ | EQ = rotateRight tree s n0 parent
+                 (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next)
+    ...     | _ | _ = rotateLeft tree s n0 parent
+                 (\ tree s n0 parent -> insertCase5 tree s n0 parent1 grandParent1 next)
+
+insertCase4 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+insertCase4 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next
+       with  (right parent) | (left grandParent)
+...    | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next
+...    | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next
+...    | Just rightParent | Just leftGrandParent with compare tree (key n0) (key rightParent) | compare tree (key parent) (key leftGrandParent)
+...                                              | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateLeft tree s (left n0) (Just grandParent)
+   (\ tree s n0 parent -> insertCase5 tree s n0 rightParent grandParent next))
+...                                              | _ | _  = insertCase41 tree s n0 parent grandParent next
+  where
+    insertCase41 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+    insertCase41 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next
+                 with  (left parent) | (right grandParent)
+    ...    | Nothing | _ = insertCase5 tree s (Just n0) parent grandParent next
+    ...    | _ | Nothing = insertCase5 tree s (Just n0) parent grandParent next
+    ...    | Just leftParent | Just rightGrandParent with compare tree (key n0) (key leftParent) | compare tree (key parent) (key rightGrandParent)
+    ...                                              | EQ | EQ = popSingleLinkedStack s (\ s n1 -> rotateRight tree s (right n0) (Just grandParent)
+       (\ tree s n0 parent -> insertCase5 tree s n0 leftParent grandParent next))
+    ...                                              | _ | _  = insertCase5 tree s (Just n0) parent grandParent next
+
+colorNode : {n : Level } {a k : Set n}  -> Node a k -> Color  -> Node a k
+colorNode old c = record old { color = c }
+
+{-# TERMINATING #-}
+insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+insertNode {n} {m} {t} {a} {k}  tree s n0 next = get2SingleLinkedStack s (insertCase1 n0)
+   where
+    insertCase1 : Node a k -> SingleLinkedStack (Node a k) -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allow mutual recursion
+          -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
+    insertCase3 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t
+    insertCase3 s n0 parent grandParent with left grandParent | right grandParent
+    ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
+    ... | Nothing | Just uncle  = insertCase4 tree s n0 parent grandParent next
+    ... | Just uncle | _  with compare tree ( key uncle ) ( key parent )
+    ...                   | EQ =  insertCase4 tree s n0 parent grandParent next
+    ...                   | _ with color uncle
+    ...                           | Red = pop2SingleLinkedStack s ( \s p0 p1 -> insertCase1  (
+           record grandParent { color = Red ; left = Just ( record parent { color = Black } )  ; right = Just ( record uncle { color = Black } ) }) s p0 p1 )
+    ...                           | Black = insertCase4 tree s n0 parent grandParent next
+    insertCase2 : SingleLinkedStack (Node a k) -> Node a k -> Node a k -> Node a k -> t
+    insertCase2 s n0 parent grandParent with color parent
+    ... | Black = replaceNode tree s n0 next
+    ... | Red =   insertCase3 s n0 parent grandParent
+    insertCase1 n0 s Nothing Nothing = next tree
+    insertCase1 n0 s Nothing (Just grandParent) = next tree
+    insertCase1 n0 s (Just parent) Nothing = replaceNode tree s (colorNode n0 Black) next
+    insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
+
+----
+-- find node potition to insert or to delete, the path will be in the stack
+--
+findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
+findNode {n} {m} {a} {k}  {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1)
+  where
+    findNode2 : SingleLinkedStack (Node a k) -> (Maybe (Node a k)) -> t
+    findNode2 s Nothing = next tree s n0
+    findNode2 s (Just n) = findNode tree s n0 n next
+    findNode1 : SingleLinkedStack (Node a k) -> (Node a k)  -> t
+    findNode1 s n1 with (compare tree (key n0) (key n1))
+    ...                                | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n0 } ) )
+    ...                                | GT = findNode2 s (right n1)
+    ...                                | LT = findNode2 s (left n1)
+
+
+leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
+leafNode k1 value = record {
+    key   = k1 ;
+    value = value ;
+    right = Nothing ;
+    left  = Nothing ;
+    color = Red
+  }
+
+putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))
+
+getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> (RedBlackTree {n} {m} {t} a k -> (Maybe (Node a k)) -> t) -> t
+getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
+  module GetRedBlackTree where                     -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html
+    search : Node a k -> t
+    checkNode : Maybe (Node a k) -> t
+    checkNode Nothing = cs tree Nothing
+    checkNode (Just n) = search n
+    search n with compare tree k1 (key n)
+    search n | LT = checkNode (left n)
+    search n | GT = checkNode (right n)
+    search n | EQ = cs tree (Just n)
+
+open import Data.Nat hiding (compare)
+
+compareℕ :  ℕ → ℕ → CompareResult {Level.zero}
+compareℕ x y with Data.Nat.compare x y
+... | less _ _ = LT
+... | equal _ = EQ
+... | greater _ _ = GT
+
+compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
+compare2 zero zero = EQ
+compare2 (suc _) zero = GT
+compare2  zero (suc _) = LT
+compare2  (suc x) (suc y) = compare2 x y
+
+
+createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
+createEmptyRedBlackTreeℕ  {m} a {t} = record {
+        root = Nothing
+     ;  nodeStack = emptySingleLinkedStack
+     ;  compare = compare2
+   }
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/SingleLinkedStack.cbc	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,110 @@
+#include "../context.h"
+#include "../origin_cs.h"
+#include <stdio.h>
+
+// typedef struct SingleLinkedStack {
+//     struct Element* top;
+// } SingleLinkedStack;
+
+Stack* createSingleLinkedStack(struct Context* context) {
+    struct Stack* stack = new Stack();
+    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
+    stack->stack = (union Data*)singleLinkedStack;
+    singleLinkedStack->top = NULL;
+    stack->push = C_pushSingleLinkedStack;
+    stack->pop  = C_popSingleLinkedStack;
+    stack->pop2  = C_pop2SingleLinkedStack;
+    stack->get  = C_getSingleLinkedStack;
+    stack->get2  = C_get2SingleLinkedStack;
+    stack->isEmpty = C_isEmptySingleLinkedStack;
+    stack->clear = C_clearSingleLinkedStack;
+    return stack;
+}
+
+void printStack1(union Data* data) {
+    struct Node* node = &data->Element.data->Node;
+    if (node == NULL) {
+        printf("NULL");
+    } else {
+        printf("key = %d ,", node->key);
+        printStack1((union Data*)data->Element.next);
+    }
+}
+
+void printStack(union Data* data) {
+    printStack1(data);
+    printf("\n");
+}
+
+__code clearSingleLinkedStack(struct SingleLinkedStack* stack,__code next(...)) {
+    stack->top = NULL;
+    goto next(...);
+}
+
+__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) {
+    Element* element = new Element();
+    element->next = stack->top;
+    element->data = data;
+    stack->top = element;
+    goto next(...);
+}
+
+__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) {
+    if (stack->top) {
+        data = stack->top->data;
+        stack->top = stack->top->next;
+    } else {
+        data = NULL;
+    }
+    goto next(data, ...);
+}
+
+__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) {
+    if (stack->top) {
+        data = stack->top->data;
+        stack->top = stack->top->next;
+    } else {
+        data = NULL;
+    }
+    if (stack->top) {
+        data1 = stack->top->data;
+        stack->top = stack->top->next;
+    } else {
+        data1 = NULL;
+    }
+    goto next(data, data1, ...);
+}
+
+
+__code getSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) {
+    if (stack->top)
+        data = stack->top->data;
+    else
+        data = NULL;
+    goto next(data, ...);
+}
+
+__code get2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) {
+    if (stack->top) {
+        data = stack->top->data;
+        if (stack->top->next) {
+            data1 = stack->top->next->data;
+        } else {
+            data1 = NULL;
+        }
+    } else {
+        data = NULL;
+        data1 = NULL;
+    }
+    goto next(data, data1, ...);
+}
+
+__code isEmptySingleLinkedStack(struct SingleLinkedStack* stack, __code next(...), __code whenEmpty(...)) {
+    if (stack->top)
+        goto next(...);
+    else
+        goto whenEmpty(...);
+}
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/ThreePlusOne.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,8 @@
+open import Relation.Binary.PropositionalEquality
+open import nat
+open import nat_add
+
+module three_plus_one where
+
+3+1 : (S (S (S O)))  +  (S O) ≡ (S (S (S (S O))))
+3+1 = refl
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/atton-master-meta-sample.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,77 @@
+module atton-master-meta-sample where
+
+open import Data.Nat
+open import Data.Unit
+open import Function
+Int = ℕ
+
+record Context : Set where
+  field
+    a  : Int
+    b  : Int
+    c  : Int
+
+open import subtype Context as N
+
+record Meta : Set where
+  field
+    context : Context
+    c'      : Int
+    next    : N.CodeSegment Context Context
+
+open import subtype Meta as M
+
+instance
+  _ : N.DataSegment Context
+  _ = record { get = id ; set = (\_ c -> c) }
+  _ : M.DataSegment Context
+  _ = record { get = (\m -> Meta.context m)  ;
+               set = (\m c -> record m {context = c}) }
+  _ : M.DataSegment Meta
+  _ = record { get = id ; set = (\_ m -> m) }
+
+
+liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
+liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
+
+liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
+liftMeta (N.cs f) = M.cs f
+
+
+gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta
+gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)})
+
+push : M.CodeSegment Meta Meta
+push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)}))
+
+
+record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
+record ds1 : Set where
+  field
+    c : Int
+
+instance
+  _ : N.DataSegment ds0
+  _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)})
+             ; get = (\c ->   record { a = (Context.a c) ; b = (Context.b c)})}
+  _ : N.DataSegment ds1
+  _ = record { set = (\c d -> record c {c = (ds1.c d)})
+             ; get = (\c ->   record { c = (Context.c c)})}
+
+cs2 : N.CodeSegment ds1 ds1
+cs2 = N.cs id
+
+cs1 : N.CodeSegment ds1 ds1
+cs1 = N.cs (\d -> N.goto cs2 d)
+
+cs0 : N.CodeSegment ds0 ds1
+cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+
+main : Meta
+main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
+-- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/atton-master-sample.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,46 @@
+module atton-master-sample where
+
+open import Data.Nat
+open import Data.Unit
+open import Function
+Int = ℕ
+
+record Context : Set where
+  field
+    a : Int
+    b : Int
+    c : Int
+
+
+open import subtype Context
+
+
+
+record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
+record ds1 : Set where
+  field
+    c : Int
+
+instance
+  _ : DataSegment ds0
+  _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)})
+             ; get = (\c ->   record { a = (Context.a c) ; b = (Context.b c)})}
+  _ : DataSegment ds1
+  _ = record { set = (\c d -> record c {c = (ds1.c d)})
+             ; get = (\c ->   record { c = (Context.c c)})}
+
+cs2 : CodeSegment ds1 ds1
+cs2 = cs id
+
+cs1 : CodeSegment ds1 ds1
+cs1 = cs (\d -> goto cs2 d)
+
+cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+main : ds1
+main = goto cs0 (record {a = 100 ; b = 50})
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/factrial.cbc	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,29 @@
+__code print_factorial(int prod)
+{
+  printf("factorial = %d\n", prod);
+  exit(0);
+}
+
+__code factorial0(int prod, int x)
+{
+  if (x >= 1) {
+    goto factorial0(prod*x, x-1);
+  } else {
+    goto print_factorial(prod);
+  }
+
+}
+
+__code factorial(int x)
+{
+  goto factorial0(1, x);
+}
+
+int main(int argc, char **argv)
+{
+  int i;
+  i = atoi(argv[1]);
+
+  goto factorial(i);
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/goto.cbc	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,7 @@
+__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
+__code cs1(int c){
+  goto cs2(c);
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/interface.cbc	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,12 @@
+typedef struct Stack<Type, Impl>{
+        union Data* stack;
+        union Data* data;
+        union Data* data1;
+
+        __code whenEmpty(...);
+        __code clear(Impl* stack,__code next(...));
+        __code push(Impl* stack,Type* data, __code next(...));
+        __code pop(Impl* stack, __code next(Type* data, ...));
+        __code get(Impl* stack, __code next(Type* data, ...));
+        __code next(...);
+} Stack;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/redBlackTreeTest.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,196 @@
+module redBlackTreeTest where
+
+open import RedBlackTree
+open import stack
+open import Level hiding (zero)
+
+open import Data.Nat
+
+open Tree
+open Node
+open RedBlackTree.RedBlackTree
+open Stack
+
+-- tests
+
+putTree1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next))
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Function
+
+
+check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
+check1 Nothing _ = False
+check1 (Just n)  x with Data.Nat.compare (value n)  x
+...  | equal _ = True
+...  | _ = False
+
+check2 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
+check2 Nothing _ = False
+check2 (Just n)  x with compare2 (value n)  x
+...  | EQ = True
+...  | _ = False
+
+test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True   ))
+test1 = refl
+
+test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
+    \t -> putTree1 t 2 2 (
+    \t -> getRedBlackTree t 1 (
+    \t x -> check2 x 1 ≡ True   )))
+test2 = refl
+
+open ≡-Reasoning
+test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1
+    $ \t -> putTree1 t 2 2
+    $ \t -> putTree1 t 3 3
+    $ \t -> putTree1 t 4 4
+    $ \t -> getRedBlackTree t 1
+    $ \t x -> check2 x 1 ≡ True
+test3 = begin
+    check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
+  ≡⟨ refl ⟩
+    True
+  ∎
+
+test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
+    $ \t -> putTree1 t 2 2
+    $ \t -> putTree1 t 3 3
+    $ \t -> putTree1 t 4 4
+    $ \t -> getRedBlackTree t 4
+    $ \t x -> x
+
+-- test5 : Maybe (Node ℕ ℕ)
+test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4
+    $ \t -> putTree1 t 6 6
+    $ \t0 ->  clearSingleLinkedStack (nodeStack t0)
+    $ \s -> findNode1 t0 s (leafNode 3 3) ( root t0 )
+    $ \t1 s n1 -> replaceNode t1 s n1
+    $ \t -> getRedBlackTree t 3
+    -- $ \t x -> SingleLinkedStack.top (stack s)
+    -- $ \t x -> n1
+    $ \t x -> root t
+  where
+     findNode1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
+     findNode1 t s n1 Nothing next = next t s n1
+     findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next
+
+-- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t ->
+--   putTree1 t 2 2 $ \t -> putTree1 t 3 3 $ \t -> root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
+-- test51 = refl
+
+test6 : Maybe (Node ℕ ℕ)
+test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)})
+
+
+test7 : Maybe (Node ℕ ℕ)
+test7 = clearSingleLinkedStack (nodeStack tree2) (\ s -> replaceNode tree2 s n2 (\ t -> root t))
+  where
+    tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}
+    k1 = 1
+    n2 = leafNode 0 0
+    value1 = 1
+
+test8 : Maybe (Node ℕ ℕ)
+test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
+    $ \t -> putTree1 t 2 2 (\ t -> root t)
+
+
+test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True   ))
+test9 = refl
+
+test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
+    \t -> putRedBlackTree t 2 2 (
+    \t -> getRedBlackTree t 1 (
+    \t x -> check2 x 1 ≡ True   )))
+test10 = refl
+
+test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
+    $ \t -> putRedBlackTree t 2 2
+    $ \t -> putRedBlackTree t 3 3
+    $ \t -> getRedBlackTree t 2
+    $ \t x -> root t
+
+
+redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
+redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
+
+-- compare2 : (x y : ℕ ) -> compareresult
+-- compare2 zero zero = eq
+-- compare2 (suc _) zero = gt
+-- compare2  zero (suc _) = lt
+-- compare2  (suc x) (suc y) = compare2 x y
+
+putTest1Lemma2 : (k : ℕ)  -> compare2 k k ≡ EQ
+putTest1Lemma2 zero = refl
+putTest1Lemma2 (suc k) = putTest1Lemma2 k
+
+putTest1Lemma1 : (x y : ℕ)  -> compareℕ x y ≡ compare2 x y
+putTest1Lemma1 zero    zero    = refl
+putTest1Lemma1 (suc m) zero    = refl
+putTest1Lemma1 zero    (suc n) = refl
+putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
+putTest1Lemma1 (suc .m)           (suc .(Data.Nat.suc m + k)) | less    m k = lemma1  m
+ where
+    lemma1 : (m :  ℕ) -> LT  ≡ compare2 m (ℕ.suc (m + k))
+    lemma1  zero = refl
+    lemma1  (suc y) = lemma1 y
+putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
+ where
+    lemma1 : (m :  ℕ) -> EQ  ≡ compare2 m m
+    lemma1  zero = refl
+    lemma1  (suc y) = lemma1 y
+putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m)           | greater m k = lemma1 m
+ where
+    lemma1 : (m :  ℕ) -> GT  ≡ compare2  (ℕ.suc (m + k))  m
+    lemma1  zero = refl
+    lemma1  (suc y) = lemma1 y
+
+putTest1Lemma3 : (k : ℕ)  -> compareℕ k k ≡ EQ
+putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  )
+
+compareLemma1 : {x  y : ℕ}  -> compare2 x y ≡ EQ -> x  ≡ y
+compareLemma1 {zero} {zero} refl = refl
+compareLemma1 {zero} {suc _} ()
+compareLemma1 {suc _} {zero} ()
+compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
+   where
+      lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
+      lemma2 = refl
+
+
+putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
+         -> (k : ℕ) (x : ℕ)
+         -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
+         (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x  ≡ True))
+putTest1 n k x with n
+...  | Just n1 = lemma2 ( record { top = Nothing } )
+   where
+     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
+         GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
+     lemma2 s with compare2 k (key n1)
+     ... |  EQ = lemma3 {!!}
+        where
+           lemma3 : compare2 k (key n1) ≡  EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
+               } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y  } ) k ( \ t x1 -> check2 x1 x  ≡ True)
+           lemma3 eq with compare2 x x | putTest1Lemma2 x
+           ... | EQ | refl with compare2 k (key n1)  | eq
+           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
+           ...                    | EQ | refl = refl
+     ... |  GT = {!!}
+     ... |  LT = {!!}
+
+...  | Nothing =  lemma1
+   where
+     lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red
+        } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k
+        ( \ t x1 -> check2 x1 x  ≡ True)
+     lemma1 with compare2 k k | putTest1Lemma2 k
+     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
+     ...              | EQ | refl = refl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/singleLinkedStackInterface.cbc	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,12 @@
+Stack* createSingleLinkedStack(struct Context* context) {
+    struct Stack* stack = new Stack();
+    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
+    stack->stack = (union Data*)singleLinkedStack;
+    singleLinkedStack->top = NULL;
+    stack->push = C_pushSingleLinkedStack;
+    stack->pop  = C_popSingleLinkedStack;
+    stack->get  = C_getSingleLinkedStack;
+    stack->isEmpty = C_isEmptySingleLinkedStack;
+    stack->clear = C_clearSingleLinkedStack;
+    return stack;
+}
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/stack-product.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,158 @@
+module stack-product where
+
+open import product
+open import Data.Product
+open import Data.Nat
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality
+
+-- definition based from Gears(209:5708390a9d88) src/parallel_execution
+goto = executeCS
+
+data Bool : Set where
+  True  : Bool
+  False : Bool
+
+data Maybe (a : Set) : Set  where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+
+
+record Stack {a t : Set} (stackImpl : Set) : Set  where
+  field
+    stack : stackImpl
+    push : CodeSegment (stackImpl × a × (CodeSegment stackImpl t)) t
+    pop  : CodeSegment (stackImpl × (CodeSegment (stackImpl × Maybe a) t)) t
+
+
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
+emptySingleLinkedStack = record {top = Nothing}
+
+
+
+
+pushSingleLinkedStack : {a t : Set} -> CodeSegment ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) t
+pushSingleLinkedStack = cs push
+  where
+    push : {a t : Set} -> ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) -> t
+    push (stack , datum , next) = goto next stack1
+      where
+        element = cons datum (top stack)
+        stack1  = record {top = Just element}
+
+popSingleLinkedStack : {a t : Set} -> CodeSegment (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t))  t
+popSingleLinkedStack = cs pop
+  where
+    pop : {a t : Set} -> (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) -> t
+    pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing)
+    pop (record { top = Just x } , nextCS)  = goto nextCS (stack1 , (Just datum1))
+      where
+        datum1 = datum x
+        stack1 = record { top = (next x) }
+
+
+
+
+
+createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a)
+createSingleLinkedStack = record { stack = emptySingleLinkedStack
+                                 ; push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 }
+
+
+
+
+test01 : {a : Set} -> CodeSegment (SingleLinkedStack a × Maybe a) Bool
+test01 = cs test01'
+  where
+    test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool
+    test01' (record { top = Nothing } , _) = False
+    test01' (record { top = Just x } ,  _)  = True
+
+
+test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) (SingleLinkedStack a × Maybe a)
+test02 = cs test02'
+  where
+    test02' : {a : Set} -> SingleLinkedStack a -> (SingleLinkedStack a × Maybe a)
+    test02' stack = goto popSingleLinkedStack (stack , (cs id))
+
+
+test03 : {a : Set} -> CodeSegment a (SingleLinkedStack a)
+test03  = cs test03'
+  where
+    test03' : {a : Set} -> a -> SingleLinkedStack a
+    test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id))
+
+
+lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False
+lemma = refl
+
+
+n-push : {A : Set} {a : A} -> CodeSegment (ℕ  × SingleLinkedStack A) (ℕ × SingleLinkedStack A)
+n-push {A} {a} = cs (push {A} {a})
+  where
+    push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A)
+    push {A} {a} (zero  , s) = (zero , s)
+    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype
+
+
+{-
+
+n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
+n-push zero s            = s
+n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s)
+
+n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
+n-pop zero    s         = s
+n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s)
+
+open ≡-Reasoning
+
+push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s
+push-pop-equiv s = refl
+
+push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s
+push-and-n-pop zero s            = refl
+push-and-n-pop {A} {a} (suc n) s = begin
+  n-pop (suc (suc n)) (pushSingleLinkedStack s a id)
+  ≡⟨ refl ⟩
+  popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
+  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩
+  popSingleLinkedStack (n-pop n s) (\s _ -> s)
+  ≡⟨ refl ⟩
+  n-pop (suc n) s
+  ∎
+
+
+n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s
+n-push-pop-equiv zero s            = refl
+n-push-pop-equiv {A} {a} (suc n) s = begin
+  n-pop (suc n) (n-push (suc n) s)
+  ≡⟨ refl ⟩
+  n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
+  ≡⟨ push-and-n-pop n (n-push n s)  ⟩
+  n-pop n (n-push n s)
+  ≡⟨ n-push-pop-equiv n s ⟩
+  s
+  ∎
+
+
+n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
+n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack
+-}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/stack-subtype-sample.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,212 @@
+module stack-subtype-sample where
+
+open import Level renaming (suc to S ; zero to O)
+open import Function
+open import Data.Nat
+open import Data.Maybe
+open import Relation.Binary.PropositionalEquality
+
+open import stack-subtype ℕ
+open import subtype Context  as N
+open import subtype Meta     as M
+
+
+record Num : Set where
+  field
+    num : ℕ
+
+instance
+  NumIsNormalDataSegment : N.DataSegment Num
+  NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
+                                  ; set = (\c n -> record c {n = Num.num n})}
+  NumIsMetaDataSegment : M.DataSegment Num
+  NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)})
+                                ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})}
+
+
+plus3 : Num -> Num
+plus3 record { num = n } = record {num = n + 3}
+
+plus3CS : N.CodeSegment Num Num
+plus3CS = N.cs plus3
+
+
+
+plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}}
+               -> M.CodeSegment Num (Meta)
+plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
+  where
+    co    = Meta.context mc
+    con : Num -> Context
+    con record { num = num } = N.DataSegment.set nn co record {num = num + 5}
+    st    = Meta.stack mc
+
+
+
+
+push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta
+push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
+  where
+    con  = record { n = 4 ; element = just 0}
+    code = N.cs (\c -> c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+
+
+push-sample-equiv : push-sample ≡ record { nextCS  = liftContext plus3CS
+                                          ; stack   = record { top = nothing}
+                                          ; context = record { n = 9} }
+push-sample-equiv = refl
+
+
+pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta
+pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc
+  where
+    con  = record { n = 4 ; element = just 0}
+    code = N.cs (\c -> c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+
+
+
+pushed-sample-equiv : {m : Meta} ->
+                      pushed-sample {m} ≡ record { nextCS  = liftContext plus3CS
+                                                  ; stack   = record { top = just (cons 0 nothing) }
+                                                  ; context = record { n   = 12} }
+pushed-sample-equiv = refl
+
+
+
+pushNum : N.CodeSegment Context Context
+pushNum = N.cs pn
+  where
+    pn : Context -> Context
+    pn record { n = n } = record { n = pred n  ; element = just n}
+
+
+pushOnce : Meta -> Meta
+pushOnce m = M.exec pushSingleLinkedStackCS m
+
+n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-push {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m))
+
+popOnce : Meta -> Meta
+popOnce m = M.exec popSingleLinkedStackCS m
+
+n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-pop {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m))
+
+
+
+initMeta : ℕ  -> Maybe ℕ -> N.CodeSegment Context Context -> Meta
+initMeta n mn code = record { context = record { n = n ; element = mn}
+                         ; stack   = emptySingleLinkedStack
+                         ; nextCS  = code
+                         }
+
+n-push-cs-exec = M.exec (n-push {meta} 3) meta
+  where
+    meta = (initMeta 5 (just 9) pushNum)
+
+
+n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS  = pushNum
+                                                ; context = record {n = 2 ; element = just 3}
+                                                ; stack   = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}}
+n-push-cs-exec-equiv = refl
+
+
+n-pop-cs-exec = M.exec (n-pop {meta} 4) meta
+  where
+    meta = record { nextCS  = N.cs id
+                  ; context = record { n = 0 ; element = nothing}
+                  ; stack   = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))}
+                  }
+
+n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS  = N.cs id
+                                              ; context = record { n = 0 ; element = just 6}
+                                              ; stack   = record { top = just (cons 5 nothing)}
+                                              }
+
+n-pop-cs-exec-equiv = refl
+
+
+open ≡-Reasoning
+
+id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta
+id-meta n e s = record { context = record {n = n ; element = just e}
+                       ; nextCS = (N.cs id) ; stack = s}
+
+exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m)
+exec-comp (M.cs x) (M.cs _) m = refl
+
+
+push-pop-type : ℕ -> ℕ  -> ℕ -> Element ℕ -> Set₁
+push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
+  where
+    meta = id-meta n e record {top = just (cons x (just s))}
+
+push-pop : (n e x : ℕ) -> (s : Element ℕ) ->  push-pop-type n e x s
+push-pop n e x s = refl
+
+
+
+pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
+pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta
+                         ≡ M.exec (n-push {meta} n) meta
+  where
+    meta = id-meta cn ce s
+
+pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s
+
+pop-n-push zero cn ce s    = refl
+pop-n-push (suc n) cn ce s = begin
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc (suc n)))) (id-meta cn ce s)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
+  ≡⟨ exec-comp (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩
+  M.exec (M.cs popOnce) (M.exec (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
+  ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩
+  M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
+  ≡⟨ refl ⟩
+  M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
+  ≡⟨ sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩
+  M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  ≡⟨ refl ⟩
+  M.exec (n-push n) (pushOnce (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)
+  ∎
+
+
+
+n-push-pop-type : ℕ ->  ℕ  -> ℕ -> SingleLinkedStack ℕ -> Set₁
+n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta
+  where
+    meta = id-meta cn ce st
+
+n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s
+n-push-pop zero    cn ce s = refl
+n-push-pop (suc n) cn ce s = begin
+  M.exec (M.csComp {id-meta cn ce s} (n-pop {id-meta cn ce s}  (suc n)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp  {id-meta cn ce s}  (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
+  ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push {id-meta cn ce s}  (suc n))  (id-meta cn ce s) ⟩
+  M.exec (M.cs (\m -> M.exec (n-pop  {id-meta cn ce s}  n) (popOnce m))) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-pop n) (popOnce (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)))
+  ≡⟨ refl ⟩
+  M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)))
+  ≡⟨ cong (\x -> M.exec (n-pop  {id-meta cn ce s}  n) x) (sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce s}  (suc n)) (id-meta cn ce s))) ⟩
+  M.exec (n-pop n) (M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s))
+  ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s}  n) x) (pop-n-push n cn ce s) ⟩
+  M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
+  ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩
+  M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
+  ≡⟨ n-push-pop n cn ce s ⟩
+  id-meta cn ce s
+  ∎
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/stack-subtype.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,123 @@
+open import Level hiding (lift)
+open import Data.Maybe
+open import Data.Product
+open import Data.Nat hiding (suc)
+open import Function
+
+module stack-subtype (A : Set) where
+
+-- data definitions
+
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+record Context : Set where
+  field
+    -- fields for concrete data segments
+    n       : ℕ
+    -- fields for stack
+    element : Maybe A
+
+
+
+
+
+open import subtype Context as N
+
+instance
+  ContextIsDataSegment : N.DataSegment Context
+  ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)}
+
+
+record Meta  : Set₁ where
+  field
+    -- context as set of data segments
+    context : Context
+    stack   : SingleLinkedStack A
+    nextCS  : N.CodeSegment Context Context
+
+
+
+
+open import subtype Meta as M
+
+instance
+  MetaIncludeContext : M.DataSegment Context
+  MetaIncludeContext = record { get = Meta.context
+                              ; set = (\m c -> record m {context = c}) }
+
+  MetaIsMetaDataSegment : M.DataSegment Meta
+  MetaIsMetaDataSegment  = record { get = (\m -> m) ; set = (\_ m -> m) }
+
+
+liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
+liftMeta (N.cs f) = M.cs f
+
+liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
+liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
+
+-- definition based from Gears(209:5708390a9d88) src/parallel_execution
+
+emptySingleLinkedStack : SingleLinkedStack A
+emptySingleLinkedStack = record {top = nothing}
+
+
+pushSingleLinkedStack : Meta -> Meta
+pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
+  where
+    n = Meta.nextCS m
+    s = Meta.stack  m
+    e = Context.element (Meta.context m)
+    push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
+    push s nothing  = s
+    push s (just x) = record {top = just (cons x (top s))}
+
+
+
+popSingleLinkedStack : Meta -> Meta
+popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
+  where
+    n = Meta.nextCS m
+    con  = Meta.context m
+    elem : Meta -> Maybe A
+    elem record {stack = record { top = (just (cons x _)) }} = just x
+    elem record {stack = record { top = nothing           }} = nothing
+    st : Meta -> SingleLinkedStack A
+    st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
+    st record {stack = record { top = nothing           }} = record {top = nothing}
+
+
+
+
+pushSingleLinkedStackCS : M.CodeSegment Meta Meta
+pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
+
+popSingleLinkedStackCS : M.CodeSegment Meta Meta
+popSingleLinkedStackCS = M.cs popSingleLinkedStack
+
+
+-- for sample
+
+firstContext : Context
+firstContext = record {element = nothing ; n = 0}
+
+
+firstMeta : Meta
+firstMeta = record { context = firstContext
+                   ; stack = emptySingleLinkedStack
+                   ; nextCS = (N.cs (\m -> m))
+                   }
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/stack.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,149 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module stack  where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat
+
+ex : 1 + 2 ≡ 3
+ex = refl
+
+data Bool {n : Level } : Set n where
+  True  : Bool
+  False : Bool
+
+record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+
+data Maybe {n : Level } (a : Set n) : Set n where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+
+record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    push : stackImpl -> a -> (stackImpl -> t) -> t
+    pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
+    pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
+    get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
+    get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
+    clear : stackImpl -> (stackImpl -> t) -> t
+open StackMethods
+
+record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
+  field
+    stack : si
+    stackMethods : StackMethods {n} {m} a {t} si
+  pushStack :  a -> (Stack a si -> t) -> t
+  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
+  popStack : (Stack a si -> Maybe a  -> t) -> t
+  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  pop2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
+  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  getStack :  (Stack a si -> Maybe a  -> t) -> t
+  getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  get2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
+  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  clearStack : (Stack a si -> t) -> t
+  clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
+
+open Stack
+
+{--
+data Element {n : Level } (a : Set n) : Set n where
+  cons : a -> Maybe (Element a) -> Element a
+
+
+datum : {n : Level } {a : Set n} -> Element a -> a
+datum (cons a _) = a
+
+next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+--}
+
+
+-- cannot define recrusive record definition. so use linked list with maybe.
+record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+
+open Element
+
+
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+
+pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
+  where
+    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    pop2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
+
+
+getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+getSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack (Just data1)
+  where
+    data1  = datum d
+
+get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
+  where
+    get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    get2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
+
+clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t
+clearSingleLinkedStack stack next = next (record {top = Nothing})
+
+
+emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
+emptySingleLinkedStack = record {top = Nothing}
+
+-----
+-- Basic stack implementations are specifications of a Stack
+--
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                           }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                             stack = emptySingleLinkedStack ;
+                             stackMethods = singleLinkedStackSpec
+                           }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/stackImpl.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,38 @@
+record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+open Element
+
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+  top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+-- push 以下は省略
+
+-- Basic stack implementations are specifications of a Stack
+
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                               }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                            stack = emptySingleLinkedStack ;
+                            stackMethods = singleLinkedStackSpec
+                          }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/stackTest.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,144 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module stackTest where
+
+open import stack
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat
+open import Function
+
+
+open SingleLinkedStack
+open Stack
+
+----
+--
+-- proof of properties ( concrete cases )
+--
+
+test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
+test01 stack _ with (top stack)
+...                  | (Just _) = True
+...                  | Nothing  = False
+
+
+test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool
+test02 stack = popSingleLinkedStack stack test01
+
+test03 : {n : Level } {a : Set n} -> a ->  Bool
+test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
+
+-- after a push and a pop, the stack is empty
+lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
+lemma = refl
+
+testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m}
+testStack01 v = pushStack createSingleLinkedStack v (
+   \s -> popStack s (\s1 d1 -> True))
+
+-- after push 1 and 2, pop2 get 1 and 2
+
+testStack02 : {m : Level } ->  ( Stack  ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
+testStack02 cs = pushStack createSingleLinkedStack 1 (
+   \s -> pushStack s 2 cs)
+
+
+testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
+testStack031 2 1 = True
+testStack031 _ _ = False
+
+testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
+testStack032  (Just d1) (Just d2) = testStack031 d1 d2
+testStack032  _ _ = False
+
+testStack03 : {m : Level } -> Stack  ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
+testStack03 s cs = pop2Stack s (
+   \s d1 d2 -> cs d1 d2 )
+
+testStack04 : Bool
+testStack04 = testStack02 (\s -> testStack03 s testStack032)
+
+testStack05 : testStack04 ≡ True
+testStack05 = refl
+
+testStack06 : {m : Level } -> Maybe (Element ℕ)
+testStack06 = pushStack createSingleLinkedStack 1 (
+   \s -> pushStack s 2 (\s -> top (stack s)))
+
+testStack07 : {m : Level } -> Maybe (Element ℕ)
+testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (
+   \s -> pushSingleLinkedStack s 2 (\s -> top s))
+
+testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
+   $ \s -> pushSingleLinkedStack s 2
+   $ \s -> pushSingleLinkedStack s 3
+   $ \s -> pushSingleLinkedStack s 4
+   $ \s -> pushSingleLinkedStack s 5
+   $ \s -> top s
+
+------
+--
+-- proof of properties with indefinite state of stack
+--
+-- this should be proved by properties of the stack inteface, not only by the implementation,
+--    and the implementation have to provides the properties.
+--
+--    we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok.
+--    anyway some implementations may result s != s3
+--
+
+stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+
+push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
+
+
+-- id : {n : Level} {A : Set n} -> A -> A
+-- id a = a
+
+-- push a, n times
+
+n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
+n-push zero s            = s
+n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s )
+
+n-pop :  {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
+n-pop zero    s         = s
+n-pop  {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s )
+
+open ≡-Reasoning
+
+push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s
+push-pop-equiv s = refl
+
+push-and-n-pop : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {_} {A} {a} n s
+push-and-n-pop zero s            = refl
+push-and-n-pop {_} {A} {a} (suc n) s = begin
+   n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
+  ≡⟨ refl ⟩
+   popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
+  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩
+   popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
+  ≡⟨ refl ⟩
+    n-pop {_} {A} {a} (suc n) s
+  ∎
+
+
+n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {_} {A} {a} n (n-push {_} {A} {a} n s)) ≡ s
+n-push-pop-equiv zero s            = refl
+n-push-pop-equiv {_} {A} {a} (suc n) s = begin
+    n-pop {_} {A} {a} (suc n) (n-push (suc n) s)
+  ≡⟨ refl ⟩
+    n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
+  ≡⟨ push-and-n-pop n (n-push n s)  ⟩
+    n-pop {_} {A} {a} n (n-push n s)
+  ≡⟨ n-push-pop-equiv n s ⟩
+    s
+  ∎
+
+
+n-push-pop-equiv-empty : {n : Level} {A : Set n} {a : A} -> (n : ℕ) -> n-pop {_} {A} {a} n (n-push {_} {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
+n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/stub.cbc	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,17 @@
+__code put(struct Context* context,
+           struct Tree* tree,
+           struct Node* root,
+           struct Allocate* allocate)
+{
+    /* 実装コードは省略 */
+}
+
+__code put_stub(struct Context* context)
+{
+    goto put(context,
+             &context->data[Tree]->tree,
+             context->data[Tree]->tree.root,
+             &context->data[Allocate]->allocate);
+}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/subtype.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,44 @@
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+module subtype {l : Level} (Context : Set l) where
+
+
+record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
+  field
+    get : Context -> A
+    set : Context -> A -> Context
+open DataSegment
+
+data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where
+  cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
+
+goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} -> CodeSegment I O -> I -> O
+goto (cs b) i = b i
+
+exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}}
+     -> CodeSegment I O -> Context -> Context
+exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))
+
+
+comp : {con : Context} -> {l1 l2 l3 l4 : Level}
+       {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
+       {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
+       -> (C -> D) -> (A -> B) -> A -> D
+comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
+
+csComp : {con : Context} -> {l1 l2 l3 l4 : Level}
+        {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
+         {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
+       -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
+csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)
+      = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
+
+
+
+comp-associative : {A B C D E F : Set l} {con : Context}
+                   {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}}
+                   {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}}
+                   -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
+                   -> csComp {con} c (csComp {con} b a)  ≡ csComp {con} (csComp {con} c b) a
+comp-associative (cs _) (cs _) (cs _) = refl