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

*To*: pvs-help@csl.sri.com*Subject*: Proof of override expressions*From*: Bin Chen <chenb3@cas.mcmaster.ca>*Date*: Thu, 20 Feb 2003 16:32:23 -0500 (EST)*Sender*: pvs-help-owner@csl.sri.com

Hi, Could anyone please tell me how to prove the following sequent? s_correct1: |-------- [1] x WITH [r(1) := x(r(2)) + x(r(3)), r(0):= x(r(2)) + x(r(3))] (r(1)) = x WITH [r(1) := x(r(2)) + x(r(3)), r(0):= x(r(2)) + x(r(3))] (r(2)) + x WITH [r(1) := x(r(2)) + x(r(3)), r(0):= x(r(2)) + x(r(3))] (r(3)) Usually how to prove sequents with override expressions? Thank you very much! Ken.

- Prev by Date:
**Re: "<" on a subset of nat is well_founded** - Next by Date:
**Re: Proof of override expressions** - Prev by thread:
**existskwantor problem** - Next by thread:
**Re: Proof of override expressions** - Index(es):