Expected Cost | +- [f] | 0 | +- [Program] | 0:While(z ≥ 1 + y) | Tick(1) | y :~ {1 : 1 + y} | 1:While(y ≥ 3) | Tick(1) | y :~ {1 : -3 + y} | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 0:While(z ≥ 1 + y) | | Tick(1) | | y :~ {1 : 1 + y} | | | +- While.step | | | | | +- [Problem] | | | 0:While(z ≥ 1 + y) | | | Tick(1) | | | y :~ {1 : 1 + y} | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ⊤] | | | | | +- linear-template | | | | | | | `- 1 + [-y + z | -y + z ≥ 0] | | | | | +- [Norms] | | | [[1 | ⊤],[-y + z | -y + z ≥ 0]] | | | | | +- [Invariant] | | | z ≥ 1 + y ==> [1 | ⊤] + h([1 | ⊤],[-1 + -y + z | -1 + -y + z ≥ 0]) ≼ h([1 | ⊤],[-y + z | -y + z ≥ 0]) | | | 1 + y ≥ 1 + z ==> 0 ≼ h([1 | ⊤],[-y + z | -y + z ≥ 0]) | | | | | `- [-y + z | -y + z ≥ 0] | | | `- [-y + z | -y + z ≥ 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 1:While(y ≥ 3) | | Tick(1) | | y :~ {1 : -3 + y} | | | +- While.step | | | | | +- [Problem] | | | 1:While(y ≥ 3) | | | Tick(1) | | | y :~ {1 : -3 + y} | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ⊤] | | | | | +- linear-template | | | | | | | `- 1 + [-2 + y | -2 + y ≥ 0] | | | | | +- [Norms] | | | [[1 | ⊤],[-2 + y | -2 + y ≥ 0]] | | | | | +- [Invariant] | | | y ≥ 3 ==> [1 | ⊤] + h([1 | ⊤],[-5 + y | -5 + y ≥ 0]) ≼ h([1 | ⊤],[-2 + y | -2 + y ≥ 0]) | | | 3 ≥ 1 + y ==> 0 ≼ h([1 | ⊤],[-2 + y | -2 + y ≥ 0]) | | | | | `- [-2 + y | -2 + y ≥ 0] | | | `- [-2 + y | -2 + y ≥ 0] | +- Expected Cost | | | +- [f] | | [-2 + y | -2 + y ≥ 0] | | | +- [Program] | | 0:While(z ≥ 1 + y) | | Tick(1) | | y :~ {1 : 1 + y} | | | +- While.step | | | | | +- [Problem] | | | 0:While(z ≥ 1 + y) | | | Tick(1) | | | y :~ {1 : 1 + y} | | | | | +- [f] | | | [-2 + y | -2 + y ≥ 0] | | | | | +- linear-template | | | | | | | `- 1 + [-2 + y | -2 + y ≥ 0] + 2·([-y + z | -y + z ≥ 0]) | | | | | +- [Norms] | | | [[1 | ⊤],[-2 + y | -2 + y ≥ 0],[-y + z | -y + z ≥ 0]] | | | | | +- [Invariant] | | | z ≥ 1 + y ==> 0 + h([1 | ⊤],[-1 + y | -1 + y ≥ 0],[-1 + -y + z | -1 + -y + z ≥ 0]) ≼ h([1 | ⊤],[-2 + y | -2 + y ≥ 0],[-y + z | -y + z ≥ 0]) | | | 1 + y ≥ 1 + z ==> [-2 + y | -2 + y ≥ 0] ≼ h([1 | ⊤],[-2 + y | -2 + y ≥ 0],[-y + z | -y + z ≥ 0]) | | | | | `- [-2 + y | -2 + y ≥ 0] + [-y + z | -y + z ≥ 0] | | | `- [-2 + y | -2 + y ≥ 0] + [-y + z | -y + z ≥ 0] | `- [-y + z | -y + z ≥ 0] + [-2 + y | -2 + y ≥ 0] + [-y + z | -y + z ≥ 0]