# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484448938 0
# Node ID ee2659635734e4614a19c1386ca50e673df10fde
# Parent  211fde284b7e23ef24f83eebed3cc911cffd9aee
Trying prove n-push/n-pop ...

diff -r 211fde284b7e -r ee2659635734 cbc/stack-subtype-sample.agda
--- a/cbc/stack-subtype-sample.agda	Sun Jan 15 02:33:47 2017 +0000
+++ b/cbc/stack-subtype-sample.agda	Sun Jan 15 02:55:38 2017 +0000
@@ -231,15 +231,11 @@
   ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩
   M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
   ≡⟨ refl ⟩
-  M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (record { nextCS  = (N.cs id) ;
-                                                           context = record {n = cn ; element = just ce} ;
-                                                           stack   = record {top = just (cons ce (SingleLinkedStack.top s)) }
-                                                         }))
-  ≡⟨ {!!} ⟩
-  M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) ?
-  ≡⟨ {!!} ⟩
-  M.exec (n-push n) (record { nextCS  = (N.cs id) ; context = record {n = cn ; element = just ce} ;
-                              stack   = record {top = just (cons ce (SingleLinkedStack.top s))}})
+  M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
+  ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩
+  M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  ≡⟨ pop-n-push {!!} cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩
+  M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
   ≡⟨ refl ⟩
   M.exec (n-push n) (pushOnce (id-meta cn ce s))
   ≡⟨ refl ⟩