# HG changeset patch
# User ryokka
# Date 1575623964 -32400
# Node ID 7fb57243a8c994ec6d574d8ec0a243197e00baaa
# Parent  8ab2e2f9469f516f88c694f47141bceaea0d56d3
fix

diff -r 8ab2e2f9469f -r 7fb57243a8c9 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Fri Dec 06 17:48:18 2019 +0900
+++ b/hoareBinaryTree.agda	Fri Dec 06 18:19:24 2019 +0900
@@ -72,7 +72,7 @@
              bt' {n} A l  → bt' {n} A r → l ≤ key → key ≤ r → bt' A key
 
 data bt'-path {n : Level} (A : Set n) : Set n where --  (a : Setn)
-  bt'-left  : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A
+  bt'-left  : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key)  → bt'-path A
   bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A
 
 
@@ -83,15 +83,19 @@
 bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack  -- no key found
 bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁
 bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c =
-         bt-find' key tree ( (bt'-left key {key₁} tr {!!} )  ∷ stack)  next
+         bt-find' key tree ( (bt'-left key {key₁} tr (<⇒≤ a) )  ∷ stack)  next
 bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack
 bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = 
-         bt-find' key tree ( (bt'-right key {key₁} tr {!!} )  ∷ stack)  next
+         bt-find' key tree ( (bt'-right key {key₁} tr (<⇒≤ c) )  ∷ stack)  next
 
 a<sa : { a : ℕ } → a < suc a
 a<sa {zero} = s≤s z≤n
 a<sa {suc a} = s≤s a<sa 
 
+a≤sa : { a : ℕ } → a ≤ suc a
+a≤sa {zero} =  z≤n
+a≤sa {suc a} = s≤s a≤sa 
+
 pa<a : { a : ℕ } → pred (suc a) < suc a
 pa<a {zero} = s≤s z≤n
 pa<a {suc a} = s≤s pa<a
@@ -101,11 +105,12 @@
 bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where
          bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A ) → t
          bt-replace0 node [] = next node 
-         bt-replace0 node (bt'-left key x x₁ ∷ stack) = {!!}
+         bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!}
+         bt-replace0 {tn} node (bt'-left key (bt'-node key₁ value x x₂ x₃ x₄) x₁ ∷ stack) = bt-replace0 {key₁} (bt'-node key₁ value  node  x₂ {!!} x₄ ) stack
          bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!}
          bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t
          bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value
-              (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ){!!} {!!}) stack
+              (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ) (≤⇒pred≤ ≤-refl) a≤sa) stack
          bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack
 
 bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} → Set n