Expected Cost | +- [f] | 0 | +- [Program] | 0:While(x ≥ 1 + y) | Tick(1) | x :~ {1 : -1 + x} | x :~ {1 : 1000 + x} | y :~ {1 : 1000 + y} | 1:While(y ≥ 1) | Tick(1) | y :~ {1 : -1 + y} | 2:While(0 ≥ 1 + x) | Tick(1) | x :~ {1 : 1 + x} | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 0:While(x ≥ 1 + y) | | Tick(1) | | x :~ {1 : -1 + x} | | x :~ {1 : 1000 + x} | | y :~ {1 : 1000 + y} | | | +- While.step | | | | | +- [Problem] | | | 0:While(x ≥ 1 + y) | | | Tick(1) | | | x :~ {1 : -1 + x} | | | x :~ {1 : 1000 + x} | | | y :~ {1 : 1000 + y} | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ⊤] | | | | | +- linear-template | | | | | | | `- 1 + [x + -y | x + -y ≥ 0] | | | | | +- [Norms] | | | [[1 | ⊤],[x + -y | x + -y ≥ 0]] | | | | | +- [Invariant] | | | x ≥ 1 + y ==> [1 | ⊤] + h([1 | ⊤],[-1 + x + -y | -1 + x + -y ≥ 0]) ≼ h([1 | ⊤],[x + -y | x + -y ≥ 0]) | | | 1 + y ≥ 1 + x ==> 0 ≼ h([1 | ⊤],[x + -y | x + -y ≥ 0]) | | | | | `- [x + -y | x + -y ≥ 0] | | | `- [x + -y | x + -y ≥ 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 1:While(y ≥ 1) | | Tick(1) | | y :~ {1 : -1 + y} | | 2:While(0 ≥ 1 + x) | | Tick(1) | | x :~ {1 : 1 + x} | | | +- Expected Cost | | | | | +- [f] | | | 0 | | | | | +- [Program] | | | 1:While(y ≥ 1) | | | Tick(1) | | | y :~ {1 : -1 + y} | | | | | +- While.step | | | | | | | +- [Problem] | | | | 1:While(y ≥ 1) | | | | Tick(1) | | | | y :~ {1 : -1 + y} | | | | | | | +- [f] | | | | 0 | | | | | | | +- Expected Cost Body | | | | | | | | | `- [1 | ⊤] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [y | y ≥ 0] | | | | | | | +- [Norms] | | | | [[1 | ⊤],[y | y ≥ 0]] | | | | | | | +- [Invariant] | | | | y ≥ 1 ==> [1 | ⊤] + h([1 | ⊤],[-1 + y | -1 + y ≥ 0]) ≼ h([1 | ⊤],[y | y ≥ 0]) | | | | 1 ≥ 1 + y ==> 0 ≼ h([1 | ⊤],[y | y ≥ 0]) | | | | | | | `- [y | y ≥ 0] | | | | | `- [y | y ≥ 0] | | | +- Expected Cost | | | | | +- [f] | | | 0 | | | | | +- [Program] | | | 2:While(0 ≥ 1 + x) | | | Tick(1) | | | x :~ {1 : 1 + x} | | | | | +- While.step | | | | | | | +- [Problem] | | | | 2:While(0 ≥ 1 + x) | | | | Tick(1) | | | | x :~ {1 : 1 + x} | | | | | | | +- [f] | | | | 0 | | | | | | | +- Expected Cost Body | | | | | | | | | `- [1 | ⊤] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [-x | -x ≥ 0] | | | | | | | +- [Norms] | | | | [[1 | ⊤],[-x | -x ≥ 0]] | | | | | | | +- [Invariant] | | | | 0 ≥ 1 + x ==> [1 | ⊤] + h([1 | ⊤],-1·[1 + x | -1 + -x ≥ 0]) ≼ h([1 | ⊤],[-x | -x ≥ 0]) | | | | 1 + x ≥ 1 ==> 0 ≼ h([1 | ⊤],[-x | -x ≥ 0]) | | | | | | | `- -1·[x | -x ≥ 0] | | | | | `- -1·[x | -x ≥ 0] | | | +- Expected Cost | | | | | +- [f] | | | -1·[x | -x ≥ 0] | | | | | +- [Program] | | | 1:While(y ≥ 1) | | | Tick(1) | | | y :~ {1 : -1 + y} | | | | | `- -1·[x | -x ≥ 0] | | | `- [y | y ≥ 0] + -1·[x | -x ≥ 0] | +- Expected Cost | | | +- [f] | | [y | y ≥ 0] + -1·[x | -x ≥ 0] | | | +- [Program] | | 0:While(x ≥ 1 + y) | | Tick(1) | | x :~ {1 : -1 + x} | | x :~ {1 : 1000 + x} | | y :~ {1 : 1000 + y} | | | +- Expected Cost | | | | | +- [f] | | | [y | y ≥ 0] | | | | | +- [Program] | | | 0:While(x ≥ 1 + y) | | | Tick(1) | | | x :~ {1 : -1 + x} | | | x :~ {1 : 1000 + x} | | | y :~ {1 : 1000 + y} | | | | | +- While.step | | | | | | | +- [Problem] | | | | 0:While(x ≥ 1 + y) | | | | Tick(1) | | | | x :~ {1 : -1 + x} | | | | x :~ {1 : 1000 + x} | | | | y :~ {1 : 1000 + y} | | | | | | | +- [f] | | | | [y | y ≥ 0] | | | | | | | +- linear-template | | | | | | | | | `- 1 + 2·([x + -y | x + -y ≥ 0]) + [y | y ≥ 0] | | | | | | | +- [Norms] | | | | [[1 | ⊤],[x + -y | x + -y ≥ 0],[y | y ≥ 0]] | | | | | | | +- [Invariant] | | | | x ≥ 1 + y ==> 0 + h([1 | ⊤],[-1 + x + -y | -1 + x + -y ≥ 0],[1000 + y | 1000 + y ≥ 0]) ≼ h([1 | ⊤],[x + -y | x + -y ≥ 0],[y | y ≥ 0]) | | | | 1 + y ≥ 1 + x ==> [y | y ≥ 0] ≼ h([1 | ⊤],[x + -y | x + -y ≥ 0],[y | y ≥ 0]) | | | | | | | `- 1000·[x + -y | x + -y ≥ 0] + [y | y ≥ 0] | | | | | `- 1000·[x + -y | x + -y ≥ 0] + [y | y ≥ 0] | | | +- Expected Cost | | | | | +- [f] | | | -1·[x | -x ≥ 0] | | | | | +- [Program] | | | 0:While(x ≥ 1 + y) | | | Tick(1) | | | x :~ {1 : -1 + x} | | | x :~ {1 : 1000 + x} | | | y :~ {1 : 1000 + y} | | | | | +- While.step | | | | | | | +- [Problem] | | | | 0:While(x ≥ 1 + y) | | | | Tick(1) | | | | x :~ {1 : -1 + x} | | | | x :~ {1 : 1000 + x} | | | | y :~ {1 : 1000 + y} | | | | | | | +- [f] | | | | -1·[x | -x ≥ 0] | | | | | | | +- square-shift-max-template | | | | | | | | | `- 2 + 2·([1 + x + -y | 1 + x + -y ≥ 0]) + 2·([x | -x ≥ 0]) + 4·([x | -x ≥ 0]·[x + -y | x + -y ≥ 0]) + [x | -x ≥ 0]^2 + [x | x ≥ 0] + 4·([x + -y | x + -y ≥ 0]) + 4·([x + -y | x + -y ≥ 0]^2) | | | | | | | +- [Norms] | | | | [[1 | ⊤],[1 + x + -y | 1 + x + -y ≥ 0],[x | -x ≥ 0],[-x·y + x^2 | -x ≥ 0 ∧ x + -y ≥ 0],[x^2 | -x ≥ 0],[x | x ≥ 0],[x + -y | x + -y ≥ 0],[-2·(x·y) + x^2 + y^2 | x + -y ≥ 0]] | | | | | | | +- [Invariant] | | | | x ≥ 1 + y ==> 0 + h([1 | ⊤],[x + -y | x + -y ≥ 0],[999 + x | -999 + -x ≥ 0],[-999 + 998·(x) + -x·y + x^2 + -999·(y) | -999 + -x ≥ 0 ∧ -1 + x + -y ≥ 0],[998001 + 1998·(x) + x^2 | -999 + -x ≥ 0],[999 + x | 999 + x ≥ 0],[-1 + x + -y | -1 + x + -y ≥ 0],[1 + -2·(x) + -2·(x·y) + x^2 + 2·(y) + y^2 | -1 + x + -y ≥ 0]) ≼ h([1 | ⊤],[1 + x + -y | 1 + x + -y ≥ 0],[x | -x ≥ 0],[-x·y + x^2 | -x ≥ 0 ∧ x + -y ≥ 0],[x^2 | -x ≥ 0],[x | x ≥ 0],[x + -y | x + -y ≥ 0],[-2·(x·y) + x^2 + y^2 | x + -y ≥ 0]) | | | | 1 + y ≥ 1 + x ==> -1·[x | -x ≥ 0] ≼ h([1 | ⊤],[1 + x + -y | 1 + x + -y ≥ 0],[x | -x ≥ 0],[-x·y + x^2 | -x ≥ 0 ∧ x + -y ≥ 0],[x^2 | -x ≥ 0],[x | x ≥ 0],[x + -y | x + -y ≥ 0],[-2·(x·y) + x^2 + y^2 | x + -y ≥ 0]) | | | | | | | `- 1/2 + 1/2·[x^2 | -x ≥ 0] | | | | | `- 1/2 + 1/2·[x^2 | -x ≥ 0] | | | `- 1000·[x + -y | x + -y ≥ 0] + [y | y ≥ 0] + 1/2 + 1/2·[x^2 | -x ≥ 0] | `- [x + -y | x + -y ≥ 0] + 1000·[x + -y | x + -y ≥ 0] + [y | y ≥ 0] + 1/2 + 1/2·[x^2 | -x ≥ 0]