Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 627:967547859521

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Nov 2021 23:17:35 +0900
parents 6465673df5bc
children ec2506b532ba
comparison
equal deleted inserted replaced
626:6465673df5bc 627:967547859521
96 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 96 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
97 97
98 treeInvariantTest1 : treeInvariant (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf))) 98 treeInvariantTest1 : treeInvariant (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf)))
99 treeInvariantTest1 = {!!} 99 treeInvariantTest1 = {!!}
100 100
101 data stackInvariant {n : Level} {A : Set n} : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where 101 data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where
102 s-nil : stackInvariant leaf leaf [] 102 s-nil : stackInvariant key0 leaf leaf []
103 s-single : (tree : bt A) → stackInvariant tree tree (tree ∷ [] ) 103 s-single : (tree : bt A) → stackInvariant key0 tree tree (tree ∷ [] )
104 s-< : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)} 104 s-< : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)}
105 → stackInvariant (node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant tree tree0 (tree ∷ node key value left tree ∷ st ) 105 → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value left tree ∷ st )
106 s-> : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)} 106 s-> : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)}
107 → stackInvariant (node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant tree tree0 (tree ∷ node key value tree right ∷ st ) 107 → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value tree right ∷ st )
108 108
109 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where 109 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where
110 r-leaf : replacedTree key value leaf (node key value leaf leaf) 110 r-leaf : replacedTree key value leaf (node key value leaf leaf)
111 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 111 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
112 r-right : {k : ℕ } {v : A} → {t t1 t2 : bt A} 112 r-right : {k : ℕ } {v : A} → {t t1 t2 : bt A}
113 → k > key → ( replacedTree key value t1 t2 → replacedTree key value (node k v t t1) (node k v t t2) ) 113 → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v t t1) (node k v t t2)
114 r-left : {k : ℕ } {v : A} → {t t1 t2 : bt A} 114 r-left : {k : ℕ } {v : A} → {t t1 t2 : bt A}
115 → k < key → ( replacedTree key value t1 t2 → replacedTree key value (node k v t1 t) (node k v t2 t) ) 115 → k < key → replacedTree key value t1 t2 → replacedTree key value (node k v t1 t) (node k v t2 t)
116 116
117 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) 117 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
118 → treeInvariant tree ∧ stackInvariant tree tree0 stack 118 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
119 → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) 119 → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t )
120 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant tree1 tree0 stack → t ) → t 120 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t
121 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st {!!} 121 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st {!!}
122 findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁ 122 findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁
123 findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st {!!} 123 findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st {!!}
124 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} {!!} 124 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} {!!}
125 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} {!!} 125 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} {!!}
128 → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t 128 → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t
129 replaceNodeP k v leaf P next = next (node k v leaf leaf) {!!} {!!} 129 replaceNodeP k v leaf P next = next (node k v leaf leaf) {!!} {!!}
130 replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!} 130 replaceNodeP k v (node key value t t₁) P next = next (node k v t t₁) {!!} {!!}
131 131
132 replaceP : {n m : Level} {A : Set n} {t : Set m} 132 replaceP : {n m : Level} {A : Set n} {t : Set m}
133 → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant repl tree stack ∧ replacedTree key value tree repl 133 → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant key repl tree stack ∧ replacedTree key value tree repl
134 → (next : ℕ → A → (tree1 repl : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant repl tree1 stack ∧ replacedTree key value tree1 repl → bt-depth tree1 < bt-depth tree → t ) 134 → (next : ℕ → A → (tree1 repl : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key repl tree1 stack ∧ replacedTree key value tree1 repl → bt-depth tree1 < bt-depth tree → t )
135 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 135 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
136 replaceP key value tree repl [] Pre next exit = exit tree repl {!!} 136 replaceP key value tree repl [] Pre next exit = exit tree repl {!!}
137 replaceP key value tree repl (leaf ∷ st) Pre next exit = next key value tree {!!} st {!!} {!!} 137 replaceP key value tree repl (leaf ∷ st) Pre next exit = next key value tree {!!} st {!!} {!!}
138 replaceP key value tree repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 138 replaceP key value tree repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
139 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) {!!} st {!!} {!!} 139 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) {!!} st {!!} {!!}
173 RTtoTI1 = {!!} 173 RTtoTI1 = {!!}
174 174
175 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree 175 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
176 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t 176 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t
177 insertTreeP {n} {m} {A} {t} tree key value P exit = 177 insertTreeP {n} {m} {A} {t} tree key value P exit =
178 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , {!!} ⟫ 178 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , {!!} ⟫
179 $ λ p P loop → findP key (proj1 p) tree (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 179 $ λ p P loop → findP key (proj1 p) tree (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t , s ⟫ {!!} lt )
180 $ λ t _ s P → replaceNodeP key value t (proj1 P) 180 $ λ t _ s P → replaceNodeP key value t (proj1 P)
181 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) 181 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
182 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } 182 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant key (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
183 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ proj1 P , ⟪ {!!} , R ⟫ ⟫ 183 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ proj1 P , ⟪ {!!} , R ⟫ ⟫
184 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!} 184 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
185 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit 185 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit
186 186
187 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A 187 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A
189 top-value (node key value tree tree₁) = just value 189 top-value (node key value tree tree₁) = just value
190 190
191 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ 191 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
192 insertTreeSpec0 _ _ _ = tt 192 insertTreeSpec0 _ _ _ = tt
193 193
194 record findPR {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where 194 record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where
195 field 195 field
196 tree0 : bt A 196 tree0 : bt A
197 ti : treeInvariant tree0 197 ti : treeInvariant tree0
198 si : stackInvariant tree tree0 stack 198 si : stackInvariant key tree tree0 stack
199 ci : C tree stack 199 ci : C tree stack
200 200
201 findPP : {n m : Level} {A : Set n} {t : Set m} 201 findPP : {n m : Level} {A : Set n} {t : Set m}
202 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 202 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
203 → (Pre : findPR tree stack (λ t s → Lift n ⊤)) 203 → (Pre : findPR key tree stack (λ t s → Lift n ⊤))
204 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 (λ t s → Lift n ⊤) → bt-depth tree1 < bt-depth tree → t ) 204 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 (λ t s → Lift n ⊤) → bt-depth tree1 < bt-depth tree → t )
205 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR tree1 stack1 (λ t s → Lift n ⊤) → t) → t 205 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR key tree1 stack1 (λ t s → Lift n ⊤) → t) → t
206 findPP key leaf st Pre next exit = exit leaf st (case1 refl) Pre 206 findPP key leaf st Pre next exit = exit leaf st (case1 refl) Pre
207 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁ 207 findPP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
208 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st (case2 {!!}) P 208 findPP key n st P next exit | tri≈ ¬a b ¬c = exit n st (case2 {!!}) P
209 findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c = 209 findPP {_} {_} {A} key n@(node key₁ v tree tree₁) st Pre next exit | tri< a ¬b ¬c =
210 next tree (n ∷ st) (record {ti = findPR.ti Pre ; si = findPP2 st (findPR.si Pre) ; ci = lift tt} ) findPP1 where 210 next tree (n ∷ st) (record {ti = findPR.ti Pre ; si = findPP2 st (findPR.si Pre) ; ci = lift tt} ) findPP1 where
211 tree0 = findPR.tree0 Pre 211 tree0 = findPR.tree0 Pre
212 findPP2 : (st : List (bt A)) → stackInvariant {!!} tree0 st → stackInvariant {!!} tree0 (node key₁ v tree tree₁ ∷ st) 212 findPP2 : (st : List (bt A)) → stackInvariant key {!!} tree0 st → stackInvariant key {!!} tree0 (node key₁ v tree tree₁ ∷ st)
213 findPP2 = {!!} 213 findPP2 = {!!}
214 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) 214 findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
215 findPP1 = {!!} 215 findPP1 = {!!}
216 findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st) 216 findPP key n@(node key₁ v tree tree₁) st Pre next exit | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} findPP2 where -- Cond n st → Cond tree₁ (n ∷ st)
217 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁) 217 findPP2 : suc (bt-depth tree₁) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
218 findPP2 = {!!} 218 findPP2 = {!!}
219 219
220 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree 220 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
221 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t 221 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t
222 insertTreePP {n} {m} {A} {t} tree key value P exit = 222 insertTreePP {n} {m} {A} {t} tree key value P exit =
223 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} 223 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!}
224 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 224 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )
225 $ λ t s _ P → replaceNodeP key value t {!!} 225 $ λ t s _ P → replaceNodeP key value t {!!}
226 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) 226 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
227 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } 227 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant key (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
228 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ 228 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫
229 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!} 229 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
230 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit 230 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit
231 231
232 -- findP key tree stack = findPP key tree stack {findPR} → record { ti = tree-invariant tree ; si stack-invariant tree stack } → 232 -- findP key tree stack = findPP key tree stack {findPR} → record { ti = tree-invariant tree ; si stack-invariant tree stack } →
238 tree1 : bt A 238 tree1 : bt A
239 ci : replacedTree key1 value1 tree tree1 239 ci : replacedTree key1 value1 tree tree1
240 240
241 findPPC : {n m : Level} {A : Set n} {t : Set m} 241 findPPC : {n m : Level} {A : Set n} {t : Set m}
242 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 242 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
243 → (Pre : findPR tree stack findP-contains) 243 → (Pre : findPR key tree stack findP-contains)
244 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR tree1 stack1 findP-contains → bt-depth tree1 < bt-depth tree → t ) 244 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 findP-contains → bt-depth tree1 < bt-depth tree → t )
245 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR tree1 stack1 findP-contains → t) → t 245 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR key tree1 stack1 findP-contains → t) → t
246 findPPC = {!!} 246 findPPC = {!!}
247 247
248 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ 248 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
249 containsTree {n} {m} {A} {t} tree tree1 key value P RT = 249 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
250 TerminatingLoopS (bt A ∧ List (bt A) ) 250 TerminatingLoopS (bt A ∧ List (bt A) )
251 {λ p → findPR (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p)) 251 {λ p → findPR key (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p))
252 ⟪ tree1 , [] ⟫ {!!} 252 ⟪ tree1 , [] ⟫ {!!}
253 $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 253 $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )
254 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value {!!} where 254 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma7 {!!} {!!} found? ) where
255 lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } → 255 lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } →
256 replacedTree key value1 tree t1 → stackInvariant t1 tree s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → node-key t1 ≡ just key 256 replacedTree key value1 tree t1 → stackInvariant key t1 tree s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value
257 lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case1 ()) 257 lemma7 = ?
258 lemma7 {key} {value1} {.(node key value1 leaf leaf)} {leaf} r-leaf s (case2 x) = x 258
259 lemma7 {.key₁} {value1} {.(node key₁ value1 s1 s2)} {node key₁ value s1 s2} r-node s or = {!!}
260 lemma7 {key} {value1} {.(node key₁ value s1 _)} {node key₁ value s1 s2} (r-right x r) s or = {!!}
261 lemma7 {key} {value1} {.(node key₁ value _ s2)} {node key₁ value s1 s2} (r-left x r) s or = {!!}
262