# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572740871 -32400
# Node ID 7e551cef35d7073f72617168b026145680dcc9e5
# Parent  d18df2e6135d525d449ef82080760deb75034a66
...

diff -r d18df2e6135d -r 7e551cef35d7 hoareRedBlackTree.agda
--- a/hoareRedBlackTree.agda	Sun Nov 03 08:53:00 2019 +0900
+++ b/hoareRedBlackTree.agda	Sun Nov 03 09:27:51 2019 +0900
@@ -139,11 +139,12 @@
 findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))
 
 data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set n where
-   fni-Top  : (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 →  FindNodeInvariant t original
-   fni-Right  : (x : Node a) (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
-      →  FindNodeInvariant ( x ∷ t ) original → findNodeRight x t →  FindNodeInvariant t original
+   fni-stackEmpty  : (now :  RedBlackTree {n}  a ) → FindNodeInvariant [] now 
+   fni-treeEmpty  : (st : SingleLinkedStack (Node a))  → FindNodeInvariant st record { root = nothing ; nodeStack = st }
+   fni-Left  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
+      →  FindNodeInvariant ( x ∷ st ) original → findNodeLeft x st →  FindNodeInvariant st original
+   fni-Right  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
+      →  FindNodeInvariant ( x ∷ st ) original → findNodeRight x st →  FindNodeInvariant st original
 
 
 findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
@@ -152,13 +153,13 @@
 findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
   module FindNodeH where
     findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree  → t
-    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st }  {!!}
+    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!}
     findNode2h (just x) st prev with <-cmp (key n0) (key x)
     ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
     ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )
     ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )
 
 
-replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t
-replaceNodeH = {!!}
+-- replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t
+-- replaceNodeH = {!!}