# PVS Bug 567

Synopsis: proof does not rerun
Severity: serious
Priority: medium
Responsible: shankar (Natarajan Shankar)
State: analyzed
Class: sw-bug
Arrival-Date: Wed May 16 12:55:00 2001
Originator: Hendrik Tews
Organization: tcs.inf.tu-dresden.de
Release: PVS 2.3
Environment:
System:
Architecture:
Description:
Hi,
consider the following theory
A : Theory
Begin
f(n : nat) : RECURSIVE nat =
if n = 0 then 1 else 1 + f(n-1) endif
MEASURE n
g(n : nat) : nat = n +1
a : Lemma f = g
end A
The following proof script proves lemma a:
;;; Proof for formula A.a
;;; developed with old decision procedures
(""
(EXTENSIONALITY "[nat -> nat]")
(INST -1 "f" "g")
(PROP)
(INDUCT-AND-SIMPLIFY "x_44"))
But if I prove the tcc's first, then extensionality creates a
variable x_46 and the script doesn't run any more. Similarly if I
try to prove the lemma for a second time.
Bye,
Hendrik
How-To-Repeat:
Fix:
[davesc, 7/18/01]
Needs a consistent naming introduction instead of gentemp, similar
to that used for skolem constants. Shankar to deal with.