--- a/hoareBinaryTree1.agda	Sat Jun 08 15:55:03 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat Jun 08 16:10:41 2024 +0900
@@ -950,12 +950,7 @@
        → ¬ ( tree ≡ leaf) 
        → (rotated : replacedRBTree key value tree repl)
        → RBI-state key value tree repl stack  -- one stage up
-   rotate-leaf  : (tree repl : bt (Color ∧ A)) →  {stack : List (bt (Color ∧ A))} → color repl ≡ Red 
-       → node-key repl ≡ just key
-       → (rotated : replacedRBTree key value leaf repl)
-       → RBI-state key value leaf repl stack  -- two stages up
    rotate  : (tree : bt (Color ∧ A)) → {repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red 
-       → ¬ ( tree ≡ leaf) 
        → (rotated : replacedRBTree key value tree repl)
        → RBI-state key value tree repl stack  -- two stages up
    top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))}  → stack ≡ tree ∷ []
@@ -1775,7 +1770,7 @@
          ; treerb = rb-leaf 
          ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf
          ; si = subst (λ k → stackInvariant key k leaf _ ) crbt01 si
-         ; state = rotate-leaf leaf _ refl refl rbr-leaf
+         ; state = rotate leaf refl rbr-leaf
          } where
              crbt01 : tree ≡ leaf
              crbt01 with si-property-last _ _ _ _ si | si-property1 si
@@ -1814,7 +1809,7 @@
          ; treerb = rb-leaf
          ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf
          ; si = si
-         ; state = rotate-leaf leaf _ refl refl rbr-leaf
+         ; state = rotate leaf refl rbr-leaf
          } 
      crbt00 (node key₁ value₁ left right ) (case1 eq) refl = ⊥-elim (bt-ne (sym eq))
      crbt00 (node key₁ value₁ left right ) (case2 eq) refl with si-property-last _ _ _ _ si | si-property1 si
@@ -2076,7 +2071,7 @@
             ; treerb = rb02
             ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (RBI.replrb r) (rb-red _ _ rb16 uncle-black rb19 rb06 rb05))
             ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
-            ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 ? rb11
+            ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11
            } rb15 where
             -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
             -- x  : PG.parent pg ≡ node kp vp (RBI.tree r) n1
@@ -2145,36 +2140,7 @@
         rb00 : RBI.tree r ≡ orig
         rb00 with si-property-last _ _ _ _ (subst (λ k → stackInvariant key (RBI.tree r) orig k) (eq) (RBI.si r))
         ... | refl = refl
-    ... | rotate-leaf tree repl repl-red keyeq rot = insertCase0 where
-        insertCase0 : t
-        insertCase0 with stackToPG (RBI.tree r) orig stack (RBI.si r)
-        ... | case1 eq = exit stack eq r
-        ... | case2 (case1 eq1) = insertCase4 orig refl eq1 rot (case1 repl-red) (RBI.si r)
-        ... | case2 (case2 pg) with color (PG.parent pg) in pcolor
-        ... | Black = insertCase1 where
-           rb00 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
-           rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
-           treerb : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg)
-           treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg))
-           rb08 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → treeInvariant (PG.parent pg)
-           rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))
-           insertCase1 : t
-           insertCase1 with PG.pg pg
-           ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
-               tree = PG.parent pg
-               ; repl = ?
-               ; origti = RBI.origti r
-               ; origrb = RBI.origrb r
-               ; treerb = treerb pg
-               ; replrb = ?
-               ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
-               ; state = rebuild (cong color x)  ? ? ?
-              } ?      
-           insertCase1 | s2-1sp2 lt x x₁ = ?
-           insertCase1 | s2-s12p lt x x₁ = ?
-           insertCase1 | s2-1s2p lt x x₁ = ?
-        ... | Red = ?
-    ... | rotate _ repl-red ¬leaf rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
+    ... | rotate _ repl-red rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
     ... | case1 eq  = exit stack eq r     -- no stack, replace top node
     ... | case2 (case1 eq) = insertCase4 orig refl eq rot (case1 repl-red) (RBI.si r)     -- one level stack, orig is parent of repl
     ... | case2 (case2 pg) with color (PG.parent pg) in pcolor
@@ -2202,8 +2168,7 @@
             rb01 : bt (Color ∧ A)
             rb01 = node kp vp repl n1
             rb03 : key < kp
-            rb03 = si-property-< ¬leaf (subst (λ k → treeInvariant k) x (rb08 pg)) 
-                (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg))
+            rb03 = lt
             rb04 :  ⟪ Black , proj2 vp ⟫ ≡ vp
             rb04 with subst (λ k → color k ≡ Black) x pcolor
             ... | refl = refl
@@ -2234,8 +2199,7 @@
     ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg   -- insertCase2 : uncle and parent are Red, flip color and go up by two level
     ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where
         insertCase2 : t
-        insertCase2 with <-cmp key kp
-        ... | tri< a ¬b ¬c = next  (PG.grand pg ∷ (PG.rest pg))
+        insertCase2 = next  (PG.grand pg ∷ (PG.rest pg))
             record {
                  tree = PG.grand pg
                  ; repl = to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg)))
@@ -2244,7 +2208,7 @@
                  ; treerb = rb01
                  ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ rb13 (RBI.replrb r) rb04) (RBtreeToBlack _ rb02)
                  ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
-                 ; state = rotate ? refl ? (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl  (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot))
+                 ; state = rotate _ refl (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl  (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot))
              }  rb15 where
                rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
                rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
@@ -2263,7 +2227,7 @@
                rb07 : treeInvariant (node kp vp (RBI.tree r) n1)
                rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00))
                rb06 : key < kp
-               rb06 = a
+               rb06 = lt
                rb10 : vg ≡ ⟪ Black , proj2 vg ⟫
                rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case1 pcolor)
                ... | refl = refl
@@ -2307,8 +2271,6 @@
                   length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩
                   length stack ∎
                      where open ≤-Reasoning
-        ... | tri≈ ¬a b ¬c  = ⊥-elim ( si-property-pne _ _ stack (trans (PG.stack=gp pg) (cong (λ k → _ ∷ k ∷ _) x) ) (RBI.si r) b ) -- can't happen
-        ... | tri> ¬a ¬b c = ?
     ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!}
     ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!}
     ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!}