# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1706067305 -32400
# Node ID a16f0b2ce509f4911b72de674212d39c2692afd9
# Parent  e22ebb0f00a3dade6d3d5ae22cd73f0e89dfd6b2
...

diff -r e22ebb0f00a3 -r a16f0b2ce509 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Wed Jan 24 10:36:44 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Jan 24 12:35:05 2024 +0900
@@ -107,6 +107,13 @@
 si-property1 (s-right _ _ _ _  si) = refl
 si-property1 (s-left _ _ _ _  si) = refl
 
+si-property2 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → (stack  : List (bt A)) →  stackInvariant key tree tree0 (tree1 ∷ stack)
+   → ¬ ( just leaf ≡ stack-last stack )
+si-property2 (.leaf ∷ []) (s-right _ _ tree₁ x ()) refl
+si-property2 (x₁ ∷ x₂ ∷ stack) (s-right _ _ tree₁ x si) eq = si-property2 (x₂ ∷ stack) si eq
+si-property2 (.leaf ∷ []) (s-left _ _ tree₁ x ()) refl
+si-property2 (x₁ ∷ x₂ ∷ stack) (s-left _ _ tree₁ x si) eq = si-property2 (x₂ ∷ stack) si eq
+
 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
 si-property-last key t t0 (t ∷ [])  (s-nil )  = refl
@@ -976,7 +983,10 @@
     insertCase12 :  (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
        → stackInvariant key (RBI.tree r) orig stack
        → t
-    insertCase12 leaf eq1 si = {!!} -- can't happen
+    insertCase12 leaf eq1 si = ⊥-elim (rb04 eq eq1 si) where -- can't happen
+       rb04 : {stack : List ( bt ( Color ∧ A))} → stack ≡ RBI.tree r ∷ orig ∷ [] → leaf ≡ orig → stackInvariant key (RBI.tree r) orig stack →   ⊥ 
+       rb04  refl refl (s-right tree leaf tree₁ x si) = si-property2 _ (s-right tree leaf tree₁ x si) refl
+       rb04  refl refl (s-left tree₁ leaf tree x si) = si-property2 _  (s-left tree₁ leaf tree x si) refl
     insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ 
     ... | tri< a ¬b ¬c = {!!} where 
        rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r