YES(O(1), O(n^1)) 0.00/0.75 YES(O(1), O(n^1)) 0.00/0.76 0.00/0.76 0.00/0.76
0.00/0.76 0.00/0.760 CpxTRS0.00/0.76
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.76
↳2 CdtProblem0.00/0.76
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.76
↳4 CdtProblem0.00/0.76
↳5 CdtKnowledgeProof (⇔)0.00/0.76
↳6 BOUNDS(O(1), O(1))0.00/0.76
f(X) → if(X, c, n__f(true)) 0.00/0.76
if(true, X, Y) → X 0.00/0.76
if(false, X, Y) → activate(Y) 0.00/0.76
f(X) → n__f(X) 0.00/0.76
activate(n__f(X)) → f(X) 0.00/0.76
activate(X) → X
Tuples:
f(z0) → if(z0, c, n__f(true)) 0.00/0.76
f(z0) → n__f(z0) 0.00/0.76
if(true, z0, z1) → z0 0.00/0.76
if(false, z0, z1) → activate(z1) 0.00/0.76
activate(n__f(z0)) → f(z0) 0.00/0.76
activate(z0) → z0
S tuples:
F(z0) → c1(IF(z0, c, n__f(true))) 0.00/0.76
IF(false, z0, z1) → c4(ACTIVATE(z1)) 0.00/0.76
ACTIVATE(n__f(z0)) → c5(F(z0))
K tuples:none
F(z0) → c1(IF(z0, c, n__f(true))) 0.00/0.76
IF(false, z0, z1) → c4(ACTIVATE(z1)) 0.00/0.76
ACTIVATE(n__f(z0)) → c5(F(z0))
f, if, activate
F, IF, ACTIVATE
c1, c4, c5
We considered the (Usable) Rules:none
IF(false, z0, z1) → c4(ACTIVATE(z1))
The order we found is given by the following interpretation:
F(z0) → c1(IF(z0, c, n__f(true))) 0.00/0.76
IF(false, z0, z1) → c4(ACTIVATE(z1)) 0.00/0.76
ACTIVATE(n__f(z0)) → c5(F(z0))
POL(ACTIVATE(x1)) = x1 0.00/0.76
POL(F(x1)) = x1 0.00/0.76
POL(IF(x1, x2, x3)) = x1 + x2 + x3 0.00/0.76
POL(c) = 0 0.00/0.76
POL(c1(x1)) = x1 0.00/0.76
POL(c4(x1)) = x1 0.00/0.76
POL(c5(x1)) = x1 0.00/0.76
POL(false) = [2] 0.00/0.76
POL(n__f(x1)) = x1 0.00/0.76
POL(true) = 0
Tuples:
f(z0) → if(z0, c, n__f(true)) 0.00/0.76
f(z0) → n__f(z0) 0.00/0.76
if(true, z0, z1) → z0 0.00/0.76
if(false, z0, z1) → activate(z1) 0.00/0.76
activate(n__f(z0)) → f(z0) 0.00/0.76
activate(z0) → z0
S tuples:
F(z0) → c1(IF(z0, c, n__f(true))) 0.00/0.76
IF(false, z0, z1) → c4(ACTIVATE(z1)) 0.00/0.76
ACTIVATE(n__f(z0)) → c5(F(z0))
K tuples:
F(z0) → c1(IF(z0, c, n__f(true))) 0.00/0.76
ACTIVATE(n__f(z0)) → c5(F(z0))
Defined Rule Symbols:
IF(false, z0, z1) → c4(ACTIVATE(z1))
f, if, activate
F, IF, ACTIVATE
c1, c4, c5
Now S is empty
ACTIVATE(n__f(z0)) → c5(F(z0)) 0.00/0.76
F(z0) → c1(IF(z0, c, n__f(true))) 0.00/0.76
IF(false, z0, z1) → c4(ACTIVATE(z1))