• Ralf Jung's avatar
    wakestpre: swap wp_value and wp_value' · 4c3cbc71
    Ralf Jung authored
    The rationale is that, just like the always lemmas about uPred and the frame-preserving updates for maps and iprdos, the versions with the ' are the "more specific" versions, hard-coding more assumptions in the shape of their conclusion.
    4c3cbc71
hoare.v 3.92 KB