ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | 0:While(l 8) | sample :~ {1/3 : 6;1/3 : 7;1/3 : 8} | l :~ {1 : l + -sample} | Tick(10) | 1:While(l 1) | l :~ {1 : -1 + l} | Tick(1) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 0:While(l 8) | | sample :~ {1/3 : 6;1/3 : 7;1/3 : 8} | | l :~ {1 : l + -sample} | | Tick(10) | | | +- While.step | | | | | +- [Problem] | | | 0:While(l 8) | | | sample :~ {1/3 : 6;1/3 : 7;1/3 : 8} | | | l :~ {1 : l + -sample} | | | Tick(10) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- 10 | | | | | +- linear-template | | | | | | | `- 1 + [-7 + l | -7 + l 0] | | | | | +- [Norms] | | | [[1 | ],[-7 + l | -7 + l 0]] | | | | | +- [Invariant] | | | l 8 ==> 10 + h([1 | ],1/3[-13 + l | -13 + l 0] + 1/3[-14 + l | -14 + l 0] + 1/3[-15 + l | -15 + l 0]) h([1 | ],[-7 + l | -7 + l 0]) | | | 8 1 + l ==> 0 h([1 | ],[-7 + l | -7 + l 0]) | | | | | `- 10[-7 + l | -7 + l 0] | | | `- 10[-7 + l | -7 + l 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 1:While(l 1) | | l :~ {1 : -1 + l} | | Tick(1) | | | +- While.step | | | | | +- [Problem] | | | 1:While(l 1) | | | l :~ {1 : -1 + l} | | | Tick(1) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ] | | | | | +- linear-template | | | | | | | `- 1 + [l | l 0] | | | | | +- [Norms] | | | [[1 | ],[l | l 0]] | | | | | +- [Invariant] | | | l 1 ==> [1 | ] + h([1 | ],[-1 + l | -1 + l 0]) h([1 | ],[l | l 0]) | | | 1 1 + l ==> 0 h([1 | ],[l | l 0]) | | | | | `- [l | l 0] | | | `- [l | l 0] | +- Expected Cost | | | +- [f] | | [l | l 0] | | | +- [Program] | | 0:While(l 8) | | sample :~ {1/3 : 6;1/3 : 7;1/3 : 8} | | l :~ {1 : l + -sample} | | Tick(10) | | | +- While.step | | | | | +- [Problem] | | | 0:While(l 8) | | | sample :~ {1/3 : 6;1/3 : 7;1/3 : 8} | | | l :~ {1 : l + -sample} | | | Tick(10) | | | | | +- [f] | | | [l | l 0] | | | | | +- linear-template | | | | | | | `- 1 + 2([-7 + l | -7 + l 0]) + [l | l 0] | | | | | +- [Norms] | | | [[1 | ],[-7 + l | -7 + l 0],[l | l 0]] | | | | | +- [Invariant] | | | l 8 ==> 0 + h([1 | ],1/3[-13 + l | -13 + l 0] + 1/3[-14 + l | -14 + l 0] + 1/3[-15 + l | -15 + l 0],1/3[-6 + l | -6 + l 0] + 1/3[-7 + l | -7 + l 0] + 1/3[-8 + l | -8 + l 0]) h([1 | ],[-7 + l | -7 + l 0],[l | l 0]) | | | 8 1 + l ==> [l | l 0] h([1 | ],[-7 + l | -7 + l 0],[l | l 0]) | | | | | `- 7 | | | `- 7 | `- 10[-7 + l | -7 + l 0] + 7 [Success] 10[-7 + l | -7 + l 0] + 7 Degree: 1