-- Sergio and Michael
-- Thu Mar 10 14:36:26 PST 2011
-- Updated Thu Apr  7 10:34:02 PDT 2011

import Quantification
import SetFunctions

getMin l | exists m (\m -> m =:= elemOf l &>
              notExists (set1 elemOf l) (\x -> x < m))
          = m
          where m free

withElem e = e:unknown ? unknown:withElem e
elemOf (withElem e) = e

getMin2 l | exists m (\m -> m =:= elemOf l &>
              forall (set1 elemOf l) (\x -> x >= m))
          = m
          where m free

testdata = [3,1,2,4,9,5]
test1 = getMin testdata
test2 = getMin2 testdata