Expected Cost
|
+- [f]
|    0
|
+- [Program]
|    coupons :~ {1 : 0}
|    draw :~ {1 : 0}
|    0:While(10 ≥ 1 + coupons ∧  coupons ≥ 0)
|        Tick(1)
|        draw :~ {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}
|        1:If(draw ≥ 1 + coupons) Then
|            coupons :~ {1 : 1 + coupons}
|          Else
|            Skip
|
+- While.step
|  |
|  +- [Problem]
|  |    0:While(10 ≥ 1 + coupons ∧  coupons ≥ 0)
|  |        Tick(1)
|  |        draw :~ {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}
|  |        1:If(draw ≥ 1 + coupons) Then
|  |            coupons :~ {1 : 1 + coupons}
|  |          Else
|  |            Skip
|  |
|  +- [f]
|  |    0
|  |
|  +- Expected Cost Body
|  |  |
|  |  `- [1 | ⊤]
|  |
|  +- linear-template
|  |  |
|  |  `- 1 + [1 + coupons | 1 + coupons ≥ 0] + [10 + -coupons | 10 + -coupons ≥ 0]
|  |
|  +- [Norms]
|  |    [[1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[10 + -coupons | 10 + -coupons ≥ 0]]
|  |
|  +- [Invariant]
|  |    10 ≥ 1 + coupons ∧  coupons ≥ 0 ==> [1 | ⊤] + h([1 | ⊤],ite(0 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(1 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(2 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(3 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(4 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(5 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(6 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(7 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(8 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(9 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]) + ite(10 ≥ 1 + coupons,1/11·[2 + coupons | 2 + coupons ≥ 0],1/11·[1 + coupons | 1 + coupons ≥ 0]),ite(0 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(1 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(2 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(3 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(4 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(5 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(6 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(7 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(8 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(9 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0]) + ite(10 ≥ 1 + coupons,1/11·[9 + -coupons | 9 + -coupons ≥ 0],1/11·[10 + -coupons | 10 + -coupons ≥ 0])) ≼ h([1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[10 + -coupons | 10 + -coupons ≥ 0])
|  |    0 ≥ 1 + coupons ∨  1 + coupons ≥ 11 ==> 0 ≼ h([1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[10 + -coupons | 10 + -coupons ≥ 0])
|  |
|  `- 11·[10 + -coupons | 10 + -coupons ≥ 0]
|
`- 110