+++ title = "Semantic invariance on the evaluation of conditions" author = "Yann Herklotz" tags = [] categories = [] backlinks = ["3a8g5c"] forwardlinks = ["3a8g5c2"] zettelid = "3a8g5c1" +++ We can design a semantic invariance on the evaluation of conditions, showing that if we have a point that has predecessors, for any two predecessors, there exists a condition such that the successors of that condition dominate the two predecessors. This property should allow you to prove that in the region that is dominated by a successor of a condition, that condition will always evaluate to either true or false, depending on which successor was chosen. This can be proven independently of the predicates themselves, which makes the proof much easier.