# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1514773154 -32400
# Node ID 6d984ea42fd22a82f8d3803258b64e30226a81c9
# Parent  2c125aa7a5773abafa27e5796631796987cdcea2
fix proof

diff -r 2c125aa7a577 -r 6d984ea42fd2 src/parallel_execution/stack.agda
--- a/src/parallel_execution/stack.agda	Mon Jan 01 09:34:46 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 11:19:14 2018 +0900
@@ -146,19 +146,19 @@
 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
 lemma = refl
 
--- after push 1 and 2, pop2 get 1 and 2
-
 testStack01 : {n : Level } {a : Set n} -> a -> Bool
 testStack01 v = pushStack createSingleLinkedStack v (
    \s -> popStack s (\s1 d1 -> True))
 
-testStack02 : (Stack (SingleLinkedStack ℕ) -> Bool) -> Bool
+-- after push 1 and 2, pop2 get 1 and 2
+
+testStack02 : ( Stack (SingleLinkedStack ℕ) -> Bool) -> Bool
 testStack02 cs = pushStack createSingleLinkedStack 1 (
    \s -> pushStack s 2 cs)
 
 
 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
-testStack031 1 2 = True
+testStack031 2 1 = True
 testStack031 _ _ = False
 
 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
@@ -172,8 +172,8 @@
 testStack04 : Bool
 testStack04 = testStack02 (\s -> testStack03 s testStack032)
 
-testStack05 : Set (succ Zero)
-testStack05 = testStack04 ≡ True
+testStack05 : testStack04 ≡ True
+testStack05 = refl
 
 id : {n : Level} {A : Set n} -> A -> A
 id a = a