# PVS Bug 1052

Synopsis: boolean tuples not simplified and strange simplification
Severity: serious
Priority: medium
Responsible: owre
State: open
Class: sw-bug
Arrival-Date: Fri Apr 16 11:35:00 -0700 2010
Originator: Hendrik Tews
Release: PVS 4.2
Organization: os.inf.tu-dresden.de
Environment:
System:
Architecture:
Description:
Hi,
consider the following theory
A : Theory
begin
d : [nat -> bool] = lambda(x:nat): true
g : Lemma Forall(x : [bool, bool]) : x = (true, false) implies (x)`1 =
d(0)
end A
and start the proof of g with (skosimp*) and (replace -1 * LR).
This gives a consequent of (TRUE, FALSE)`1 = d(0).
1. Strangely, assert does now not simplify (TRUE, FALSE)`1 to
TRUE
2. Even more stange a second assert simplifies the consequent to
TRUE = FALSE, which turns g into unprovable.
Bye,
Hendrik
How-To-Repeat:
Fix: