From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,48e1a3c594fb62e8 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!c11g2000vbe.googlegroups.com!not-for-mail From: Phil Clayton Newsgroups: comp.lang.ada Subject: Re: SPARK Date: Sat, 15 May 2010 11:43:05 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: NNTP-Posting-Host: 91.110.192.224 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1273948986 16432 127.0.0.1 (15 May 2010 18:43:06 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sat, 15 May 2010 18:43:06 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: c11g2000vbe.googlegroups.com; posting-host=91.110.192.224; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-GB; rv:1.9.0.15) Gecko/2009102704 Fedora/3.0.15-1.fc10 Firefox/3.0.15,gzip(gfe) Xref: g2news2.google.com comp.lang.ada:11641 Date: 2010-05-15T11:43:05-07:00 List-Id: On May 15, 5:41=A0pm, Yannick Duch=EAne (Hibou57) wrote: > > =A0 =A0 =A0 =A0--# assert ((Part * 100) <=3D (Whole * 100)) -> > =A0 =A0 =A0 =A0--# =A0 =A0 =A0 =A0(((Part * 100) / Whole) <=3D ((Whole * = 100) / Whole)); > > It was not able to prove it. Do I miss something or does it simply means = =A0 > the simplifier does not know about a rule which seems basic to me, that i= s =A0 > (A <=3D B) -> ((A / C) <=3D (B / C)) ? ... which is still valid for integ= er =A0 > arithmetic. This isn't valid for all values of A, B and C: consider C =3D -1. It would be sufficient to know 0 < C, so perhaps sufficient information needs to be propagated to show 0 < Whole ? Phil C.