1 files changed, 24 insertions, 0 deletions
diff --git a/content/zettel/3a8g5e3.md b/content/zettel/3a8g5e3.md
new file mode 100644
index 0000000..9ac35b2
--- /dev/null
+++ b/content/zettel/3a8g5e3.md
@@ -0,0 +1,24 @@
++++
+title = "PTrue predicate under dominance"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5e2"]
+forwardlinks = ["3a8g5e4", "3a8g5e3a"]
+zettelid = "3a8g5e3"
++++
+
+The global predicate correct property is only true under dominance of
+the header (even though in reality this seems to be an optimisation
+actually). This means that not every predicate needs to be checked, but
+only the predicates that are actually dominated by the header node.
+Because of this optimisation, however, we actually need to preserve the
+fact that if the successor is dominated by the original header, that the
+current node is dominated too.
+
+This is correct, because if the successor is strictly dominated by the
+node, then all the previous nodes have to be dominated too, or one of
+the previous nodes must be the dominator, and there must be a path from
+that node to the other predecessors of the current node. Otherwise, not
+all paths from the input to the current node would pass through the
+dominator.