active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(f(b, X, c)) → F(X, c, X)
ACTIVE(f(X1, X2, X3)) → F(X1, active(X2), X3)
F(ok(X1), ok(X2), ok(X3)) → F(X1, X2, X3)
TOP(mark(X)) → PROPER(X)
F(X1, mark(X2), X3) → F(X1, X2, X3)
TOP(ok(X)) → ACTIVE(X)
PROPER(f(X1, X2, X3)) → PROPER(X1)
PROPER(f(X1, X2, X3)) → PROPER(X2)
PROPER(f(X1, X2, X3)) → PROPER(X3)
TOP(mark(X)) → TOP(proper(X))
ACTIVE(f(X1, X2, X3)) → ACTIVE(X2)
PROPER(f(X1, X2, X3)) → F(proper(X1), proper(X2), proper(X3))
TOP(ok(X)) → TOP(active(X))
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ACTIVE(f(b, X, c)) → F(X, c, X)
ACTIVE(f(X1, X2, X3)) → F(X1, active(X2), X3)
F(ok(X1), ok(X2), ok(X3)) → F(X1, X2, X3)
TOP(mark(X)) → PROPER(X)
F(X1, mark(X2), X3) → F(X1, X2, X3)
TOP(ok(X)) → ACTIVE(X)
PROPER(f(X1, X2, X3)) → PROPER(X1)
PROPER(f(X1, X2, X3)) → PROPER(X2)
PROPER(f(X1, X2, X3)) → PROPER(X3)
TOP(mark(X)) → TOP(proper(X))
ACTIVE(f(X1, X2, X3)) → ACTIVE(X2)
PROPER(f(X1, X2, X3)) → F(proper(X1), proper(X2), proper(X3))
TOP(ok(X)) → TOP(active(X))
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
F(ok(X1), ok(X2), ok(X3)) → F(X1, X2, X3)
F(X1, mark(X2), X3) → F(X1, X2, X3)
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(ok(X1), ok(X2), ok(X3)) → F(X1, X2, X3)
F(X1, mark(X2), X3) → F(X1, X2, X3)
The value of delta used in the strict ordering is 3.
POL(ok(x1)) = 1 + (4)x_1
POL(mark(x1)) = 1 + (2)x_1
POL(F(x1, x2, x3)) = (2)x_1 + (3)x_2 + x_3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
PROPER(f(X1, X2, X3)) → PROPER(X1)
PROPER(f(X1, X2, X3)) → PROPER(X2)
PROPER(f(X1, X2, X3)) → PROPER(X3)
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(f(X1, X2, X3)) → PROPER(X1)
PROPER(f(X1, X2, X3)) → PROPER(X2)
PROPER(f(X1, X2, X3)) → PROPER(X3)
The value of delta used in the strict ordering is 4.
POL(PROPER(x1)) = (4)x_1
POL(f(x1, x2, x3)) = 1 + (4)x_1 + (4)x_2 + (4)x_3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ACTIVE(f(X1, X2, X3)) → ACTIVE(X2)
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(f(X1, X2, X3)) → ACTIVE(X2)
The value of delta used in the strict ordering is 4.
POL(f(x1, x2, x3)) = 1 + (4)x_2
POL(ACTIVE(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))
active(f(b, X, c)) → mark(f(X, c, X))
active(c) → mark(b)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))