FDL > PVS > Prelude > min_nat : Theory

PVS-2.4 prelude.pvs

min_nat [T: TYPE FROM nat] : THEORY
BEGIN

S: VAR (nonempty?[T])

a: VAR T

x: VAR T

%%(TCC) min_TCC1: OBLIGATION

min(S): {a | 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 FORALL (S:(nonempty?[T]) ) : (min(S) = a) IFF minimum?(a, S)

END min_nat