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

On 04/06/15 10:30, YuHui Lin wrote:
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