Expected Cost | +- [f] | 0 | +- [Program] | 0:While(b ≥ 1 + x ∧ x ≥ 1 + a) | Tick(1) | Choice | 1/2: x :~ {1 : -1 + x} | 1/2: x :~ {1 : 1 + x} | +- While.step | | | +- [Problem] | | 0:While(b ≥ 1 + x ∧ x ≥ 1 + a) | | Tick(1) | | Choice | | 1/2: x :~ {1 : -1 + x} | | 1/2: x :~ {1 : 1 + x} | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- [1 | ⊤] | | | +- mixed-iteration-template | | | | | `- [-a + x | -a + x ≥ 0] + 2·([-a + x | -a + x ≥ 0]·[b + -x | b + -x ≥ 0]) + [-a + x | -a + x ≥ 0]^2 + [b + -x | b + -x ≥ 0] + [b + -x | b + -x ≥ 0]^2 | | | +- [Norms] | | [[-a + x | -a + x ≥ 0],[-a·b + a·x + b·x + -x^2 | -a + x ≥ 0 ∧ b + -x ≥ 0],[-2·(a·x) + a^2 + x^2 | -a + x ≥ 0],[b + -x | b + -x ≥ 0],[-2·(b·x) + b^2 + x^2 | b + -x ≥ 0]] | | | +- [Invariant] | | b ≥ 1 + x ∧ x ≥ 1 + a ==> [1 | ⊤] + h(1/2·[-1 + -a + x | -1 + -a + x ≥ 0] + 1/2·[1 + -a + x | 1 + -a + x ≥ 0],1/2·[-1 + -a + -a·b + a·x + -b + b·x + 2·(x) + -x^2 | -1 + -a + x ≥ 0 ∧ 1 + b + -x ≥ 0] + 1/2·[-1 + a + -a·b + a·x + b + b·x + -2·(x) + -x^2 | -1 + b + -x ≥ 0 ∧ 1 + -a + x ≥ 0],1/2·[1 + 2·(a) + -2·(a·x) + a^2 + -2·(x) + x^2 | -1 + -a + x ≥ 0] + 1/2·[1 + -2·(a) + -2·(a·x) + a^2 + 2·(x) + x^2 | 1 + -a + x ≥ 0],1/2·[1 + b + -x | 1 + b + -x ≥ 0] + 1/2·[-1 + b + -x | -1 + b + -x ≥ 0],1/2·[1 + 2·(b) + -2·(b·x) + b^2 + -2·(x) + x^2 | 1 + b + -x ≥ 0] + 1/2·[1 + -2·(b) + -2·(b·x) + b^2 + 2·(x) + x^2 | -1 + b + -x ≥ 0]) ≼ h([-a + x | -a + x ≥ 0],[-a·b + a·x + b·x + -x^2 | -a + x ≥ 0 ∧ b + -x ≥ 0],[-2·(a·x) + a^2 + x^2 | -a + x ≥ 0],[b + -x | b + -x ≥ 0],[-2·(b·x) + b^2 + x^2 | b + -x ≥ 0]) | | 1 + a ≥ 1 + x ∨ 1 + x ≥ 1 + b ==> 0 ≼ h([-a + x | -a + x ≥ 0],[-a·b + a·x + b·x + -x^2 | -a + x ≥ 0 ∧ b + -x ≥ 0],[-2·(a·x) + a^2 + x^2 | -a + x ≥ 0],[b + -x | b + -x ≥ 0],[-2·(b·x) + b^2 + x^2 | b + -x ≥ 0]) | | | `- [-a·b + a·x + b·x + -x^2 | -a + x ≥ 0 ∧ b + -x ≥ 0] | `- [-a·b + a·x + b·x + -x^2 | -a + x ≥ 0 ∧ b + -x ≥ 0]