MAYBE 7.72/2.91 MAYBE 7.72/2.93 7.72/2.93 7.72/2.93 7.72/2.93 7.72/2.93 7.72/2.93 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 7.72/2.93 7.72/2.93 7.72/2.93
7.72/2.93
7.72/2.93
7.72/2.93
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
7.72/2.93 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
7.72/2.93 
↳2 CdtProblem
7.72/2.93 
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
7.72/2.93 
↳4 CdtProblem
7.72/2.93 
↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
7.72/2.93 
↳6 CdtProblem
7.72/2.93 
↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
7.72/2.93 
↳8 CdtProblem
7.72/2.93 
↳9 CdtLeafRemovalProof (ComplexityIfPolyImplication)
7.72/2.93 
↳10 CdtProblem
7.72/2.93 
↳11 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
7.72/2.93 
↳12 CdtProblem
7.72/2.93 
↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
7.72/2.93 
↳14 CdtProblem
7.72/2.93
7.72/2.93 7.72/2.93
7.72/2.93
7.72/2.93

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

purge(nil) → nil 7.72/2.93
purge(.(x, y)) → .(x, purge(remove(x, y))) 7.72/2.93
remove(x, nil) → nil 7.72/2.93
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))

Rewrite Strategy: INNERMOST
7.72/2.93
7.72/2.93

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
7.72/2.93
7.72/2.93

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

purge(nil) → nil 7.72/2.93
purge(.(z0, z1)) → .(z0, purge(remove(z0, z1))) 7.72/2.93
remove(z0, nil) → nil 7.72/2.93
remove(z0, .(z1, z2)) → if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))
Tuples:

PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) 7.72/2.93
REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
S tuples:

PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) 7.72/2.93
REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
K tuples:none
Defined Rule Symbols:

purge, remove

Defined Pair Symbols:

PURGE, REMOVE

Compound Symbols:

c1, c3

7.72/2.93
7.72/2.93

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1))
We considered the (Usable) Rules:

remove(z0, nil) → nil 7.72/2.93
remove(z0, .(z1, z2)) → if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))
And the Tuples:

PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) 7.72/2.93
REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 7.72/2.93

POL(.(x1, x2)) = [2] + x1 + x2    7.72/2.93
POL(=(x1, x2)) = x2    7.72/2.93
POL(PURGE(x1)) = [4]x1    7.72/2.93
POL(REMOVE(x1, x2)) = 0    7.72/2.93
POL(c1(x1, x2)) = x1 + x2    7.72/2.93
POL(c3(x1, x2)) = x1 + x2    7.72/2.93
POL(if(x1, x2, x3)) = x1    7.72/2.93
POL(nil) = 0    7.72/2.93
POL(remove(x1, x2)) = x2   
7.72/2.93
7.72/2.93

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

purge(nil) → nil 7.72/2.93
purge(.(z0, z1)) → .(z0, purge(remove(z0, z1))) 7.72/2.93
remove(z0, nil) → nil 7.72/2.93
remove(z0, .(z1, z2)) → if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))
Tuples:

PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) 7.72/2.93
REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
S tuples:

REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
K tuples:

PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1))
Defined Rule Symbols:

purge, remove

Defined Pair Symbols:

PURGE, REMOVE

Compound Symbols:

c1, c3

7.72/2.93
7.72/2.93

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1)) by

PURGE(.(z0, nil)) → c1(PURGE(nil), REMOVE(z0, nil)) 7.72/2.93
PURGE(.(z0, .(z1, z2))) → c1(PURGE(if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))), REMOVE(z0, .(z1, z2)))
7.72/2.93
7.72/2.93

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

purge(nil) → nil 7.72/2.93
purge(.(z0, z1)) → .(z0, purge(remove(z0, z1))) 7.72/2.93
remove(z0, nil) → nil 7.72/2.93
remove(z0, .(z1, z2)) → if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))
Tuples:

REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2)) 7.72/2.93
PURGE(.(z0, nil)) → c1(PURGE(nil), REMOVE(z0, nil)) 7.72/2.93
PURGE(.(z0, .(z1, z2))) → c1(PURGE(if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))), REMOVE(z0, .(z1, z2)))
S tuples:

REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
K tuples:

PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1))
Defined Rule Symbols:

purge, remove

Defined Pair Symbols:

REMOVE, PURGE

Compound Symbols:

c3, c1

7.72/2.93
7.72/2.93

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing tuple parts
7.72/2.93
7.72/2.93

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

purge(nil) → nil 7.72/2.93
purge(.(z0, z1)) → .(z0, purge(remove(z0, z1))) 7.72/2.93
remove(z0, nil) → nil 7.72/2.93
remove(z0, .(z1, z2)) → if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))
Tuples:

REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2)) 7.72/2.93
PURGE(.(z0, nil)) → c1 7.72/2.93
PURGE(.(z0, .(z1, z2))) → c1(REMOVE(z0, .(z1, z2)))
S tuples:

REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
K tuples:

PURGE(.(z0, z1)) → c1(PURGE(remove(z0, z1)), REMOVE(z0, z1))
Defined Rule Symbols:

purge, remove

Defined Pair Symbols:

REMOVE, PURGE

Compound Symbols:

c3, c1, c1

7.72/2.93
7.72/2.93

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

PURGE(.(z0, .(z1, z2))) → c1(REMOVE(z0, .(z1, z2)))
Removed 1 trailing nodes:

PURGE(.(z0, nil)) → c1
7.72/2.93
7.72/2.93

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

purge(nil) → nil 7.72/2.93
purge(.(z0, z1)) → .(z0, purge(remove(z0, z1))) 7.72/2.93
remove(z0, nil) → nil 7.72/2.93
remove(z0, .(z1, z2)) → if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))
Tuples:

REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
S tuples:

REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2))
K tuples:none
Defined Rule Symbols:

purge, remove

Defined Pair Symbols:

REMOVE

Compound Symbols:

c3

7.72/2.93
7.72/2.93

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace REMOVE(z0, .(z1, z2)) → c3(REMOVE(z0, z2), REMOVE(z0, z2)) by

REMOVE(z0, .(z1, .(y1, y2))) → c3(REMOVE(z0, .(y1, y2)), REMOVE(z0, .(y1, y2)))
7.72/2.93
7.72/2.93

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

purge(nil) → nil 7.72/2.93
purge(.(z0, z1)) → .(z0, purge(remove(z0, z1))) 7.72/2.93
remove(z0, nil) → nil 7.72/2.93
remove(z0, .(z1, z2)) → if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))
Tuples:

REMOVE(z0, .(z1, .(y1, y2))) → c3(REMOVE(z0, .(y1, y2)), REMOVE(z0, .(y1, y2)))
S tuples:

REMOVE(z0, .(z1, .(y1, y2))) → c3(REMOVE(z0, .(y1, y2)), REMOVE(z0, .(y1, y2)))
K tuples:none
Defined Rule Symbols:

purge, remove

Defined Pair Symbols:

REMOVE

Compound Symbols:

c3

7.72/2.93
7.72/2.93

(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace REMOVE(z0, .(z1, .(y1, y2))) → c3(REMOVE(z0, .(y1, y2)), REMOVE(z0, .(y1, y2))) by

REMOVE(z0, .(z1, .(z2, .(y2, y3)))) → c3(REMOVE(z0, .(z2, .(y2, y3))), REMOVE(z0, .(z2, .(y2, y3))))
7.72/2.93
7.72/2.93

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

purge(nil) → nil 7.72/2.93
purge(.(z0, z1)) → .(z0, purge(remove(z0, z1))) 7.72/2.93
remove(z0, nil) → nil 7.72/2.93
remove(z0, .(z1, z2)) → if(=(z0, z1), remove(z0, z2), .(z1, remove(z0, z2)))
Tuples:

REMOVE(z0, .(z1, .(z2, .(y2, y3)))) → c3(REMOVE(z0, .(z2, .(y2, y3))), REMOVE(z0, .(z2, .(y2, y3))))
S tuples:

REMOVE(z0, .(z1, .(z2, .(y2, y3)))) → c3(REMOVE(z0, .(z2, .(y2, y3))), REMOVE(z0, .(z2, .(y2, y3))))
K tuples:none
Defined Rule Symbols:

purge, remove

Defined Pair Symbols:

REMOVE

Compound Symbols:

c3

7.72/2.93
7.72/2.93
7.72/2.97 EOF