knowledge_propagation leads to new time bound 0 {O(1)} for transition t₁₃: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f18(X₀,X₁,X₂,X₃,1+X₄,X₅,X₆,I) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆

knowledge_propagation leads to new time bound X₂+1 {O(n)} for transition t₁₈: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f22_v1(X₀,X₁,X₂,X₃,X₄,X₅,1+X₆,X₇) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃

knowledge_propagation leads to new time bound X₂+1 {O(n)} for transition t₁₉: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f22_v2(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃

knowledge_propagation leads to new time bound X₂+1 {O(n)} for transition t₂₁: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f22_v3(X₀,X₁,X₂,X₃,X₄,X₆,1+X₆,X₇) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃

knowledge_propagation leads to new time bound X₂+1 {O(n)} for transition t₂₂: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f22_v2(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ 1+X₆ ≤ X₃

knowledge_propagation leads to new time bound 0 {O(1)} for transition t₂₄: f22(X₀,X₁,X₂,X₃,X₄,X₅,X₆,X₇) → f18(X₀,X₁,X₂,X₃,1+X₄,X₅,X₆,I) :|: 1 ≤ X₄+X₆ ∧ 1+X₄ ≤ X₆ ∧ 1 ≤ X₆ ∧ 2 ≤ X₁ ∧ 2 ≤ X₁+X₄ ∧ 2+X₄ ≤ X₁ ∧ 2 ≤ X₂ ∧ 2 ≤ X₂+X₄ ∧ 2+X₄ ≤ X₂ ∧ 2 ≤ X₃ ∧ 2 ≤ X₃+X₄ ∧ 2+X₄ ≤ X₃ ∧ 3 ≤ X₁+X₆ ∧ 3 ≤ X₂+X₆ ∧ 3 ≤ X₃+X₆ ∧ 4 ≤ X₁+X₂ ∧ 4 ≤ X₁+X₃ ∧ 4 ≤ X₂+X₃ ∧ X₂ ≤ X₁ ∧ X₃ ≤ X₁ ∧ X₆ ≤ X₁ ∧ X₃ ≤ X₂ ∧ X₆ ≤ X₂ ∧ X₂ ≤ X₃ ∧ X₆ ≤ X₃ ∧ 0 ≤ X₄ ∧ X₃ ≤ X₆

Run classical analysis on SCC: [f34]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:36⋅X₂⋅X₂+40⋅X₂+5 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 16⋅X₂⋅X₂+16⋅X₂ {O(n^2)}
g₉: 20⋅X₂⋅X₂+20⋅X₂ {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
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}

Sizebounds

(g₀,f10), X₁: 0 {O(1)}
(g₀,f10), X₂: X₂ {O(n)}
(g₀,f10), X₃: X₃ {O(n)}
(g₀,f10), X₄: X₄ {O(n)}
(g₀,f10), X₅: X₅ {O(n)}
(g₀,f10), X₆: X₆ {O(n)}
(g₀,f10), X₇: X₇ {O(n)}
(g₂,f10), X₁: X₂ {O(n)}
(g₂,f10), X₂: X₂ {O(n)}
(g₂,f10), X₃: X₃ {O(n)}
(g₂,f10), X₄: X₄ {O(n)}
(g₂,f10), X₅: X₅ {O(n)}
(g₂,f10), X₆: X₆ {O(n)}
(g₂,f10), X₇: X₇ {O(n)}
(g₄,f22), X₁: X₂ {O(n)}
(g₄,f22), X₂: 2⋅X₂ {O(n)}
(g₄,f22), X₃: 2⋅X₂ {O(n)}
(g₄,f22), X₄: 2⋅X₂+1 {O(n)}
(g₄,f22), X₅: 2⋅X₂+1 {O(n)}
(g₄,f22), X₆: 2⋅X₂+3 {O(n)}
(g₆,f22), X₁: X₂ {O(n)}
(g₆,f22), X₂: 4⋅X₂ {O(n)}
(g₆,f22), X₃: 4⋅X₂ {O(n)}
(g₆,f22), X₄: 4⋅X₂+2 {O(n)}
(g₆,f22), X₅: 96⋅X₂⋅X₂+120⋅X₂+40 {O(n^2)}
(g₆,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₉,f22), X₁: X₂ {O(n)}
(g₉,f22), X₂: 4⋅X₂ {O(n)}
(g₉,f22), X₃: 4⋅X₂ {O(n)}
(g₉,f22), X₄: 4⋅X₂+2 {O(n)}
(g₉,f22), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₉,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₂,f18), X₁: X₂ {O(n)}
(g₁₂,f18), X₂: 2⋅X₂ {O(n)}
(g₁₂,f18), X₃: 2⋅X₂ {O(n)}
(g₁₂,f18), X₄: 2⋅X₂+1 {O(n)}
(g₁₂,f18), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₁₂,f18), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₄,f34), X₁: 2⋅X₂ {O(n)}
(g₁₄,f34), X₂: 4⋅X₂ {O(n)}
(g₁₄,f34), X₃: 4⋅X₂ {O(n)}
(g₁₄,f34), X₄: 0 {O(1)}
(g₁₄,f34), X₅: 96⋅X₂⋅X₂+118⋅X₂+2⋅X₅+39 {O(n^2)}
(g₁₄,f34), X₆: 24⋅X₂⋅X₂+2⋅X₆+28⋅X₂+8 {O(n^2)}
(g₁₆,f18), X₁: X₂ {O(n)}
(g₁₆,f18), X₂: 2⋅X₂ {O(n)}
(g₁₆,f18), X₃: 2⋅X₂ {O(n)}
(g₁₆,f18), X₄: 0 {O(1)}
(g₁₆,f18), X₅: 2⋅X₅ {O(n)}
(g₁₆,f18), X₆: 2⋅X₆ {O(n)}
(g₁₆,f18), X₇: 2⋅X₇ {O(n)}

Run probabilistic analysis on SCC: [f34]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:36⋅X₂⋅X₂+40⋅X₂+5 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 16⋅X₂⋅X₂+16⋅X₂ {O(n^2)}
g₉: 20⋅X₂⋅X₂+20⋅X₂ {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}

Costbounds

Overall costbound: 72⋅X₂⋅X₂+76⋅X₂+5 {O(n^2)}
g₀: 1 {O(1)}
g₂: X₂ {O(n)}
g₄: X₂+1 {O(n)}
g₆: 32⋅X₂⋅X₂+32⋅X₂ {O(n^2)}
g₉: 40⋅X₂⋅X₂+40⋅X₂ {O(n^2)}
g₁₂: 2⋅X₂+1 {O(n)}
g₁₄: 1 {O(1)}
g₁₆: 1 {O(1)}

Sizebounds

(g₀,f10), X₁: 0 {O(1)}
(g₀,f10), X₂: X₂ {O(n)}
(g₀,f10), X₃: X₃ {O(n)}
(g₀,f10), X₄: X₄ {O(n)}
(g₀,f10), X₅: X₅ {O(n)}
(g₀,f10), X₆: X₆ {O(n)}
(g₀,f10), X₇: X₇ {O(n)}
(g₂,f10), X₁: X₂ {O(n)}
(g₂,f10), X₂: X₂ {O(n)}
(g₂,f10), X₃: X₃ {O(n)}
(g₂,f10), X₄: X₄ {O(n)}
(g₂,f10), X₅: X₅ {O(n)}
(g₂,f10), X₆: X₆ {O(n)}
(g₂,f10), X₇: X₇ {O(n)}
(g₄,f22), X₁: X₂ {O(n)}
(g₄,f22), X₂: 2⋅X₂ {O(n)}
(g₄,f22), X₃: 2⋅X₂ {O(n)}
(g₄,f22), X₄: 2⋅X₂+1 {O(n)}
(g₄,f22), X₅: 2⋅X₂+1 {O(n)}
(g₄,f22), X₆: 2⋅X₂+3 {O(n)}
(g₆,f22), X₁: X₂ {O(n)}
(g₆,f22), X₂: 4⋅X₂ {O(n)}
(g₆,f22), X₃: 4⋅X₂ {O(n)}
(g₆,f22), X₄: 4⋅X₂+2 {O(n)}
(g₆,f22), X₅: 96⋅X₂⋅X₂+120⋅X₂+40 {O(n^2)}
(g₆,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₉,f22), X₁: X₂ {O(n)}
(g₉,f22), X₂: 4⋅X₂ {O(n)}
(g₉,f22), X₃: 4⋅X₂ {O(n)}
(g₉,f22), X₄: 4⋅X₂+2 {O(n)}
(g₉,f22), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₉,f22), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₂,f18), X₁: X₂ {O(n)}
(g₁₂,f18), X₂: 2⋅X₂ {O(n)}
(g₁₂,f18), X₃: 2⋅X₂ {O(n)}
(g₁₂,f18), X₄: 2⋅X₂+1 {O(n)}
(g₁₂,f18), X₅: 96⋅X₂⋅X₂+118⋅X₂+39 {O(n^2)}
(g₁₂,f18), X₆: 24⋅X₂⋅X₂+28⋅X₂+8 {O(n^2)}
(g₁₄,f34), X₁: 2⋅X₂ {O(n)}
(g₁₄,f34), X₂: 4⋅X₂ {O(n)}
(g₁₄,f34), X₃: 4⋅X₂ {O(n)}
(g₁₄,f34), X₄: 0 {O(1)}
(g₁₄,f34), X₅: 96⋅X₂⋅X₂+118⋅X₂+2⋅X₅+39 {O(n^2)}
(g₁₄,f34), X₆: 24⋅X₂⋅X₂+2⋅X₆+28⋅X₂+8 {O(n^2)}
(g₁₆,f18), X₁: X₂ {O(n)}
(g₁₆,f18), X₂: 2⋅X₂ {O(n)}
(g₁₆,f18), X₃: 2⋅X₂ {O(n)}
(g₁₆,f18), X₄: 0 {O(1)}
(g₁₆,f18), X₅: 2⋅X₅ {O(n)}
(g₁₆,f18), X₆: 2⋅X₆ {O(n)}
(g₁₆,f18), X₇: 2⋅X₇ {O(n)}