Mercurial > hg > Members > Moririn
comparison hoareBinaryTree1.agda @ 763:799325a71422
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 06 May 2023 01:25:46 +0900 |
parents | 56de8e7dca7a |
children | 3b4e31a7ccfe |
comparison
equal
deleted
inserted
replaced
762:56de8e7dca7a | 763:799325a71422 |
---|---|
795 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) | 795 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) |
796 insertCase1 : t | 796 insertCase1 : t |
797 insertCase1 with stackToPG tree orig stack si | 797 insertCase1 with stackToPG tree orig stack si |
798 ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri | 798 ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri |
799 ... | case2 (case1 eq ) = ? where | 799 ... | case2 (case1 eq ) = ? where |
800 insertCase12 : (orig : bt (Color ∧ A)) | 800 insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant to d → to ≡ orig |
801 → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree orig stack ) | 801 → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree to stack ) |
802 → stack ≡ tree ∷ orig ∷ [] → t | 802 → stack ≡ tree ∷ to ∷ [] → t |
803 insertCase12 (node k1 ⟪ Red , v1 ⟫ t1 tree) (s-right x s-nil) refl = exit rot repl rbir ? ? | 803 insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node k2 ⟪ Black , v2 ⟫ t1 t2)) (rb-right-red x₁ ro) eq (s-right x s-nil) refl = ? |
804 insertCase12 (node k1 ⟪ Black , v1 ⟫ t1 tree) (s-right x s-nil) refl = ? | 804 insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) leaf) (rb-left-red x₁ ro) eq (s-right x s-nil) refl = ? |
805 insertCase12 (node k1 ⟪ Red , v1 ⟫ tree t1) (s-left x s-nil) refl = ? | 805 insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) (rb-node-red x₁ x₂ ro ro₁) eq (s-right x s-nil) refl = exit (node k1 ⟪ Red , v1 ⟫ t1 rot) (node k1 ⟪ Black , v1 ⟫ ? ?) (rb-node-black ? ? ? ?) |
806 insertCase12 (node k1 ⟪ Black , v1 ⟫ tree t1) (s-left x s-nil) refl = ? | 806 (subst₂ (λ j k → rotatedTree j k ) eq ? (rr-right ? rr-node rr-node roti)) |
807 (subst (λ k → replacedTree key ⟪ ? , value ⟫ ? ?) ? (r-right ? ri)) | |
808 -- k1 < key | |
809 -- ⟪ red , k1 ⟫ | |
810 -- t1 tree → rot → repl | |
811 insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq (s-right x s-nil) refl = ? | |
812 insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq (s-right x s-nil) refl = ? | |
813 insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq (s-right x s-nil) refl = ? | |
814 insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ ro ro₁) eq (s-right x s-nil) refl = ? | |
815 insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node _ ⟪ Black , _ ⟫ _ _)) (rb-right-red x₁ ro) eq (s-left x s-nil) refl = ? | |
816 insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) leaf) (rb-left-red x₁ ro) eq (s-left x s-nil) refl = ? | |
817 insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x₁ x₂ ro ro₁) eq (s-left x s-nil) refl = ? | |
818 insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq (s-left x s-nil) refl = ? | |
819 insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq (s-left x s-nil) refl = ? | |
820 insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq (s-left x s-nil) refl = ? | |
821 insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ ro ro₁) eq (s-left x s-nil) refl = ? | |
807 -- exit rot repl rbir ? ? | 822 -- exit rot repl rbir ? ? |
808 ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) | 823 ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) |
809 | 824 |
810 | 825 |