Preprocessing

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

Found invariant 1+X₂ ≤ X₃ for location h

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁, X₂, X₃, X₄
Temp_Vars:
Locations: f, g, h
Transitions:
g₀:f(X₀,X₁,X₂,X₃,X₄) -{0}> t₁:g(X₀,X₁,X₂,X₃,X₄) :|:
g₂:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₃:h(X₀,X₁,X₂,X₃,X₄) :|: 1+X₂ ≤ X₃
g₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₅:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₆:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₇:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₈:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1+X₂ ≤ X₃
g₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₀:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₁₁:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₂:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₃:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 1+X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
g₁₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₅:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₁₆:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₁₇:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₈:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
g₁₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₂₀:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₁:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₂:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₃:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 1 ≤ X₁ ∧ 1+X₂ ≤ X₃
g₂₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₂₅:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₆:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₇:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₈:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
g₂₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₃₀:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₃₁:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₂:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₃₃:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃
g₃₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₃₅:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₆:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₃₇:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₈:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1+X₂ ≤ X₃
g₃₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₄₀:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₁:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₄₂:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₃:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1+X₂ ≤ X₃
g₄₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₄₅:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₆:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₇:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₈:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ 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}
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}
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)}

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g; h]

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}
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}
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₂,h), X₃: X₃ {O(n)}
(g₂,h), X₄: X₄ {O(n)}
(g₄,g), X₃: 4⋅X₃ {O(n)}
(g₄,g), X₄: 4⋅X₄ {O(n)}
(g₉,g), X₃: 4⋅X₃ {O(n)}
(g₉,g), X₄: 4⋅X₄ {O(n)}
(g₁₄,g), X₁: 2 {O(1)}
(g₁₄,g), X₃: 4⋅X₃ {O(n)}
(g₁₄,g), X₄: 4⋅X₄ {O(n)}
(g₁₉,g), X₃: 4⋅X₃ {O(n)}
(g₁₉,g), X₄: 4⋅X₄ {O(n)}
(g₂₄,g), X₃: 4⋅X₃ {O(n)}
(g₂₄,g), X₄: 4⋅X₄ {O(n)}
(g₂₉,g), X₁: 2 {O(1)}
(g₂₉,g), X₃: 4⋅X₃ {O(n)}
(g₂₉,g), X₄: 4⋅X₄ {O(n)}
(g₃₄,g), X₀: 2 {O(1)}
(g₃₄,g), X₃: 4⋅X₃ {O(n)}
(g₃₄,g), X₄: 4⋅X₄ {O(n)}
(g₃₉,g), X₀: 2 {O(1)}
(g₃₉,g), X₃: 4⋅X₃ {O(n)}
(g₃₉,g), X₄: 4⋅X₄ {O(n)}
(g₄₄,g), X₀: 2 {O(1)}
(g₄₄,g), X₁: 2 {O(1)}
(g₄₄,g), X₃: 4⋅X₃ {O(n)}
(g₄₄,g), X₄: 4⋅X₄ {O(n)}

Run probabilistic analysis on SCC: [g; h]

Plrf for transition g₂:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₃:h(X₀,X₁,X₂,X₃,X₄) :|: 1+X₂ ≤ X₃:

new bound:

2⋅X₂+2⋅X₃+2 {O(n)}

PLRF:

• g: 2+2⋅X₃-2⋅X₂
• h: 1+2⋅X₃-2⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₅:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₆:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₇:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₈:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1 ≤ X₀ ∧ 1 ≤ X₁ ∧ 1+X₂ ≤ X₃:

new bound:

2⋅X₂+2⋅X₃+2 {O(n)}

PLRF:

• g: 2+2⋅X₃-2⋅X₂
• h: 2+2⋅X₃-2⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₀:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₁₁:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₂:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₃:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 1+X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:

new bound:

2⋅X₂+2⋅X₃+2 {O(n)}

PLRF:

• g: 2+2⋅X₃-2⋅X₂
• h: 2+2⋅X₃-2⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₁₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₅:g(2+X₀,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₁₆:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₁₇:g(X₀-1,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₁₈:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:

new bound:

4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}

PLRF:

• g: 4/3+4/3⋅X₃-4/3⋅X₂
• h: 4/3+4/3⋅X₃-4/3⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₁₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₂₀:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₁:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₂:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₃:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 1 ≤ X₁ ∧ 1+X₂ ≤ X₃:

new bound:

2⋅X₂+2⋅X₃+2 {O(n)}

PLRF:

• g: 2+2⋅X₃-2⋅X₂
• h: 2+2⋅X₃-2⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₂₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₂₅:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₆:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₂₇:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₂₈:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 1+X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:

new bound:

2⋅X₂+2⋅X₃+2 {O(n)}

PLRF:

• g: 2+2⋅X₃-2⋅X₂
• h: 2+2⋅X₃-2⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₂₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₃₀:g(1+X₀,X₁,X₂-1,X₃,X₄) :+: [1/4]:t₃₁:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₂:g(X₀-2,X₁,2+X₂,X₃,X₄) :+: [1/4]:t₃₃:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 1+X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:

new bound:

4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}

PLRF:

• g: 4/3+4/3⋅X₃-4/3⋅X₂
• h: 4/3+4/3⋅X₃-4/3⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₃₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₃₅:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₆:g(X₀,2+X₁,2+X₂,X₃,X₄) :+: [1/4]:t₃₇:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₃₈:g(X₀,X₁-1,X₂-1,X₃,X₄) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1+X₂ ≤ X₃:

new bound:

4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}

PLRF:

• g: 4/3+4/3⋅X₃-4/3⋅X₂
• h: 4/3+4/3⋅X₃-4/3⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₃₉:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₄₀:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₁:g(X₀,1+X₁,X₂-1,X₃,X₄) :+: [1/4]:t₄₂:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₃:g(X₀,X₁-2,2+X₂,X₃,X₄) :|: 1+X₁ ≤ 0 ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 1+X₂ ≤ X₃:

new bound:

4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}

PLRF:

• g: 4/3+4/3⋅X₃-4/3⋅X₂
• h: 4/3+4/3⋅X₃-4/3⋅X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Plrf for transition g₄₄:h(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₄₅:g(1+X₀,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₆:g(X₀,1+X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₇:g(X₀-1,X₁,1+X₂,X₃,X₄) :+: [1/4]:t₄₈:g(X₀,X₁-1,1+X₂,X₃,X₄) :|: 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ 0 ≤ X₁ ∧ X₁ ≤ 0 ∧ 1+X₂ ≤ X₃:

new bound:

X₂+X₃+1 {O(n)}

PLRF:

• g: 1+X₃-X₂
• h: 1+X₃-X₂

Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use expected size bounds for entry point (g₀:f→[t₁:1:g],g)
Use classical time bound for entry point (g₀:f→[t₁:1:g],g)

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:49/3⋅X₂+49/3⋅X₃+52/3 {O(n)}
g₀: 1 {O(1)}
g₂: 2⋅X₂+2⋅X₃+2 {O(n)}
g₄: 2⋅X₂+2⋅X₃+2 {O(n)}
g₉: 2⋅X₂+2⋅X₃+2 {O(n)}
g₁₄: 4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
g₁₉: 2⋅X₂+2⋅X₃+2 {O(n)}
g₂₄: 2⋅X₂+2⋅X₃+2 {O(n)}
g₂₉: 4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
g₃₄: 4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
g₃₉: 4/3⋅X₂+4/3⋅X₃+4/3 {O(n)}
g₄₄: X₂+X₃+1 {O(n)}

Costbounds

Overall costbound: 172/3⋅X₂+172/3⋅X₃+172/3 {O(n)}
g₀: 0 {O(1)}
g₂: 0 {O(1)}
g₄: 8⋅X₂+8⋅X₃+8 {O(n)}
g₉: 8⋅X₂+8⋅X₃+8 {O(n)}
g₁₄: 16/3⋅X₂+16/3⋅X₃+16/3 {O(n)}
g₁₉: 8⋅X₂+8⋅X₃+8 {O(n)}
g₂₄: 8⋅X₂+8⋅X₃+8 {O(n)}
g₂₉: 16/3⋅X₂+16/3⋅X₃+16/3 {O(n)}
g₃₄: 16/3⋅X₂+16/3⋅X₃+16/3 {O(n)}
g₃₉: 16/3⋅X₂+16/3⋅X₃+16/3 {O(n)}
g₄₄: 4⋅X₂+4⋅X₃+4 {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₂,h), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₂,h), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₂,h), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₂,h), X₃: X₃ {O(n)}
(g₂,h), X₄: X₄ {O(n)}
(g₄,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₄,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₄,g), X₃: X₃ {O(n)}
(g₄,g), X₄: X₄ {O(n)}
(g₉,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₉,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₉,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₉,g), X₃: X₃ {O(n)}
(g₉,g), X₄: X₄ {O(n)}
(g₁₄,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₁₄,g), X₁: 2 {O(1)}
(g₁₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₁₄,g), X₃: X₃ {O(n)}
(g₁₄,g), X₄: X₄ {O(n)}
(g₁₉,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₁₉,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₁₉,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₁₉,g), X₃: X₃ {O(n)}
(g₁₉,g), X₄: X₄ {O(n)}
(g₂₄,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₂₄,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₂₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₂₄,g), X₃: X₃ {O(n)}
(g₂₄,g), X₄: X₄ {O(n)}
(g₂₉,g), X₀: 43/6⋅X₂+43/6⋅X₃+X₀+43/6 {O(n)}
(g₂₉,g), X₁: 2 {O(1)}
(g₂₉,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₂₉,g), X₃: X₃ {O(n)}
(g₂₉,g), X₄: X₄ {O(n)}
(g₃₄,g), X₀: 2 {O(1)}
(g₃₄,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₃₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₃₄,g), X₃: X₃ {O(n)}
(g₃₄,g), X₄: X₄ {O(n)}
(g₃₉,g), X₀: 2 {O(1)}
(g₃₉,g), X₁: 43/6⋅X₂+43/6⋅X₃+X₁+43/6 {O(n)}
(g₃₉,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₃₉,g), X₃: X₃ {O(n)}
(g₃₉,g), X₄: X₄ {O(n)}
(g₄₄,g), X₀: 2 {O(1)}
(g₄₄,g), X₁: 2 {O(1)}
(g₄₄,g), X₂: 59/3⋅X₃+62/3⋅X₂+59/3 {O(n)}
(g₄₄,g), X₃: X₃ {O(n)}
(g₄₄,g), X₄: X₄ {O(n)}