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

*To*: pvs-help@csl.sri.com*Subject*: trivial theorem*From*: mandrio5@ipmel3 (Stud. D. Mandrioli)*Date*: Tue, 29 Jul 1997 00:11:29 +0200*Cc*: mandrio5@elet.polimi.it

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?

- Prev by Date:
**lemma,inst? and replace** - Next by Date:
**Re: trivial theorem** - Prev by thread:
**Re: A doubt regarding use of records and functions.** - Next by thread:
**Re: trivial theorem** - Index(es):