Preprocessing

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

Found invariant X₁ ≤ X₀ for location j

Found invariant X₄ ≤ X₁ ∧ 0 ≤ X₄ ∧ 1 ≤ X₃+X₄ ∧ 2 ≤ X₁+X₄ ∧ 1 ≤ X₀+X₄ ∧ 1+X₃ ≤ X₁ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₃ ∧ 3 ≤ X₁+X₃ ∧ 2 ≤ X₀+X₃ ∧ 2 ≤ X₁ ∧ 3 ≤ X₀+X₁ ∧ 1+X₀ ≤ X₁ ∧ 1 ≤ X₀ for location i

Probabilistic Analysis

Probabilistic Program after Preprocessing

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

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; i]

MPRF for transition t₃: g(X₀,X₁,X₂,X₃,X₄) -{0}> h(X₀,X₁,X₂,Temp_Int₁₀₇,X₄) :|: 1+X₀ ≤ X₁ ∧ Temp_Int₁₀₇ ≤ 0 ∧ 0 ≤ Temp_Int₁₀₇ ∧ 1+X₀ ≤ X₁ of depth 1:

new bound:

X₀+X₁ {O(n)}

MPRF:

• g: [X₁-X₀]
• h: [X₁-2-X₀]
• i: [X₁-2-X₀]

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

new bound:

X₀+X₁+1 {O(n)}

MPRF:

• g: [1+X₁-X₀]
• h: [X₁-X₀]
• i: [X₁-X₀]

MPRF for transition t₅: h(X₀,X₁,X₂,X₃,X₄) -{0}> i(X₀,X₁,X₂,1+X₃,Temp_Int₁₁₁) :|: 1+X₀ ≤ X₁ ∧ 0 ≤ X₃ ∧ 1+X₀ ≤ X₁ ∧ 1+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ Temp_Int₁₁₁ ≤ 0 ∧ 0 ≤ Temp_Int₁₁₁ ∧ 1+X₃ ≤ X₀ of depth 1:

new bound:

2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}

MPRF:

• g: [X₀]
• h: [X₀-X₃]
• i: [X₀-X₃]

MPRF for transition t₉: i(X₀,X₁,X₂,X₃,X₄) -{0}> h(X₀,X₁,X₂,X₃,X₄) :|: 1 ≤ X₀ ∧ 1 ≤ X₀+X₄ ∧ 1+X₀ ≤ X₁ ∧ 1+X₃ ≤ X₁ ∧ 1 ≤ X₃ ∧ 1 ≤ X₃+X₄ ∧ 2 ≤ X₀+X₃ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₁+X₃ ∧ X₃ ≤ X₀ ∧ X₄ ≤ X₁ ∧ 0 ≤ X₄ ∧ X₁ ≤ X₄ of depth 1:

new bound:

2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}

MPRF:

• g: [X₀]
• h: [X₀-X₃]
• i: [1+X₀-X₃]

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

new bound:

14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}

MPRF:

• g: [2⋅X₁]
• h: [2⋅X₁]
• i: [2⋅X₁-X₄]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: X₀+X₁ {O(n)}
g₄: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
g₆: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
g₈: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
g₁₀: X₀+X₁+1 {O(n)}
g₁₂: 1 {O(1)}
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}

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₀: 2⋅X₀+X₁+1 {O(n)}
(g₂,h), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₂,h), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+X₄+2 {O(n^3)}
(g₄,i), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₄,i), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₄,i), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₄,i), X₄: 0 {O(1)}
(g₆,i), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₆,i), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₆,i), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₆,i), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
(g₈,h), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₈,h), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₈,h), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₈,h), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
(g₁₀,g), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₁₀,g), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₁₀,g), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₁₀,g), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+X₄+2 {O(n^3)}
(g₁₂,j), X₀: 3⋅X₀+X₁+1 {O(n)}
(g₁₂,j), X₁: 3⋅X₁+X₀+1 {O(n)}
(g₁₂,j), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+X₃+1 {O(n^2)}
(g₁₂,j), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2⋅X₄+2 {O(n^3)}

Run probabilistic analysis on SCC: [g; h; i]

Run classical analysis on SCC: [j]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: X₀+X₁ {O(n)}
g₄: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
g₆: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
g₈: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
g₁₀: X₀+X₁+1 {O(n)}
g₁₂: 1 {O(1)}
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}

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₀: 2⋅X₀+X₁+1 {O(n)}
(g₂,h), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₂,h), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₂,h), X₃: 0 {O(1)}
(g₂,h), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+X₄+2 {O(n^3)}
(g₄,i), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₄,i), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₄,i), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₄,i), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₄,i), X₄: 0 {O(1)}
(g₆,i), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₆,i), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₆,i), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₆,i), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₆,i), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
(g₈,h), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₈,h), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₈,h), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₈,h), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₈,h), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
(g₁₀,g), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₁₀,g), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₁₀,g), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₁₀,g), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₁₀,g), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+X₄+2 {O(n^3)}
(g₁₂,j), X₀: 3⋅X₀+X₁+1 {O(n)}
(g₁₂,j), X₁: 3⋅X₁+X₀+1 {O(n)}
(g₁₂,j), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+2⋅X₂+64⋅X₀+64⋅X₁+8 {O(n^5)}
(g₁₂,j), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+X₃+1 {O(n^2)}
(g₁₂,j), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2⋅X₄+2 {O(n^3)}
(g₁₄,j), X₀: 2⋅X₁+6⋅X₀+2 {O(n)}
(g₁₄,j), X₁: 2⋅X₀+6⋅X₁+2 {O(n)}
(g₁₄,j), X₃: 2⋅X₁⋅X₁+4⋅X₀⋅X₀+6⋅X₀⋅X₁+2⋅X₃+4⋅X₁+8⋅X₀+2 {O(n^2)}
(g₁₄,j), X₄: 28⋅X₀⋅X₀⋅X₁+28⋅X₀⋅X₁⋅X₁+8⋅X₀⋅X₀⋅X₀+8⋅X₁⋅X₁⋅X₁+20⋅X₁⋅X₁+24⋅X₀⋅X₀+52⋅X₀⋅X₁+20⋅X₀+20⋅X₁+4⋅X₄+4 {O(n^3)}

Run probabilistic analysis on SCC: [j]

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

new bound:

384⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+384⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+64⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+64⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+848⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+848⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1248⋅X₀⋅X₁⋅X₁⋅X₁+1328⋅X₀⋅X₀⋅X₀⋅X₁+2064⋅X₀⋅X₀⋅X₁⋅X₁+256⋅X₁⋅X₁⋅X₁⋅X₁+288⋅X₀⋅X₀⋅X₀⋅X₀+1536⋅X₀⋅X₁⋅X₁+1584⋅X₀⋅X₀⋅X₁+432⋅X₁⋅X₁⋅X₁+480⋅X₀⋅X₀⋅X₀+352⋅X₁⋅X₁+368⋅X₀⋅X₀+768⋅X₀⋅X₁+128⋅X₀+128⋅X₁+4⋅X₂+16 {O(n^5)}

PLRF:

• j: 2⋅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:384⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+384⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+64⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+64⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+848⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+848⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1248⋅X₀⋅X₁⋅X₁⋅X₁+1328⋅X₀⋅X₀⋅X₀⋅X₁+2064⋅X₀⋅X₀⋅X₁⋅X₁+256⋅X₁⋅X₁⋅X₁⋅X₁+288⋅X₀⋅X₀⋅X₀⋅X₀+1550⋅X₀⋅X₁⋅X₁+1598⋅X₀⋅X₀⋅X₁+436⋅X₁⋅X₁⋅X₁+484⋅X₀⋅X₀⋅X₀+364⋅X₁⋅X₁+384⋅X₀⋅X₀+800⋅X₀⋅X₁+144⋅X₁+148⋅X₀+4⋅X₂+23 {O(n^5)}
g₀: 1 {O(1)}
g₂: X₀+X₁ {O(n)}
g₄: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
g₆: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
g₈: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
g₁₀: X₀+X₁+1 {O(n)}
g₁₂: 1 {O(1)}
g₁₄: 384⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+384⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+64⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+64⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+848⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+848⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1248⋅X₀⋅X₁⋅X₁⋅X₁+1328⋅X₀⋅X₀⋅X₀⋅X₁+2064⋅X₀⋅X₀⋅X₁⋅X₁+256⋅X₁⋅X₁⋅X₁⋅X₁+288⋅X₀⋅X₀⋅X₀⋅X₀+1536⋅X₀⋅X₁⋅X₁+1584⋅X₀⋅X₀⋅X₁+432⋅X₁⋅X₁⋅X₁+480⋅X₀⋅X₀⋅X₀+352⋅X₁⋅X₁+368⋅X₀⋅X₀+768⋅X₀⋅X₁+128⋅X₀+128⋅X₁+4⋅X₂+16 {O(n^5)}

Costbounds

Overall costbound: 128⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+128⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+1696⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+1696⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+768⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+768⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+2496⋅X₀⋅X₁⋅X₁⋅X₁+2656⋅X₀⋅X₀⋅X₀⋅X₁+4128⋅X₀⋅X₀⋅X₁⋅X₁+512⋅X₁⋅X₁⋅X₁⋅X₁+576⋅X₀⋅X₀⋅X₀⋅X₀+3086⋅X₀⋅X₁⋅X₁+3182⋅X₀⋅X₀⋅X₁+868⋅X₁⋅X₁⋅X₁+964⋅X₀⋅X₀⋅X₀+1562⋅X₀⋅X₁+714⋅X₁⋅X₁+748⋅X₀⋅X₀+266⋅X₀+266⋅X₁+8⋅X₂+34 {O(n^5)}
g₀: 0 {O(1)}
g₂: 0 {O(1)}
g₄: 0 {O(1)}
g₆: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
g₈: 0 {O(1)}
g₁₀: 0 {O(1)}
g₁₂: 0 {O(1)}
g₁₄: 128⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+128⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+1696⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+1696⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+768⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+768⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+2496⋅X₀⋅X₁⋅X₁⋅X₁+2656⋅X₀⋅X₀⋅X₀⋅X₁+4128⋅X₀⋅X₀⋅X₁⋅X₁+512⋅X₁⋅X₁⋅X₁⋅X₁+576⋅X₀⋅X₀⋅X₀⋅X₀+3072⋅X₀⋅X₁⋅X₁+3168⋅X₀⋅X₀⋅X₁+864⋅X₁⋅X₁⋅X₁+960⋅X₀⋅X₀⋅X₀+1536⋅X₀⋅X₁+704⋅X₁⋅X₁+736⋅X₀⋅X₀+256⋅X₀+256⋅X₁+8⋅X₂+32 {O(n^5)}

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₀: 2⋅X₀+X₁+1 {O(n)}
(g₂,h), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₂,h), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₂,h), X₃: 0 {O(1)}
(g₂,h), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+X₄+2 {O(n^3)}
(g₄,i), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₄,i), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₄,i), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₄,i), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₄,i), X₄: 0 {O(1)}
(g₆,i), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₆,i), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₆,i), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₆,i), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₆,i), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
(g₈,h), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₈,h), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₈,h), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₈,h), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₈,h), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2 {O(n^3)}
(g₁₀,g), X₀: 2⋅X₀+X₁+1 {O(n)}
(g₁₀,g), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₁₀,g), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+64⋅X₀+64⋅X₁+X₂+8 {O(n^5)}
(g₁₀,g), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+1 {O(n^2)}
(g₁₀,g), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+X₄+2 {O(n^3)}
(g₁₂,j), X₀: 3⋅X₀+X₁+1 {O(n)}
(g₁₂,j), X₁: 3⋅X₁+X₀+1 {O(n)}
(g₁₂,j), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+2⋅X₂+64⋅X₀+64⋅X₁+8 {O(n^5)}
(g₁₂,j), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+X₃+1 {O(n^2)}
(g₁₂,j), X₄: 14⋅X₀⋅X₀⋅X₁+14⋅X₀⋅X₁⋅X₁+4⋅X₀⋅X₀⋅X₀+4⋅X₁⋅X₁⋅X₁+10⋅X₁⋅X₁+12⋅X₀⋅X₀+26⋅X₀⋅X₁+10⋅X₀+10⋅X₁+2⋅X₄+2 {O(n^3)}
(g₁₄,j), X₀: 3⋅X₀+X₁+1 {O(n)}
(g₁₄,j), X₁: 3⋅X₁+X₀+1 {O(n)}
(g₁₄,j), X₂: 192⋅X₀⋅X₀⋅X₀⋅X₀⋅X₁+192⋅X₀⋅X₁⋅X₁⋅X₁⋅X₁+32⋅X₀⋅X₀⋅X₀⋅X₀⋅X₀+32⋅X₁⋅X₁⋅X₁⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₀⋅X₁⋅X₁+424⋅X₀⋅X₀⋅X₁⋅X₁⋅X₁+1032⋅X₀⋅X₀⋅X₁⋅X₁+128⋅X₁⋅X₁⋅X₁⋅X₁+144⋅X₀⋅X₀⋅X₀⋅X₀+624⋅X₀⋅X₁⋅X₁⋅X₁+664⋅X₀⋅X₀⋅X₀⋅X₁+216⋅X₁⋅X₁⋅X₁+240⋅X₀⋅X₀⋅X₀+768⋅X₀⋅X₁⋅X₁+792⋅X₀⋅X₀⋅X₁+176⋅X₁⋅X₁+184⋅X₀⋅X₀+384⋅X₀⋅X₁+2⋅X₂+64⋅X₀+64⋅X₁+8 {O(n^5)}
(g₁₄,j), X₃: 2⋅X₀⋅X₀+3⋅X₀⋅X₁+X₁⋅X₁+2⋅X₁+4⋅X₀+X₃+1 {O(n^2)}
(g₁₄,j), X₄: 28⋅X₀⋅X₀⋅X₁+28⋅X₀⋅X₁⋅X₁+8⋅X₀⋅X₀⋅X₀+8⋅X₁⋅X₁⋅X₁+20⋅X₁⋅X₁+24⋅X₀⋅X₀+52⋅X₀⋅X₁+20⋅X₀+20⋅X₁+4⋅X₄+4 {O(n^3)}