[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

really basic question



Hi,

  I'm trying to prove the theorem "simple" below, but can't get it to go
through. Am I missing something about what this theorem means in PVS?

simple: THEORY

  BEGIN

    UNIVERSE : TYPE+
    PRED : TYPE = [ UNIVERSE -> bool ]

    Q : VAR PRED
    x: VAR UNIVERSE

    simple: THEOREM
      ( ( FORALL x : Q(x) ) => ( EXISTS x : Q(x) ) )

  END simple


Thanks!

-eric


           o----
           | Eric Klavins
           | Postdoctoral Scholar
             Caltech Computer Science
             klavins@cs.caltech.edu
             (626)395-4858