Hi, How can I apply a conditional rewrite rule in proof power. For example, applying the following thm:
forall x,y, z | x > y dot x - y + z = x + z -y where x > y is the condition, to generate the following two subgoals: 1) x > y 2) goal [x - y + z / x + z -y] Also, I wonder is there any interface of this mail list for searching, so that i can find possible solutions from previous questions of the mail list achieve ?x - y + z = x + z -y Many thanks best, Yuhui ----- We invite research leaders and ambitious early career researchers to join us in leading and driving research in key inter-disciplinary themes. Please see www.hw.ac.uk/researchleaders for further information and how to apply. Heriot-Watt University is a Scottish charity registered under charity number SC000278. _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
