# 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.