Expected Cost | +- [f] | 0 | +- [Program] | coupons :~ {1 : 0} | 0:While(N ≥ 1 + coupons ∧ coupons ≥ 0) | Tick(1) | draw :~ rand(N) | draw :~ {1 : 1 + draw} | 1:If(draw ≥ 1 + coupons) Then | coupons :~ {1 : 1 + coupons} | Else | Skip | +- While.step | | | +- [Problem] | | 0:While(N ≥ 1 + coupons ∧ coupons ≥ 0) | | Tick(1) | | draw :~ rand(N) | | draw :~ {1 : 1 + draw} | | 1:If(draw ≥ 1 + coupons) Then | | coupons :~ {1 : 1 + coupons} | | Else | | Skip | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- [1 | ⊤] | | | +- mixed-iteration-template | | | | | `- [1 + coupons | 1 + coupons ≥ 0] + 2·([1 + coupons | 1 + coupons ≥ 0]·[N + -coupons | N + -coupons ≥ 0]) + [1 + coupons | 1 + coupons ≥ 0]^2 + [N + -coupons | N + -coupons ≥ 0] + [N + -coupons | N + -coupons ≥ 0]^2 | | | +- [Norms] | | [[1 + coupons | 1 + coupons ≥ 0],[N + N·coupons + -coupons + -coupons^2 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0],[1 + 2·(coupons) + coupons^2 | 1 + coupons ≥ 0],[N + -coupons | N + -coupons ≥ 0],[-2·(N·coupons) + N^2 + coupons^2 | N + -coupons ≥ 0]] | | | +- expectation | | | | | +- [dist] | | | rand(N) | | | | | +- [f] | | | ite(1 + @i ≥ 1 + coupons,[-2 + 2·(N) + N·coupons + -3·(coupons) + -coupons^2 | -1 + N + -coupons ≥ 0 ∧ 2 + coupons ≥ 0],[N + N·coupons + -coupons + -coupons^2 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0]) | | | | | +- bounded-sum | | | | | | | +- [expression] | | | | sum{[1 + @i ≥ 1 + coupons] · [-2 + 2·(N) + N·coupons + -3·(coupons) + -coupons^2 | -1 + N + -coupons ≥ 0 ∧ 2 + coupons ≥ 0] | 0 <= @i <= -1 + N} | | | | | | | +- guarded-template | | | | | | | | | `- [-2 + 2·(N) + N·coupons + -3·(coupons) + -coupons^2 | -1 + N + -coupons ≥ 0 ∧ 2 + coupons ≥ 0]·[1 + @i + -coupons | 1 + @i + -coupons ≥ 0] | | | | | | | `- [-2·(N) + -5·(N·coupons) + -2·(N·coupons^2) + 2·(N^2) + N^2·coupons + 2·(coupons) + 3·(coupons^2) + coupons^3 | -1 + N + -coupons ≥ 0 ∧ 2 + coupons ≥ 0 ∧ N + -coupons ≥ 0] | | | | | +- bounded-sum | | | | | | | +- [expression] | | | | sum{[1 + coupons ≥ 2 + @i] · [N + N·coupons + -coupons + -coupons^2 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0] | 0 <= @i <= -1 + N} | | | | | | | +- guarded-template | | | | | | | | | `- [N + N·coupons + -coupons + -coupons^2 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0]·[-@i + coupons | -@i + coupons ≥ 0] | | | | | | | `- [N·coupons + N·coupons^2 + -coupons^2 + -coupons^3 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0 ∧ coupons ≥ 0] | | | | | `- [N ≥ 1] · ([-2·(N) + -5·(N·coupons) + -2·(N·coupons^2) + 2·(N^2) + N^2·coupons + 2·(coupons) + 3·(coupons^2) + coupons^3 | -1 + N + -coupons ≥ 0 ∧ 2 + coupons ≥ 0 ∧ N + -coupons ≥ 0] + [N·coupons + N·coupons^2 + -coupons^2 + -coupons^3 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0 ∧ coupons ≥ 0] / N) | | | +- expectation | | | | | +- [dist] | | | rand(N) | | | | | +- [f] | | | ite(1 + @i ≥ 1 + coupons,[4 + 4·(coupons) + coupons^2 | 2 + coupons ≥ 0],[1 + 2·(coupons) + coupons^2 | 1 + coupons ≥ 0]) | | | | | +- bounded-sum | | | | | | | +- [expression] | | | | sum{[1 + @i ≥ 1 + coupons] · [4 + 4·(coupons) + coupons^2 | 2 + coupons ≥ 0] | 0 <= @i <= -1 + N} | | | | | | | +- guarded-template | | | | | | | | | `- [1 + @i + -coupons | 1 + @i + -coupons ≥ 0]·[4 + 4·(coupons) + coupons^2 | 2 + coupons ≥ 0] | | | | | | | `- [4·(N) + 4·(N·coupons) + N·coupons^2 + -4·(coupons) + -4·(coupons^2) + -coupons^3 | 2 + coupons ≥ 0 ∧ N + -coupons ≥ 0] | | | | | +- bounded-sum | | | | | | | +- [expression] | | | | sum{[1 + coupons ≥ 2 + @i] · [1 + 2·(coupons) + coupons^2 | 1 + coupons ≥ 0] | 0 <= @i <= -1 + N} | | | | | | | +- guarded-template | | | | | | | | | `- [1 + 2·(coupons) + coupons^2 | 1 + coupons ≥ 0]·[-@i + coupons | -@i + coupons ≥ 0] | | | | | | | `- [coupons + 2·(coupons^2) + coupons^3 | 1 + coupons ≥ 0 ∧ coupons ≥ 0] | | | | | `- [N ≥ 1] · ([4·(N) + 4·(N·coupons) + N·coupons^2 + -4·(coupons) + -4·(coupons^2) + -coupons^3 | 2 + coupons ≥ 0 ∧ N + -coupons ≥ 0] + [coupons + 2·(coupons^2) + coupons^3 | 1 + coupons ≥ 0 ∧ coupons ≥ 0] / N) | | | +- expectation | | | | | +- [dist] | | | rand(N) | | | | | +- [f] | | | ite(1 + @i ≥ 1 + coupons,[1 + -2·(N) + -2·(N·coupons) + N^2 + 2·(coupons) + coupons^2 | -1 + N + -coupons ≥ 0],[-2·(N·coupons) + N^2 + coupons^2 | N + -coupons ≥ 0]) | | | | | +- bounded-sum | | | | | | | +- [expression] | | | | sum{[1 + @i ≥ 1 + coupons] · [1 + -2·(N) + -2·(N·coupons) + N^2 + 2·(coupons) + coupons^2 | -1 + N + -coupons ≥ 0] | 0 <= @i <= -1 + N} | | | | | | | +- guarded-template | | | | | | | | | `- [1 + -2·(N) + -2·(N·coupons) + N^2 + 2·(coupons) + coupons^2 | -1 + N + -coupons ≥ 0]·[1 + @i + -coupons | 1 + @i + -coupons ≥ 0] | | | | | | | `- [N + 4·(N·coupons) + 3·(N·coupons^2) + -2·(N^2) + -3·(N^2·coupons) + N^3 + -coupons + -2·(coupons^2) + -coupons^3 | -1 + N + -coupons ≥ 0 ∧ N + -coupons ≥ 0] | | | | | +- bounded-sum | | | | | | | +- [expression] | | | | sum{[1 + coupons ≥ 2 + @i] · [-2·(N·coupons) + N^2 + coupons^2 | N + -coupons ≥ 0] | 0 <= @i <= -1 + N} | | | | | | | +- guarded-template | | | | | | | | | `- [-@i + coupons | -@i + coupons ≥ 0]·[-2·(N·coupons) + N^2 + coupons^2 | N + -coupons ≥ 0] | | | | | | | `- [-2·(N·coupons^2) + N^2·coupons + coupons^3 | N + -coupons ≥ 0 ∧ coupons ≥ 0] | | | | | `- [N ≥ 1] · ([N + 4·(N·coupons) + 3·(N·coupons^2) + -2·(N^2) + -3·(N^2·coupons) + N^3 + -coupons + -2·(coupons^2) + -coupons^3 | -1 + N + -coupons ≥ 0 ∧ N + -coupons ≥ 0] + [-2·(N·coupons^2) + N^2·coupons + coupons^3 | N + -coupons ≥ 0 ∧ coupons ≥ 0] / N) | | | +- [Invariant] | | N ≥ 1 + coupons ∧ coupons ≥ 0 ==> [1 | ⊤] + h([N ≥ 1] · ([2·(N) + N·coupons + -2·(coupons) + -coupons^2 | 2 + coupons ≥ 0 ∧ N + -coupons ≥ 0] + [coupons + coupons^2 | 1 + coupons ≥ 0 ∧ coupons ≥ 0] / N),[N ≥ 1] · ([-2·(N) + -5·(N·coupons) + -2·(N·coupons^2) + 2·(N^2) + N^2·coupons + 2·(coupons) + 3·(coupons^2) + coupons^3 | -1 + N + -coupons ≥ 0 ∧ 2 + coupons ≥ 0 ∧ N + -coupons ≥ 0] + [N·coupons + N·coupons^2 + -coupons^2 + -coupons^3 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0 ∧ coupons ≥ 0] / N),[N ≥ 1] · ([4·(N) + 4·(N·coupons) + N·coupons^2 + -4·(coupons) + -4·(coupons^2) + -coupons^3 | 2 + coupons ≥ 0 ∧ N + -coupons ≥ 0] + [coupons + 2·(coupons^2) + coupons^3 | 1 + coupons ≥ 0 ∧ coupons ≥ 0] / N),[N ≥ 1] · ([-N + -2·(N·coupons) + N^2 + coupons + coupons^2 | -1 + N + -coupons ≥ 0 ∧ N + -coupons ≥ 0] + [N·coupons + -coupons^2 | N + -coupons ≥ 0 ∧ coupons ≥ 0] / N),[N ≥ 1] · ([N + 4·(N·coupons) + 3·(N·coupons^2) + -2·(N^2) + -3·(N^2·coupons) + N^3 + -coupons + -2·(coupons^2) + -coupons^3 | -1 + N + -coupons ≥ 0 ∧ N + -coupons ≥ 0] + [-2·(N·coupons^2) + N^2·coupons + coupons^3 | N + -coupons ≥ 0 ∧ coupons ≥ 0] / N)) ≼ h([1 + coupons | 1 + coupons ≥ 0],[N + N·coupons + -coupons + -coupons^2 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0],[1 + 2·(coupons) + coupons^2 | 1 + coupons ≥ 0],[N + -coupons | N + -coupons ≥ 0],[-2·(N·coupons) + N^2 + coupons^2 | N + -coupons ≥ 0]) | | 0 ≥ 1 + coupons ∨ 1 + coupons ≥ 1 + N ==> 0 ≼ h([1 + coupons | 1 + coupons ≥ 0],[N + N·coupons + -coupons + -coupons^2 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0],[1 + 2·(coupons) + coupons^2 | 1 + coupons ≥ 0],[N + -coupons | N + -coupons ≥ 0],[-2·(N·coupons) + N^2 + coupons^2 | N + -coupons ≥ 0]) | | | `- 1/2·[1 + coupons | 1 + coupons ≥ 0] + [N + N·coupons + -coupons + -coupons^2 | 1 + coupons ≥ 0 ∧ N + -coupons ≥ 0] + 1/2·[-2·(N·coupons) + N^2 + coupons^2 | N + -coupons ≥ 0] | `- 1/2 + [N | N ≥ 0] + 1/2·[N^2 | N ≥ 0]