Expected Cost | +- [f] | 0 | +- [Program] | 0:If(y ≥ 0) Then | Skip | Else | Abort | 1:While(x ≥ 1 + y) | x :~ {1 : x + -y} | x :~ {1 : -1 + x} | t :~ {1 : y} | 2:While(t ≥ 1) | r :~ {1/2 : 0;1/2 : 1} | t :~ {1 : -r + t} | Tick(1) | Tick(1) | +- While.step | | | +- [Problem] | | 1:While(x ≥ 1 + y) | | x :~ {1 : x + -y} | | x :~ {1 : -1 + x} | | t :~ {1 : y} | | 2:While(t ≥ 1) | | r :~ {1/2 : 0;1/2 : 1} | | t :~ {1 : -r + t} | | Tick(1) | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | 2:While(t ≥ 1) | | | | r :~ {1/2 : 0;1/2 : 1} | | | | t :~ {1 : -r + t} | | | | Tick(1) | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 2:While(t ≥ 1) | | | | | r :~ {1/2 : 0;1/2 : 1} | | | | | t :~ {1 : -r + t} | | | | | Tick(1) | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | `- [1 | ⊤] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [t | t ≥ 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ⊤],[t | t ≥ 0]] | | | | | | | | | +- [Invariant] | | | | | t ≥ 1 ==> [1 | ⊤] + h([1 | ⊤],1/2·[t | t ≥ 0] + 1/2·[-1 + t | -1 + t ≥ 0]) ≼ h([1 | ⊤],[t | t ≥ 0]) | | | | | 1 ≥ 1 + t ==> 0 ≼ h([1 | ⊤],[t | t ≥ 0]) | | | | | | | | | `- 2·[t | t ≥ 0] | | | | | | | `- 2·[t | t ≥ 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | Tick(1) | | | | | | | `- [1 | ⊤] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | [1 | ⊤] | | | | | | | +- [Program] | | | | 2:While(t ≥ 1) | | | | r :~ {1/2 : 0;1/2 : 1} | | | | t :~ {1 : -r + t} | | | | Tick(1) | | | | | | | `- [1 | ⊤] | | | | | `- 2·[y | y ≥ 0] + [1 | ⊤] | | | +- shift-avg-template | | | | | `- 1 + [1 + x | 1 + x ≥ 0] + [1 + y | 1 + y ≥ 0] + [y | y ≥ 0] | | | +- [Norms] | | [[1 | ⊤],[1 + x | 1 + x ≥ 0],[1 + y | 1 + y ≥ 0],[y | y ≥ 0]] | | | +- [Invariant] | | x ≥ 1 + y ∧ y ≥ 0 ==> 2·[y | y ≥ 0] + [1 | ⊤] + h([1 | ⊤],[x + -y | x + -y ≥ 0],[1 + y | 1 + y ≥ 0],[y | y ≥ 0]) ≼ h([1 | ⊤],[1 + x | 1 + x ≥ 0],[1 + y | 1 + y ≥ 0],[y | y ≥ 0]) | | 1 + y ≥ 1 + x ∧ y ≥ 0 ==> 0 ≼ h([1 | ⊤],[1 + x | 1 + x ≥ 0],[1 + y | 1 + y ≥ 0],[y | y ≥ 0]) | | | `- [y ≥ 0] · 2·[1 + x | 1 + x ≥ 0] | `- [y ≥ 0] · 2·[1 + x | 1 + x ≥ 0]