Quelle  min_posnat.pvs

min_posnat: THEORY
BEGIN

  S: VAR (nonempty?[posnat])
  n,a,x: VAR posnat

  min(S): {a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}

  minimum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a <= x)

  min_def        : LEMMA min(S) = a IFF minimum?(a, S)

  min_lem        : LEMMA minimum?(min(S),S)


END min_posnat