abbreviation R where"R l a r \ Node l (a, Red) r" abbreviation B where"B l a r \ Node l (a, Black) r"
fun baliL :: "'a rbt \ 'a \ 'a rbt \ 'a rbt" where "baliL (R (R t1 a t2) b t3) c t4 = R (B t1 a t2) b (B t3 c t4)" | "baliL (R t1 a (R t2 b t3)) c t4 = R (B t1 a t2) b (B t3 c t4)" | "baliL t1 a t2 = B t1 a t2"
fun baliR :: "'a rbt \ 'a \ 'a rbt \ 'a rbt" where "baliR t1 a (R t2 b (R t3 c t4)) = R (B t1 a t2) b (B t3 c t4)" | "baliR t1 a (R (R t2 b t3) c t4) = R (B t1 a t2) b (B t3 c t4)" | "baliR t1 a t2 = B t1 a t2"
fun paint :: "color \ 'a rbt \ 'a rbt" where "paint c Leaf = Leaf" | "paint c (Node l (a,_) r) = Node l (a,c) r"
fun baldL :: "'a rbt \ 'a \ 'a rbt \ 'a rbt" where "baldL (R t1 a t2) b t3 = R (B t1 a t2) b t3" | "baldL t1 a (B t2 b t3) = baliR t1 a (R t2 b t3)" | "baldL t1 a (R (B t2 b t3) c t4) = R (B t1 a t2) b (baliR t3 c (paint Red t4))" | "baldL t1 a t2 = R t1 a t2"
fun baldR :: "'a rbt \ 'a \ 'a rbt \ 'a rbt" where "baldR t1 a (R t2 b t3) = R t1 a (B t2 b t3)" | "baldR (B t1 a t2) b t3 = baliL (R t1 a t2) b t3" | "baldR (R t1 a (B t2 b t3)) c t4 = R (baliL (paint Red t1) a t2) b (B t3 c t4)" | "baldR t1 a t2 = R t1 a t2"
fun join :: "'a rbt \ 'a rbt \ 'a rbt" where "join Leaf t = t" | "join t Leaf = t" | "join (R t1 a t2) (R t3 c t4) =
(case join t2 t3 of
R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
t23 \<Rightarrow> R t1 a (R t23 c t4))" | "join (B t1 a t2) (B t3 c t4) =
(case join t2 t3 of
R u2 b u3 \<Rightarrow> R (B t1 a u2) b (B u3 c t4) |
t23 \<Rightarrow> baldL t1 a (B t23 c t4))" | "join t1 (R t2 a t3) = R (join t1 t2) a t3" | "join (R t1 a t2) t3 = R t1 a (join t2 t3)"
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
