Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

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.

Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools