--- a/hoareRedBlackTree.agda	Sat Nov 02 16:37:27 2019 +0900
+++ b/hoareRedBlackTree.agda	Sat Nov 02 17:34:46 2019 +0900
@@ -12,6 +12,7 @@
 
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
+open import logic
 
 
 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
@@ -114,15 +115,17 @@
      ;  nodeStack = emptySingleLinkedStack
    }
 
-popAllnode : {n m  : Level } {a : Set n} → RedBlackTree {n} {m}  a  → Maybe (Node a)
-popAllnode {n} {m} {a} tree = popAllNode1 (nodeStack tree) where
-    popAllNode1 : SingleLinkedStack (Node a ) →  Maybe (Node a)
-    popAllNode1 [] = nothing
-    popAllNode1 (x ∷ t) = just {!!}
+popAllNode1 : {n : Level } {a : Set n} → SingleLinkedStack (Node a ) → Node a →  Maybe (Node a)
+popAllNode1 [] r = nothing
+popAllNode1 (x ∷ t) r with popAllNode1 t r
+... | ttt = {!!}
 
-record findNodeInvariant {n m  : Level } {a : Set n} {t : Set m} (ordinal now :  RedBlackTree {n} {m}  a ) : Set (m Level.⊔ n) where
+popAllnode : {n m  : Level } {a : Set n} → RedBlackTree {n} {m}  a  → RedBlackTree {n} {m}  a → Set
+popAllnode {n} {m} {a} now original = {!!}
+
+record findNodeInvariant {n m  : Level } {a : Set n} {t : Set m} (now original :  RedBlackTree {n} {m}  a ) : Set (m Level.⊔ n) where
    field
-     tree+stack : popAllnode now ≡ root ordinal
+     tree+stack : popAllnode now original