Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 837:887d84484e11

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, 18 Mar 2024 15:13:57 +0900
parents 61f56e51ba3d
children 4b8e11846478
comparison
equal deleted inserted replaced
836:61f56e51ba3d 837:887d84484e11
981 RB-repl→ti (node _ ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ ca , v1 ⟫ leaf (node key₃ value₁ t t₁)) key value 981 RB-repl→ti (node _ ⟪ _ , _ ⟫ leaf (node key₁ _ _ _)) (node key₂ ⟪ ca , v1 ⟫ leaf (node key₃ value₁ t t₁)) key value
982 (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-right x trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where 982 (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-right x trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where
983 rr00 : (key₂ < key₃) ∧ tr> key₂ t ∧ tr> key₂ t₁ 983 rr00 : (key₂ < key₃) ∧ tr> key₂ t ∧ tr> key₂ t₁
984 rr00 = RB-repl→ti> _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫ 984 rr00 = RB-repl→ti> _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫
985 RB-repl→ti .(node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) leaf) (node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) (node key₃ value₂ t₂ t₃)) key value 985 RB-repl→ti .(node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) leaf) (node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) (node key₃ value₂ t₂ t₃)) key value
986 (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right x trb) = ? 986 (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right x trb) = t-node _ _ _ x₁ (proj1 rr00) x₂ x₃ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ t-leaf trb) where
987 RB-repl→ti .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node _ ⟪ _ , _ ⟫ (node key₁ _ _ _) _) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-right x trb) = ? 987 rr00 : (key₂ < key₃) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃
988 rr00 = RB-repl→ti> _ _ _ _ _ trb x tt
989 RB-repl→ti .(node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₂ _ _ _)) (node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₄ value₁ t₃ t₄)) key value (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-right x trb) = t-node _ _ _ ? ? ? ? ? ? ? ? where
990 rr00 : (key₃ < key₄) ∧ tr> key₃ t₃ ∧ tr> key₃ t₄
991 rr00 = RB-repl→ti> _ _ _ _ _ trb x ?
988 RB-repl→ti .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key value ti (rbr-left x trb) = ? 992 RB-repl→ti .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key value ti (rbr-left x trb) = ?
989 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-right x trb) = ? 993 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-right x trb) = ?
990 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-left x trb) = ? 994 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key value ti (rbr-black-left x trb) = ?
991 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-ll x trb) = ? 995 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-ll x trb) = ?
992 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-lr x trb) = ? 996 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-lr x trb) = ?