ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | 0:While(n 1) | i :~ {3/10 : 1;7/10 : 0} | z :~ {1 : 1 + z} | d :~ {2/5 : 1;3/5 : 0} | Tick(1) | 1:If(1 1 + d 1 1 + i) Then | g :~ {7/10 : 1;3/10 : 0} | Tick(1) | Else | 2:If(1 1 + i d 1) Then | g :~ {19/20 : 1;1/20 : 0} | Tick(1) | Else | 3:If(1 1 + d i 1) Then | g :~ {1/10 : 1;9/10 : 0} | Tick(1) | Else | g :~ {1/2 : 1;1/2 : 0} | Tick(1) | 4:If(1 1 + i) Then | s :~ {1/20 : 1;19/20 : 0} | Tick(1) | Else | s :~ {4/5 : 1;1/5 : 0} | Tick(1) | 5:If(1 1 + g) Then | l :~ {1/10 : 1;9/10 : 0} | Tick(1) | Else | l :~ {3/5 : 1;2/5 : 0} | Tick(1) | n :~ {1 : -1 + n} | +- While.step | | | +- [Problem] | | 0:While(n 1) | | i :~ {3/10 : 1;7/10 : 0} | | z :~ {1 : 1 + z} | | d :~ {2/5 : 1;3/5 : 0} | | Tick(1) | | 1:If(1 1 + d 1 1 + i) Then | | g :~ {7/10 : 1;3/10 : 0} | | Tick(1) | | Else | | 2:If(1 1 + i d 1) Then | | g :~ {19/20 : 1;1/20 : 0} | | Tick(1) | | Else | | 3:If(1 1 + d i 1) Then | | g :~ {1/10 : 1;9/10 : 0} | | Tick(1) | | Else | | g :~ {1/2 : 1;1/2 : 0} | | Tick(1) | | 4:If(1 1 + i) Then | | s :~ {1/20 : 1;19/20 : 0} | | Tick(1) | | Else | | s :~ {4/5 : 1;1/5 : 0} | | Tick(1) | | 5:If(1 1 + g) Then | | l :~ {1/10 : 1;9/10 : 0} | | Tick(1) | | Else | | l :~ {3/5 : 1;2/5 : 0} | | Tick(1) | | n :~ {1 : -1 + n} | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- 4 | | | +- linear-template | | | | | `- 1 + [n | n 0] | | | +- [Norms] | | [[1 | ],[n | n 0]] | | | +- [Invariant] | | n 1 ==> 4 + h([1 | ],[-1 + n | -1 + n 0]) h([1 | ],[n | n 0]) | | 1 1 + n ==> 0 h([1 | ],[n | n 0]) | | | `- 4[n | n 0] | `- 4[n | n 0] [Success] 4[n | n 0] Degree: 1