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