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

Reply via email to