1 files changed, 44 insertions, 0 deletions
diff --git a/content/zettel/3a8g2d.md b/content/zettel/3a8g2d.md
new file mode 100644
index 0000000..48b5a44
--- /dev/null
+++ b/content/zettel/3a8g2d.md
@@ -0,0 +1,44 @@
++++
+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