Expected Cost | +- [f] | 0 | +- [Program] | 0:While(x ≥ 1) | Choice | 1/4: x :~ {1 : 1 + x} | 3/4: x :~ {1 : -1 + x} | y :~ {1 : -1 + x} | 1:While(y ≥ 1) | r :~ {1/3 : 0;1/3 : 1;1/3 : 2} | y :~ {1 : -r + y} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(x ≥ 1) | | Choice | | 1/4: x :~ {1 : 1 + x} | | 3/4: x :~ {1 : -1 + x} | | y :~ {1 : -1 + x} | | 1:While(y ≥ 1) | | r :~ {1/3 : 0;1/3 : 1;1/3 : 2} | | y :~ {1 : -r + y} | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | +- While.step | | | | | | | +- [Problem] | | | | 1:While(y ≥ 1) | | | | r :~ {1/3 : 0;1/3 : 1;1/3 : 2} | | | | y :~ {1 : -r + y} | | | | Tick(1) | | | | | | | +- [f] | | | | 0 | | | | | | | +- Expected Cost Body | | | | | | | | | `- [1 | ⊤] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [y | y ≥ 0] | | | | | | | +- [Norms] | | | | [[1 | ⊤],[y | y ≥ 0]] | | | | | | | +- [Invariant] | | | | y ≥ 1 ==> [1 | ⊤] + h([1 | ⊤],1/3·[y | y ≥ 0] + 1/3·[-1 + y | -1 + y ≥ 0] + 1/3·[-2 + y | -2 + y ≥ 0]) ≼ h([1 | ⊤],[y | y ≥ 0]) | | | | 1 ≥ 1 + y ==> 0 ≼ h([1 | ⊤],[y | y ≥ 0]) | | | | | | | `- 3/2·[y | y ≥ 0] | | | | | `- 3/8·[x | x ≥ 0] + 9/8·[-2 + x | -2 + x ≥ 0] | | | +- mixed-iteration-template | | | | | `- [x | x ≥ 0] + [x | x ≥ 0]^2 | | | +- [Norms] | | [[x | x ≥ 0],[x^2 | x ≥ 0]] | | | +- [Invariant] | | x ≥ 1 ==> 3/8·[x | x ≥ 0] + 9/8·[-2 + x | -2 + x ≥ 0] + h(1/4·[1 + x | 1 + x ≥ 0] + 3/4·[-1 + x | -1 + x ≥ 0],1/4·[1 + 2·(x) + x^2 | 1 + x ≥ 0] + 3/4·[1 + -2·(x) + x^2 | -1 + x ≥ 0]) ≼ h([x | x ≥ 0],[x^2 | x ≥ 0]) | | 1 ≥ 1 + x ==> 0 ≼ h([x | x ≥ 0],[x^2 | x ≥ 0]) | | | `- 3/4·[x | x ≥ 0] + 3/2·[x^2 | x ≥ 0] | `- 3/4·[x | x ≥ 0] + 3/2·[x^2 | x ≥ 0]