Expected Cost | +- [f] | 0 | +- [Program] | 0:While(min ≥ 0 ∧ price ≥ 1 + min) | Choice | 1/4: price :~ {1 : 1 + price} | 3/4: price :~ {1 : -1 + price} | nShares :~ {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:While(nShares ≥ 1) | nShares :~ {1 : -1 + nShares} | Tick(price) | +- While.step | | | +- [Problem] | | 0:While(min ≥ 0 ∧ price ≥ 1 + min) | | Choice | | 1/4: price :~ {1 : 1 + price} | | 3/4: price :~ {1 : -1 + price} | | nShares :~ {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:While(nShares ≥ 1) | | nShares :~ {1 : -1 + nShares} | | Tick(price) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | +- While.step | | | | | | | +- [Problem] | | | | 1:While(nShares ≥ 1) | | | | nShares :~ {1 : -1 + nShares} | | | | Tick(price) | | | | | | | +- [f] | | | | 0 | | | | | | | +- Expected Cost Body | | | | | | | | | `- [price | price ≥ 0] | | | | | | | +- mixed-lin-template | | | | | | | | | `- 1 + 2·([nShares | nShares ≥ 0]) + [nShares | nShares ≥ 0]·[price | price ≥ 0] + [nShares | nShares ≥ 0]^2 + [price | price ≥ 0] | | | | | | | +- [Norms] | | | | [[1 | ⊤],[nShares | nShares ≥ 0],[nShares·price | nShares ≥ 0 ∧ price ≥ 0],[nShares^2 | nShares ≥ 0],[price | price ≥ 0]] | | | | | | | +- [Invariant] | | | | nShares ≥ 1 ==> [price | price ≥ 0] + h([1 | ⊤],[-1 + nShares | -1 + nShares ≥ 0],[nShares·price + -price | -1 + nShares ≥ 0 ∧ price ≥ 0],[1 + -2·(nShares) + nShares^2 | -1 + nShares ≥ 0],[price | price ≥ 0]) ≼ h([1 | ⊤],[nShares | nShares ≥ 0],[nShares·price | nShares ≥ 0 ∧ price ≥ 0],[nShares^2 | nShares ≥ 0],[price | price ≥ 0]) | | | | 1 ≥ 1 + nShares ==> 0 ≼ h([1 | ⊤],[nShares | nShares ≥ 0],[nShares·price | nShares ≥ 0 ∧ price ≥ 0],[nShares^2 | nShares ≥ 0],[price | price ≥ 0]) | | | | | | | `- [nShares·price | nShares ≥ 0 ∧ price ≥ 0] | | | | | `- 25/2·[1 + price | 1 + price ≥ 0] + 75/2·[-1 + price | -1 + price ≥ 0] | | | +- mixed-iteration-template | | | | | `- [1 + min | 1 + min ≥ 0] + 2·([1 + min | 1 + min ≥ 0]·[-min + price | -min + price ≥ 0]) + [1 + min | 1 + min ≥ 0]^2 + [-min + price | -min + price ≥ 0] + [-min + price | -min + price ≥ 0]^2 | | | +- [Norms] | | [[1 + min | 1 + min ≥ 0],[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0],[1 + 2·(min) + min^2 | 1 + min ≥ 0],[-min + price | -min + price ≥ 0],[-2·(min·price) + min^2 + price^2 | -min + price ≥ 0]] | | | +- [Invariant] | | min ≥ 0 ∧ price ≥ 1 + min ==> 25/2·[1 + price | 1 + price ≥ 0] + 75/2·[-1 + price | -1 + price ≥ 0] + h([1 + min | 1 + min ≥ 0],1/4·[1 + min·price + -min^2 + price | 1 + -min + price ≥ 0 ∧ 1 + min ≥ 0] + 3/4·[-1 + -2·(min) + min·price + -min^2 + price | -1 + -min + price ≥ 0 ∧ 1 + min ≥ 0],[1 + 2·(min) + min^2 | 1 + min ≥ 0],1/4·[1 + -min + price | 1 + -min + price ≥ 0] + 3/4·[-1 + -min + price | -1 + -min + price ≥ 0],1/4·[1 + -2·(min) + -2·(min·price) + min^2 + 2·(price) + price^2 | 1 + -min + price ≥ 0] + 3/4·[1 + 2·(min) + -2·(min·price) + min^2 + -2·(price) + price^2 | -1 + -min + price ≥ 0]) ≼ h([1 + min | 1 + min ≥ 0],[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0],[1 + 2·(min) + min^2 | 1 + min ≥ 0],[-min + price | -min + price ≥ 0],[-2·(min·price) + min^2 + price^2 | -min + price ≥ 0]) | | 0 ≥ 1 + min ∨ 1 + min ≥ 1 + price ==> 0 ≼ h([1 + min | 1 + min ≥ 0],[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0],[1 + 2·(min) + min^2 | 1 + min ≥ 0],[-min + price | -min + price ≥ 0],[-2·(min·price) + min^2 + price^2 | -min + price ≥ 0]) | | | `- 100·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 50·[-2·(min·price) + min^2 + price^2 | -min + price ≥ 0] | `- 100·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 50·[-2·(min·price) + min^2 + price^2 | -min + price ≥ 0]