pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta
                         ≡ M.exec (n-push n) meta
  where
    meta = id-meta cn ce s

pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s
pop-n-push zero cn ce s    = refl
pop-n-push (suc n) cn ce s = begin
  M.exec (M.csComp  (M.cs popOnce) (n-push  (suc (suc n)))) (id-meta cn ce s)
  ≡⟨ refl ⟩
  M.exec (M.csComp (M.cs popOnce) (M.csComp  (n-push  (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
  ≡⟨ exec-comp (M.cs popOnce) (M.csComp  (n-push  (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩
  M.exec (M.cs popOnce) (M.exec (M.csComp  (n-push  (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
  ≡⟨ 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)) (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 n 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 ⟩
  M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
  ≡⟨ refl ⟩
  M.exec (n-push (suc n)) (id-meta cn ce s)
  ∎



n-push-pop-type : ℕ ->  ℕ  -> ℕ -> SingleLinkedStack ℕ -> Set₁
n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta ≡ meta
  where
    meta = id-meta cn ce st

n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s
n-push-pop zero    cn ce s = refl
n-push-pop (suc n) cn ce s = begin
  M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s)
  ≡⟨ refl ⟩
  M.exec (M.csComp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s)
  ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))  (id-meta cn ce s) ⟩
  M.exec (M.cs (\m -> M.exec (n-pop  n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s))
  ≡⟨ refl ⟩
  M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s)))
  ≡⟨ refl ⟩
  M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s)))
  ≡⟨ cong (\x -> M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) ⟩
  M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s))
  ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩
  M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
  ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩
  M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
  ≡⟨ n-push-pop n cn ce s ⟩
  id-meta cn ce s
  ∎