FDL > PVS > Number Theory > max bounded posnat > max : const-decl

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