Preprocessing
Found invariant 1 ≤ X₃ ∧ 1 ≤ X₀+X₃ ∧ X₀ ≤ X₃ ∧ 0 ≤ X₀ for location h
Found invariant X₃ ≤ X₀ ∧ 0 ≤ X₀ for location j
Found invariant X₃ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ 0 ≤ X₀ for location k
Found invariant 0 ≤ X₀ for location g
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f
Program_Vars: X₀, X₁, X₂, X₃, X₄
Temp_Vars:
Locations: f, g, h, j, k
Transitions:
g₂:f(X₀,X₁,X₂,X₃,X₄) -{0}> t₃:g(0,X₁,X₂,X₃,X₄) :|:
g₄:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₅:h(X₀+UNIFORM(0, 1),X₁+3⋅X₄,X₂,X₃,X₄) :|: 1+X₀ ≤ X₃ ∧ 0 ≤ 1 ∧ 0 ≤ X₀
g₆:h(X₀,X₁,X₂,X₃,X₄) -{0}> t₇:g(X₀,X₁+Binomial (3, 1/2),X₂,X₃,X₄) :|: 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃
g₈:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₉:j(X₀,X₁,X₂,X₃,X₄) :|: X₃ ≤ X₀ ∧ 0 ≤ X₀
g₁₀:j(X₀,X₁,X₂,X₃,X₄) -{0}> t₁₁:k(X₀,X₁,X₂,X₃,X₄) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀
g₁₂:k(X₀,X₁,X₂,X₃,X₄) → t₁₃:k(X₀,X₁,X₂-1,X₃,X₄) :|: 1 ≤ X₂ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀
g₁₄:k(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₅:j(X₀,1+X₁,X₂,X₃,X₄) :+: [3/4]:t₁₆:j(X₀,X₁-1,X₂,X₃,X₄) :|: X₂ ≤ 0 ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₃ ∈ g₂
η (X₀) = 0
{0}
h
h
g->h
p = 1
t₅ ∈ g₄
η (X₀) = X₀+UNIFORM(0, 1)
η (X₁) = X₁+3⋅X₄
τ = 0 ≤ 1 ∧ 0 ≤ X₀ ∧ 1+X₀ ≤ X₃
{0}
j
j
g->j
p = 1
t₉ ∈ g₈
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀
{0}
h->g
p = 1
t₇ ∈ g₆
η (X₁) = X₁+Binomial (3, 1/2)
τ = 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃
{0}
k
k
j->k
p = 1
t₁₁ ∈ g₁₀
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₁
{0}
k->j
p = 1/4
t₁₅ ∈ g₁₄
η (X₁) = 1+X₁
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->j
p = 3/4
t₁₆ ∈ g₁₄
η (X₁) = X₁-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->k
p = 1
t₁₃ ∈ g₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ 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₈: 1 {O(1)}
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}
Sizebounds
(g₂,g), X₀: 0 {O(1)}
(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₈: 1 {O(1)}
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}
Sizebounds
(g₂,g), X₀: 0 {O(1)}
(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₄,h), X₄: X₄ {O(n)}
(g₆,g), X₂: X₂ {O(n)}
(g₆,g), X₃: X₃ {O(n)}
(g₆,g), X₄: X₄ {O(n)}
(g₈,j), X₂: 2⋅X₂ {O(n)}
(g₈,j), X₃: 2⋅X₃ {O(n)}
(g₈,j), X₄: 2⋅X₄ {O(n)}
Run probabilistic analysis on SCC: [g; h]
Plrf for transition g₄:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₅:h(X₀+UNIFORM(0, 1),X₁+3⋅X₄,X₂,X₃,X₄) :|: 1+X₀ ≤ X₃ ∧ 0 ≤ 1 ∧ 0 ≤ X₀:
new bound:
2⋅X₃ {O(n)}
PLRF:
• g: 2⋅X₃-2⋅X₀
• h: 2⋅X₃-2⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₃ ∈ g₂
η (X₀) = 0
{0}
h
h
g->h
p = 1
t₅ ∈ g₄
η (X₀) = X₀+UNIFORM(0, 1)
η (X₁) = X₁+3⋅X₄
τ = 0 ≤ 1 ∧ 0 ≤ X₀ ∧ 1+X₀ ≤ X₃
{0}
j
j
g->j
p = 1
t₉ ∈ g₈
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀
{0}
h->g
p = 1
t₇ ∈ g₆
η (X₁) = X₁+Binomial (3, 1/2)
τ = 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃
{0}
k
k
j->k
p = 1
t₁₁ ∈ g₁₀
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₁
{0}
k->j
p = 1/4
t₁₅ ∈ g₁₄
η (X₁) = 1+X₁
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->j
p = 3/4
t₁₆ ∈ g₁₄
η (X₁) = X₁-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->k
p = 1
t₁₃ ∈ g₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ 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₄) -{0}> t₇:g(X₀,X₁+Binomial (3, 1/2),X₂,X₃,X₄) :|: 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃:
new bound:
2⋅X₃ {O(n)}
PLRF:
• g: 2⋅X₃-2⋅X₀
• h: 1+2⋅X₃-2⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₃ ∈ g₂
η (X₀) = 0
{0}
h
h
g->h
p = 1
t₅ ∈ g₄
η (X₀) = X₀+UNIFORM(0, 1)
η (X₁) = X₁+3⋅X₄
τ = 0 ≤ 1 ∧ 0 ≤ X₀ ∧ 1+X₀ ≤ X₃
{0}
j
j
g->j
p = 1
t₉ ∈ g₈
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀
{0}
h->g
p = 1
t₇ ∈ g₆
η (X₁) = X₁+Binomial (3, 1/2)
τ = 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃
{0}
k
k
j->k
p = 1
t₁₁ ∈ g₁₀
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₁
{0}
k->j
p = 1/4
t₁₅ ∈ g₁₄
η (X₁) = 1+X₁
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->j
p = 3/4
t₁₆ ∈ g₁₄
η (X₁) = X₁-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->k
p = 1
t₁₃ ∈ g₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ 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)
Run classical analysis on SCC: [j; k]
MPRF for transition t₁₃: k(X₀,X₁,X₂,X₃,X₄) → k(X₀,X₁,X₂-1,X₃,X₄) :|: 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₂ of depth 1:
new bound:
2⋅X₂ {O(n)}
MPRF:
• j: [X₂]
• k: [X₂]
Show Graph
G
f
f
g
g
f->g
t₃
η (X₀) = 0
{0}
h
h
g->h
t₅
η (X₀) = Temp_Int₁
η (X₁) = X₁+3⋅X₄
τ = 0 ≤ 1 ∧ 0 ≤ X₀ ∧ Temp_Int₁ ≤ Temp_Int₂+X₀ ∧ Temp_Int₂+X₀ ≤ Temp_Int₁ ∧ 0 ≤ Temp_Int₂ ∧ Temp_Int₂ ≤ 1 ∧ 1+X₀ ≤ X₃
{0}
j
j
g->j
t₉
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀
{0}
h->g
t₇
η (X₁) = Temp_Int₃
τ = 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃ ∧ Temp_Int₃ ≤ Temp_Int₄+X₁ ∧ Temp_Int₄+X₁ ≤ Temp_Int₃ ∧ 0 ≤ Temp_Int₄ ∧ Temp_Int₄ ≤ 3
{0}
k
k
j->k
t₁₁
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₁
{0}
k->j
t₁₅
η (X₁) = 1+X₁
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->j
t₁₆
η (X₁) = X₁-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->k
t₁₃
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₂
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₂: 1 {O(1)}
g₄: 2⋅X₃ {O(n)}
g₆: 2⋅X₃ {O(n)}
g₈: 1 {O(1)}
g₁₀: inf {Infinity}
g₁₂: 2⋅X₂ {O(n)}
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}
Sizebounds
(g₂,g), X₀: 0 {O(1)}
(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₁: 12⋅X₃⋅X₄+3⋅X₃+X₁ {O(n^2)}
(g₄,h), X₂: X₂ {O(n)}
(g₄,h), X₃: X₃ {O(n)}
(g₄,h), X₄: X₄ {O(n)}
(g₆,g), X₀: X₃ {O(n)}
(g₆,g), X₁: 12⋅X₃⋅X₄+3⋅X₃+X₁ {O(n^2)}
(g₆,g), X₂: X₂ {O(n)}
(g₆,g), X₃: X₃ {O(n)}
(g₆,g), X₄: X₄ {O(n)}
(g₈,j), X₀: X₃ {O(n)}
(g₈,j), X₁: 12⋅X₃⋅X₄+2⋅X₁+3⋅X₃ {O(n^2)}
(g₈,j), X₂: 2⋅X₂ {O(n)}
(g₈,j), X₃: 2⋅X₃ {O(n)}
(g₈,j), X₄: 2⋅X₄ {O(n)}
(g₁₀,k), X₂: 2⋅X₂ {O(n)}
(g₁₀,k), X₃: 2⋅X₃ {O(n)}
(g₁₀,k), X₄: 2⋅X₄ {O(n)}
(g₁₂,k), X₂: 2⋅X₂ {O(n)}
(g₁₂,k), X₃: 2⋅X₃ {O(n)}
(g₁₂,k), X₄: 2⋅X₄ {O(n)}
(g₁₄,j), X₂: 4⋅X₂ {O(n)}
(g₁₄,j), X₃: 4⋅X₃ {O(n)}
(g₁₄,j), X₄: 4⋅X₄ {O(n)}
Run probabilistic analysis on SCC: [j; k]
Plrf for transition g₁₀:j(X₀,X₁,X₂,X₃,X₄) -{0}> t₁₁:k(X₀,X₁,X₂,X₃,X₄) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀:
new bound:
24⋅X₃⋅X₄+4⋅X₁+6⋅X₃+1 {O(n^2)}
PLRF:
• j: 1+2⋅X₁
• k: 2⋅X₁
Show Graph
G
f
f
g
g
f->g
p = 1
t₃ ∈ g₂
η (X₀) = 0
{0}
h
h
g->h
p = 1
t₅ ∈ g₄
η (X₀) = X₀+UNIFORM(0, 1)
η (X₁) = X₁+3⋅X₄
τ = 0 ≤ 1 ∧ 0 ≤ X₀ ∧ 1+X₀ ≤ X₃
{0}
j
j
g->j
p = 1
t₉ ∈ g₈
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀
{0}
h->g
p = 1
t₇ ∈ g₆
η (X₁) = X₁+Binomial (3, 1/2)
τ = 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃
{0}
k
k
j->k
p = 1
t₁₁ ∈ g₁₀
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₁
{0}
k->j
p = 1/4
t₁₅ ∈ g₁₄
η (X₁) = 1+X₁
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->j
p = 3/4
t₁₆ ∈ g₁₄
η (X₁) = X₁-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->k
p = 1
t₁₃ ∈ g₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₂
Use expected size bounds for entry point (g₈:g→[t₉:1:j],j)
Use classical time bound for entry point (g₈:g→[t₉:1:j],j)
Plrf for transition g₁₄:k(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₅:j(X₀,1+X₁,X₂,X₃,X₄) :+: [3/4]:t₁₆:j(X₀,X₁-1,X₂,X₃,X₄) :|: X₂ ≤ 0 ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀:
new bound:
24⋅X₃⋅X₄+4⋅X₁+6⋅X₃ {O(n^2)}
PLRF:
• j: 2⋅X₁
• k: 2⋅X₁
Show Graph
G
f
f
g
g
f->g
p = 1
t₃ ∈ g₂
η (X₀) = 0
{0}
h
h
g->h
p = 1
t₅ ∈ g₄
η (X₀) = X₀+UNIFORM(0, 1)
η (X₁) = X₁+3⋅X₄
τ = 0 ≤ 1 ∧ 0 ≤ X₀ ∧ 1+X₀ ≤ X₃
{0}
j
j
g->j
p = 1
t₉ ∈ g₈
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀
{0}
h->g
p = 1
t₇ ∈ g₆
η (X₁) = X₁+Binomial (3, 1/2)
τ = 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃
{0}
k
k
j->k
p = 1
t₁₁ ∈ g₁₀
τ = 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₁
{0}
k->j
p = 1/4
t₁₅ ∈ g₁₄
η (X₁) = 1+X₁
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->j
p = 3/4
t₁₆ ∈ g₁₄
η (X₁) = X₁-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ X₂ ≤ 0
k->k
p = 1
t₁₃ ∈ g₁₂
η (X₂) = X₂-1
τ = 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₂
Use expected size bounds for entry point (g₈:g→[t₉:1:j],j)
Use classical time bound for entry point (g₈:g→[t₉:1:j],j)
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:48⋅X₃⋅X₄+16⋅X₃+2⋅X₂+8⋅X₁+3 {O(n^2)}
g₂: 1 {O(1)}
g₄: 2⋅X₃ {O(n)}
g₆: 2⋅X₃ {O(n)}
g₈: 1 {O(1)}
g₁₀: 24⋅X₃⋅X₄+4⋅X₁+6⋅X₃+1 {O(n^2)}
g₁₂: 2⋅X₂ {O(n)}
g₁₄: 24⋅X₃⋅X₄+4⋅X₁+6⋅X₃ {O(n^2)}
Costbounds
Overall costbound: 48⋅X₃⋅X₄+12⋅X₃+2⋅X₂+8⋅X₁ {O(n^2)}
g₂: 0 {O(1)}
g₄: 0 {O(1)}
g₆: 0 {O(1)}
g₈: 0 {O(1)}
g₁₀: 0 {O(1)}
g₁₂: 2⋅X₂ {O(n)}
g₁₄: 48⋅X₃⋅X₄+12⋅X₃+8⋅X₁ {O(n^2)}
Sizebounds
(g₂,g), X₀: 0 {O(1)}
(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₁: 12⋅X₃⋅X₄+3⋅X₃+X₁ {O(n^2)}
(g₄,h), X₂: X₂ {O(n)}
(g₄,h), X₃: X₃ {O(n)}
(g₄,h), X₄: X₄ {O(n)}
(g₆,g), X₀: X₃ {O(n)}
(g₆,g), X₁: 12⋅X₃⋅X₄+3⋅X₃+X₁ {O(n^2)}
(g₆,g), X₂: X₂ {O(n)}
(g₆,g), X₃: X₃ {O(n)}
(g₆,g), X₄: X₄ {O(n)}
(g₈,j), X₀: X₃ {O(n)}
(g₈,j), X₁: 12⋅X₃⋅X₄+2⋅X₁+3⋅X₃ {O(n^2)}
(g₈,j), X₂: 2⋅X₂ {O(n)}
(g₈,j), X₃: 2⋅X₃ {O(n)}
(g₈,j), X₄: 2⋅X₄ {O(n)}
(g₁₀,k), X₀: X₃ {O(n)}
(g₁₀,k), X₁: 18⋅X₃⋅X₄+3⋅X₁+9/2⋅X₃ {O(n^2)}
(g₁₀,k), X₂: 2⋅X₂ {O(n)}
(g₁₀,k), X₃: 2⋅X₃ {O(n)}
(g₁₀,k), X₄: 2⋅X₄ {O(n)}
(g₁₂,k), X₀: X₃ {O(n)}
(g₁₂,k), X₁: 18⋅X₃⋅X₄+3⋅X₁+9/2⋅X₃ {O(n^2)}
(g₁₂,k), X₂: 2⋅X₂ {O(n)}
(g₁₂,k), X₃: 2⋅X₃ {O(n)}
(g₁₂,k), X₄: 2⋅X₄ {O(n)}
(g₁₄,j), X₀: X₃ {O(n)}
(g₁₄,j), X₁: 18⋅X₃⋅X₄+3⋅X₁+9/2⋅X₃ {O(n^2)}
(g₁₄,j), X₂: 4⋅X₂ {O(n)}
(g₁₄,j), X₃: 4⋅X₃ {O(n)}
(g₁₄,j), X₄: 4⋅X₄ {O(n)}