Mercurial > hg > Gears > GearsAgda

changeset 181:78b28c8ffff2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove equivalence n-push/n-pop to empty stack
author atton
date Tue, 13 Dec 2016 02:12:49 +0000
parents d8947747ff3b
children 57a11c15ff4c
files src/parallel_execution/stack.agda
diffstat 1 files changed, 4 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/stack.agda	Tue Dec 13 02:08:40 2016 +0000
+++ b/src/parallel_execution/stack.agda	Tue Dec 13 02:12:49 2016 +0000
@@ -129,3 +129,7 @@
   ≡⟨ n-push-pop-equiv n s ⟩
   s
   ∎
+
+
+n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
+n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack