$$$unsoundRec.pvs
% W.H. Hesselink, September 2004
% a proof of false, but neglecting a TCC

unsoundRec: THEORY

BEGIN 
  n, k: VAR nat

  f(n): RECURSIVE nat = f(n+1)+1 
    MEASURE LAMBDA n: n

  large: LEMMA
    f(n) >= k

  contradiction: LEMMA
    false

END unsoundRec

$$$unsoundRec.prf
(|unsoundRec| (|f_TCC1| "" (TERMINATION-TCC))
 (|large| "" (INDUCT "k")
  (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL)
   ("2" (SKOSIMP)
    (("2" (SKOLEM!)
      (("2" (EXPAND "f" +) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|contradiction| "" (USE "large" ("n" "0" "k" "f(0)+1"))
  (("" (ASSERT) NIL NIL)) NIL))