ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | 0:While(i 101) | Choice | 1/2: i :~ {1 : -1 + i} | 1/2: i :~ {1 : i} | Tick(1) | i :~ {1 : i + k} | i :~ {1 : 50 + i} | 1:While(i 0) | i :~ {1 : -1 + i} | Tick(1) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 0:While(i 101) | | Choice | | 1/2: i :~ {1 : -1 + i} | | 1/2: i :~ {1 : i} | | Tick(1) | | | +- While.step | | | | | +- [Problem] | | | 0:While(i 101) | | | Choice | | | 1/2: i :~ {1 : -1 + i} | | | 1/2: i :~ {1 : i} | | | Tick(1) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ] | | | | | +- linear-template | | | | | | | `- 1 + [-100 + i | -100 + i 0] | | | | | +- [Norms] | | | [[1 | ],[-100 + i | -100 + i 0]] | | | | | +- [Invariant] | | | i 101 ==> [1 | ] + h([1 | ],1/2[-101 + i | -101 + i 0] + 1/2[-100 + i | -100 + i 0]) h([1 | ],[-100 + i | -100 + i 0]) | | | 101 1 + i ==> 0 h([1 | ],[-100 + i | -100 + i 0]) | | | | | `- 2[-100 + i | -100 + i 0] | | | `- 2[-100 + i | -100 + i 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | i :~ {1 : i + k} | | i :~ {1 : 50 + i} | | 1:While(i 0) | | i :~ {1 : -1 + i} | | Tick(1) | | | +- While.step | | | | | +- [Problem] | | | 1:While(i 0) | | | i :~ {1 : -1 + i} | | | Tick(1) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ] | | | | | +- linear-template | | | | | | | `- 1 + [1 + i | 1 + i 0] | | | | | +- [Norms] | | | [[1 | ],[1 + i | 1 + i 0]] | | | | | +- [Invariant] | | | i 0 ==> [1 | ] + h([1 | ],[i | i 0]) h([1 | ],[1 + i | 1 + i 0]) | | | 0 1 + i ==> 0 h([1 | ],[1 + i | 1 + i 0]) | | | | | `- [1 + i | 1 + i 0] | | | `- [51 + i + k | 51 + i + k 0] | +- Expected Cost | | | +- [f] | | [51 + i + k | 51 + i + k 0] | | | +- [Program] | | 0:While(i 101) | | Choice | | 1/2: i :~ {1 : -1 + i} | | 1/2: i :~ {1 : i} | | Tick(1) | | | +- While.step | | | | | +- [Problem] | | | 0:While(i 101) | | | Choice | | | 1/2: i :~ {1 : -1 + i} | | | 1/2: i :~ {1 : i} | | | Tick(1) | | | | | +- [f] | | | [51 + i + k | 51 + i + k 0] | | | | | +- linear-template | | | | | | | `- 1 + 2([-100 + i | -100 + i 0]) + [51 + i + k | 51 + i + k 0] | | | | | +- [Norms] | | | [[1 | ],[-100 + i | -100 + i 0],[51 + i + k | 51 + i + k 0]] | | | | | +- [Invariant] | | | i 101 ==> 0 + h([1 | ],1/2[-101 + i | -101 + i 0] + 1/2[-100 + i | -100 + i 0],1/2[50 + i + k | 50 + i + k 0] + 1/2[51 + i + k | 51 + i + k 0]) h([1 | ],[-100 + i | -100 + i 0],[51 + i + k | 51 + i + k 0]) | | | 101 1 + i ==> [51 + i + k | 51 + i + k 0] h([1 | ],[-100 + i | -100 + i 0],[51 + i + k | 51 + i + k 0]) | | | | | `- [51 + i + k | 51 + i + k 0] | | | `- [51 + i + k | 51 + i + k 0] | `- 2[-100 + i | -100 + i 0] + [51 + i + k | 51 + i + k 0] [Success] 2[-100 + i | -100 + i 0] + [51 + i + k | 51 + i + k 0] Degree: 1