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

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: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools