SSL fun_below_props.pvs

fun_below_props : THEORY
%------------------------------------------------------------------------
%      by Bruno Dutertre    Royal Holloway & Bedford New College
%------------------------------------------------------------------------

BEGIN

  n, m : VAR nat
  p : VAR posnat

  % ----- Cartesian product of {0 ... n-1} and {0 ... m-1} -----

  cartesian_bijection : THEOREM
 (EXISTS (f: [[below[n], below[m]] -> below[n * m]]): bijective?(f))

  %  ----- Functions from {0 ... n-1} to {0 ... m-1} -----

  empty_domain1    : LEMMA (EXISTS (f: [below[0] -> below[m]]): TRUE)

  empty_domain2    : LEMMA (FORALL (f1, f2: [below[0] -> below[m]]): f1 = f2)

  empty_range      : LEMMA m = 0 IMPLIES 
                             (FORALL (f: [below[p]-> below[m]]): FALSE)

  funset_bijection : THEOREM
 (EXISTS (f: [[below[n] -> below[m]] -> below[m ^ n]]): bijective?(f))

END fun_below_props