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]