+++
title = "Linking the invariance of conditions to predicates"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5c1"]
forwardlinks = []
zettelid = "3a8g5c2"
+++

However, linking the invariance of conditions to the predicates is more
difficult than it originally seems, mainly because of disjunctions and
because the form of the predicates is well defined. The only structural
property one has of those predicates is the dynamic evaluation
equivalence of that predicate to the disjunction of the previous
predicates together with their path condition.

The random disjunctions in the predicate severely complicate the
argument of why a predicate will evaluate to false, because it is not
local anymore. As soon as one encounters a disjunction, one has to look
at the predecessors and one must find a condition which separates each
path from at least one other path from all the other predicates.

Otherwise, it would have been enough to say that if the condition who's
branch dominates the current point evaluates to false, that it implies
that the whole predicate evaluates to false. That is not the case though
with disjunctions, and a more complicated algorithm would be needed.