- Orderings are done is a such a way that:
⊥ < C < T
- This can be imagined as having three levels, the uppermost contains T, the last one contains ⊥ and the mid level contains number of incomparable constants.
lub(T, a) = T; lub(⊥, a) = a; lub(T, ⊥) = T; lub(a,b) = T
The rules stated in some previous post was:
1. C(x,pi,out) = T ∀i ⇒ C(x,s,in) = T 2. C(x,pi,out) = c or d and c ≠ d ∀i ⇒ C(x,s,in)=T 3. C(x,pi,out) = c or ⊥ ∀i ⇒ C(x,s,in) = c 4. C(x,pi,out) = ⊥ ∀i ⇒ C(x,s,in) = ⊥ these all rules can be combined and stated as: C(s,x,in) = lub(C(p,x,out) | p is a predecessor of s)
In this arrangement value X_in and X_out can change at most twice. Hence the algorithm can be terminated if all the elements has changed twice or no change is there. Also number of steps would be number of statements times 4.