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

Re: Proofing problem

At 02:56 PM 02/20/2002 +0100, Christoph Berg wrote:
>On Tue, Feb 19, 2002 at 11:46:13AM +0100, Wilfried Steiner wrote:
> > {-1}  interval > 0
> > {-2}  interval <= max_interval
> > [-3]  number_intervals > 0
> > [-4]  p!1 >= 0
> > [-5]  p!1 < number_intervals
> >   |-------
> > [1]   interval * number_intervals > p!1 * interval - interval

If you load up the Manip strategies from

     http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html

you could prove this with two easy, intuitive steps:

      (factor 1 R)
      (div-by 1 "interval")

The first command factors the left-hand side of 1:

       interval * number_intervals > interval *(p!1-1)

The second command divides both sides by "interval" and completes the proof.

Rick