79.26/23.00
79.26/23.00
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(f(x)) → mark(f(f(x)))
79.26/23.00
chk(no(f(x))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
79.26/23.00
mat(f(x), f(y)) → f(mat(x, y))
79.26/23.00
chk(no(c)) → active(c)
79.26/23.00
mat(f(x), c) → no(c)
79.26/23.00
f(active(x)) → active(f(x))
79.26/23.00
f(no(x)) → no(f(x))
79.26/23.00
f(mark(x)) → mark(f(x))
79.26/23.00
tp(mark(x)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
Rewrite Strategy: INNERMOST
79.26/23.00
79.26/23.00
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
79.26/23.00
79.26/23.00
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.26/23.00
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.26/23.00
chk(no(c)) → active(c)
79.26/23.00
mat(f(z0), f(y)) → f(mat(z0, y))
79.26/23.00
mat(f(z0), c) → no(c)
79.26/23.00
f(active(z0)) → active(f(z0))
79.26/23.00
f(no(z0)) → no(f(z0))
79.26/23.00
f(mark(z0)) → mark(f(z0))
79.26/23.00
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
ACTIVE(f(z0)) → c1(F(f(z0)), F(z0))
79.26/23.00
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
79.26/23.00
CHK(no(c)) → c3(ACTIVE(c))
79.26/23.00
MAT(f(z0), f(y)) → c4(F(mat(z0, y)), MAT(z0, y))
79.26/23.00
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.26/23.00
F(no(z0)) → c7(F(z0))
79.26/23.00
F(mark(z0)) → c8(F(z0))
79.26/23.00
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
S tuples:
ACTIVE(f(z0)) → c1(F(f(z0)), F(z0))
79.26/23.00
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
79.26/23.00
CHK(no(c)) → c3(ACTIVE(c))
79.26/23.00
MAT(f(z0), f(y)) → c4(F(mat(z0, y)), MAT(z0, y))
79.26/23.00
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.26/23.00
F(no(z0)) → c7(F(z0))
79.26/23.00
F(mark(z0)) → c8(F(z0))
79.26/23.00
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
K tuples:none
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
ACTIVE, CHK, MAT, F, TP
Compound Symbols:
c1, c2, c3, c4, c6, c7, c8, c9
79.26/23.00
79.26/23.00
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 24 trailing tuple parts
79.26/23.00
79.26/23.00
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.26/23.00
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.26/23.00
chk(no(c)) → active(c)
79.26/23.00
mat(f(z0), f(y)) → f(mat(z0, y))
79.26/23.00
mat(f(z0), c) → no(c)
79.26/23.00
f(active(z0)) → active(f(z0))
79.26/23.00
f(no(z0)) → no(f(z0))
79.26/23.00
f(mark(z0)) → mark(f(z0))
79.26/23.00
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.06
F(no(z0)) → c7(F(z0))
79.89/23.06
F(mark(z0)) → c8(F(z0))
79.89/23.06
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.06
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.06
CHK(no(c)) → c3
79.89/23.06
MAT(f(z0), f(y)) → c4
79.89/23.06
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.06
F(no(z0)) → c7(F(z0))
79.89/23.06
F(mark(z0)) → c8(F(z0))
79.89/23.06
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.06
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.06
CHK(no(c)) → c3
79.89/23.06
MAT(f(z0), f(y)) → c4
79.89/23.06
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
K tuples:none
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c2, c3, c4, c9
79.89/23.09
79.89/23.09
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
79.89/23.09
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
chk(no(c)) → active(c)
79.89/23.09
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
K tuples:none
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c2, c3, c4, c9
79.89/23.09
79.89/23.09
(7) 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.
MAT(f(z0), f(y)) → c4
We considered the (Usable) Rules:
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
chk(no(c)) → active(c)
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
active(f(z0)) → mark(f(f(z0)))
And the Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
79.89/23.09
POL(ACTIVE(x1)) = 0
79.89/23.09
POL(CHK(x1)) = x1
79.89/23.09
POL(F(x1)) = 0
79.89/23.09
POL(MAT(x1, x2)) = x2
79.89/23.09
POL(TP(x1)) = [2]x1
79.89/23.09
POL(X) = 0
79.89/23.09
POL(active(x1)) = [4]x1
79.89/23.09
POL(c) = 0
79.89/23.09
POL(c1(x1)) = x1
79.89/23.09
POL(c2(x1, x2, x3)) = x1 + x2 + x3
79.89/23.09
POL(c3) = 0
79.89/23.09
POL(c4) = 0
79.89/23.09
POL(c6(x1, x2)) = x1 + x2
79.89/23.09
POL(c7(x1)) = x1
79.89/23.09
POL(c8(x1)) = x1
79.89/23.09
POL(c9(x1, x2, x3)) = x1 + x2 + x3
79.89/23.09
POL(chk(x1)) = x1
79.89/23.09
POL(f(x1)) = [4]x1
79.89/23.09
POL(mark(x1)) = x1
79.89/23.09
POL(mat(x1, x2)) = 0
79.89/23.09
POL(no(x1)) = x1
79.89/23.09
POL(y) = [4]
79.89/23.09
79.89/23.09
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
chk(no(c)) → active(c)
79.89/23.09
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
K tuples:
MAT(f(z0), f(y)) → c4
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c2, c3, c4, c9
79.89/23.09
79.89/23.09
(9) 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(no(z0)) → c7(F(z0))
We considered the (Usable) Rules:
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
chk(no(c)) → active(c)
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
active(f(z0)) → mark(f(f(z0)))
And the Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
79.89/23.09
POL(ACTIVE(x1)) = [4]x1
79.89/23.09
POL(CHK(x1)) = 0
79.89/23.09
POL(F(x1)) = [4]x1
79.89/23.09
POL(MAT(x1, x2)) = 0
79.89/23.09
POL(TP(x1)) = 0
79.89/23.09
POL(X) = 0
79.89/23.09
POL(active(x1)) = [4]x1
79.89/23.09
POL(c) = 0
79.89/23.09
POL(c1(x1)) = x1
79.89/23.09
POL(c2(x1, x2, x3)) = x1 + x2 + x3
79.89/23.09
POL(c3) = 0
79.89/23.09
POL(c4) = 0
79.89/23.09
POL(c6(x1, x2)) = x1 + x2
79.89/23.09
POL(c7(x1)) = x1
79.89/23.09
POL(c8(x1)) = x1
79.89/23.09
POL(c9(x1, x2, x3)) = x1 + x2 + x3
79.89/23.09
POL(chk(x1)) = 0
79.89/23.09
POL(f(x1)) = x1
79.89/23.09
POL(mark(x1)) = x1
79.89/23.09
POL(mat(x1, x2)) = 0
79.89/23.09
POL(no(x1)) = [1] + x1
79.89/23.09
POL(y) = 0
79.89/23.09
79.89/23.09
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
chk(no(c)) → active(c)
79.89/23.09
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(f(z0))) → c2(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.09
F(no(z0)) → c7(F(z0))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c2, c3, c4, c9
79.89/23.09
79.89/23.09
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
CHK(
no(
f(
z0))) →
c2(
F(
chk(
mat(
f(
f(
f(
f(
f(
f(
f(
f(
f(
f(
X)))))))))),
z0))),
CHK(
mat(
f(
f(
f(
f(
f(
f(
f(
f(
f(
f(
X)))))))))),
z0)),
MAT(
f(
f(
f(
f(
f(
f(
f(
f(
f(
f(
X)))))))))),
z0)) by
CHK(no(f(f(y)))) → c2(F(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.09
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), c))
79.89/23.09
79.89/23.09
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
chk(no(c)) → active(c)
79.89/23.09
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(f(f(y)))) → c2(F(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.09
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), c))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(f(f(y)))) → c2(F(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.09
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), c))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.09
F(no(z0)) → c7(F(z0))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c9, c2
79.89/23.09
79.89/23.09
(13) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
79.89/23.09
79.89/23.09
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
chk(no(c)) → active(c)
79.89/23.09
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.09
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.09
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.09
F(no(z0)) → c7(F(z0))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c9, c2
79.89/23.09
79.89/23.09
(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
79.89/23.09
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
chk(no(c)) → active(c)
79.89/23.09
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.09
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.09
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.09
F(no(z0)) → c7(F(z0))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c9, c2
79.89/23.09
79.89/23.09
(17) 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.
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
We considered the (Usable) Rules:
chk(no(c)) → active(c)
79.89/23.09
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.09
mat(f(z0), c) → no(c)
79.89/23.09
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.09
f(active(z0)) → active(f(z0))
79.89/23.09
f(no(z0)) → no(f(z0))
79.89/23.09
f(mark(z0)) → mark(f(z0))
79.89/23.09
active(f(z0)) → mark(f(f(z0)))
And the Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.09
F(no(z0)) → c7(F(z0))
79.89/23.09
F(mark(z0)) → c8(F(z0))
79.89/23.09
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.09
CHK(no(c)) → c3
79.89/23.09
MAT(f(z0), f(y)) → c4
79.89/23.09
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.09
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.09
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
The order we found is given by the following interpretation:
Polynomial interpretation :
79.89/23.09
POL(ACTIVE(x1)) = 0
79.89/23.09
POL(CHK(x1)) = [4]x1
79.89/23.09
POL(F(x1)) = 0
79.89/23.09
POL(MAT(x1, x2)) = 0
79.89/23.09
POL(TP(x1)) = 0
79.89/23.09
POL(X) = 0
79.89/23.09
POL(active(x1)) = 0
79.89/23.09
POL(c) = 0
79.89/23.09
POL(c1(x1)) = x1
79.89/23.09
POL(c2(x1, x2)) = x1 + x2
79.89/23.10
POL(c3) = 0
79.89/23.10
POL(c4) = 0
79.89/23.10
POL(c6(x1, x2)) = x1 + x2
79.89/23.10
POL(c7(x1)) = x1
79.89/23.10
POL(c8(x1)) = x1
79.89/23.10
POL(c9(x1, x2, x3)) = x1 + x2 + x3
79.89/23.10
POL(chk(x1)) = 0
79.89/23.10
POL(f(x1)) = x1
79.89/23.10
POL(mark(x1)) = 0
79.89/23.10
POL(mat(x1, x2)) = 0
79.89/23.10
POL(no(x1)) = x1
79.89/23.10
POL(y) = [2]
79.89/23.10
79.89/23.10
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.10
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
TP(mark(z0)) → c9(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c9, c2
79.89/23.10
79.89/23.10
(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
TP(
mark(
z0)) →
c9(
TP(
chk(
mat(
f(
f(
f(
f(
f(
f(
f(
f(
f(
f(
X)))))))))),
z0))),
CHK(
mat(
f(
f(
f(
f(
f(
f(
f(
f(
f(
f(
X)))))))))),
z0)),
MAT(
f(
f(
f(
f(
f(
f(
f(
f(
f(
f(
X)))))))))),
z0)) by
TP(mark(f(y))) → c9(TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), c))
79.89/23.10
79.89/23.10
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.10
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c9(TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), c))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c9(TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), c))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9
79.89/23.10
79.89/23.10
(21) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
79.89/23.10
79.89/23.10
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.10
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c9(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c9(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9
79.89/23.10
79.89/23.10
(23) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
79.89/23.10
79.89/23.10
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.10
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9, c5
79.89/23.10
79.89/23.10
(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
79.89/23.10
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.10
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9, c5
79.89/23.10
79.89/23.10
(27) 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.
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
We considered the (Usable) Rules:
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
active(f(z0)) → mark(f(f(z0)))
And the Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
The order we found is given by the following interpretation:
Polynomial interpretation :
79.89/23.10
POL(ACTIVE(x1)) = 0
79.89/23.10
POL(CHK(x1)) = 0
79.89/23.10
POL(F(x1)) = 0
79.89/23.10
POL(MAT(x1, x2)) = 0
79.89/23.10
POL(TP(x1)) = [1]
79.89/23.10
POL(X) = 0
79.89/23.10
POL(active(x1)) = 0
79.89/23.10
POL(c) = 0
79.89/23.10
POL(c1(x1)) = x1
79.89/23.10
POL(c2(x1, x2)) = x1 + x2
79.89/23.10
POL(c3) = 0
79.89/23.10
POL(c4) = 0
79.89/23.10
POL(c5(x1)) = x1
79.89/23.10
POL(c6(x1, x2)) = x1 + x2
79.89/23.10
POL(c7(x1)) = x1
79.89/23.10
POL(c8(x1)) = x1
79.89/23.10
POL(c9(x1, x2)) = x1 + x2
79.89/23.10
POL(chk(x1)) = 0
79.89/23.10
POL(f(x1)) = 0
79.89/23.10
POL(mark(x1)) = 0
79.89/23.10
POL(mat(x1, x2)) = 0
79.89/23.10
POL(no(x1)) = 0
79.89/23.10
POL(y) = 0
79.89/23.10
79.89/23.10
(28) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.10
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9, c5
79.89/23.10
79.89/23.10
(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.
CHK(no(c)) → c3
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
We considered the (Usable) Rules:
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
active(f(z0)) → mark(f(f(z0)))
And the Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
The order we found is given by the following interpretation:
Polynomial interpretation :
79.89/23.10
POL(ACTIVE(x1)) = 0
79.89/23.10
POL(CHK(x1)) = [1]
79.89/23.10
POL(F(x1)) = 0
79.89/23.10
POL(MAT(x1, x2)) = 0
79.89/23.10
POL(TP(x1)) = x1
79.89/23.10
POL(X) = 0
79.89/23.10
POL(active(x1)) = 0
79.89/23.10
POL(c) = [4]
79.89/23.10
POL(c1(x1)) = x1
79.89/23.10
POL(c2(x1, x2)) = x1 + x2
79.89/23.10
POL(c3) = 0
79.89/23.10
POL(c4) = 0
79.89/23.10
POL(c5(x1)) = x1
79.89/23.10
POL(c6(x1, x2)) = x1 + x2
79.89/23.10
POL(c7(x1)) = x1
79.89/23.10
POL(c8(x1)) = x1
79.89/23.10
POL(c9(x1, x2)) = x1 + x2
79.89/23.10
POL(chk(x1)) = [2]
79.89/23.10
POL(f(x1)) = [4] + [4]x1
79.89/23.10
POL(mark(x1)) = x1
79.89/23.10
POL(mat(x1, x2)) = [4]x1
79.89/23.10
POL(no(x1)) = x1
79.89/23.10
POL(y) = [1]
79.89/23.10
79.89/23.10
(30) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.10
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.10
chk(no(c)) → active(c)
79.89/23.10
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.10
mat(f(z0), c) → no(c)
79.89/23.10
f(active(z0)) → active(f(z0))
79.89/23.10
f(no(z0)) → no(f(z0))
79.89/23.10
f(mark(z0)) → mark(f(z0))
79.89/23.10
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(no(z0)) → c7(F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.10
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.10
CHK(no(c)) → c3
79.89/23.10
MAT(f(z0), f(y)) → c4
79.89/23.10
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.10
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.10
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.10
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.10
F(mark(z0)) → c8(F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.11
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.11
F(no(z0)) → c7(F(z0))
79.89/23.11
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.11
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
CHK(no(c)) → c3
79.89/23.11
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9, c5
79.89/23.11
79.89/23.11
(31) 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.
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
We considered the (Usable) Rules:
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.11
mat(f(z0), c) → no(c)
79.89/23.11
chk(no(c)) → active(c)
79.89/23.11
f(active(z0)) → active(f(z0))
79.89/23.11
f(no(z0)) → no(f(z0))
79.89/23.11
f(mark(z0)) → mark(f(z0))
79.89/23.11
active(f(z0)) → mark(f(f(z0)))
And the Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.11
F(no(z0)) → c7(F(z0))
79.89/23.11
F(mark(z0)) → c8(F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.11
CHK(no(c)) → c3
79.89/23.11
MAT(f(z0), f(y)) → c4
79.89/23.11
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.11
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
The order we found is given by the following interpretation:
Polynomial interpretation :
79.89/23.11
POL(ACTIVE(x1)) = 0
79.89/23.11
POL(CHK(x1)) = [2]x1
79.89/23.11
POL(F(x1)) = 0
79.89/23.11
POL(MAT(x1, x2)) = 0
79.89/23.11
POL(TP(x1)) = [2]
79.89/23.11
POL(X) = 0
79.89/23.11
POL(active(x1)) = 0
79.89/23.11
POL(c) = 0
79.89/23.11
POL(c1(x1)) = x1
79.89/23.11
POL(c2(x1, x2)) = x1 + x2
79.89/23.11
POL(c3) = 0
79.89/23.11
POL(c4) = 0
79.89/23.11
POL(c5(x1)) = x1
79.89/23.11
POL(c6(x1, x2)) = x1 + x2
79.89/23.11
POL(c7(x1)) = x1
79.89/23.11
POL(c8(x1)) = x1
79.89/23.11
POL(c9(x1, x2)) = x1 + x2
79.89/23.11
POL(chk(x1)) = [4]
79.89/23.11
POL(f(x1)) = [1]
79.89/23.11
POL(mark(x1)) = 0
79.89/23.11
POL(mat(x1, x2)) = x2
79.89/23.11
POL(no(x1)) = x1
79.89/23.11
POL(y) = 0
79.89/23.11
79.89/23.11
(32) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.11
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.11
chk(no(c)) → active(c)
79.89/23.11
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.11
mat(f(z0), c) → no(c)
79.89/23.11
f(active(z0)) → active(f(z0))
79.89/23.11
f(no(z0)) → no(f(z0))
79.89/23.11
f(mark(z0)) → mark(f(z0))
79.89/23.11
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.11
F(no(z0)) → c7(F(z0))
79.89/23.11
F(mark(z0)) → c8(F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.11
CHK(no(c)) → c3
79.89/23.11
MAT(f(z0), f(y)) → c4
79.89/23.11
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.11
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
S tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.11
F(mark(z0)) → c8(F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.11
F(no(z0)) → c7(F(z0))
79.89/23.11
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.11
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
CHK(no(c)) → c3
79.89/23.11
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9, c5
79.89/23.11
79.89/23.11
(33) 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(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
We considered the (Usable) Rules:
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.11
mat(f(z0), c) → no(c)
79.89/23.11
chk(no(c)) → active(c)
79.89/23.11
f(active(z0)) → active(f(z0))
79.89/23.11
f(no(z0)) → no(f(z0))
79.89/23.11
f(mark(z0)) → mark(f(z0))
79.89/23.11
active(f(z0)) → mark(f(f(z0)))
And the Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.11
F(no(z0)) → c7(F(z0))
79.89/23.11
F(mark(z0)) → c8(F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.11
CHK(no(c)) → c3
79.89/23.11
MAT(f(z0), f(y)) → c4
79.89/23.11
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.11
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
The order we found is given by the following interpretation:
Polynomial interpretation :
79.89/23.11
POL(ACTIVE(x1)) = x1
79.89/23.11
POL(CHK(x1)) = [2]x1
79.89/23.11
POL(F(x1)) = [2]x1
79.89/23.11
POL(MAT(x1, x2)) = [1] + x2
79.89/23.11
POL(TP(x1)) = [4]
79.89/23.11
POL(X) = 0
79.89/23.11
POL(active(x1)) = [1] + [2]x1
79.89/23.11
POL(c) = 0
79.89/23.11
POL(c1(x1)) = x1
79.89/23.11
POL(c2(x1, x2)) = x1 + x2
79.89/23.11
POL(c3) = 0
79.89/23.11
POL(c4) = 0
79.89/23.11
POL(c5(x1)) = x1
79.89/23.11
POL(c6(x1, x2)) = x1 + x2
79.89/23.11
POL(c7(x1)) = x1
79.89/23.11
POL(c8(x1)) = x1
79.89/23.11
POL(c9(x1, x2)) = x1 + x2
79.89/23.11
POL(chk(x1)) = [1]
79.89/23.11
POL(f(x1)) = [1] + [2]x1
79.89/23.11
POL(mark(x1)) = x1
79.89/23.11
POL(mat(x1, x2)) = [2]x2
79.89/23.11
POL(no(x1)) = x1
79.89/23.11
POL(y) = 0
79.89/23.11
79.89/23.11
(34) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.11
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
79.89/23.11
chk(no(c)) → active(c)
79.89/23.11
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.11
mat(f(z0), c) → no(c)
79.89/23.11
f(active(z0)) → active(f(z0))
79.89/23.11
f(no(z0)) → no(f(z0))
79.89/23.11
f(mark(z0)) → mark(f(z0))
79.89/23.11
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.11
F(no(z0)) → c7(F(z0))
79.89/23.11
F(mark(z0)) → c8(F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.11
CHK(no(c)) → c3
79.89/23.11
MAT(f(z0), f(y)) → c4
79.89/23.11
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.11
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
S tuples:
F(mark(z0)) → c8(F(z0))
K tuples:
MAT(f(z0), f(y)) → c4
79.89/23.11
F(no(z0)) → c7(F(z0))
79.89/23.11
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.11
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
CHK(no(c)) → c3
79.89/23.11
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9, c5
79.89/23.11
79.89/23.11
(35) 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(mark(z0)) → c8(F(z0))
We considered the (Usable) Rules:
mat(f(z0), f(y)) → f(mat(z0, y))
79.89/23.11
mat(f(z0), c) → no(c)
79.89/23.11
chk(no(c)) → active(c)
79.89/23.11
f(active(z0)) → active(f(z0))
79.89/23.11
f(no(z0)) → no(f(z0))
79.89/23.11
f(mark(z0)) → mark(f(z0))
79.89/23.11
active(f(z0)) → mark(f(f(z0)))
And the Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
79.89/23.11
F(no(z0)) → c7(F(z0))
79.89/23.11
F(mark(z0)) → c8(F(z0))
79.89/23.11
ACTIVE(f(z0)) → c1(F(z0))
79.89/23.11
CHK(no(c)) → c3
79.89/23.11
MAT(f(z0), f(y)) → c4
79.89/23.11
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
79.89/23.11
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
79.89/23.11
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
79.89/23.11
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
The order we found is given by the following interpretation:
Polynomial interpretation :
79.89/23.11
POL(ACTIVE(x1)) = [1] + x1
79.89/23.11
POL(CHK(x1)) = [3]x1
79.89/23.11
POL(F(x1)) = x1
79.89/23.11
POL(MAT(x1, x2)) = x2
79.89/23.11
POL(TP(x1)) = [3]
79.89/23.11
POL(X) = 0
79.89/23.11
POL(active(x1)) = [2] + [5]x1
79.89/23.11
POL(c) = 0
79.89/23.11
POL(c1(x1)) = x1
79.89/23.11
POL(c2(x1, x2)) = x1 + x2
79.89/23.11
POL(c3) = 0
79.89/23.11
POL(c4) = 0
79.89/23.11
POL(c5(x1)) = x1
79.89/23.11
POL(c6(x1, x2)) = x1 + x2
79.89/23.11
POL(c7(x1)) = x1
79.89/23.11
POL(c8(x1)) = x1
79.89/23.11
POL(c9(x1, x2)) = x1 + x2
79.89/23.11
POL(chk(x1)) = [3]
79.89/23.11
POL(f(x1)) = [1] + [4]x1
79.89/23.11
POL(mark(x1)) = [2] + x1
79.89/23.11
POL(mat(x1, x2)) = x2
79.89/23.11
POL(no(x1)) = x1
79.89/23.11
POL(y) = 0
79.89/23.11
79.89/23.11
(36) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(f(z0)) → mark(f(f(z0)))
79.89/23.11
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
80.29/23.12
chk(no(c)) → active(c)
80.29/23.12
mat(f(z0), f(y)) → f(mat(z0, y))
80.29/23.12
mat(f(z0), c) → no(c)
80.29/23.12
f(active(z0)) → active(f(z0))
80.29/23.12
f(no(z0)) → no(f(z0))
80.29/23.12
f(mark(z0)) → mark(f(z0))
80.29/23.12
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
Tuples:
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
80.29/23.12
F(no(z0)) → c7(F(z0))
80.29/23.12
F(mark(z0)) → c8(F(z0))
80.29/23.12
ACTIVE(f(z0)) → c1(F(z0))
80.29/23.12
CHK(no(c)) → c3
80.29/23.12
MAT(f(z0), f(y)) → c4
80.29/23.12
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
80.29/23.12
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
80.29/23.12
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
80.29/23.12
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
80.29/23.12
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
S tuples:none
K tuples:
MAT(f(z0), f(y)) → c4
80.29/23.12
F(no(z0)) → c7(F(z0))
80.29/23.12
CHK(no(f(f(y)))) → c2(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
80.29/23.12
TP(mark(f(y))) → c5(CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y))))
80.29/23.12
TP(mark(f(y))) → c5(MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), f(y)))
80.29/23.12
CHK(no(c)) → c3
80.29/23.12
TP(mark(c)) → c9(TP(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
80.29/23.12
CHK(no(f(c))) → c2(F(chk(no(c))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), c)))
80.29/23.12
F(active(z0)) → c6(ACTIVE(f(z0)), F(z0))
80.29/23.12
ACTIVE(f(z0)) → c1(F(z0))
80.29/23.12
F(mark(z0)) → c8(F(z0))
Defined Rule Symbols:
active, chk, mat, f, tp
Defined Pair Symbols:
F, ACTIVE, CHK, MAT, TP
Compound Symbols:
c6, c7, c8, c1, c3, c4, c2, c9, c5
80.29/23.12
80.29/23.12
(37) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
80.29/23.12
80.29/23.12
(38) BOUNDS(O(1), O(1))
80.29/23.12