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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,c032b2e4ea2d28a0,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,CP1252
Received: by 10.224.39.75 with SMTP id f11mr8704365qae.8.1346681968334;
        Mon, 03 Sep 2012 07:19:28 -0700 (PDT)
Received: by 10.236.184.196 with SMTP id s44mr1210969yhm.16.1346681968314;
 Mon, 03 Sep 2012 07:19:28 -0700 (PDT)
Path: 
 da15ni7637554qab.0!nntp.google.com!b19no474143qas.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Mon, 3 Sep 2012 07:19:28 -0700 (PDT)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=8.25.3.17;
 posting-account=hKGsDAoAAAC9HB_9misjykjawYQeT_yf
NNTP-Posting-Host: 8.25.3.17
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <c05c6143-cbde-4916-8655-e16197981997@googlegroups.com>
Subject: Proving B given that A >= 0 -> B and A < 0 -> B
From: Ben Hocking <benjaminhocking@gmail.com>
Injection-Date: Mon, 03 Sep 2012 14:19:28 +0000
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: quoted-printable
Date: 2012-09-03T07:19:28-07:00
List-Id: <comp.lang.ada>

I've run into this scenario a couple times and I have yet to come up with a=
 simple solution. I have the following rule in my .rlu file:
  combine_cases2: PREDB may_be_deduced_from [A >=3D 0 -> PREDB, A < 0 -> PR=
EDB, goal(checktype(A, number))].
(Evidently there's no boolean type in prolog, so I can't assert that PREDB =
is of type boolean. Correct me if I'm wrong on that.)

Unfortunately, this rule doesn't seem to be helping me on the following:
=85
H15:   x - a * (y - z) div b >=3D 0 ->=20
          my_fn(x - a * (y - z) div b)  <=3D c .
H16:   x - a * (y - z) div b < 0 ->=20
          my_fn(x - a * (y - z) div b)  <=3D c .
=85
       ->
C1:    my_fn(x - a * (y - z) div b) <=3D c .

I'm also open to solving this problem using "checker", but I'm not sure wha=
t rules I would use on the .siv file, either.

Thanks for any help or insight.

-Ben