ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:While(n  2 + x)
   |        sample :~ {351/435 : 0;81/435 : 1;3/435 : 2}
   |        x :~ {1 : sample + x}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(n  2 + x)
   |  |        sample :~ {351/435 : 0;81/435 : 1;3/435 : 2}
   |  |        x :~ {1 : sample + x}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- [1 | ]
   |  |
   |  +- linear-template
   |  |  |
   |  |  `- 1 + [-1 + n + -x | -1 + n + -x  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[-1 + n + -x | -1 + n + -x  0]]
   |  |
   |  +- [Invariant]
   |  |    n  2 + x ==> [1 | ] + h([1 | ],117/145[-1 + n + -x | -1 + n + -x  0] + 27/145[-2 + n + -x | -2 + n + -x  0] + 1/145[-3 + n + -x | -3 + n + -x  0])  h([1 | ],[-1 + n + -x | -1 + n + -x  0])
   |  |    2 + x  1 + n ==> 0  h([1 | ],[-1 + n + -x | -1 + n + -x  0])
   |  |
   |  `- 145/28[-1 + n + -x | -1 + n + -x  0]
   |
   `- 145/28[-1 + n + -x | -1 + n + -x  0]

[Success] 145/28[-1 + n + -x
                  | -1 + n + -x  0]
Degree: 1