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,c7103d08119b3a51
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.224.87.77 with SMTP id v13mr12314214qal.5.1346768666021;
        Tue, 04 Sep 2012 07:24:26 -0700 (PDT)
Received: by 10.52.37.74 with SMTP id w10mr2336509vdj.8.1346768665981; Tue, 04
 Sep 2012 07:24:25 -0700 (PDT)
Path: 
 da15ni7637554qab.0!nntp.google.com!b19no848248qas.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 4 Sep 2012 07:24:25 -0700 (PDT)
In-Reply-To: <f2ed6dda-4e8b-4c5c-8a99-011167eb8158@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: <f2ed6dda-4e8b-4c5c-8a99-011167eb8158@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <c0acfa15-1895-46c6-8172-6a202c04d559@googlegroups.com>
Subject: Re: Having trouble proving modus ponens using checker
From: Ben Hocking <benjaminhocking@gmail.com>
Injection-Date: Tue, 04 Sep 2012 14:24:26 +0000
Content-Type: text/plain; charset=ISO-8859-1
Date: 2012-09-04T07:24:25-07:00
List-Id: <comp.lang.ada>

On Tuesday, September 4, 2012 9:49:03 AM UTC-4, Ben Hocking wrote:
> I have the following VC:
> 
> ====================
> 
> H1: a - b * (c - d) div e < 0 -> my_fn(a - b * (c - d) div e) <= f
> 
> H2: a - b * (c - d) div e < 0
> 
> -->
> 
>   C1: my_fn(a - b * (c - d) div e) <= f
> 
> ====================
> 
> I've tried the following:
> 
> ====================
> 
> [EXECUTE]: infer c#1 using implies.
> 
> infer c # 1 using implies.
> 
> Cannot infer my_fn(a - b * (c - d) div e) <= f using rule-family implies.
> 
> 
> 
> FAIL
> 
> 
> 
> [EXECUTE]: infer c#1 using implies(3).
> 
> infer c # 1 using implies(3).
> 
> Cannot infer my_fn(a - b * (c - d) div e) <= f using rule implies(3).
> 
> 
> 
> FAIL
> 
> 
> 
> [EXECUTE]: infer c#1 using implies(3) from [2, 1].
> 
> infer c # 1 using implies(3) from [2, 1].
> 
> Cannot infer my_fn(a - b * (c - d) div e) <= f using rule implies(3).
> 
> 
> 
> FAIL
> 
> ====================
> 
> Does anybody know what I might be doing wrong?
> 
> The rule implies(3) is defined in LOGIC.RUL as:
> 
> implies(3):       true -> A     may_be_replaced_by   A.
> 
> That's the closest I can find to modus ponens.
> 
> 
> 
> Thanks for any help,
> 
> -Ben

Never mind. Using "simplify." was all I needed.

-Ben