--- a/src/parallel_execution/stack.agda	Mon Jan 01 11:19:14 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 18:32:20 2018 +0900
@@ -8,11 +8,11 @@
 ex : 1 + 2 ≡ 3
 ex = refl
 
-data Bool {n : Level } : Set (succ n) where
+data Bool {n : Level } : Set n where
   True  : Bool
   False : Bool
 
-record _∧_ {n : Level } {a b : Set n} : Set n where
+record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
   field
     pi1 : a
     pi2 : b
@@ -31,20 +31,20 @@
     get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
 open Stack
 
-pushStack : {n : Level } {t : Set (succ n)} {a si : Set n}  -> Stack si -> a -> (Stack si -> t) -> t
-pushStack {t} {a} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} ))
+pushStack : {n m : Level } {t : Set m} {a si : Set n}  -> Stack si -> a -> (Stack si -> t) -> t
+pushStack s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} ))
 
-popStack : {n : Level } { t : Set (succ n)} {a si : Set n} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
-popStack {t} {a} s0  next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
+popStack : {n m : Level } { t : Set m} {a si : Set n} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
+popStack s0  next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
 
-pop2Stack : {n : Level } { t : Set (succ n)} { a  si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
-pop2Stack {t} {a} s0 next = pop2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
+pop2Stack : {n m : Level } { t : Set m} { a  si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
+pop2Stack s0 next = pop2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
 
-getStack : {n : Level } {t : Set (succ n)} {a  si : Set n} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
-getStack {t} {a} s0 next = get s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
+getStack : {n m : Level } {t : Set m} {a  si : Set n} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
+getStack s0 next = get s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
 
-get2Stack : {n : Level } {t : Set (succ n)} {a  si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
-get2Stack {t} {a} s0 next = get2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
+get2Stack : {n m : Level } {t : Set m} {a  si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
+get2Stack s0 next = get2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
 
 
 data Element {n : Level } (a : Set n) : Set n where
@@ -146,13 +146,13 @@
 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
 lemma = refl
 
-testStack01 : {n : Level } {a : Set n} -> a -> Bool
+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 : ( Stack (SingleLinkedStack ℕ) -> Bool) -> Bool
+testStack02 : {m : Level } -> ( Stack (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
 testStack02 cs = pushStack createSingleLinkedStack 1 (
    \s -> pushStack s 2 cs)
 
@@ -165,7 +165,7 @@
 testStack032  (Just d1) (Just d2) = testStack031 d1 d2
 testStack032  _ _ = False
 
-testStack03 : Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool ) -> Bool
+testStack03 : {m : Level } -> Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
 testStack03 s cs = pop2Stack s (
    \s d1 d2 -> cs d1 d2 )
 
@@ -175,6 +175,12 @@
 testStack05 : testStack04 ≡ True
 testStack05 = refl
 
+------
+-- 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 = {!!}
+
+
 id : {n : Level} {A : Set n} -> A -> A
 id a = a