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/21 : 0;1/21 : 1;1/21 : 2;1/21 : 3;1/21 : 4;1/21 : 5;1/21 : 6;1/21 : 7;1/21 : 8;1/21 : 9;1/21 : 10;1/21 : 11;1/21 : 12;1/21 : 13;1/21 : 14;1/21 : 15;1/21 : 16;1/21 : 17;1/21 : 18;1/21 : 19;1/21 : 20}
|        1:While(numShares ≥ 1)
|            numShares :~ {1 : -1 + numShares}
|            Tick(sPrice)
|
+- 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/21 : 0;1/21 : 1;1/21 : 2;1/21 : 3;1/21 : 4;1/21 : 5;1/21 : 6;1/21 : 7;1/21 : 8;1/21 : 9;1/21 : 10;1/21 : 11;1/21 : 12;1/21 : 13;1/21 : 14;1/21 : 15;1/21 : 16;1/21 : 17;1/21 : 18;1/21 : 19;1/21 : 20}
|  |        1:While(numShares ≥ 1)
|  |            numShares :~ {1 : -1 + numShares}
|  |            Tick(sPrice)
|  |
|  +- [f]
|  |    0
|  |
|  +- Expected Cost Body
|  |  |
|  |  +- While.step
|  |  |  |
|  |  |  +- [Problem]
|  |  |  |    1:While(numShares ≥ 1)
|  |  |  |        numShares :~ {1 : -1 + numShares}
|  |  |  |        Tick(sPrice)
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- Expected Cost Body
|  |  |  |  |
|  |  |  |  `- [sPrice | sPrice ≥ 0]
|  |  |  |
|  |  |  +- mixed-lin-template
|  |  |  |  |
|  |  |  |  `- 1 + 2·([numShares | numShares ≥ 0]) + [numShares | numShares ≥ 0]·[sPrice | sPrice ≥ 0] + [numShares | numShares ≥ 0]^2 + [sPrice | sPrice ≥ 0]
|  |  |  |
|  |  |  +- [Norms]
|  |  |  |    [[1 | ⊤],[numShares | numShares ≥ 0],[numShares·sPrice | numShares ≥ 0 ∧  sPrice ≥ 0],[numShares^2 | numShares ≥ 0],[sPrice | sPrice ≥ 0]]
|  |  |  |
|  |  |  +- [Invariant]
|  |  |  |    numShares ≥ 1 ==> [sPrice | sPrice ≥ 0] + h([1 | ⊤],[-1 + numShares | -1 + numShares ≥ 0],[numShares·sPrice + -sPrice | -1 + numShares ≥ 0 ∧  sPrice ≥ 0],[1 + -2·(numShares) + numShares^2 | -1 + numShares ≥ 0],[sPrice | sPrice ≥ 0]) ≼ h([1 | ⊤],[numShares | numShares ≥ 0],[numShares·sPrice | numShares ≥ 0 ∧  sPrice ≥ 0],[numShares^2 | numShares ≥ 0],[sPrice | sPrice ≥ 0])
|  |  |  |    1 ≥ 1 + numShares ==> 0 ≼ h([1 | ⊤],[numShares | numShares ≥ 0],[numShares·sPrice | numShares ≥ 0 ∧  sPrice ≥ 0],[numShares^2 | numShares ≥ 0],[sPrice | sPrice ≥ 0])
|  |  |  |
|  |  |  `- [numShares·sPrice | numShares ≥ 0 ∧  sPrice ≥ 0]
|  |  |
|  |  `- 5/2·[1 + sPrice | 1 + sPrice ≥ 0] + 15/2·[-1 + sPrice | -1 + sPrice ≥ 0]
|  |
|  +- mixed-iteration-template
|  |  |
|  |  `- [1 + minPrice | 1 + minPrice ≥ 0] + 2·([1 + minPrice | 1 + minPrice ≥ 0]·[-minPrice + sPrice | -minPrice + sPrice ≥ 0]) + [1 + minPrice | 1 + minPrice ≥ 0]^2 + [-minPrice + sPrice | -minPrice + sPrice ≥ 0] + [-minPrice + sPrice | -minPrice + sPrice ≥ 0]^2
|  |
|  +- [Norms]
|  |    [[1 + minPrice | 1 + minPrice ≥ 0],[-minPrice + minPrice·sPrice + -minPrice^2 + sPrice | 1 + minPrice ≥ 0 ∧  -minPrice + sPrice ≥ 0],[1 + 2·(minPrice) + minPrice^2 | 1 + minPrice ≥ 0],[-minPrice + sPrice | -minPrice + sPrice ≥ 0],[-2·(minPrice·sPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice ≥ 0]]
|  |
|  +- [Invariant]
|  |    minPrice ≥ 0 ∧  sPrice ≥ 1 + minPrice ==> 5/2·[1 + sPrice | 1 + sPrice ≥ 0] + 15/2·[-1 + sPrice | -1 + sPrice ≥ 0] + h([1 + minPrice | 1 + minPrice ≥ 0],1/4·[1 + minPrice·sPrice + -minPrice^2 + sPrice | 1 + -minPrice + sPrice ≥ 0 ∧  1 + minPrice ≥ 0] + 3/4·[-1 + -2·(minPrice) + minPrice·sPrice + -minPrice^2 + sPrice | -1 + -minPrice + sPrice ≥ 0 ∧  1 + minPrice ≥ 0],[1 + 2·(minPrice) + minPrice^2 | 1 + minPrice ≥ 0],1/4·[1 + -minPrice + sPrice | 1 + -minPrice + sPrice ≥ 0] + 3/4·[-1 + -minPrice + sPrice | -1 + -minPrice + sPrice ≥ 0],1/4·[1 + -2·(minPrice) + -2·(minPrice·sPrice) + minPrice^2 + 2·(sPrice) + sPrice^2 | 1 + -minPrice + sPrice ≥ 0] + 3/4·[1 + 2·(minPrice) + -2·(minPrice·sPrice) + minPrice^2 + -2·(sPrice) + sPrice^2 | -1 + -minPrice + sPrice ≥ 0]) ≼ h([1 + minPrice | 1 + minPrice ≥ 0],[-minPrice + minPrice·sPrice + -minPrice^2 + sPrice | 1 + minPrice ≥ 0 ∧  -minPrice + sPrice ≥ 0],[1 + 2·(minPrice) + minPrice^2 | 1 + minPrice ≥ 0],[-minPrice + sPrice | -minPrice + sPrice ≥ 0],[-2·(minPrice·sPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice ≥ 0])
|  |    0 ≥ 1 + minPrice ∨  1 + minPrice ≥ 1 + sPrice ==> 0 ≼ h([1 + minPrice | 1 + minPrice ≥ 0],[-minPrice + minPrice·sPrice + -minPrice^2 + sPrice | 1 + minPrice ≥ 0 ∧  -minPrice + sPrice ≥ 0],[1 + 2·(minPrice) + minPrice^2 | 1 + minPrice ≥ 0],[-minPrice + sPrice | -minPrice + sPrice ≥ 0],[-2·(minPrice·sPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice ≥ 0])
|  |
|  `- 20·[-minPrice + minPrice·sPrice + -minPrice^2 + sPrice | 1 + minPrice ≥ 0 ∧  -minPrice + sPrice ≥ 0] + 10·[-2·(minPrice·sPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice ≥ 0]
|
`- 20·[-minPrice + minPrice·sPrice + -minPrice^2 + sPrice | 1 + minPrice ≥ 0 ∧  -minPrice + sPrice ≥ 0] + 10·[-2·(minPrice·sPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice ≥ 0]