|
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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
