diff options
Diffstat (limited to 'content/zettel/3a8g5e3a.md')
| -rw-r--r-- | content/zettel/3a8g5e3a.md | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/content/zettel/3a8g5e3a.md b/content/zettel/3a8g5e3a.md new file mode 100644 index 0000000..331eba8 --- /dev/null +++ b/content/zettel/3a8g5e3a.md @@ -0,0 +1,15 @@ ++++ +title = "Proving `PTrue` through the states" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3a8g5e3"] +forwardlinks = [] +zettelid = "3a8g5e3a" ++++ + +`PTrue` is a lemma that should be proven to be preserved throughout the +execution of the semantics. This means that at each proof of semantic +preservation, one must prove that assuming `PTrue pc` is true, that +means that `PTrue pc'` is true. `PTrue pc` always refers to the current +predicate that is assigned to `pc` from the map. |