ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | x :~ {1/3 : 1;1/3 : 2;1/3 : 3} | z :~ {1 : x} | Tick(1) | 0:While(x 1) | Tick(1) | y :~ {1 : z} | 1:While(y 1) | y :~ {1 : -1 + y} | Tick(1) | x :~ {1 : -1 + x} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(x 1) | | Tick(1) | | y :~ {1 : z} | | 1:While(y 1) | | y :~ {1 : -1 + y} | | Tick(1) | | x :~ {1 : -1 + x} | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | 1:While(y 1) | | | | y :~ {1 : -1 + y} | | | | Tick(1) | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 1:While(y 1) | | | | | y :~ {1 : -1 + y} | | | | | Tick(1) | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | `- [1 | ] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [y | y 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ],[y | y 0]] | | | | | | | | | +- [Invariant] | | | | | y 1 ==> [1 | ] + h([1 | ],[-1 + y | -1 + y 0]) h([1 | ],[y | y 0]) | | | | | 1 1 + y ==> 0 h([1 | ],[y | y 0]) | | | | | | | | | `- [y | y 0] | | | | | | | `- [y | y 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | x :~ {1 : -1 + x} | | | | Tick(1) | | | | | | | `- [1 | ] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | [1 | ] | | | | | | | +- [Program] | | | | 1:While(y 1) | | | | y :~ {1 : -1 + y} | | | | Tick(1) | | | | | | | `- [1 | ] | | | | | `- [1 | ] + [z | z 0] + [1 | ] | | | +- mixed-lin-template | | | | | `- 1 + 2([x | x 0]) + [x | x 0][z | z 0] + [x | x 0]^2 + [z | z 0] | | | +- [Norms] | | [[1 | ],[x | x 0],[xz | x 0 z 0],[x^2 | x 0],[z | z 0]] | | | +- [Invariant] | | x 1 ==> [1 | ] + [z | z 0] + [1 | ] + h([1 | ],[-1 + x | -1 + x 0],[xz + -z | -1 + x 0 z 0],[1 + -2(x) + x^2 | -1 + x 0],[z | z 0]) h([1 | ],[x | x 0],[xz | x 0 z 0],[x^2 | x 0],[z | z 0]) | | 1 1 + x ==> 0 h([1 | ],[x | x 0],[xz | x 0 z 0],[x^2 | x 0],[z | z 0]) | | | `- 2[x | x 0] + [xz | x 0 z 0] | `- 29/3 [Success] 29/3 Degree: 0