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

Proof of override expressions

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.