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 <[email protected]> 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 [email protected] or (510) 659-7333. > >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
