# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1514800685 -32400
# Node ID 8d997f0c9b2ce64ae61f4b516235d0aa5cb34659
# Parent  55077dd40a51de11aab2b121062496d94d959316
stack.agda comment

diff -r 55077dd40a51 -r 8d997f0c9b2c src/parallel_execution/stack.agda
--- a/src/parallel_execution/stack.agda	Mon Jan 01 18:32:20 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 18:58:05 2018 +0900
@@ -177,8 +177,17 @@
 
 ------
 -- 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 ) ) ))))
+--     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 = {!!}
 
 
 id : {n : Level} {A : Set n} -> A -> A