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
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
Heriot-Watt University is a Scottish charity
registered under charity number SC000278.
Proofpower mailing list