# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1709616213 -32400
# Node ID 2a19292edd8876b50b155ca314600b2cb87f365b
# Parent  c9850c2261950f21bf29004d315037651e86d218
...

diff -r c9850c226195 -r 2a19292edd88 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Thu Feb 29 17:35:40 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue Mar 05 14:23:33 2024 +0900
@@ -502,9 +502,9 @@
 RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x a b ti
 RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ a b c d ti ti₁
 -- r-right case
-RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right x ? ? (t-single key value)
+RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right x _ _ (t-single key value)
 RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right x₁ a b ti) (r-right x ri) = t-single key₁ value₁
-RTtoTI0 (node key₁ _ leaf right@(node key₂ _ _ _)) (node key₁ value₁ leaf right₁@(node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) =
+RTtoTI0 (node key₁ _ leaf right@(node key₂ _ left₁ right₁)) (node key₁ value₁ leaf right₃@(node key₃ _ left₂ right₂)) key value (t-right x₁ a b ti) (r-right x ri) =
       t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri)
 RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ a b ti) (r-right x ())
 RTtoTI0 (node key₁ _ (node key₃ _ _ _) leaf) (node key₁ _ (node key₃ value₃ _ _) (node key value leaf leaf)) key value (t-left x₁ a b ti) (r-right x r-leaf) =
@@ -518,27 +518,27 @@
       t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃
 RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂  ? ? c d (RTtoTI0 _ _ key value ti ri) ti₁
 
-RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
-     → replacedTree key value tree repl → treeInvariant tree
-RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf
-RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁
-RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x a b ti
-RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x a b ti
-RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ a b c d ti ti₁
--- r-right case
-RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ a b ti) (r-right x r-leaf) = t-single key₁ value₁
-RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) =
-   t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) ? ?  (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂
-RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x r-leaf) =
-    t-left x₁ ? ? ti
-RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) a b ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁
--- r-left case
-RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ a b ti) (r-left x ri) = t-single key₁ value₁
-RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ a b ti) (r-left x ri) =
-   t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁
-RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right x₂ c d ti₁
-RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) =
-    t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? c d (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
+-- RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
+--      → replacedTree key value tree repl → treeInvariant tree
+-- RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf
+-- RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁
+-- RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x a b ti
+-- RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x a b ti
+-- RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ a b c d ti ti₁
+-- -- r-right case
+-- RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ a b ti) (r-right x r-leaf) = t-single key₁ value₁
+-- RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) =
+--    t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) ? ?  (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂
+-- RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x r-leaf) =
+--     t-left x₁ ? ? ti
+-- RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) a b ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁
+-- -- r-left case
+-- RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ a b ti) (r-left x ri) = t-single key₁ value₁
+-- RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ a b ti) (r-left x ri) =
+--    t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁
+-- RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right x₂ c d ti₁
+-- RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) =
+--     t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? c d (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
 
 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
      → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t
@@ -551,7 +551,7 @@
                (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt }
        $  λ p P1 loop → replaceP key value  (proj2 (proj2 p)) (proj1 p) P1
             (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1  ⟫ ⟫ P2 lt )
-       $ λ tree repl P → exit tree repl {!!} --exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫
+       $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫
 
 insertTestP1 = insertTreeP leaf 1 1 t-leaf
   $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0)