% @(#)$Id: answer1.lsl,v 1.2 1997/01/10 22:16:35 leavens Exp $

answer1: trait
  includes unsignedInt
  introduces
    factorial: unsignedInt -> unsignedInt
  asserts \forall n: unsignedInt
    factorial(0) == 1;
    factorial(succ(n)) == succ(n) * factorial(n);

  % The above axioms are stated using a kind of mathematical induction.
  % They cover all the values, technically because of the generated by clause
  % in the trait IntCycle.
  % Another way to do this is to use if-then-else:
  % (we can state this as a checkable consequence by continuing the above)
  implies \forall n: unsignedInt
    factorial(n) == if n = 0 then 1 else n * factorial(pred(n))

  % Would it have been okay to write the following?
  %   factorial(n) == if n = 0 then 1 else n * factorial(n - 1)