blob: 331eba86de35d09f914778637c148e27a6e1a38d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.
|
