Expected Cost | +- [f] | 0 | +- [Program] | 0:If(y ≥ 10) Then | Skip | Else | Abort | 1:While(x + -y ≥ 3) | r :~ {1/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4} | 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/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4} | | y :~ {1 : r + y} | | Tick(3) | | | +- While.step | | | | | +- [Problem] | | | 1:While(x + -y ≥ 3) | | | r :~ {1/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4} | | | 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/16·[-2 + x + -y | -2 + x + -y ≥ 0] + 1/4·[-3 + x + -y | -3 + x + -y ≥ 0] + 3/8·[-4 + x + -y | -4 + x + -y ≥ 0] + 1/4·[-5 + x + -y | -5 + x + -y ≥ 0] + 1/16·[-6 + x + -y | -6 + 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]) | | | | | `- 16/5·[-2 + x + -y | -2 + x + -y ≥ 0] | | | `- 16/5·[-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/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4} | | y :~ {1 : r + y} | | Tick(3) | | | +- While.step | | | | | +- [Problem] | | | 1:While(x + -y ≥ 3) | | | r :~ {1/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4} | | | 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/16·[-9 + y | -9 + y ≥ 0] + 1/4·[-8 + y | -8 + y ≥ 0] + 3/8·[-7 + y | -7 + y ≥ 0] + 1/4·[-6 + y | -6 + y ≥ 0] + 1/16·[-5 + y | -5 + y ≥ 0],1/16·[-2 + x + -y | -2 + x + -y ≥ 0] + 1/4·[-3 + x + -y | -3 + x + -y ≥ 0] + 3/8·[-4 + x + -y | -4 + x + -y ≥ 0] + 1/4·[-5 + x + -y | -5 + x + -y ≥ 0] + 1/16·[-6 + x + -y | -6 + 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] + 16/5·[-2 + x + -y | -2 + x + -y ≥ 0] | | | `- 3/2·[-9 + y | -9 + y ≥ 0] + 16/5·[-2 + x + -y | -2 + x + -y ≥ 0] | `- [y ≥ 10] · (16/5·[-2 + x + -y | -2 + x + -y ≥ 0] + 3/2·[-9 + y | -9 + y ≥ 0] + 16/5·[-2 + x + -y | -2 + x + -y ≥ 0])