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 > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
