Found invariant 0 ≤ X₀ for location l1
Found invariant 1 ≤ X₀ for location l2
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
(g₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
new bound:
X₁+101 {O(n)}
MPRF:
• l1: [91+10⋅X₀-X₁]
• l2: [91+10⋅X₀-X₁]
new bound:
X₁⋅X₁+204⋅X₁+10405 {O(n^2)}
MPRF:
• l1: [1+X₀]
• l2: [X₀]
new bound:
X₁⋅X₁+203⋅X₁+10303 {O(n^2)}
MPRF:
• l1: [X₀]
• l2: [X₀]
Overall timebound:2⋅X₁⋅X₁+408⋅X₁+20810 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₁⋅X₁+204⋅X₁+10405 {O(n^2)}
g₄: X₁⋅X₁+203⋅X₁+10303 {O(n^2)}
g₆: X₁+101 {O(n)}
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
(g₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₂,l2), X₀: X₁+102 {O(n)}
(g₂,l2), X₁: 12⋅X₁+1111 {O(n)}
(g₄,l1), X₀: X₁+102 {O(n)}
(g₄,l1), X₁: 12⋅X₁+1111 {O(n)}
(g₆,l1), X₀: X₁+102 {O(n)}
(g₆,l1), X₁: 12⋅X₁+1111 {O(n)}
Overall timebound:2⋅X₁⋅X₁+408⋅X₁+20810 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₁⋅X₁+204⋅X₁+10405 {O(n^2)}
g₄: X₁⋅X₁+203⋅X₁+10303 {O(n^2)}
g₆: X₁+101 {O(n)}
Overall costbound: 2⋅X₁⋅X₁+408⋅X₁+20810 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₁⋅X₁+204⋅X₁+10405 {O(n^2)}
g₄: X₁⋅X₁+203⋅X₁+10303 {O(n^2)}
g₆: X₁+101 {O(n)}
(g₀,l1), X₀: 1 {O(1)}
(g₀,l1), X₁: X₁ {O(n)}
(g₂,l2), X₀: X₁+102 {O(n)}
(g₂,l2), X₁: 12⋅X₁+1111 {O(n)}
(g₄,l1), X₀: X₁+102 {O(n)}
(g₄,l1), X₁: 12⋅X₁+1111 {O(n)}
(g₆,l1), X₀: X₁+102 {O(n)}
(g₆,l1), X₁: 12⋅X₁+1111 {O(n)}