+++
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.