--- a/hoareRedBlackTree.agda	Sat Nov 02 17:34:46 2019 +0900
+++ b/hoareRedBlackTree.agda	Sat Nov 02 18:08:26 2019 +0900
@@ -58,7 +58,7 @@
     color : Color {n}
 open Node
 
-record RedBlackTree {n m : Level } (a : Set n) : Set (m Level.⊔ n) where
+record RedBlackTree {n : Level } (a : Set n) : Set n where
   field
     root : Maybe (Node a )
     nodeStack : SingleLinkedStack  (Node a )
@@ -73,7 +73,7 @@
 --
 
 {-# TERMINATING #-}
-findNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} {m}  a  → (Node a ) → (RedBlackTree {n} {m}  a → t) → t
+findNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n}  a  → (Node a ) → (RedBlackTree {n}  a → t) → t
 findNode {n} {m} {a}  {t} tree n0 next with root tree
 findNode {n} {m} {a}  {t} tree n0 next | nothing = next tree
 findNode {n} {m} {a}  {t} tree n0 next | just x with <-cmp (key x) (key n0)
@@ -82,7 +82,7 @@
 findNode {n} {m} {a}  {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
 
 
-findNode1 : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} {m}  a  → (Node a ) → (RedBlackTree {n} {m}  a  → t) → t
+findNode1 : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
 findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
   module FindNode where
     findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t
@@ -109,25 +109,24 @@
    node001 ( λ tree → tree )
 
 createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
-     → RedBlackTree {n} {m}  a 
+     → RedBlackTree {n}  a 
 createEmptyRedBlackTreeℕ a b = record {
         root = nothing
      ;  nodeStack = emptySingleLinkedStack
    }
 
-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 = {!!}
+findNodeLeft : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}   a ) → Set
+findNodeLeft x t original = {!!}
+findNodeRight : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set
+findNodeRight x t original = {!!}
 
-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 original
+data findNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set n where
+   FNI-Last  : (now :  RedBlackTree {n}  a ) → findNodeInvariant [] now 
+   FNI-Left  : (x : Node a) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
+      →  findNodeInvariant ( x ∷ t ) original → findNodeLeft x t original  →  findNodeInvariant t original
+   FNI-Right  : (x : Node a) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
+      →  findNodeInvariant ( x ∷ t ) original → findNodeRight x t original  →  findNodeInvariant t original
 
 
 
 
-