(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
b(y, z) → f(c(c(y, z, z), a, a))
b(b(z, y), a) → z
c(f(z), f(c(a, x, a)), y) → c(f(b(x, z)), c(z, y, a), a)
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(c(z0, z1, z1), a, a), C(z0, z1, z1))
C(f(z0), f(c(a, z1, a)), z2) → c3(C(f(b(z1, z0)), c(z0, z2, a), a), B(z1, z0), C(z0, z2, a))
S tuples:
B(z0, z1) → c1(C(c(z0, z1, z1), a, a), C(z0, z1, z1))
C(f(z0), f(c(a, z1, a)), z2) → c3(C(f(b(z1, z0)), c(z0, z2, a), a), B(z1, z0), C(z0, z2, a))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
C(f(z0), f(c(a, z1, a)), z2) → c3(C(f(b(z1, z0)), c(z0, z2, a), a), B(z1, z0), C(z0, z2, a))
B(z0, z1) → c1(C(z0, z1, z1))
S tuples:
C(f(z0), f(c(a, z1, a)), z2) → c3(C(f(b(z1, z0)), c(z0, z2, a), a), B(z1, z0), C(z0, z2, a))
B(z0, z1) → c1(C(z0, z1, z1))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
C, B
Compound Symbols:
c3, c1
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
C(
f(
z0),
f(
c(
a,
z1,
a)),
z2) →
c3(
C(
f(
b(
z1,
z0)),
c(
z0,
z2,
a),
a),
B(
z1,
z0),
C(
z0,
z2,
a)) by
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(C(f(b(x1, f(z0))), c(f(b(z1, z0)), c(z0, a, a), a), a), B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(z1), f(c(a, z0, a)), x2) → c3(C(f(f(c(c(z0, z1, z1), a, a))), c(z1, x2, a), a), B(z0, z1), C(z1, x2, a))
C(f(x0), f(c(a, x1, a)), x2) → c3
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(C(f(b(x1, f(z0))), c(f(b(z1, z0)), c(z0, a, a), a), a), B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(z1), f(c(a, z0, a)), x2) → c3(C(f(f(c(c(z0, z1, z1), a, a))), c(z1, x2, a), a), B(z0, z1), C(z1, x2, a))
C(f(x0), f(c(a, x1, a)), x2) → c3
S tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(C(f(b(x1, f(z0))), c(f(b(z1, z0)), c(z0, a, a), a), a), B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(z1), f(c(a, z0, a)), x2) → c3(C(f(f(c(c(z0, z1, z1), a, a))), c(z1, x2, a), a), B(z0, z1), C(z1, x2, a))
C(f(x0), f(c(a, x1, a)), x2) → c3
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3, c3
(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
C(f(x0), f(c(a, x1, a)), x2) → c3
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(C(f(b(x1, f(z0))), c(f(b(z1, z0)), c(z0, a, a), a), a), B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(z1), f(c(a, z0, a)), x2) → c3(C(f(f(c(c(z0, z1, z1), a, a))), c(z1, x2, a), a), B(z0, z1), C(z1, x2, a))
S tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(C(f(b(x1, f(z0))), c(f(b(z1, z0)), c(z0, a, a), a), a), B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(z1), f(c(a, z0, a)), x2) → c3(C(f(f(c(c(z0, z1, z1), a, a))), c(z1, x2, a), a), B(z0, z1), C(z1, x2, a))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3
(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(z1), f(c(a, z0, a)), x2) → c3(C(f(f(c(c(z0, z1, z1), a, a))), c(z1, x2, a), a), B(z0, z1), C(z1, x2, a))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
S tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(z1), f(c(a, z0, a)), x2) → c3(C(f(f(c(c(z0, z1, z1), a, a))), c(z1, x2, a), a), B(z0, z1), C(z1, x2, a))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3, c3
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
C(
f(
z1),
f(
c(
a,
z0,
a)),
x2) →
c3(
C(
f(
f(
c(
c(
z0,
z1,
z1),
a,
a))),
c(
z1,
x2,
a),
a),
B(
z0,
z1),
C(
z1,
x2,
a)) by
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(C(f(f(c(c(x1, f(z0), f(z0)), a, a))), c(f(b(z1, z0)), c(z0, a, a), a), a), B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z1, a))), f(c(a, f(z0), a)), x2) → c3(C(f(f(c(c(f(b(z1, z0)), c(z0, f(c(a, z1, a)), a), a), a, a))), c(f(c(a, z1, a)), x2, a), a), B(f(z0), f(c(a, z1, a))), C(f(c(a, z1, a)), x2, a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(C(f(f(c(c(x1, f(z0), f(z0)), a, a))), c(f(b(z1, z0)), c(z0, a, a), a), a), B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z1, a))), f(c(a, f(z0), a)), x2) → c3(C(f(f(c(c(f(b(z1, z0)), c(z0, f(c(a, z1, a)), a), a), a, a))), c(f(c(a, z1, a)), x2, a), a), B(f(z0), f(c(a, z1, a))), C(f(c(a, z1, a)), x2, a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
S tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(C(f(f(c(c(x1, f(z0), f(z0)), a, a))), c(f(b(z1, z0)), c(z0, a, a), a), a), B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z1, a))), f(c(a, f(z0), a)), x2) → c3(C(f(f(c(c(f(b(z1, z0)), c(z0, f(c(a, z1, a)), a), a), a, a))), c(f(c(a, z1, a)), x2, a), a), B(f(z0), f(c(a, z1, a))), C(f(c(a, z1, a)), x2, a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3, c3, c3
(13) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z1, a))), f(c(a, f(z0), a)), x2) → c3(C(f(f(c(c(f(b(z1, z0)), c(z0, f(c(a, z1, a)), a), a), a, a))), c(f(c(a, z1, a)), x2, a), a), B(f(z0), f(c(a, z1, a))), C(f(c(a, z1, a)), x2, a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
S tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z1, a))), f(c(a, f(z0), a)), x2) → c3(C(f(f(c(c(f(b(z1, z0)), c(z0, f(c(a, z1, a)), a), a), a, a))), c(f(c(a, z1, a)), x2, a), a), B(f(z0), f(c(a, z1, a))), C(f(c(a, z1, a)), x2, a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3, c3, c3
(15) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
C(
f(
f(
c(
a,
z1,
a))),
f(
c(
a,
f(
z0),
a)),
x2) →
c3(
C(
f(
f(
c(
c(
f(
b(
z1,
z0)),
c(
z0,
f(
c(
a,
z1,
a)),
a),
a),
a,
a))),
c(
f(
c(
a,
z1,
a)),
x2,
a),
a),
B(
f(
z0),
f(
c(
a,
z1,
a))),
C(
f(
c(
a,
z1,
a)),
x2,
a)) by
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), a, a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), a, a))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(C(f(f(c(c(f(b(a, z1)), c(z1, f(c(a, a, a)), a), a), a, a))), c(f(c(a, a, a)), a, a), a), B(f(z1), f(c(a, a, a))), C(f(c(a, a, a)), a, a))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), a, a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), a, a))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(C(f(f(c(c(f(b(a, z1)), c(z1, f(c(a, a, a)), a), a), a, a))), c(f(c(a, a, a)), a, a), a), B(f(z1), f(c(a, a, a))), C(f(c(a, a, a)), a, a))
S tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), a, a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), a, a))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(C(f(f(c(c(f(b(a, z1)), c(z1, f(c(a, a, a)), a), a), a, a))), c(f(c(a, a, a)), a, a), a), B(f(z1), f(c(a, a, a))), C(f(c(a, a, a)), a, a))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3, c3, c3
(17) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, z0, a))))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, a, a))))
S tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(x0), f(c(a, x1, a)), x2) → c3(B(x1, x0))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, z0, a))))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, a, a))))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3, c3, c3
(19) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
C(
f(
x0),
f(
c(
a,
x1,
a)),
x2) →
c3(
B(
x1,
x0)) by
C(f(z0), f(c(a, z1, a)), f(c(a, z1, a))) → c3(B(z1, z0))
C(f(x0), f(c(a, x2, a)), a) → c3(B(x2, x0))
C(f(f(c(y2, a, a))), f(c(a, z1, a)), a) → c3(B(z1, f(c(y2, a, a))))
C(f(c(a, x0, a)), f(c(a, f(x1), a)), a) → c3(B(f(x1), c(a, x0, a)))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, z0, a))))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, a, a))))
C(f(z0), f(c(a, z1, a)), f(c(a, z1, a))) → c3(B(z1, z0))
C(f(x0), f(c(a, x2, a)), a) → c3(B(x2, x0))
C(f(f(c(y2, a, a))), f(c(a, z1, a)), a) → c3(B(z1, f(c(y2, a, a))))
C(f(c(a, x0, a)), f(c(a, f(x1), a)), a) → c3(B(f(x1), c(a, x0, a)))
S tuples:
B(z0, z1) → c1(C(z0, z1, z1))
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, z0, a))))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, a, a))))
C(f(z0), f(c(a, z1, a)), f(c(a, z1, a))) → c3(B(z1, z0))
C(f(x0), f(c(a, x2, a)), a) → c3(B(x2, x0))
C(f(f(c(y2, a, a))), f(c(a, z1, a)), a) → c3(B(z1, f(c(y2, a, a))))
C(f(c(a, x0, a)), f(c(a, f(x1), a)), a) → c3(B(f(x1), c(a, x0, a)))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
B, C
Compound Symbols:
c1, c3, c3, c3
(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
B(
z0,
z1) →
c1(
C(
z0,
z1,
z1)) by
B(f(f(y0)), f(c(a, y1, a))) → c1(C(f(f(y0)), f(c(a, y1, a)), f(c(a, y1, a))))
B(f(f(c(a, y0, a))), f(c(a, f(y1), a))) → c1(C(f(f(c(a, y0, a))), f(c(a, f(y1), a)), f(c(a, f(y1), a))))
B(f(y0), f(c(a, y1, a))) → c1(C(f(y0), f(c(a, y1, a)), f(c(a, y1, a))))
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, z0, a))))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, a, a))))
C(f(z0), f(c(a, z1, a)), f(c(a, z1, a))) → c3(B(z1, z0))
C(f(x0), f(c(a, x2, a)), a) → c3(B(x2, x0))
C(f(f(c(y2, a, a))), f(c(a, z1, a)), a) → c3(B(z1, f(c(y2, a, a))))
C(f(c(a, x0, a)), f(c(a, f(x1), a)), a) → c3(B(f(x1), c(a, x0, a)))
B(f(f(y0)), f(c(a, y1, a))) → c1(C(f(f(y0)), f(c(a, y1, a)), f(c(a, y1, a))))
B(f(f(c(a, y0, a))), f(c(a, f(y1), a))) → c1(C(f(f(c(a, y0, a))), f(c(a, f(y1), a)), f(c(a, f(y1), a))))
B(f(y0), f(c(a, y1, a))) → c1(C(f(y0), f(c(a, y1, a)), f(c(a, y1, a))))
S tuples:
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, z0, a))))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, a, a))))
C(f(z0), f(c(a, z1, a)), f(c(a, z1, a))) → c3(B(z1, z0))
C(f(x0), f(c(a, x2, a)), a) → c3(B(x2, x0))
C(f(f(c(y2, a, a))), f(c(a, z1, a)), a) → c3(B(z1, f(c(y2, a, a))))
C(f(c(a, x0, a)), f(c(a, f(x1), a)), a) → c3(B(f(x1), c(a, x0, a)))
B(f(f(y0)), f(c(a, y1, a))) → c1(C(f(f(y0)), f(c(a, y1, a)), f(c(a, y1, a))))
B(f(f(c(a, y0, a))), f(c(a, f(y1), a))) → c1(C(f(f(c(a, y0, a))), f(c(a, f(y1), a)), f(c(a, f(y1), a))))
B(f(y0), f(c(a, y1, a))) → c1(C(f(y0), f(c(a, y1, a)), f(c(a, y1, a))))
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:
C, B
Compound Symbols:
c3, c3, c3, c1
(23) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
C(f(f(z0)), f(c(a, x1, a)), f(c(a, z1, a))) → c3(B(x1, f(z0)), C(f(z0), f(c(a, z1, a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), f(c(a, f(z1), a))) → c3(C(f(f(c(c(f(b(z0, z1)), c(z1, f(c(a, z0, a)), a), a), a, a))), c(f(c(a, z0, a)), f(c(a, f(z1), a)), a), a), B(f(z1), f(c(a, z0, a))), C(f(c(a, z0, a)), f(c(a, f(z1), a)), a))
C(f(f(c(a, z0, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, z0, a))))
C(f(f(c(a, a, a))), f(c(a, f(z1), a)), a) → c3(B(f(z1), f(c(a, a, a))))
C(f(z0), f(c(a, z1, a)), f(c(a, z1, a))) → c3(B(z1, z0))
C(f(x0), f(c(a, x2, a)), a) → c3(B(x2, x0))
C(f(f(c(y2, a, a))), f(c(a, z1, a)), a) → c3(B(z1, f(c(y2, a, a))))
C(f(c(a, x0, a)), f(c(a, f(x1), a)), a) → c3(B(f(x1), c(a, x0, a)))
B(f(f(y0)), f(c(a, y1, a))) → c1(C(f(f(y0)), f(c(a, y1, a)), f(c(a, y1, a))))
B(f(f(c(a, y0, a))), f(c(a, f(y1), a))) → c1(C(f(f(c(a, y0, a))), f(c(a, f(y1), a)), f(c(a, f(y1), a))))
B(f(y0), f(c(a, y1, a))) → c1(C(f(y0), f(c(a, y1, a)), f(c(a, y1, a))))
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
b(z0, z1) → f(c(c(z0, z1, z1), a, a))
b(b(z0, z1), a) → z0
c(f(z0), f(c(a, z1, a)), z2) → c(f(b(z1, z0)), c(z0, z2, a), a)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
b, c
Defined Pair Symbols:none
Compound Symbols:none
(25) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(26) BOUNDS(O(1), O(1))