Preprocessing

Eliminate variables [K; L; X₁; X₂] that do not contribute to the problem

Found invariant X₄ ≤ X₇ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₀ for location f65

Found invariant X₄ ≤ X₆ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₃ for location f45

Found invariant X₄ ≤ X₆ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₀ for location f55

Found invariant X₄ ≤ X₅ ∧ X₄ ≤ X₃ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀ for location f37

Found invariant X₄ ≤ X₉ ∧ X₄ ≤ X₈ ∧ X₄ ≤ X₇ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₃ for location f83

Found invariant X₄ ≤ X₈ ∧ X₄ ≤ X₇ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₀ for location f75

Found invariant X₄ ≤ X₉ ∧ X₄ ≤ X₈ ∧ X₄ ≤ X₇ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₀ for location f93

Found invariant X₀ ≤ 0 ∧ 0 ≤ X₀ for location f17

Found invariant X₄ ≤ X₃ ∧ X₀ ≤ 0 ∧ 0 ≤ X₀ for location f27

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f0
Program_Vars: X₀, X₁, X₂, X₃, X₄, X₅, X₆, X₇, X₈, X₉
Temp_Vars:
Locations: f0, f17, f27, f37, f45, f55, f65, f75, f83, f93
Transitions:
g₀:f0(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₁:f17(0,K,L,0,X₄,X₅,X₆,X₇,X₈,X₉) :|:
g₂:f17(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → [3/4]:t₃:f17(X₀,X₁,X₂,1+X₃,X₄,X₅,X₆,X₇,X₈,X₉) :+: [1/4]:t₄:f17(X₀,X₁,X₂,X₃-1,X₄,X₅,X₆,X₇,X₈,X₉) :|: 1+X₃ ≤ X₄ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0
g₅:f27(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → [3/4]:t₆:f27(X₀,X₁,X₂,X₃,X₄,1+X₅,X₆,X₇,X₈,X₉) :+: [1/4]:t₇:f27(X₀,X₁,X₂,X₃,X₄,X₅-1,X₆,X₇,X₈,X₉) :|: 1+X₅ ≤ X₄ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ X₄ ≤ X₃
g₈:f37(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → [3/4]:t₉:f37(X₀,X₁,X₂,X₃,X₄,X₅,1+X₆,X₇,X₈,X₉) :+: [1/4]:t₁₀:f37(X₀,X₁,X₂,X₃,X₄,X₅,X₆-1,X₇,X₈,X₉) :|: 1+X₆ ≤ X₄ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅
g₁₁:f45(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → [3/4]:t₁₂:f45(1+X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :+: [1/4]:t₁₃:f45(X₀-1,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :|: 1+X₀ ≤ X₄ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆
g₁₄:f55(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → [3/4]:t₁₅:f55(X₀,X₁,X₂,X₃,X₄,X₅,X₆,1+X₇,X₈,X₉) :+: [1/4]:t₁₆:f55(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇-1,X₈,X₉) :|: 1+X₇ ≤ X₄ ∧ X₄ ≤ X₀ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆
g₁₇:f65(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → [3/4]:t₁₈:f65(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,1+X₈,X₉) :+: [1/4]:t₁₉:f65(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈-1,X₉) :|: 1+X₈ ≤ X₄ ∧ X₄ ≤ X₀ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₇
g₂₀:f75(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → [3/4]:t₂₁:f75(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,1+X₉) :+: [1/4]:t₂₂:f75(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉-1) :|: 1+X₉ ≤ X₄ ∧ X₄ ≤ X₀ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₇ ∧ X₄ ≤ X₈
g₂₃:f83(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → [3/4]:t₂₄:f83(1+X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :+: [1/4]:t₂₅:f83(X₀-1,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :|: 1+X₀ ≤ X₄ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₇ ∧ X₄ ≤ X₈ ∧ X₄ ≤ X₉
g₂₆:f83(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₂₇:f93(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :|: X₄ ≤ X₀ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₇ ∧ X₄ ≤ X₈ ∧ X₄ ≤ X₉
g₂₈:f75(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₂₉:f83(0,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :|: X₄ ≤ X₉ ∧ X₄ ≤ X₀ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₇ ∧ X₄ ≤ X₈
g₃₀:f65(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₃₁:f75(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,0) :|: X₄ ≤ X₈ ∧ X₄ ≤ X₀ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆ ∧ X₄ ≤ X₇
g₃₂:f55(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₃₃:f65(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,0,X₉) :|: X₄ ≤ X₇ ∧ X₄ ≤ X₀ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆
g₃₄:f45(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₃₅:f55(X₀,X₁,X₂,X₃,X₄,X₅,X₆,0,X₈,X₉) :|: X₄ ≤ X₀ ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅ ∧ X₄ ≤ X₆
g₃₆:f37(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₃₇:f45(0,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) :|: X₄ ≤ X₆ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ X₄ ≤ X₃ ∧ X₄ ≤ X₅
g₃₈:f27(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₃₉:f37(X₀,X₁,X₂,X₃,X₄,X₅,0,X₇,X₈,X₉) :|: X₄ ≤ X₅ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0 ∧ X₄ ≤ X₃
g₄₀:f17(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇,X₈,X₉) → t₄₁:f27(X₀,X₁,X₂,X₃,X₄,0,X₆,X₇,X₈,X₉) :|: X₄ ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ 0

Run classical analysis on SCC: [f0]

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₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}

Run probabilistic analysis on SCC: [f0]

Run classical analysis on SCC: [f17]

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₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₄: 2⋅X₄ {O(n)}
(g₂,f17), X₅: 2⋅X₅ {O(n)}
(g₂,f17), X₆: 2⋅X₆ {O(n)}
(g₂,f17), X₇: 2⋅X₇ {O(n)}
(g₂,f17), X₈: 2⋅X₈ {O(n)}
(g₂,f17), X₉: 2⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f17]

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

new bound:

2⋅X₄ {O(n)}

PLRF:

• f17: 2⋅X₄-2⋅X₃

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

Run classical analysis on SCC: [f27]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₁: inf {Infinity}
g₁₄: inf {Infinity}
g₁₇: inf {Infinity}
g₂₀: inf {Infinity}
g₂₃: inf {Infinity}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f27]

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

new bound:

4⋅X₄ {O(n)}

PLRF:

• f27: 2⋅X₄-2⋅X₅

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

Run classical analysis on SCC: [f37]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: 4⋅X₄ {O(n)}
g₈: inf {Infinity}
g₁₁: inf {Infinity}
g₁₄: inf {Infinity}
g₁₇: inf {Infinity}
g₂₀: inf {Infinity}
g₂₃: inf {Infinity}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₃: 2⋅X₄ {O(n)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₅: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₈,f37), X₀: 0 {O(1)}
(g₈,f37), X₄: 8⋅X₄ {O(n)}
(g₈,f37), X₇: 8⋅X₇ {O(n)}
(g₈,f37), X₈: 8⋅X₈ {O(n)}
(g₈,f37), X₉: 8⋅X₉ {O(n)}
(g₃₆,f45), X₀: 0 {O(1)}
(g₃₆,f45), X₄: 8⋅X₄ {O(n)}
(g₃₆,f45), X₇: 8⋅X₇ {O(n)}
(g₃₆,f45), X₈: 8⋅X₈ {O(n)}
(g₃₆,f45), X₉: 8⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₃: 4⋅X₄ {O(n)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₅: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f37]

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

new bound:

8⋅X₄ {O(n)}

PLRF:

• f37: 2⋅X₅-2⋅X₆

Use expected size bounds for entry point (g₃₈:f27→[t₃₉:1:f37],f37)
Use expected size bounds for entry point (g₃₈:f27→[t₃₉:1:f37],f37)
Use classical time bound for entry point (g₃₈:f27→[t₃₉:1:f37],f37)

Run classical analysis on SCC: [f45]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: 4⋅X₄ {O(n)}
g₈: 8⋅X₄ {O(n)}
g₁₁: inf {Infinity}
g₁₄: inf {Infinity}
g₁₇: inf {Infinity}
g₂₀: inf {Infinity}
g₂₃: inf {Infinity}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₃: 2⋅X₄ {O(n)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₅: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₈,f37), X₀: 0 {O(1)}
(g₈,f37), X₃: 4⋅X₄ {O(n)}
(g₈,f37), X₄: 8⋅X₄ {O(n)}
(g₈,f37), X₅: 4⋅X₄ {O(n)}
(g₈,f37), X₆: 8⋅X₄ {O(n)}
(g₈,f37), X₇: 8⋅X₇ {O(n)}
(g₈,f37), X₈: 8⋅X₈ {O(n)}
(g₈,f37), X₉: 8⋅X₉ {O(n)}
(g₁₁,f45), X₄: 16⋅X₄ {O(n)}
(g₁₁,f45), X₇: 16⋅X₇ {O(n)}
(g₁₁,f45), X₈: 16⋅X₈ {O(n)}
(g₁₁,f45), X₉: 16⋅X₉ {O(n)}
(g₃₄,f55), X₄: 16⋅X₄ {O(n)}
(g₃₄,f55), X₇: 0 {O(1)}
(g₃₄,f55), X₈: 16⋅X₈ {O(n)}
(g₃₄,f55), X₉: 16⋅X₉ {O(n)}
(g₃₆,f45), X₀: 0 {O(1)}
(g₃₆,f45), X₃: 8⋅X₄ {O(n)}
(g₃₆,f45), X₄: 8⋅X₄ {O(n)}
(g₃₆,f45), X₅: 8⋅X₄ {O(n)}
(g₃₆,f45), X₆: 8⋅X₄ {O(n)}
(g₃₆,f45), X₇: 8⋅X₇ {O(n)}
(g₃₆,f45), X₈: 8⋅X₈ {O(n)}
(g₃₆,f45), X₉: 8⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₃: 4⋅X₄ {O(n)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₅: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f45]

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

new bound:

16⋅X₄ {O(n)}

PLRF:

• f45: 2⋅X₆-2⋅X₀

Use expected size bounds for entry point (g₃₆:f37→[t₃₇:1:f45],f45)
Use expected size bounds for entry point (g₃₆:f37→[t₃₇:1:f45],f45)
Use classical time bound for entry point (g₃₆:f37→[t₃₇:1:f45],f45)

Run classical analysis on SCC: [f55]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: 4⋅X₄ {O(n)}
g₈: 8⋅X₄ {O(n)}
g₁₁: 16⋅X₄ {O(n)}
g₁₄: inf {Infinity}
g₁₇: inf {Infinity}
g₂₀: inf {Infinity}
g₂₃: inf {Infinity}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₃: 2⋅X₄ {O(n)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₅: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₈,f37), X₀: 0 {O(1)}
(g₈,f37), X₃: 4⋅X₄ {O(n)}
(g₈,f37), X₄: 8⋅X₄ {O(n)}
(g₈,f37), X₅: 4⋅X₄ {O(n)}
(g₈,f37), X₆: 8⋅X₄ {O(n)}
(g₈,f37), X₇: 8⋅X₇ {O(n)}
(g₈,f37), X₈: 8⋅X₈ {O(n)}
(g₈,f37), X₉: 8⋅X₉ {O(n)}
(g₁₁,f45), X₀: 16⋅X₄ {O(n)}
(g₁₁,f45), X₃: 8⋅X₄ {O(n)}
(g₁₁,f45), X₄: 8⋅X₄ {O(n)}
(g₁₁,f45), X₅: 8⋅X₄ {O(n)}
(g₁₁,f45), X₆: 8⋅X₄ {O(n)}
(g₁₁,f45), X₇: 8⋅X₇ {O(n)}
(g₁₁,f45), X₈: 8⋅X₈ {O(n)}
(g₁₁,f45), X₉: 8⋅X₉ {O(n)}
(g₁₄,f55), X₄: 32⋅X₄ {O(n)}
(g₁₄,f55), X₈: 32⋅X₈ {O(n)}
(g₁₄,f55), X₉: 32⋅X₉ {O(n)}
(g₃₂,f65), X₄: 32⋅X₄ {O(n)}
(g₃₂,f65), X₈: 0 {O(1)}
(g₃₂,f65), X₉: 32⋅X₉ {O(n)}
(g₃₄,f55), X₀: 16⋅X₄ {O(n)}
(g₃₄,f55), X₃: 16⋅X₄ {O(n)}
(g₃₄,f55), X₄: 16⋅X₄ {O(n)}
(g₃₄,f55), X₅: 16⋅X₄ {O(n)}
(g₃₄,f55), X₆: 16⋅X₄ {O(n)}
(g₃₄,f55), X₇: 0 {O(1)}
(g₃₄,f55), X₈: 16⋅X₈ {O(n)}
(g₃₄,f55), X₉: 16⋅X₉ {O(n)}
(g₃₆,f45), X₀: 0 {O(1)}
(g₃₆,f45), X₃: 8⋅X₄ {O(n)}
(g₃₆,f45), X₄: 8⋅X₄ {O(n)}
(g₃₆,f45), X₅: 8⋅X₄ {O(n)}
(g₃₆,f45), X₆: 8⋅X₄ {O(n)}
(g₃₆,f45), X₇: 8⋅X₇ {O(n)}
(g₃₆,f45), X₈: 8⋅X₈ {O(n)}
(g₃₆,f45), X₉: 8⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₃: 4⋅X₄ {O(n)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₅: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f55]

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

new bound:

32⋅X₄ {O(n)}

PLRF:

• f55: 2⋅X₅-2⋅X₇

Use expected size bounds for entry point (g₃₄:f45→[t₃₅:1:f55],f55)
Use expected size bounds for entry point (g₃₄:f45→[t₃₅:1:f55],f55)
Use classical time bound for entry point (g₃₄:f45→[t₃₅:1:f55],f55)

Run classical analysis on SCC: [f65]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: 4⋅X₄ {O(n)}
g₈: 8⋅X₄ {O(n)}
g₁₁: 16⋅X₄ {O(n)}
g₁₄: 32⋅X₄ {O(n)}
g₁₇: inf {Infinity}
g₂₀: inf {Infinity}
g₂₃: inf {Infinity}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₃: 2⋅X₄ {O(n)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₅: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₈,f37), X₀: 0 {O(1)}
(g₈,f37), X₃: 4⋅X₄ {O(n)}
(g₈,f37), X₄: 8⋅X₄ {O(n)}
(g₈,f37), X₅: 4⋅X₄ {O(n)}
(g₈,f37), X₆: 8⋅X₄ {O(n)}
(g₈,f37), X₇: 8⋅X₇ {O(n)}
(g₈,f37), X₈: 8⋅X₈ {O(n)}
(g₈,f37), X₉: 8⋅X₉ {O(n)}
(g₁₁,f45), X₀: 16⋅X₄ {O(n)}
(g₁₁,f45), X₃: 8⋅X₄ {O(n)}
(g₁₁,f45), X₄: 8⋅X₄ {O(n)}
(g₁₁,f45), X₅: 8⋅X₄ {O(n)}
(g₁₁,f45), X₆: 8⋅X₄ {O(n)}
(g₁₁,f45), X₇: 8⋅X₇ {O(n)}
(g₁₁,f45), X₈: 8⋅X₈ {O(n)}
(g₁₁,f45), X₉: 8⋅X₉ {O(n)}
(g₁₄,f55), X₀: 16⋅X₄ {O(n)}
(g₁₄,f55), X₃: 16⋅X₄ {O(n)}
(g₁₄,f55), X₄: 32⋅X₄ {O(n)}
(g₁₄,f55), X₅: 16⋅X₄ {O(n)}
(g₁₄,f55), X₆: 16⋅X₄ {O(n)}
(g₁₄,f55), X₇: 32⋅X₄ {O(n)}
(g₁₄,f55), X₈: 32⋅X₈ {O(n)}
(g₁₄,f55), X₉: 32⋅X₉ {O(n)}
(g₁₇,f65), X₄: 64⋅X₄ {O(n)}
(g₁₇,f65), X₉: 64⋅X₉ {O(n)}
(g₃₀,f75), X₄: 64⋅X₄ {O(n)}
(g₃₀,f75), X₉: 0 {O(1)}
(g₃₂,f65), X₀: 32⋅X₄ {O(n)}
(g₃₂,f65), X₃: 32⋅X₄ {O(n)}
(g₃₂,f65), X₄: 32⋅X₄ {O(n)}
(g₃₂,f65), X₅: 32⋅X₄ {O(n)}
(g₃₂,f65), X₆: 32⋅X₄ {O(n)}
(g₃₂,f65), X₇: 32⋅X₄ {O(n)}
(g₃₂,f65), X₈: 0 {O(1)}
(g₃₂,f65), X₉: 32⋅X₉ {O(n)}
(g₃₄,f55), X₀: 16⋅X₄ {O(n)}
(g₃₄,f55), X₃: 16⋅X₄ {O(n)}
(g₃₄,f55), X₄: 16⋅X₄ {O(n)}
(g₃₄,f55), X₅: 16⋅X₄ {O(n)}
(g₃₄,f55), X₆: 16⋅X₄ {O(n)}
(g₃₄,f55), X₇: 0 {O(1)}
(g₃₄,f55), X₈: 16⋅X₈ {O(n)}
(g₃₄,f55), X₉: 16⋅X₉ {O(n)}
(g₃₆,f45), X₀: 0 {O(1)}
(g₃₆,f45), X₃: 8⋅X₄ {O(n)}
(g₃₆,f45), X₄: 8⋅X₄ {O(n)}
(g₃₆,f45), X₅: 8⋅X₄ {O(n)}
(g₃₆,f45), X₆: 8⋅X₄ {O(n)}
(g₃₆,f45), X₇: 8⋅X₇ {O(n)}
(g₃₆,f45), X₈: 8⋅X₈ {O(n)}
(g₃₆,f45), X₉: 8⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₃: 4⋅X₄ {O(n)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₅: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f65]

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

new bound:

64⋅X₄ {O(n)}

PLRF:

• f65: 2⋅X₅-2⋅X₈

Use expected size bounds for entry point (g₃₂:f55→[t₃₃:1:f65],f65)
Use expected size bounds for entry point (g₃₂:f55→[t₃₃:1:f65],f65)
Use classical time bound for entry point (g₃₂:f55→[t₃₃:1:f65],f65)

Run classical analysis on SCC: [f75]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: 4⋅X₄ {O(n)}
g₈: 8⋅X₄ {O(n)}
g₁₁: 16⋅X₄ {O(n)}
g₁₄: 32⋅X₄ {O(n)}
g₁₇: 64⋅X₄ {O(n)}
g₂₀: inf {Infinity}
g₂₃: inf {Infinity}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₃: 2⋅X₄ {O(n)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₅: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₈,f37), X₀: 0 {O(1)}
(g₈,f37), X₃: 4⋅X₄ {O(n)}
(g₈,f37), X₄: 8⋅X₄ {O(n)}
(g₈,f37), X₅: 4⋅X₄ {O(n)}
(g₈,f37), X₆: 8⋅X₄ {O(n)}
(g₈,f37), X₇: 8⋅X₇ {O(n)}
(g₈,f37), X₈: 8⋅X₈ {O(n)}
(g₈,f37), X₉: 8⋅X₉ {O(n)}
(g₁₁,f45), X₀: 16⋅X₄ {O(n)}
(g₁₁,f45), X₃: 8⋅X₄ {O(n)}
(g₁₁,f45), X₄: 8⋅X₄ {O(n)}
(g₁₁,f45), X₅: 8⋅X₄ {O(n)}
(g₁₁,f45), X₆: 8⋅X₄ {O(n)}
(g₁₁,f45), X₇: 8⋅X₇ {O(n)}
(g₁₁,f45), X₈: 8⋅X₈ {O(n)}
(g₁₁,f45), X₉: 8⋅X₉ {O(n)}
(g₁₄,f55), X₀: 16⋅X₄ {O(n)}
(g₁₄,f55), X₃: 16⋅X₄ {O(n)}
(g₁₄,f55), X₄: 32⋅X₄ {O(n)}
(g₁₄,f55), X₅: 16⋅X₄ {O(n)}
(g₁₄,f55), X₆: 16⋅X₄ {O(n)}
(g₁₄,f55), X₇: 32⋅X₄ {O(n)}
(g₁₄,f55), X₈: 32⋅X₈ {O(n)}
(g₁₄,f55), X₉: 32⋅X₉ {O(n)}
(g₁₇,f65), X₀: 32⋅X₄ {O(n)}
(g₁₇,f65), X₃: 32⋅X₄ {O(n)}
(g₁₇,f65), X₄: 64⋅X₄ {O(n)}
(g₁₇,f65), X₅: 32⋅X₄ {O(n)}
(g₁₇,f65), X₆: 32⋅X₄ {O(n)}
(g₁₇,f65), X₇: 32⋅X₄ {O(n)}
(g₁₇,f65), X₈: 64⋅X₄ {O(n)}
(g₁₇,f65), X₉: 64⋅X₉ {O(n)}
(g₂₀,f75), X₄: 128⋅X₄ {O(n)}
(g₂₈,f83), X₀: 0 {O(1)}
(g₂₈,f83), X₄: 128⋅X₄ {O(n)}
(g₃₀,f75), X₀: 64⋅X₄ {O(n)}
(g₃₀,f75), X₃: 64⋅X₄ {O(n)}
(g₃₀,f75), X₄: 64⋅X₄ {O(n)}
(g₃₀,f75), X₅: 64⋅X₄ {O(n)}
(g₃₀,f75), X₆: 64⋅X₄ {O(n)}
(g₃₀,f75), X₇: 64⋅X₄ {O(n)}
(g₃₀,f75), X₈: 64⋅X₄ {O(n)}
(g₃₀,f75), X₉: 0 {O(1)}
(g₃₂,f65), X₀: 32⋅X₄ {O(n)}
(g₃₂,f65), X₃: 32⋅X₄ {O(n)}
(g₃₂,f65), X₄: 32⋅X₄ {O(n)}
(g₃₂,f65), X₅: 32⋅X₄ {O(n)}
(g₃₂,f65), X₆: 32⋅X₄ {O(n)}
(g₃₂,f65), X₇: 32⋅X₄ {O(n)}
(g₃₂,f65), X₈: 0 {O(1)}
(g₃₂,f65), X₉: 32⋅X₉ {O(n)}
(g₃₄,f55), X₀: 16⋅X₄ {O(n)}
(g₃₄,f55), X₃: 16⋅X₄ {O(n)}
(g₃₄,f55), X₄: 16⋅X₄ {O(n)}
(g₃₄,f55), X₅: 16⋅X₄ {O(n)}
(g₃₄,f55), X₆: 16⋅X₄ {O(n)}
(g₃₄,f55), X₇: 0 {O(1)}
(g₃₄,f55), X₈: 16⋅X₈ {O(n)}
(g₃₄,f55), X₉: 16⋅X₉ {O(n)}
(g₃₆,f45), X₀: 0 {O(1)}
(g₃₆,f45), X₃: 8⋅X₄ {O(n)}
(g₃₆,f45), X₄: 8⋅X₄ {O(n)}
(g₃₆,f45), X₅: 8⋅X₄ {O(n)}
(g₃₆,f45), X₆: 8⋅X₄ {O(n)}
(g₃₆,f45), X₇: 8⋅X₇ {O(n)}
(g₃₆,f45), X₈: 8⋅X₈ {O(n)}
(g₃₆,f45), X₉: 8⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₃: 4⋅X₄ {O(n)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₅: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f75]

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

new bound:

128⋅X₄ {O(n)}

PLRF:

• f75: 2⋅X₆-2⋅X₉

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

Run classical analysis on SCC: [f83]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: 4⋅X₄ {O(n)}
g₈: 8⋅X₄ {O(n)}
g₁₁: 16⋅X₄ {O(n)}
g₁₄: 32⋅X₄ {O(n)}
g₁₇: 64⋅X₄ {O(n)}
g₂₀: 128⋅X₄ {O(n)}
g₂₃: inf {Infinity}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₃: 2⋅X₄ {O(n)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₅: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₈,f37), X₀: 0 {O(1)}
(g₈,f37), X₃: 4⋅X₄ {O(n)}
(g₈,f37), X₄: 8⋅X₄ {O(n)}
(g₈,f37), X₅: 4⋅X₄ {O(n)}
(g₈,f37), X₆: 8⋅X₄ {O(n)}
(g₈,f37), X₇: 8⋅X₇ {O(n)}
(g₈,f37), X₈: 8⋅X₈ {O(n)}
(g₈,f37), X₉: 8⋅X₉ {O(n)}
(g₁₁,f45), X₀: 16⋅X₄ {O(n)}
(g₁₁,f45), X₃: 8⋅X₄ {O(n)}
(g₁₁,f45), X₄: 8⋅X₄ {O(n)}
(g₁₁,f45), X₅: 8⋅X₄ {O(n)}
(g₁₁,f45), X₆: 8⋅X₄ {O(n)}
(g₁₁,f45), X₇: 8⋅X₇ {O(n)}
(g₁₁,f45), X₈: 8⋅X₈ {O(n)}
(g₁₁,f45), X₉: 8⋅X₉ {O(n)}
(g₁₄,f55), X₀: 16⋅X₄ {O(n)}
(g₁₄,f55), X₃: 16⋅X₄ {O(n)}
(g₁₄,f55), X₄: 32⋅X₄ {O(n)}
(g₁₄,f55), X₅: 16⋅X₄ {O(n)}
(g₁₄,f55), X₆: 16⋅X₄ {O(n)}
(g₁₄,f55), X₇: 32⋅X₄ {O(n)}
(g₁₄,f55), X₈: 32⋅X₈ {O(n)}
(g₁₄,f55), X₉: 32⋅X₉ {O(n)}
(g₁₇,f65), X₀: 32⋅X₄ {O(n)}
(g₁₇,f65), X₃: 32⋅X₄ {O(n)}
(g₁₇,f65), X₄: 64⋅X₄ {O(n)}
(g₁₇,f65), X₅: 32⋅X₄ {O(n)}
(g₁₇,f65), X₆: 32⋅X₄ {O(n)}
(g₁₇,f65), X₇: 32⋅X₄ {O(n)}
(g₁₇,f65), X₈: 64⋅X₄ {O(n)}
(g₁₇,f65), X₉: 64⋅X₉ {O(n)}
(g₂₀,f75), X₀: 64⋅X₄ {O(n)}
(g₂₀,f75), X₃: 64⋅X₄ {O(n)}
(g₂₀,f75), X₄: 64⋅X₄ {O(n)}
(g₂₀,f75), X₅: 64⋅X₄ {O(n)}
(g₂₀,f75), X₆: 64⋅X₄ {O(n)}
(g₂₀,f75), X₇: 64⋅X₄ {O(n)}
(g₂₀,f75), X₈: 64⋅X₄ {O(n)}
(g₂₀,f75), X₉: 128⋅X₄ {O(n)}
(g₂₃,f83), X₄: 256⋅X₄ {O(n)}
(g₂₆,f93), X₄: 256⋅X₄ {O(n)}
(g₂₈,f83), X₀: 0 {O(1)}
(g₂₈,f83), X₃: 128⋅X₄ {O(n)}
(g₂₈,f83), X₄: 128⋅X₄ {O(n)}
(g₂₈,f83), X₅: 128⋅X₄ {O(n)}
(g₂₈,f83), X₆: 128⋅X₄ {O(n)}
(g₂₈,f83), X₇: 128⋅X₄ {O(n)}
(g₂₈,f83), X₈: 128⋅X₄ {O(n)}
(g₂₈,f83), X₉: 128⋅X₄ {O(n)}
(g₃₀,f75), X₀: 64⋅X₄ {O(n)}
(g₃₀,f75), X₃: 64⋅X₄ {O(n)}
(g₃₀,f75), X₄: 64⋅X₄ {O(n)}
(g₃₀,f75), X₅: 64⋅X₄ {O(n)}
(g₃₀,f75), X₆: 64⋅X₄ {O(n)}
(g₃₀,f75), X₇: 64⋅X₄ {O(n)}
(g₃₀,f75), X₈: 64⋅X₄ {O(n)}
(g₃₀,f75), X₉: 0 {O(1)}
(g₃₂,f65), X₀: 32⋅X₄ {O(n)}
(g₃₂,f65), X₃: 32⋅X₄ {O(n)}
(g₃₂,f65), X₄: 32⋅X₄ {O(n)}
(g₃₂,f65), X₅: 32⋅X₄ {O(n)}
(g₃₂,f65), X₆: 32⋅X₄ {O(n)}
(g₃₂,f65), X₇: 32⋅X₄ {O(n)}
(g₃₂,f65), X₈: 0 {O(1)}
(g₃₂,f65), X₉: 32⋅X₉ {O(n)}
(g₃₄,f55), X₀: 16⋅X₄ {O(n)}
(g₃₄,f55), X₃: 16⋅X₄ {O(n)}
(g₃₄,f55), X₄: 16⋅X₄ {O(n)}
(g₃₄,f55), X₅: 16⋅X₄ {O(n)}
(g₃₄,f55), X₆: 16⋅X₄ {O(n)}
(g₃₄,f55), X₇: 0 {O(1)}
(g₃₄,f55), X₈: 16⋅X₈ {O(n)}
(g₃₄,f55), X₉: 16⋅X₉ {O(n)}
(g₃₆,f45), X₀: 0 {O(1)}
(g₃₆,f45), X₃: 8⋅X₄ {O(n)}
(g₃₆,f45), X₄: 8⋅X₄ {O(n)}
(g₃₆,f45), X₅: 8⋅X₄ {O(n)}
(g₃₆,f45), X₆: 8⋅X₄ {O(n)}
(g₃₆,f45), X₇: 8⋅X₇ {O(n)}
(g₃₆,f45), X₈: 8⋅X₈ {O(n)}
(g₃₆,f45), X₉: 8⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₃: 4⋅X₄ {O(n)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₅: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f83]

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

new bound:

256⋅X₄ {O(n)}

PLRF:

• f83: 2⋅X₈-2⋅X₀

Use expected size bounds for entry point (g₂₈:f75→[t₂₉:1:f83],f83)
Use expected size bounds for entry point (g₂₈:f75→[t₂₉:1:f83],f83)
Use classical time bound for entry point (g₂₈:f75→[t₂₉:1:f83],f83)

Run classical analysis on SCC: [f93]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:510⋅X₄+9 {O(n)}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: 4⋅X₄ {O(n)}
g₈: 8⋅X₄ {O(n)}
g₁₁: 16⋅X₄ {O(n)}
g₁₄: 32⋅X₄ {O(n)}
g₁₇: 64⋅X₄ {O(n)}
g₂₀: 128⋅X₄ {O(n)}
g₂₃: 256⋅X₄ {O(n)}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
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}
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₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₃: 2⋅X₄ {O(n)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₅: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₈,f37), X₀: 0 {O(1)}
(g₈,f37), X₃: 4⋅X₄ {O(n)}
(g₈,f37), X₄: 8⋅X₄ {O(n)}
(g₈,f37), X₅: 4⋅X₄ {O(n)}
(g₈,f37), X₆: 8⋅X₄ {O(n)}
(g₈,f37), X₇: 8⋅X₇ {O(n)}
(g₈,f37), X₈: 8⋅X₈ {O(n)}
(g₈,f37), X₉: 8⋅X₉ {O(n)}
(g₁₁,f45), X₀: 16⋅X₄ {O(n)}
(g₁₁,f45), X₃: 8⋅X₄ {O(n)}
(g₁₁,f45), X₄: 8⋅X₄ {O(n)}
(g₁₁,f45), X₅: 8⋅X₄ {O(n)}
(g₁₁,f45), X₆: 8⋅X₄ {O(n)}
(g₁₁,f45), X₇: 8⋅X₇ {O(n)}
(g₁₁,f45), X₈: 8⋅X₈ {O(n)}
(g₁₁,f45), X₉: 8⋅X₉ {O(n)}
(g₁₄,f55), X₀: 16⋅X₄ {O(n)}
(g₁₄,f55), X₃: 16⋅X₄ {O(n)}
(g₁₄,f55), X₄: 32⋅X₄ {O(n)}
(g₁₄,f55), X₅: 16⋅X₄ {O(n)}
(g₁₄,f55), X₆: 16⋅X₄ {O(n)}
(g₁₄,f55), X₇: 32⋅X₄ {O(n)}
(g₁₄,f55), X₈: 32⋅X₈ {O(n)}
(g₁₄,f55), X₉: 32⋅X₉ {O(n)}
(g₁₇,f65), X₀: 32⋅X₄ {O(n)}
(g₁₇,f65), X₃: 32⋅X₄ {O(n)}
(g₁₇,f65), X₄: 64⋅X₄ {O(n)}
(g₁₇,f65), X₅: 32⋅X₄ {O(n)}
(g₁₇,f65), X₆: 32⋅X₄ {O(n)}
(g₁₇,f65), X₇: 32⋅X₄ {O(n)}
(g₁₇,f65), X₈: 64⋅X₄ {O(n)}
(g₁₇,f65), X₉: 64⋅X₉ {O(n)}
(g₂₀,f75), X₀: 64⋅X₄ {O(n)}
(g₂₀,f75), X₃: 64⋅X₄ {O(n)}
(g₂₀,f75), X₄: 64⋅X₄ {O(n)}
(g₂₀,f75), X₅: 64⋅X₄ {O(n)}
(g₂₀,f75), X₆: 64⋅X₄ {O(n)}
(g₂₀,f75), X₇: 64⋅X₄ {O(n)}
(g₂₀,f75), X₈: 64⋅X₄ {O(n)}
(g₂₀,f75), X₉: 128⋅X₄ {O(n)}
(g₂₃,f83), X₀: 256⋅X₄ {O(n)}
(g₂₃,f83), X₃: 128⋅X₄ {O(n)}
(g₂₃,f83), X₄: 256⋅X₄ {O(n)}
(g₂₃,f83), X₅: 128⋅X₄ {O(n)}
(g₂₃,f83), X₆: 128⋅X₄ {O(n)}
(g₂₃,f83), X₇: 128⋅X₄ {O(n)}
(g₂₃,f83), X₈: 128⋅X₄ {O(n)}
(g₂₃,f83), X₉: 128⋅X₄ {O(n)}
(g₂₆,f93), X₀: 256⋅X₄ {O(n)}
(g₂₆,f93), X₃: 256⋅X₄ {O(n)}
(g₂₆,f93), X₄: 256⋅X₄ {O(n)}
(g₂₆,f93), X₅: 256⋅X₄ {O(n)}
(g₂₆,f93), X₆: 256⋅X₄ {O(n)}
(g₂₆,f93), X₇: 256⋅X₄ {O(n)}
(g₂₆,f93), X₈: 256⋅X₄ {O(n)}
(g₂₆,f93), X₉: 256⋅X₄ {O(n)}
(g₂₈,f83), X₀: 0 {O(1)}
(g₂₈,f83), X₃: 128⋅X₄ {O(n)}
(g₂₈,f83), X₄: 128⋅X₄ {O(n)}
(g₂₈,f83), X₅: 128⋅X₄ {O(n)}
(g₂₈,f83), X₆: 128⋅X₄ {O(n)}
(g₂₈,f83), X₇: 128⋅X₄ {O(n)}
(g₂₈,f83), X₈: 128⋅X₄ {O(n)}
(g₂₈,f83), X₉: 128⋅X₄ {O(n)}
(g₃₀,f75), X₀: 64⋅X₄ {O(n)}
(g₃₀,f75), X₃: 64⋅X₄ {O(n)}
(g₃₀,f75), X₄: 64⋅X₄ {O(n)}
(g₃₀,f75), X₅: 64⋅X₄ {O(n)}
(g₃₀,f75), X₆: 64⋅X₄ {O(n)}
(g₃₀,f75), X₇: 64⋅X₄ {O(n)}
(g₃₀,f75), X₈: 64⋅X₄ {O(n)}
(g₃₀,f75), X₉: 0 {O(1)}
(g₃₂,f65), X₀: 32⋅X₄ {O(n)}
(g₃₂,f65), X₃: 32⋅X₄ {O(n)}
(g₃₂,f65), X₄: 32⋅X₄ {O(n)}
(g₃₂,f65), X₅: 32⋅X₄ {O(n)}
(g₃₂,f65), X₆: 32⋅X₄ {O(n)}
(g₃₂,f65), X₇: 32⋅X₄ {O(n)}
(g₃₂,f65), X₈: 0 {O(1)}
(g₃₂,f65), X₉: 32⋅X₉ {O(n)}
(g₃₄,f55), X₀: 16⋅X₄ {O(n)}
(g₃₄,f55), X₃: 16⋅X₄ {O(n)}
(g₃₄,f55), X₄: 16⋅X₄ {O(n)}
(g₃₄,f55), X₅: 16⋅X₄ {O(n)}
(g₃₄,f55), X₆: 16⋅X₄ {O(n)}
(g₃₄,f55), X₇: 0 {O(1)}
(g₃₄,f55), X₈: 16⋅X₈ {O(n)}
(g₃₄,f55), X₉: 16⋅X₉ {O(n)}
(g₃₆,f45), X₀: 0 {O(1)}
(g₃₆,f45), X₃: 8⋅X₄ {O(n)}
(g₃₆,f45), X₄: 8⋅X₄ {O(n)}
(g₃₆,f45), X₅: 8⋅X₄ {O(n)}
(g₃₆,f45), X₆: 8⋅X₄ {O(n)}
(g₃₆,f45), X₇: 8⋅X₇ {O(n)}
(g₃₆,f45), X₈: 8⋅X₈ {O(n)}
(g₃₆,f45), X₉: 8⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₃: 4⋅X₄ {O(n)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₅: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}

Run probabilistic analysis on SCC: [f93]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:510⋅X₄+9 {O(n)}
g₀: 1 {O(1)}
g₂: 2⋅X₄ {O(n)}
g₅: 4⋅X₄ {O(n)}
g₈: 8⋅X₄ {O(n)}
g₁₁: 16⋅X₄ {O(n)}
g₁₄: 32⋅X₄ {O(n)}
g₁₇: 64⋅X₄ {O(n)}
g₂₀: 128⋅X₄ {O(n)}
g₂₃: 256⋅X₄ {O(n)}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
g₄₀: 1 {O(1)}

Costbounds

Overall costbound: 1020⋅X₄+9 {O(n)}
g₀: 1 {O(1)}
g₂: 4⋅X₄ {O(n)}
g₅: 8⋅X₄ {O(n)}
g₈: 16⋅X₄ {O(n)}
g₁₁: 32⋅X₄ {O(n)}
g₁₄: 64⋅X₄ {O(n)}
g₁₇: 128⋅X₄ {O(n)}
g₂₀: 256⋅X₄ {O(n)}
g₂₃: 512⋅X₄ {O(n)}
g₂₆: 1 {O(1)}
g₂₈: 1 {O(1)}
g₃₀: 1 {O(1)}
g₃₂: 1 {O(1)}
g₃₄: 1 {O(1)}
g₃₆: 1 {O(1)}
g₃₈: 1 {O(1)}
g₄₀: 1 {O(1)}

Sizebounds

(g₀,f17), X₀: 0 {O(1)}
(g₀,f17), X₃: 0 {O(1)}
(g₀,f17), X₄: X₄ {O(n)}
(g₀,f17), X₅: X₅ {O(n)}
(g₀,f17), X₆: X₆ {O(n)}
(g₀,f17), X₇: X₇ {O(n)}
(g₀,f17), X₈: X₈ {O(n)}
(g₀,f17), X₉: X₉ {O(n)}
(g₂,f17), X₀: 0 {O(1)}
(g₂,f17), X₃: 2⋅X₄ {O(n)}
(g₂,f17), X₄: X₄ {O(n)}
(g₂,f17), X₅: X₅ {O(n)}
(g₂,f17), X₆: X₆ {O(n)}
(g₂,f17), X₇: X₇ {O(n)}
(g₂,f17), X₈: X₈ {O(n)}
(g₂,f17), X₉: X₉ {O(n)}
(g₅,f27), X₀: 0 {O(1)}
(g₅,f27), X₃: 2⋅X₄ {O(n)}
(g₅,f27), X₄: 4⋅X₄ {O(n)}
(g₅,f27), X₅: 4⋅X₄ {O(n)}
(g₅,f27), X₆: 4⋅X₆ {O(n)}
(g₅,f27), X₇: 4⋅X₇ {O(n)}
(g₅,f27), X₈: 4⋅X₈ {O(n)}
(g₅,f27), X₉: 4⋅X₉ {O(n)}
(g₈,f37), X₀: 0 {O(1)}
(g₈,f37), X₃: 4⋅X₄ {O(n)}
(g₈,f37), X₄: 8⋅X₄ {O(n)}
(g₈,f37), X₅: 4⋅X₄ {O(n)}
(g₈,f37), X₆: 8⋅X₄ {O(n)}
(g₈,f37), X₇: 8⋅X₇ {O(n)}
(g₈,f37), X₈: 8⋅X₈ {O(n)}
(g₈,f37), X₉: 8⋅X₉ {O(n)}
(g₁₁,f45), X₀: 16⋅X₄ {O(n)}
(g₁₁,f45), X₃: 8⋅X₄ {O(n)}
(g₁₁,f45), X₄: 8⋅X₄ {O(n)}
(g₁₁,f45), X₅: 8⋅X₄ {O(n)}
(g₁₁,f45), X₆: 8⋅X₄ {O(n)}
(g₁₁,f45), X₇: 8⋅X₇ {O(n)}
(g₁₁,f45), X₈: 8⋅X₈ {O(n)}
(g₁₁,f45), X₉: 8⋅X₉ {O(n)}
(g₁₄,f55), X₀: 16⋅X₄ {O(n)}
(g₁₄,f55), X₃: 16⋅X₄ {O(n)}
(g₁₄,f55), X₄: 32⋅X₄ {O(n)}
(g₁₄,f55), X₅: 16⋅X₄ {O(n)}
(g₁₄,f55), X₆: 16⋅X₄ {O(n)}
(g₁₄,f55), X₇: 32⋅X₄ {O(n)}
(g₁₄,f55), X₈: 32⋅X₈ {O(n)}
(g₁₄,f55), X₉: 32⋅X₉ {O(n)}
(g₁₇,f65), X₀: 32⋅X₄ {O(n)}
(g₁₇,f65), X₃: 32⋅X₄ {O(n)}
(g₁₇,f65), X₄: 64⋅X₄ {O(n)}
(g₁₇,f65), X₅: 32⋅X₄ {O(n)}
(g₁₇,f65), X₆: 32⋅X₄ {O(n)}
(g₁₇,f65), X₇: 32⋅X₄ {O(n)}
(g₁₇,f65), X₈: 64⋅X₄ {O(n)}
(g₁₇,f65), X₉: 64⋅X₉ {O(n)}
(g₂₀,f75), X₀: 64⋅X₄ {O(n)}
(g₂₀,f75), X₃: 64⋅X₄ {O(n)}
(g₂₀,f75), X₄: 64⋅X₄ {O(n)}
(g₂₀,f75), X₅: 64⋅X₄ {O(n)}
(g₂₀,f75), X₆: 64⋅X₄ {O(n)}
(g₂₀,f75), X₇: 64⋅X₄ {O(n)}
(g₂₀,f75), X₈: 64⋅X₄ {O(n)}
(g₂₀,f75), X₉: 128⋅X₄ {O(n)}
(g₂₃,f83), X₀: 256⋅X₄ {O(n)}
(g₂₃,f83), X₃: 128⋅X₄ {O(n)}
(g₂₃,f83), X₄: 256⋅X₄ {O(n)}
(g₂₃,f83), X₅: 128⋅X₄ {O(n)}
(g₂₃,f83), X₆: 128⋅X₄ {O(n)}
(g₂₃,f83), X₇: 128⋅X₄ {O(n)}
(g₂₃,f83), X₈: 128⋅X₄ {O(n)}
(g₂₃,f83), X₉: 128⋅X₄ {O(n)}
(g₂₆,f93), X₀: 256⋅X₄ {O(n)}
(g₂₆,f93), X₃: 256⋅X₄ {O(n)}
(g₂₆,f93), X₄: 256⋅X₄ {O(n)}
(g₂₆,f93), X₅: 256⋅X₄ {O(n)}
(g₂₆,f93), X₆: 256⋅X₄ {O(n)}
(g₂₆,f93), X₇: 256⋅X₄ {O(n)}
(g₂₆,f93), X₈: 256⋅X₄ {O(n)}
(g₂₆,f93), X₉: 256⋅X₄ {O(n)}
(g₂₈,f83), X₀: 0 {O(1)}
(g₂₈,f83), X₃: 128⋅X₄ {O(n)}
(g₂₈,f83), X₄: 128⋅X₄ {O(n)}
(g₂₈,f83), X₅: 128⋅X₄ {O(n)}
(g₂₈,f83), X₆: 128⋅X₄ {O(n)}
(g₂₈,f83), X₇: 128⋅X₄ {O(n)}
(g₂₈,f83), X₈: 128⋅X₄ {O(n)}
(g₂₈,f83), X₉: 128⋅X₄ {O(n)}
(g₃₀,f75), X₀: 64⋅X₄ {O(n)}
(g₃₀,f75), X₃: 64⋅X₄ {O(n)}
(g₃₀,f75), X₄: 64⋅X₄ {O(n)}
(g₃₀,f75), X₅: 64⋅X₄ {O(n)}
(g₃₀,f75), X₆: 64⋅X₄ {O(n)}
(g₃₀,f75), X₇: 64⋅X₄ {O(n)}
(g₃₀,f75), X₈: 64⋅X₄ {O(n)}
(g₃₀,f75), X₉: 0 {O(1)}
(g₃₂,f65), X₀: 32⋅X₄ {O(n)}
(g₃₂,f65), X₃: 32⋅X₄ {O(n)}
(g₃₂,f65), X₄: 32⋅X₄ {O(n)}
(g₃₂,f65), X₅: 32⋅X₄ {O(n)}
(g₃₂,f65), X₆: 32⋅X₄ {O(n)}
(g₃₂,f65), X₇: 32⋅X₄ {O(n)}
(g₃₂,f65), X₈: 0 {O(1)}
(g₃₂,f65), X₉: 32⋅X₉ {O(n)}
(g₃₄,f55), X₀: 16⋅X₄ {O(n)}
(g₃₄,f55), X₃: 16⋅X₄ {O(n)}
(g₃₄,f55), X₄: 16⋅X₄ {O(n)}
(g₃₄,f55), X₅: 16⋅X₄ {O(n)}
(g₃₄,f55), X₆: 16⋅X₄ {O(n)}
(g₃₄,f55), X₇: 0 {O(1)}
(g₃₄,f55), X₈: 16⋅X₈ {O(n)}
(g₃₄,f55), X₉: 16⋅X₉ {O(n)}
(g₃₆,f45), X₀: 0 {O(1)}
(g₃₆,f45), X₃: 8⋅X₄ {O(n)}
(g₃₆,f45), X₄: 8⋅X₄ {O(n)}
(g₃₆,f45), X₅: 8⋅X₄ {O(n)}
(g₃₆,f45), X₆: 8⋅X₄ {O(n)}
(g₃₆,f45), X₇: 8⋅X₇ {O(n)}
(g₃₆,f45), X₈: 8⋅X₈ {O(n)}
(g₃₆,f45), X₉: 8⋅X₉ {O(n)}
(g₃₈,f37), X₀: 0 {O(1)}
(g₃₈,f37), X₃: 4⋅X₄ {O(n)}
(g₃₈,f37), X₄: 4⋅X₄ {O(n)}
(g₃₈,f37), X₅: 4⋅X₄ {O(n)}
(g₃₈,f37), X₆: 0 {O(1)}
(g₃₈,f37), X₇: 4⋅X₇ {O(n)}
(g₃₈,f37), X₈: 4⋅X₈ {O(n)}
(g₃₈,f37), X₉: 4⋅X₉ {O(n)}
(g₄₀,f27), X₀: 0 {O(1)}
(g₄₀,f27), X₃: 2⋅X₄ {O(n)}
(g₄₀,f27), X₄: 2⋅X₄ {O(n)}
(g₄₀,f27), X₅: 0 {O(1)}
(g₄₀,f27), X₆: 2⋅X₆ {O(n)}
(g₄₀,f27), X₇: 2⋅X₇ {O(n)}
(g₄₀,f27), X₈: 2⋅X₈ {O(n)}
(g₄₀,f27), X₉: 2⋅X₉ {O(n)}