# Re: [ProofPower] ProofPower and Discrete Math

```Since the slides for this book use slightly different notation, I am back
to trying to implement the proofs in the main book:  UsingZ from
www.usingz.com  (in text link, it is zedbook)```
```
On page 42, the proof is using nested existentials, and I am trying
to get past my lack of understanding in applying E-elim
(Roger already helped me with E-intro)

Here are two of my attempts (using ASCII since I can't attach pdf here)
val L1 = asm_rule %<%p(x,y):BOOL%>%;
val L2 = %<%%exists%x:'a%spot%p(x,y)%>%;
val L3 = %exists%_intro L2 L1;
val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p(x,y)%>%;
val L5 = %exists%_intro L4 L3;
val L6 = asm_rule %<%%exists%y:'b%spot%p(x,y)%>%;
val L7 = %exists%_elim L4 L5 L6;

val L1 = asm_rule %<%p:BOOL%>%;
val L2 = %<%%exists%x:'a%spot%p%>%;
val L3 = %exists%_intro L2 L1;
val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p%>%;
val L5 = %exists%_intro L4 L3;
val L6 = asm_rule %<%%exists%y:'b%spot%p%>%;
val L7 = %exists%_elim L4 L5 L6;

The error I get is "does not match the bound varstruct"

Does anyone have a suggestion to get me past this roadblock?

-Dave

On Sun, Aug 14, 2016 at 2:21 AM, Roger Bishop Jones <r...@rbjones.com> wrote:

>
> On 14/08/2016 08:44, David Topham wrote:
>
>> Thanks Roger, I am using slides he distributes.  He  has false
>> introduction rules starting on page 24 (attached).
>> Sorry about my poor example, please ignore that since is a confused use
>> of this technique anyway!  -Dave
>>
>> Looks like he changed the name.
>
> In fact the original name (the one he uses in the book) is good in
> ProofPower.
> ¬_elim is available in ProofPower and does what you want (though it is
> sligftly more general, it proves anything from a contradiction so you have
> to tell it what result you are after).
> Details in reference manual.
>
> Roger
>
>
> This message did not originate from Ohlone College  and must be viewed
> with caution. Viruses and phishing attempts can be transmitted via email.
> E-mail transmission cannot be guaranteed to be secure or error-free as
> information could be intercepted, corrupted, lost, destroyed, arrive late
> or incomplete, or contain viruses.
>
```_______________________________________________