blob: af27b6149c24ce3e0e8d1311d10c6557b4b3c34d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
+++
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.
|
