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

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

(0) Obligation:

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

f(a, a) → f(a, b) 2.47/1.18
f(a, b) → f(s(a), c) 2.47/1.18
f(s(X), c) → f(X, c) 2.47/1.18
f(c, c) → f(a, a)

Rewrite Strategy: INNERMOST
2.47/1.18
2.47/1.18

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

Converted CpxTRS to CDT
2.47/1.18
2.47/1.18

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, a) → f(a, b) 2.47/1.18
f(a, b) → f(s(a), c) 2.47/1.18
f(s(z0), c) → f(z0, c) 2.47/1.18
f(c, c) → f(a, a)
Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.18
F(a, b) → c2(F(s(a), c)) 2.47/1.18
F(s(z0), c) → c3(F(z0, c)) 2.47/1.18
F(c, c) → c4(F(a, a))
S tuples:

F(a, a) → c1(F(a, b)) 2.47/1.18
F(a, b) → c2(F(s(a), c)) 2.47/1.18
F(s(z0), c) → c3(F(z0, c)) 2.47/1.18
F(c, c) → c4(F(a, a))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c3, c4

2.47/1.18
2.47/1.18

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

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

F(c, c) → c4(F(a, a))
We considered the (Usable) Rules:none
And the Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2(F(s(a), c)) 2.47/1.19
F(s(z0), c) → c3(F(z0, c)) 2.47/1.19
F(c, c) → c4(F(a, a))
The order we found is given by the following interpretation:
Polynomial interpretation : 2.47/1.19

POL(F(x1, x2)) = x12    2.47/1.19
POL(a) = 0    2.47/1.19
POL(b) = 0    2.47/1.19
POL(c) = [1]    2.47/1.19
POL(c1(x1)) = x1    2.47/1.19
POL(c2(x1)) = x1    2.47/1.19
POL(c3(x1)) = x1    2.47/1.19
POL(c4(x1)) = x1    2.47/1.19
POL(s(x1)) = x1   
2.47/1.19
2.47/1.19

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, a) → f(a, b) 2.47/1.19
f(a, b) → f(s(a), c) 2.47/1.19
f(s(z0), c) → f(z0, c) 2.47/1.19
f(c, c) → f(a, a)
Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2(F(s(a), c)) 2.47/1.19
F(s(z0), c) → c3(F(z0, c)) 2.47/1.19
F(c, c) → c4(F(a, a))
S tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2(F(s(a), c)) 2.47/1.19
F(s(z0), c) → c3(F(z0, c))
K tuples:

F(c, c) → c4(F(a, a))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c3, c4

2.47/1.19
2.47/1.19

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

The following tuples could be moved from S to K by knowledge propagation:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2(F(s(a), c)) 2.47/1.19
F(a, b) → c2(F(s(a), c))
2.47/1.19
2.47/1.19

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, a) → f(a, b) 2.47/1.19
f(a, b) → f(s(a), c) 2.47/1.19
f(s(z0), c) → f(z0, c) 2.47/1.19
f(c, c) → f(a, a)
Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2(F(s(a), c)) 2.47/1.19
F(s(z0), c) → c3(F(z0, c)) 2.47/1.19
F(c, c) → c4(F(a, a))
S tuples:

F(s(z0), c) → c3(F(z0, c))
K tuples:

F(c, c) → c4(F(a, a)) 2.47/1.19
F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2(F(s(a), c))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c3, c4

2.47/1.19
2.47/1.19

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

Use forward instantiation to replace F(s(z0), c) → c3(F(z0, c)) by

F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c))
2.47/1.19
2.47/1.19

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, a) → f(a, b) 2.47/1.19
f(a, b) → f(s(a), c) 2.47/1.19
f(s(z0), c) → f(z0, c) 2.47/1.19
f(c, c) → f(a, a)
Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2(F(s(a), c)) 2.47/1.19
F(c, c) → c4(F(a, a)) 2.47/1.19
F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c))
S tuples:

F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c))
K tuples:

F(c, c) → c4(F(a, a)) 2.47/1.19
F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2(F(s(a), c))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c4, c3

2.47/1.19
2.47/1.19

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

Removed 1 trailing tuple parts
2.47/1.19
2.47/1.19

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, a) → f(a, b) 2.47/1.19
f(a, b) → f(s(a), c) 2.47/1.19
f(s(z0), c) → f(z0, c) 2.47/1.19
f(c, c) → f(a, a)
Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(c, c) → c4(F(a, a)) 2.47/1.19
F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c)) 2.47/1.19
F(a, b) → c2
S tuples:

F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c))
K tuples:

F(c, c) → c4(F(a, a)) 2.47/1.19
F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c4, c3, c2

2.47/1.19
2.47/1.19

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

Removed 4 trailing nodes:

F(a, b) → c2 2.47/1.19
F(s(c), c) → c3(F(c, c)) 2.47/1.19
F(a, a) → c1(F(a, b)) 2.47/1.19
F(c, c) → c4(F(a, a))
2.47/1.19
2.47/1.19

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, a) → f(a, b) 2.47/1.19
f(a, b) → f(s(a), c) 2.47/1.19
f(s(z0), c) → f(z0, c) 2.47/1.19
f(c, c) → f(a, a)
Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(c, c) → c4(F(a, a)) 2.47/1.19
F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c)) 2.47/1.19
F(a, b) → c2
S tuples:

F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c))
K tuples:

F(c, c) → c4(F(a, a)) 2.47/1.19
F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c4, c3, c2

2.47/1.19
2.47/1.19

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

F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c))
We considered the (Usable) Rules:none
And the Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(c, c) → c4(F(a, a)) 2.47/1.19
F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c)) 2.47/1.19
F(a, b) → c2
The order we found is given by the following interpretation:
Polynomial interpretation : 2.47/1.19

POL(F(x1, x2)) = [4]x1 + [2]x2    2.47/1.19
POL(a) = [2]    2.47/1.19
POL(b) = 0    2.47/1.19
POL(c) = [4]    2.47/1.19
POL(c1(x1)) = x1    2.47/1.19
POL(c2) = 0    2.47/1.19
POL(c3(x1)) = x1    2.47/1.19
POL(c4(x1)) = x1    2.47/1.19
POL(s(x1)) = [4] + x1   
2.47/1.19
2.47/1.19

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, a) → f(a, b) 2.47/1.19
f(a, b) → f(s(a), c) 2.47/1.19
f(s(z0), c) → f(z0, c) 2.47/1.19
f(c, c) → f(a, a)
Tuples:

F(a, a) → c1(F(a, b)) 2.47/1.19
F(c, c) → c4(F(a, a)) 2.47/1.19
F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c)) 2.47/1.19
F(a, b) → c2
S tuples:none
K tuples:

F(c, c) → c4(F(a, a)) 2.47/1.19
F(a, a) → c1(F(a, b)) 2.47/1.19
F(a, b) → c2 2.47/1.19
F(s(s(y0)), c) → c3(F(s(y0), c)) 2.47/1.19
F(s(c), c) → c3(F(c, c))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c4, c3, c2

2.47/1.19
2.47/1.19

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

The set S is empty
2.47/1.19
2.47/1.19

(16) BOUNDS(O(1), O(1))

2.47/1.19
2.47/1.19
2.77/1.26 EOF