Expected Cost
|
+- [f]
|    0
|
+- [Program]
|    l1 :~ {1 : 0}
|    l2 :~ {1 : 0}
|    i :~ {1 : 0}
|    0:While(n ≥ i)
|        n :~ {1 : -1 + n}
|        1:If(l1 ≥ 1) Then
|            l1 :~ {1 : -1 + l1}
|          Else
|            Skip
|        2:If(l2 ≥ 1) Then
|            l2 :~ {1 : -1 + l2}
|          Else
|            Skip
|        Choice
|          1/50: Choice
|                  1/5: l1 :~ {1 : 3 + l1}
|                  4/5: Choice
|                         1/2: l2 :~ {1 : 2 + l2}
|                         1/2: l1 :~ {1 : 2 + l1}
|                              l2 :~ {1 : 1 + l2}
|          49/50: Skip
|        3:If(l1 ≥ l2) Then
|            Tick(l1)
|          Else
|            Tick(l2)
|
+- While.step
|  |
|  +- [Problem]
|  |    0:While(n ≥ i)
|  |        n :~ {1 : -1 + n}
|  |        1:If(l1 ≥ 1) Then
|  |            l1 :~ {1 : -1 + l1}
|  |          Else
|  |            Skip
|  |        2:If(l2 ≥ 1) Then
|  |            l2 :~ {1 : -1 + l2}
|  |          Else
|  |            Skip
|  |        Choice
|  |          1/50: Choice
|  |                  1/5: l1 :~ {1 : 3 + l1}
|  |                  4/5: Choice
|  |                         1/2: l2 :~ {1 : 2 + l2}
|  |                         1/2: l1 :~ {1 : 2 + l1}
|  |                              l2 :~ {1 : 1 + l2}
|  |          49/50: Skip
|  |        3:If(l1 ≥ l2) Then
|  |            Tick(l1)
|  |          Else
|  |            Tick(l2)
|  |
|  +- [f]
|  |    0
|  |
|  +- Expected Cost Body
|  |  |
|  |  `- ite(l1 ≥ 1,ite(l2 ≥ 1,ite(2 + l1 ≥ -1 + l2,1/250·[2 + l1 | 2 + l1 ≥ 0],1/250·[-1 + l2 | -1 + l2 ≥ 0]) + ite(-1 + l1 ≥ 1 + l2,1/125·[-1 + l1 | -1 + l1 ≥ 0],1/125·[1 + l2 | 1 + l2 ≥ 0]) + ite(1 + l1 ≥ l2,1/125·[1 + l1 | 1 + l1 ≥ 0],1/125·[l2 | l2 ≥ 0]) + ite(-1 + l1 ≥ -1 + l2,49/50·[-1 + l1 | -1 + l1 ≥ 0],49/50·[-1 + l2 | -1 + l2 ≥ 0]),ite(2 + l1 ≥ l2,1/250·[2 + l1 | 2 + l1 ≥ 0],1/250·[l2 | l2 ≥ 0]) + ite(-1 + l1 ≥ 2 + l2,1/125·[-1 + l1 | -1 + l1 ≥ 0],1/125·[2 + l2 | 2 + l2 ≥ 0]) + ite(1 + l1 ≥ 1 + l2,1/125·[1 + l1 | 1 + l1 ≥ 0],1/125·[1 + l2 | 1 + l2 ≥ 0]) + ite(-1 + l1 ≥ l2,49/50·[-1 + l1 | -1 + l1 ≥ 0],49/50·[l2 | l2 ≥ 0])),ite(l2 ≥ 1,ite(3 + l1 ≥ -1 + l2,1/250·[3 + l1 | 3 + l1 ≥ 0],1/250·[-1 + l2 | -1 + l2 ≥ 0]) + ite(l1 ≥ 1 + l2,1/125·[l1 | l1 ≥ 0],1/125·[1 + l2 | 1 + l2 ≥ 0]) + ite(2 + l1 ≥ l2,1/125·[2 + l1 | 2 + l1 ≥ 0],1/125·[l2 | l2 ≥ 0]) + ite(l1 ≥ -1 + l2,49/50·[l1 | l1 ≥ 0],49/50·[-1 + l2 | -1 + l2 ≥ 0]),ite(3 + l1 ≥ l2,1/250·[3 + l1 | 3 + l1 ≥ 0],1/250·[l2 | l2 ≥ 0]) + ite(l1 ≥ 2 + l2,1/125·[l1 | l1 ≥ 0],1/125·[2 + l2 | 2 + l2 ≥ 0]) + ite(2 + l1 ≥ 1 + l2,1/125·[2 + l1 | 2 + l1 ≥ 0],1/125·[1 + l2 | 1 + l2 ≥ 0]) + ite(l1 ≥ l2,49/50·[l1 | l1 ≥ 0],49/50·[l2 | l2 ≥ 0])))
|  |
|  +- mixed-iteration-template
|  |  |
|  |  `- [1 + -i + n | 1 + -i + n ≥ 0] + 2·([1 + -i + n | 1 + -i + n ≥ 0]·[1 + l1 | 1 + l1 ≥ 0]) + 2·([1 + -i + n | 1 + -i + n ≥ 0]·[1 + l2 | 1 + l2 ≥ 0]) + [1 + -i + n | 1 + -i + n ≥ 0]^2 + [1 + l1 | 1 + l1 ≥ 0] + 2·([1 + l1 | 1 + l1 ≥ 0]·[1 + l2 | 1 + l2 ≥ 0]) + [1 + l1 | 1 + l1 ≥ 0]^2 + [1 + l2 | 1 + l2 ≥ 0] + [1 + l2 | 1 + l2 ≥ 0]^2
|  |
|  +- [Norms]
|  |    [[1 + -i + n | 1 + -i + n ≥ 0],[1 + -i + -i·l1 + l1 + l1·n + n | 1 + -i + n ≥ 0 ∧  1 + l1 ≥ 0],[1 + -i + -i·l2 + l2 + l2·n + n | 1 + -i + n ≥ 0 ∧  1 + l2 ≥ 0],[1 + -2·(i) + -2·(i·n) + i^2 + 2·(n) + n^2 | 1 + -i + n ≥ 0],[1 + l1 | 1 + l1 ≥ 0],[1 + l1 + l1·l2 + l2 | 1 + l1 ≥ 0 ∧  1 + l2 ≥ 0],[1 + 2·(l1) + l1^2 | 1 + l1 ≥ 0],[1 + l2 | 1 + l2 ≥ 0],[1 + 2·(l2) + l2^2 | 1 + l2 ≥ 0]]
|  |
|  +- [Invariant]
|  |    l1 ≥ 0 ∧  l2 ≥ 0 ∧  n ≥ i ==> ite(l1 ≥ 1,ite(l2 ≥ 1,ite(2 + l1 ≥ -1 + l2,1/250·[2 + l1 | 2 + l1 ≥ 0],1/250·[-1 + l2 | -1 + l2 ≥ 0]) + ite(-1 + l1 ≥ 1 + l2,1/125·[-1 + l1 | -1 + l1 ≥ 0],1/125·[1 + l2 | 1 + l2 ≥ 0]) + ite(1 + l1 ≥ l2,1/125·[1 + l1 | 1 + l1 ≥ 0],1/125·[l2 | l2 ≥ 0]) + ite(-1 + l1 ≥ -1 + l2,49/50·[-1 + l1 | -1 + l1 ≥ 0],49/50·[-1 + l2 | -1 + l2 ≥ 0]),ite(2 + l1 ≥ l2,1/250·[2 + l1 | 2 + l1 ≥ 0],1/250·[l2 | l2 ≥ 0]) + ite(-1 + l1 ≥ 2 + l2,1/125·[-1 + l1 | -1 + l1 ≥ 0],1/125·[2 + l2 | 2 + l2 ≥ 0]) + ite(1 + l1 ≥ 1 + l2,1/125·[1 + l1 | 1 + l1 ≥ 0],1/125·[1 + l2 | 1 + l2 ≥ 0]) + ite(-1 + l1 ≥ l2,49/50·[-1 + l1 | -1 + l1 ≥ 0],49/50·[l2 | l2 ≥ 0])),ite(l2 ≥ 1,ite(3 + l1 ≥ -1 + l2,1/250·[3 + l1 | 3 + l1 ≥ 0],1/250·[-1 + l2 | -1 + l2 ≥ 0]) + ite(l1 ≥ 1 + l2,1/125·[l1 | l1 ≥ 0],1/125·[1 + l2 | 1 + l2 ≥ 0]) + ite(2 + l1 ≥ l2,1/125·[2 + l1 | 2 + l1 ≥ 0],1/125·[l2 | l2 ≥ 0]) + ite(l1 ≥ -1 + l2,49/50·[l1 | l1 ≥ 0],49/50·[-1 + l2 | -1 + l2 ≥ 0]),ite(3 + l1 ≥ l2,1/250·[3 + l1 | 3 + l1 ≥ 0],1/250·[l2 | l2 ≥ 0]) + ite(l1 ≥ 2 + l2,1/125·[l1 | l1 ≥ 0],1/125·[2 + l2 | 2 + l2 ≥ 0]) + ite(2 + l1 ≥ 1 + l2,1/125·[2 + l1 | 2 + l1 ≥ 0],1/125·[1 + l2 | 1 + l2 ≥ 0]) + ite(l1 ≥ l2,49/50·[l1 | l1 ≥ 0],49/50·[l2 | l2 ≥ 0]))) + h([-i + n | -i + n ≥ 0],ite(l1 ≥ 1,1/250·[-3·(i) + -i·l1 + l1·n + 3·(n) | 3 + l1 ≥ 0 ∧  -i + n ≥ 0] + 1/125·[-i·l1 + l1·n | -i + n ≥ 0 ∧  l1 ≥ 0] + 1/125·[-2·(i) + -i·l1 + l1·n + 2·(n) | 2 + l1 ≥ 0 ∧  -i + n ≥ 0] + 49/50·[-i·l1 + l1·n | -i + n ≥ 0 ∧  l1 ≥ 0],1/250·[-4·(i) + -i·l1 + l1·n + 4·(n) | 4 + l1 ≥ 0 ∧  -i + n ≥ 0] + 1/125·[-i + -i·l1 + l1·n + n | 1 + l1 ≥ 0 ∧  -i + n ≥ 0] + 1/125·[-3·(i) + -i·l1 + l1·n + 3·(n) | 3 + l1 ≥ 0 ∧  -i + n ≥ 0] + 49/50·[-i + -i·l1 + l1·n + n | 1 + l1 ≥ 0 ∧  -i + n ≥ 0]),ite(l2 ≥ 1,1/250·[-i·l2 + l2·n | -i + n ≥ 0 ∧  l2 ≥ 0] + 1/125·[-2·(i) + -i·l2 + l2·n + 2·(n) | 2 + l2 ≥ 0 ∧  -i + n ≥ 0] + 1/125·[-i + -i·l2 + l2·n + n | 1 + l2 ≥ 0 ∧  -i + n ≥ 0] + 49/50·[-i·l2 + l2·n | -i + n ≥ 0 ∧  l2 ≥ 0],1/250·[-i + -i·l2 + l2·n + n | 1 + l2 ≥ 0 ∧  -i + n ≥ 0] + 1/125·[-3·(i) + -i·l2 + l2·n + 3·(n) | 3 + l2 ≥ 0 ∧  -i + n ≥ 0] + 1/125·[-2·(i) + -i·l2 + l2·n + 2·(n) | 2 + l2 ≥ 0 ∧  -i + n ≥ 0] + 49/50·[-i + -i·l2 + l2·n + n | 1 + l2 ≥ 0 ∧  -i + n ≥ 0]),[-2·(i·n) + i^2 + n^2 | -i + n ≥ 0],ite(l1 ≥ 1,1/250·[3 + l1 | 3 + l1 ≥ 0] + 1/125·[l1 | l1 ≥ 0] + 1/125·[2 + l1 | 2 + l1 ≥ 0] + 49/50·[l1 | l1 ≥ 0],1/250·[4 + l1 | 4 + l1 ≥ 0] + 1/125·[1 + l1 | 1 + l1 ≥ 0] + 1/125·[3 + l1 | 3 + l1 ≥ 0] + 49/50·[1 + l1 | 1 + l1 ≥ 0]),ite(l1 ≥ 1,ite(l2 ≥ 1,1/250·[l1·l2 + 3·(l2) | 3 + l1 ≥ 0 ∧  l2 ≥ 0] + 1/125·[2·(l1) + l1·l2 | 2 + l2 ≥ 0 ∧  l1 ≥ 0] + 1/125·[2 + l1 + l1·l2 + 2·(l2) | 1 + l2 ≥ 0 ∧  2 + l1 ≥ 0] + 49/50·[l1·l2 | l1 ≥ 0 ∧  l2 ≥ 0],1/250·[3 + l1 + l1·l2 + 3·(l2) | 1 + l2 ≥ 0 ∧  3 + l1 ≥ 0] + 1/125·[3·(l1) + l1·l2 | 3 + l2 ≥ 0 ∧  l1 ≥ 0] + 1/125·[4 + 2·(l1) + l1·l2 + 2·(l2) | 2 + l1 ≥ 0 ∧  2 + l2 ≥ 0] + 49/50·[l1 + l1·l2 | 1 + l2 ≥ 0 ∧  l1 ≥ 0]),ite(l2 ≥ 1,1/250·[l1·l2 + 4·(l2) | 4 + l1 ≥ 0 ∧  l2 ≥ 0] + 1/125·[2 + 2·(l1) + l1·l2 + l2 | 1 + l1 ≥ 0 ∧  2 + l2 ≥ 0] + 1/125·[3 + l1 + l1·l2 + 3·(l2) | 1 + l2 ≥ 0 ∧  3 + l1 ≥ 0] + 49/50·[l1·l2 + l2 | 1 + l1 ≥ 0 ∧  l2 ≥ 0],1/250·[4 + l1 + l1·l2 + 4·(l2) | 1 + l2 ≥ 0 ∧  4 + l1 ≥ 0] + 1/125·[3 + 3·(l1) + l1·l2 + l2 | 1 + l1 ≥ 0 ∧  3 + l2 ≥ 0] + 1/125·[6 + 2·(l1) + l1·l2 + 3·(l2) | 2 + l2 ≥ 0 ∧  3 + l1 ≥ 0] + 49/50·[1 + l1 + l1·l2 + l2 | 1 + l1 ≥ 0 ∧  1 + l2 ≥ 0])),ite(l1 ≥ 1,1/250·[9 + 6·(l1) + l1^2 | 3 + l1 ≥ 0] + 1/125·[l1^2 | l1 ≥ 0] + 1/125·[4 + 4·(l1) + l1^2 | 2 + l1 ≥ 0] + 49/50·[l1^2 | l1 ≥ 0],1/250·[16 + 8·(l1) + l1^2 | 4 + l1 ≥ 0] + 1/125·[1 + 2·(l1) + l1^2 | 1 + l1 ≥ 0] + 1/125·[9 + 6·(l1) + l1^2 | 3 + l1 ≥ 0] + 49/50·[1 + 2·(l1) + l1^2 | 1 + l1 ≥ 0]),ite(l2 ≥ 1,1/250·[l2 | l2 ≥ 0] + 1/125·[2 + l2 | 2 + l2 ≥ 0] + 1/125·[1 + l2 | 1 + l2 ≥ 0] + 49/50·[l2 | l2 ≥ 0],1/250·[1 + l2 | 1 + l2 ≥ 0] + 1/125·[3 + l2 | 3 + l2 ≥ 0] + 1/125·[2 + l2 | 2 + l2 ≥ 0] + 49/50·[1 + l2 | 1 + l2 ≥ 0]),ite(l2 ≥ 1,1/250·[l2^2 | l2 ≥ 0] + 1/125·[4 + 4·(l2) + l2^2 | 2 + l2 ≥ 0] + 1/125·[1 + 2·(l2) + l2^2 | 1 + l2 ≥ 0] + 49/50·[l2^2 | l2 ≥ 0],1/250·[1 + 2·(l2) + l2^2 | 1 + l2 ≥ 0] + 1/125·[9 + 6·(l2) + l2^2 | 3 + l2 ≥ 0] + 1/125·[4 + 4·(l2) + l2^2 | 2 + l2 ≥ 0] + 49/50·[1 + 2·(l2) + l2^2 | 1 + l2 ≥ 0])) ≼ h([1 + -i + n | 1 + -i + n ≥ 0],[1 + -i + -i·l1 + l1 + l1·n + n | 1 + -i + n ≥ 0 ∧  1 + l1 ≥ 0],[1 + -i + -i·l2 + l2 + l2·n + n | 1 + -i + n ≥ 0 ∧  1 + l2 ≥ 0],[1 + -2·(i) + -2·(i·n) + i^2 + 2·(n) + n^2 | 1 + -i + n ≥ 0],[1 + l1 | 1 + l1 ≥ 0],[1 + l1 + l1·l2 + l2 | 1 + l1 ≥ 0 ∧  1 + l2 ≥ 0],[1 + 2·(l1) + l1^2 | 1 + l1 ≥ 0],[1 + l2 | 1 + l2 ≥ 0],[1 + 2·(l2) + l2^2 | 1 + l2 ≥ 0])
|  |    i ≥ 1 + n ∧  l1 ≥ 0 ∧  l2 ≥ 0 ==> 0 ≼ h([1 + -i + n | 1 + -i + n ≥ 0],[1 + -i + -i·l1 + l1 + l1·n + n | 1 + -i + n ≥ 0 ∧  1 + l1 ≥ 0],[1 + -i + -i·l2 + l2 + l2·n + n | 1 + -i + n ≥ 0 ∧  1 + l2 ≥ 0],[1 + -2·(i) + -2·(i·n) + i^2 + 2·(n) + n^2 | 1 + -i + n ≥ 0],[1 + l1 | 1 + l1 ≥ 0],[1 + l1 + l1·l2 + l2 | 1 + l1 ≥ 0 ∧  1 + l2 ≥ 0],[1 + 2·(l1) + l1^2 | 1 + l1 ≥ 0],[1 + l2 | 1 + l2 ≥ 0],[1 + 2·(l2) + l2^2 | 1 + l2 ≥ 0])
|  |
|  `- [l1 ≥ 0 ∧  l2 ≥ 0] · (1132981/7411500·[1 + -i + n | 1 + -i + n ≥ 0] + 125/243·[1 + 2·(l1) + l1^2 | 1 + l1 ≥ 0] + 125/244·[1 + 2·(l2) + l2^2 | 1 + l2 ≥ 0])
|
`- 1132981/7411500·[1 + n | 1 + n ≥ 0] + 125/243 + 125/244