1 files changed, 27 insertions, 0 deletions
diff --git a/content/zettel/3a7c.md b/content/zettel/3a7c.md
new file mode 100644
index 0000000..0b05b13
--- /dev/null
+++ b/content/zettel/3a7c.md
@@ -0,0 +1,27 @@
++++
+title = "Proof of translation validation theorem"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a7b"]
+forwardlinks = ["3a7d"]
+zettelid = "3a7c"
++++
+
+The proof follows from the fact that the translation to the abstract
+interpretation is semantics preserving. As the abstract interpretation
+of both languages is equal, this means that
+
+$$ \frac{\Sigma_s, s \downarrow_S \Sigma_s' \quad \Sigma_t, t \downarrow_T\Sigma_t' \quad s \sim t \quad \Sigma_s \sim \Sigma_t}{\Sigma_s' \sim \Sigma_t'}$$
+
+This is because:
+
+$$ \frac{\Sigma_s, \alpha \downarrow_{\mathcal{A}} \Sigma_s' \quad \Sigma_t,\alpha' \downarrow_{\mathcal{A}} \Sigma_t' \quad \alpha \sim \alpha' \quad\Sigma_s \sim \Sigma_t}{\Sigma_s' \sim \Sigma_t'} $$
+
+And the latter can be used because :
+
+$$ s \rightarrow_s \alpha \land t \rightarrow_t \alpha' $$
+
+We can therefore get the following:
+
+$$ \cfrac{\cfrac{}{\alpha \sim \alpha'} \quad \cfrac{\cfrac{}{\Sigma_s, s\downarrow_S \Sigma_s'} \quad \cfrac{}{s \rightarrow_s \alpha}}{\Sigma_s, \alpha\downarrow_{\mathcal{A}} \Sigma_s'} \quad \cfrac{\cfrac{}{\Sigma_t, t\downarrow_T \Sigma_t'} \quad \cfrac{}{t \rightarrow_t \alpha'}}{\Sigma_t,\alpha' \downarrow_{\mathcal{A}} \Sigma_t'} \quad \cfrac{}{\Sigma_s \sim\Sigma_t}}{\Sigma_s' \sim \Sigma_t' \land s \sim t} $$