Expected Cost
|
+- [f]
|    0
|
+- [Program]
|    coupons :~ {1 : 0}
|    draw :~ {1 : 0}
|    0:While(50 ≥ 1 + coupons ∧  coupons ≥ 0)
|        Tick(1)
|        draw :~ {1/51 : 0;1/51 : 1;1/51 : 2;1/51 : 3;1/51 : 4;1/51 : 5;1/51 : 6;1/51 : 7;1/51 : 8;1/51 : 9;1/51 : 10;1/51 : 11;1/51 : 12;1/51 : 13;1/51 : 14;1/51 : 15;1/51 : 16;1/51 : 17;1/51 : 18;1/51 : 19;1/51 : 20;1/51 : 21;1/51 : 22;1/51 : 23;1/51 : 24;1/51 : 25;1/51 : 26;1/51 : 27;1/51 : 28;1/51 : 29;1/51 : 30;1/51 : 31;1/51 : 32;1/51 : 33;1/51 : 34;1/51 : 35;1/51 : 36;1/51 : 37;1/51 : 38;1/51 : 39;1/51 : 40;1/51 : 41;1/51 : 42;1/51 : 43;1/51 : 44;1/51 : 45;1/51 : 46;1/51 : 47;1/51 : 48;1/51 : 49;1/51 : 50}
|        1:If(draw ≥ 1 + coupons) Then
|            coupons :~ {1 : 1 + coupons}
|          Else
|            Skip
|
+- While.step
|  |
|  +- [Problem]
|  |    0:While(50 ≥ 1 + coupons ∧  coupons ≥ 0)
|  |        Tick(1)
|  |        draw :~ {1/51 : 0;1/51 : 1;1/51 : 2;1/51 : 3;1/51 : 4;1/51 : 5;1/51 : 6;1/51 : 7;1/51 : 8;1/51 : 9;1/51 : 10;1/51 : 11;1/51 : 12;1/51 : 13;1/51 : 14;1/51 : 15;1/51 : 16;1/51 : 17;1/51 : 18;1/51 : 19;1/51 : 20;1/51 : 21;1/51 : 22;1/51 : 23;1/51 : 24;1/51 : 25;1/51 : 26;1/51 : 27;1/51 : 28;1/51 : 29;1/51 : 30;1/51 : 31;1/51 : 32;1/51 : 33;1/51 : 34;1/51 : 35;1/51 : 36;1/51 : 37;1/51 : 38;1/51 : 39;1/51 : 40;1/51 : 41;1/51 : 42;1/51 : 43;1/51 : 44;1/51 : 45;1/51 : 46;1/51 : 47;1/51 : 48;1/51 : 49;1/51 : 50}
|  |        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] + [50 + -coupons | 50 + -coupons ≥ 0]
|  |
|  +- [Norms]
|  |    [[1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[50 + -coupons | 50 + -coupons ≥ 0]]
|  |
|  +- [Invariant]
|  |    50 ≥ 1 + coupons ∧  coupons ≥ 0 ==> [1 | ⊤] + h([1 | ⊤],ite(0 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(1 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(2 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(3 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(4 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(5 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(6 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(7 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(8 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(9 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(10 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(11 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(12 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(13 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(14 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(15 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(16 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(17 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(18 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(19 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(20 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(21 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(22 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(23 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(24 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(25 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(26 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(27 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(28 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(29 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(30 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(31 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(32 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(33 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(34 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(35 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(36 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(37 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(38 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(39 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(40 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(41 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(42 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(43 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(44 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(45 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(46 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(47 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(48 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(49 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]) + ite(50 ≥ 1 + coupons,1/51·[2 + coupons | 2 + coupons ≥ 0],1/51·[1 + coupons | 1 + coupons ≥ 0]),ite(0 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(1 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(2 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(3 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(4 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(5 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(6 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(7 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(8 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(9 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(10 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(11 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(12 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(13 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(14 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(15 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(16 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(17 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(18 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(19 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(20 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(21 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(22 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(23 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(24 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(25 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(26 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(27 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(28 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(29 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(30 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(31 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(32 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(33 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(34 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(35 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(36 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(37 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(38 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(39 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(40 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(41 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(42 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(43 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(44 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(45 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(46 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(47 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(48 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(49 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0]) + ite(50 ≥ 1 + coupons,1/51·[49 + -coupons | 49 + -coupons ≥ 0],1/51·[50 + -coupons | 50 + -coupons ≥ 0])) ≼ h([1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[50 + -coupons | 50 + -coupons ≥ 0])
|  |    0 ≥ 1 + coupons ∨  1 + coupons ≥ 51 ==> 0 ≼ h([1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[50 + -coupons | 50 + -coupons ≥ 0])
|  |
|  `- 51·[50 + -coupons | 50 + -coupons ≥ 0]
|
`- 2550