PVSinduction  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  n:VAR nat

  Ex1: THEOREM
    2*(n+2) <=(n+2)^2

fac(n): RECURSIVE nat =
   (IF n = 0 THEN 1 ELSE n * fac(n-1) ENDIF)
   MEASURE n

  i:VAR upfrom(4)
  Ex2: THEOREM 2^i < fac(i)

  END PVSinduction