Preprocessing

Eliminate variables [X₃; X₄] that do not contribute to the problem

Found invariant X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 2 ∧ X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 1+X₂ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ 1 ∧ X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀ for location h

Found invariant X₅ ≤ 1 ∧ X₅ ≤ 1+X₂ ∧ X₂+X₅ ≤ 2 ∧ X₅ ≤ 1+X₁ ∧ X₁+X₅ ≤ 2 ∧ X₅ ≤ X₀ ∧ 0 ≤ X₅ ∧ 0 ≤ X₂+X₅ ∧ X₂ ≤ 1+X₅ ∧ 0 ≤ X₁+X₅ ∧ X₁ ≤ 1+X₅ ∧ 1 ≤ X₀+X₅ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 2 ∧ X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 1+X₂ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ 1 ∧ X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀ for location j

Found invariant X₅ ≤ 1 ∧ X₅ ≤ 1+X₂ ∧ X₂+X₅ ≤ 2 ∧ X₅ ≤ 1+X₁ ∧ X₁+X₅ ≤ 2 ∧ X₅ ≤ X₀ ∧ 0 ≤ X₅ ∧ 0 ≤ X₂+X₅ ∧ X₂ ≤ 1+X₅ ∧ 0 ≤ X₁+X₅ ∧ X₁ ≤ 1+X₅ ∧ 1 ≤ X₀+X₅ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₁ ∧ X₁+X₂ ≤ 2 ∧ X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ X₁ ≤ 1+X₂ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ 1 ∧ X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀ for location k

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁, X₂, X₃, X₄, X₅
Temp_Vars:
Locations: f, g, h, j, k
Transitions:
g₀:f(X₀,X₁,X₂,X₃,X₄,X₅) -{0}> t₁:g(X₀,X₁,X₂,X₃,X₄,X₅) :|:
g₂:g(X₀,X₁,X₂,X₃,X₄,X₅) → [3/25]:t₃:h(X₀,1,1,X₃,X₄,X₅) :+: [9/50]:t₄:h(X₀,1,0,X₃,X₄,X₅) :+: [7/25]:t₅:h(X₀,0,1,X₃,X₄,X₅) :+: [21/50]:t₆:h(X₀,0,0,X₃,X₄,X₅) :|: 1 ≤ X₀
g₇:h(X₀,X₁,X₂,X₃,X₄,X₅) → [7/10]:t₈:j(X₀,X₁,X₂,X₃,X₄,1) :+: [3/10]:t₉:j(X₀,X₁,X₂,X₃,X₄,0) :|: X₁ ≤ 0 ∧ X₂ ≤ 0 ∧ X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂
g₁₀:h(X₀,X₁,X₂,X₃,X₄,X₅) → [19/20]:t₁₁:j(X₀,X₁,X₂,X₃,X₄,1) :+: [1/20]:t₁₂:j(X₀,X₁,X₂,X₃,X₄,0) :|: 1 ≤ X₂ ∧ X₁ ≤ 0 ∧ X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂
g₁₃:h(X₀,X₁,X₂,X₃,X₄,X₅) → [1/10]:t₁₄:j(X₀,X₁,X₂,X₃,X₄,1) :+: [9/10]:t₁₅:j(X₀,X₁,X₂,X₃,X₄,0) :|: 1 ≤ X₁ ∧ X₂ ≤ 0 ∧ X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂
g₁₆:h(X₀,X₁,X₂,X₃,X₄,X₅) → [1/2]:t₁₇:j(X₀,X₁,X₂,X₃,X₄,1) :+: [1/2]:t₁₈:j(X₀,X₁,X₂,X₃,X₄,0) :|: 1 ≤ X₁ ∧ 1 ≤ X₂ ∧ X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂
g₁₉:j(X₀,X₁,X₂,X₃,X₄,X₅) → [1/20]:t₂₀:k(X₀,X₁,X₂,1,X₄,X₅) :+: [19/20]:t₂₁:k(X₀,X₁,X₂,0,X₄,X₅) :|: X₁ ≤ 0 ∧ X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅
g₂₂:j(X₀,X₁,X₂,X₃,X₄,X₅) → [4/5]:t₂₃:k(X₀,X₁,X₂,1,X₄,X₅) :+: [1/5]:t₂₄:k(X₀,X₁,X₂,0,X₄,X₅) :|: 1 ≤ X₁ ∧ X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅
g₂₅:k(X₀,X₁,X₂,X₃,X₄,X₅) → [1/10]:t₂₆:g(X₀-1,X₁,X₂,X₃,1,X₅) :+: [9/10]:t₂₇:g(X₀-1,X₁,X₂,X₃,0,X₅) :|: X₅ ≤ 0 ∧ X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅
g₂₈:k(X₀,X₁,X₂,X₃,X₄,X₅) → [3/5]:t₂₉:g(X₀-1,X₁,X₂,X₃,1,X₅) :+: [2/5]:t₃₀:g(X₀-1,X₁,X₂,X₃,0,X₅) :|: 1 ≤ X₅ ∧ X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅

Run classical analysis on SCC: [f]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₇: inf {Infinity}
g₁₀: inf {Infinity}
g₁₃: inf {Infinity}
g₁₆: inf {Infinity}
g₁₉: inf {Infinity}
g₂₂: inf {Infinity}
g₂₅: inf {Infinity}
g₂₈: inf {Infinity}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₇: inf {Infinity}
g₁₀: inf {Infinity}
g₁₃: inf {Infinity}
g₁₆: inf {Infinity}
g₁₉: inf {Infinity}
g₂₂: inf {Infinity}
g₂₅: inf {Infinity}
g₂₈: inf {Infinity}

Sizebounds

(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: X₃ {O(n)}
(g₀,g), X₄: X₄ {O(n)}
(g₀,g), X₅: X₅ {O(n)}

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g; h; j; k]

MPRF for transition t₃: g(X₀,X₁,X₂,X₅) → h(X₀,Temp_Int₅₇₃,Temp_Int₅₇₄,X₅) :|: 1 ≤ X₀ ∧ Temp_Int₅₇₃ ≤ 1 ∧ 1 ≤ Temp_Int₅₇₃ ∧ 1 ≤ X₀ ∧ Temp_Int₅₇₄ ≤ 1 ∧ 1 ≤ Temp_Int₅₇₄ ∧ 1 ≤ X₀ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀-1]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₄: g(X₀,X₁,X₂,X₅) → h(X₀,Temp_Int₅₇₅,Temp_Int₅₇₆,X₅) :|: 1 ≤ X₀ ∧ Temp_Int₅₇₅ ≤ 1 ∧ 1 ≤ Temp_Int₅₇₅ ∧ 1 ≤ X₀ ∧ Temp_Int₅₇₆ ≤ 0 ∧ 0 ≤ Temp_Int₅₇₆ ∧ 1 ≤ X₀ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀-1]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₅: g(X₀,X₁,X₂,X₅) → h(X₀,Temp_Int₅₇₇,Temp_Int₅₇₈,X₅) :|: 1 ≤ X₀ ∧ Temp_Int₅₇₇ ≤ 0 ∧ 0 ≤ Temp_Int₅₇₇ ∧ 1 ≤ X₀ ∧ Temp_Int₅₇₈ ≤ 1 ∧ 1 ≤ Temp_Int₅₇₈ ∧ 1 ≤ X₀ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀-1]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₆: g(X₀,X₁,X₂,X₅) → h(X₀,Temp_Int₅₇₉,Temp_Int₅₈₀,X₅) :|: 1 ≤ X₀ ∧ Temp_Int₅₇₉ ≤ 0 ∧ 0 ≤ Temp_Int₅₇₉ ∧ 1 ≤ X₀ ∧ Temp_Int₅₈₀ ≤ 0 ∧ 0 ≤ Temp_Int₅₈₀ ∧ 1 ≤ X₀ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀-1]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₈: h(X₀,X₁,X₂,X₃,X₄,X₅) → j(X₀,X₁,X₂,X₃,X₄,Temp_Int₅₈₁) :|: X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₁ ∧ X₂ ≤ 0 ∧ 0 ≤ X₂ ∧ Temp_Int₅₈₁ ≤ 1 ∧ 1 ≤ Temp_Int₅₈₁ ∧ X₁ ≤ 0 ∧ X₂ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₉: h(X₀,X₁,X₂,X₃,X₄,X₅) → j(X₀,X₁,X₂,X₃,X₄,Temp_Int₅₈₂) :|: X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₁ ∧ X₂ ≤ 0 ∧ 0 ≤ X₂ ∧ Temp_Int₅₈₂ ≤ 0 ∧ 0 ≤ Temp_Int₅₈₂ ∧ X₁ ≤ 0 ∧ X₂ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₁₁: h(X₀,X₁,X₂,X₃,X₄,X₅) → j(X₀,X₁,X₂,X₃,X₄,Temp_Int₅₈₃) :|: X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₁ ∧ X₂ ≤ 1 ∧ 1 ≤ X₂ ∧ Temp_Int₅₈₃ ≤ 1 ∧ 1 ≤ Temp_Int₅₈₃ ∧ 1 ≤ X₂ ∧ X₁ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₁₂: h(X₀,X₁,X₂,X₃,X₄,X₅) → j(X₀,X₁,X₂,X₃,X₄,Temp_Int₅₈₄) :|: X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₁ ∧ X₂ ≤ 1 ∧ 1 ≤ X₂ ∧ Temp_Int₅₈₄ ≤ 0 ∧ 0 ≤ Temp_Int₅₈₄ ∧ 1 ≤ X₂ ∧ X₁ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₁₄: h(X₀,X₁,X₂,X₃,X₄,X₅) → j(X₀,X₁,X₂,X₃,X₄,Temp_Int₅₈₅) :|: X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 1 ∧ 1 ≤ X₁ ∧ X₂ ≤ 0 ∧ 0 ≤ X₂ ∧ Temp_Int₅₈₅ ≤ 1 ∧ 1 ≤ Temp_Int₅₈₅ ∧ 1 ≤ X₁ ∧ X₂ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₁₅: h(X₀,X₁,X₂,X₃,X₄,X₅) → j(X₀,X₁,X₂,X₃,X₄,Temp_Int₅₈₆) :|: X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 1 ∧ 1 ≤ X₁ ∧ X₂ ≤ 0 ∧ 0 ≤ X₂ ∧ Temp_Int₅₈₆ ≤ 0 ∧ 0 ≤ Temp_Int₅₈₆ ∧ 1 ≤ X₁ ∧ X₂ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₁₇: h(X₀,X₁,X₂,X₃,X₄,X₅) → j(X₀,X₁,X₂,X₃,X₄,Temp_Int₅₈₇) :|: X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 1 ∧ 1 ≤ X₁ ∧ X₂ ≤ 1 ∧ 1 ≤ X₂ ∧ Temp_Int₅₈₇ ≤ 1 ∧ 1 ≤ Temp_Int₅₈₇ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₁₈: h(X₀,X₁,X₂,X₃,X₄,X₅) → j(X₀,X₁,X₂,X₃,X₄,Temp_Int₅₈₈) :|: X₁+X₂ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ ∧ 1 ≤ X₀ ∧ X₁ ≤ 1 ∧ 1 ≤ X₁ ∧ X₂ ≤ 1 ∧ 1 ≤ X₂ ∧ Temp_Int₅₈₈ ≤ 0 ∧ 0 ≤ Temp_Int₅₈₈ ∧ 1 ≤ X₁ ∧ 1 ≤ X₂ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀-1]
• k: [X₀-1]

MPRF for transition t₂₀: j(X₀,X₁,X₂,X₃,X₄,X₅) → k(X₀,X₁,X₂,Temp_Int₅₈₉,X₄,X₅) :|: X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₅ ∧ X₅ ≤ 1 ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₁ ∧ Temp_Int₅₈₉ ≤ 1 ∧ 1 ≤ Temp_Int₅₈₉ ∧ X₁ ≤ 0 of depth 1:

new bound:

X₀+1 {O(n)}

MPRF:

• g: [1+X₀]
• h: [1+X₀]
• j: [1+X₀]
• k: [X₀]

MPRF for transition t₂₁: j(X₀,X₁,X₂,X₃,X₄,X₅) → k(X₀,X₁,X₂,Temp_Int₅₉₀,X₄,X₅) :|: X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₅ ∧ X₅ ≤ 1 ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ 0 ∧ 0 ≤ X₁ ∧ Temp_Int₅₉₀ ≤ 0 ∧ 0 ≤ Temp_Int₅₉₀ ∧ X₁ ≤ 0 of depth 1:

new bound:

X₀+1 {O(n)}

MPRF:

• g: [1+X₀]
• h: [1+X₀]
• j: [1+X₀]
• k: [X₀]

MPRF for transition t₂₃: j(X₀,X₁,X₂,X₃,X₄,X₅) → k(X₀,X₁,X₂,Temp_Int₅₉₁,X₄,X₅) :|: X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₅ ∧ X₅ ≤ 1 ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ 1 ∧ 1 ≤ X₁ ∧ Temp_Int₅₉₁ ≤ 1 ∧ 1 ≤ Temp_Int₅₉₁ ∧ 1 ≤ X₁ of depth 1:

new bound:

2⋅X₀+1 {O(n)}

MPRF:

• g: [2⋅X₀-1]
• h: [2⋅X₀-1]
• j: [2⋅X₀+X₁-2]
• k: [2⋅X₀+X₁-3]

MPRF for transition t₂₄: j(X₀,X₁,X₂,X₃,X₄,X₅) → k(X₀,X₁,X₂,Temp_Int₅₉₂,X₄,X₅) :|: X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₅ ∧ X₅ ≤ 1 ∧ X₂ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ 1 ∧ 1 ≤ X₁ ∧ Temp_Int₅₉₂ ≤ 0 ∧ 0 ≤ Temp_Int₅₉₂ ∧ 1 ≤ X₁ of depth 1:

new bound:

X₀+1 {O(n)}

MPRF:

• g: [1+X₀]
• h: [1+X₀]
• j: [X₀+X₁]
• k: [X₀]

MPRF for transition t₂₆: k(X₀,X₁,X₂,X₃,X₄,X₅) → g(X₀-1,X₁,X₂,X₃,Temp_Int₅₉₃,X₅) :|: X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅ ∧ 0 ≤ X₁ ∧ 0 ≤ X₂ ∧ X₂ ≤ 1 ∧ X₁ ≤ 1 ∧ 1 ≤ X₀ ∧ X₅ ≤ 0 ∧ 0 ≤ X₅ ∧ Temp_Int₅₉₃ ≤ 1 ∧ 1 ≤ Temp_Int₅₉₃ ∧ X₅ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀]
• k: [X₀]

MPRF for transition t₂₇: k(X₀,X₁,X₂,X₃,X₄,X₅) → g(X₀-1,X₁,X₂,X₃,Temp_Int₅₉₄,X₅) :|: X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅ ∧ 0 ≤ X₁ ∧ 0 ≤ X₂ ∧ X₂ ≤ 1 ∧ X₁ ≤ 1 ∧ 1 ≤ X₀ ∧ X₅ ≤ 0 ∧ 0 ≤ X₅ ∧ Temp_Int₅₉₄ ≤ 0 ∧ 0 ≤ Temp_Int₅₉₄ ∧ X₅ ≤ 0 of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀]
• k: [X₀]

MPRF for transition t₂₉: k(X₀,X₁,X₂,X₃,X₄,X₅) → g(X₀-1,X₁,X₂,X₃,Temp_Int₅₉₅,X₅) :|: X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅ ∧ 0 ≤ X₁ ∧ 0 ≤ X₂ ∧ X₂ ≤ 1 ∧ X₁ ≤ 1 ∧ 1 ≤ X₀ ∧ X₅ ≤ 1 ∧ 1 ≤ X₅ ∧ Temp_Int₅₉₅ ≤ 1 ∧ 1 ≤ Temp_Int₅₉₅ ∧ 1 ≤ X₅ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀]
• k: [X₀]

MPRF for transition t₃₀: k(X₀,X₁,X₂,X₃,X₄,X₅) → g(X₀-1,X₁,X₂,X₃,Temp_Int₅₉₆,X₅) :|: X₁+X₂ ≤ 2 ∧ X₁+X₅ ≤ 2 ∧ X₂+X₅ ≤ 2 ∧ X₂ ≤ 1+X₁ ∧ X₅ ≤ 1+X₁ ∧ X₁ ≤ 1 ∧ X₁ ≤ 1+X₂ ∧ X₁ ≤ 1+X₅ ∧ X₅ ≤ 1+X₂ ∧ X₂ ≤ 1 ∧ X₂ ≤ 1+X₅ ∧ X₅ ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀+X₂ ∧ 1 ≤ X₀+X₅ ∧ X₁ ≤ X₀ ∧ X₂ ≤ X₀ ∧ X₅ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₅ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₅ ∧ 0 ≤ X₅ ∧ 0 ≤ X₁ ∧ 0 ≤ X₂ ∧ X₂ ≤ 1 ∧ X₁ ≤ 1 ∧ 1 ≤ X₀ ∧ X₅ ≤ 1 ∧ 1 ≤ X₅ ∧ Temp_Int₅₉₆ ≤ 0 ∧ 0 ≤ Temp_Int₅₉₆ ∧ 1 ≤ X₅ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• g: [X₀]
• h: [X₀]
• j: [X₀]
• k: [X₀]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:21⋅X₀+5 {O(n)}
g₀: 1 {O(1)}
g₂: 4⋅X₀ {O(n)}
g₇: 2⋅X₀ {O(n)}
g₁₀: 2⋅X₀ {O(n)}
g₁₃: 2⋅X₀ {O(n)}
g₁₆: 2⋅X₀ {O(n)}
g₁₉: 2⋅X₀+2 {O(n)}
g₂₂: 3⋅X₀+2 {O(n)}
g₂₅: 2⋅X₀ {O(n)}
g₂₈: 2⋅X₀ {O(n)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₇: inf {Infinity}
g₁₀: inf {Infinity}
g₁₃: inf {Infinity}
g₁₆: inf {Infinity}
g₁₉: inf {Infinity}
g₂₂: inf {Infinity}
g₂₅: inf {Infinity}
g₂₈: inf {Infinity}

Sizebounds

(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: X₃ {O(n)}
(g₀,g), X₄: X₄ {O(n)}
(g₀,g), X₅: X₅ {O(n)}
(g₂,h), X₀: 4⋅X₀ {O(n)}
(g₂,h), X₁: 2 {O(1)}
(g₂,h), X₂: 2 {O(1)}
(g₂,h), X₃: 4⋅X₃+32 {O(n)}
(g₂,h), X₄: 4⋅X₄+8 {O(n)}
(g₂,h), X₅: 4⋅X₅+8 {O(n)}
(g₇,j), X₀: 2⋅X₀ {O(n)}
(g₇,j), X₁: 0 {O(1)}
(g₇,j), X₂: 0 {O(1)}
(g₇,j), X₃: 2⋅X₃+16 {O(n)}
(g₇,j), X₄: 2⋅X₄+4 {O(n)}
(g₇,j), X₅: 1 {O(1)}
(g₁₀,j), X₀: 2⋅X₀ {O(n)}
(g₁₀,j), X₁: 0 {O(1)}
(g₁₀,j), X₂: 2 {O(1)}
(g₁₀,j), X₃: 2⋅X₃+16 {O(n)}
(g₁₀,j), X₄: 2⋅X₄+4 {O(n)}
(g₁₀,j), X₅: 1 {O(1)}
(g₁₃,j), X₀: 2⋅X₀ {O(n)}
(g₁₃,j), X₁: 2 {O(1)}
(g₁₃,j), X₂: 0 {O(1)}
(g₁₃,j), X₃: 2⋅X₃+16 {O(n)}
(g₁₃,j), X₄: 2⋅X₄+4 {O(n)}
(g₁₃,j), X₅: 1 {O(1)}
(g₁₆,j), X₀: 2⋅X₀ {O(n)}
(g₁₆,j), X₁: 2 {O(1)}
(g₁₆,j), X₂: 2 {O(1)}
(g₁₆,j), X₃: 2⋅X₃+16 {O(n)}
(g₁₆,j), X₄: 2⋅X₄+4 {O(n)}
(g₁₆,j), X₅: 1 {O(1)}
(g₁₉,k), X₀: 2⋅X₀ {O(n)}
(g₁₉,k), X₁: 0 {O(1)}
(g₁₉,k), X₂: 2 {O(1)}
(g₁₉,k), X₃: 1 {O(1)}
(g₁₉,k), X₄: 8⋅X₄+16 {O(n)}
(g₁₉,k), X₅: 2 {O(1)}
(g₂₂,k), X₀: 2⋅X₀ {O(n)}
(g₂₂,k), X₁: 2 {O(1)}
(g₂₂,k), X₂: 2 {O(1)}
(g₂₂,k), X₃: 1 {O(1)}
(g₂₂,k), X₄: 8⋅X₄+16 {O(n)}
(g₂₂,k), X₅: 2 {O(1)}
(g₂₅,g), X₀: 2⋅X₀ {O(n)}
(g₂₅,g), X₁: 2 {O(1)}
(g₂₅,g), X₂: 2 {O(1)}
(g₂₅,g), X₃: 4 {O(1)}
(g₂₅,g), X₄: 1 {O(1)}
(g₂₅,g), X₅: 0 {O(1)}
(g₂₈,g), X₀: 2⋅X₀ {O(n)}
(g₂₈,g), X₁: 2 {O(1)}
(g₂₈,g), X₂: 2 {O(1)}
(g₂₈,g), X₃: 4 {O(1)}
(g₂₈,g), X₄: 1 {O(1)}
(g₂₈,g), X₅: 2 {O(1)}

Run probabilistic analysis on SCC: [g; h; j; k]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:21⋅X₀+5 {O(n)}
g₀: 1 {O(1)}
g₂: 4⋅X₀ {O(n)}
g₇: 2⋅X₀ {O(n)}
g₁₀: 2⋅X₀ {O(n)}
g₁₃: 2⋅X₀ {O(n)}
g₁₆: 2⋅X₀ {O(n)}
g₁₉: 2⋅X₀+2 {O(n)}
g₂₂: 3⋅X₀+2 {O(n)}
g₂₅: 2⋅X₀ {O(n)}
g₂₈: 2⋅X₀ {O(n)}

Costbounds

Overall costbound: 50⋅X₀+8 {O(n)}
g₀: 0 {O(1)}
g₂: 16⋅X₀ {O(n)}
g₇: 4⋅X₀ {O(n)}
g₁₀: 4⋅X₀ {O(n)}
g₁₃: 4⋅X₀ {O(n)}
g₁₆: 4⋅X₀ {O(n)}
g₁₉: 4⋅X₀+4 {O(n)}
g₂₂: 6⋅X₀+4 {O(n)}
g₂₅: 4⋅X₀ {O(n)}
g₂₈: 4⋅X₀ {O(n)}

Sizebounds

(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: X₃ {O(n)}
(g₀,g), X₄: X₄ {O(n)}
(g₀,g), X₅: X₅ {O(n)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: 2 {O(1)}
(g₂,h), X₂: 2 {O(1)}
(g₂,h), X₃: 4⋅X₃+32 {O(n)}
(g₂,h), X₄: 4⋅X₄+8 {O(n)}
(g₂,h), X₅: 4⋅X₅+8 {O(n)}
(g₇,j), X₀: X₀ {O(n)}
(g₇,j), X₁: 0 {O(1)}
(g₇,j), X₂: 0 {O(1)}
(g₇,j), X₃: 2⋅X₃+16 {O(n)}
(g₇,j), X₄: 2⋅X₄+4 {O(n)}
(g₇,j), X₅: 1 {O(1)}
(g₁₀,j), X₀: X₀ {O(n)}
(g₁₀,j), X₁: 0 {O(1)}
(g₁₀,j), X₂: 2 {O(1)}
(g₁₀,j), X₃: 2⋅X₃+16 {O(n)}
(g₁₀,j), X₄: 2⋅X₄+4 {O(n)}
(g₁₀,j), X₅: 1 {O(1)}
(g₁₃,j), X₀: X₀ {O(n)}
(g₁₃,j), X₁: 2 {O(1)}
(g₁₃,j), X₂: 0 {O(1)}
(g₁₃,j), X₃: 2⋅X₃+16 {O(n)}
(g₁₃,j), X₄: 2⋅X₄+4 {O(n)}
(g₁₃,j), X₅: 1 {O(1)}
(g₁₆,j), X₀: X₀ {O(n)}
(g₁₆,j), X₁: 2 {O(1)}
(g₁₆,j), X₂: 2 {O(1)}
(g₁₆,j), X₃: 2⋅X₃+16 {O(n)}
(g₁₆,j), X₄: 2⋅X₄+4 {O(n)}
(g₁₆,j), X₅: 1 {O(1)}
(g₁₉,k), X₀: X₀ {O(n)}
(g₁₉,k), X₁: 0 {O(1)}
(g₁₉,k), X₂: 2 {O(1)}
(g₁₉,k), X₃: 1 {O(1)}
(g₁₉,k), X₄: 8⋅X₄+16 {O(n)}
(g₁₉,k), X₅: 2 {O(1)}
(g₂₂,k), X₀: X₀ {O(n)}
(g₂₂,k), X₁: 2 {O(1)}
(g₂₂,k), X₂: 2 {O(1)}
(g₂₂,k), X₃: 1 {O(1)}
(g₂₂,k), X₄: 8⋅X₄+16 {O(n)}
(g₂₂,k), X₅: 2 {O(1)}
(g₂₅,g), X₀: X₀ {O(n)}
(g₂₅,g), X₁: 2 {O(1)}
(g₂₅,g), X₂: 2 {O(1)}
(g₂₅,g), X₃: 4 {O(1)}
(g₂₅,g), X₄: 1 {O(1)}
(g₂₅,g), X₅: 0 {O(1)}
(g₂₈,g), X₀: X₀ {O(n)}
(g₂₈,g), X₁: 2 {O(1)}
(g₂₈,g), X₂: 2 {O(1)}
(g₂₈,g), X₃: 4 {O(1)}
(g₂₈,g), X₄: 1 {O(1)}
(g₂₈,g), X₅: 2 {O(1)}