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 : 50 + i + k} | 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 : 50 + i + k} | | 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]