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

# PVS Bug 551

```Synopsis:        Unprovable TCC for theory actual
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Apr  2 15:50:00 2001
Originator:      Christoph Berg
Organization:    cs.uni-sb.de
Release:         PVS 2.3
Environment:
System:
Architecture:

Description:

Hello,

in the following PVS file, an unprovable TCC is generated for the second
lemma, whereas both lemmas should be equivalent.

-------8<-------
anyfunction[x: real]: theory
begin
anyfunction: real =3D 0
end anyfunction

nonzerofunc: theory
begin
nonzerofunc(x: nonzero_real): real
end nonzerofunc

nonzerotcc: theory
begin
importing anyfunction, nonzerofunc

% this lemma is ok:
nonzero_lemma_ok: lemma
forall (x: real):
x /= 0 implies
let xx = nonzerofunc(x) in anyfunction[xx] = 0

% the following lemma generates an unprovable TCC:
% nonzerolemma_TCC1: OBLIGATION FORALL (x: real): x /= 0
nonzerolemma: lemma
forall (x: real):
x /= 0 implies
anyfunction[nonzerofunc(x)] =3D 0

end nonzerotcc
-------8<---------

Proof summary for theory anyfunction
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

Proof summary for theory nonzerofunc
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

Proof summary for theory nonzerotcc
nonzero_lemma_ok............................proved - complete   [O](0.0=
2 s)
nonzerolemma_TCC1...........................unfinished          [O](0.0=
7 s)
nonzerolemma................................proved - incomplete [O](0.0=
1 s)
Theory totals: 3 formulas, 3 attempted, 2 succeeded (0.10 s)

Grand Totals: 3 proofs, 3 attempted, 2 succeeded (0.10 s)

Christoph Berg

How-To-Repeat: