(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
a(C(x1, x2), y, z) → C(a(x1, y, z), a(x2, y, y))
a(Z, y, z) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
a(C(z0, z1), z2, z3) → C(a(z0, z2, z3), a(z1, z2, z2))
a(Z, z0, z1) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
Tuples:
AND(False, False) → c
AND(True, False) → c1
AND(False, True) → c2
AND(True, True) → c3
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
A(Z, z0, z1) → c5
EQZLIST(C(z0, z1), C(z2, z3)) → c6(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
EQZLIST(C(z0, z1), Z) → c7
EQZLIST(Z, C(z0, z1)) → c8
EQZLIST(Z, Z) → c9
SECOND(C(z0, z1)) → c10
FIRST(C(z0, z1)) → c11
S tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
A(Z, z0, z1) → c5
EQZLIST(C(z0, z1), C(z2, z3)) → c6(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
EQZLIST(C(z0, z1), Z) → c7
EQZLIST(Z, C(z0, z1)) → c8
EQZLIST(Z, Z) → c9
SECOND(C(z0, z1)) → c10
FIRST(C(z0, z1)) → c11
K tuples:none
Defined Rule Symbols:
a, eqZList, second, first, and
Defined Pair Symbols:
AND, A, EQZLIST, SECOND, FIRST
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 10 trailing nodes:
EQZLIST(Z, C(z0, z1)) → c8
FIRST(C(z0, z1)) → c11
AND(False, True) → c2
SECOND(C(z0, z1)) → c10
AND(False, False) → c
EQZLIST(C(z0, z1), Z) → c7
A(Z, z0, z1) → c5
AND(True, False) → c1
EQZLIST(Z, Z) → c9
AND(True, True) → c3
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
a(C(z0, z1), z2, z3) → C(a(z0, z2, z3), a(z1, z2, z2))
a(Z, z0, z1) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
Tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:
a, eqZList, second, first, and
Defined Pair Symbols:
A, EQZLIST
Compound Symbols:
c4, c6
(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
a(C(z0, z1), z2, z3) → C(a(z0, z2, z3), a(z1, z2, z2))
a(Z, z0, z1) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
Tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:
a, eqZList, second, first, and
Defined Pair Symbols:
A, EQZLIST
Compound Symbols:
c4, c6
(7) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
a(C(z0, z1), z2, z3) → C(a(z0, z2, z3), a(z1, z2, z2))
a(Z, z0, z1) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:
A, EQZLIST
Compound Symbols:
c4, c6
(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))
We considered the (Usable) Rules:none
And the Tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(A(x1, x2, x3)) = [4]x1
POL(C(x1, x2)) = [1] + x1 + x2
POL(EQZLIST(x1, x2)) = [5] + [4]x1 + [4]x2
POL(c4(x1, x2)) = x1 + x2
POL(c6(x1, x2)) = x1 + x2
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:none
K tuples:
A(C(z0, z1), z2, z3) → c4(A(z0, z2, z3), A(z1, z2, z2))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))
Defined Rule Symbols:none
Defined Pair Symbols:
A, EQZLIST
Compound Symbols:
c4, c6
(11) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(12) BOUNDS(1, 1)