Preprocessing

Cut unsatisfiable transition [t₈∈g₇: lbl52→1:stop; t₁₈∈g₁₇: lbl72→1:lbl72]

Found invariant X₅ ≤ X₀ ∧ X₃ ≤ X₅ ∧ X₀ ≤ X₅ ∧ X₃ ≤ 0 ∧ X₃ ≤ X₀ for location stop

Found invariant X₅ ≤ X₁ ∧ X₅ ≤ X₀ ∧ 1 ≤ X₅ ∧ 1 ≤ X₃+X₅ ∧ 1+X₃ ≤ X₅ ∧ 2 ≤ X₁+X₅ ∧ X₁ ≤ X₅ ∧ 2 ≤ X₀+X₅ ∧ X₀ ≤ X₅ ∧ 1+X₃ ≤ X₁ ∧ 1+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 1 ≤ X₁+X₃ ∧ 1 ≤ X₀+X₃ ∧ X₁ ≤ X₀ ∧ 1 ≤ X₁ ∧ 2 ≤ X₀+X₁ ∧ X₀ ≤ X₁ ∧ 1 ≤ X₀ for location lbl72

Found invariant X₅ ≤ X₀ ∧ 1 ≤ X₅ ∧ 2 ≤ X₃+X₅ ∧ X₃ ≤ X₅ ∧ 1 ≤ X₁+X₅ ∧ 2 ≤ X₀+X₅ ∧ X₀ ≤ X₅ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₃ ∧ 1 ≤ X₁+X₃ ∧ 2 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀ for location lbl52

Found invariant X₅ ≤ X₀ ∧ X₀ ≤ X₅ ∧ X₄ ≤ X₃ ∧ X₃ ≤ X₄ ∧ X₂ ≤ X₁ ∧ X₁ ≤ X₂ for location start

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: start0
Program_Vars: X₀, X₁, X₂, X₃, X₄, X₅
Temp_Vars:
Locations: lbl52, lbl72, start, start0, stop
Transitions:
g₁:start(X₀,X₁,X₂,X₃,X₄,X₅) → t₂:stop(X₀,X₁,X₂,X₅,X₄,X₅) :|: X₅ ≤ X₀ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₅ ∧ X₂ ≤ X₁ ∧ X₁ ≤ X₂ ∧ X₄ ≤ X₃ ∧ X₃ ≤ X₄
g₃:start(X₀,X₁,X₂,X₃,X₄,X₅) → t₄:lbl52(X₀,X₁-1,X₂,X₅,X₄,X₅) :|: 1 ≤ X₀ ∧ 1 ≤ X₂ ∧ X₅ ≤ X₀ ∧ X₀ ≤ X₅ ∧ X₂ ≤ X₁ ∧ X₁ ≤ X₂ ∧ X₄ ≤ X₃ ∧ X₃ ≤ X₄
g₅:start(X₀,X₁,X₂,X₃,X₄,X₅) → t₆:lbl72(X₀,X₅,X₂,X₅-1,X₄,X₅) :|: 1 ≤ X₀ ∧ X₅ ≤ X₀ ∧ X₀ ≤ X₅ ∧ X₂ ≤ X₁ ∧ X₁ ≤ X₂ ∧ X₂ ≤ 0 ∧ X₄ ≤ X₃ ∧ X₃ ≤ X₄
g₉:lbl52(X₀,X₁,X₂,X₃,X₄,X₅) → t₁₀:lbl52(X₀,X₁+UNIFORM(-1, 0),X₂,X₃,X₄,X₅) :|: 1 ≤ X₁ ∧ 1 ≤ X₃ ∧ X₃ ≤ X₀ ∧ X₅ ≤ X₀ ∧ X₀ ≤ X₅ ∧ 0 ≤ X₁ ∧ 0 ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁+X₃ ∧ 1 ≤ X₁+X₅ ∧ 1 ≤ X₅ ∧ 2 ≤ X₀+X₃ ∧ 2 ≤ X₀+X₅ ∧ 2 ≤ X₃+X₅ ∧ X₃ ≤ X₅
g₁₁:lbl52(X₀,X₁,X₂,X₃,X₄,X₅) → t₁₂:lbl72(X₀,X₅,X₂,X₃-1,X₄,X₅) :|: 1 ≤ X₃ ∧ X₃ ≤ X₀ ∧ X₅ ≤ X₀ ∧ X₀ ≤ X₅ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁+X₃ ∧ 1 ≤ X₁+X₅ ∧ 1 ≤ X₅ ∧ 2 ≤ X₀+X₃ ∧ 2 ≤ X₀+X₅ ∧ 2 ≤ X₃+X₅ ∧ X₃ ≤ X₅
g₁₃:lbl72(X₀,X₁,X₂,X₃,X₄,X₅) → t₁₄:stop(X₀,X₁,X₂,X₃,X₄,X₅) :|: 1 ≤ X₀ ∧ X₁ ≤ X₀ ∧ X₅ ≤ X₀ ∧ X₀ ≤ X₁ ∧ X₀ ≤ X₅ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0 ∧ 1 ≤ X₀+X₃ ∧ 1+X₃ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 1 ≤ X₃+X₅ ∧ 1+X₃ ≤ X₅ ∧ 1 ≤ X₅ ∧ 2 ≤ X₀+X₁ ∧ 2 ≤ X₀+X₅ ∧ 2 ≤ X₁+X₅ ∧ X₅ ≤ X₁ ∧ X₁ ≤ X₅
g₁₅:lbl72(X₀,X₁,X₂,X₃,X₄,X₅) → t₁₆:lbl52(X₀,X₁-1,X₂,X₃,X₄,X₅) :|: 1 ≤ X₀ ∧ 1+X₃ ≤ X₀ ∧ 1 ≤ X₃ ∧ X₁ ≤ X₀ ∧ X₅ ≤ X₀ ∧ X₀ ≤ X₁ ∧ X₀ ≤ X₅ ∧ 0 ≤ X₃ ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 1 ≤ X₃+X₅ ∧ 1+X₃ ≤ X₅ ∧ 1 ≤ X₅ ∧ 2 ≤ X₀+X₁ ∧ 2 ≤ X₀+X₅ ∧ 2 ≤ X₁+X₅ ∧ X₅ ≤ X₁ ∧ X₁ ≤ X₅
g₁₉:start0(X₀,X₁,X₂,X₃,X₄,X₅) → t₂₀:start(X₀,X₂,X₂,X₄,X₄,X₀) :|:

Run classical analysis on SCC: [start0]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: inf {Infinity}
g₁₁: inf {Infinity}
g₁₃: 1 {O(1)}
g₁₅: inf {Infinity}
g₁₉: 1 {O(1)}

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}

Sizebounds

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

Run probabilistic analysis on SCC: [start0]

Run classical analysis on SCC: [start]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: inf {Infinity}
g₁₁: inf {Infinity}
g₁₃: 1 {O(1)}
g₁₅: inf {Infinity}
g₁₉: 1 {O(1)}

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}

Sizebounds

(g₁,stop), X₀: X₀ {O(n)}
(g₁,stop), X₁: X₂ {O(n)}
(g₁,stop), X₂: X₂ {O(n)}
(g₁,stop), X₃: X₀ {O(n)}
(g₁,stop), X₄: X₄ {O(n)}
(g₁,stop), X₅: X₀ {O(n)}
(g₃,lbl52), X₀: X₀ {O(n)}
(g₃,lbl52), X₁: X₂ {O(n)}
(g₃,lbl52), X₂: X₂ {O(n)}
(g₃,lbl52), X₃: X₀ {O(n)}
(g₃,lbl52), X₄: X₄ {O(n)}
(g₃,lbl52), X₅: X₀ {O(n)}
(g₅,lbl72), X₀: X₀ {O(n)}
(g₅,lbl72), X₁: X₀ {O(n)}
(g₅,lbl72), X₂: X₂ {O(n)}
(g₅,lbl72), X₃: X₀ {O(n)}
(g₅,lbl72), X₄: X₄ {O(n)}
(g₅,lbl72), X₅: X₀ {O(n)}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}

Run probabilistic analysis on SCC: [start]

Run classical analysis on SCC: [lbl52; lbl72]

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

new bound:

2⋅X₀ {O(n)}

MPRF:

• lbl52: [X₃]
• lbl72: [X₃]

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

new bound:

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

MPRF:

• lbl52: [X₃-1]
• lbl72: [X₃]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: inf {Infinity}
g₁₁: 2⋅X₀ {O(n)}
g₁₃: 1 {O(1)}
g₁₅: 2⋅X₀+1 {O(n)}
g₁₉: 1 {O(1)}

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}

Sizebounds

(g₁,stop), X₀: X₀ {O(n)}
(g₁,stop), X₁: X₂ {O(n)}
(g₁,stop), X₂: X₂ {O(n)}
(g₁,stop), X₃: X₀ {O(n)}
(g₁,stop), X₄: X₄ {O(n)}
(g₁,stop), X₅: X₀ {O(n)}
(g₃,lbl52), X₀: X₀ {O(n)}
(g₃,lbl52), X₁: X₂ {O(n)}
(g₃,lbl52), X₂: X₂ {O(n)}
(g₃,lbl52), X₃: X₀ {O(n)}
(g₃,lbl52), X₄: X₄ {O(n)}
(g₃,lbl52), X₅: X₀ {O(n)}
(g₅,lbl72), X₀: X₀ {O(n)}
(g₅,lbl72), X₁: X₀ {O(n)}
(g₅,lbl72), X₂: X₂ {O(n)}
(g₅,lbl72), X₃: X₀ {O(n)}
(g₅,lbl72), X₄: X₄ {O(n)}
(g₅,lbl72), X₅: X₀ {O(n)}
(g₉,lbl52), X₀: 2⋅X₀ {O(n)}
(g₉,lbl52), X₁: 4⋅X₀+X₂ {O(n)}
(g₉,lbl52), X₂: 2⋅X₂ {O(n)}
(g₉,lbl52), X₃: 2⋅X₀ {O(n)}
(g₉,lbl52), X₄: 2⋅X₄ {O(n)}
(g₉,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₀: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₁: 3⋅X₀ {O(n)}
(g₁₁,lbl72), X₂: 2⋅X₂ {O(n)}
(g₁₁,lbl72), X₃: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₄: 2⋅X₄ {O(n)}
(g₁₁,lbl72), X₅: 2⋅X₀ {O(n)}
(g₁₃,stop), X₀: 3⋅X₀ {O(n)}
(g₁₃,stop), X₁: 4⋅X₀ {O(n)}
(g₁₃,stop), X₂: 3⋅X₂ {O(n)}
(g₁₃,stop), X₃: 0 {O(1)}
(g₁₃,stop), X₄: 3⋅X₄ {O(n)}
(g₁₃,stop), X₅: 3⋅X₀ {O(n)}
(g₁₅,lbl52), X₀: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₁: 4⋅X₀ {O(n)}
(g₁₅,lbl52), X₂: 2⋅X₂ {O(n)}
(g₁₅,lbl52), X₃: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₄: 2⋅X₄ {O(n)}
(g₁₅,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}

Run probabilistic analysis on SCC: [lbl52; lbl72]

Plrf for transition g₉:lbl52(X₀,X₁,X₂,X₃,X₄,X₅) → t₁₀:lbl52(X₀,X₁+UNIFORM(-1, 0),X₂,X₃,X₄,X₅) :|: 1 ≤ X₁ ∧ 1 ≤ X₃ ∧ X₃ ≤ X₀ ∧ X₅ ≤ X₀ ∧ X₀ ≤ X₅ ∧ 0 ≤ X₁ ∧ 0 ≤ 1 ∧ 1 ≤ X₀ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁+X₃ ∧ 1 ≤ X₁+X₅ ∧ 1 ≤ X₅ ∧ 2 ≤ X₀+X₃ ∧ 2 ≤ X₀+X₅ ∧ 2 ≤ X₃+X₅ ∧ X₃ ≤ X₅:

new bound:

24⋅X₀⋅X₀+14⋅X₀+2⋅X₂ {O(n^2)}

PLRF:

• lbl52: 2⋅X₁+2⋅X₅
• lbl72: 2⋅X₀

Use expected size bounds for entry point (g₃:start→[t₄:1:lbl52],lbl52)
Use expected size bounds for entry point (g₃:start→[t₄:1:lbl52],lbl52)
Use classical time bound for entry point (g₃:start→[t₄:1:lbl52],lbl52)
Use expected size bounds for entry point (g₁₅:lbl72→[t₁₆:1:lbl52],lbl52)
Use expected size bounds for entry point (g₁₅:lbl72→[t₁₆:1:lbl52],lbl52)
Use classical time bound for entry point (g₁₅:lbl72→[t₁₆:1:lbl52],lbl52)

Run classical analysis on SCC: [stop]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:24⋅X₀⋅X₀+18⋅X₀+2⋅X₂+6 {O(n^2)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: 24⋅X₀⋅X₀+14⋅X₀+2⋅X₂ {O(n^2)}
g₁₁: 2⋅X₀ {O(n)}
g₁₃: 1 {O(1)}
g₁₅: 2⋅X₀+1 {O(n)}
g₁₉: 1 {O(1)}

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}

Sizebounds

(g₁,stop), X₀: X₀ {O(n)}
(g₁,stop), X₁: X₂ {O(n)}
(g₁,stop), X₂: X₂ {O(n)}
(g₁,stop), X₃: X₀ {O(n)}
(g₁,stop), X₄: X₄ {O(n)}
(g₁,stop), X₅: X₀ {O(n)}
(g₃,lbl52), X₀: X₀ {O(n)}
(g₃,lbl52), X₁: X₂ {O(n)}
(g₃,lbl52), X₂: X₂ {O(n)}
(g₃,lbl52), X₃: X₀ {O(n)}
(g₃,lbl52), X₄: X₄ {O(n)}
(g₃,lbl52), X₅: X₀ {O(n)}
(g₅,lbl72), X₀: X₀ {O(n)}
(g₅,lbl72), X₁: X₀ {O(n)}
(g₅,lbl72), X₂: X₂ {O(n)}
(g₅,lbl72), X₃: X₀ {O(n)}
(g₅,lbl72), X₄: X₄ {O(n)}
(g₅,lbl72), X₅: X₀ {O(n)}
(g₉,lbl52), X₀: 2⋅X₀ {O(n)}
(g₉,lbl52), X₁: 4⋅X₀+X₂ {O(n)}
(g₉,lbl52), X₂: 2⋅X₂ {O(n)}
(g₉,lbl52), X₃: 2⋅X₀ {O(n)}
(g₉,lbl52), X₄: 2⋅X₄ {O(n)}
(g₉,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₀: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₁: 3⋅X₀ {O(n)}
(g₁₁,lbl72), X₂: 2⋅X₂ {O(n)}
(g₁₁,lbl72), X₃: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₄: 2⋅X₄ {O(n)}
(g₁₁,lbl72), X₅: 2⋅X₀ {O(n)}
(g₁₃,stop), X₀: 3⋅X₀ {O(n)}
(g₁₃,stop), X₁: 4⋅X₀ {O(n)}
(g₁₃,stop), X₂: 3⋅X₂ {O(n)}
(g₁₃,stop), X₃: 0 {O(1)}
(g₁₃,stop), X₄: 3⋅X₄ {O(n)}
(g₁₃,stop), X₅: 3⋅X₀ {O(n)}
(g₁₅,lbl52), X₀: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₁: 4⋅X₀ {O(n)}
(g₁₅,lbl52), X₂: 2⋅X₂ {O(n)}
(g₁₅,lbl52), X₃: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₄: 2⋅X₄ {O(n)}
(g₁₅,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}

Run probabilistic analysis on SCC: [stop]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:24⋅X₀⋅X₀+18⋅X₀+2⋅X₂+6 {O(n^2)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: 24⋅X₀⋅X₀+14⋅X₀+2⋅X₂ {O(n^2)}
g₁₁: 2⋅X₀ {O(n)}
g₁₃: 1 {O(1)}
g₁₅: 2⋅X₀+1 {O(n)}
g₁₉: 1 {O(1)}

Costbounds

Overall costbound: 24⋅X₀⋅X₀+18⋅X₀+2⋅X₂+6 {O(n^2)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: 24⋅X₀⋅X₀+14⋅X₀+2⋅X₂ {O(n^2)}
g₁₁: 2⋅X₀ {O(n)}
g₁₃: 1 {O(1)}
g₁₅: 2⋅X₀+1 {O(n)}
g₁₉: 1 {O(1)}

Sizebounds

(g₁,stop), X₀: X₀ {O(n)}
(g₁,stop), X₁: X₂ {O(n)}
(g₁,stop), X₂: X₂ {O(n)}
(g₁,stop), X₃: X₀ {O(n)}
(g₁,stop), X₄: X₄ {O(n)}
(g₁,stop), X₅: X₀ {O(n)}
(g₃,lbl52), X₀: X₀ {O(n)}
(g₃,lbl52), X₁: X₂ {O(n)}
(g₃,lbl52), X₂: X₂ {O(n)}
(g₃,lbl52), X₃: X₀ {O(n)}
(g₃,lbl52), X₄: X₄ {O(n)}
(g₃,lbl52), X₅: X₀ {O(n)}
(g₅,lbl72), X₀: X₀ {O(n)}
(g₅,lbl72), X₁: X₀ {O(n)}
(g₅,lbl72), X₂: X₂ {O(n)}
(g₅,lbl72), X₃: X₀ {O(n)}
(g₅,lbl72), X₄: X₄ {O(n)}
(g₅,lbl72), X₅: X₀ {O(n)}
(g₉,lbl52), X₀: 2⋅X₀ {O(n)}
(g₉,lbl52), X₁: 4⋅X₀+X₂ {O(n)}
(g₉,lbl52), X₂: 2⋅X₂ {O(n)}
(g₉,lbl52), X₃: 2⋅X₀ {O(n)}
(g₉,lbl52), X₄: 2⋅X₄ {O(n)}
(g₉,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₀: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₁: 3⋅X₀ {O(n)}
(g₁₁,lbl72), X₂: 2⋅X₂ {O(n)}
(g₁₁,lbl72), X₃: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₄: 2⋅X₄ {O(n)}
(g₁₁,lbl72), X₅: 2⋅X₀ {O(n)}
(g₁₃,stop), X₀: 3⋅X₀ {O(n)}
(g₁₃,stop), X₁: 4⋅X₀ {O(n)}
(g₁₃,stop), X₂: 3⋅X₂ {O(n)}
(g₁₃,stop), X₃: 0 {O(1)}
(g₁₃,stop), X₄: 3⋅X₄ {O(n)}
(g₁₃,stop), X₅: 3⋅X₀ {O(n)}
(g₁₅,lbl52), X₀: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₁: 4⋅X₀ {O(n)}
(g₁₅,lbl52), X₂: 2⋅X₂ {O(n)}
(g₁₅,lbl52), X₃: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₄: 2⋅X₄ {O(n)}
(g₁₅,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}