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
