The Leastness Correctness Property:

  
   LEAST(xs, n) ==   (i)  n in xs   
                     and
                     (ii) n is <= all the ints in  xs

"int  n  is in  int list  xs  and it is the least int in  xs"

(* (small xs)  returns the least int in *nonempty* intlist  xs :
         Forall arg: int list, 
            if arg != []
            then  Exists ans : int, such that  LEAST(arg, ans).
*)
fun small [] = raise EmptyListException   (* ensures  arg != []  *)

|   small [x] = x    (* "basis case" for nonempty lists:
                           LEAST([x], x)  holds true  because
                           (i)  x  in  [x]
                           (ii) x  is <= all the ints in  [x]  *)
                      
|   small (x::xs) =  (* "induction case" for lists with 2+ ints:  *)
                     let val a = (small xs)
                         (* LEAST(xs, a)  holds true here --- "induction hypothesis" *)

                     in  if  x < a 
                         then (*return*)  x
                         (* EXPLAIN why  LEAST(x::xs, x)  holds true.
                            USE (i) and (ii) of LEAST(xs, a) to explain:
                         
                         We know that: x < a      <-- from the if-test
                                       a in xs    <-- from (i) of induction hypothesis
                                       a <= all ints in xs  <-- from (ii) of ind. hyp.

                         So, it follows that:
                               (I)   x in (x::xs)   <-- obvious!
                               (II)  x <= all ints in (x::xs)  <-- because x < a
                                                                   and (ii) just above

                         So,  LEAST(x::xs, x)  holds true in this case.
                         *)


                         else (*return*)  a
                         (* EXPLAIN why  LEAST(x::xs, a)  holds true.
                            USE (i) and (ii) of LEAST(xs, a) to explain:
                         
                         We know that: a <= x     <-- from the if-test
                                       a in xs    <-- from (i) of induction hypothesis
                                       a <= all ints in xs  <-- from (ii) of ind. hyp.

                         So, it follows that:
                               (I)   a in (x::xs)   <-- from (i) just above
                               (II)  a <= all ints in (x::xs)  <-- because a <= x
                                                                   and (ii) just above

                         So,  LEAST(x::xs, a)  holds true in this case.
                         *)

      (* In both arms of if-then-else, we proved LEAST(x::xs, answer) *)
(* In all equations of  small,  we proved  LEAST(arg, answer) *)