[ProofPower] apply conditional rewriting

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

Re: [ProofPower] apply conditional rewriting

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