MAYBE 110.54/80.61 MAYBE 110.54/80.63 110.54/80.63 110.54/80.63 110.54/80.63 110.54/80.63 110.54/80.63 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 110.54/80.63 110.54/80.63 110.54/80.63
110.54/80.63 110.54/80.63 110.54/80.63
110.54/80.63
110.54/80.63

(0) Obligation:

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

f(f(0, x), 1) → f(g(f(x, x)), x) 110.54/80.63
f(g(x), y) → g(f(x, y))

Rewrite Strategy: INNERMOST
110.54/80.63
110.54/80.63

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

Converted CpxTRS to CDT
110.54/80.63
110.54/80.63

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(f(0, z0), 1) → c(F(g(f(z0, z0)), z0), F(z0, z0)) 110.54/80.63
F(g(z0), z1) → c1(F(z0, z1))
S tuples:

F(f(0, z0), 1) → c(F(g(f(z0, z0)), z0), F(z0, z0)) 110.54/80.63
F(g(z0), z1) → c1(F(z0, z1))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

110.54/80.63
110.54/80.63

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

Use forward instantiation to replace F(g(z0), z1) → c1(F(z0, z1)) by

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1))
110.54/80.63
110.54/80.63

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(f(0, z0), 1) → c(F(g(f(z0, z0)), z0), F(z0, z0)) 110.54/80.63
F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1))
S tuples:

F(f(0, z0), 1) → c(F(g(f(z0, z0)), z0), F(z0, z0)) 110.54/80.63
F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

110.54/80.63
110.54/80.63

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

Use narrowing to replace F(f(0, z0), 1) → c(F(g(f(z0, z0)), z0), F(z0, z0)) by

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
110.54/80.63
110.54/80.63

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1)) 110.54/80.63
F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
S tuples:

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1)) 110.54/80.63
F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

110.54/80.63
110.54/80.63

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

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
We considered the (Usable) Rules:

f(g(z0), z1) → g(f(z0, z1)) 110.54/80.63
f(f(0, z0), 1) → f(g(f(z0, z0)), z0)
And the Tuples:

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1)) 110.54/80.63
F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 110.54/80.63

POL(0) = 0    110.54/80.63
POL(1) = [5]    110.54/80.63
POL(F(x1, x2)) = [1] + [2]x2    110.54/80.63
POL(c(x1, x2)) = x1 + x2    110.54/80.63
POL(c1(x1)) = x1    110.54/80.63
POL(f(x1, x2)) = [4] + [2]x1 + [2]x2    110.54/80.63
POL(g(x1)) = [2]   
110.54/80.63
110.54/80.63

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1)) 110.54/80.63
F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
S tuples:

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1))
K tuples:

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

110.54/80.63
110.54/80.63

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

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1))
We considered the (Usable) Rules:

f(g(z0), z1) → g(f(z0, z1)) 110.54/80.63
f(f(0, z0), 1) → f(g(f(z0, z0)), z0)
And the Tuples:

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1)) 110.54/80.63
F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 110.54/80.63

POL(0) = 0    110.54/80.63
POL(1) = [5]    110.54/80.63
POL(F(x1, x2)) = x1 + [5]x2    110.54/80.63
POL(c(x1, x2)) = x1 + x2    110.54/80.63
POL(c1(x1)) = x1    110.54/80.63
POL(f(x1, x2)) = [1]    110.54/80.63
POL(g(x1)) = [2]   
110.54/80.63
110.54/80.63

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) 110.54/80.63
F(g(g(y0)), z1) → c1(F(g(y0), z1)) 110.54/80.63
F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0)))
S tuples:

F(g(g(y0)), z1) → c1(F(g(y0), z1))
K tuples:

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0))) 110.54/80.63
F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

110.54/80.63
110.54/80.63

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

Use forward instantiation to replace F(g(f(0, y0)), 1) → c1(F(f(0, y0), 1)) by

F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1))
110.54/80.63
110.54/80.63

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(g(g(y0)), z1) → c1(F(g(y0), z1)) 110.54/80.63
F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0))) 110.54/80.63
F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1))
S tuples:

F(g(g(y0)), z1) → c1(F(g(y0), z1))
K tuples:

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0))) 110.54/80.63
F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

110.54/80.63
110.54/80.63

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

Use forward instantiation to replace F(g(g(y0)), z1) → c1(F(g(y0), z1)) by

F(g(g(g(y0))), z1) → c1(F(g(g(y0)), z1)) 110.54/80.63
F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1))
110.54/80.63
110.54/80.63

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0))) 110.54/80.63
F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1)) 110.54/80.63
F(g(g(g(y0))), z1) → c1(F(g(g(y0)), z1)) 110.54/80.63
F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1))
S tuples:

F(g(g(g(y0))), z1) → c1(F(g(g(y0)), z1)) 110.54/80.63
F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1))
K tuples:

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0))) 110.54/80.63
F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

110.54/80.63
110.54/80.63

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

Use narrowing to replace F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0))) by

F(f(0, g(g(z0))), 1) → c(F(g(g(g(f(z0, g(g(z0)))))), g(g(z0))), F(g(g(z0)), g(g(z0))))
110.54/80.63
110.54/80.63

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1)) 110.54/80.63
F(g(g(g(y0))), z1) → c1(F(g(g(y0)), z1)) 110.54/80.63
F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1)) 110.54/80.63
F(f(0, g(g(z0))), 1) → c(F(g(g(g(f(z0, g(g(z0)))))), g(g(z0))), F(g(g(z0)), g(g(z0))))
S tuples:

F(g(g(g(y0))), z1) → c1(F(g(g(y0)), z1)) 110.54/80.63
F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1))
K tuples:

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0))) 110.54/80.63
F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

110.54/80.63
110.54/80.63

(17) CdtMatrixRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

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

F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1)) 110.54/80.63
F(f(0, g(g(z0))), 1) → c(F(g(g(g(f(z0, g(g(z0)))))), g(g(z0))), F(g(g(z0)), g(g(z0))))
We considered the (Usable) Rules:

f(g(z0), z1) → g(f(z0, z1)) 110.54/80.63
f(f(0, z0), 1) → f(g(f(z0, z0)), z0)
And the Tuples:

F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1)) 110.54/80.63
F(g(g(g(y0))), z1) → c1(F(g(g(y0)), z1)) 110.54/80.63
F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1)) 110.54/80.63
F(f(0, g(g(z0))), 1) → c(F(g(g(g(f(z0, g(g(z0)))))), g(g(z0))), F(g(g(z0)), g(g(z0))))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]: 110.54/80.63
Non-tuple symbols:
110.54/80.63
M( f(x1, x2) ) = 110.54/80.63 110.54/80.63 110.54/80.63
/0\
|0|
\0/
+ 110.54/80.63 110.54/80.63 110.54/80.63
/300\
|010|
\000/
·x1+ 110.54/80.63 110.54/80.63 110.54/80.63
/033\
|001|
\000/
·x2

110.54/80.63
M( g(x1) ) = 110.54/80.63 110.54/80.63 110.54/80.63
/2\
|1|
\0/
+ 110.54/80.63 110.54/80.63 110.54/80.63
/021\
|000|
\000/
·x1

110.54/80.63
M( 0 ) = 110.54/80.63 110.54/80.63 110.54/80.63
/0\
|0|
\0/

110.54/80.63
M( 1 ) = 110.54/80.63 110.54/80.63 110.54/80.63
/0\
|0|
\3/

Tuple symbols:
110.54/80.63
M( c1(x1) ) = 110.54/80.63 110.54/80.63 110.54/80.63
/0\
|0|
\0/
+ 110.54/80.63 110.54/80.63 110.54/80.63
/100\
|000|
\000/
·x1

110.54/80.63
M( c(x1, x2) ) = 110.54/80.63 110.54/80.63 110.54/80.63
/0\
|0|
\0/
+ 110.54/80.63 110.54/80.63 110.54/80.63
/100\
|000|
\000/
·x1+ 110.54/80.63 110.54/80.63 110.54/80.63
/100\
|000|
\000/
·x2

110.54/80.63
M( f(x1, x2) ) = 110.54/80.63 110.54/80.63 110.54/80.63
/0\
|0|
\1/
+ 110.54/80.63 110.54/80.63 110.54/80.63
/300\
|010|
\000/
·x1+ 110.54/80.63 110.54/80.63 110.54/80.63
/033\
|001|
\000/
·x2

110.54/80.63
M( F(x1, x2) ) = 110.54/80.63 110.54/80.63 110.54/80.63
/0\
|2|
\0/
+ 110.54/80.63 110.54/80.63 110.54/80.63
/100\
|000|
\000/
·x1+ 110.54/80.63 110.54/80.63 110.54/80.63
/003\
|000|
\000/
·x2


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
110.54/80.63
110.54/80.63

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(0, z0), 1) → f(g(f(z0, z0)), z0) 110.54/80.63
f(g(z0), z1) → g(f(z0, z1))
Tuples:

F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1)) 110.54/80.63
F(g(g(g(y0))), z1) → c1(F(g(g(y0)), z1)) 110.54/80.63
F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1)) 110.54/80.63
F(f(0, g(g(z0))), 1) → c(F(g(g(g(f(z0, g(g(z0)))))), g(g(z0))), F(g(g(z0)), g(g(z0))))
S tuples:

F(g(g(g(y0))), z1) → c1(F(g(g(y0)), z1))
K tuples:

F(f(0, g(z0)), 1) → c(F(g(g(f(z0, g(z0)))), g(z0)), F(g(z0), g(z0))) 110.54/80.63
F(g(f(0, g(y0))), 1) → c1(F(f(0, g(y0)), 1)) 110.54/80.63
F(g(g(f(0, g(y0)))), 1) → c1(F(g(f(0, g(y0))), 1)) 110.54/80.63
F(f(0, g(g(z0))), 1) → c(F(g(g(g(f(z0, g(g(z0)))))), g(g(z0))), F(g(g(z0)), g(g(z0))))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

110.54/80.63
110.54/80.63
110.54/80.69 EOF