Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 778:4d71d0894cfa

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, 22 May 2023 19:06:08 +0900
parents 8e5159a02b76
children 7e5dfe642064 0b791ae19543
comparison
equal deleted inserted replaced
777:8e5159a02b76 778:4d71d0894cfa
729 → RBtreeInvariant orig d0 729 → RBtreeInvariant orig d0
730 → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack ) 730 → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack )
731 → RBtreeInvariant tree ds ∧ RBtreeInvariant (PG.parent pg) dp ∧ RBtreeInvariant (PG.grand pg) dg 731 → RBtreeInvariant tree ds ∧ RBtreeInvariant (PG.parent pg) dp ∧ RBtreeInvariant (PG.grand pg) dg
732 PGtoRBinvariant = {!!} 732 PGtoRBinvariant = {!!}
733 733
734 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree0 : bt (Color ∧ A) ) 734 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
735 → (stack : List (bt (Color ∧ A)))
736 → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack
735 → {d : ℕ} → RBtreeInvariant tree0 d 737 → {d : ℕ} → RBtreeInvariant tree0 d
736 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack 738 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
739 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
737 → {d1 : ℕ} → RBtreeInvariant tree1 d1 740 → {d1 : ℕ} → RBtreeInvariant tree1 d1
738 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t 741 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
739 findRBT = {!!} 742 findRBT {_} {_} {A} {t} key tree0 leaf stack ti {d} rb0 exit = ?
743 findRBT {_} {_} {A} {t} key tree0 (node key₁ value left right) stack ti {d} rb0 exit with <-cmp key key₁
744 ... | tri< a ¬b ¬c = ?
745 ... | tri≈ ¬a b ¬c = ?
746 ... | tri> ¬a ¬b c = ?
740 747
741 rotateLeft : {n m : Level} {A : Set n} {t : Set m} 748 rotateLeft : {n m : Level} {A : Set n} {t : Set m}
742 → (key : ℕ) → (value : A) 749 → (key : ℕ) → (value : A)
743 → (orig tree : bt (Color ∧ A)) 750 → (orig tree : bt (Color ∧ A))
744 → (stack : List (bt (Color ∧ A))) 751 → (stack : List (bt (Color ∧ A)))