(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(a(f(x, y))) → f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) → a(f(x, y))
f(b(x), b(y)) → b(f(x, y))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(b(a(b(a(z0))))), A(b(a(z0))), A(z0), A(b(a(b(a(z1))))), A(b(a(z1))), A(z1))
F(a(z0), a(z1)) → c1(A(f(z0, z1)), F(z0, z1))
F(b(z0), b(z1)) → c2(F(z0, z1))
S tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(b(a(b(a(z0))))), A(b(a(z0))), A(z0), A(b(a(b(a(z1))))), A(b(a(z1))), A(z1))
F(a(z0), a(z1)) → c1(A(f(z0, z1)), F(z0, z1))
F(b(z0), b(z1)) → c2(F(z0, z1))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
A, F
Compound Symbols:
c, c1, c2
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
F(a(z0), a(z1)) → c1(A(f(z0, z1)), F(z0, z1))
F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
S tuples:
F(a(z0), a(z1)) → c1(A(f(z0, z1)), F(z0, z1))
F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
F, A
Compound Symbols:
c1, c2, c
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a(
z0),
a(
z1)) →
c1(
A(
f(
z0,
z1)),
F(
z0,
z1)) by
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(A(b(f(z0, z1))), F(b(z0), b(z1)))
F(a(x0), a(x1)) → c1
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(A(b(f(z0, z1))), F(b(z0), b(z1)))
F(a(x0), a(x1)) → c1
S tuples:
F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(A(b(f(z0, z1))), F(b(z0), b(z1)))
F(a(x0), a(x1)) → c1
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
F, A
Compound Symbols:
c2, c, c1, c1
(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(a(x0), a(x1)) → c1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(A(b(f(z0, z1))), F(b(z0), b(z1)))
S tuples:
F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(A(b(f(z0, z1))), F(b(z0), b(z1)))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
F, A
Compound Symbols:
c2, c, c1
(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(F(b(z0), b(z1)))
S tuples:
F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(F(b(z0), b(z1)))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
F, A
Compound Symbols:
c2, c, c1, c1
(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
b(
z0),
b(
z1)) →
c2(
F(
z0,
z1)) by
F(b(b(y0)), b(b(y1))) → c2(F(b(y0), b(y1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(b(a(b(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(F(b(z0), b(z1)))
F(b(b(y0)), b(b(y1))) → c2(F(b(y0), b(y1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(b(a(b(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
S tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(a(b(z0)), a(b(z1))) → c1(F(b(z0), b(z1)))
F(b(b(y0)), b(b(y1))) → c2(F(b(y0), b(y1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(b(a(b(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
A, F
Compound Symbols:
c, c1, c1, c2
(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
a(
b(
z0)),
a(
b(
z1))) →
c1(
F(
b(
z0),
b(
z1))) by
F(a(b(b(y0))), a(b(b(y1)))) → c1(F(b(b(y0)), b(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(b(y0)), b(b(y1))) → c2(F(b(y0), b(y1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(b(a(b(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
F(a(b(b(y0))), a(b(b(y1)))) → c1(F(b(b(y0)), b(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
S tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(b(y0)), b(b(y1))) → c2(F(b(y0), b(y1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(b(a(b(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
F(a(b(b(y0))), a(b(b(y1)))) → c1(F(b(b(y0)), b(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
A, F
Compound Symbols:
c, c1, c2, c1
(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
b(
b(
y0)),
b(
b(
y1))) →
c2(
F(
b(
y0),
b(
y1))) by
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(b(a(b(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
F(a(b(b(y0))), a(b(b(y1)))) → c1(F(b(b(y0)), b(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
S tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(b(a(b(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
F(a(b(b(y0))), a(b(b(y1)))) → c1(F(b(b(y0)), b(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
A, F
Compound Symbols:
c, c1, c2, c1
(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
b(
a(
b(
y0))),
b(
a(
b(
y1)))) →
c2(
F(
a(
b(
y0)),
a(
b(
y1)))) by
F(b(a(b(b(y0)))), b(a(b(b(y1))))) → c2(F(a(b(b(y0))), a(b(b(y1)))))
F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))) → c2(F(a(b(a(a(y0)))), a(b(a(a(y1))))))
F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))) → c2(F(a(b(a(b(y0)))), a(b(a(b(y1))))))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(a(b(b(y0))), a(b(b(y1)))) → c1(F(b(b(y0)), b(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
F(b(a(b(b(y0)))), b(a(b(b(y1))))) → c2(F(a(b(b(y0))), a(b(b(y1)))))
F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))) → c2(F(a(b(a(a(y0)))), a(b(a(a(y1))))))
F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))) → c2(F(a(b(a(b(y0)))), a(b(a(b(y1))))))
S tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(a(b(b(y0))), a(b(b(y1)))) → c1(F(b(b(y0)), b(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
F(b(a(b(b(y0)))), b(a(b(b(y1))))) → c2(F(a(b(b(y0))), a(b(b(y1)))))
F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))) → c2(F(a(b(a(a(y0)))), a(b(a(a(y1))))))
F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))) → c2(F(a(b(a(b(y0)))), a(b(a(b(y1))))))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
A, F
Compound Symbols:
c, c1, c2, c1
(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
a(
b(
b(
y0))),
a(
b(
b(
y1)))) →
c1(
F(
b(
b(
y0)),
b(
b(
y1)))) by
F(a(b(b(b(y0)))), a(b(b(b(y1))))) → c1(F(b(b(b(y0))), b(b(b(y1)))))
F(a(b(b(a(a(y0))))), a(b(b(a(a(y1)))))) → c1(F(b(b(a(a(y0)))), b(b(a(a(y1))))))
F(a(b(b(a(b(y0))))), a(b(b(a(b(y1)))))) → c1(F(b(b(a(b(y0)))), b(b(a(b(y1))))))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
F(b(a(b(b(y0)))), b(a(b(b(y1))))) → c2(F(a(b(b(y0))), a(b(b(y1)))))
F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))) → c2(F(a(b(a(a(y0)))), a(b(a(a(y1))))))
F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))) → c2(F(a(b(a(b(y0)))), a(b(a(b(y1))))))
F(a(b(b(b(y0)))), a(b(b(b(y1))))) → c1(F(b(b(b(y0))), b(b(b(y1)))))
F(a(b(b(a(a(y0))))), a(b(b(a(a(y1)))))) → c1(F(b(b(a(a(y0)))), b(b(a(a(y1))))))
F(a(b(b(a(b(y0))))), a(b(b(a(b(y1)))))) → c1(F(b(b(a(b(y0)))), b(b(a(b(y1))))))
S tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(F(b(a(b(y0))), b(a(b(y1)))))
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
F(b(a(b(b(y0)))), b(a(b(b(y1))))) → c2(F(a(b(b(y0))), a(b(b(y1)))))
F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))) → c2(F(a(b(a(a(y0)))), a(b(a(a(y1))))))
F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))) → c2(F(a(b(a(b(y0)))), a(b(a(b(y1))))))
F(a(b(b(b(y0)))), a(b(b(b(y1))))) → c1(F(b(b(b(y0))), b(b(b(y1)))))
F(a(b(b(a(a(y0))))), a(b(b(a(a(y1)))))) → c1(F(b(b(a(a(y0)))), b(b(a(a(y1))))))
F(a(b(b(a(b(y0))))), a(b(b(a(b(y1)))))) → c1(F(b(b(a(b(y0)))), b(b(a(b(y1))))))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
A, F
Compound Symbols:
c, c1, c2, c1
(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
a(
b(
a(
b(
y0)))),
a(
b(
a(
b(
y1))))) →
c1(
F(
b(
a(
b(
y0))),
b(
a(
b(
y1))))) by
F(a(b(a(b(b(y0))))), a(b(a(b(b(y1)))))) → c1(F(b(a(b(b(y0)))), b(a(b(b(y1))))))
F(a(b(a(b(a(a(y0)))))), a(b(a(b(a(a(y1))))))) → c1(F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))))
F(a(b(a(b(a(b(y0)))))), a(b(a(b(a(b(y1))))))) → c1(F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))))
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(f(z0, z1))) → f(a(b(a(b(a(z0))))), a(b(a(b(a(z1))))))
f(a(z0), a(z1)) → a(f(z0, z1))
f(b(z0), b(z1)) → b(f(z0, z1))
Tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
F(b(a(b(b(y0)))), b(a(b(b(y1))))) → c2(F(a(b(b(y0))), a(b(b(y1)))))
F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))) → c2(F(a(b(a(a(y0)))), a(b(a(a(y1))))))
F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))) → c2(F(a(b(a(b(y0)))), a(b(a(b(y1))))))
F(a(b(b(b(y0)))), a(b(b(b(y1))))) → c1(F(b(b(b(y0))), b(b(b(y1)))))
F(a(b(b(a(a(y0))))), a(b(b(a(a(y1)))))) → c1(F(b(b(a(a(y0)))), b(b(a(a(y1))))))
F(a(b(b(a(b(y0))))), a(b(b(a(b(y1)))))) → c1(F(b(b(a(b(y0)))), b(b(a(b(y1))))))
F(a(b(a(b(b(y0))))), a(b(a(b(b(y1)))))) → c1(F(b(a(b(b(y0)))), b(a(b(b(y1))))))
F(a(b(a(b(a(a(y0)))))), a(b(a(b(a(a(y1))))))) → c1(F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))))
F(a(b(a(b(a(b(y0)))))), a(b(a(b(a(b(y1))))))) → c1(F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))))
S tuples:
A(a(f(z0, z1))) → c(F(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))), A(z0), A(z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
F(b(a(a(y0))), b(a(a(y1)))) → c2(F(a(a(y0)), a(a(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(b(y0))), b(b(b(y1)))) → c2(F(b(b(y0)), b(b(y1))))
F(b(b(a(a(y0)))), b(b(a(a(y1))))) → c2(F(b(a(a(y0))), b(a(a(y1)))))
F(b(b(a(b(y0)))), b(b(a(b(y1))))) → c2(F(b(a(b(y0))), b(a(b(y1)))))
F(b(a(b(b(y0)))), b(a(b(b(y1))))) → c2(F(a(b(b(y0))), a(b(b(y1)))))
F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))) → c2(F(a(b(a(a(y0)))), a(b(a(a(y1))))))
F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))) → c2(F(a(b(a(b(y0)))), a(b(a(b(y1))))))
F(a(b(b(b(y0)))), a(b(b(b(y1))))) → c1(F(b(b(b(y0))), b(b(b(y1)))))
F(a(b(b(a(a(y0))))), a(b(b(a(a(y1)))))) → c1(F(b(b(a(a(y0)))), b(b(a(a(y1))))))
F(a(b(b(a(b(y0))))), a(b(b(a(b(y1)))))) → c1(F(b(b(a(b(y0)))), b(b(a(b(y1))))))
F(a(b(a(b(b(y0))))), a(b(a(b(b(y1)))))) → c1(F(b(a(b(b(y0)))), b(a(b(b(y1))))))
F(a(b(a(b(a(a(y0)))))), a(b(a(b(a(a(y1))))))) → c1(F(b(a(b(a(a(y0))))), b(a(b(a(a(y1)))))))
F(a(b(a(b(a(b(y0)))))), a(b(a(b(a(b(y1))))))) → c1(F(b(a(b(a(b(y0))))), b(a(b(a(b(y1)))))))
K tuples:none
Defined Rule Symbols:
a, f
Defined Pair Symbols:
A, F
Compound Symbols:
c, c1, c2, c1
(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
b0(0) → 0
a0(0) → 1
f0(0, 0) → 2
f1(0, 0) → 3
b1(3) → 2
b1(3) → 3
(24) BOUNDS(O(1), O(n^1))