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 


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

Reply via email to