Hi Dave, With this rule, the theorems need to precisely match up with how they are described in the manual, so you need to have the conclusion of the 2nd theorem as the logical negation of the LHS of the "or" in the 1st thm (not vice versa). So just use the double logical negation introduction rule on the 2nd theorem, and then it works.
Perhaps using good old ASCII versions of the logical symbols a good idea. This is what the HOL4 and HOL Light use. So there's: disjunction: \/ conjuntion: /\ logical negation: ~ implication: ==> logical equivalence: <=> universal quantification: ! existential quantification: ? unique existential quantification: ?! Mark. On 11/03/2016 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(R) is Á-convertible to ¬t1(R) or ¬t2(R) > [²_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
