Forked from
Iris / Iris
Source project has a limited visibility.
-
Ralf Jung authoredThe good news is, this one works without FSAs, and it can be applied around the "view shift with a step"-thing. Furthermore, the FSA lemma can be derived from the new one. The bad news is, the FSA lemma proof doesn't even get shorter in doing this change.
Ralf Jung authoredThe good news is, this one works without FSAs, and it can be applied around the "view shift with a step"-thing. Furthermore, the FSA lemma can be derived from the new one. The bad news is, the FSA lemma proof doesn't even get shorter in doing this change.