+++
title = "A Possible Destruction Proof"
date = "2022-06-28"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g2c"]
forwardlinks = ["3a8g2b1", "3a8g2e"]
zettelid = "3a8g2d"
+++

The idea hinges on the following lemma, which talks about a path $p$
from nodes $n$ to $m$, an arbitrary predicate $\mathcal{P}$ which gets
simplified over that path into $\mathcal{P}'$, and finally an execution
along a path from $n$ with register state $R$ to $m$ with register state
$R'$. The execution of the predicate $P$ with $R'$ should give the same
result as executing the predicate $P'$ with the initial state $R'$.

```{=latex}
\begin{gather*}
\frac{\begin{array}{c}
  S^p(\mathcal{P}) = \mathcal{P}' \\
  n, R \overset{p}{\longrightarrow^*} m, R'
\end{array}}{
  R', \mathcal{P} \Downarrow \lfloor b \rfloor \Longleftrightarrow R, \mathcal{P}'
\Downarrow \lfloor b \rfloor
}
\end{gather*}
```
However, in addition to that we will also have to prove the
generalisation of the simplification ([\#3a8g2b1]) to show that this has
been done along the path of execution.

The idea, finally, is that during the proof of semantic preservation, a
path $n\rightsquigarrow_p m$, as well as the execution along that path
$n, R\overset{p}{\longrightarrow^*} m, R'$ are remembered, so that once
a γ function is reached, the lemma above can be applied. It might also
be true that:

$$ \frac{n, R \overset{p}{\longrightarrow^*} m, R'}{n \rightsquigarrow_p m} $$

In which case the lemma can be simplified.

  [\#3a8g2b1]: /zettel/3a8g2b1