[ect] 0 | +- [Problem] | 0:While(x ≥ 1) | z :~ {1/2 : 1;1/2 : 2} | x :~ {1 : x + -z} | t :~ {1 : x} | x :~ {1 : y} | y :~ {1 : t} | Tick(1) | +- [While.Step] | | | +- [ect] 0 | | | | | +- [Problem] | | | z :~ {1/2 : 1;1/2 : 2} | | | x :~ {1 : x + -z} | | | t :~ {1 : x} | | | x :~ {1 : y} | | | y :~ {1 : t} | | | Tick(1) | | | | | `- 1 | | | +- additive | | | +- optimistic | | | +- [Norms] | | [1,|0,2 + y|,|0,x|] | | | +- [evt] 1 | | | | | +- [Problem] | | | z :~ {1/2 : 1;1/2 : 2} | | | x :~ {1 : x + -z} | | | t :~ {1 : x} | | | x :~ {1 : y} | | | y :~ {1 : t} | | | Tick(1) | | | | | `- 1 | | | +- [evt] |0,2 + y| | | | | | +- [Problem] | | | z :~ {1/2 : 1;1/2 : 2} | | | x :~ {1 : x + -z} | | | t :~ {1 : x} | | | x :~ {1 : y} | | | y :~ {1 : t} | | | Tick(1) | | | | | `- 1/2·(|0,1 + x|) + 1/2·(|0,x|) | | | +- [evt] |0,x| | | | | | +- [Problem] | | | z :~ {1/2 : 1;1/2 : 2} | | | x :~ {1 : x + -z} | | | t :~ {1 : x} | | | x :~ {1 : y} | | | y :~ {1 : t} | | | Tick(1) | | | | | `- |0,y| | | | +- [Invariant] | | x ≥ 1 ∧ y ≥ -1 ==> 1 + h(1,1/2·(|0,1 + x|) + 1/2·(|0,x|),|0,y|) ≼ h(1,|0,2 + y|,|0,x|) | | 1 ≥ 1 + x ∧ y ≥ -1 ==> 0 ≼ h(1,|0,2 + y|,|0,x|) | | | `- [x ≥ 1 ∧ y ≥ -1]·(2·(|0,2 + y|) + 2·(|0,x|)) | `- [x ≥ 1 ∧ y ≥ -1]·(2·(|0,2 + y|) + 2·(|0,x|))