content: {-@ LIQUID "--no-totality" @-}
  {-@ LIQUID "--no-termination"   @-}
  
  module Case_lambda_join where
  
  import Language.Haskell.Liquid.Prelude
  import Data.Set (Set (..))
  
  data RBTree a = Leaf | Node Color a !(RBTree a) !(RBTree a)
  data Color    = B | R deriving (Eq)
  
  {-@ rbalBAD, rbalOK :: k:_ -> l:_ -> r:_ -> {v:_ | Join v k l r} @-}
  rbalBAD x l r = case r of
    Node R y b (Node R z c d) -> unsafeError "ASD" -- Node R y (Node B x l b) (Node B z c d)
    Node R z (Node R y b c) d -> Node R y (Node B x l b) (Node B z c d)
  
  rbalOK x l r = case r of
    -- Node R y b (Node R z c d) -> Node R y (Node B x l b) (Node B z c d)
    Node R z (Node R y b c) d -> Node R y (Node B x l b) (Node B z c d)
  
  {-@ measure elems :: RBTree a -> (Set a)
        elems Leaf         = (Set_empty 0)
        elems (Node c k l r) = (Set_cup (Set_sng k) (Set_cup (elems l) (elems r))) 
    @-}
  
  {-@ predicate Union V L R  = elems V = Set_cup (elems L) (elems R)                       @-}
  {-@ predicate Join V X L R = elems V = Set_cup (Set_sng X) (Set_cup (elems L) (elems R)) @-}
  