% Trivial PVS example by David A. Wheeler

mortality: THEORY
 BEGIN
  man: TYPE+              % The "+" means there's at least one man.
  mortal(m: man): bool    % Returns True if m is mortal.

  % Socrates is a man.
  Socrates: man

  % All men are mortal.
  all_men_mortal: AXIOM FORALL (m: man): mortal(m)

  % Socrates is mortal.
  socrates_mortal: CLAIM mortal(Socrates)

  % Prove using:    (rewrite "all_men_mortal")
  % or:             (grind :rewrites ("all_men_mortal"))

  % In normal PVS use it'd be better to omit the axiom and say:
  %      mortal(m: man): bool = true
  % but this tries to stay close to the traditional example.
END mortality