ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:While(n  1 + x)
   |        Choice
   |          1/2: sample :~ {1/3 : 0;1/3 : 1;1/3 : 2}
   |               x :~ {1 : sample + x}
   |          1/2: sample :~ {1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3;1/6 : 4;1/6 : 5}
   |               x :~ {1 : sample + x}
   |        Tick(2)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(n  1 + x)
   |  |        Choice
   |  |          1/2: sample :~ {1/3 : 0;1/3 : 1;1/3 : 2}
   |  |               x :~ {1 : sample + x}
   |  |          1/2: sample :~ {1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3;1/6 : 4;1/6 : 5}
   |  |               x :~ {1 : sample + x}
   |  |        Tick(2)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- 2
   |  |
   |  +- linear-template
   |  |  |
   |  |  `- 1 + [n + -x | n + -x  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[n + -x | n + -x  0]]
   |  |
   |  +- [Invariant]
   |  |    n  1 + x ==> 2 + h([1 | ],1/6[n + -x | n + -x  0] + 1/6[-1 + n + -x | -1 + n + -x  0] + 1/6[-2 + n + -x | -2 + n + -x  0] + 1/12[n + -x | n + -x  0] + 1/12[-1 + n + -x | -1 + n + -x  0] + 1/12[-2 + n + -x | -2 + n + -x  0] + 1/12[-3 + n + -x | -3 + n + -x  0] + 1/12[-4 + n + -x | -4 + n + -x  0] + 1/12[-5 + n + -x | -5 + n + -x  0])  h([1 | ],[n + -x | n + -x  0])
   |  |    1 + x  1 + n ==> 0  h([1 | ],[n + -x | n + -x  0])
   |  |
   |  `- 8/3[n + -x | n + -x  0]
   |
   `- 8/3[n + -x | n + -x  0]

[Success] 8/3[n + -x | n + -x
                0]
Degree: 1