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

PVS Bug 566


Synopsis:        detuple-boundvars
Severity:        serious
Priority:        medium
Responsible:     owre
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,
  
  if I apply detuple-boundvars to 
  
      A[A,B : Type] : Theory
      begin
        a : Lemma Forall(x:[A,B]) : 
  	    Forall(R,S : PRED[[A,B]]) : R(x) IMPLIES S(x)
      end A
  
  I get as second subgoal
  
      a.2 :  
  
        |-------
      {1}   (FORALL (x: [A, B]): FORALL (R, S: PRED[[A, B]]): R(x) IMPLIES S(x)
 )
  	   =
  	   (FORALL (x_42: A), (x_43: B):
  	      FORALL (R, S: PRED[[A, B]]): R(x_42, x_43) IMPLIES S(x_42, x_43))
      [2]   FORALL (x: [A, B]): FORALL (R, S: PRED[[A, B]]): R(x) IMPLIES S(x)
  
  
  So I am required to prove exactly for what I called
  detuple-boundvars. Is this a bug or a feature?
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 
Modified make-compatible-bindings* to generate, in addition to
variables-projections bindings, the variable-tuple binding as well.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools