--- a/hoareBinaryTree1.agda	Sun Jan 28 12:19:45 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jan 29 11:42:39 2024 +0900
@@ -41,6 +41,8 @@
 
 open import Data.Unit hiding ( _≟_ ) -- ;  _≤?_ ; _≤_)
 
+--
+--
 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
     t-leaf : treeInvariant leaf
     t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf)
@@ -54,6 +56,30 @@
        → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
 
 --
+-- treeInvraiant is not enough to show that a tree is sorted
+--
+max-key-in-left : {n : Level} {A : Set n} → (key : ℕ) → bt A → ℕ
+max-key-in-left {_} {A} key tr = ?
+
+min-key-in-right : {n : Level} {A : Set n} → (key : ℕ) →  bt A → ℕ
+min-key-in-right {_} {A} key tr = ?
+
+data treeInvariantSorted {n : Level} {A : Set n} : (tree : bt A) → Set n where
+    st-leaf : treeInvariantSorted leaf
+    st-single : (key : ℕ) → (value : A) →  treeInvariantSorted (node key value leaf leaf)
+    st-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariantSorted (node key₁ value₁ t₁ t₂)
+       → treeInvariantSorted (node key value leaf (node key₁ value₁ t₁ t₂))
+    st-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariantSorted (node key value t₁ t₂)
+       → treeInvariantSorted (node key₁ value₁ (node key value t₁ t₂) leaf )
+    st-node  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {left right : bt A} 
+       → (tl : treeInvariantSorted left )
+       → (tr : treeInvariantSorted right )
+       → max-key-in-left key left < key →  key < min-key-in-right key right 
+       → treeInvariantSorted (node key value₁ left right)
+
+
+
+--
 --  stack always contains original top at end (path of the tree)
 --
 data stackInvariant {n : Level} {A : Set n}  (key : ℕ) : (top orig : bt A) → (stack  : List (bt A)) → Set n where
@@ -122,6 +148,17 @@
 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
+Diffkey : {n : Level} (A : Set n) (tree0 : bt A) → (key : ℕ) →  (tree : bt A) → (stack  : List (bt A)) → (si : stackInvariant key tree tree0 stack) → Set
+Diffkey A leaf key .leaf .(leaf ∷ []) s-nil = ?
+Diffkey A (node key₁ value tree0 tree1) key .(node key₁ value tree0 tree1) .(node key₁ value tree0 tree1 ∷ []) s-nil = ?
+Diffkey A tree0 key leaf .(leaf ∷ _) (s-right .leaf .tree0 tree₁ x si) = ?
+Diffkey A tree0 key (node key₁ value tree tree₂) .(node key₁ value tree tree₂ ∷ _) (s-right .(node key₁ value tree tree₂) .tree0 tree₁ x si) = ?
+Diffkey A tree0 key tree .(tree ∷ _) (s-left .tree .tree0 tree₁ x si) = ?
+
+si-property-ne :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
+   → length stack > 1 → ¬ ( node-key tree ≡ just key )
+si-property-ne = ?
+
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
@@ -868,15 +905,6 @@
 ... | s2-s12p refl refl = ⟪ (λ () ) , ( λ () ) ⟫
 ... | s2-1s2p refl refl = ⟪ (λ () ) , ( λ () ) ⟫
 
-pg-prop-2 : {n : Level} (A : Set n) → (tree orig : bt A ) → {key : ℕ }
-           →  (stack : List (bt A)) → (si : stackInvariant key tree orig stack)  → (pg : PG A tree stack)
-           → ¬  (node-key (PG.parent pg) ≡ node-key tree) 
-pg-prop-2 {_} A tree orig stack si pg with PG.pg pg | PG.stack=gp pg
-... | s2-s1p2 x x₁ | t = ?
-... | s2-1sp2 x x₁ | t = ?
-... | s2-s12p x x₁ | t = ?
-... | s2-1s2p x x₁ | t = ?
-
 -- PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) )
 --            →  RBtreeInvariant orig
 --            →  (stack : List (bt (Color ∧ A)))  → (pg : PG (Color ∧ A) tree stack )