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

Re: Proofing problem



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

Hello,

you have to use (LEMMA "both_sides_times_pos_gt1").
See the attached files.

Christoph Berg
-- 
cb@cs.uni-sb.de, http://www-wjp.cs.uni-sb.de/~cb/
Office +49/681/302-4129, Fax -4290, Home +49/681/9657944
Computer Science Dept., Universität des Saarlandes, Saarbrücken
steiner: theory
begin

%{-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

interval: nat
number_intervals: nat
max_interval: nat
p: Var real

steiner: lemma
 interval > 0 and
 interval <= max_interval and
 number_intervals > 0 and
 p >= 0 and
 p < number_intervals
implies
 interval * number_intervals > p * interval - interval

end steiner
(|steiner|
 (|steiner| "" (SKOSIMP*)
  (("" (LEMMA "both_sides_times_pos_gt1")
    (("" (INST -1 "interval" "number_intervals" "p!1") (("" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL))

PGP signature