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".

## Advertising

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.
None of the theorems you show meet these requirements.
Roger
On 11/03/16 08:53, David Topham wrote:
> I am trying to do a forward proof using hypothetical syllogism
> (V_cancel_Rule)
> 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@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com