[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Laurent FERIER wrote:
> 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 | email@example.com
CSL, SRI International | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717
- From: Laurent FERIER <firstname.lastname@example.org>