program_logic/sts.v · 2c0f9c993278a7738ff14bce5b04c030514a4dc2 · Simcha van Collem / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

9 years ago
2c0f9c99
change STS construction: non-emptiness of the state set is now part of validity, not of closedness. · 2c0f9c99
Ralf Jung authored 9 years ago
```
This strengthens some lemmas that are written using the notion of closednes, shortening some proofs all the way up to barrier.v
```
2c0f9c99

History
change STS construction: non-emptiness of the state set is now part of validity, not of closedness.
Ralf Jung authored 9 years ago
```
This strengthens some lemmas that are written using the notion of closednes, shortening some proofs all the way up to barrier.v
```