Runtime Complexity (innermost) proof of /tmp/tmplI0KJQ/z07.xml

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 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳4 CdtProblem

    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 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 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳16 CdtProblem

    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳22 CdtProblem

    ↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳24 CdtProblem

    ↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳26 CdtProblem

    ↳27 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳28 CdtProblem

    ↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 32 ms)

    ↳30 CdtProblem

    ↳31 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳32 CdtProblem

    ↳33 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳34 CdtProblem

↳35 CpxTrsMatchBoundsTAProof (⇔, 0 ms)

↳36 BOUNDS(O(1), O(n^1))

(0) Obligation:

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

f(a, x) → f(b, f(c, x))
f(a, f(b, x)) → f(b, f(a, x))
f(d, f(c, x)) → f(d, f(a, x))
f(a, f(c, x)) → f(c, f(a, x))

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, z0) → c1(F(b, f(c, z0)), F(c, z0))
F(a, f(b, z0)) → c2(F(b, f(a, z0)), F(a, z0))
F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0))
F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))

S tuples:

F(a, z0) → c1(F(b, f(c, z0)), F(c, z0))
F(a, f(b, z0)) → c2(F(b, f(a, z0)), F(a, z0))
F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0))
F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c3, c4

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

Removed 1 trailing nodes:

F(a, z0) → c1(F(b, f(c, z0)), F(c, z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, f(b, z0)) → c2(F(b, f(a, z0)), F(a, z0))
F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0))
F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))

S tuples:

F(a, f(b, z0)) → c2(F(b, f(a, z0)), F(a, z0))
F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0))
F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4

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

Use narrowing to replace F(a, f(b, z0)) → c2(F(b, f(a, z0)), F(a, z0)) by

F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0))
F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))
F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2

S tuples:

F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0))
F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))
F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c4, c2, c2

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

Removed 1 trailing nodes:

F(a, f(b, x0)) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0))
F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))
F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))

S tuples:

F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0))
F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))
F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c4, c2

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

Use narrowing to replace F(d, f(c, z0)) → c3(F(d, f(a, z0)), F(a, z0)) by

F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, x0)) → c3

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))
F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, x0)) → c3

S tuples:

F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))
F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, x0)) → c3

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c4, c2, c3, c3

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

Removed 1 trailing nodes:

F(d, f(c, x0)) → c3

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))
F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))

S tuples:

F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0))
F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c4, c2, c3

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

Use narrowing to replace F(a, f(c, z0)) → c4(F(c, f(a, z0)), F(a, z0)) by

F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, x0)) → c4

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, x0)) → c4

S tuples:

F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, x0)) → c4

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4, c4

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

Removed 1 trailing nodes:

F(a, f(c, x0)) → c4

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))

S tuples:

F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4

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

Use narrowing to replace F(a, f(b, z0)) → c2(F(b, f(b, f(c, z0))), F(a, z0)) by

F(a, f(b, x0)) → c2(F(a, x0))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))

S tuples:

F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4, c2

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

Use narrowing to replace F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(a, z0))), F(a, f(b, z0))) by

F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(b, x0))) → c2

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(b, x0))) → c2

S tuples:

F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(b, x0))) → c2

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4, c2, c2

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

Removed 1 trailing nodes:

F(a, f(b, f(b, x0))) → c2

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))

S tuples:

F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0)))
F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4, c2

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

Use narrowing to replace F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(a, z0))), F(a, f(c, z0))) by

F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(a, f(b, f(c, x0))) → c2

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(a, f(b, f(c, x0))) → c2

S tuples:

F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(a, f(b, f(c, x0))) → c2

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c4, c2, c2, c2

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

Removed 1 trailing nodes:

F(a, f(b, f(c, x0))) → c2

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))

S tuples:

F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c4, c2, c2

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

Use narrowing to replace F(d, f(c, z0)) → c3(F(d, f(b, f(c, z0))), F(a, z0)) by

F(d, f(c, x0)) → c3(F(a, x0))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(d, f(c, x0)) → c3(F(a, x0))

S tuples:

F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(d, f(c, x0)) → c3(F(a, x0))

K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c4, c2, c2, c3

(29) 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(d, f(c, x0)) → c3(F(a, x0))

We considered the (Usable) Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

And the Tuples:

F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(d, f(c, x0)) → c3(F(a, x0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x₁, x₂)) = x₁
POL(a) = 0
POL(b) = 0
POL(c) = 0
POL(c2(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁, x₂)) = x₁ + x₂
POL(d) = [1]
POL(f(x₁, x₂)) = [2]

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(d, f(c, x0)) → c3(F(a, x0))

S tuples:

F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0)))
F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))

K tuples:

F(d, f(c, x0)) → c3(F(a, x0))

Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c4, c2, c2, c3

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

Use narrowing to replace F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(a, z0))), F(a, f(b, z0))) by

F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(d, f(c, f(b, f(b, z0)))) → c3(F(d, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(d, f(c, f(b, f(c, z0)))) → c3(F(d, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(d, f(c, f(b, x0))) → c3

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(d, f(c, x0)) → c3(F(a, x0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(d, f(c, f(b, f(b, z0)))) → c3(F(d, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(d, f(c, f(b, f(c, z0)))) → c3(F(d, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(d, f(c, f(b, x0))) → c3

S tuples:

F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(d, f(c, f(b, f(b, z0)))) → c3(F(d, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(d, f(c, f(b, f(c, z0)))) → c3(F(d, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(d, f(c, f(b, x0))) → c3

K tuples:

F(d, f(c, x0)) → c3(F(a, x0))

Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c4, c2, c2, c3, c3

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

Removed 1 trailing nodes:

F(d, f(c, f(b, x0))) → c3

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(a, z0) → f(b, f(c, z0))
f(a, f(b, z0)) → f(b, f(a, z0))
f(d, f(c, z0)) → f(d, f(a, z0))
f(a, f(c, z0)) → f(c, f(a, z0))

Tuples:

F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(d, f(c, x0)) → c3(F(a, x0))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(d, f(c, f(b, f(b, z0)))) → c3(F(d, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(d, f(c, f(b, f(c, z0)))) → c3(F(d, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))

S tuples:

F(d, f(c, f(c, z0))) → c3(F(d, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(c, z0)) → c4(F(c, f(b, f(c, z0))), F(a, z0))
F(a, f(c, f(b, z0))) → c4(F(c, f(b, f(a, z0))), F(a, f(b, z0)))
F(a, f(c, f(c, z0))) → c4(F(c, f(c, f(a, z0))), F(a, f(c, z0)))
F(a, f(b, x0)) → c2(F(a, x0))
F(a, f(b, f(b, z0))) → c2(F(b, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(a, f(b, f(b, f(b, z0)))) → c2(F(b, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, f(c, z0)))) → c2(F(b, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))
F(a, f(b, f(c, z0))) → c2(F(b, f(c, f(b, f(c, z0)))), F(a, f(c, z0)))
F(a, f(b, f(c, f(b, z0)))) → c2(F(b, f(c, f(b, f(a, z0)))), F(a, f(c, f(b, z0))))
F(a, f(b, f(c, f(c, z0)))) → c2(F(b, f(c, f(c, f(a, z0)))), F(a, f(c, f(c, z0))))
F(d, f(c, f(b, z0))) → c3(F(d, f(b, f(b, f(c, z0)))), F(a, f(b, z0)))
F(d, f(c, f(b, f(b, z0)))) → c3(F(d, f(b, f(b, f(a, z0)))), F(a, f(b, f(b, z0))))
F(d, f(c, f(b, f(c, z0)))) → c3(F(d, f(b, f(c, f(a, z0)))), F(a, f(b, f(c, z0))))

K tuples:

F(d, f(c, x0)) → c3(F(a, x0))

Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c4, c2, c2, c3

(35) 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]
transitions:
a0() → 0
b0() → 0
c0() → 0
d0() → 0
f0(0, 0) → 1
b1() → 2
c1() → 4
f1(4, 0) → 3
f1(2, 3) → 1

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

(35) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

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