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.
None of the theorems you show meet these requirements.
On 11/03/16 08:53, David Topham wrote:
> I am trying to do a forward proof using hypothetical syllogism
> of this form: ~q v r, q |- r
> but get an alpha-conversion error.
> (sorry for the hard to read format here, but I know I can't post
> images or pdf files here, so what other way is there to show the
> extended chars of ProofPower? I did
> ascii-conv to get this format)
> val L1 = p %thm% p: THM
> val L2 = p %implies% q %thm% p %implies% q: THM
> val L3 = p %implies% q, p %thm% q: THM
> val L4 = %not% q %or% r %thm% %not% q %or% r: THM
> Exception Fail * ³ q ² r ô ³ q ² r and p ´ q, p ô q are not of the
> form: `‡1 ô
> t1 ² t2' and `‡2 ô ³t3' where ¬t3® is Á-convertible to ¬t1® or ¬t2®
> [²_cancel_rule.7050] * raised
> Proofpower mailing list
Proofpower mailing list