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

PVS Bug 1015


Synopsis:        show-expanded-form switches between AND and booleans.AND
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Nov 27 10:15:01 2007
Originator:      Hendrik Tews
Organization:    cs.ru.nl
Release:         PVS 4.1
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  typecheck the appended theory and do C-u C-. on x. Some of the
  conjunctions will be displayes in functional notation with
  booleans.AND and some with inlined AND.
  
  A canonical representation in the expanded forms would make it
  much easier to check for differences in formulas during proof
  (with show-expanded-sequent and compare-windows).
  
  
  Bye,
  
  Hendrik
  
  
  A[T : Type] : Theory
  Begin
    path_list?(l : list[T]) : bool
    path?(l : list[T]) : bool
  
    x : Lemma Forall(P : PRED[T], R : PRED[[T,T]], x,y : T) :
       Forall(l : list[T]) : 
           (every(P)(l) and path_list?(l) AND 
                  car(l) = x AND
                  nth(l, length(l) - 1) = y AND
                  (FORALL (i: below(length(l) - 1)):
                    R(nth(l, i), nth(l, i + 1)))) 
       IFF
          (path?(l) AND car(l) = x AND nth(l, length(l) - 1) = y)
  
  End A

How-To-Repeat: 

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