Expected Cost | +- [f] | 0 | +- [Program] | 0:While(t ≥ h) | t :~ {1 : 1 + t} | Choice | 1/2: r :~ {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 + r} | 1/2: h :~ {1 : h} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(t ≥ h) | | t :~ {1 : 1 + t} | | Choice | | 1/2: r :~ {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 + r} | | 1/2: h :~ {1 : h} | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- [1 | ⊤] | | | +- shift-avg-template | | | | | `- 1 + [3 + -h + t | 3 + -h + t ≥ 0] | | | +- [Norms] | | [[1 | ⊤],[3 + -h + t | 3 + -h + t ≥ 0]] | | | +- [Invariant] | | t ≥ h ==> [1 | ⊤] + 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]) ≼ h([1 | ⊤],[3 + -h + t | 3 + -h + t ≥ 0]) | | h ≥ 1 + t ==> 0 ≼ h([1 | ⊤],[3 + -h + t | 3 + -h + t ≥ 0]) | | | `- 11/6·[3 + -h + t | 3 + -h + t ≥ 0] | `- 11/6·[3 + -h + t | 3 + -h + t ≥ 0]