p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
ACTIVATE(n__s(X)) → S(activate(X))
IF(true, X, Y) → ACTIVATE(X)
DIFF(X, Y) → LEQ(X, Y)
ACTIVATE(n__diff(X1, X2)) → DIFF(activate(X1), activate(X2))
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__diff(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__p(X)) → P(activate(X))
ACTIVATE(n__p(X)) → ACTIVATE(X)
ACTIVATE(n__0) → 01
LEQ(s(X), s(Y)) → LEQ(X, Y)
ACTIVATE(n__diff(X1, X2)) → ACTIVATE(X2)
DIFF(X, Y) → IF(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ACTIVATE(n__s(X)) → S(activate(X))
IF(true, X, Y) → ACTIVATE(X)
DIFF(X, Y) → LEQ(X, Y)
ACTIVATE(n__diff(X1, X2)) → DIFF(activate(X1), activate(X2))
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__diff(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__p(X)) → P(activate(X))
ACTIVATE(n__p(X)) → ACTIVATE(X)
ACTIVATE(n__0) → 01
LEQ(s(X), s(Y)) → LEQ(X, Y)
ACTIVATE(n__diff(X1, X2)) → ACTIVATE(X2)
DIFF(X, Y) → IF(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
LEQ(s(X), s(Y)) → LEQ(X, Y)
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LEQ(s(X), s(Y)) → LEQ(X, Y)
The value of delta used in the strict ordering is 3.
POL(LEQ(x1, x2)) = (3)x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
ACTIVATE(n__p(X)) → ACTIVATE(X)
ACTIVATE(n__diff(X1, X2)) → ACTIVATE(X2)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__diff(X1, X2)) → DIFF(activate(X1), activate(X2))
DIFF(X, Y) → IF(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__diff(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__diff(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__diff(X1, X2)) → ACTIVATE(X1)
Used ordering: Polynomial interpretation [25,35]:
ACTIVATE(n__p(X)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__diff(X1, X2)) → DIFF(activate(X1), activate(X2))
DIFF(X, Y) → IF(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
The value of delta used in the strict ordering is 4.
POL(DIFF(x1, x2)) = 4 + (4)x_1 + (4)x_2
POL(n__p(x1)) = x_1
POL(true) = 0
POL(activate(x1)) = x_1
POL(p(x1)) = x_1
POL(n__s(x1)) = x_1
POL(IF(x1, x2, x3)) = (4)x_2 + (4)x_3
POL(0) = 0
POL(if(x1, x2, x3)) = x_2 + x_3
POL(diff(x1, x2)) = 1 + x_1 + x_2
POL(n__0) = 0
POL(false) = 0
POL(s(x1)) = x_1
POL(ACTIVATE(x1)) = (4)x_1
POL(leq(x1, x2)) = x_2
POL(n__diff(x1, x2)) = 1 + x_1 + x_2
p(0) → 0
p(s(X)) → X
s(X) → n__s(X)
0 → n__0
p(X) → n__p(X)
diff(X1, X2) → n__diff(X1, X2)
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__p(X)) → p(activate(X))
if(false, X, Y) → activate(Y)
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
if(true, X, Y) → activate(X)
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
ACTIVATE(n__p(X)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__diff(X1, X2)) → DIFF(activate(X1), activate(X2))
DIFF(X, Y) → IF(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__p(X)) → ACTIVATE(X)
Used ordering: Polynomial interpretation [25,35]:
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__diff(X1, X2)) → DIFF(activate(X1), activate(X2))
DIFF(X, Y) → IF(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
The value of delta used in the strict ordering is 1.
POL(DIFF(x1, x2)) = 0
POL(n__p(x1)) = 1 + (4)x_1
POL(true) = 0
POL(activate(x1)) = 3
POL(p(x1)) = 3 + (3)x_1
POL(n__s(x1)) = (2)x_1
POL(IF(x1, x2, x3)) = x_2 + x_3
POL(0) = 4
POL(if(x1, x2, x3)) = 1 + (4)x_1 + (2)x_2 + (4)x_3
POL(diff(x1, x2)) = 1 + (3)x_1 + (4)x_2
POL(n__0) = 0
POL(false) = 0
POL(s(x1)) = 3
POL(ACTIVATE(x1)) = x_1
POL(leq(x1, x2)) = (2)x_2
POL(n__diff(x1, x2)) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
IF(true, X, Y) → ACTIVATE(X)
ACTIVATE(n__diff(X1, X2)) → DIFF(activate(X1), activate(X2))
DIFF(X, Y) → IF(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__s(X)) → ACTIVATE(X)
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X