--- a/src/parallel_execution/stack.agda	Tue Jan 02 02:23:41 2018 +0900
+++ b/src/parallel_execution/stack.agda	Wed Jan 03 18:22:14 2018 +0900
@@ -120,18 +120,28 @@
 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
 emptySingleLinkedStack = record {top = Nothing}
 
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a)
-createSingleLinkedStack = record {
-                             stack = emptySingleLinkedStack ;
-                             stackMethods = record {
+-----
+-- 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
-                                 }
                            }
 
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                             stack = emptySingleLinkedStack ;
+                             stackMethods = singleLinkedStackSpec 
+                           }
+
+----
+--
+-- proof of properties ( concrete cases )
+--
 
 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
 test01 stack _ with (top stack)
@@ -180,23 +190,21 @@
 
 ------
 --
+-- 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 we cant use stack s ≡ stack s3
+--    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
 --  
--- push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : Stack (SingleLinkedStack D) ) ->
---     pushStack s x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))))
--- push->push->pop2 {l} {D} x y s = {!!}
---    where
---       t0 :  (s3 : Stack {_} {succ l} {D} {Set l} (SingleLinkedStack D)) (x1 y1 : Maybe D) -> (stack s ≡ stack s3 )  ->  (Just x ≡ x1 ) -> (Just y ≡ y1 )
---           -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) )) 
---       t0 s3 x1 y1 refl refl refl = record { pi1 = refl ; pi2 = record { pi1 = refl ; pi2 = refl } }
---       t1 :  (s2 : Stack (SingleLinkedStack D))  ->   pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
---       t1 s2 = {!!} 
---       t2 :  (s1 : Stack (SingleLinkedStack D)) (x1 y1 : Maybe D) ->   
---            pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ) ))
---       t2 s1 = {!!}
+
+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