1 files changed, 28 insertions, 0 deletions
diff --git a/content/zettel/3a8e3.md b/content/zettel/3a8e3.md
new file mode 100644
index 0000000..92affd0
--- /dev/null
+++ b/content/zettel/3a8e3.md
@@ -0,0 +1,28 @@
++++
+title = "Equation lemma proof"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8e2"]
+forwardlinks = ["3a8g"]
+zettelid = "3a8e3"
++++
+
+The equation lemma is proven by defining a constant property over the
+semantics, and proving that correct. This is proven in two parts:
+
+1.  Prove the property using the initial entry point of the control flow
+    graph.
+2.  Prove the property for an arbitrary point, assuming that the
+    property holds for the previous value in the control flow graph.
+
+This therefore results in a kind of induction over the semantics
+themselves, and then allows one to use the property anywhere in the
+semantics preservation proof.
+
+This can be used to prove the equation lemma, because the proof of
+preservation of the registers can be proven that way, but it can also be
+used for other proofs, such as proving the CompCertGSA ([\#3a8g])
+generation correct.
+
+  [\#3a8g]: /zettel/3a8g