Preprocessing

Cut unsatisfiable transition [t₁₇∈g₁₆: evalrealheapsortbb4in→1:evalrealheapsortbb2in; t₂₁∈g₂₀: evalrealheapsortbb4in→1:evalrealheapsortbb2in; t₂₃∈g₂₂: evalrealheapsortbb4in→1:evalrealheapsortbb5in; t₂₇∈g₂₆: evalrealheapsortbb4in→1:evalrealheapsortbb5in; t₃₁∈g₃₀: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₃₃∈g₃₂: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₃₅∈g₃₄: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₃₇∈g₃₆: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₃₉∈g₃₈: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₄₁∈g₄₀: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₄₃∈g₄₂: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₄₅∈g₄₄: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₄₇∈g₄₆: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₄₉∈g₄₈: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₅₁∈g₅₀: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₅₃∈g₅₂: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₅₇∈g₅₆: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₅₉∈g₅₈: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₆₁∈g₆₀: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₆₃∈g₆₂: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₆₅∈g₆₄: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₆₇∈g₆₆: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₆₉∈g₆₈: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₇₁∈g₇₀: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₇₃∈g₇₂: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₇₅∈g₇₄: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₇₇∈g₇₆: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₇₉∈g₇₈: evalrealheapsortbb2in→1:evalrealheapsortbb3in; t₁₀₁∈g₁₀₀: evalrealheapsortbb9in→1:evalrealheapsortbb10in]

Found invariant 0 ≤ X₃ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ 3+X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ 3 ≤ X₀+X₂ ∧ 3+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb9in

Found invariant 0 ≤ X₃ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₁+X₃ ∧ 4 ≤ X₀+X₃ ∧ 4+X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ 4 ≤ X₀+X₂ ∧ 4+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 4 ≤ X₀+X₁ ∧ 4 ≤ X₀ for location evalrealheapsortbb10in

Found invariant 0 ≤ X₃ for location evalrealheapsortreturnin

Found invariant 0 ≤ X₃ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ 3+X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ 3 ≤ X₀+X₂ ∧ 3+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb11in

Found invariant 1 ≤ X₃ ∧ 1 ≤ X₂+X₃ ∧ 1+X₂ ≤ X₃ ∧ 1 ≤ X₁+X₃ ∧ 4 ≤ X₀+X₃ ∧ 3+X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ 3 ≤ X₀+X₂ ∧ 3+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb14in

Found invariant 0 ≤ X₃ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₁+X₃ ∧ 4 ≤ X₀+X₃ ∧ 4+X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ 4 ≤ X₀+X₂ ∧ 4+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 4 ≤ X₀+X₁ ∧ 4 ≤ X₀ for location evalrealheapsortbb12in

Found invariant 0 ≤ X₃ for location evalrealheapsortstop

Found invariant 0 ≤ X₃ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ 3 ≤ X₀+X₂ ∧ 2+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb16in

Found invariant 1 ≤ X₃ ∧ 1 ≤ X₂+X₃ ∧ 1+X₂ ≤ X₃ ∧ 1 ≤ X₁+X₃ ∧ 4 ≤ X₀+X₃ ∧ 3+X₂ ≤ X₀ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ 3 ≤ X₀+X₂ ∧ 3+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb13in

Found invariant X₃ ≤ 0 ∧ 3+X₃ ≤ X₁ ∧ 3+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 3 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ X₁ ≤ X₀ ∧ 3 ≤ X₁ ∧ 6 ≤ X₀+X₁ ∧ X₀ ≤ X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb7in

Found invariant X₃ ≤ 0 ∧ X₃ ≤ 1+X₂ ∧ 1+X₃ ≤ X₁ ∧ 3+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 0 ≤ 1+X₂+X₃ ∧ 1 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ X₂ ≤ X₁ ∧ 1+X₂ ≤ X₀ ∧ 0 ≤ 1+X₂ ∧ 0 ≤ X₁+X₂ ∧ 2 ≤ X₀+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1 ≤ X₁ ∧ 4 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb3in

Found invariant 0 ≤ X₃ ∧ 0 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ 2+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb8in

Found invariant X₃ ≤ 0 ∧ 1+X₃ ≤ X₁ ∧ 3+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 1 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ X₁ ≤ X₀ ∧ 1 ≤ X₁ ∧ 4 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb6in

Found invariant X₃ ≤ 0 ∧ 1+X₃ ≤ X₂ ∧ 1+X₃ ≤ X₁ ∧ 3+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 1 ≤ X₂+X₃ ∧ 1 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ X₂ ≤ X₁ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₂ ∧ 2 ≤ X₁+X₂ ∧ 4 ≤ X₀+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1 ≤ X₁ ∧ 4 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb4in

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

Found invariant X₃ ≤ 0 ∧ X₃ ≤ 1+X₂ ∧ 1+X₃ ≤ X₁ ∧ 3+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 0 ≤ 1+X₂+X₃ ∧ 1 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ X₂ ≤ X₁ ∧ 1+X₂ ≤ X₀ ∧ 0 ≤ 1+X₂ ∧ 0 ≤ X₁+X₂ ∧ 2 ≤ X₀+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1 ≤ X₁ ∧ 4 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb5in

Found invariant 0 ≤ X₃ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₁+X₂ ∧ 3 ≤ X₀+X₂ ∧ 2+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb17in

Found invariant X₃ ≤ 0 ∧ 0 ≤ X₃ for location evalrealheapsortentryin

Found invariant X₃ ≤ 0 ∧ X₃ ≤ 1+X₂ ∧ 1+X₃ ≤ X₁ ∧ 3+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 0 ≤ 1+X₂+X₃ ∧ 1 ≤ X₁+X₃ ∧ 3 ≤ X₀+X₃ ∧ X₂ ≤ X₁ ∧ 1+X₂ ≤ X₀ ∧ 0 ≤ 1+X₂ ∧ 0 ≤ X₁+X₂ ∧ 2 ≤ X₀+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1 ≤ X₁ ∧ 4 ≤ X₀+X₁ ∧ 3 ≤ X₀ for location evalrealheapsortbb2in

Cut unsatisfiable transition [t₈₁∈g₈₀: evalrealheapsortbb2in→1:evalrealheapsortbb3in]

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: evalrealheapsortstart
Program_Vars: X₀, X₁, X₂, X₃
Temp_Vars: E, F, G
Locations: evalrealheapsortbb10in, evalrealheapsortbb11in, evalrealheapsortbb12in, evalrealheapsortbb13in, evalrealheapsortbb14in, evalrealheapsortbb16in, evalrealheapsortbb17in, evalrealheapsortbb18in, evalrealheapsortbb2in, evalrealheapsortbb3in, evalrealheapsortbb4in, evalrealheapsortbb5in, evalrealheapsortbb6in, evalrealheapsortbb7in, evalrealheapsortbb8in, evalrealheapsortbb9in, evalrealheapsortentryin, evalrealheapsortreturnin, evalrealheapsortstart, evalrealheapsortstop
Transitions:
g₀:evalrealheapsortstart(X₀,X₁,X₂,X₃) → t₁:evalrealheapsortentryin(X₀,X₁,X₂,X₃) :|: 0 ≤ X₃ ∧ X₃ ≤ 0
g₂:evalrealheapsortentryin(X₀,X₁,X₂,X₃) → t₃:evalrealheapsortbb6in(X₀,1,X₂,X₃) :|: 3 ≤ X₀ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₄:evalrealheapsortentryin(X₀,X₁,X₂,X₃) → t₅:evalrealheapsortreturnin(X₀,X₁,X₂,X₃) :|: X₀ ≤ 2 ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₆:evalrealheapsortbb6in(X₀,X₁,X₂,X₃) → t₇:evalrealheapsortbb3in(X₀,X₁,X₁,X₃) :|: 1+X₁ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₈:evalrealheapsortbb6in(X₀,X₁,X₂,X₃) → t₉:evalrealheapsortbb7in(X₀,X₁,X₂,X₃) :|: X₀ ≤ X₁ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₁₀:evalrealheapsortbb3in(X₀,X₁,X₂,X₃) → [1/2]:t₁₁:evalrealheapsortbb5in(X₀,X₁,X₂,X₃) :+: [1/2]:t₁₂:evalrealheapsortbb2in(X₀,X₁,X₂,X₃) :|: X₂ ≤ 0 ∧ 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₁₃:evalrealheapsortbb3in(X₀,X₁,X₂,X₃) → [1/2]:t₁₄:evalrealheapsortbb3in(X₀,X₁,X₂,X₃) :+: [1/2]:t₁₅:evalrealheapsortbb4in(X₀,X₁,X₂,X₃) :|: 1 ≤ X₂ ∧ 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₁₈:evalrealheapsortbb4in(X₀,X₁,X₂,X₃) → t₁₉:evalrealheapsortbb2in(X₀,X₁,X₂,X₃) :|: 2⋅E ≤ 1+X₂ ∧ X₂ ≤ 2⋅E ∧ 0 ≤ E ∧ 0 ≤ X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 1 ≤ X₂ ∧ 1 ≤ X₂+X₃ ∧ 1+X₃ ≤ X₂ ∧ 2 ≤ X₁+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4 ≤ X₀+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₂₄:evalrealheapsortbb4in(X₀,X₁,X₂,X₃) → t₂₅:evalrealheapsortbb5in(X₀,X₁,X₂,X₃) :|: 2⋅E ≤ 1+X₂ ∧ X₂ ≤ 2⋅E ∧ 0 ≤ E ∧ 0 ≤ X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 1 ≤ X₂ ∧ 1 ≤ X₂+X₃ ∧ 1+X₃ ≤ X₂ ∧ 2 ≤ X₁+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4 ≤ X₀+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₂₈:evalrealheapsortbb2in(X₀,X₁,X₂,X₃) → t₂₉:evalrealheapsortbb3in(X₀,X₁,-1,X₃) :|: 0 ≤ 1+X₂ ∧ 1+X₂ ≤ 0 ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₅₄:evalrealheapsortbb2in(X₀,X₁,X₂,X₃) → t₅₅:evalrealheapsortbb3in(X₀,X₁,E-1,X₃) :|: 2⋅E ≤ 1+X₂ ∧ 2⋅F ≤ 1+X₂ ∧ 2⋅G ≤ 1+X₂ ∧ X₂ ≤ 2⋅E ∧ 0 ≤ E ∧ X₂ ≤ 2⋅F ∧ 0 ≤ F ∧ X₂ ≤ 2⋅G ∧ 0 ≤ G ∧ 0 ≤ X₂ ∧ 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₈₂:evalrealheapsortbb5in(X₀,X₁,X₂,X₃) → t₈₃:evalrealheapsortbb6in(X₀,1+X₁,X₂,X₃) :|: 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₈₄:evalrealheapsortbb7in(X₀,X₁,X₂,X₃) → t₈₅:evalrealheapsortbb18in(X₀,0,X₂,X₃) :|: 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 3 ≤ X₁ ∧ 3 ≤ X₁+X₃ ∧ 3+X₃ ≤ X₁ ∧ 6 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0
g₈₆:evalrealheapsortbb18in(X₀,X₁,X₂,X₃) → t₈₇:evalrealheapsortbb8in(X₀,X₁,X₂,X₃) :|: 2+X₁ ≤ X₀ ∧ 1+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₃
g₈₈:evalrealheapsortbb18in(X₀,X₁,X₂,X₃) → t₈₉:evalrealheapsortreturnin(X₀,X₁,X₂,X₃) :|: X₀ ≤ 1+X₁ ∧ 1+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₃
g₉₀:evalrealheapsortbb8in(X₀,X₁,X₂,X₃) → t₉₁:evalrealheapsortbb16in(X₀,X₁,0,X₃) :|: 2+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₃
g₉₂:evalrealheapsortbb16in(X₀,X₁,X₂,X₃) → t₉₃:evalrealheapsortbb9in(X₀,X₁,X₂,X₃) :|: 3+X₁+2⋅X₂ ≤ X₀ ∧ 2+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₂ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₉₄:evalrealheapsortbb16in(X₀,X₁,X₂,X₃) → t₉₅:evalrealheapsortbb17in(X₀,X₁,X₂,X₃) :|: X₀ ≤ 2+X₁+2⋅X₂ ∧ 2+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₂ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₉₆:evalrealheapsortbb9in(X₀,X₁,X₂,X₃) → t₉₇:evalrealheapsortbb11in(X₀,X₁,X₂,X₃) :|: X₀ ≤ 3+X₁+2⋅X₂ ∧ 3+X₁+2⋅X₂ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₉₈:evalrealheapsortbb9in(X₀,X₁,X₂,X₃) → t₉₉:evalrealheapsortbb10in(X₀,X₁,X₂,X₃) :|: 4+X₁+2⋅X₂ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₁₀₂:evalrealheapsortbb10in(X₀,X₁,X₂,X₃) → t₁₀₃:evalrealheapsortbb11in(X₀,X₁,X₂,X₃) :|: 4 ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4+X₁ ≤ X₀ ∧ 4 ≤ X₀+X₂ ∧ 4+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₁₀₄:evalrealheapsortbb10in(X₀,X₁,X₂,X₃) → t₁₀₅:evalrealheapsortbb12in(X₀,X₁,X₂,X₃) :|: 4 ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4+X₁ ≤ X₀ ∧ 4 ≤ X₀+X₂ ∧ 4+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₁₀₆:evalrealheapsortbb11in(X₀,X₁,X₂,X₃) → t₁₀₇:evalrealheapsortbb13in(X₀,X₁,X₂,1+2⋅X₂) :|: 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₁₀₈:evalrealheapsortbb12in(X₀,X₁,X₂,X₃) → t₁₀₉:evalrealheapsortbb13in(X₀,X₁,X₂,2+2⋅X₂) :|: 4 ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4+X₁ ≤ X₀ ∧ 4 ≤ X₀+X₂ ∧ 4+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₁₁₀:evalrealheapsortbb13in(X₀,X₁,X₂,X₃) → t₁₁₁:evalrealheapsortbb14in(X₀,X₁,X₂,X₃) :|: 1 ≤ X₁+X₃ ∧ 1 ≤ X₂+X₃ ∧ 1+X₂ ≤ X₃ ∧ 1 ≤ X₃ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂
g₁₁₂:evalrealheapsortbb13in(X₀,X₁,X₂,X₃) → t₁₁₃:evalrealheapsortbb16in(X₀,X₁,X₀,X₃) :|: 1 ≤ X₁+X₃ ∧ 1 ≤ X₂+X₃ ∧ 1+X₂ ≤ X₃ ∧ 1 ≤ X₃ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂
g₁₁₄:evalrealheapsortbb14in(X₀,X₁,X₂,X₃) → t₁₁₅:evalrealheapsortbb16in(X₀,X₁,X₃,X₃) :|: 1 ≤ X₁+X₃ ∧ 1 ≤ X₂+X₃ ∧ 1+X₂ ≤ X₃ ∧ 1 ≤ X₃ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂
g₁₁₆:evalrealheapsortbb17in(X₀,X₁,X₂,X₃) → t₁₁₇:evalrealheapsortbb18in(X₀,1+X₁,X₂,X₃) :|: 2+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₂ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃
g₁₁₈:evalrealheapsortreturnin(X₀,X₁,X₂,X₃) → t₁₁₉:evalrealheapsortstop(X₀,X₁,X₂,X₃) :|: 0 ≤ X₃

Run classical analysis on SCC: [evalrealheapsortstart]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: 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₈₄: 1 {O(1)}
g₈₆: 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}
g₁₁₂: inf {Infinity}
g₁₁₄: inf {Infinity}
g₁₁₆: inf {Infinity}
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}
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₀,evalrealheapsortentryin), X₀: X₀ {O(n)}
(g₀,evalrealheapsortentryin), X₁: X₁ {O(n)}
(g₀,evalrealheapsortentryin), X₂: X₂ {O(n)}
(g₀,evalrealheapsortentryin), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [evalrealheapsortstart]

Run classical analysis on SCC: [evalrealheapsortentryin]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: 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₈₄: 1 {O(1)}
g₈₆: 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}
g₁₁₂: inf {Infinity}
g₁₁₄: inf {Infinity}
g₁₁₆: inf {Infinity}
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}
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₀,evalrealheapsortentryin), X₀: X₀ {O(n)}
(g₀,evalrealheapsortentryin), X₁: X₁ {O(n)}
(g₀,evalrealheapsortentryin), X₂: X₂ {O(n)}
(g₀,evalrealheapsortentryin), X₃: 0 {O(1)}
(g₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₂,evalrealheapsortbb6in), X₁: 1 {O(1)}
(g₂,evalrealheapsortbb6in), X₂: X₂ {O(n)}
(g₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₄,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₄,evalrealheapsortreturnin), X₁: X₁ {O(n)}
(g₄,evalrealheapsortreturnin), X₂: X₂ {O(n)}
(g₄,evalrealheapsortreturnin), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [evalrealheapsortentryin]

Run classical analysis on SCC: [evalrealheapsortbb2in; evalrealheapsortbb3in; evalrealheapsortbb4in; evalrealheapsortbb5in; evalrealheapsortbb6in]

MPRF for transition t₇: evalrealheapsortbb6in(X₀,X₁,X₂,X₃) → evalrealheapsortbb3in(X₀,X₁,X₁,X₃) :|: 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0 ∧ 1+X₁ ≤ X₀ of depth 1:

new bound:

X₀+2 {O(n)}

MPRF:

• evalrealheapsortbb2in: [X₀-X₁]
• evalrealheapsortbb3in: [X₀-X₁]
• evalrealheapsortbb4in: [X₀-X₁]
• evalrealheapsortbb5in: [X₀-X₁]
• evalrealheapsortbb6in: [1+X₀-X₁]

MPRF for transition t₁₁: evalrealheapsortbb3in(X₀,X₁,X₂,X₃) → evalrealheapsortbb5in(X₀,X₁,X₂,X₃) :|: 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0 ∧ X₂ ≤ 0 of depth 1:

new bound:

X₀+1 {O(n)}

MPRF:

• evalrealheapsortbb2in: [X₀-X₁]
• evalrealheapsortbb3in: [X₀-X₁]
• evalrealheapsortbb4in: [X₀-X₁]
• evalrealheapsortbb5in: [X₀-1-X₁]
• evalrealheapsortbb6in: [X₀-X₁]

MPRF for transition t₂₅: evalrealheapsortbb4in(X₀,X₁,X₂,X₃) → evalrealheapsortbb5in(X₀,X₁,X₂,X₃) :|: 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 1 ≤ X₂ ∧ 1 ≤ X₂+X₃ ∧ 1+X₃ ≤ X₂ ∧ 2 ≤ X₁+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4 ≤ X₀+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ E ∧ 2⋅E ≤ 1+X₂ ∧ X₂ ≤ 2⋅E of depth 1:

new bound:

3⋅X₀+3 {O(n)}

MPRF:

• evalrealheapsortbb2in: [3⋅X₀-3⋅X₁]
• evalrealheapsortbb3in: [3⋅X₀-3⋅X₁]
• evalrealheapsortbb4in: [3⋅X₀-3⋅X₁]
• evalrealheapsortbb5in: [3⋅X₀-3-3⋅X₁]
• evalrealheapsortbb6in: [3⋅X₀-3⋅X₁]

MPRF for transition t₈₃: evalrealheapsortbb5in(X₀,X₁,X₂,X₃) → evalrealheapsortbb6in(X₀,1+X₁,X₂,X₃) :|: 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0 of depth 1:

new bound:

X₀+2 {O(n)}

MPRF:

• evalrealheapsortbb2in: [1+X₀-X₁]
• evalrealheapsortbb3in: [1+X₀-X₁]
• evalrealheapsortbb4in: [1+X₀-X₁]
• evalrealheapsortbb5in: [1+X₀-X₁]
• evalrealheapsortbb6in: [1+X₀-X₁]

MPRF for transition t₁₅: evalrealheapsortbb3in(X₀,X₁,X₂,X₃) → evalrealheapsortbb4in(X₀,X₁,X₂,X₃) :|: 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0 ∧ 1 ≤ X₂ of depth 1:

new bound:

4⋅X₀⋅X₀+20⋅X₀+28 {O(n^2)}

MPRF:

• evalrealheapsortbb2in: [2⋅X₁+X₂-2]
• evalrealheapsortbb3in: [2⋅X₁+2⋅X₂-1]
• evalrealheapsortbb4in: [2⋅X₁+2⋅X₂-3]
• evalrealheapsortbb5in: [2⋅X₁+2⋅X₂-3]
• evalrealheapsortbb6in: [4⋅X₁]

MPRF for transition t₁₉: evalrealheapsortbb4in(X₀,X₁,X₂,X₃) → evalrealheapsortbb2in(X₀,X₁,X₂,X₃) :|: 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 1 ≤ X₂ ∧ 1 ≤ X₂+X₃ ∧ 1+X₃ ≤ X₂ ∧ 2 ≤ X₁+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4 ≤ X₀+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ E ∧ 2⋅E ≤ 1+X₂ ∧ X₂ ≤ 2⋅E of depth 1:

new bound:

3⋅X₀⋅X₀+13⋅X₀+14 {O(n^2)}

MPRF:

• evalrealheapsortbb2in: [X₀+X₂-1]
• evalrealheapsortbb3in: [X₀+2⋅X₂]
• evalrealheapsortbb4in: [X₀+2⋅X₂]
• evalrealheapsortbb5in: [X₀+2⋅X₂]
• evalrealheapsortbb6in: [X₀+2⋅X₁]

MPRF for transition t₅₅: evalrealheapsortbb2in(X₀,X₁,X₂,X₃) → evalrealheapsortbb3in(X₀,X₁,E-1,X₃) :|: 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0 ∧ 0 ≤ X₂ ∧ 0 ≤ F ∧ 2⋅F ≤ 1+X₂ ∧ X₂ ≤ 2⋅F ∧ 0 ≤ G ∧ 2⋅G ≤ 1+X₂ ∧ X₂ ≤ 2⋅G ∧ 0 ≤ E ∧ 2⋅E ≤ 1+X₂ ∧ X₂ ≤ 2⋅E of depth 1:

new bound:

2⋅X₀⋅X₀+11⋅X₀+17 {O(n^2)}

MPRF:

• evalrealheapsortbb2in: [1+2⋅X₂]
• evalrealheapsortbb3in: [1+2⋅X₂]
• evalrealheapsortbb4in: [1+2⋅X₂]
• evalrealheapsortbb5in: [2⋅X₂]
• evalrealheapsortbb6in: [1+2⋅X₁]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: X₀+2 {O(n)}
g₈: 1 {O(1)}
g₁₀: inf {Infinity}
g₁₃: inf {Infinity}
g₁₈: 3⋅X₀⋅X₀+13⋅X₀+14 {O(n^2)}
g₂₄: 3⋅X₀+3 {O(n)}
g₂₈: inf {Infinity}
g₅₄: 2⋅X₀⋅X₀+11⋅X₀+17 {O(n^2)}
g₈₂: X₀+2 {O(n)}
g₈₄: 1 {O(1)}
g₈₆: 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}
g₁₁₂: inf {Infinity}
g₁₁₄: inf {Infinity}
g₁₁₆: inf {Infinity}
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}
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₀,evalrealheapsortentryin), X₀: X₀ {O(n)}
(g₀,evalrealheapsortentryin), X₁: X₁ {O(n)}
(g₀,evalrealheapsortentryin), X₂: X₂ {O(n)}
(g₀,evalrealheapsortentryin), X₃: 0 {O(1)}
(g₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₂,evalrealheapsortbb6in), X₁: 1 {O(1)}
(g₂,evalrealheapsortbb6in), X₂: X₂ {O(n)}
(g₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₄,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₄,evalrealheapsortreturnin), X₁: X₁ {O(n)}
(g₄,evalrealheapsortreturnin), X₂: X₂ {O(n)}
(g₄,evalrealheapsortreturnin), X₃: 0 {O(1)}
(g₆,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₆,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₆,evalrealheapsortbb3in), X₂: X₀+4 {O(n)}
(g₆,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈,evalrealheapsortbb7in), X₀: X₀ {O(n)}
(g₈,evalrealheapsortbb7in), X₁: X₀+3 {O(n)}
(g₈,evalrealheapsortbb7in), X₂: X₀+7 {O(n)}
(g₈,evalrealheapsortbb7in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₀: 2⋅X₀ {O(n)}
(g₁₀,evalrealheapsortbb2in), X₁: 2⋅X₀+6 {O(n)}
(g₁₀,evalrealheapsortbb2in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₀: 2⋅X₀ {O(n)}
(g₁₀,evalrealheapsortbb5in), X₁: 2⋅X₀+6 {O(n)}
(g₁₀,evalrealheapsortbb5in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb3in), X₀: 2⋅X₀ {O(n)}
(g₁₃,evalrealheapsortbb3in), X₁: 2⋅X₀+6 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb4in), X₀: 2⋅X₀ {O(n)}
(g₁₃,evalrealheapsortbb4in), X₁: 2⋅X₀+6 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₃: 0 {O(1)}
(g₁₈,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₈,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₂: X₀+6 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₂₄,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₂₄,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₂: X₀+6 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₂₈,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₂₈,evalrealheapsortbb3in), X₂: 1 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₅₄,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₅₄,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₂: X₀+6 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₈₂,evalrealheapsortbb6in), X₁: X₀+3 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₂: X₀+7 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [evalrealheapsortbb2in; evalrealheapsortbb3in; evalrealheapsortbb4in; evalrealheapsortbb5in; evalrealheapsortbb6in]

Plrf for transition g₁₀:evalrealheapsortbb3in(X₀,X₁,X₂,X₃) → [1/2]:t₁₁:evalrealheapsortbb5in(X₀,X₁,X₂,X₃) :+: [1/2]:t₁₂:evalrealheapsortbb2in(X₀,X₁,X₂,X₃) :|: X₂ ≤ 0 ∧ 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0:

new bound:

2⋅X₀+2 {O(n)}

PLRF:

• evalrealheapsortbb2in: 2⋅X₀-2⋅X₁
• evalrealheapsortbb3in: 2⋅X₀-2⋅X₁
• evalrealheapsortbb4in: 2⋅X₀-2⋅X₁
• evalrealheapsortbb5in: 2⋅X₀-2-2⋅X₁
• evalrealheapsortbb6in: 2⋅X₀-2⋅X₁

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

Plrf for transition g₁₃:evalrealheapsortbb3in(X₀,X₁,X₂,X₃) → [1/2]:t₁₄:evalrealheapsortbb3in(X₀,X₁,X₂,X₃) :+: [1/2]:t₁₅:evalrealheapsortbb4in(X₀,X₁,X₂,X₃) :|: 1 ≤ X₂ ∧ 0 ≤ 1+X₂ ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0:

new bound:

2⋅X₀⋅X₀+12⋅X₀+20 {O(n^2)}

PLRF:

• evalrealheapsortbb2in: 1+X₂
• evalrealheapsortbb3in: 2+2⋅X₂
• evalrealheapsortbb4in: 2⋅X₂
• evalrealheapsortbb5in: 0
• evalrealheapsortbb6in: 2+2⋅X₁

Use expected size bounds for entry point (g₂:evalrealheapsortentryin→[t₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)
Use classical time bound for entry point (g₂:evalrealheapsortentryin→[t₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)
Use expected size bounds for entry point (g₈₂:evalrealheapsortbb5in→[t₈₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)
Use classical time bound for entry point (g₈₂:evalrealheapsortbb5in→[t₈₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)

Plrf for transition g₂₈:evalrealheapsortbb2in(X₀,X₁,X₂,X₃) → t₂₉:evalrealheapsortbb3in(X₀,X₁,-1,X₃) :|: 0 ≤ 1+X₂ ∧ 1+X₂ ≤ 0 ∧ 0 ≤ 1+X₂+X₃ ∧ X₃ ≤ 1+X₂ ∧ 1+X₁ ≤ X₀ ∧ 1+X₂ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₁+X₃ ∧ 1+X₃ ≤ X₁ ∧ 2 ≤ X₀+X₂ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 3+X₃ ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 0 ≤ X₁+X₂ ∧ X₂ ≤ X₁ ∧ 0 ≤ X₃ ∧ X₃ ≤ 0:

new bound:

10/3⋅X₀⋅X₀+12⋅X₀+7 {O(n^2)}

PLRF:

• evalrealheapsortbb2in: 7/3⋅X₀+1/2⋅X₂-1/2-2⋅X₁
• evalrealheapsortbb3in: 7/3⋅X₀+X₂-1-2⋅X₁
• evalrealheapsortbb4in: 7/3⋅X₀+X₂-1-2⋅X₁
• evalrealheapsortbb5in: 0
• evalrealheapsortbb6in: 7/3⋅X₀-X₁

Use expected size bounds for entry point (g₂:evalrealheapsortentryin→[t₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)
Use expected size bounds for entry point (g₂:evalrealheapsortentryin→[t₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)
Use classical time bound for entry point (g₂:evalrealheapsortentryin→[t₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)
Use expected size bounds for entry point (g₈₂:evalrealheapsortbb5in→[t₈₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)
Use expected size bounds for entry point (g₈₂:evalrealheapsortbb5in→[t₈₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)
Use classical time bound for entry point (g₈₂:evalrealheapsortbb5in→[t₈₃:1:evalrealheapsortbb6in],evalrealheapsortbb6in)

Run classical analysis on SCC: [evalrealheapsortbb7in]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: X₀+2 {O(n)}
g₈: 1 {O(1)}
g₁₀: 2⋅X₀+2 {O(n)}
g₁₃: 2⋅X₀⋅X₀+12⋅X₀+20 {O(n^2)}
g₁₈: 3⋅X₀⋅X₀+13⋅X₀+14 {O(n^2)}
g₂₄: 3⋅X₀+3 {O(n)}
g₂₈: 10/3⋅X₀⋅X₀+12⋅X₀+7 {O(n^2)}
g₅₄: 2⋅X₀⋅X₀+11⋅X₀+17 {O(n^2)}
g₈₂: X₀+2 {O(n)}
g₈₄: 1 {O(1)}
g₈₆: 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}
g₁₁₂: inf {Infinity}
g₁₁₄: inf {Infinity}
g₁₁₆: inf {Infinity}
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}
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₀,evalrealheapsortentryin), X₀: X₀ {O(n)}
(g₀,evalrealheapsortentryin), X₁: X₁ {O(n)}
(g₀,evalrealheapsortentryin), X₂: X₂ {O(n)}
(g₀,evalrealheapsortentryin), X₃: 0 {O(1)}
(g₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₂,evalrealheapsortbb6in), X₁: 1 {O(1)}
(g₂,evalrealheapsortbb6in), X₂: X₂ {O(n)}
(g₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₄,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₄,evalrealheapsortreturnin), X₁: X₁ {O(n)}
(g₄,evalrealheapsortreturnin), X₂: X₂ {O(n)}
(g₄,evalrealheapsortreturnin), X₃: 0 {O(1)}
(g₆,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₆,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₆,evalrealheapsortbb3in), X₂: X₀+4 {O(n)}
(g₆,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈,evalrealheapsortbb7in), X₀: X₀ {O(n)}
(g₈,evalrealheapsortbb7in), X₁: X₀+3 {O(n)}
(g₈,evalrealheapsortbb7in), X₂: X₀+7 {O(n)}
(g₈,evalrealheapsortbb7in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb2in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb5in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb4in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb4in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₃: 0 {O(1)}
(g₁₈,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₈,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₂: X₀+6 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₂₄,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₂₄,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₂: X₀+6 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₂₈,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₂₈,evalrealheapsortbb3in), X₂: 1 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₅₄,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₅₄,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₂: X₀+6 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₈₂,evalrealheapsortbb6in), X₁: X₀+3 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₂: X₀+7 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₈₄,evalrealheapsortbb18in), X₁: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₂: X₀+7 {O(n)}
(g₈₄,evalrealheapsortbb18in), X₃: 0 {O(1)}

Run probabilistic analysis on SCC: [evalrealheapsortbb7in]

Run classical analysis on SCC: [evalrealheapsortbb10in; evalrealheapsortbb11in; evalrealheapsortbb12in; evalrealheapsortbb13in; evalrealheapsortbb14in; evalrealheapsortbb16in; evalrealheapsortbb17in; evalrealheapsortbb18in; evalrealheapsortbb8in; evalrealheapsortbb9in]

MPRF for transition t₈₇: evalrealheapsortbb18in(X₀,X₁,X₂,X₃) → evalrealheapsortbb8in(X₀,X₁,X₂,X₃) :|: 1+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₃ ∧ 2+X₁ ≤ X₀ of depth 1:

new bound:

X₀+1 {O(n)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₁]
• evalrealheapsortbb11in: [X₀-X₁]
• evalrealheapsortbb12in: [X₀-X₁]
• evalrealheapsortbb13in: [X₀-X₁]
• evalrealheapsortbb14in: [X₀-X₁]
• evalrealheapsortbb16in: [X₀-X₁]
• evalrealheapsortbb17in: [X₀-X₁]
• evalrealheapsortbb18in: [1+X₀-X₁]
• evalrealheapsortbb8in: [X₀-X₁]
• evalrealheapsortbb9in: [X₀-X₁]

MPRF for transition t₉₁: evalrealheapsortbb8in(X₀,X₁,X₂,X₃) → evalrealheapsortbb16in(X₀,X₁,Temp_Int₈₃₉,X₃) :|: 2+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₃ ∧ 2+X₁ ≤ X₀ ∧ 0 ≤ X₁ ∧ 3 ≤ X₀ ∧ 0 ≤ X₃ ∧ Temp_Int₈₃₉ ≤ 0 ∧ 0 ≤ Temp_Int₈₃₉ of depth 1:

new bound:

X₀+1 {O(n)}

MPRF:

• evalrealheapsortbb10in: [X₀-2-X₁]
• evalrealheapsortbb11in: [X₀-2-X₁]
• evalrealheapsortbb12in: [X₀-2-X₁]
• evalrealheapsortbb13in: [X₀-2-X₁]
• evalrealheapsortbb14in: [X₀-2-X₁]
• evalrealheapsortbb16in: [X₀-2-X₁]
• evalrealheapsortbb17in: [X₀-2-X₁]
• evalrealheapsortbb18in: [X₀-1-X₁]
• evalrealheapsortbb8in: [X₀-1-X₁]
• evalrealheapsortbb9in: [X₀-2-X₁]

MPRF for transition t₉₅: evalrealheapsortbb16in(X₀,X₁,X₂,X₃) → evalrealheapsortbb17in(X₀,X₁,X₂,X₃) :|: 2+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₂ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃ ∧ X₀ ≤ 2+X₁+2⋅X₂ of depth 1:

new bound:

X₀ {O(n)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₁]
• evalrealheapsortbb11in: [X₀-X₁]
• evalrealheapsortbb12in: [X₀-X₁]
• evalrealheapsortbb13in: [X₀-X₁]
• evalrealheapsortbb14in: [X₀-X₁]
• evalrealheapsortbb16in: [X₀-X₁]
• evalrealheapsortbb17in: [X₀-1-X₁]
• evalrealheapsortbb18in: [X₀-X₁]
• evalrealheapsortbb8in: [X₀-X₁]
• evalrealheapsortbb9in: [X₀-X₁]

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

new bound:

X₀ {O(n)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₁]
• evalrealheapsortbb11in: [X₀-X₁]
• evalrealheapsortbb12in: [X₀-X₁]
• evalrealheapsortbb13in: [X₀-X₁]
• evalrealheapsortbb14in: [X₀-X₁]
• evalrealheapsortbb16in: [X₀-X₁]
• evalrealheapsortbb17in: [X₀-X₁]
• evalrealheapsortbb18in: [X₀-X₁]
• evalrealheapsortbb8in: [X₀-X₁]
• evalrealheapsortbb9in: [X₀-X₁]

MPRF for transition t₉₃: evalrealheapsortbb16in(X₀,X₁,X₂,X₃) → evalrealheapsortbb9in(X₀,X₁,X₂,X₃) :|: 2+X₁ ≤ X₀ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3 ≤ X₀+X₂ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃ ∧ 3+X₁+2⋅X₂ ≤ X₀ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-3-X₂]
• evalrealheapsortbb11in: [X₀-3-X₂]
• evalrealheapsortbb12in: [X₀-3-X₂]
• evalrealheapsortbb13in: [X₀-3-X₂]
• evalrealheapsortbb14in: [X₀-3-X₂]
• evalrealheapsortbb16in: [X₀-2-X₂]
• evalrealheapsortbb17in: [X₀-2-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-3-X₂]

MPRF for transition t₉₇: evalrealheapsortbb9in(X₀,X₁,X₂,X₃) → evalrealheapsortbb11in(X₀,X₁,X₂,X₃) :|: 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃ ∧ X₀ ≤ 3+X₁+2⋅X₂ ∧ 3+X₁+2⋅X₂ ≤ X₀ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₂]
• evalrealheapsortbb11in: [X₀-1-X₂]
• evalrealheapsortbb12in: [X₀-X₂]
• evalrealheapsortbb13in: [X₀-1-X₂]
• evalrealheapsortbb14in: [X₀-X₃]
• evalrealheapsortbb16in: [X₀-X₂]
• evalrealheapsortbb17in: [X₀-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-X₂]

MPRF for transition t₉₉: evalrealheapsortbb9in(X₀,X₁,X₂,X₃) → evalrealheapsortbb10in(X₀,X₁,X₂,X₃) :|: 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃ ∧ 4+X₁+2⋅X₂ ≤ X₀ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-1-X₂]
• evalrealheapsortbb11in: [X₀-1-X₂]
• evalrealheapsortbb12in: [X₀-1-X₂]
• evalrealheapsortbb13in: [X₀-1-X₂]
• evalrealheapsortbb14in: [X₀-X₃]
• evalrealheapsortbb16in: [X₀-X₂]
• evalrealheapsortbb17in: [X₀-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-X₂]

MPRF for transition t₁₀₃: evalrealheapsortbb10in(X₀,X₁,X₂,X₃) → evalrealheapsortbb11in(X₀,X₁,X₂,X₃) :|: 4 ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4+X₁ ≤ X₀ ∧ 4 ≤ X₀+X₂ ∧ 4+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₂]
• evalrealheapsortbb11in: [X₀-1-X₂]
• evalrealheapsortbb12in: [X₀-1-X₂]
• evalrealheapsortbb13in: [X₀-1-X₂]
• evalrealheapsortbb14in: [X₀-1-X₂]
• evalrealheapsortbb16in: [X₀-X₂]
• evalrealheapsortbb17in: [X₀-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-X₂]

MPRF for transition t₁₀₅: evalrealheapsortbb10in(X₀,X₁,X₂,X₃) → evalrealheapsortbb12in(X₀,X₁,X₂,X₃) :|: 4 ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4+X₁ ≤ X₀ ∧ 4 ≤ X₀+X₂ ∧ 4+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₂]
• evalrealheapsortbb11in: [X₀-1-X₂]
• evalrealheapsortbb12in: [X₀-1-X₂]
• evalrealheapsortbb13in: [X₀-1-X₂]
• evalrealheapsortbb14in: [X₀-X₃]
• evalrealheapsortbb16in: [X₀-X₂]
• evalrealheapsortbb17in: [X₀-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-X₂]

MPRF for transition t₁₀₇: evalrealheapsortbb11in(X₀,X₁,X₂,X₃) → evalrealheapsortbb13in(X₀,X₁,X₂,1+2⋅X₂) :|: 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 3 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₂]
• evalrealheapsortbb11in: [X₀-X₂]
• evalrealheapsortbb12in: [X₀-1-X₂]
• evalrealheapsortbb13in: [X₀-1-X₂]
• evalrealheapsortbb14in: [X₀-1-X₂]
• evalrealheapsortbb16in: [X₀-X₂]
• evalrealheapsortbb17in: [X₀-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-X₂]

MPRF for transition t₁₀₉: evalrealheapsortbb12in(X₀,X₁,X₂,X₃) → evalrealheapsortbb13in(X₀,X₁,X₂,2+2⋅X₂) :|: 4 ≤ X₀ ∧ 4 ≤ X₀+X₁ ∧ 4+X₁ ≤ X₀ ∧ 4 ≤ X₀+X₂ ∧ 4+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₂ ∧ 0 ≤ X₂+X₃ ∧ 0 ≤ X₃ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₂]
• evalrealheapsortbb11in: [X₀-X₂]
• evalrealheapsortbb12in: [X₀-X₂]
• evalrealheapsortbb13in: [X₀-1-X₂]
• evalrealheapsortbb14in: [X₀-1-X₂]
• evalrealheapsortbb16in: [X₀-X₂]
• evalrealheapsortbb17in: [X₀-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-X₂]

MPRF for transition t₁₁₁: evalrealheapsortbb13in(X₀,X₁,X₂,X₃) → evalrealheapsortbb14in(X₀,X₁,X₂,X₃) :|: 1 ≤ X₁+X₃ ∧ 1 ≤ X₂+X₃ ∧ 1+X₂ ≤ X₃ ∧ 1 ≤ X₃ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₂]
• evalrealheapsortbb11in: [X₀-X₂]
• evalrealheapsortbb12in: [X₀-X₂]
• evalrealheapsortbb13in: [X₀-X₂]
• evalrealheapsortbb14in: [X₀-1-X₂]
• evalrealheapsortbb16in: [X₀-X₂]
• evalrealheapsortbb17in: [X₀-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-X₂]

MPRF for transition t₁₁₃: evalrealheapsortbb13in(X₀,X₁,X₂,X₃) → evalrealheapsortbb16in(X₀,X₁,X₀,X₃) :|: 1 ≤ X₁+X₃ ∧ 1 ≤ X₂+X₃ ∧ 1+X₂ ≤ X₃ ∧ 1 ≤ X₃ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-X₂]
• evalrealheapsortbb11in: [X₀-X₂]
• evalrealheapsortbb12in: [X₀-X₂]
• evalrealheapsortbb13in: [X₀-X₂]
• evalrealheapsortbb14in: [X₀-1-X₂]
• evalrealheapsortbb16in: [X₀-X₂]
• evalrealheapsortbb17in: [X₀-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-X₂]

MPRF for transition t₁₁₅: evalrealheapsortbb14in(X₀,X₁,X₂,X₃) → evalrealheapsortbb16in(X₀,X₁,X₃,X₃) :|: 1 ≤ X₁+X₃ ∧ 1 ≤ X₂+X₃ ∧ 1+X₂ ≤ X₃ ∧ 1 ≤ X₃ ∧ 3 ≤ X₀ ∧ 3 ≤ X₀+X₁ ∧ 3+X₁ ≤ X₀ ∧ 3 ≤ X₀+X₂ ∧ 3+X₂ ≤ X₀ ∧ 4 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₁+X₂ ∧ 0 ≤ X₂ of depth 1:

new bound:

X₀⋅X₀+X₀ {O(n^2)}

MPRF:

• evalrealheapsortbb10in: [X₀-2-X₂]
• evalrealheapsortbb11in: [X₀-2-X₂]
• evalrealheapsortbb12in: [X₀-2-X₂]
• evalrealheapsortbb13in: [X₀-2-X₂]
• evalrealheapsortbb14in: [X₀-2-X₂]
• evalrealheapsortbb16in: [X₀-2-X₂]
• evalrealheapsortbb17in: [X₀-2-X₂]
• evalrealheapsortbb18in: [X₀]
• evalrealheapsortbb8in: [X₀]
• evalrealheapsortbb9in: [X₀-2-X₂]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:61/3⋅X₀⋅X₀+69⋅X₀+76 {O(n^2)}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: X₀+2 {O(n)}
g₈: 1 {O(1)}
g₁₀: 2⋅X₀+2 {O(n)}
g₁₃: 2⋅X₀⋅X₀+12⋅X₀+20 {O(n^2)}
g₁₈: 3⋅X₀⋅X₀+13⋅X₀+14 {O(n^2)}
g₂₄: 3⋅X₀+3 {O(n)}
g₂₈: 10/3⋅X₀⋅X₀+12⋅X₀+7 {O(n^2)}
g₅₄: 2⋅X₀⋅X₀+11⋅X₀+17 {O(n^2)}
g₈₂: X₀+2 {O(n)}
g₈₄: 1 {O(1)}
g₈₆: X₀+1 {O(n)}
g₈₈: 1 {O(1)}
g₉₀: X₀+1 {O(n)}
g₉₂: X₀⋅X₀+X₀ {O(n^2)}
g₉₄: X₀ {O(n)}
g₉₆: X₀⋅X₀+X₀ {O(n^2)}
g₉₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₆: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₀: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₆: X₀ {O(n)}
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}
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₀,evalrealheapsortentryin), X₀: X₀ {O(n)}
(g₀,evalrealheapsortentryin), X₁: X₁ {O(n)}
(g₀,evalrealheapsortentryin), X₂: X₂ {O(n)}
(g₀,evalrealheapsortentryin), X₃: 0 {O(1)}
(g₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₂,evalrealheapsortbb6in), X₁: 1 {O(1)}
(g₂,evalrealheapsortbb6in), X₂: X₂ {O(n)}
(g₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₄,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₄,evalrealheapsortreturnin), X₁: X₁ {O(n)}
(g₄,evalrealheapsortreturnin), X₂: X₂ {O(n)}
(g₄,evalrealheapsortreturnin), X₃: 0 {O(1)}
(g₆,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₆,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₆,evalrealheapsortbb3in), X₂: X₀+4 {O(n)}
(g₆,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈,evalrealheapsortbb7in), X₀: X₀ {O(n)}
(g₈,evalrealheapsortbb7in), X₁: X₀+3 {O(n)}
(g₈,evalrealheapsortbb7in), X₂: X₀+7 {O(n)}
(g₈,evalrealheapsortbb7in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb2in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb5in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb4in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb4in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₃: 0 {O(1)}
(g₁₈,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₈,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₂: X₀+6 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₂₄,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₂₄,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₂: X₀+6 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₂₈,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₂₈,evalrealheapsortbb3in), X₂: 1 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₅₄,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₅₄,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₂: X₀+6 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₈₂,evalrealheapsortbb6in), X₁: X₀+3 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₂: X₀+7 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₈₄,evalrealheapsortbb18in), X₁: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₂: X₀+7 {O(n)}
(g₈₄,evalrealheapsortbb18in), X₃: 0 {O(1)}
(g₈₆,evalrealheapsortbb8in), X₀: X₀ {O(n)}
(g₈₆,evalrealheapsortbb8in), X₁: X₀ {O(n)}
(g₈₆,evalrealheapsortbb8in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+3⋅X₀+7 {O(EXP)}
(g₈₆,evalrealheapsortbb8in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₈₈,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₈₈,evalrealheapsortreturnin), X₁: X₀ {O(n)}
(g₈₈,evalrealheapsortreturnin), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₈₈,evalrealheapsortreturnin), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₀,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₉₀,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₉₀,evalrealheapsortbb16in), X₂: 0 {O(1)}
(g₉₀,evalrealheapsortbb16in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₂,evalrealheapsortbb9in), X₀: X₀ {O(n)}
(g₉₂,evalrealheapsortbb9in), X₁: X₀ {O(n)}
(g₉₂,evalrealheapsortbb9in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₂,evalrealheapsortbb9in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₉₄,evalrealheapsortbb17in), X₀: X₀ {O(n)}
(g₉₄,evalrealheapsortbb17in), X₁: X₀ {O(n)}
(g₉₄,evalrealheapsortbb17in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₉₄,evalrealheapsortbb17in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₆,evalrealheapsortbb11in), X₀: X₀ {O(n)}
(g₉₆,evalrealheapsortbb11in), X₁: X₀ {O(n)}
(g₉₆,evalrealheapsortbb11in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₆,evalrealheapsortbb11in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₉₈,evalrealheapsortbb10in), X₀: X₀ {O(n)}
(g₉₈,evalrealheapsortbb10in), X₁: X₀ {O(n)}
(g₉₈,evalrealheapsortbb10in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₈,evalrealheapsortbb10in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₂,evalrealheapsortbb11in), X₀: X₀ {O(n)}
(g₁₀₂,evalrealheapsortbb11in), X₁: X₀ {O(n)}
(g₁₀₂,evalrealheapsortbb11in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₂,evalrealheapsortbb11in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₄,evalrealheapsortbb12in), X₀: X₀ {O(n)}
(g₁₀₄,evalrealheapsortbb12in), X₁: X₀ {O(n)}
(g₁₀₄,evalrealheapsortbb12in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₄,evalrealheapsortbb12in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₆,evalrealheapsortbb13in), X₀: X₀ {O(n)}
(g₁₀₆,evalrealheapsortbb13in), X₁: X₀ {O(n)}
(g₁₀₆,evalrealheapsortbb13in), X₂: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₀₆,evalrealheapsortbb13in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₈,evalrealheapsortbb13in), X₀: X₀ {O(n)}
(g₁₀₈,evalrealheapsortbb13in), X₁: X₀ {O(n)}
(g₁₀₈,evalrealheapsortbb13in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₈,evalrealheapsortbb13in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₀,evalrealheapsortbb14in), X₀: X₀ {O(n)}
(g₁₁₀,evalrealheapsortbb14in), X₁: X₀ {O(n)}
(g₁₁₀,evalrealheapsortbb14in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₀,evalrealheapsortbb14in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₂,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₂: 2⋅X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₄,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₁₁₄,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₁₁₄,evalrealheapsortbb16in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₄,evalrealheapsortbb16in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₆,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₁₁₆,evalrealheapsortbb18in), X₁: X₀ {O(n)}
(g₁₁₆,evalrealheapsortbb18in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₁₁₆,evalrealheapsortbb18in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}

Run probabilistic analysis on SCC: [evalrealheapsortbb10in; evalrealheapsortbb11in; evalrealheapsortbb12in; evalrealheapsortbb13in; evalrealheapsortbb14in; evalrealheapsortbb16in; evalrealheapsortbb17in; evalrealheapsortbb18in; evalrealheapsortbb8in; evalrealheapsortbb9in]

Run classical analysis on SCC: [evalrealheapsortreturnin]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:61/3⋅X₀⋅X₀+69⋅X₀+76 {O(n^2)}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: X₀+2 {O(n)}
g₈: 1 {O(1)}
g₁₀: 2⋅X₀+2 {O(n)}
g₁₃: 2⋅X₀⋅X₀+12⋅X₀+20 {O(n^2)}
g₁₈: 3⋅X₀⋅X₀+13⋅X₀+14 {O(n^2)}
g₂₄: 3⋅X₀+3 {O(n)}
g₂₈: 10/3⋅X₀⋅X₀+12⋅X₀+7 {O(n^2)}
g₅₄: 2⋅X₀⋅X₀+11⋅X₀+17 {O(n^2)}
g₈₂: X₀+2 {O(n)}
g₈₄: 1 {O(1)}
g₈₆: X₀+1 {O(n)}
g₈₈: 1 {O(1)}
g₉₀: X₀+1 {O(n)}
g₉₂: X₀⋅X₀+X₀ {O(n^2)}
g₉₄: X₀ {O(n)}
g₉₆: X₀⋅X₀+X₀ {O(n^2)}
g₉₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₆: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₀: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₆: X₀ {O(n)}
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}
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₀,evalrealheapsortentryin), X₀: X₀ {O(n)}
(g₀,evalrealheapsortentryin), X₁: X₁ {O(n)}
(g₀,evalrealheapsortentryin), X₂: X₂ {O(n)}
(g₀,evalrealheapsortentryin), X₃: 0 {O(1)}
(g₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₂,evalrealheapsortbb6in), X₁: 1 {O(1)}
(g₂,evalrealheapsortbb6in), X₂: X₂ {O(n)}
(g₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₄,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₄,evalrealheapsortreturnin), X₁: X₁ {O(n)}
(g₄,evalrealheapsortreturnin), X₂: X₂ {O(n)}
(g₄,evalrealheapsortreturnin), X₃: 0 {O(1)}
(g₆,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₆,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₆,evalrealheapsortbb3in), X₂: X₀+4 {O(n)}
(g₆,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈,evalrealheapsortbb7in), X₀: X₀ {O(n)}
(g₈,evalrealheapsortbb7in), X₁: X₀+3 {O(n)}
(g₈,evalrealheapsortbb7in), X₂: X₀+7 {O(n)}
(g₈,evalrealheapsortbb7in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb2in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb5in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb4in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb4in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₃: 0 {O(1)}
(g₁₈,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₈,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₂: X₀+6 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₂₄,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₂₄,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₂: X₀+6 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₂₈,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₂₈,evalrealheapsortbb3in), X₂: 1 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₅₄,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₅₄,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₂: X₀+6 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₈₂,evalrealheapsortbb6in), X₁: X₀+3 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₂: X₀+7 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₈₄,evalrealheapsortbb18in), X₁: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₂: X₀+7 {O(n)}
(g₈₄,evalrealheapsortbb18in), X₃: 0 {O(1)}
(g₈₆,evalrealheapsortbb8in), X₀: X₀ {O(n)}
(g₈₆,evalrealheapsortbb8in), X₁: X₀ {O(n)}
(g₈₆,evalrealheapsortbb8in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+3⋅X₀+7 {O(EXP)}
(g₈₆,evalrealheapsortbb8in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₈₈,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₈₈,evalrealheapsortreturnin), X₁: X₀ {O(n)}
(g₈₈,evalrealheapsortreturnin), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₈₈,evalrealheapsortreturnin), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₀,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₉₀,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₉₀,evalrealheapsortbb16in), X₂: 0 {O(1)}
(g₉₀,evalrealheapsortbb16in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₂,evalrealheapsortbb9in), X₀: X₀ {O(n)}
(g₉₂,evalrealheapsortbb9in), X₁: X₀ {O(n)}
(g₉₂,evalrealheapsortbb9in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₂,evalrealheapsortbb9in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₉₄,evalrealheapsortbb17in), X₀: X₀ {O(n)}
(g₉₄,evalrealheapsortbb17in), X₁: X₀ {O(n)}
(g₉₄,evalrealheapsortbb17in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₉₄,evalrealheapsortbb17in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₆,evalrealheapsortbb11in), X₀: X₀ {O(n)}
(g₉₆,evalrealheapsortbb11in), X₁: X₀ {O(n)}
(g₉₆,evalrealheapsortbb11in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₆,evalrealheapsortbb11in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₉₈,evalrealheapsortbb10in), X₀: X₀ {O(n)}
(g₉₈,evalrealheapsortbb10in), X₁: X₀ {O(n)}
(g₉₈,evalrealheapsortbb10in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₈,evalrealheapsortbb10in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₂,evalrealheapsortbb11in), X₀: X₀ {O(n)}
(g₁₀₂,evalrealheapsortbb11in), X₁: X₀ {O(n)}
(g₁₀₂,evalrealheapsortbb11in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₂,evalrealheapsortbb11in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₄,evalrealheapsortbb12in), X₀: X₀ {O(n)}
(g₁₀₄,evalrealheapsortbb12in), X₁: X₀ {O(n)}
(g₁₀₄,evalrealheapsortbb12in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₄,evalrealheapsortbb12in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₆,evalrealheapsortbb13in), X₀: X₀ {O(n)}
(g₁₀₆,evalrealheapsortbb13in), X₁: X₀ {O(n)}
(g₁₀₆,evalrealheapsortbb13in), X₂: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₀₆,evalrealheapsortbb13in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₈,evalrealheapsortbb13in), X₀: X₀ {O(n)}
(g₁₀₈,evalrealheapsortbb13in), X₁: X₀ {O(n)}
(g₁₀₈,evalrealheapsortbb13in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₈,evalrealheapsortbb13in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₀,evalrealheapsortbb14in), X₀: X₀ {O(n)}
(g₁₁₀,evalrealheapsortbb14in), X₁: X₀ {O(n)}
(g₁₁₀,evalrealheapsortbb14in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₀,evalrealheapsortbb14in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₂,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₂: 2⋅X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₄,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₁₁₄,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₁₁₄,evalrealheapsortbb16in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₄,evalrealheapsortbb16in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₆,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₁₁₆,evalrealheapsortbb18in), X₁: X₀ {O(n)}
(g₁₁₆,evalrealheapsortbb18in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₁₁₆,evalrealheapsortbb18in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₈,evalrealheapsortstop), X₀: 2⋅X₀ {O(n)}
(g₁₁₈,evalrealheapsortstop), X₁: X₀+X₁ {O(n)}
(g₁₁₈,evalrealheapsortstop), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀+X₂ {O(EXP)}
(g₁₁₈,evalrealheapsortstop), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}

Run probabilistic analysis on SCC: [evalrealheapsortreturnin]

Run classical analysis on SCC: [evalrealheapsortstop]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:61/3⋅X₀⋅X₀+69⋅X₀+76 {O(n^2)}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: X₀+2 {O(n)}
g₈: 1 {O(1)}
g₁₀: 2⋅X₀+2 {O(n)}
g₁₃: 2⋅X₀⋅X₀+12⋅X₀+20 {O(n^2)}
g₁₈: 3⋅X₀⋅X₀+13⋅X₀+14 {O(n^2)}
g₂₄: 3⋅X₀+3 {O(n)}
g₂₈: 10/3⋅X₀⋅X₀+12⋅X₀+7 {O(n^2)}
g₅₄: 2⋅X₀⋅X₀+11⋅X₀+17 {O(n^2)}
g₈₂: X₀+2 {O(n)}
g₈₄: 1 {O(1)}
g₈₆: X₀+1 {O(n)}
g₈₈: 1 {O(1)}
g₉₀: X₀+1 {O(n)}
g₉₂: X₀⋅X₀+X₀ {O(n^2)}
g₉₄: X₀ {O(n)}
g₉₆: X₀⋅X₀+X₀ {O(n^2)}
g₉₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₆: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₀: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₆: X₀ {O(n)}
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}
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₀,evalrealheapsortentryin), X₀: X₀ {O(n)}
(g₀,evalrealheapsortentryin), X₁: X₁ {O(n)}
(g₀,evalrealheapsortentryin), X₂: X₂ {O(n)}
(g₀,evalrealheapsortentryin), X₃: 0 {O(1)}
(g₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₂,evalrealheapsortbb6in), X₁: 1 {O(1)}
(g₂,evalrealheapsortbb6in), X₂: X₂ {O(n)}
(g₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₄,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₄,evalrealheapsortreturnin), X₁: X₁ {O(n)}
(g₄,evalrealheapsortreturnin), X₂: X₂ {O(n)}
(g₄,evalrealheapsortreturnin), X₃: 0 {O(1)}
(g₆,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₆,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₆,evalrealheapsortbb3in), X₂: X₀+4 {O(n)}
(g₆,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈,evalrealheapsortbb7in), X₀: X₀ {O(n)}
(g₈,evalrealheapsortbb7in), X₁: X₀+3 {O(n)}
(g₈,evalrealheapsortbb7in), X₂: X₀+7 {O(n)}
(g₈,evalrealheapsortbb7in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb2in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb5in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb4in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb4in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₃: 0 {O(1)}
(g₁₈,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₈,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₂: X₀+6 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₂₄,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₂₄,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₂: X₀+6 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₂₈,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₂₈,evalrealheapsortbb3in), X₂: 1 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₅₄,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₅₄,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₂: X₀+6 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₈₂,evalrealheapsortbb6in), X₁: X₀+3 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₂: X₀+7 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₈₄,evalrealheapsortbb18in), X₁: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₂: X₀+7 {O(n)}
(g₈₄,evalrealheapsortbb18in), X₃: 0 {O(1)}
(g₈₆,evalrealheapsortbb8in), X₀: X₀ {O(n)}
(g₈₆,evalrealheapsortbb8in), X₁: X₀ {O(n)}
(g₈₆,evalrealheapsortbb8in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+3⋅X₀+7 {O(EXP)}
(g₈₆,evalrealheapsortbb8in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₈₈,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₈₈,evalrealheapsortreturnin), X₁: X₀ {O(n)}
(g₈₈,evalrealheapsortreturnin), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₈₈,evalrealheapsortreturnin), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₀,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₉₀,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₉₀,evalrealheapsortbb16in), X₂: 0 {O(1)}
(g₉₀,evalrealheapsortbb16in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₂,evalrealheapsortbb9in), X₀: X₀ {O(n)}
(g₉₂,evalrealheapsortbb9in), X₁: X₀ {O(n)}
(g₉₂,evalrealheapsortbb9in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₂,evalrealheapsortbb9in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₉₄,evalrealheapsortbb17in), X₀: X₀ {O(n)}
(g₉₄,evalrealheapsortbb17in), X₁: X₀ {O(n)}
(g₉₄,evalrealheapsortbb17in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₉₄,evalrealheapsortbb17in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₆,evalrealheapsortbb11in), X₀: X₀ {O(n)}
(g₉₆,evalrealheapsortbb11in), X₁: X₀ {O(n)}
(g₉₆,evalrealheapsortbb11in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₆,evalrealheapsortbb11in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₉₈,evalrealheapsortbb10in), X₀: X₀ {O(n)}
(g₉₈,evalrealheapsortbb10in), X₁: X₀ {O(n)}
(g₉₈,evalrealheapsortbb10in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₈,evalrealheapsortbb10in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₂,evalrealheapsortbb11in), X₀: X₀ {O(n)}
(g₁₀₂,evalrealheapsortbb11in), X₁: X₀ {O(n)}
(g₁₀₂,evalrealheapsortbb11in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₂,evalrealheapsortbb11in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₄,evalrealheapsortbb12in), X₀: X₀ {O(n)}
(g₁₀₄,evalrealheapsortbb12in), X₁: X₀ {O(n)}
(g₁₀₄,evalrealheapsortbb12in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₄,evalrealheapsortbb12in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₆,evalrealheapsortbb13in), X₀: X₀ {O(n)}
(g₁₀₆,evalrealheapsortbb13in), X₁: X₀ {O(n)}
(g₁₀₆,evalrealheapsortbb13in), X₂: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₀₆,evalrealheapsortbb13in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₈,evalrealheapsortbb13in), X₀: X₀ {O(n)}
(g₁₀₈,evalrealheapsortbb13in), X₁: X₀ {O(n)}
(g₁₀₈,evalrealheapsortbb13in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₈,evalrealheapsortbb13in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₀,evalrealheapsortbb14in), X₀: X₀ {O(n)}
(g₁₁₀,evalrealheapsortbb14in), X₁: X₀ {O(n)}
(g₁₁₀,evalrealheapsortbb14in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₀,evalrealheapsortbb14in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₂,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₂: 2⋅X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₄,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₁₁₄,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₁₁₄,evalrealheapsortbb16in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₄,evalrealheapsortbb16in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₆,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₁₁₆,evalrealheapsortbb18in), X₁: X₀ {O(n)}
(g₁₁₆,evalrealheapsortbb18in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₁₁₆,evalrealheapsortbb18in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₈,evalrealheapsortstop), X₀: 2⋅X₀ {O(n)}
(g₁₁₈,evalrealheapsortstop), X₁: X₀+X₁ {O(n)}
(g₁₁₈,evalrealheapsortstop), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀+X₂ {O(EXP)}
(g₁₁₈,evalrealheapsortstop), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}

Run probabilistic analysis on SCC: [evalrealheapsortstop]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:61/3⋅X₀⋅X₀+69⋅X₀+76 {O(n^2)}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: X₀+2 {O(n)}
g₈: 1 {O(1)}
g₁₀: 2⋅X₀+2 {O(n)}
g₁₃: 2⋅X₀⋅X₀+12⋅X₀+20 {O(n^2)}
g₁₈: 3⋅X₀⋅X₀+13⋅X₀+14 {O(n^2)}
g₂₄: 3⋅X₀+3 {O(n)}
g₂₈: 10/3⋅X₀⋅X₀+12⋅X₀+7 {O(n^2)}
g₅₄: 2⋅X₀⋅X₀+11⋅X₀+17 {O(n^2)}
g₈₂: X₀+2 {O(n)}
g₈₄: 1 {O(1)}
g₈₆: X₀+1 {O(n)}
g₈₈: 1 {O(1)}
g₉₀: X₀+1 {O(n)}
g₉₂: X₀⋅X₀+X₀ {O(n^2)}
g₉₄: X₀ {O(n)}
g₉₆: X₀⋅X₀+X₀ {O(n^2)}
g₉₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₆: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₀: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₆: X₀ {O(n)}
g₁₁₈: 1 {O(1)}

Costbounds

Overall costbound: 67/3⋅X₀⋅X₀+83⋅X₀+98 {O(n^2)}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₄: 1 {O(1)}
g₆: X₀+2 {O(n)}
g₈: 1 {O(1)}
g₁₀: 4⋅X₀+4 {O(n)}
g₁₃: 4⋅X₀⋅X₀+24⋅X₀+40 {O(n^2)}
g₁₈: 3⋅X₀⋅X₀+13⋅X₀+14 {O(n^2)}
g₂₄: 3⋅X₀+3 {O(n)}
g₂₈: 10/3⋅X₀⋅X₀+12⋅X₀+7 {O(n^2)}
g₅₄: 2⋅X₀⋅X₀+11⋅X₀+17 {O(n^2)}
g₈₂: X₀+2 {O(n)}
g₈₄: 1 {O(1)}
g₈₆: X₀+1 {O(n)}
g₈₈: 1 {O(1)}
g₉₀: X₀+1 {O(n)}
g₉₂: X₀⋅X₀+X₀ {O(n^2)}
g₉₄: X₀ {O(n)}
g₉₆: X₀⋅X₀+X₀ {O(n^2)}
g₉₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₆: X₀⋅X₀+X₀ {O(n^2)}
g₁₀₈: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₀: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₂: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₄: X₀⋅X₀+X₀ {O(n^2)}
g₁₁₆: X₀ {O(n)}
g₁₁₈: 1 {O(1)}

Sizebounds

(g₀,evalrealheapsortentryin), X₀: X₀ {O(n)}
(g₀,evalrealheapsortentryin), X₁: X₁ {O(n)}
(g₀,evalrealheapsortentryin), X₂: X₂ {O(n)}
(g₀,evalrealheapsortentryin), X₃: 0 {O(1)}
(g₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₂,evalrealheapsortbb6in), X₁: 1 {O(1)}
(g₂,evalrealheapsortbb6in), X₂: X₂ {O(n)}
(g₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₄,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₄,evalrealheapsortreturnin), X₁: X₁ {O(n)}
(g₄,evalrealheapsortreturnin), X₂: X₂ {O(n)}
(g₄,evalrealheapsortreturnin), X₃: 0 {O(1)}
(g₆,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₆,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₆,evalrealheapsortbb3in), X₂: X₀+4 {O(n)}
(g₆,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈,evalrealheapsortbb7in), X₀: X₀ {O(n)}
(g₈,evalrealheapsortbb7in), X₁: X₀+3 {O(n)}
(g₈,evalrealheapsortbb7in), X₂: X₀+7 {O(n)}
(g₈,evalrealheapsortbb7in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb2in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₁₀,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₁₀,evalrealheapsortbb5in), X₂: 2 {O(1)}
(g₁₀,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₁₃,evalrealheapsortbb4in), X₀: X₀ {O(n)}
(g₁₃,evalrealheapsortbb4in), X₁: X₀+3 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₂: 2⋅X₀+12 {O(n)}
(g₁₃,evalrealheapsortbb4in), X₃: 0 {O(1)}
(g₁₈,evalrealheapsortbb2in), X₀: X₀ {O(n)}
(g₁₈,evalrealheapsortbb2in), X₁: X₀+3 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₂: X₀+6 {O(n)}
(g₁₈,evalrealheapsortbb2in), X₃: 0 {O(1)}
(g₂₄,evalrealheapsortbb5in), X₀: X₀ {O(n)}
(g₂₄,evalrealheapsortbb5in), X₁: X₀+3 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₂: X₀+6 {O(n)}
(g₂₄,evalrealheapsortbb5in), X₃: 0 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₂₈,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₂₈,evalrealheapsortbb3in), X₂: 1 {O(1)}
(g₂₈,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₅₄,evalrealheapsortbb3in), X₀: X₀ {O(n)}
(g₅₄,evalrealheapsortbb3in), X₁: X₀+3 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₂: X₀+6 {O(n)}
(g₅₄,evalrealheapsortbb3in), X₃: 0 {O(1)}
(g₈₂,evalrealheapsortbb6in), X₀: X₀ {O(n)}
(g₈₂,evalrealheapsortbb6in), X₁: X₀+3 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₂: X₀+7 {O(n)}
(g₈₂,evalrealheapsortbb6in), X₃: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₈₄,evalrealheapsortbb18in), X₁: 0 {O(1)}
(g₈₄,evalrealheapsortbb18in), X₂: X₀+7 {O(n)}
(g₈₄,evalrealheapsortbb18in), X₃: 0 {O(1)}
(g₈₆,evalrealheapsortbb8in), X₀: X₀ {O(n)}
(g₈₆,evalrealheapsortbb8in), X₁: X₀ {O(n)}
(g₈₆,evalrealheapsortbb8in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+3⋅X₀+7 {O(EXP)}
(g₈₆,evalrealheapsortbb8in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₈₈,evalrealheapsortreturnin), X₀: X₀ {O(n)}
(g₈₈,evalrealheapsortreturnin), X₁: X₀ {O(n)}
(g₈₈,evalrealheapsortreturnin), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₈₈,evalrealheapsortreturnin), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₀,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₉₀,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₉₀,evalrealheapsortbb16in), X₂: 0 {O(1)}
(g₉₀,evalrealheapsortbb16in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₂,evalrealheapsortbb9in), X₀: X₀ {O(n)}
(g₉₂,evalrealheapsortbb9in), X₁: X₀ {O(n)}
(g₉₂,evalrealheapsortbb9in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₂,evalrealheapsortbb9in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₉₄,evalrealheapsortbb17in), X₀: X₀ {O(n)}
(g₉₄,evalrealheapsortbb17in), X₁: X₀ {O(n)}
(g₉₄,evalrealheapsortbb17in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₉₄,evalrealheapsortbb17in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₉₆,evalrealheapsortbb11in), X₀: X₀ {O(n)}
(g₉₆,evalrealheapsortbb11in), X₁: X₀ {O(n)}
(g₉₆,evalrealheapsortbb11in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₆,evalrealheapsortbb11in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₉₈,evalrealheapsortbb10in), X₀: X₀ {O(n)}
(g₉₈,evalrealheapsortbb10in), X₁: X₀ {O(n)}
(g₉₈,evalrealheapsortbb10in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₉₈,evalrealheapsortbb10in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₂,evalrealheapsortbb11in), X₀: X₀ {O(n)}
(g₁₀₂,evalrealheapsortbb11in), X₁: X₀ {O(n)}
(g₁₀₂,evalrealheapsortbb11in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₂,evalrealheapsortbb11in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₄,evalrealheapsortbb12in), X₀: X₀ {O(n)}
(g₁₀₄,evalrealheapsortbb12in), X₁: X₀ {O(n)}
(g₁₀₄,evalrealheapsortbb12in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₄,evalrealheapsortbb12in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅8⋅X₀⋅X₀ {O(EXP)}
(g₁₀₆,evalrealheapsortbb13in), X₀: X₀ {O(n)}
(g₁₀₆,evalrealheapsortbb13in), X₁: X₀ {O(n)}
(g₁₀₆,evalrealheapsortbb13in), X₂: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₀₆,evalrealheapsortbb13in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₈,evalrealheapsortbb13in), X₀: X₀ {O(n)}
(g₁₀₈,evalrealheapsortbb13in), X₁: X₀ {O(n)}
(g₁₀₈,evalrealheapsortbb13in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₀₈,evalrealheapsortbb13in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₀,evalrealheapsortbb14in), X₀: X₀ {O(n)}
(g₁₁₀,evalrealheapsortbb14in), X₁: X₀ {O(n)}
(g₁₁₀,evalrealheapsortbb14in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₀,evalrealheapsortbb14in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₂,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₂: 2⋅X₀ {O(n)}
(g₁₁₂,evalrealheapsortbb16in), X₃: 2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₄,evalrealheapsortbb16in), X₀: X₀ {O(n)}
(g₁₁₄,evalrealheapsortbb16in), X₁: X₀ {O(n)}
(g₁₁₄,evalrealheapsortbb16in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₄,evalrealheapsortbb16in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀ {O(EXP)}
(g₁₁₆,evalrealheapsortbb18in), X₀: X₀ {O(n)}
(g₁₁₆,evalrealheapsortbb18in), X₁: X₀ {O(n)}
(g₁₁₆,evalrealheapsortbb18in), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀ {O(EXP)}
(g₁₁₆,evalrealheapsortbb18in), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}
(g₁₁₈,evalrealheapsortstop), X₀: 2⋅X₀ {O(n)}
(g₁₁₈,evalrealheapsortstop), X₁: X₀+X₁ {O(n)}
(g₁₁₈,evalrealheapsortstop), X₂: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2⋅X₀+X₂ {O(EXP)}
(g₁₁₈,evalrealheapsortstop), X₃: 2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀+2⋅2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅X₀⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀+2^(X₀⋅X₀+X₀)⋅2^(X₀⋅X₀+X₀)⋅4⋅X₀⋅X₀ {O(EXP)}