> On 12 Mar 2016, at 17:30, Roger Bishop Jones <r...@rbjones.com> wrote:
> 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
> 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
the conclusion of L3 to ¬ ¬ q to get this to work.
Proofpower mailing list