# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1706519754 -32400
# Node ID cfdb145f1581d099267fcfbc543a4e392a42bf7d
# Parent  02f431665ebc08752b742f005effb2b28e929eac
...

diff -r 02f431665ebc -r cfdb145f1581 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Mon Jan 29 11:42:39 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jan 29 18:15:54 2024 +0900
@@ -634,34 +634,6 @@
        → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)
        → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄))
 
--- data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
---  rtt-unit : {t : bt A} → rotatedTree t t
---  rtt-node : {left left' right right' : bt A} → {ke : ℕ} {ve : A} → 
---      rotatedTree left left' → rotatedTree right right' → rotatedTree (node ke ve left right) (node ke ve left' right')
---  --     a              b
---  --   b   c          d   a
---  -- d   e              e   c
---  --
---  rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
---    --kd < kb < ke < ka< kc
---   → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A}
---   → kd < kb → kb < ke → ke < ka → ka < kc
---   → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
---   → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
---   → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
---   → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
---    (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
--- 
---  rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
---    --kd < kb < ke < ka< kc
---   → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child
---   → kd < kb → kb < ke → ke < ka → ka < kc
---   → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
---   → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
---   → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
---   → rotatedTree  (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
---   (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
---   
 RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A)
 RightDown leaf = leaf
 RightDown (node key ⟪ c , value ⟫ t1 t2) = t2