[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] two problems

On Thu, Jul 31, 2008 at 10:43:19PM +0800, applehopedream wrote:
>    2.in the proving,if I want to substitute a definition in a formula just for partly,how could I do?
> 

I was actually wondering about this myself. Is it possible to do
partial replacement? For example:

  [-1] A = B
  -------------
  [ 1] A = C + D + A

I'd like to say, for example (replace -1 (1) (instance 2)), and have

  [-1] A = B
  -------------
  [ 1] A = C + D + B

Thanks

jerome