ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:While(t  h)
   |        t :~ {1 : 1 + t}
   |        Choice
   |          1/2: sample :~ {1/11 : 0;1/11 : 1;1/11 : 2;1/11 : 3;1/11 : 4;1/11 : 5;1/11 : 6;1/11 : 7;1/11 : 8;1/11 : 9;1/11 : 10}
   |               h :~ {1 : h + sample}
   |          1/2: h :~ {1 : h}
   |        z :~ {1 : 1 + z}
   |    Tick(z)
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- [Program]
   |  |    0:While(t  h)
   |  |        t :~ {1 : 1 + t}
   |  |        Choice
   |  |          1/2: sample :~ {1/11 : 0;1/11 : 1;1/11 : 2;1/11 : 3;1/11 : 4;1/11 : 5;1/11 : 6;1/11 : 7;1/11 : 8;1/11 : 9;1/11 : 10}
   |  |               h :~ {1 : h + sample}
   |  |          1/2: h :~ {1 : h}
   |  |        z :~ {1 : 1 + z}
   |  |
   |  `- 0
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- [Program]
   |  |    Tick(z)
   |  |
   |  `- [z | z  0]
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    [z | z  0]
   |  |
   |  +- [Program]
   |  |    0:While(t  h)
   |  |        t :~ {1 : 1 + t}
   |  |        Choice
   |  |          1/2: sample :~ {1/11 : 0;1/11 : 1;1/11 : 2;1/11 : 3;1/11 : 4;1/11 : 5;1/11 : 6;1/11 : 7;1/11 : 8;1/11 : 9;1/11 : 10}
   |  |               h :~ {1 : h + sample}
   |  |          1/2: h :~ {1 : h}
   |  |        z :~ {1 : 1 + z}
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    0:While(t  h)
   |  |  |        t :~ {1 : 1 + t}
   |  |  |        Choice
   |  |  |          1/2: sample :~ {1/11 : 0;1/11 : 1;1/11 : 2;1/11 : 3;1/11 : 4;1/11 : 5;1/11 : 6;1/11 : 7;1/11 : 8;1/11 : 9;1/11 : 10}
   |  |  |               h :~ {1 : h + sample}
   |  |  |          1/2: h :~ {1 : h}
   |  |  |        z :~ {1 : 1 + z}
   |  |  |
   |  |  +- [f]
   |  |  |    [z | z  0]
   |  |  |
   |  |  +- shift-avg-template
   |  |  |  |
   |  |  |  `- 1 + 2([3 + -h + t | 3 + -h + t  0]) + [z | z  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[3 + -h + t | 3 + -h + t  0],[z | z  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    t  h ==> 0 + h([1 | ],1/22[4 + -h + t | 4 + -h + t  0] + 1/22[3 + -h + t | 3 + -h + t  0] + 1/22[2 + -h + t | 2 + -h + t  0] + 1/22[1 + -h + t | 1 + -h + t  0] + 1/22[-h + t | -h + t  0] + 1/22[-1 + -h + t | -1 + -h + t  0] + 1/22[-2 + -h + t | -2 + -h + t  0] + 1/22[-3 + -h + t | -3 + -h + t  0] + 1/22[-4 + -h + t | -4 + -h + t  0] + 1/22[-5 + -h + t | -5 + -h + t  0] + 1/22[-6 + -h + t | -6 + -h + t  0] + 1/2[4 + -h + t | 4 + -h + t  0],[1 + z | 1 + z  0])  h([1 | ],[3 + -h + t | 3 + -h + t  0],[z | z  0])
   |  |  |    h  1 + t ==> [z | z  0]  h([1 | ],[3 + -h + t | 3 + -h + t  0],[z | z  0])
   |  |  |
   |  |  `- 11/6[3 + -h + t | 3 + -h + t  0] + [z | z  0]
   |  |
   |  `- 11/6[3 + -h + t | 3 + -h + t  0] + [z | z  0]
   |
   `- 11/6[3 + -h + t | 3 + -h + t  0] + [z | z  0]

[Success] 11/6[3 + -h + t | 3
                 + -h + t  0] + [z | z  0]
Degree: 1