YES(O(1), O(n^2)) 2.81/1.18 YES(O(1), O(n^2)) 2.81/1.20 2.81/1.20 2.81/1.20
2.81/1.20 2.81/1.200 CpxTRS2.81/1.20
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))2.81/1.20
↳2 CdtProblem2.81/1.20
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))2.81/1.20
↳4 CdtProblem2.81/1.20
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))2.81/1.20
↳6 CdtProblem2.81/1.20
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))2.81/1.20
↳8 CdtProblem2.81/1.20
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))2.81/1.20
↳10 CdtProblem2.81/1.20
↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))2.81/1.20
↳12 CdtProblem2.81/1.20
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))2.81/1.20
↳14 CdtProblem2.81/1.20
↳15 SIsEmptyProof (BOTH BOUNDS(ID, ID))2.81/1.20
↳16 BOUNDS(O(1), O(1))2.81/1.20
f(X) → if(X, c, n__f(n__true)) 2.81/1.20
if(true, X, Y) → X 2.81/1.20
if(false, X, Y) → activate(Y) 2.81/1.20
f(X) → n__f(X) 2.81/1.20
true → n__true 2.81/1.20
activate(n__f(X)) → f(activate(X)) 2.81/1.20
activate(n__true) → true 2.81/1.20
activate(X) → X
Tuples:
f(z0) → if(z0, c, n__f(n__true)) 2.81/1.20
f(z0) → n__f(z0) 2.81/1.20
if(true, z0, z1) → z0 2.81/1.20
if(false, z0, z1) → activate(z1) 2.81/1.20
true → n__true 2.81/1.20
activate(n__f(z0)) → f(activate(z0)) 2.81/1.20
activate(n__true) → true 2.81/1.20
activate(z0) → z0
S tuples:
F(z0) → c1(IF(z0, c, n__f(n__true))) 2.81/1.20
IF(false, z0, z1) → c4(ACTIVATE(z1)) 2.81/1.20
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 2.81/1.20
ACTIVATE(n__true) → c7(TRUE)
K tuples:none
F(z0) → c1(IF(z0, c, n__f(n__true))) 2.81/1.20
IF(false, z0, z1) → c4(ACTIVATE(z1)) 2.81/1.20
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7(TRUE)
f, if, true, activate
F, IF, ACTIVATE
c1, c4, c6, c7
Tuples:
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
S tuples:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
K tuples:none
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
f, if, true, activate
F, IF, ACTIVATE
c1, c4, c6, c7
ACTIVATE(n__true) → c7
Tuples:
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
S tuples:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
K tuples:none
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
f, if, true, activate
F, IF, ACTIVATE
c1, c4, c6, c7
We considered the (Usable) Rules:
ACTIVATE(n__true) → c7
And the Tuples:
if(false, z0, z1) → activate(z1) 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0 3.15/1.21
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
true → n__true
The order we found is given by the following interpretation:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
POL(ACTIVATE(x1)) = [1] + x12 3.15/1.21
POL(F(x1)) = [1] + [2]x1 3.15/1.21
POL(IF(x1, x2, x3)) = x1 + [3]x2 + x32 + [3]x1·x2 + [3]x22 3.15/1.21
POL(activate(x1)) = x1 3.15/1.21
POL(c) = 0 3.15/1.21
POL(c1(x1)) = x1 3.15/1.21
POL(c4(x1)) = x1 3.15/1.21
POL(c6(x1, x2)) = x1 + x2 3.15/1.21
POL(c7) = 0 3.15/1.21
POL(f(x1)) = [1] + x1 3.15/1.21
POL(false) = [1] 3.15/1.21
POL(if(x1, x2, x3)) = [3]x2 + x3 + [3]x1·x2 3.15/1.21
POL(n__f(x1)) = [1] + x1 3.15/1.21
POL(n__true) = 0 3.15/1.21
POL(true) = 0
Tuples:
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
S tuples:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
K tuples:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
Defined Rule Symbols:
ACTIVATE(n__true) → c7
f, if, true, activate
F, IF, ACTIVATE
c1, c4, c6, c7
We considered the (Usable) Rules:
F(z0) → c1(IF(z0, c, n__f(n__true)))
And the Tuples:
if(false, z0, z1) → activate(z1) 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0 3.15/1.21
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
true → n__true
The order we found is given by the following interpretation:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
POL(ACTIVATE(x1)) = x1 + x12 3.15/1.21
POL(F(x1)) = [2] + [2]x1 3.15/1.21
POL(IF(x1, x2, x3)) = [3]x2 + x32 + [2]x1·x3 + [3]x1·x2 + [3]x22 3.15/1.21
POL(activate(x1)) = x1 3.15/1.21
POL(c) = 0 3.15/1.21
POL(c1(x1)) = x1 3.15/1.21
POL(c4(x1)) = x1 3.15/1.21
POL(c6(x1, x2)) = x1 + x2 3.15/1.21
POL(c7) = 0 3.15/1.21
POL(f(x1)) = [1] + x1 3.15/1.21
POL(false) = [2] 3.15/1.21
POL(if(x1, x2, x3)) = [3]x2 + x1·x3 + [3]x1·x2 3.15/1.21
POL(n__f(x1)) = [1] + x1 3.15/1.21
POL(n__true) = 0 3.15/1.21
POL(true) = 0
Tuples:
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
S tuples:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
K tuples:
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
Defined Rule Symbols:
ACTIVATE(n__true) → c7 3.15/1.21
F(z0) → c1(IF(z0, c, n__f(n__true)))
f, if, true, activate
F, IF, ACTIVATE
c1, c4, c6, c7
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__true) → c7
Tuples:
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
S tuples:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
K tuples:
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
Defined Rule Symbols:
ACTIVATE(n__true) → c7 3.15/1.21
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1))
f, if, true, activate
F, IF, ACTIVATE
c1, c4, c6, c7
We considered the (Usable) Rules:
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
And the Tuples:
if(false, z0, z1) → activate(z1) 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0 3.15/1.21
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
true → n__true
The order we found is given by the following interpretation:
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
POL(ACTIVATE(x1)) = [2]x1 + x12 3.15/1.21
POL(F(x1)) = [1] + x1 3.15/1.21
POL(IF(x1, x2, x3)) = [3]x2 + x32 + x1·x3 + [3]x1·x2 + [3]x22 3.15/1.21
POL(activate(x1)) = [2]x1 3.15/1.21
POL(c) = 0 3.15/1.21
POL(c1(x1)) = x1 3.15/1.21
POL(c4(x1)) = x1 3.15/1.21
POL(c6(x1, x2)) = x1 + x2 3.15/1.21
POL(c7) = 0 3.15/1.21
POL(f(x1)) = [1] + x1 3.15/1.21
POL(false) = [2] 3.15/1.21
POL(if(x1, x2, x3)) = [3]x2 + x1·x3 + [3]x1·x2 3.15/1.21
POL(n__f(x1)) = [1] + x1 3.15/1.21
POL(n__true) = 0 3.15/1.21
POL(true) = 0
Tuples:
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
S tuples:none
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
Defined Rule Symbols:
ACTIVATE(n__true) → c7 3.15/1.21
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
f, if, true, activate
F, IF, ACTIVATE
c1, c4, c6, c7