Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 600:016a8deed93d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix old binary tree
author ryokka
date Wed, 04 Mar 2020 17:51:05 +0900
parents 89fd7cf09b2a
children 803c423c2855
comparison
equal deleted inserted replaced
599:7ae0c25d2b58 600:016a8deed93d
55 -- 55 --
56 -- 56 --
57 -- no children , having left node , having right node , having both 57 -- no children , having left node , having right node , having both
58 -- 58 --
59 data bt {n : Level} (A : Set n) : Set n where 59 data bt {n : Level} (A : Set n) : Set n where
60 bt-leaf : (key : ℕ) → bt A 60 L : bt A
61 bt-node : (key : ℕ) → 61 N : (key : ℕ) →
62 (ltree : bt A) → (rtree : bt A) → bt A 62 (ltree : bt A ) → (rtree : bt A ) → bt A
63 63
64 64
65 data bt-path {n : Level} (A : Set n) : Set n where 65 -- data bt-path {n : Level} (A : Set n) : Set n where
66 bt-left : (key : ℕ) → (bt A ) → bt-path A 66 -- bt-left : (key : ℕ) → (bt A ) → bt-path A
67 bt-right : (key : ℕ) → (bt A ) → bt-path A 67 -- bt-right : (key : ℕ) → (bt A ) → bt-path A
68 68
69 69 data bt-path' {n : Level} (A : Set n) : Set n where
70 bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path A) 70 left : (bt A) → bt-path' A
71 → ( bt A → List (bt-path A) → t ) → t 71 right : (bt A) → bt-path' A
72 bt-find {n} {m} {A} {t} key leaf@(bt-leaf key₁) stack exit = exit leaf stack 72
73 bt-find {n} {m} {A} {t} key (bt-node key₁ tree tree₁) stack next with <-cmp key key₁ 73
74 bt-find {n} {m} {A} {t} key node@(bt-node key₁ tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack 74
75 bt-find {n} {m} {A} {t} key node@(bt-node key₁ ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (bt-left key node ∷ stack) next 75 tree->key : {n : Level} {A : Set n} → (tree : bt A) → ℕ
76 bt-find {n} {m} {A} {t} key node@(bt-node key₁ ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (bt-right key node ∷ stack) next 76 tree->key {n} L = zero
77 77 tree->key {n} (N key tree tree₁) = key
78 78
79 bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt-path A) → (bt A → t ) → t 79 -- path2tree : {n : Level} {A : Set n} → (bt-path' {n} A) → bt A
80 bt-replace {n} {m} {A} {t} ikey otree stack next = bt-replace0 otree where 80 -- path2tree {n} {A} (left x) = x
81 bt-replace1 : bt A → List (bt-path A) → t 81 -- path2tree {n} {A} (right x) = x
82 bt-replace1 tree [] = next tree 82
83 bt-replace1 node (bt-left key (bt-leaf key₁) ∷ stack) = bt-replace1 node stack 83
84 bt-replace1 node (bt-right key (bt-leaf key₁) ∷ stack) = bt-replace1 node stack 84 -- bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path A)
85 bt-replace1 node (bt-left key (bt-node key₁ x x₁) ∷ stack) = bt-replace1 (bt-node key₁ node x₁) stack 85 -- → ( bt A → List (bt-path A) → t ) → t
86 bt-replace1 node (bt-right key (bt-node key₁ x x₁) ∷ stack) = bt-replace1 (bt-node key₁ x node) stack 86 -- bt-find {n} {m} {A} {t} key leaf@(L) stack exit = exit leaf stack
87 bt-replace0 : (tree : bt A) → t 87 -- bt-find {n} {m} {A} {t} key (N key₁ tree tree₁) stack next with <-cmp key key₁
88 bt-replace0 tree@(bt-node key ltr rtr) = bt-replace1 tree stack -- find case 88 -- bt-find {n} {m} {A} {t} key node@(N key₁ tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack
89 bt-replace0 (bt-leaf key) with <-cmp key ikey -- not-find case 89 -- bt-find {n} {m} {A} {t} key node@(N key₁ ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (bt-left key node ∷ stack) next
90 bt-replace0 (bt-leaf key) | tri< a ¬b ¬c = bt-replace1 (bt-node ikey (bt-leaf key) (bt-leaf (suc ikey))) stack 90 -- bt-find {n} {m} {A} {t} key node@(N key₁ ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (bt-right key node ∷ stack) next
91 bt-replace0 (bt-leaf key) | tri≈ ¬a b ¬c = bt-replace1 (bt-node ikey (bt-leaf (pred ikey)) (bt-leaf (suc ikey))) stack 91
92 bt-replace0 (bt-leaf key) | tri> ¬a ¬b c = bt-replace1 (bt-node ikey (bt-leaf (suc ikey)) (bt-leaf (key))) stack 92
93 93 -- bt-find' : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path' A) → ( bt A → List (bt-path' A) → t ) → t
94 -- bt-replace1 (bt-node ikey (bt-leaf {!!}) (bt-leaf {!!})) stack -- not-find case 94 -- bt-find' key leaf@(L) stack exit = exit leaf stack
95 95 -- bt-find' key node@(N key1 lnode rnode) stack exit with <-cmp key key1
96 96 -- bt-find' key node@(N key1 lnode rnode) stack exit | tri≈ ¬a b ¬c = exit node stack
97 bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → (bt A → t ) → t 97 -- bt-find' key node@(N key1 lnode rnode) stack next | tri< a ¬b ¬c = bt-find' key lnode ((left node) ∷ stack) next
98 bt-insert {n} {m} {A} {t} key tree next = bt-find key tree [] (λ tr st → bt-replace key tr st (λ new → next new)) 98 -- bt-find' key node@(N key1 lnode rnode) stack next | tri> ¬a ¬b c = bt-find' key rnode ((right node) ∷ stack) next
99 99
100 100
101 tree->key : {n : Level} {A : Set n} → (tree : bt A ) → ℕ 101 -- find-next : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path' A)
102 tree->key {n} (bt-leaf key) = key 102 -- → (next : bt A → List (bt-path' A) → t ) → (exit : bt A → List (bt-path' A) → t ) → t
103 tree->key {n} (bt-node key tree tree₁) = key 103 -- find-next key leaf@(L) st _ exit = exit leaf st
104 -- find-next key (N key₁ tree tree₁) st next exit with <-cmp key key₁
105 -- find-next key node@(N key₁ tree tree₁) st _ exit | tri≈ ¬a b ¬c = exit node st
106 -- find-next key node@(N key₁ tree tree₁) st next _ | tri< a ¬b ¬c = next tree ((left node) ∷ st)
107 -- find-next key node@(N key₁ tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ ((right node) ∷ st)
108
109 -- find-loop は bt-find' とだいたい一緒(induction してるくらい)
110 -- これも多分 Zコンビネータの一種?
111 -- loop で induction してる hight は現在の木の最大長より大きければよい(find-next が抜けきるため)
112 -- 逆に木の最大長より小さい(たどるルートより小さい)場合は途中経過の値が返る
113
114 -- find-loop : {n m : Level} {A : Set n} {t : Set m} → (hight key : ℕ) → (tree : bt A ) → List (bt-path' A) → (exit : bt A → List (bt-path' A) → t) → t
115 -- find-loop zero key tree st exit = exit tree st
116 -- find-loop (suc h) key lf@(L) st exit = exit lf st
117 -- find-loop (suc h) key tr@(N key₁ tree tree₁) st exit = find-next key tr st ((λ tr1 st1 → find-loop h key tr1 st1 exit)) exit
118
119
120
121 node-ex : {n : Level} {A : Set n} → bt A
122 node-ex {n} {A} = (N zero (L) (L))
123
124 ex : {n : Level} {A : Set n} → bt A
125 ex {n} {A} = (N {n} {A} 8 (N 6 (N 2 (N 1 L L) (N 3 L L)) (N 7 L L)) (N 9 L L))
126
127 exLR : {n : Level} {A : Set n} → bt A
128 exLR {n} {A} = (N {n} {A} 4 (N 2 L (N 3 L L)) (N 5 L L))
129
130 exRL : {n : Level} {A : Set n} → bt A
131 exRL {n} {A} = (N {n} {A} 3 L (N 5 (N 4 L L) L))
132
133
134
135
136 leaf-ex : {n : Level} {A : Set n} → bt A
137 leaf-ex {n} {A} = L
138
139
140
141
142
143
144 findLoopInv : {n m : Level} {A : Set n} {t : Set m} → (orig : bt A) → (modify : bt A )
145 → (stack : List (bt-path' A)) → Set n
146 -- findLoopInv {n} {m} {A} {t} tree mtree [] = tree ≡ mtree
147 -- findLoopInv {n} {m} {A} {t} tree mtree (left (L) ∷ st) = mtree ≡ (L)
148 -- findLoopInv {n} {m} {A} {t} tree mtree (right (L) ∷ st) = mtree ≡ (L)
149 findLoopInv {n} {m} {A} {t} tree mtree [] = tree ≡ mtree
150 findLoopInv {n} {m} {A} {t} tree mtree (left L ∷ st) = mtree ≡ (L)
151 findLoopInv {n} {m} {A} {t} tree mtree (right L ∷ st) = mtree ≡ (L)
152 findLoopInv {n} {m} {A} {t} tree mtree (left (N key x x₁) ∷ st) = mtree ≡ x
153 findLoopInv {n} {m} {A} {t} tree mtree (right (N key x x₁) ∷ st) = mtree ≡ x₁
154
155
156
157
158
159
160
161
162
163 hightMerge : {n m : Level} {A : Set n} {t : Set m} → (l r : ℕ) → (ℕ → t) → t
164 hightMerge lh rh next with <-cmp lh rh
165 hightMerge lh rh next | tri< a ¬b ¬c = next rh
166 hightMerge lh rh next | tri≈ ¬a b ¬c = next lh
167 hightMerge lh rh next | tri> ¬a ¬b c = next lh
168
169 isHightL : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t
170 isHightL L next = next zero
171 isHightL {n} {_} {A} (N key tree tree₁) next = isHightL tree λ x → next (suc x)
172
173 isHightR : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t
174 isHightR L next = next zero
175 isHightR {n} {_} {A} (N key tree tree₁) next = isHightR tree₁ λ x → next (suc x)
176
177 isHight : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t
178 isHight L next = next zero
179 isHight {n} {_} {A} tr@(N key tree tree₁) next = isHightL tr (λ lh → isHightR tr λ rh → hightMerge {n} {_} {A} (suc lh) (suc rh) next)
180
181
182 treeHight : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t
183 treeHight L next = next zero
184 treeHight {n} {_} {A} (N key tree tree₁) next = isHight tree (λ lh → isHight tree₁ (λ rh → hightMerge {n} {_} {A} (lh) (rh) next))
185
186 rhight : {n : Level} {A : Set n} → bt A → ℕ
187 rhight L = zero
188 rhight (N key tree tree₁) with <-cmp (rhight tree) (rhight tree₁)
189 rhight (N key tree tree₁) | tri< a ¬b ¬c = suc (rhight tree₁)
190 rhight (N key tree tree₁) | tri≈ ¬a b ¬c = suc (rhight tree₁)
191 rhight (N key tree tree₁) | tri> ¬a ¬b c = suc (rhight tree)
192
193 leaf≠node : {n : Level} {A : Set n} {a : ℕ} {l r : bt A} → ((N {n} {A} a l r) ≡ L) → ⊥
194 leaf≠node ()
195
196 leafIsNoHight : {n : Level} {A : Set n} (tree : bt A) → tree ≡ L → (treeHight tree (λ x → x) ≡ 0)
197 leafIsNoHight L refl = refl
198
199
200
201 hight-tree : {n : Level} {A : Set n} {k : ℕ} {l r : bt A} → ℕ → (tree : bt A) → Set n
202 hight-tree zero tree = tree ≡ L
203 hight-tree {n} {A} {k} {l} {r} (suc h) tree = tree ≡ (N k l r)
204
205
206 hightIsNotLeaf : {n : Level} {A : Set n} (h : ℕ) → (tree : bt A) → (h ≡ 0 ) ∧ (h ≡ treeHight tree (λ x → x)) → (tree ≡ L)
207 hightIsNotLeaf .0 tree record { proj1 = refl ; proj2 = p2 } = {!!}
208
209 -- leaf≡0 : {n : Level} {A : Set n} (tree : bt A) → (rhight tree ≡ 0) → tree ≡ L
210 -- leaf≡0 L _ = refl
211
212
213
214
215
216
217
218
219
220 find-hoare-next : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mt : bt A ) → (st : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree mt st)
221 → (next : (nt : bt A) → (ns : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree nt ns) → t )
222 → (exit : (nt : bt A) → (ns : List (bt-path' A)) → (nt ≡ L) ∨ (key ≡ tree->key nt) → t ) → t
223 find-hoare-next key leaf@(L) mt st eq _ exit = exit leaf st (case1 refl)
224 find-hoare-next key (N key₁ tree tree₁) mt st eq next exit with <-cmp key key₁
225 find-hoare-next key node@(N key₁ tree tree₁) mt st eq _ exit | tri≈ ¬a b ¬c = exit node st (case2 b)
226 find-hoare-next key node@(N key₁ tree tree₁) mt st eq next _ | tri< a ¬b ¬c = next tree ((left node) ∷ st) refl
227 find-hoare-next key node@(N key₁ tree tree₁) mt st eq next _ | tri> ¬a ¬b c = next tree₁ ((right node) ∷ st) refl
228
229 find-hoare-loop : {n m : Level} {A : Set n} {t : Set m} → (hight key : ℕ) → (tree mt : bt A ) → (st : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree mt st)
230 → (exit : (nt : bt A) → (ns : List (bt-path' A)) → (nt ≡ L) ∨ (key ≡ tree->key nt) → t) → t
231 find-hoare-loop zero key tree mt st eq exit with key ≟ (tree->key tree)
232 find-hoare-loop zero key tree mt st eq exit | yes p = exit tree st (case2 p)
233 find-hoare-loop zero key tree mt st eq exit | no ¬p = exit tree st (case1 {!!})
234
235 find-hoare-loop (suc h) key otr lf@(L) st eq exit = exit lf st (case1 refl)
236 find-hoare-loop (suc h) key otr tr@(N key₁ tree tree₁) st eq exit = find-hoare-next key otr tr st {!!} ((λ tr1 st1 eq → find-hoare-loop h key otr tr1 st1 {!!} exit)) exit
237
238
239 -- bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt-path A) → (bt A → t ) → t
240 -- bt-replace {n} {m} {A} {t} ikey otree stack next = bt-replace0 otree where
241 -- bt-replace1 : bt A → List (bt-path A) → t
242 -- bt-replace1 tree [] = next tree
243 -- bt-replace1 node (bt-left key (L) ∷ stack) = bt-replace1 node stack
244 -- bt-replace1 node (bt-right key (L) ∷ stack) = bt-replace1 node stack
245 -- bt-replace1 node (bt-left key (N key₁ x x₁) ∷ stack) = bt-replace1 (N key₁ node x₁) stack
246 -- bt-replace1 node (bt-right key (N key₁ x x₁) ∷ stack) = bt-replace1 (N key₁ x node) stack
247 -- bt-replace0 : (tree : bt A) → t
248 -- bt-replace0 tree@(N key ltr rtr) = bt-replace1 tree stack -- find case
249 -- bt-replace0 (L) = {!!}
250
251
252
253 -- bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → (bt A → t ) → t
254 -- bt-insert {n} {m} {A} {t} key tree next = bt-find key tree [] (λ tr st → bt-replace key tr st (λ new → next new))
255
104 256
105 {-- 257 {--
106 find でステップ毎にみている node と stack の top を一致させる 258 [ok] find でステップ毎にみている node と stack の top を一致させる
107 find 中はnode と stack の top が一致する(root に来た時 stack top がなくなる) 259 [ok] find 中はnode と stack の top が一致する(pre は stack の中身がなく, post は stack の top とずれる)
108 -- どうやって経路の入ったstackを手に入れるか?(find 実行後でよい?) 260
109 tree+stack≡tree は find 後の tree と stack をもって 261 tree+stack≡tree は find 後の tree と stack をもって
110 reverse した stack を使って find をチェックするかんじ? 262 reverse した stack を使って find をチェックするかんじ?
111 --} 263 --}
112 264
113 265 {--
114 tree+stack : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A ) 266 tree+stack は tree と stack を受け取ってひとしさ(関係)を返すやつ
115 → (stack : List (bt-path A)) → Set n 267
116 tree+stack tree mtree [] = tree ≡ mtree -- fin case 268 --}
117 tree+stack {n} {m} {A} {t} tree mtree@(bt-leaf key1) (bt-left key x ∷ stack) = (mtree ≡ x) -- unknow case 269
118 tree+stack {n} {m} {A} {t} tree mtree@(bt-leaf key₁) (bt-right key x ∷ stack) = (mtree ≡ x) -- we nofound leaf's left, right node 270 -- tree+stack : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A )
119 tree+stack {n} {m} {A} {t} tree mtree@(bt-node key1 ltree rtree) (bt-left key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree ltree stack) -- correct case 271 -- → (stack : List (bt-path A)) → Set n
120 tree+stack {n} {m} {A} {t} tree mtree@(bt-node key₁ ltree rtree) (bt-right key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree rtree stack) 272 -- tree+stack tree mtree [] = tree ≡ mtree -- fin case
121 273 -- tree+stack {n} {m} {A} {t} tree mtree@(L) (bt-left key x ∷ stack) = (mtree ≡ x) -- unknow case
122 274 -- tree+stack {n} {m} {A} {t} tree mtree@(L) (bt-right key x ∷ stack) = (mtree ≡ x) -- we nofound leaf's left, right node
123 tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A ) 275 -- tree+stack {n} {m} {A} {t} tree mtree@(N key1 ltree rtree) (bt-left key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree ltree stack) -- correct case
124 → (stack : List (bt-path A )) → tree+stack {_} {m} {_} {t} tree mtree (reverse stack) 276 -- tree+stack {n} {m} {A} {t} tree mtree@(N key₁ ltree rtree) (bt-right key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree rtree stack)
125 tree+stack≡tree tree (bt-leaf key) stack = {!!} 277
126 tree+stack≡tree tree (bt-node key rtree ltree) stack = {!!} 278 {--
279 tree+stack
280 2. find loop → "top of reverse stack" ≡ "find route orig tree"
281 --}
282
283 -- s+t≡t : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt-path' {n} A)) → bt-find' key tree stack (λ mt st → s+t {n} {A} tree mt st)
284 -- s+t≡t {n} {m} {A} {t} key (L) [] = refl
285 -- s+t≡t {n} {m} {A} {t} key (L) (left x ∷ []) = refl
286 -- s+t≡t {n} {m} {A} {t} key (L) (left x ∷ x₁ ∷ stack) = refl
287 -- s+t≡t {n} {m} {A} {t} key (L) (right x ∷ []) = refl
288 -- s+t≡t {n} {m} {A} {t} key (L) (right x ∷ x₁ ∷ stack) = refl
289 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] with <-cmp key key₁
290 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl
291 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!}
292 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!}
293 -- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) (x ∷ stack) = {!!}
294
295
296
297 -- s+t : {n : Level} {A : Set n} → (tree mtree : bt A ) → (stack : List (bt-path' {n} A)) → Set n
298 -- s+t tree mtree [] = tree ≡ mtree
299 -- s+t tree mtree (x ∷ []) = tree ≡ mtree
300 -- s+t tr@(L) mt (left x ∷ x₁ ∷ stack) = tr ≡ mt
301 -- s+t {n} {A} tr@(N key tree tree₁) mt (left x ∷ x₁ ∷ stack) = (mt ≡ x) ∧ (s+t {n} {A} tree (path2tree x₁) stack)
302 -- s+t tr@(L) mt (right x ∷ x₁ ∷ stack) = tr ≡ mt
303 -- s+t {n} {A} tr@(N key tree tree₁) mt (right x ∷ x₁ ∷ stack) = (mt ≡ x) ∧ (s+t {n} {A} tree₁ (path2tree x₁) stack)
304
305 -- data treeType {n : Level} (A : Set n) : Set n where
306 -- leaf-t : treeType A
307 -- node-t : treeType A
308
309 -- isType : {n : Level} {A : Set n} → bt A → treeType A
310 -- isType (L) = leaf-t
311 -- isType (N key tree tree₁) = node-t
312
313 -- data findState : Set where
314 -- s1 : findState
315 -- s2 : findState
316 -- sf : findState
317
318 -- findStateP : {n : Level} {A : Set n} → findState → ℕ → bt A → (mnode : bt A) → List (bt-path' A) → Set n
319 -- findStateP s1 key node mnode stack = stack ≡ []
320 -- findStateP s2 key node mnode stack = (s+t node mnode (reverse stack))
321 -- findStateP sf key node mnode stack = (key ≡ (tree->key mnode)) ∨ ((isType mnode) ≡ leaf-t)
322
323 -- findStartPwP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (findStateP s1 key tree mtree [] → t) → t
324 -- findStartPwP key tree mtree next = next refl
325
326
327
328 -- findLoopPwP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (st : List (bt-path' A))
329 -- → (findStateP s2 key tree mtree st)
330 -- → (next : (tr : bt A) → (st : List (bt-path' A)) → (findStateP s2 key tree mtree st) → t)
331 -- → (exit : (tr : bt A) → (st : List (bt-path' A)) → (findStateP sf key tree mtree st) → t ) → t
332 -- findLoopPwP key tree (L) [] state next exit = exit tree [] (case2 refl)
333 -- findLoopPwP key tree (N key₁ mtree mtree₁) [] state next exit = next tree [] {!!}
334 -- findLoopPwP key tree mtree (x ∷ []) state next exit = {!!}
335 -- findLoopPwP key tree (L) (x ∷ x₁ ∷ stack) state next exit = {!!}
336 -- findLoopPwP key tree (N key₁ mtree mtree₁) (left x ∷ x₁ ∷ stack) state next exit =
337 -- next {!!} {!!} {!!}
338 -- findLoopPwP key tree (N key₁ mtree mtree₁) (right x ∷ x₁ ∷ stack) state next exit = {!!}
339
340
341 -- -- tree+stack' {n} {m} {A} {t} (N key ltree rtree) mtree@(N key₁ lmtree rmtree) (x ∷ stack) with <-cmp key key₁
342 -- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) (x ∷ stack) | tri≈ ¬a b ¬c = tt ≡ mt
343 -- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) st@(x ∷ stack) | tri< a ¬b ¬c = (mt ≡ x) ∧ tree+stack' {n} {m} {A} {t} tt lmtree (mt ∷ st)
344 -- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) st@(x ∷ stack) | tri> ¬a ¬b c = (mt ≡ x) ∧ tree+stack' {n} {m} {A} {t} tt rmtree (mt ∷ st)
345
346
347
348 -- tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A )
349 -- → (stack : List (bt-path A )) → tree+stack {_} {m} {_} {t} tree mtree (reverse stack)
350 -- tree+stack≡tree tree (L key) stack = {!!}
351 -- tree+stack≡tree tree (N key rtree ltree) stack = {!!}
352
127 353
128 354
129 -- loop はきっと start, running, stop の3つに分けて考えるといいよね 355 -- loop はきっと start, running, stop の3つに分けて考えるといいよね
130 {-- find status 356 {-- find status
131 1. find start → stack empty 357 1. find start → stack empty
133 or "in reverse stack" ≡ "find route orig tree" 359 or "in reverse stack" ≡ "find route orig tree"
134 3. find fin → "stack Not empty ∧ current node is leaf" 360 3. find fin → "stack Not empty ∧ current node is leaf"
135 or "stack Not empty ∧ current node key ≡ find-key" 361 or "stack Not empty ∧ current node key ≡ find-key"
136 --} 362 --}
137 363
138 find-step : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt-path A)) 364 -- find-step : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A) → (stack : List (bt A))
139 → (next : bt A → List (bt-path A) → (¬ (stack ≡ [])) ∧ (tree ≡ bt-leaf key) → t) 365 -- → (next : (mtree : bt A) → (stack1 : List (bt A)) → (tree+stack' {n} {m} {A} {t} tree mtree stack1 ) → t)
140 → (next : bt A → List (bt-path A) 366 -- → (exit : (mtree : bt A) → List (bt A) → (tree ≡ L (tree->key mtree )) ∨ (key ≡ (tree->key mtree)) → t) → t
141 → ((¬ (stack ≡ [])) ∧ (tree ≡ bt-leaf key) 367 -- find-step {n} {m} {A} {t} key (L) stack next exit = exit (L) stack (case1 refl)
142 ∨ (¬ (stack ≡ [])) ∧ (key ≡ (tree->key tree)) )→ t) → t 368 -- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit with <-cmp key key₁
143 find-step {n} {m} {A} {t} key node stack next exit = {!!} 369 -- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri≈ ¬a b ¬c = exit (N key₁ node node₁) stack (case2 b)
144 370 -- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri< a ¬b ¬c = next node stack {!!}
145 371 -- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri> ¬a ¬b c = next node₁ stack {!!}
146 find-check : {n m : Level} {A : Set n} {t : Set m} → (k : ℕ) → (tree : bt A ) 372
147 → (stack : List (bt-path A )) → bt-find k tree [] (λ mtree mstack → tree+stack {_} {m} {_} {t} tree mtree (reverse mstack)) 373
148 find-check {n} {m} {A} {t} key (bt-leaf key₁) [] = refl 374 -- find-check : {n m : Level} {A : Set n} {t : Set m} → (k : ℕ) → (tree : bt A )
149 find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] with <-cmp key key₁ 375 -- → (stack : List (bt-path A )) → bt-find k tree [] (λ mtree mstack → tree+stack {_} {m} {_} {t} tree mtree (reverse mstack))
150 find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl 376 -- find-check {n} {m} {A} {t} key (L) [] = refl
151 find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!} 377 -- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] with <-cmp key key₁
152 find-check {n} {m} {A} {t} key (bt-node key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!} 378 -- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl
153 find-check {n} {m} {A} {t} key tree (x ∷ stack) = {!!} 379 -- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!}
154 380 -- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!}
155 381 -- find-check {n} {m} {A} {t} key tree (x ∷ stack) = {!!}
156 module ts where 382
157 tbt : {n : Level} {A : Set n} → bt A 383
158 tbt {n} {A} = bt-node {n} {A} 8 (bt-node 6 (bt-node 2 (bt-leaf 1) (bt-leaf 3)) (bt-leaf 7)) (bt-leaf 9) 384 -- module ts where
159 385 -- tbt : {n : Level} {A : Set n} → bt A
160 find : {n : Level} {A : Set n} → ℕ → List (bt-path A) 386 -- tbt {n} {A} = N {n} {A} 8 (N 6 (N 2 (L) (L)) (L)) (L)
161 find {n} {A} key = bt-find key tbt [] (λ x y → y ) 387
162 388 -- find : {n : Level} {A : Set n} → ℕ → List (bt-path A)
163 rep : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A 389 -- find {n} {A} key = bt-find key tbt [] (λ x y → y )
164 rep {n} {m} {A} {t} key = bt-find {n} {_} {A} key tbt [] (λ tr st → bt-replace key tr st (λ mtr → mtr)) 390
165 391 -- find' : {n : Level} {A : Set n} → ℕ → bt A
166 ins : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A 392 -- find' {n} {A} key = bt-find' key tbt [] (λ x y → x )
167 ins {n} {m} {A} {t} key = bt-insert key tbt (λ tr → tr) 393
168 -- 394 -- rep : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A
395 -- rep {n} {m} {A} {t} key = bt-find {n} {_} {A} key tbt [] (λ tr st → bt-replace key tr st (λ mtr → mtr))
396
397 -- ins : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A
398 -- ins {n} {m} {A} {t} key = bt-insert key tbt (λ tr → tr)
399
400 -- test : {n m : Level} {A : Set n} {t : Set m} (key : ℕ)
401 -- → bt-find {n} {_} {A} {_} key tbt [] (λ x y → tree+stack {n} {m} {A} {t} tbt x y)
402 -- test key = {!!}
403 -- --
169 -- 404 --
170 -- no children , having left node , having right node , having both 405 -- no children , having left node , having right node , having both
171 -- 406 --
172 -- data bt' {n : Level} { l r : ℕ } (A : Set n) : (key : ℕ) → Set n where -- (a : Setn) 407 data bt' {n : Level} (A : Set n) : (key : ℕ) → Set n where -- (a : Setn)
173 -- bt'-leaf : (key : ℕ) → bt' A key 408 bt'-leaf : (key : ℕ) → bt' A key
174 -- bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) → 409 bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
175 -- bt' {n} {{!!}} {{!!}} A l → bt' {n} {{!!}} {{!!}} A r → l ≤ key → key ≤ r → bt' A key 410 bt' A l → bt' A r → l ≤ key → key ≤ r → bt' A key
176 411
177 -- data bt'-path {n : Level} (A : Set n) : ℕ → Set n where -- (a : Setn) 412 -- data bt'-path {n : Level} (A : Set n) : ℕ → Set n where -- (a : Setn)
178 -- bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A left-key 413 -- bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A left-key
179 -- bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key 414 -- bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key
180 415
182 -- test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n))) 417 -- test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n)))
183 418
184 419
185 420
186 -- reverse1 : List (bt' A tn) → List (bt' A tn) → List (bt' A tn) 421 -- reverse1 : List (bt' A tn) → List (bt' A tn) → List (bt' A tn)
187 -- reverse1 [] s1 = s1 422 -- reverse1 [] s1 = s1+
188 -- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1) 423 -- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1)
189 -- ... | as = {!!} 424 -- ... | as = {!!}
190 425
191 426
192 427
260 -- (λ st2 → find'-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg) 495 -- (λ st2 → find'-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)
261 496
262 497
263 498
264 -- lleaf : {n : Level} {a : Set n} → bt {n} {a} 499 -- lleaf : {n : Level} {a : Set n} → bt {n} {a}
265 -- lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n) 500 -- lleaf = (L ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
266 501
267 -- lleaf1 : {n : Level} {A : Set n} → (0 < 3) → (a : A) → (d : ℕ ) → bt' {n} A d 502 -- lleaf1 : {n : Level} {A : Set n} → (0 < 3) → (a : A) → (d : ℕ ) → bt' {n} A d
268 -- lleaf1 0<3 a d = bt'-leaf d 503 -- lleaf1 0<3 a d = bt'-leaf d
269 504
270 -- test-node1 : bt' ℕ 3 505 -- test-node1 : bt' ℕ 3
271 -- test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!}))) 506 -- test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!})))
272 507
273 508
274 -- rleaf : {n : Level} {a : Set n} → bt {n} {a} 509 -- rleaf : {n : Level} {a : Set n} → bt {n} {a}
275 -- rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n)))) 510 -- rleaf = (L ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n))))
276 511
277 -- test-node : {n : Level} {a : Set n} → bt {n} {a} 512 -- test-node : {n : Level} {a : Set n} → bt {n} {a}
278 -- test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl ) 513 -- test-node {n} {a} = (N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
279 514
280 -- -- stt : {n m : Level} {a : Set n} {t : Set m} → {!!} 515 -- -- stt : {n m : Level} {a : Set n} {t : Set m} → {!!}
281 -- -- stt {n} {m} {a} {t} = pushSingleLinkedStack [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) ) 516 -- -- stt {n} {m} {a} {t} = pushSingleLinkedStack [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) )
282 517
283 518
284 519
285 -- -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい 520 -- -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい
286 -- -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる 521 -- -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる
287 -- bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t 522 -- bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
288 -- bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing 523 -- bt-search {n} {m} {a} {t} key (L x) cg = cg nothing
289 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d 524 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d
290 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg 525 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
291 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) 526 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
292 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg 527 -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
293 528
294 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg 529 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
295 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) 530 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
296 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg 531 -- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg
297 532
298 533
299 -- -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう 534 -- -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
300 -- bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t 535 -- bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t
301 -- bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node 536 -- bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node
307 -- -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ) 542 -- -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ)
308 -- -- up-some (just (fst , snd)) = just fst 543 -- -- up-some (just (fst , snd)) = just fst
309 -- -- up-some nothing = nothing 544 -- -- up-some nothing = nothing
310 545
311 -- search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} ) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata) 546 -- search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} ) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata)
312 -- search-lem {n} {m} {a} {t} key (bt-leaf x) = refl 547 -- search-lem {n} {m} {a} {t} key (L x) = refl
313 -- search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d 548 -- search-lem {n} {m} {a} {t} key (N d tree₁ tree₂ x x₁) with <-cmp key d
314 -- search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁ 549 -- search-lem {n} {m} {a} {t} key (N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁
315 -- search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl 550 -- search-lem {n} {m} {a} {t} key (N d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl
316 -- search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂ 551 -- search-lem {n} {m} {a} {t} key (N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂
317 552
318 553
319 -- -- bt-find 554 -- -- bt-find
320 -- find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t 555 -- find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
321 556
322 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing 557 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(L x) st cg = cg leaf st nothing
323 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d 558 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N d tree₁ tree₂ x x₁) st cg with <-cmp key d
324 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c)) 559 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(N d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))
325 560
326 -- find-support {n} {m} {a} {t} key node@(bt-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c = 561 -- find-support {n} {m} {a} {t} key node@(N ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c =
327 -- pushSingleLinkedStack st node 562 -- pushSingleLinkedStack st node
328 -- (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg) 563 -- (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg)
329 564
330 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node 565 -- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node
331 -- (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg) 566 -- (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)
332 567
333 -- bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t 568 -- bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t
334 -- bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st 569 -- bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st
335 -- (λ cst → find-support ⦃ l ⦄ ⦃ u ⦄ key tr cst cg) 570 -- (λ cst → find-support ⦃ l ⦄ ⦃ u ⦄ key tr cst cg)
336 571
337 -- find-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → List bt -- ? 572 -- find-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → List bt -- ?
338 -- find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st) 573 -- find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st)
339 -- {-- result 574 -- {-- result
340 -- λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ → 575 -- λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ →
341 -- bt-node 3 (bt-leaf z≤n) (bt-leaf (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ [] 576 -- N 3 (L z≤n) (L (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ []
342 -- --} 577 -- --}
343 578
344 -- find-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) → (st : List (bt {n} {a})) → find-support {{l}} {{u}} d tree st (λ ta st ad → ta ≡ ta) 579 -- find-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) → (st : List (bt {n} {a})) → find-support {{l}} {{u}} d tree st (λ ta st ad → ta ≡ ta)
345 -- find-lem d (bt-leaf x) st = refl 580 -- find-lem d (L x) st = refl
346 -- find-lem d (bt-node d₁ tree tree₁ x x₁) st with <-cmp d d₁ 581 -- find-lem d (N d₁ tree tree₁ x x₁) st with <-cmp d d₁
347 -- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl 582 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl
348 583
349 584
350 -- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with tri< a ¬b ¬c 585 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with tri< a ¬b ¬c
351 -- find-lem {n} {m} {a} {t} {{l}} {{u}} d (bt-node d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!} 586 -- find-lem {n} {m} {a} {t} {{l}} {{u}} d (N d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!}
352 -- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!} 587 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!}
353 -- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!} 588 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!}
354 589
355 -- find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!} 590 -- find-lem d (N d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!}
356 591
357 -- bt-singleton :{n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t 592 -- bt-singleton :{n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t
358 -- bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl) 593 -- bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)
359 594
360 595
361 -- singleton-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? 596 -- singleton-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
362 -- singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x 597 -- singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x
363 598
364 599
365 -- replace-helper : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → t ) → t 600 -- replace-helper : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → t ) → t
366 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree 601 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree
367 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(bt-node d L R x₁ x₂) (bt-leaf x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case 602 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(N d L R x₁ x₂) (L x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case
368 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁ 603 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁
369 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg 604 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ subt x₃ x₄ x₅) st cg
370 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg 605 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ subt x₃ x₄ x₅) st cg
371 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ x₃ subt x₄ x₅) st cg 606 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ x₃ subt x₄ x₅) st cg
372 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case 607 -- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case
373 608
374 609
375 610
376 -- bt-replace : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ 611 -- bt-replace : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄
377 -- → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) 612 -- → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} )
378 -- → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t 613 -- → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t
379 -- bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg 614 -- bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg
380 615
381 616
382 617
383 -- -- 証明に insert がはいっててほしい 618 -- -- 証明に insert がはいっててほしい
384 -- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) 619 -- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a})
385 -- → ((bt {n} {a}) → t) → t 620 -- → ((bt {n} {a}) → t) → t
386 621
387 -- bt-insert {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree cg = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree [] (λ tt st ad → bt-replace ⦃ l ⦄ ⦃ u ⦄ d tt st ad cg ) 622 -- bt-insert {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree cg = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree [] (λ tt st ad → bt-replace ⦃ l ⦄ ⦃ u ⦄ d tt st ad cg )
388 623
389 -- pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ 624 -- pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ
390 -- pickKey (bt-leaf x) = nothing 625 -- pickKey (L x) = nothing
391 -- pickKey (bt-node d tree tree₁ x x₁) = just d 626 -- pickKey (N d tree tree₁ x x₁) = just d
392 627
393 -- insert-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? 628 -- insert-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
394 -- insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x 629 -- insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x
395 630
396 -- insert-test-l : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? 631 -- insert-test-l : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ?
400 -- insert-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) 635 -- insert-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a})
401 -- → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 [] 636 -- → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 []
402 -- (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt) ≡ just d ) ) 637 -- (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt) ≡ just d ) )
403 638
404 639
405 -- insert-lem d (bt-leaf x) with <-cmp d d -- bt-insert d (bt-leaf x) (λ tree1 → {!!}) 640 -- insert-lem d (L x) with <-cmp d d -- bt-insert d (L x) (λ tree1 → {!!})
406 -- insert-lem d (bt-leaf x) | tri< a ¬b ¬c = ⊥-elim (¬b refl) 641 -- insert-lem d (L x) | tri< a ¬b ¬c = ⊥-elim (¬b refl)
407 -- insert-lem d (bt-leaf x) | tri≈ ¬a b ¬c = refl 642 -- insert-lem d (L x) | tri≈ ¬a b ¬c = refl
408 -- insert-lem d (bt-leaf x) | tri> ¬a ¬b c = ⊥-elim (¬b refl) 643 -- insert-lem d (L x) | tri> ¬a ¬b c = ⊥-elim (¬b refl)
409 -- insert-lem d (bt-node d₁ tree tree₁ x x₁) with <-cmp d d₁ 644 -- insert-lem d (N d₁ tree tree₁ x x₁) with <-cmp d d₁
410 -- -- bt-insert d (bt-node d₁ tree tree₁ x x₁) (λ tree1 → {!!}) 645 -- -- bt-insert d (N d₁ tree tree₁ x x₁) (λ tree1 → {!!})
411 -- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d 646 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d
412 -- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) 647 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
413 -- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl 648 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
414 -- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) 649 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
415 650
416 -- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!} 651 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!}
417 -- where 652 -- where
418 -- lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (bt-node d₁ tree tree₁ x x₁ ∷ []) (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄ (bt-node ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (bt-leaf ⦃ {!!} ⦄ ⦃ {!!} ⦄ (≤-reflexive refl)) z≤n (≤-reflexive refl)) st (λ tree1 → find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄ tt₂ ≡ just d))) 653 -- lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (N d₁ tree tree₁ x x₁ ∷ []) (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄ (N ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (L ⦃ {!!} ⦄ ⦃ {!!} ⦄ (≤-reflexive refl)) z≤n (≤-reflexive refl)) st (λ tree1 → find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄ tt₂ ≡ just d)))
419 -- lem-helper = {!!} 654 -- lem-helper = {!!}
420 655
421 -- insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!} 656 -- insert-lem d (N d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!}
422 657