-- =============================================================
-- Theory for the sorting problem.
-- =============================================================

-- ********
--! FUNS
-- ********

-- -------------------------------------------------------------
-- The traditional specification of the sorting algorithm.
-- -------------------------------------------------------------

sort :: [a] -> [a]
sort xs = some (\ys -> issorted ys && elementsof ys `equals` elementsof xs)

issorted :: [a] -> Bool
issorted [] = True
issorted (x:xs) = x == minimum (x:xs) && issorted xs

-- ********
--! RULES
-- ********

-- ********
--! CLAUSES
-- ********