Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 775:fb74ba4fa38e

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 Thu, 11 May 2023 17:52:58 +0900
parents ebd8a73543dd
children 576b35b1d2d7
comparison
equal deleted inserted replaced
774:ebd8a73543dd 775:fb74ba4fa38e
613 parent grand uncle : bt A 613 parent grand uncle : bt A
614 pg : ParentGrand self parent uncle grand 614 pg : ParentGrand self parent uncle grand
615 rest : List (bt A) 615 rest : List (bt A)
616 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest ) 616 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
617 617
618 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where 618 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where
619 field 619 field
620 od d rd : ℕ 620 od d rd : ℕ
621 tree rot repl : bt (Color ∧ A) 621 tree rot : bt (Color ∧ A)
622 origti : treeInvariant orig 622 origti : treeInvariant orig
623 origrb : RBtreeInvariant orig od 623 origrb : RBtreeInvariant orig od
624 treerb : RBtreeInvariant tree d 624 treerb : RBtreeInvariant tree d
625 replrb : RBtreeInvariant repl rd 625 replrb : RBtreeInvariant repl rd
626 d=rd : ( d ≡ rd ) ∨ ( (suc d ≡ rd ) ∧ (color tree ≡ Red)) 626 d=rd : ( d ≡ rd ) ∨ ( (suc d ≡ rd ) ∧ (color tree ≡ Red))
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 : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → {d d0 : ℕ} 734 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt (Color ∧ A) )
735 → RBtreeInvariant tree0 d0 735 → {d : ℕ} → RBtreeInvariant tree d
736 → RBtreeInvariant tree d ∧ stackInvariant key tree tree0 stack 736 → (exit : (current : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
737 → (next : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) 737 → RBI key value tree current stack → t ) → t
738 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack
739 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
740 findRBT = {!!} 738 findRBT = {!!}
741 739
742 rotateLeft : {n m : Level} {A : Set n} {t : Set m} 740 rotateLeft : {n m : Level} {A : Set n} {t : Set m}
743 → (key : ℕ) → (value : A) → {d0 : ℕ} 741 → (key : ℕ) → (value : A)
744 → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ} 742 → (orig tree : bt (Color ∧ A))
745 → RBtreeInvariant orig d0 743 → (stack : List (bt (Color ∧ A)))
746 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant repl dr 744 → (r : RBI key value orig tree stack )
747 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 745 → (next : (tree1 (bt (Color ∧ A))) → (stack1 : List (bt (Color ∧ A)))
748 → rotatedTree tree rot 746 → (r : RBI key value orig current stack1 )
749 → replacedRBTree key value (child-replaced key rot) repl
750 → (next : {key2 d2 : ℕ} {c2 : Color}
751 → (to tr rot rr : bt (Color ∧ A))
752 → RBtreeInvariant orig d0
753 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr
754 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1
755 → rotatedTree tr rot
756 → replacedRBTree key value (child-replaced key rot) rr
757 → length stack1 < length stack → t ) 747 → length stack1 < length stack → t )
758 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) ) 748 → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
759 → {d : ℕ} → RBtreeInvariant repl d 749 → stack1 ≡ (orig ∷ [])
760 → (ri : rotatedTree orig rot ) → replacedRBTree key value rot repl → t ) → t 750 → RBI key value orig repl stack1
761 rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateLeft1 where 751 → t ) → t
752 rotateLeft {n} {m} {A} {t} key value = ? where
762 rotateLeft1 : t 753 rotateLeft1 : t
763 rotateLeft1 with stackToPG tree orig stack si 754 rotateLeft1 with stackToPG ? orig stack si
764 ... | case1 x = exit {!!} {!!} {!!} {!!} rr 755 ... | case1 x = exit {!!} {!!} {!!} {!!} rr
765 ... | case2 (case1 x) = {!!} 756 ... | case2 (case1 x) = {!!}
766 ... | case2 (case2 pg) = {!!} 757 ... | case2 (case2 pg) = {!!}
767 758
768 rotateRight : {n m : Level} {A : Set n} {t : Set m} 759 rotateRight : {n m : Level} {A : Set n} {t : Set m}
769 → (key : ℕ) → (value : A) → {d0 : ℕ} 760 → (key : ℕ) → (value : A)
770 → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ} 761 → (orig tree : bt (Color ∧ A))
771 → RBtreeInvariant orig d0 762 → (stack : List (bt (Color ∧ A)))
772 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant repl dr 763 → (r : RBI key value orig tree stack )
773 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 764 → (next : (stack1 : List (bt (Color ∧ A)))
774 → rotatedTree tree rot 765 → (r : RBI key value orig stack1 )
775 → replacedRBTree key value (child-replaced key rot) repl
776 → (next : {key2 d2 : ℕ} {c2 : Color}
777 → (to tr rot rr : bt (Color ∧ A))
778 → RBtreeInvariant orig d0
779 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr
780 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1
781 → rotatedTree tr rot
782 → replacedRBTree key value (child-replaced key rot) rr
783 → length stack1 < length stack → t ) 766 → length stack1 < length stack → t )
784 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) ) 767 → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
785 → {d : ℕ} → RBtreeInvariant repl d 768 → stack1 ≡ (orig ∷ [])
786 → (ri : rotatedTree orig rot ) → replacedRBTree key value rot repl → t ) → t 769 → RBI key value orig repl stack1
787 rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateRight1 where 770 → t ) → t
771 rotateRight {n} {m} {A} {t} key value = ? where
788 rotateRight1 : t 772 rotateRight1 : t
789 rotateRight1 with stackToPG tree orig stack si 773 rotateRight1 with stackToPG ? ? ? ?
790 ... | case1 x = {!!} 774 ... | case1 x = {!!}
791 ... | case2 (case1 x) = {!!} 775 ... | case2 (case1 x) = {!!}
792 ... | case2 (case2 pg) = {!!} 776 ... | case2 (case2 pg) = {!!}
793 777
794 insertCase5 : {n m : Level} {A : Set n} {t : Set m} 778 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
795 → (key : ℕ) → (value : A) → {d0 : ℕ} 779 → (key : ℕ) → (value : A)
796 → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ} 780 → (orig tree : bt (Color ∧ A))
797 → RBtreeInvariant orig d0 781 → (stack : List (bt (Color ∧ A)))
798 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant repl dr 782 → (r : RBI key value orig tree stack )
799 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 783 → (next : (tree1 (bt (Color ∧ A))) (stack1 : List (bt (Color ∧ A)))
800 → rotatedTree tree rot 784 → (r : RBI key value orig tree1 stack1 )
801 → replacedRBTree key value (child-replaced key rot) repl
802 → (next : {key2 d2 : ℕ} {c2 : Color}
803 → (to tr rot rr : bt (Color ∧ A))
804 → RBtreeInvariant orig d0
805 → {d : ℕ} → RBtreeInvariant tree d → {dr : ℕ} → RBtreeInvariant rr dr
806 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1
807 → rotatedTree tr rot
808 → replacedRBTree key value (child-replaced key rot) rr
809 → length stack1 < length stack → t ) 785 → length stack1 < length stack → t )
810 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) ) 786 → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
811 → {d : ℕ} → RBtreeInvariant repl d 787 → stack1 ≡ (orig ∷ [])
812 → (ri : rotatedTree orig rot ) → replacedRBTree key value rot repl → t ) → t 788 → RBI key value orig repl stack1
813 insertCase5 {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = insertCase51 where 789 → t ) → t
790 insertCase5 {n} {m} {A} {t} key value = ? where
814 insertCase51 : t 791 insertCase51 : t
815 insertCase51 with stackToPG tree orig stack si 792 insertCase51 with stackToPG ? orig stack ?
816 ... | case1 eq = {!!} 793 ... | case1 eq = {!!}
817 ... | case2 (case1 eq ) = {!!} 794 ... | case2 (case1 eq ) = {!!}
818 ... | case2 (case2 pg) with PG.pg pg 795 ... | case2 (case2 pg) with PG.pg pg
819 ... | s2-s1p2 x x₁ = rotateRight {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit 796 ... | s2-s1p2 x x₁ = ? -- rotateRight {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
820 -- x : PG.parent pg ≡ node kp vp tree n1 797 -- x : PG.parent pg ≡ node kp vp tree n1
821 -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg) 798 -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
822 ... | s2-1sp2 x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit 799 ... | s2-1sp2 x x₁ = ? -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
823 ... | s2-s12p x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit 800 ... | s2-s12p x x₁ = ? -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
824 ... | s2-1s2p x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit 801 ... | s2-1s2p x x₁ = ? -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
825 -- = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 802 -- = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)
826 803
827 804
828 -- if we have replacedNode on RBTree, we have RBtreeInvariant 805 -- if we have replacedNode on RBTree, we have RBtreeInvariant
829 806
830 replaceRBP : {n m : Level} {A : Set n} {t : Set m} 807 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
831 → (key : ℕ) → (value : A) 808 → (key : ℕ) → (value : A)
832 → (orig : bt (Color ∧ A)) 809 → (orig repl : bt (Color ∧ A))
833 → (stack : List (bt (Color ∧ A))) 810 → (stack : List (bt (Color ∧ A)))
834 → (r : RBI key value orig stack ) 811 → (r : RBI key value orig stack )
835 → (next : (stack1 : List (bt (Color ∧ A))) 812 → (next : (stack1 : List (bt (Color ∧ A)))
836 → (r : RBI key value orig stack1 ) 813 → (r : RBI key value orig stack1 )
837 → length stack1 < length stack → t ) 814 → length stack1 < length stack → t )
838 → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A))) 815 → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
839 → stack1 ≡ (orig ∷ []) 816 → stack1 ≡ (orig ∷ [])
840 → RBI key value orig stack1 817 → RBI key value orig stack1
841 → t ) → t 818 → t ) → t
842 replaceRBP = ? 819 replaceRBP {n} {m} {A} {t} key value orig stack r next exit = ? where
843
844 replaceRBP' : {n m : Level} {A : Set n} {t : Set m}
845 → (key : ℕ) → (value : A)
846 → (to tr rot rr : bt (Color ∧ A))
847 → {d0 : ℕ} → RBtreeInvariant to d0
848 → {d : ℕ} → RBtreeInvariant tr d → {dr : ℕ} → RBtreeInvariant rr dr
849 → (stack : List (bt (Color ∧ A))) → stackInvariant key tr to stack
850 → rotatedTree tr rot
851 → replacedRBTree key value (child-replaced key rot) rr
852 → (next : {key2 d2 : ℕ} {c2 : Color}
853 → (to tr rot rr : bt (Color ∧ A))
854 → RBtreeInvariant to d0
855 → {d : ℕ} → RBtreeInvariant tr d → {dr : ℕ} → RBtreeInvariant rr dr
856 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1
857 → rotatedTree tr rot
858 → replacedRBTree key value (child-replaced key rot) rr
859 → length stack1 < length stack → t )
860 → (exit : (rot repl : bt (Color ∧ A) )
861 → {d : ℕ} → RBtreeInvariant repl d
862 → (ri : rotatedTree to rot ) → replacedRBTree key value (child-replaced key rot) repl → t ) → t
863 replaceRBP' {n} {m} {A} {t} key value orig tree rot repl rbio rbit rbir stack si roti ri next exit = ? where
864 insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 820 insertCase2 : (tree parent uncle grand : bt (Color ∧ A))
865 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 821 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack )
866 → (pg : ParentGrand tree parent uncle grand ) → t 822 → (pg : ParentGrand tree parent uncle grand ) → t
867 insertCase2 tree leaf uncle grand stack si (s2-s1p2 () x₁) 823 insertCase2 tree leaf uncle grand stack si (s2-s1p2 () x₁)
868 insertCase2 tree leaf uncle grand stack si (s2-1sp2 () x₁) 824 insertCase2 tree leaf uncle grand stack si (s2-1sp2 () x₁)
869 insertCase2 tree leaf uncle grand stack si (s2-s12p () x₁) 825 insertCase2 tree leaf uncle grand stack si (s2-s12p () x₁)
870 insertCase2 tree leaf uncle grand stack si (s2-1s2p () x₁) 826 insertCase2 tree leaf uncle grand stack si (s2-1s2p () x₁)
871 insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} 827 insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = ? -- next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
872 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = {!!} 828 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = {!!}
873 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} 829 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = ? -- next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
874 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = 830 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = ?
875 insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit 831 -- insertCase5 key value orig tree {!!} rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
876 -- tree is left of parent, parent is left of grand 832 -- tree is left of parent, parent is left of grand
877 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1 833 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
878 -- grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁) 834 -- grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
879 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = 835 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = ?
880 rotateLeft key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} 836 -- rotateLeft key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!}
881 (λ a b c d e f h i j k l m → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit 837 -- (λ a b c d e f h i j k l m → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
882 -- tree is right of parent, parent is left of grand rotateLeft 838 -- tree is right of parent, parent is left of grand rotateLeft
883 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree 839 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
884 -- grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁) 840 -- grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
885 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = 841 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = ?
886 rotateRight key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} 842 -- rotateRight key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!}
887 (λ a b c d e f h i j k l m → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit 843 -- (λ a b c d e f h i j k l m → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
888 -- tree is left of parent, parent is right of grand, rotateRight 844 -- tree is left of parent, parent is right of grand, rotateRight
889 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1 845 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
890 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) 846 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
891 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = 847 insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = ?
892 insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit 848 -- insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
893 -- tree is right of parent, parent is right of grand 849 -- tree is right of parent, parent is right of grand
894 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree 850 -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
895 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) 851 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
896 insertCase1 : t 852 insertCase1 : t
897 insertCase1 with stackToPG tree orig stack si 853 insertCase1 with stackToPG ? orig stack ?
898 ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 854 ... | case1 eq = ? -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri
899 ... | case2 (case1 eq ) = ? where 855 ... | case2 (case1 eq ) = ? where
900 insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant orig d → to ≡ orig 856 insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant orig d → to ≡ orig
901 → (rr : bt (Color ∧ A)) → {dr : ℕ} → RBtreeInvariant repl dr → rr ≡ repl 857 → (rr : bt (Color ∧ A)) → {dr : ℕ} → RBtreeInvariant ? dr → rr ≡ ?
902 → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree to stack ) 858 → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key ? to stack )
903 → stack ≡ tree ∷ to ∷ [] → t 859 → stack ≡ ? ∷ to ∷ [] → t
904 insertCase12 = ? 860 insertCase12 = ?
905 -- exit rot repl rbir ? ? 861 -- exit rot repl rbir ? ?
906 ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 862 ... | case2 (case2 pg) = ? -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)
907 863
908 864
865