Expected Cost | +- [f] | 0 | +- [Program] | 0:If(y ≥ 10) Then | Skip | Else | Abort | 1:While(x + -y ≥ 3) | r :~ {1/3 : 1;1/3 : 2;1/3 : 3} | y :~ {1 : r + y} | Tick(3) | 2:While(y ≥ 10) | Choice | 2/3: y :~ {1 : -10 + y} | 1/3: y :~ {1 : y} | Tick(1) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 1:While(x + -y ≥ 3) | | r :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | y :~ {1 : r + y} | | Tick(3) | | | +- While.step | | | | | +- [Problem] | | | 1:While(x + -y ≥ 3) | | | r :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | | y :~ {1 : r + y} | | | Tick(3) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- 3 | | | | | +- linear-template | | | | | | | `- 1 + [-2 + x + -y | -2 + x + -y ≥ 0] | | | | | +- [Norms] | | | [[1 | ⊤],[-2 + x + -y | -2 + x + -y ≥ 0]] | | | | | +- [Invariant] | | | x + -y ≥ 3 ==> 3 + h([1 | ⊤],1/3·[-3 + x + -y | -3 + x + -y ≥ 0] + 1/3·[-4 + x + -y | -4 + x + -y ≥ 0] + 1/3·[-5 + x + -y | -5 + x + -y ≥ 0]) ≼ h([1 | ⊤],[-2 + x + -y | -2 + x + -y ≥ 0]) | | | 3 ≥ 1 + x + -y ==> 0 ≼ h([1 | ⊤],[-2 + x + -y | -2 + x + -y ≥ 0]) | | | | | `- 3·[-2 + x + -y | -2 + x + -y ≥ 0] | | | `- 3·[-2 + x + -y | -2 + x + -y ≥ 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 2:While(y ≥ 10) | | Choice | | 2/3: y :~ {1 : -10 + y} | | 1/3: y :~ {1 : y} | | Tick(1) | | | +- While.step | | | | | +- [Problem] | | | 2:While(y ≥ 10) | | | Choice | | | 2/3: y :~ {1 : -10 + y} | | | 1/3: y :~ {1 : y} | | | Tick(1) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ⊤] | | | | | +- linear-template | | | | | | | `- 1 + [-9 + y | -9 + y ≥ 0] | | | | | +- [Norms] | | | [[1 | ⊤],[-9 + y | -9 + y ≥ 0]] | | | | | +- [Invariant] | | | y ≥ 10 ==> [1 | ⊤] + h([1 | ⊤],2/3·[-19 + y | -19 + y ≥ 0] + 1/3·[-9 + y | -9 + y ≥ 0]) ≼ h([1 | ⊤],[-9 + y | -9 + y ≥ 0]) | | | 10 ≥ 1 + y ==> 0 ≼ h([1 | ⊤],[-9 + y | -9 + y ≥ 0]) | | | | | `- 3/2·[-9 + y | -9 + y ≥ 0] | | | `- 3/2·[-9 + y | -9 + y ≥ 0] | +- Expected Cost | | | +- [f] | | 3/2·[-9 + y | -9 + y ≥ 0] | | | +- [Program] | | 1:While(x + -y ≥ 3) | | r :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | y :~ {1 : r + y} | | Tick(3) | | | +- While.step | | | | | +- [Problem] | | | 1:While(x + -y ≥ 3) | | | r :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | | y :~ {1 : r + y} | | | Tick(3) | | | | | +- [f] | | | 3/2·[-9 + y | -9 + y ≥ 0] | | | | | +- linear-template | | | | | | | `- 1 + [-9 + y | -9 + y ≥ 0] + 2·([-2 + x + -y | -2 + x + -y ≥ 0]) | | | | | +- [Norms] | | | [[1 | ⊤],[-9 + y | -9 + y ≥ 0],[-2 + x + -y | -2 + x + -y ≥ 0]] | | | | | +- [Invariant] | | | x + -y ≥ 3 ==> 0 + h([1 | ⊤],1/3·[-8 + y | -8 + y ≥ 0] + 1/3·[-7 + y | -7 + y ≥ 0] + 1/3·[-6 + y | -6 + y ≥ 0],1/3·[-3 + x + -y | -3 + x + -y ≥ 0] + 1/3·[-4 + x + -y | -4 + x + -y ≥ 0] + 1/3·[-5 + x + -y | -5 + x + -y ≥ 0]) ≼ h([1 | ⊤],[-9 + y | -9 + y ≥ 0],[-2 + x + -y | -2 + x + -y ≥ 0]) | | | 3 ≥ 1 + x + -y ==> 3/2·[-9 + y | -9 + y ≥ 0] ≼ h([1 | ⊤],[-9 + y | -9 + y ≥ 0],[-2 + x + -y | -2 + x + -y ≥ 0]) | | | | | `- 3/2·[-9 + y | -9 + y ≥ 0] + 3·[-2 + x + -y | -2 + x + -y ≥ 0] | | | `- 3/2·[-9 + y | -9 + y ≥ 0] + 3·[-2 + x + -y | -2 + x + -y ≥ 0] | `- [y ≥ 10] · (3·[-2 + x + -y | -2 + x + -y ≥ 0] + 3/2·[-9 + y | -9 + y ≥ 0] + 3·[-2 + x + -y | -2 + x + -y ≥ 0])