1 files changed, 31 insertions, 0 deletions
diff --git a/content/zettel/3a8g5b.md b/content/zettel/3a8g5b.md
new file mode 100644
index 0000000..37938de
--- /dev/null
+++ b/content/zettel/3a8g5b.md
@@ -0,0 +1,31 @@
++++
+title = "Proving correctness by reducing to correctness of paths"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5d", "3a8g5a"]
+forwardlinks = ["3a8e", "3a8g5c"]
+zettelid = "3a8g5b"
++++
+
+The problem of correctness of path expressions can therefore be reduced
+to the correctness of paths themselves, using the following theorem (if
+it can be proven):
+
+```{=latex}
+\begin{align}
+\forall a\ &b\ P\ P'\ R\ s,\ \exists p,\\
+  &\textit{path}\ a\ p\ b \\
+  &\implies t_p\ p\ P \\
+  &\implies t\ R_{a \rightarrow b}\ P' \\
+  &\implies P \Downarrow s = T \\
+  &\implies P' \Downarrow s = T
+\end{align}
+```
+This therefore reduces the proof to a proof that there is at least one
+path that convert to a predicate which will then finally evaluate to
+true. This property is therefore useful to prove the induction of the
+semantics of SSA to prove the proper invariant, similar to the equations
+Lemma ([\#3a8e]).
+
+  [\#3a8e]: /zettel/3a8e