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

Re: Quantifiers

Laurent FERIER wrote:
> 
> Hello!
> 
> I (unsucessfully) tried to prove something in the following form:
> 
>   [-1] (FORALL (t: Time): P(t)
>   [-2] (FORALL (t: FiniteTime): NOT P(t)
>     |--------
> 
> This is trivially true, but I've know no mean to prove it.
> Furthermore, I do not understand the extensionality proof
> commands. Can someone help me?
> 

Presumably, FiniteTime is a subtype of Time. For the
sequent to be true, you need FiniteTime to be nonempty.

In this case, the proof is simply to instantiate formula
-1 and -2 with the same constant of type FiniteTime.
For example, if "0" is of type FiniteTime, just do
(inst - "0")(inst - "0").

You can also do something like 
(inst - "epsilon! (x: FiniteTime): true")
(inst - "epsilon! (x: FiniteTime): true").


-- 
Bruno Dutertre                             | bruno@csl.sri.com
CSL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717