> David, Good to hear you are still moving forward.
If the transformation you seek is a propositional tautology, the following general prescription should work. 1. Formulate the transformation as an equivalence using propositional (Boolean) variables, with the starting point on the left of the equivalence and the desired form on the right, and universally quantify the equivalence over all the Boolean variables. 2. Prove this sentence using “prove_rule[]”. 3. Use rewrite_rule with the resulting theorem to effect the transformation in a forward proof. I’m not in a position to check any specific examples at the moment, but if you have any difficulties I will be better placed later in the week. Roger Jones
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
