--- a/src/parallel_execution/stack.agda	Tue Nov 29 18:09:28 2016 +0900
+++ b/src/parallel_execution/stack.agda	Tue Dec 06 08:17:08 2016 +0000
@@ -2,6 +2,10 @@
 
 open import Relation.Binary.PropositionalEquality
 
+data Nat : Set where
+  zero : Nat
+  suc  : Nat -> Nat
+
 data Bool : Set where
   True  : Bool
   False : Bool
@@ -83,3 +87,45 @@
 
 lemma : {A : Set} {a : A} -> test03 a ≡ False
 lemma = refl
+
+id : {A : Set} -> A -> A
+id a = a
+
+
+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
+  ∎