--- a/hoareBinaryTree1.agda	Wed May 29 14:23:41 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed May 29 21:31:02 2024 +0900
@@ -96,6 +96,17 @@
         suc i ≤⟨ m≤m+n (suc i) j ⟩
         suc i + j ∎  where open ≤-Reasoning
 
+nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
+nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
+
+nat-<≡ : { x : ℕ } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
 treeTest1  : bt ℕ
 treeTest1  =  node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
 treeTest2  : bt ℕ
@@ -138,12 +149,28 @@
 
 si-property-< :  {n : Level} {A : Set n} {key key₁ kp : ℕ} {value₁ value₂ : A} {tree orig tree₁ tree₂ tree₃ : bt A} → {stack  : List (bt A)}
    → tree ≡ node key₁ value₁ tree₁ tree₂
-   → stackInvariant key orig tree (tree ∷ node kp value₂ tree  tree₃ ∷ stack)
+   → treeInvariant (node kp value₂ tree  tree₃ )
+   → stackInvariant key tree orig (tree ∷ node kp value₂ tree  tree₃ ∷ stack)
+   → key < kp
+si-property-< refl (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂)
+si-property-< refl (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₇ si)) = ⊥-elim (nat-<> x₁ x₂)
+si-property-< refl (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₇ si)) = ⊥-elim (nat-<> x₁ x₂)
+si-property-< refl (t-left _ _ x₁ x₂ x₃ ti) (s-left .(node _ _ _ _) _ .leaf x s-nil) = x
+si-property-< refl (t-node _ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node _ _ _ _) _ .(node key₂ _ _ _) x s-nil) = x
+si-property-< refl ti (s-left .(node _ _ _ _) _ tree x (s-right .(node _ _ (node _ _ _ _) tree) _ tree₁ x₁ si)) = x
+si-property-< refl ti (s-left .(node _ _ _ _) _ tree x (s-left .(node _ _ (node _ _ _ _) tree) _ tree₁ x₁ si)) = x
+
+si-property-> :  {n : Level} {A : Set n} {key key₁ kp : ℕ} {value₁ value₂ : A} {tree orig tree₁ tree₂ tree₃ : bt A} → {stack  : List (bt A)}
+   → tree ≡ node key₁ value₁ tree₁ tree₂
+   → treeInvariant (node kp value₂ tree₃  tree )
+   → stackInvariant key tree orig (tree ∷ node kp value₂ tree₃  tree ∷ stack)
    → kp < key
-si-property-< refl (s-right _ _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) .(node _ _ _ _) tree₁ x₁ si)) = ?
-si-property-< refl (s-right _ _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) .(node _ _ _ _) tree x₁ si)) = x
-si-property-< refl (s-left _ _ tree x (s-right .(node _ _ (node _ _ _ _) tree) .(node _ _ _ _) tree₁ x₁ si)) = ?
-si-property-< refl (s-left _ _ tree x (s-left .(node _ _ (node _ _ _ _) tree) .(node _ _ _ _) tree₁ x₁ si)) = ?
+si-property-> refl ti (s-right .(node _ _ _ _) _ tree₁ x s-nil) = x
+si-property-> refl ti (s-right .(node _ _ _ _) _ tree₁ x (s-right .(node _ _ tree₁ (node _ _ _ _)) _ tree₂ x₁ si)) = x
+si-property-> refl ti (s-right .(node _ _ _ _) _ tree₁ x (s-left .(node _ _ tree₁ (node _ _ _ _)) _ tree x₁ si)) = x
+si-property-> refl (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂)
+si-property-> refl (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₁ si)) = ⊥-elim (nat-<> x₂ x₃)
+si-property-> refl (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₁ si)) = ⊥-elim (nat-<> x₂ x₃)
 
 si-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-last stack ≡ just tree0
@@ -183,17 +210,6 @@
 rt-property-key (r-right x ri) = refl
 rt-property-key (r-left x ri) = refl
 
-nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
-nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
-nat-<> : { x y : ℕ } → x < y → y < x → ⊥
-nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
-
-nat-<≡ : { x : ℕ } → x < x → ⊥
-nat-<≡  (s≤s lt) = nat-<≡ lt
-
-nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
-nat-≡< refl lt = nat-<≡ lt
-
 
 open _∧_
 
@@ -1574,6 +1590,23 @@
      sc01 (s-left .parent .orig tree x si2) with si-property1 si2
      ... | refl = si2
 
+stackCase3 : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A)))
+           → ( tree orig : bt (Color ∧ A)) →  (key : ℕ)
+           → treeInvariant orig
+           → stackInvariant key tree  orig ( tree ∷ rest )
+           → treeInvariant tree 
+stackCase3 .[] tree .tree key ti s-nil = ti
+stackCase3 .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-right .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf
+stackCase3 .(node _ _ leaf (node key₁ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-right .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) .leaf x s-nil) = ti
+stackCase3 .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x s-nil) = t-leaf
+stackCase3 .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x s-nil) = ti₁
+stackCase3 .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with stackCase3 _ _ _ _ ti si2
+... | t-single _ _ = t-leaf
+... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁
+... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf
+... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂
+stackCase3 .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) = ?
+stackCase3 rest tree orig key ti (s-left .tree .orig tree₁ x si) = ?
 
 PGtoRBinvariant1 : {n : Level} {A : Set n} 
            → (tree orig : bt (Color ∧ A) )
@@ -1807,6 +1840,8 @@
        rb04 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb03)
        rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red
        rb05 refl refl = refl
+       rb06 : key < kp
+       rb06 = si-property-< ? ? ?
 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}