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:
M( f(x1, x2) ) = | / | 0 | \ |
110.54/80.63 | | 0 | | |
110.54/80.63 \ | 0 | / |
110.54/80.63
| + | / | 3 | 0 | 0 | \ |
110.54/80.63 | | 0 | 1 | 0 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x1 | + | / | 0 | 3 | 3 | \ |
110.54/80.63 | | 0 | 0 | 1 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x2 |
110.54/80.63
M( g(x1) ) = | / | 2 | \ |
110.54/80.63 | | 1 | | |
110.54/80.63 \ | 0 | / |
110.54/80.63
| + | / | 0 | 2 | 1 | \ |
110.54/80.63 | | 0 | 0 | 0 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x1 |
110.54/80.63
M( 0 ) = | / | 0 | \ |
110.54/80.63 | | 0 | | |
110.54/80.63 \ | 0 | / |
110.54/80.63
|
110.54/80.63
M( 1 ) = | / | 0 | \ |
110.54/80.63 | | 0 | | |
110.54/80.63 \ | 3 | / |
110.54/80.63
|
110.54/80.63
Tuple symbols:
M( c1(x1) ) = | / | 0 | \ |
110.54/80.63 | | 0 | | |
110.54/80.63 \ | 0 | / |
110.54/80.63
| + | / | 1 | 0 | 0 | \ |
110.54/80.63 | | 0 | 0 | 0 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x1 |
110.54/80.63
M( c(x1, x2) ) = | / | 0 | \ |
110.54/80.63 | | 0 | | |
110.54/80.63 \ | 0 | / |
110.54/80.63
| + | / | 1 | 0 | 0 | \ |
110.54/80.63 | | 0 | 0 | 0 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x1 | + | / | 1 | 0 | 0 | \ |
110.54/80.63 | | 0 | 0 | 0 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x2 |
110.54/80.63
M( f(x1, x2) ) = | / | 0 | \ |
110.54/80.63 | | 0 | | |
110.54/80.63 \ | 1 | / |
110.54/80.63
| + | / | 3 | 0 | 0 | \ |
110.54/80.63 | | 0 | 1 | 0 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x1 | + | / | 0 | 3 | 3 | \ |
110.54/80.63 | | 0 | 0 | 1 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x2 |
110.54/80.63
M( F(x1, x2) ) = | / | 0 | \ |
110.54/80.63 | | 2 | | |
110.54/80.63 \ | 0 | / |
110.54/80.63
| + | / | 1 | 0 | 0 | \ |
110.54/80.63 | | 0 | 0 | 0 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x1 | + | / | 0 | 0 | 3 | \ |
110.54/80.63 | | 0 | 0 | 0 | | |
110.54/80.63 \ | 0 | 0 | 0 | / |
110.54/80.63
| · | x2 |
110.54/80.63
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