define Data.Set.Base.singleton x = (Set_sng x)
define Data.Set.Base.union x y = (Set_cup x y)
define Data.Set.Base.intersection x y = (Set_cap x y)
define Data.Set.Base.difference x y = (Set_dif x y)
define Data.Set.Base.empty = (Set_empty 0)
define Data.Set.Base.null x = (Set_emp x)
define Data.Set.Base.member x xs = (Set_mem x xs)
define Data.Set.Base.isSubsetOf x y = (Set_sub x y)
define Data.Set.Base.fromList xs = (listElts xs)
define Data.Set.Internal.singleton x = (Set_sng x)
define Data.Set.Internal.union x y = (Set_cup x y)
define Data.Set.Internal.intersection x y = (Set_cap x y)
define Data.Set.Internal.difference x y = (Set_dif x y)
define Data.Set.Internal.empty = (Set_empty 0)
define Data.Set.Internal.null x = (Set_emp x)
define Data.Set.Internal.member x xs = (Set_mem x xs)
define Data.Set.Internal.isSubsetOf x y = (Set_sub x y)
define Data.Set.Internal.fromList xs = (listElts xs)
define GHC.Real.fromIntegral x = (x)
define GHC.Types.True = (true)
define GHC.Real.div x y = (x / y)
define GHC.Real.mod x y = (x mod y)
define GHC.Classes.not x = (~ x)
define GHC.Base.$ f x = (f x)
define Language.Haskell.Liquid.Bag.get k m = (Map_select m k)
define Language.Haskell.Liquid.Bag.put k m = (Map_store m k (1 + (Map_select m k)))
define Language.Haskell.Liquid.Bag.union m n = (Map_union m n)
define Language.Haskell.Liquid.Bag.empty = (Map_default 0)
define Data.Map.Base.insert k v m = (Map_store m k v)
define Data.Map.Base.select k v = (Map_select m k)
define Language.Haskell.Liquid.String.stringEmp = (stringEmp)
define Data.RString.RString.stringEmp = (stringEmp)
define String.stringEmp = (stringEmp)
define Main.mempty = (mempty)
define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)
define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)
define ProofCombinators.cast x y = (y)
define Liquid.ProofCombinators.cast x y = (y)
define Control.Parallel.Strategies.withStrategy s x = (x)
define Language.Haskell.Liquid.Equational.eq x y = (y)
define GHC.CString.unpackCString# x = x