Expected Cost | +- [f] | 0 | +- [Program] | coupons :~ {1 : 0} | draw :~ {1 : 0} | 0:While(100 ≥ 1 + coupons ∧ coupons ≥ 0) | Tick(1) | draw :~ {1/101 : 0;1/101 : 1;1/101 : 2;1/101 : 3;1/101 : 4;1/101 : 5;1/101 : 6;1/101 : 7;1/101 : 8;1/101 : 9;1/101 : 10;1/101 : 11;1/101 : 12;1/101 : 13;1/101 : 14;1/101 : 15;1/101 : 16;1/101 : 17;1/101 : 18;1/101 : 19;1/101 : 20;1/101 : 21;1/101 : 22;1/101 : 23;1/101 : 24;1/101 : 25;1/101 : 26;1/101 : 27;1/101 : 28;1/101 : 29;1/101 : 30;1/101 : 31;1/101 : 32;1/101 : 33;1/101 : 34;1/101 : 35;1/101 : 36;1/101 : 37;1/101 : 38;1/101 : 39;1/101 : 40;1/101 : 41;1/101 : 42;1/101 : 43;1/101 : 44;1/101 : 45;1/101 : 46;1/101 : 47;1/101 : 48;1/101 : 49;1/101 : 50;1/101 : 51;1/101 : 52;1/101 : 53;1/101 : 54;1/101 : 55;1/101 : 56;1/101 : 57;1/101 : 58;1/101 : 59;1/101 : 60;1/101 : 61;1/101 : 62;1/101 : 63;1/101 : 64;1/101 : 65;1/101 : 66;1/101 : 67;1/101 : 68;1/101 : 69;1/101 : 70;1/101 : 71;1/101 : 72;1/101 : 73;1/101 : 74;1/101 : 75;1/101 : 76;1/101 : 77;1/101 : 78;1/101 : 79;1/101 : 80;1/101 : 81;1/101 : 82;1/101 : 83;1/101 : 84;1/101 : 85;1/101 : 86;1/101 : 87;1/101 : 88;1/101 : 89;1/101 : 90;1/101 : 91;1/101 : 92;1/101 : 93;1/101 : 94;1/101 : 95;1/101 : 96;1/101 : 97;1/101 : 98;1/101 : 99;1/101 : 100} | 1:If(draw ≥ 1 + coupons) Then | coupons :~ {1 : 1 + coupons} | Else | Skip | +- While.step | | | +- [Problem] | | 0:While(100 ≥ 1 + coupons ∧ coupons ≥ 0) | | Tick(1) | | draw :~ {1/101 : 0;1/101 : 1;1/101 : 2;1/101 : 3;1/101 : 4;1/101 : 5;1/101 : 6;1/101 : 7;1/101 : 8;1/101 : 9;1/101 : 10;1/101 : 11;1/101 : 12;1/101 : 13;1/101 : 14;1/101 : 15;1/101 : 16;1/101 : 17;1/101 : 18;1/101 : 19;1/101 : 20;1/101 : 21;1/101 : 22;1/101 : 23;1/101 : 24;1/101 : 25;1/101 : 26;1/101 : 27;1/101 : 28;1/101 : 29;1/101 : 30;1/101 : 31;1/101 : 32;1/101 : 33;1/101 : 34;1/101 : 35;1/101 : 36;1/101 : 37;1/101 : 38;1/101 : 39;1/101 : 40;1/101 : 41;1/101 : 42;1/101 : 43;1/101 : 44;1/101 : 45;1/101 : 46;1/101 : 47;1/101 : 48;1/101 : 49;1/101 : 50;1/101 : 51;1/101 : 52;1/101 : 53;1/101 : 54;1/101 : 55;1/101 : 56;1/101 : 57;1/101 : 58;1/101 : 59;1/101 : 60;1/101 : 61;1/101 : 62;1/101 : 63;1/101 : 64;1/101 : 65;1/101 : 66;1/101 : 67;1/101 : 68;1/101 : 69;1/101 : 70;1/101 : 71;1/101 : 72;1/101 : 73;1/101 : 74;1/101 : 75;1/101 : 76;1/101 : 77;1/101 : 78;1/101 : 79;1/101 : 80;1/101 : 81;1/101 : 82;1/101 : 83;1/101 : 84;1/101 : 85;1/101 : 86;1/101 : 87;1/101 : 88;1/101 : 89;1/101 : 90;1/101 : 91;1/101 : 92;1/101 : 93;1/101 : 94;1/101 : 95;1/101 : 96;1/101 : 97;1/101 : 98;1/101 : 99;1/101 : 100} | | 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] + [100 + -coupons | 100 + -coupons ≥ 0] | | | +- [Norms] | | [[1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[100 + -coupons | 100 + -coupons ≥ 0]] | | | +- [Invariant] | | 100 ≥ 1 + coupons ∧ coupons ≥ 0 ==> [1 | ⊤] + h([1 | ⊤] | | ,ite(0 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(1 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(2 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(3 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(4 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(5 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(6 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(7 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(8 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(9 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(10 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(11 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(12 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(13 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(14 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(15 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(16 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(17 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(18 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(19 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(20 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(21 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(22 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(23 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(24 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(25 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(26 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(27 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(28 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(29 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(30 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(31 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(32 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(33 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(34 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(35 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(36 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(37 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(38 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(39 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(40 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(41 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(42 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(43 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(44 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(45 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(46 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(47 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(48 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(49 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(50 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(51 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(52 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(53 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(54 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(55 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(56 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(57 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(58 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(59 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(60 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(61 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(62 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(63 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(64 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(65 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(66 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(67 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(68 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(69 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(70 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(71 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(72 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(73 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(74 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(75 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(76 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(77 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(78 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(79 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(80 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(81 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(82 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(83 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(84 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(85 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(86 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(87 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(88 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(89 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(90 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(91 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(92 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(93 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(94 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(95 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(96 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(97 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(98 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(99 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) + ite(100 ≥ 1 + coupons,1/101·[2 + coupons | 2 + coupons ≥ 0],1/101·[1 + coupons | 1 + coupons ≥ 0]) | | ,ite(0 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(1 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(2 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(3 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(4 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(5 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(6 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(7 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(8 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(9 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(10 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(11 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(12 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(13 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(14 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(15 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(16 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(17 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(18 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(19 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(20 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(21 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(22 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(23 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(24 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(25 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(26 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(27 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(28 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(29 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(30 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(31 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(32 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(33 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(34 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(35 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(36 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(37 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(38 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(39 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(40 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(41 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(42 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(43 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(44 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(45 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(46 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(47 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(48 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(49 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(50 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(51 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(52 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(53 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(54 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(55 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(56 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(57 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(58 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(59 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(60 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(61 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(62 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(63 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(64 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(65 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(66 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(67 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(68 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(69 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(70 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(71 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(72 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(73 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(74 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(75 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(76 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(77 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(78 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(79 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(80 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(81 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(82 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(83 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(84 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(85 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(86 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(87 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(88 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(89 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(90 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(91 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(92 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(93 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(94 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(95 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(96 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(97 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(98 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(99 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0]) + ite(100 ≥ 1 + coupons,1/101·[99 + -coupons | 99 + -coupons ≥ 0],1/101·[100 + -coupons | 100 + -coupons ≥ 0])) ≼ h([1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[100 + -coupons | 100 + -coupons ≥ 0]) | | 0 ≥ 1 + coupons ∨ 1 + coupons ≥ 101 ==> 0 ≼ h([1 | ⊤],[1 + coupons | 1 + coupons ≥ 0],[100 + -coupons | 100 + -coupons ≥ 0]) | | | `- 101·[100 + -coupons | 100 + -coupons ≥ 0] | `- 10100