ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    x :~ {1 : 0}
   |    0:While(n  1 + x)
   |        sample :~ {1/1024 : 0;10/1024 : 1;45/1024 : 2;120/1024 : 3;210/1024 : 4;252/1024 : 5;210/1024 : 6;120/1024 : 7;45/1024 : 8;10/1024 : 9;1/1024 : 10}
   |        x :~ {1 : sample + x}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(n  1 + x)
   |  |        sample :~ {1/1024 : 0;10/1024 : 1;45/1024 : 2;120/1024 : 3;210/1024 : 4;252/1024 : 5;210/1024 : 6;120/1024 : 7;45/1024 : 8;10/1024 : 9;1/1024 : 10}
   |  |        x :~ {1 : sample + x}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- [1 | ]
   |  |
   |  +- linear-template
   |  |  |
   |  |  `- 1 + [n + -x | n + -x  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[n + -x | n + -x  0]]
   |  |
   |  +- [Invariant]
   |  |    n  1 + x ==> [1 | ] + h([1 | ],1/1024[n + -x | n + -x  0] + 5/512[-1 + n + -x | -1 + n + -x  0] + 45/1024[-2 + n + -x | -2 + n + -x  0] + 15/128[-3 + n + -x | -3 + n + -x  0] + 105/512[-4 + n + -x | -4 + n + -x  0] + 63/256[-5 + n + -x | -5 + n + -x  0] + 105/512[-6 + n + -x | -6 + n + -x  0] + 15/128[-7 + n + -x | -7 + n + -x  0] + 45/1024[-8 + n + -x | -8 + n + -x  0] + 5/512[-9 + n + -x | -9 + n + -x  0] + 1/1024[-10 + n + -x | -10 + n + -x  0])  h([1 | ],[n + -x | n + -x  0])
   |  |    1 + x  1 + n ==> 0  h([1 | ],[n + -x | n + -x  0])
   |  |
   |  `- 1024/1023[n + -x | n + -x  0]
   |
   `- 1024/1023[n | n  0]

[Success] 1024/1023[n | n  0]
Degree: 1