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