Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 699:59f80c1049e9

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 Sat, 04 Dec 2021 19:51:58 +0900
parents 28e0f7f4777d
children adb7c2101f67
comparison
equal deleted inserted replaced
698:28e0f7f4777d 699:59f80c1049e9
646 lemma7 : (t1 : bt A) ( s1 : List (bt A) ) (tree0 tree1 : bt A) 646 lemma7 : (t1 : bt A) ( s1 : List (bt A) ) (tree0 tree1 : bt A)
647 → replacedTree key value tree1 t1 → stackInvariant key t1 tree0 s1 647 → replacedTree key value tree1 t1 → stackInvariant key t1 tree0 s1
648 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value 648 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value
649 lemma7 .leaf (.leaf ∷ []) .leaf tree1 () s-single (case1 refl) 649 lemma7 .leaf (.leaf ∷ []) .leaf tree1 () s-single (case1 refl)
650 lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ []) .(node key value t1 t2) tree1 ri s-single (case2 x) = {!!} 650 lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ []) .(node key value t1 t2) tree1 ri s-single (case2 x) = {!!}
651 lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-right x si) found = ? 651 lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-right x si) (case2 x₂) = {!!}
652 lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-left x si) found = ? 652 lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-left x si) (case2 x₂) = {!!}
653 653