YES(O(1), O(n^1)) 2.46/1.07 YES(O(1), O(n^1)) 2.46/1.09 2.46/1.09 2.46/1.09 2.46/1.09 2.46/1.09 2.46/1.09 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 2.46/1.09 2.46/1.09 2.46/1.09
2.46/1.09
2.46/1.09
2.46/1.09
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

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

(0) Obligation:

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

a__f(a, X, X) → a__f(X, a__b, b) 2.46/1.09
a__b → a 2.46/1.09
mark(f(X1, X2, X3)) → a__f(X1, mark(X2), X3) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a 2.46/1.09
a__f(X1, X2, X3) → f(X1, X2, X3) 2.46/1.09
a__b → b

Rewrite Strategy: INNERMOST
2.46/1.09
2.46/1.09

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

Converted CpxTRS to CDT
2.46/1.09
2.46/1.09

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2) 2.46/1.09
a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a
Tuples:

A__F(a, z0, z0) → c(A__F(z0, a__b, b), A__B) 2.46/1.09
MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
MARK(b) → c5(A__B)
S tuples:

A__F(a, z0, z0) → c(A__F(z0, a__b, b), A__B) 2.46/1.09
MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
MARK(b) → c5(A__B)
K tuples:none
Defined Rule Symbols:

a__f, a__b, mark

Defined Pair Symbols:

A__F, MARK

Compound Symbols:

c, c4, c5

2.46/1.09
2.46/1.09

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

Removed 2 trailing tuple parts
2.46/1.09
2.46/1.09

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2) 2.46/1.09
a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a
Tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
S tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
K tuples:none
Defined Rule Symbols:

a__f, a__b, mark

Defined Pair Symbols:

MARK, A__F

Compound Symbols:

c4, c, c5

2.46/1.09
2.46/1.09

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

Removed 1 trailing nodes:

MARK(b) → c5
2.46/1.09
2.46/1.09

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2) 2.46/1.09
a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a
Tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
S tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
K tuples:none
Defined Rule Symbols:

a__f, a__b, mark

Defined Pair Symbols:

MARK, A__F

Compound Symbols:

c4, c, c5

2.46/1.09
2.46/1.09

(7) 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.

MARK(b) → c5
We considered the (Usable) Rules:

a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a 2.46/1.09
a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2)
And the Tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
The order we found is given by the following interpretation:
Polynomial interpretation : 2.46/1.09

POL(A__F(x1, x2, x3)) = 0    2.46/1.09
POL(MARK(x1)) = [3]    2.46/1.09
POL(a) = [2]    2.46/1.09
POL(a__b) = 0    2.46/1.09
POL(a__f(x1, x2, x3)) = [5] + x1 + x2 + [5]x3    2.46/1.09
POL(b) = 0    2.46/1.09
POL(c(x1)) = x1    2.46/1.09
POL(c4(x1, x2)) = x1 + x2    2.46/1.09
POL(c5) = 0    2.46/1.09
POL(f(x1, x2, x3)) = [3] + x1 + x2 + x3    2.46/1.09
POL(mark(x1)) = [1] + [5]x1   
2.46/1.09
2.46/1.09

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2) 2.46/1.09
a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a
Tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
S tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b))
K tuples:

MARK(b) → c5
Defined Rule Symbols:

a__f, a__b, mark

Defined Pair Symbols:

MARK, A__F

Compound Symbols:

c4, c, c5

2.46/1.09
2.46/1.09

(9) 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.

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1))
We considered the (Usable) Rules:

a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a 2.46/1.09
a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2)
And the Tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
The order we found is given by the following interpretation:
Polynomial interpretation : 2.46/1.09

POL(A__F(x1, x2, x3)) = x1 + x3    2.46/1.09
POL(MARK(x1)) = [2]x1    2.46/1.09
POL(a) = 0    2.46/1.09
POL(a__b) = 0    2.46/1.09
POL(a__f(x1, x2, x3)) = [1] + [2]x1 + x2 + [3]x3    2.46/1.09
POL(b) = 0    2.46/1.09
POL(c(x1)) = x1    2.46/1.09
POL(c4(x1, x2)) = x1 + x2    2.46/1.09
POL(c5) = 0    2.46/1.09
POL(f(x1, x2, x3)) = [1] + x1 + x2 + x3    2.46/1.09
POL(mark(x1)) = [1] + [3]x1   
2.46/1.09
2.46/1.09

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2) 2.46/1.09
a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a
Tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
S tuples:

A__F(a, z0, z0) → c(A__F(z0, a__b, b))
K tuples:

MARK(b) → c5 2.46/1.09
MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1))
Defined Rule Symbols:

a__f, a__b, mark

Defined Pair Symbols:

MARK, A__F

Compound Symbols:

c4, c, c5

2.46/1.09
2.46/1.09

(11) 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.

A__F(a, z0, z0) → c(A__F(z0, a__b, b))
We considered the (Usable) Rules:

a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a 2.46/1.09
a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2)
And the Tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
The order we found is given by the following interpretation:
Polynomial interpretation : 2.46/1.09

POL(A__F(x1, x2, x3)) = [2] + [4]x1 + [4]x3    2.46/1.09
POL(MARK(x1)) = [4]x1    2.46/1.09
POL(a) = [4]    2.46/1.09
POL(a__b) = 0    2.46/1.09
POL(a__f(x1, x2, x3)) = [3] + [3]x2    2.46/1.09
POL(b) = [1]    2.46/1.09
POL(c(x1)) = x1    2.46/1.09
POL(c4(x1, x2)) = x1 + x2    2.46/1.09
POL(c5) = 0    2.46/1.09
POL(f(x1, x2, x3)) = [4] + x1 + x2 + x3    2.46/1.09
POL(mark(x1)) = 0   
2.46/1.09
2.46/1.09

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__f(a, z0, z0) → a__f(z0, a__b, b) 2.46/1.09
a__f(z0, z1, z2) → f(z0, z1, z2) 2.46/1.09
a__b → a 2.46/1.09
a__b → b 2.46/1.09
mark(f(z0, z1, z2)) → a__f(z0, mark(z1), z2) 2.46/1.09
mark(b) → a__b 2.46/1.09
mark(a) → a
Tuples:

MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b)) 2.46/1.09
MARK(b) → c5
S tuples:none
K tuples:

MARK(b) → c5 2.46/1.09
MARK(f(z0, z1, z2)) → c4(A__F(z0, mark(z1), z2), MARK(z1)) 2.46/1.09
A__F(a, z0, z0) → c(A__F(z0, a__b, b))
Defined Rule Symbols:

a__f, a__b, mark

Defined Pair Symbols:

MARK, A__F

Compound Symbols:

c4, c, c5

2.46/1.09
2.46/1.09

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

The set S is empty
2.46/1.09
2.46/1.09

(14) BOUNDS(O(1), O(1))

2.46/1.09
2.46/1.09
2.91/1.24 EOF