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/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: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/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: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] | | | | | `- 5/4·[1 + price | 1 + price ≥ 0] + 15/4·[-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 ==> 5/4·[1 + price | 1 + price ≥ 0] + 15/4·[-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]) | | | `- 10·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 5·[-2·(min·price) + min^2 + price^2 | -min + price ≥ 0] | `- 10·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 5·[-2·(min·price) + min^2 + price^2 | -min + price ≥ 0]