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

Quantifiers



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?

Thank you.

Laurent FERIER
Researcher at FUNDP, Namur -- Belgium
mailto:Laurent.Ferier@info.fundp.ac.be