YES(O(1), O(n^1)) 0.00/0.70 YES(O(1), O(n^1)) 0.00/0.71 0.00/0.71 0.00/0.71
0.00/0.71 0.00/0.710 CpxRelTRS0.00/0.71
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))0.00/0.71
↳2 CdtProblem0.00/0.71
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.71
↳4 CdtProblem0.00/0.71
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.71
↳6 CdtProblem0.00/0.71
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.71
↳8 BOUNDS(O(1), O(1))0.00/0.71
div2(S(S(x))) → +(S(0), div2(x)) 0.00/0.71
div2(S(0)) → 0 0.00/0.71
div2(0) → 0
+(x, S(0)) → S(x) 0.00/0.71
+(S(0), y) → S(y)
Tuples:
+(z0, S(0)) → S(z0) 0.00/0.71
+(S(0), z0) → S(z0) 0.00/0.71
div2(S(S(z0))) → +(S(0), div2(z0)) 0.00/0.71
div2(S(0)) → 0 0.00/0.71
div2(0) → 0
S tuples:
DIV2(S(S(z0))) → c2(+'(S(0), div2(z0)), DIV2(z0))
K tuples:none
DIV2(S(S(z0))) → c2(+'(S(0), div2(z0)), DIV2(z0))
div2, +
DIV2
c2
Tuples:
+(z0, S(0)) → S(z0) 0.00/0.71
+(S(0), z0) → S(z0) 0.00/0.71
div2(S(S(z0))) → +(S(0), div2(z0)) 0.00/0.71
div2(S(0)) → 0 0.00/0.71
div2(0) → 0
S tuples:
DIV2(S(S(z0))) → c2(DIV2(z0))
K tuples:none
DIV2(S(S(z0))) → c2(DIV2(z0))
div2, +
DIV2
c2
We considered the (Usable) Rules:none
DIV2(S(S(z0))) → c2(DIV2(z0))
The order we found is given by the following interpretation:
DIV2(S(S(z0))) → c2(DIV2(z0))
POL(DIV2(x1)) = [4]x1 0.00/0.71
POL(S(x1)) = [4] + x1 0.00/0.71
POL(c2(x1)) = x1
Tuples:
+(z0, S(0)) → S(z0) 0.00/0.71
+(S(0), z0) → S(z0) 0.00/0.71
div2(S(S(z0))) → +(S(0), div2(z0)) 0.00/0.71
div2(S(0)) → 0 0.00/0.71
div2(0) → 0
S tuples:none
DIV2(S(S(z0))) → c2(DIV2(z0))
Defined Rule Symbols:
DIV2(S(S(z0))) → c2(DIV2(z0))
div2, +
DIV2
c2