(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(x, c(x), c(y)) → f(y, y, f(y, x, y))
f(s(x), y, z) → f(x, s(c(y)), c(z))
f(c(x), x, y) → c(y)
g(x, y) → x
g(x, y) → y
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1
Tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5
S tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F, G
Compound Symbols:
c1, c2, c3, c4, c5
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
G(z0, z1) → c4
F(c(z0), z0, z1) → c3
G(z0, z1) → c5
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1
Tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
S tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
(5) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
g(z0, z1) → z0
g(z0, z1) → z1
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
S tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
z0,
c(
z0),
c(
z1)) →
c1(
F(
z1,
z1,
f(
z1,
z0,
z1)),
F(
z1,
z0,
z1)) by
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1
(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1
(11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c1
(13) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c3
(15) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c3
(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
We considered the (Usable) Rules:none
And the Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F(x1, x2, x3)) = [4]x2
POL(c(x1)) = [2] + x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(f(x1, x2, x3)) = [3] + [2]x2 + [2]x3
POL(s(x1)) = 0
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c3
(19) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
s(
z0),
z1,
z2) →
c2(
F(
z0,
s(
c(
z1)),
c(
z2))) by
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
S tuples:
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c3, c2
(21) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
S tuples:
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c3, c2
(23) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
z1,
c(
z1),
c(
s(
z0))) →
c3(
F(
s(
z0),
s(
z0),
f(
z0,
s(
c(
z1)),
c(
s(
z0))))) by
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
S tuples:
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c3, c2
(25) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
z1,
c(
z1),
c(
s(
z0))) →
c3(
F(
s(
z0),
z1,
s(
z0))) by
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
S tuples:
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c3
(27) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
We considered the (Usable) Rules:
f(c(z0), z0, z1) → c(z1)
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
And the Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F(x1, x2, x3)) = [4]x1 + [4]x3
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(f(x1, x2, x3)) = x3
POL(s(x1)) = [1] + x1
(28) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
S tuples:none
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c3
(29) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(30) BOUNDS(1, 1)