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: 103376,c032b2e4ea2d28a0
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,CP1252
Received: by 10.224.186.143 with SMTP id cs15mr12309402qab.3.1346768636253;
        Tue, 04 Sep 2012 07:23:56 -0700 (PDT)
Received: by 10.52.33.34 with SMTP id o2mr2341552vdi.12.1346768636205; Tue, 04
 Sep 2012 07:23:56 -0700 (PDT)
Path: 
 da15ni7637554qab.0!nntp.google.com!b19no846887qas.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 4 Sep 2012 07:23:56 -0700 (PDT)
In-Reply-To: <c05c6143-cbde-4916-8655-e16197981997@googlegroups.com>
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
References: <c05c6143-cbde-4916-8655-e16197981997@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <51a6e2d9-ad61-4686-aea2-64684fb765e3@googlegroups.com>
Subject: Re: Proving B given that A >= 0 -> B and A < 0 -> B
From: Ben Hocking <benjaminhocking@gmail.com>
Injection-Date: Tue, 04 Sep 2012 14:23:56 +0000
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: quoted-printable
Date: 2012-09-04T07:23:56-07:00
List-Id: <comp.lang.ada>

On Monday, September 3, 2012 10:19:28 AM UTC-4, Ben Hocking wrote:
> 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:
>=20
>   combine_cases2: PREDB may_be_deduced_from [A >=3D 0 -> PREDB, A < 0 -> =
PREDB, goal(checktype(A, number))].
>=20
> (Evidently there's no boolean type in prolog, so I can't assert that PRED=
B is of type boolean. Correct me if I'm wrong on that.)
>=20
>=20
>=20
> Unfortunately, this rule doesn't seem to be helping me on the following:
>=20
> =85
>=20
> H15:   x - a * (y - z) div b >=3D 0 ->=20
>=20
>           my_fn(x - a * (y - z) div b)  <=3D c .
>=20
> H16:   x - a * (y - z) div b < 0 ->=20
>=20
>           my_fn(x - a * (y - z) div b)  <=3D c .
>=20
> =85
>=20
>        ->
>=20
> C1:    my_fn(x - a * (y - z) div b) <=3D c .
>=20
>=20
>=20
> I'm also open to solving this problem using "checker", but I'm not sure w=
hat rules I would use on the .siv file, either.
>=20
>=20
>=20
> Thanks for any help or insight.
>=20
>=20
>=20
> -Ben

Thanks, Phil.

That worked for me. I thought there should be some sort of command like "si=
mplify." but I didn't remember it or hadn't encountered it yet.

-Ben