Expected Cost
|
+- [f]
|    0
|
+- [Program]
|    i :~ {1 : 0}
|    0:While(5 ≥ 1 + i)
|        1:If(0 ≥ i ∧  i ≥ 0) Then
|            i :~ {1 : 1 + i}
|          Else
|            2:If(1 ≥ i ∧  i ≥ 1) Then
|                Choice
|                  1/5: i :~ {1 : 1}
|                  4/5: i :~ {1 : 1 + i}
|              Else
|                3:If(2 ≥ i ∧  i ≥ 2) Then
|                    Choice
|                      2/5: i :~ {1 : 2}
|                      3/5: i :~ {1 : 1 + i}
|                  Else
|                    4:If(3 ≥ i ∧  i ≥ 3) Then
|                        Choice
|                          3/5: i :~ {1 : 3}
|                          2/5: i :~ {1 : 1 + i}
|                      Else
|                        Choice
|                          4/5: i :~ {1 : 4}
|                          1/5: i :~ {1 : 1 + i}
|        Tick(1)
|
+- While.step
|  |
|  +- [Problem]
|  |    0:While(5 ≥ 1 + i)
|  |        1:If(0 ≥ i ∧  i ≥ 0) Then
|  |            i :~ {1 : 1 + i}
|  |          Else
|  |            2:If(1 ≥ i ∧  i ≥ 1) Then
|  |                Choice
|  |                  1/5: i :~ {1 : 1}
|  |                  4/5: i :~ {1 : 1 + i}
|  |              Else
|  |                3:If(2 ≥ i ∧  i ≥ 2) Then
|  |                    Choice
|  |                      2/5: i :~ {1 : 2}
|  |                      3/5: i :~ {1 : 1 + i}
|  |                  Else
|  |                    4:If(3 ≥ i ∧  i ≥ 3) Then
|  |                        Choice
|  |                          3/5: i :~ {1 : 3}
|  |                          2/5: i :~ {1 : 1 + i}
|  |                      Else
|  |                        Choice
|  |                          4/5: i :~ {1 : 4}
|  |                          1/5: i :~ {1 : 1 + i}
|  |        Tick(1)
|  |
|  +- [f]
|  |    0
|  |
|  +- Expected Cost Body
|  |  |
|  |  `- [1 | ⊤]
|  |
|  +- linear-template
|  |  |
|  |  `- 1 + [5 + -i | 5 + -i ≥ 0]
|  |
|  +- [Norms]
|  |    [[1 | ⊤],[5 + -i | 5 + -i ≥ 0]]
|  |
|  +- [Invariant]
|  |    5 ≥ 1 + i ==> [1 | ⊤] + h([1 | ⊤],ite(0 ≥ i ∧  i ≥ 0,[4 + -i | 4 + -i ≥ 0],ite(1 ≥ i ∧  i ≥ 1,4/5 + 4/5·[4 + -i | 4 + -i ≥ 0],ite(2 ≥ i ∧  i ≥ 2,6/5 + 3/5·[4 + -i | 4 + -i ≥ 0],ite(3 ≥ i ∧  i ≥ 3,6/5 + 2/5·[4 + -i | 4 + -i ≥ 0],4/5 + 1/5·[4 + -i | 4 + -i ≥ 0]))))) ≼ h([1 | ⊤],[5 + -i | 5 + -i ≥ 0])
|  |    1 + i ≥ 6 ==> 0 ≼ h([1 | ⊤],[5 + -i | 5 + -i ≥ 0])
|  |
|  `- 5·[5 + -i | 5 + -i ≥ 0]
|
`- 25