Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 679:ce79298f4c00

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, 29 Nov 2021 15:52:08 +0900
parents 8dd9b11aa358
children 83a5c1f1fa4b
comparison
equal deleted inserted replaced
678:8dd9b11aa358 679:ce79298f4c00
292 repl01 : replacedTree key value (replacePR.tree0 Pre) repl 292 repl01 : replacedTree key value (replacePR.tree0 Pre) repl
293 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) 293 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre)
294 repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre) 294 repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre)
295 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen 295 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
296 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ | si-property1 (replacePR.si Pre) 296 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ | si-property1 (replacePR.si Pre)
297 ... | tri< a ¬b ¬c | refl = next key value {{!!}} (node key₁ value₁ repl right ) st Post ≤-refl where 297 ... | tri< a ¬b ¬c | refl = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
298 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 298 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤)
299 Post with replacePR.si Pre 299 Post with replacePR.si Pre
300 ... | s-right x t = {!!} 300 ... | s-right x t = {!!} -- can't happen
301 ... | s-left lt si with si-property1 si | replacePR.ri Pre 301 ... | s-left lt si with si-property1 si | replacePR.ri Pre
302 ... | refl | ri = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si ; ri = {!!} ; ci = lift tt } where 302 ... | refl | ri = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si ; ri = repl04 ; ci = lift tt } where
303 repl03 : replacedTree key value {!!} repl 303 repl04 : replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si) (node key₁ value₁ repl right)
304 repl04 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right)) {!!} (r-left a ri)
305 repl03 : replacedTree key value (child-replaced key value (node key₁ value₁ left right ∷ st) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) repl
304 repl03 = ri 306 repl03 = ri
305 repl02 : replacedTree key value tree (node key₁ value₁ repl right)
306 repl02 = subst (λ k → replacedTree key value (node key₁ value₁ k right) _ ) {!!} ( r-left {!!} ri )
307 ... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl -- can't happen 307 ... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl -- can't happen
308 ... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl 308 ... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
309 309
310 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) 310 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
311 → (r : Index) → (p : Invraiant r) 311 → (r : Index) → (p : Invraiant r)