search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

st = update st x (st x) #115

Open HyeongMee opened 9 years ago

HyeongMee commented 9 years ago

Hi I derived such an expression as is stated in the title. I know intuitively it is right, but how can I prove it?

Thanks :-D

jaewooklee93 commented 9 years ago

One Lemma already proved in Assignment07_09.v and one Axiom in Assignment08_00.v are needed.

HyeongMee commented 9 years ago

@jaewooklee93 THX :D