The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 1 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 11 ms)
    ↳20 CdtProblem
↳21 CpxTrsMatchBoundsTAProof (⇔, 14 ms)
↳22 BOUNDS(O(1), O(n^1))

(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) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace 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)) by

A(a(f(a(f(z0, z1)), x1))) → c(F(a(b(a(b(a(a(f(z0, z1))))))), a(b(a(b(a(x1)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))

(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(a(f(z0, z1)), x1))) → c(F(a(b(a(b(a(a(f(z0, z1))))))), a(b(a(b(a(x1)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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(a(f(z0, z1)), x1))) → c(F(a(b(a(b(a(a(f(z0, z1))))))), a(b(a(b(a(x1)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c1, c2, c, 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(a(f(z0, z1)), x1))) → c(F(a(b(a(b(a(a(f(z0, z1))))))), a(b(a(b(a(x1)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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(a(f(z0, z1)), x1))) → c(F(a(b(a(b(a(a(f(z0, z1))))))), a(b(a(b(a(x1)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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, 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(a(f(z0, z1)), x1))) → c(F(a(b(a(b(a(a(f(z0, z1))))))), a(b(a(b(a(x1)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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(a(f(z0, z1)), x1))) → c(F(a(b(a(b(a(a(f(z0, z1))))))), a(b(a(b(a(x1)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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, c, c1

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

Use narrowing to replace A(a(f(a(f(z0, z1)), x1))) → c(F(a(b(a(b(a(a(f(z0, z1))))))), a(b(a(b(a(x1)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1)) by

A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(a(f(x0, x1)), x2))) → c(A(b(a(b(f(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))))))

(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(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(a(f(x0, x1)), x2))) → c(A(b(a(b(f(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))))))
S tuples:

F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(a(f(x0, x1)), x2))) → c(A(b(a(b(f(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))))))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c2, c, c1, c, c

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

Removed 1 trailing nodes:

A(a(f(a(f(x0, x1)), x2))) → c(A(b(a(b(f(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))))))

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

F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
S tuples:

F(b(z0), b(z1)) → c2(F(z0, z1))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1))
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)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c2, c, c1, c

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

Use narrowing to replace A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))), A(b(a(b(a(x1))))), A(b(a(x1))), A(x1)) by

A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))

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

F(b(z0), b(z1)) → c2(F(z0, 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)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))
S tuples:

F(b(z0), b(z1)) → c2(F(z0, 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)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c2, c1, c, c, c

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

Use narrowing to replace F(a(b(z0)), a(b(z1))) → c1(A(b(f(z0, z1))), F(b(z0), b(z1))) by

F(a(b(a(z0))), a(b(a(z1)))) → c1(A(b(a(f(z0, z1)))), F(b(a(z0)), b(a(z1))))
F(a(b(b(z0))), a(b(b(z1)))) → c1(A(b(b(f(z0, z1)))), F(b(b(z0)), b(b(z1))))
F(a(b(x0)), a(b(x1))) → c1(F(b(x0), b(x1)))

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

F(b(z0), b(z1)) → c2(F(z0, z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))
F(a(b(a(z0))), a(b(a(z1)))) → c1(A(b(a(f(z0, z1)))), F(b(a(z0)), b(a(z1))))
F(a(b(b(z0))), a(b(b(z1)))) → c1(A(b(b(f(z0, z1)))), F(b(b(z0)), b(b(z1))))
F(a(b(x0)), a(b(x1))) → c1(F(b(x0), b(x1)))
S tuples:

F(b(z0), b(z1)) → c2(F(z0, z1))
F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))
F(a(b(a(z0))), a(b(a(z1)))) → c1(A(b(a(f(z0, z1)))), F(b(a(z0)), b(a(z1))))
F(a(b(b(z0))), a(b(b(z1)))) → c1(A(b(b(f(z0, z1)))), F(b(b(z0)), b(b(z1))))
F(a(b(x0)), a(b(x1))) → c1(F(b(x0), b(x1)))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c2, c1, c, c, c, c1

(17) 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(a(y0)))), b(a(b(a(y1))))) → c2(F(a(b(a(y0))), a(b(a(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(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), 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:

F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))
F(a(b(a(z0))), a(b(a(z1)))) → c1(A(b(a(f(z0, z1)))), F(b(a(z0)), b(a(z1))))
F(a(b(b(z0))), a(b(b(z1)))) → c1(A(b(b(f(z0, z1)))), F(b(b(z0)), b(b(z1))))
F(a(b(x0)), a(b(x1))) → c1(F(b(x0), b(x1)))
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(a(y0)))), b(a(b(a(y1))))) → c2(F(a(b(a(y0))), a(b(a(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(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
S tuples:

F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))
F(a(b(a(z0))), a(b(a(z1)))) → c1(A(b(a(f(z0, z1)))), F(b(a(z0)), b(a(z1))))
F(a(b(b(z0))), a(b(b(z1)))) → c1(A(b(b(f(z0, z1)))), F(b(b(z0)), b(b(z1))))
F(a(b(x0)), a(b(x1))) → c1(F(b(x0), b(x1)))
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(a(y0)))), b(a(b(a(y1))))) → c2(F(a(b(a(y0))), a(b(a(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(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c1, c, c, c, c1, c2

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

Use forward instantiation to replace F(a(b(a(z0))), a(b(a(z1)))) → c1(A(b(a(f(z0, z1)))), F(b(a(z0)), b(a(z1)))) by

F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(A(b(a(f(a(y0), a(y1))))), F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(a(y0))))), a(b(a(b(a(y1)))))) → c1(A(b(a(f(b(a(y0)), b(a(y1)))))), F(b(a(b(a(y0)))), b(a(b(a(y1))))))
F(a(b(a(b(b(y0))))), a(b(a(b(b(y1)))))) → c1(A(b(a(f(b(b(y0)), b(b(y1)))))), F(b(a(b(b(y0)))), b(a(b(b(y1))))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(A(b(a(f(b(y0), b(y1))))), F(b(a(b(y0))), 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:

F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))
F(a(b(b(z0))), a(b(b(z1)))) → c1(A(b(b(f(z0, z1)))), F(b(b(z0)), b(b(z1))))
F(a(b(x0)), a(b(x1))) → c1(F(b(x0), b(x1)))
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(a(y0)))), b(a(b(a(y1))))) → c2(F(a(b(a(y0))), a(b(a(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(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(A(b(a(f(a(y0), a(y1))))), F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(a(y0))))), a(b(a(b(a(y1)))))) → c1(A(b(a(f(b(a(y0)), b(a(y1)))))), F(b(a(b(a(y0)))), b(a(b(a(y1))))))
F(a(b(a(b(b(y0))))), a(b(a(b(b(y1)))))) → c1(A(b(a(f(b(b(y0)), b(b(y1)))))), F(b(a(b(b(y0)))), b(a(b(b(y1))))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(A(b(a(f(b(y0), b(y1))))), F(b(a(b(y0))), b(a(b(y1)))))
S tuples:

F(a(a(z0)), a(a(z1))) → c1(A(a(f(z0, z1))), F(a(z0), a(z1)))
A(a(f(a(f(z0, z1)), x2))) → c(F(a(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), a(b(a(b(a(x2)))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))), A(b(a(b(a(x2))))), A(b(a(x2))), A(x2))
A(a(f(x0, a(f(z0, z1))))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(a(f(z0, z1)))))))), A(b(a(b(f(a(b(a(b(a(z0))))), a(b(a(b(a(z1)))))))))), A(b(a(a(f(z0, z1))))), A(a(f(z0, z1))))
A(a(f(x0, x1))) → c(F(a(b(a(b(a(x0))))), a(b(a(b(a(x1)))))))
F(a(b(b(z0))), a(b(b(z1)))) → c1(A(b(b(f(z0, z1)))), F(b(b(z0)), b(b(z1))))
F(a(b(x0)), a(b(x1))) → c1(F(b(x0), b(x1)))
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(a(y0)))), b(a(b(a(y1))))) → c2(F(a(b(a(y0))), a(b(a(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(y0))), b(a(b(y1)))) → c2(F(a(b(y0)), a(b(y1))))
F(a(b(a(a(y0)))), a(b(a(a(y1))))) → c1(A(b(a(f(a(y0), a(y1))))), F(b(a(a(y0))), b(a(a(y1)))))
F(a(b(a(b(a(y0))))), a(b(a(b(a(y1)))))) → c1(A(b(a(f(b(a(y0)), b(a(y1)))))), F(b(a(b(a(y0)))), b(a(b(a(y1))))))
F(a(b(a(b(b(y0))))), a(b(a(b(b(y1)))))) → c1(A(b(a(f(b(b(y0)), b(b(y1)))))), F(b(a(b(b(y0)))), b(a(b(b(y1))))))
F(a(b(a(b(y0)))), a(b(a(b(y1))))) → c1(A(b(a(f(b(y0), b(y1))))), F(b(a(b(y0))), b(a(b(y1)))))
K tuples:none
Defined Rule Symbols:

a, f

Defined Pair Symbols:

F, A

Compound Symbols:

c1, c, c, c, c1, c2

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

(22) BOUNDS(O(1), O(n^1))