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

trivial theorem



I can't prove this:
  bah : LEMMA FORALL (r:real, k1,k2:int) : NOT ( r>0 AND r<1 AND k1+r=k2)
               
bah :

  |-------
{1}    FORALL (r: real, k1, k2: int): NOT((r > 0 AND r < 1 AND k1 + r = k2))

Rule?  (grind)
stty: TCGETS: Operation not supported on socket
stty: TCGETS: Operation not supported on socket
stty: TCGETS: Operation not supported on socket
stty: TCGETS: Operation not supported on socket

Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to:
bah :

{-1}    real_pred(r!1)
{-2}    integer_pred(k1!1)
{-3}    integer_pred(k2!1)
{-4}    r!1 > 0
{-5}    r!1 < 1
{-6}    k1!1 + r!1 = k2!1
  |-------

Rule?