Expected Cost | +- [f] | 0 | +- [Program] | tick_z :~ {1 : 0} | 0:While(minPrice ≥ 0 ∧ sPrice ≥ 1 + minPrice) | Choice | 1/4: sPrice :~ {1 : 1 + sPrice} | 3/4: sPrice :~ {1 : -1 + sPrice} | numShares :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | 1:While(numShares ≥ 1) | numShares :~ {1 : -1 + numShares} | tick_z :~ {1 : sPrice + tick_z} | 2:While(0 ≥ 1 + numShares) | numShares :~ {1 : 1 + numShares} | tick_z :~ {1 : -sPrice + tick_z} | Tick(tick_z) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 0:While(minPrice ≥ 0 ∧ sPrice ≥ 1 + minPrice) | | Choice | | 1/4: sPrice :~ {1 : 1 + sPrice} | | 3/4: sPrice :~ {1 : -1 + sPrice} | | numShares :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | | 1:While(numShares ≥ 1) | | numShares :~ {1 : -1 + numShares} | | tick_z :~ {1 : sPrice + tick_z} | | 2:While(0 ≥ 1 + numShares) | | numShares :~ {1 : 1 + numShares} | | tick_z :~ {1 : -sPrice + tick_z} | | | `- 0 | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | Tick(tick_z) | | | `- [tick_z | tick_z ≥ 0] | +- Expected Cost | | | +- [f] | | [tick_z | tick_z ≥ 0] | | | +- [Program] | | 0:While(minPrice ≥ 0 ∧ sPrice ≥ 1 + minPrice) | | Choice | | 1/4: sPrice :~ {1 : 1 + sPrice} | | 3/4: sPrice :~ {1 : -1 + sPrice} | | numShares :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | | 1:While(numShares ≥ 1) | | numShares :~ {1 : -1 + numShares} | | tick_z :~ {1 : sPrice + tick_z} | | 2:While(0 ≥ 1 + numShares) | | numShares :~ {1 : 1 + numShares} | | tick_z :~ {1 : -sPrice + tick_z} | | | +- While.step | | | | | +- [Problem] | | | 0:While(minPrice ≥ 0 ∧ sPrice ≥ 1 + minPrice) | | | Choice | | | 1/4: sPrice :~ {1 : 1 + sPrice} | | | 3/4: sPrice :~ {1 : -1 + sPrice} | | | numShares :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | | | 1:While(numShares ≥ 1) | | | numShares :~ {1 : -1 + numShares} | | | tick_z :~ {1 : sPrice + tick_z} | | | 2:While(0 ≥ 1 + numShares) | | | numShares :~ {1 : 1 + numShares} | | | tick_z :~ {1 : -sPrice + tick_z} | | | | | +- [f] | | | [tick_z | tick_z ≥ 0] | | | | | +- While.step | | | | | | | +- [Problem] | | | | 2:While(0 ≥ 1 + numShares) | | | | numShares :~ {1 : 1 + numShares} | | | | tick_z :~ {1 : -sPrice + tick_z} | | | | | | | +- [f] | | | | [tick_z | tick_z ≥ 0] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [-numShares | -numShares ≥ 0] + [-numShares | -numShares ≥ 0]·[-sPrice | -sPrice ≥ 0] + [tick_z | tick_z ≥ 0] | | | | | | | +- [Norms] | | | | [[1 | ⊤],[-numShares | -numShares ≥ 0],[numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0],[tick_z | tick_z ≥ 0]] | | | | | | | +- [Invariant] | | | | 0 ≥ 1 + numShares ==> 0 + h([1 | ⊤],-1·[1 + numShares | -1 + -numShares ≥ 0],[numShares·sPrice + sPrice | -1 + -numShares ≥ 0 ∧ -sPrice ≥ 0],[-sPrice + tick_z | -sPrice + tick_z ≥ 0]) ≼ h([1 | ⊤],[-numShares | -numShares ≥ 0],[numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0],[tick_z | tick_z ≥ 0]) | | | | 1 + numShares ≥ 1 ==> [tick_z | tick_z ≥ 0] ≼ h([1 | ⊤],[-numShares | -numShares ≥ 0],[numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0],[tick_z | tick_z ≥ 0]) | | | | | | | `- [numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0] + [tick_z | tick_z ≥ 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | [numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0] | | | | | | | +- [Program] | | | | 1:While(numShares ≥ 1) | | | | numShares :~ {1 : -1 + numShares} | | | | tick_z :~ {1 : sPrice + tick_z} | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 1:While(numShares ≥ 1) | | | | | numShares :~ {1 : -1 + numShares} | | | | | tick_z :~ {1 : sPrice + tick_z} | | | | | | | | | +- [f] | | | | | [numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0] + [numShares | numShares ≥ 0] + [numShares | numShares ≥ 0]·[-sPrice | -sPrice ≥ 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ⊤],[numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0],[numShares | numShares ≥ 0],[-numShares·sPrice | numShares ≥ 0 ∧ -sPrice ≥ 0]] | | | | | | | | | +- [Invariant] | | | | | numShares ≥ 1 ==> 0 + h([1 | ⊤],[numShares·sPrice + -sPrice | 1 + -numShares ≥ 0 ∧ -sPrice ≥ 0],[-1 + numShares | -1 + numShares ≥ 0],-1·[numShares·sPrice + -sPrice | -1 + numShares ≥ 0 ∧ -sPrice ≥ 0]) ≼ h([1 | ⊤],[numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0],[numShares | numShares ≥ 0],[-numShares·sPrice | numShares ≥ 0 ∧ -sPrice ≥ 0]) | | | | | 1 ≥ 1 + numShares ==> [numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0] ≼ h([1 | ⊤],[numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0],[numShares | numShares ≥ 0],[-numShares·sPrice | numShares ≥ 0 ∧ -sPrice ≥ 0]) | | | | | | | | | `- [numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0] | | | | | | | `- [numShares·sPrice | -numShares ≥ 0 ∧ -sPrice ≥ 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | [tick_z | tick_z ≥ 0] | | | | | | | +- [Program] | | | | 1:While(numShares ≥ 1) | | | | numShares :~ {1 : -1 + numShares} | | | | tick_z :~ {1 : sPrice + tick_z} | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 1:While(numShares ≥ 1) | | | | | numShares :~ {1 : -1 + numShares} | | | | | tick_z :~ {1 : sPrice + tick_z} | | | | | | | | | +- [f] | | | | | [tick_z | tick_z ≥ 0] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [numShares | numShares ≥ 0] + [numShares | numShares ≥ 0]·[sPrice | sPrice ≥ 0] + [tick_z | tick_z ≥ 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ⊤],[numShares | numShares ≥ 0],[numShares·sPrice | numShares ≥ 0 ∧ sPrice ≥ 0],[tick_z | tick_z ≥ 0]] | | | | | | | | | +- [Invariant] | | | | | numShares ≥ 1 ==> 0 + h([1 | ⊤],[-1 + numShares | -1 + numShares ≥ 0],[numShares·sPrice + -sPrice | -1 + numShares ≥ 0 ∧ sPrice ≥ 0],[sPrice + tick_z | sPrice + tick_z ≥ 0]) ≼ h([1 | ⊤],[numShares | numShares ≥ 0],[numShares·sPrice | numShares ≥ 0 ∧ sPrice ≥ 0],[tick_z | tick_z ≥ 0]) | | | | | 1 ≥ 1 + numShares ==> [tick_z | tick_z ≥ 0] ≼ h([1 | ⊤],[numShares | numShares ≥ 0],[numShares·sPrice | numShares ≥ 0 ∧ sPrice ≥ 0],[tick_z | tick_z ≥ 0]) | | | | | | | | | `- [numShares·sPrice | numShares ≥ 0 ∧ sPrice ≥ 0] + [tick_z | tick_z ≥ 0] | | | | | | | `- [numShares·sPrice | numShares ≥ 0 ∧ sPrice ≥ 0] + [tick_z | tick_z ≥ 0] | | | | | +- linear-template | | | | | | | `- 1 + [1 + minPrice | 1 + minPrice ≥ 0] + [1 + minPrice | 1 + minPrice ≥ 0]·[1 + sPrice | 1 + sPrice ≥ 0] + [1 + sPrice | 1 + sPrice ≥ 0]·[-minPrice + sPrice | -minPrice + sPrice ≥ 0] + [-minPrice + sPrice | -minPrice + sPrice ≥ 0] + [tick_z | tick_z ≥ 0] | | | | | +- [Norms] | | | [[1 | ⊤],[1 + minPrice | 1 + minPrice ≥ 0],[1 + minPrice + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 1 + sPrice ≥ 0],[-minPrice + -minPrice·sPrice + sPrice + sPrice^2 | 1 + sPrice ≥ 0 ∧ -minPrice + sPrice ≥ 0],[-minPrice + sPrice | -minPrice + sPrice ≥ 0],[tick_z | tick_z ≥ 0]] | | | | | +- [Invariant] | | | minPrice ≥ 0 ∧ sPrice ≥ 1 + minPrice ==> 0 + h([1 | ⊤],[1 + minPrice | 1 + minPrice ≥ 0],1/4·[2 + 2·(minPrice) + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 2 + sPrice ≥ 0] + 3/4·[minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ sPrice ≥ 0],1/4·[2 + -2·(minPrice) + -minPrice·sPrice + 3·(sPrice) + sPrice^2 | 1 + -minPrice + sPrice ≥ 0 ∧ 2 + sPrice ≥ 0] + 3/4·[-minPrice·sPrice + -sPrice + sPrice^2 | -1 + -minPrice + sPrice ≥ 0 ∧ sPrice ≥ 0],1/4·[1 + -minPrice + sPrice | 1 + -minPrice + sPrice ≥ 0] + 3/4·[-1 + -minPrice + sPrice | -1 + -minPrice + sPrice ≥ 0],-1/12·[1 + sPrice | -1 + -sPrice ≥ 0] + 1/24·[tick_z | tick_z ≥ 0] + -1/24·[1 + sPrice | -1 + -sPrice ≥ 0] + 1/24·[tick_z | tick_z ≥ 0] + 1/24·[tick_z | tick_z ≥ 0] + 1/24·[1 + sPrice | 1 + sPrice ≥ 0] + 1/24·[tick_z | tick_z ≥ 0] + 1/12·[1 + sPrice | 1 + sPrice ≥ 0] + 1/24·[tick_z | tick_z ≥ 0] + 1/8·[1 + sPrice | 1 + sPrice ≥ 0] + 1/24·[tick_z | tick_z ≥ 0] + -1/4·[-1 + sPrice | 1 + -sPrice ≥ 0] + 1/8·[tick_z | tick_z ≥ 0] + -1/8·[-1 + sPrice | 1 + -sPrice ≥ 0] + 1/8·[tick_z | tick_z ≥ 0] + 1/8·[tick_z | tick_z ≥ 0] + 1/8·[-1 + sPrice | -1 + sPrice ≥ 0] + 1/8·[tick_z | tick_z ≥ 0] + 1/4·[-1 + sPrice | -1 + sPrice ≥ 0] + 1/8·[tick_z | tick_z ≥ 0] + 3/8·[-1 + sPrice | -1 + sPrice ≥ 0] + 1/8·[tick_z | tick_z ≥ 0]) ≼ h([1 | ⊤],[1 + minPrice | 1 + minPrice ≥ 0],[1 + minPrice + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 1 + sPrice ≥ 0],[-minPrice + -minPrice·sPrice + sPrice + sPrice^2 | 1 + sPrice ≥ 0 ∧ -minPrice + sPrice ≥ 0],[-minPrice + sPrice | -minPrice + sPrice ≥ 0],[tick_z | tick_z ≥ 0]) | | | 0 ≥ 1 + minPrice ∨ 1 + minPrice ≥ 1 + sPrice ==> [tick_z | tick_z ≥ 0] ≼ h([1 | ⊤],[1 + minPrice | 1 + minPrice ≥ 0],[1 + minPrice + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 1 + sPrice ≥ 0],[-minPrice + -minPrice·sPrice + sPrice + sPrice^2 | 1 + sPrice ≥ 0 ∧ -minPrice + sPrice ≥ 0],[-minPrice + sPrice | -minPrice + sPrice ≥ 0],[tick_z | tick_z ≥ 0]) | | | | | `- [1 + minPrice + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 1 + sPrice ≥ 0] + [-minPrice + -minPrice·sPrice + sPrice + sPrice^2 | 1 + sPrice ≥ 0 ∧ -minPrice + sPrice ≥ 0] + [tick_z | tick_z ≥ 0] | | | `- [1 + minPrice + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 1 + sPrice ≥ 0] + [-minPrice + -minPrice·sPrice + sPrice + sPrice^2 | 1 + sPrice ≥ 0 ∧ -minPrice + sPrice ≥ 0] + [tick_z | tick_z ≥ 0] | `- [1 + minPrice + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 1 + sPrice ≥ 0] + [-minPrice + -minPrice·sPrice + sPrice + sPrice^2 | 1 + sPrice ≥ 0 ∧ -minPrice + sPrice ≥ 0]