Roger,
> On 12 Mar 2016, at 17:30, Roger Bishop Jones <r...@rbjones.com> 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.

## Advertising

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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com