YES(O(1), O(n^1)) 0.00/0.86 YES(O(1), O(n^1)) 0.00/0.89 0.00/0.89 0.00/0.89
0.00/0.89 0.00/0.890 CpxTRS0.00/0.89
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.89
↳2 CdtProblem0.00/0.89
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.89
↳4 CdtProblem0.00/0.89
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.89
↳6 CdtProblem0.00/0.89
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.89
↳8 CdtProblem0.00/0.89
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.89
↳10 CdtProblem0.00/0.89
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.89
↳12 BOUNDS(O(1), O(1))0.00/0.89
perfectp(0) → false 0.00/0.89
perfectp(s(x)) → f(x, s(0), s(x), s(x)) 0.00/0.89
f(0, y, 0, u) → true 0.00/0.89
f(0, y, s(z), u) → false 0.00/0.89
f(s(x), 0, z, u) → f(x, u, minus(z, s(x)), u) 0.00/0.89
f(s(x), s(y), z, u) → if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))
Tuples:
perfectp(0) → false 0.00/0.89
perfectp(s(z0)) → f(z0, s(0), s(z0), s(z0)) 0.00/0.89
f(0, z0, 0, z1) → true 0.00/0.89
f(0, z0, s(z1), z2) → false 0.00/0.89
f(s(z0), 0, z1, z2) → f(z0, z2, minus(z1, s(z0)), z2) 0.00/0.89
f(s(z0), s(z1), z2, z3) → if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
S tuples:
PERFECTP(s(z0)) → c1(F(z0, s(0), s(z0), s(z0))) 0.00/0.89
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(s(z0), minus(z1, z0), z2, z3), F(z0, z3, z2, z3))
K tuples:none
PERFECTP(s(z0)) → c1(F(z0, s(0), s(z0), s(z0))) 0.00/0.89
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(s(z0), minus(z1, z0), z2, z3), F(z0, z3, z2, z3))
perfectp, f
PERFECTP, F
c1, c4, c5
Tuples:
perfectp(0) → false 0.00/0.89
perfectp(s(z0)) → f(z0, s(0), s(z0), s(z0)) 0.00/0.89
f(0, z0, 0, z1) → true 0.00/0.89
f(0, z0, s(z1), z2) → false 0.00/0.89
f(s(z0), 0, z1, z2) → f(z0, z2, minus(z1, s(z0)), z2) 0.00/0.89
f(s(z0), s(z1), z2, z3) → if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
S tuples:
PERFECTP(s(z0)) → c1(F(z0, s(0), s(z0), s(z0))) 0.00/0.89
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
K tuples:none
PERFECTP(s(z0)) → c1(F(z0, s(0), s(z0), s(z0))) 0.00/0.89
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
perfectp, f
PERFECTP, F
c1, c4, c5
PERFECTP(s(z0)) → c1(F(z0, s(0), s(z0), s(z0)))
Tuples:
perfectp(0) → false 0.00/0.89
perfectp(s(z0)) → f(z0, s(0), s(z0), s(z0)) 0.00/0.89
f(0, z0, 0, z1) → true 0.00/0.89
f(0, z0, s(z1), z2) → false 0.00/0.89
f(s(z0), 0, z1, z2) → f(z0, z2, minus(z1, s(z0)), z2) 0.00/0.89
f(s(z0), s(z1), z2, z3) → if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
S tuples:
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
K tuples:none
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
perfectp, f
F
c4, c5
We considered the (Usable) Rules:none
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
The order we found is given by the following interpretation:
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
POL(0) = 0 0.00/0.89
POL(F(x1, x2, x3, x4)) = [4]x1 + [4]x3 0.00/0.89
POL(c4(x1)) = x1 0.00/0.89
POL(c5(x1)) = x1 0.00/0.89
POL(minus(x1, x2)) = [4] + x1 0.00/0.89
POL(s(x1)) = [4] + x1
Tuples:
perfectp(0) → false 0.00/0.89
perfectp(s(z0)) → f(z0, s(0), s(z0), s(z0)) 0.00/0.89
f(0, z0, 0, z1) → true 0.00/0.89
f(0, z0, s(z1), z2) → false 0.00/0.89
f(s(z0), 0, z1, z2) → f(z0, z2, minus(z1, s(z0)), z2) 0.00/0.89
f(s(z0), s(z1), z2, z3) → if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
S tuples:
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
K tuples:
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2))
Defined Rule Symbols:
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
perfectp, f
F
c4, c5
We considered the (Usable) Rules:none
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2))
The order we found is given by the following interpretation:
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
POL(0) = 0 0.00/0.89
POL(F(x1, x2, x3, x4)) = [4]x1 0.00/0.89
POL(c4(x1)) = x1 0.00/0.89
POL(c5(x1)) = x1 0.00/0.89
POL(minus(x1, x2)) = [1] + x1 + x2 0.00/0.89
POL(s(x1)) = [4] + x1
Tuples:
perfectp(0) → false 0.00/0.89
perfectp(s(z0)) → f(z0, s(0), s(z0), s(z0)) 0.00/0.89
f(0, z0, 0, z1) → true 0.00/0.89
f(0, z0, s(z1), z2) → false 0.00/0.89
f(s(z0), 0, z1, z2) → f(z0, z2, minus(z1, s(z0)), z2) 0.00/0.89
f(s(z0), s(z1), z2, z3) → if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
S tuples:none
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2)) 0.00/0.89
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3))
Defined Rule Symbols:
F(s(z0), s(z1), z2, z3) → c5(F(z0, z3, z2, z3)) 0.00/0.89
F(s(z0), 0, z1, z2) → c4(F(z0, z2, minus(z1, s(z0)), z2))
perfectp, f
F
c4, c5