# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1575622098 -32400
# Node ID 8ab2e2f9469f516f88c694f47141bceaea0d56d3
# Parent  7c424dd0945d09012598e8e0d210ded64e974706
use <=

diff -r 7c424dd0945d -r 8ab2e2f9469f hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Fri Dec 06 17:39:37 2019 +0900
+++ b/hoareBinaryTree.agda	Fri Dec 06 17:48:18 2019 +0900
@@ -69,24 +69,24 @@
 data bt' {n : Level} (A : Set n) : (key : ℕ) →  Set n where --  (a : Setn)
   bt'-leaf : (key : ℕ) → bt' A key
   bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
-             bt' {n} A l  → bt' {n} A r → l < key → key < r → bt' A key
+             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'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key < 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
 
 
-test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s (s≤s z≤n))))
+test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s {!!})))
 
 bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A )
     → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
 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 a )  ∷ stack)  next
+         bt-find' key tree ( (bt'-left key {key₁} tr {!!} )  ∷ 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 c )  ∷ stack)  next
+         bt-find' key tree ( (bt'-right key {key₁} tr {!!} )  ∷ stack)  next
 
 a<sa : { a : ℕ } → a < suc a
 a<sa {zero} = s≤s z≤n
@@ -104,10 +104,8 @@
          bt-replace0 node (bt'-left key x x₁ ∷ stack) = {!!}
          bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!}
          bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t
-         bt-replace1 zero (bt'-leaf key0) = bt-replace0 (bt'-node (suc zero) value
-              (bt'-leaf zero) (bt'-leaf (suc (suc zero))) {!!} {!!}) stack
-         bt-replace1 (suc tn) (bt'-leaf key0) = bt-replace0 (bt'-node (suc tn) value
-              (bt'-leaf tn) (bt'-leaf (suc (suc tn)) ){!!} {!!}) stack
+         bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value
+              (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ){!!} {!!}) 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
@@ -136,7 +134,7 @@
 lleaf1 0<3 a d = bt'-leaf d
 
 test-node1 : bt' ℕ 3
-test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n))))
+test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!})))
 
 
 rleaf : {n : Level} {a : Set n} → bt {n} {a}