Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 887:e92daa8d617b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
main part start again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 May 2024 10:59:03 +0900
parents 0aac292a5e1c
children 5b6225b81409
comparison
equal deleted inserted replaced
886:0aac292a5e1c 887:e92daa8d617b
1505 → RBtreeInvariant tree0 1505 → RBtreeInvariant tree0
1506 → (tree1 : bt (Color ∧ A)) 1506 → (tree1 : bt (Color ∧ A))
1507 → (stack : List (bt (Color ∧ A))) 1507 → (stack : List (bt (Color ∧ A)))
1508 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack 1508 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
1509 → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t 1509 → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t
1510 replaceRBTNode = ? 1510 replaceRBTNode key value tree0 rbi tree1 stack rbi-stack exit = ?
1511 1511
1512 -- 1512 --
1513 -- RBT is blanced with the stack, simply rebuild tree without rototation 1513 -- RBT is blanced with the stack, simply rebuild tree without rototation
1514 -- 1514 --
1515 rebuildRBT : {n m : Level} {A : Set n} {t : Set m} 1515 rebuildRBT : {n m : Level} {A : Set n} {t : Set m}
1523 → length stack1 < length stack → t ) 1523 → length stack1 < length stack → t )
1524 → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A))) 1524 → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
1525 → stack1 ≡ (orig ∷ []) 1525 → stack1 ≡ (orig ∷ [])
1526 → RBI key value orig repl stack1 1526 → RBI key value orig repl stack1
1527 → t ) → t 1527 → t ) → t
1528 rebuildRBT = ? 1528 rebuildRBT key value orig repl stack r bdepth-eq next exit = ?
1529 1529
1530 insertCase5 : {n m : Level} {A : Set n} {t : Set m} 1530 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
1531 → (key : ℕ) → (value : A) 1531 → (key : ℕ) → (value : A)
1532 → (orig tree : bt (Color ∧ A)) 1532 → (orig tree : bt (Color ∧ A))
1533 → (stack : List (bt (Color ∧ A))) 1533 → (stack : List (bt (Color ∧ A)))