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