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])