Roger, > On 12 Mar 2016, at 17:30, Roger Bishop Jones <[email protected]> wrote: > > David, > > This is not an alph-conversion error. > The reference to apha conversion is a normal qualifier when > any rule doesn't get what it needs, since in general a statement of of what > is needed need only be complied with "up to alpha conversion". > > The real problem here (I guess since I can't actually see the command > which caused the error, and I can't see the error message), is that you > have not supplied the arguments required by the rule you are using. > > You have to give it a theorem with a disjunction in the conclusion and a > theorem > whose conclusion is the negation of one of the disjuncts.
Yes. David was optimistically expecting q in the conclusion of L3 to hook up with ¬ q in the conclusion of L4, but, as Mark pointed out, you need to use ¬_¬_intro to change the conclusion of L3 to ¬ ¬ q to get this to work. Regards, Rob. _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
