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)

## Advertising

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.
>
> If you have any concerns, please contact the Ohlone College IT Service
> Desk at itserviced...@ohlone.edu or (510) 659-7333.
>
>

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com