MAYBE 254.94/218.75 MAYBE 254.94/218.77 254.94/218.77 254.94/218.77
254.94/218.77 254.94/218.770 CpxTRS254.94/218.77
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))254.94/218.77
↳2 CdtProblem254.94/218.77
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))254.94/218.77
↳4 CdtProblem254.94/218.77
↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID))254.94/218.77
↳6 CdtProblem254.94/218.77
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))254.94/218.77
↳8 CdtProblem254.94/218.77
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))254.94/218.77
↳10 CdtProblem254.94/218.77
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))254.94/218.77
↳12 CdtProblem254.94/218.77
↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))254.94/218.77
↳14 CdtProblem254.94/218.77
↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))254.94/218.77
↳16 CdtProblem254.94/218.77
p(s(x)) → x 254.94/218.77
fact(0) → s(0) 254.94/218.77
fact(s(x)) → *(s(x), fact(p(s(x)))) 254.94/218.77
*(0, y) → 0 254.94/218.77
*(s(x), y) → +(*(x, y), y) 254.94/218.77
+(x, 0) → x 254.94/218.77
+(x, s(y)) → s(+(x, y))
Tuples:
p(s(z0)) → z0 254.94/218.77
fact(0) → s(0) 254.94/218.77
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.77
*(0, z0) → 0 254.94/218.77
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.77
+(z0, 0) → z0 254.94/218.77
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
FACT(s(z0)) → c2(*'(s(z0), fact(p(s(z0)))), FACT(p(s(z0))), P(s(z0))) 254.94/218.77
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.77
+'(z0, s(z1)) → c6(+'(z0, z1))
K tuples:none
FACT(s(z0)) → c2(*'(s(z0), fact(p(s(z0)))), FACT(p(s(z0))), P(s(z0))) 254.94/218.77
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.77
+'(z0, s(z1)) → c6(+'(z0, z1))
p, fact, *, +
FACT, *', +'
c2, c4, c6
Tuples:
p(s(z0)) → z0 254.94/218.77
fact(0) → s(0) 254.94/218.77
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.77
*(0, z0) → 0 254.94/218.77
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.77
+(z0, 0) → z0 254.94/218.77
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.77
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.77
FACT(s(z0)) → c2(*'(s(z0), fact(p(s(z0)))), FACT(p(s(z0))))
K tuples:none
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.77
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.77
FACT(s(z0)) → c2(*'(s(z0), fact(p(s(z0)))), FACT(p(s(z0))))
p, fact, *, +
*', +', FACT
c4, c6, c2
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(p(s(z0))))
Tuples:
p(s(z0)) → z0 254.94/218.77
fact(0) → s(0) 254.94/218.77
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.77
*(0, z0) → 0 254.94/218.77
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.77
+(z0, 0) → z0 254.94/218.77
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.77
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.77
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(p(s(z0))))
K tuples:none
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.77
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.77
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(p(s(z0))))
p, fact, *, +
*', +', FACT
c4, c6, c2
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
Tuples:
p(s(z0)) → z0 254.94/218.77
fact(0) → s(0) 254.94/218.77
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.77
*(0, z0) → 0 254.94/218.77
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.77
+(z0, 0) → z0 254.94/218.78
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.78
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
K tuples:none
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.78
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
p, fact, *, +
*', +', FACT
c4, c6, c2
We considered the (Usable) Rules:
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
And the Tuples:
fact(0) → s(0) 254.94/218.78
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.78
p(s(z0)) → z0 254.94/218.78
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.78
*(0, z0) → 0 254.94/218.78
+(z0, 0) → z0 254.94/218.78
+(z0, s(z1)) → s(+(z0, z1))
The order we found is given by the following interpretation:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.78
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
POL(*(x1, x2)) = [2]x2 254.94/218.78
POL(*'(x1, x2)) = 0 254.94/218.78
POL(+(x1, x2)) = [5] + [3]x2 254.94/218.78
POL(+'(x1, x2)) = 0 254.94/218.78
POL(0) = [5] 254.94/218.78
POL(FACT(x1)) = [4]x1 254.94/218.78
POL(c2(x1, x2)) = x1 + x2 254.94/218.78
POL(c4(x1, x2)) = x1 + x2 254.94/218.78
POL(c6(x1)) = x1 254.94/218.78
POL(fact(x1)) = [2] + [4]x1 254.94/218.78
POL(p(x1)) = [1] 254.94/218.78
POL(s(x1)) = [4] + x1
Tuples:
p(s(z0)) → z0 254.94/218.78
fact(0) → s(0) 254.94/218.78
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.78
*(0, z0) → 0 254.94/218.78
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.78
+(z0, 0) → z0 254.94/218.78
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.78
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
K tuples:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
+'(z0, s(z1)) → c6(+'(z0, z1))
Defined Rule Symbols:
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
p, fact, *, +
*', +', FACT
c4, c6, c2
We considered the (Usable) Rules:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1))
And the Tuples:
fact(0) → s(0) 254.94/218.78
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.78
p(s(z0)) → z0 254.94/218.78
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.78
*(0, z0) → 0 254.94/218.78
+(z0, 0) → z0 254.94/218.78
+(z0, s(z1)) → s(+(z0, z1))
The order we found is given by the following interpretation:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.78
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
POL(*(x1, x2)) = 0 254.94/218.78
POL(*'(x1, x2)) = [2]x1 254.94/218.78
POL(+(x1, x2)) = [3] + [3]x2 + [3]x22 254.94/218.78
POL(+'(x1, x2)) = 0 254.94/218.78
POL(0) = 0 254.94/218.78
POL(FACT(x1)) = [2]x1 + x12 254.94/218.78
POL(c2(x1, x2)) = x1 + x2 254.94/218.78
POL(c4(x1, x2)) = x1 + x2 254.94/218.78
POL(c6(x1)) = x1 254.94/218.78
POL(fact(x1)) = 0 254.94/218.78
POL(p(x1)) = 0 254.94/218.78
POL(s(x1)) = [2] + x1
Tuples:
p(s(z0)) → z0 254.94/218.78
fact(0) → s(0) 254.94/218.78
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.78
*(0, z0) → 0 254.94/218.78
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.78
+(z0, 0) → z0 254.94/218.78
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
+'(z0, s(z1)) → c6(+'(z0, z1)) 254.94/218.78
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0))
K tuples:
+'(z0, s(z1)) → c6(+'(z0, z1))
Defined Rule Symbols:
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0)) 254.94/218.78
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1))
p, fact, *, +
*', +', FACT
c4, c6, c2
+'(z0, s(s(y1))) → c6(+'(z0, s(y1)))
Tuples:
p(s(z0)) → z0 254.94/218.78
fact(0) → s(0) 254.94/218.78
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.78
*(0, z0) → 0 254.94/218.78
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.78
+(z0, 0) → z0 254.94/218.78
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0)) 254.94/218.78
+'(z0, s(s(y1))) → c6(+'(z0, s(y1)))
K tuples:
+'(z0, s(s(y1))) → c6(+'(z0, s(y1)))
Defined Rule Symbols:
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0)) 254.94/218.78
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1))
p, fact, *, +
*', FACT, +'
c4, c2, c6
+'(z0, s(s(s(y1)))) → c6(+'(z0, s(s(y1))))
Tuples:
p(s(z0)) → z0 254.94/218.78
fact(0) → s(0) 254.94/218.78
fact(s(z0)) → *(s(z0), fact(p(s(z0)))) 254.94/218.78
*(0, z0) → 0 254.94/218.78
*(s(z0), z1) → +(*(z0, z1), z1) 254.94/218.78
+(z0, 0) → z0 254.94/218.78
+(z0, s(z1)) → s(+(z0, z1))
S tuples:
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1)) 254.94/218.78
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0)) 254.94/218.78
+'(z0, s(s(s(y1)))) → c6(+'(z0, s(s(y1))))
K tuples:
+'(z0, s(s(s(y1)))) → c6(+'(z0, s(s(y1))))
Defined Rule Symbols:
FACT(s(z0)) → c2(*'(s(z0), fact(z0)), FACT(z0)) 254.94/218.78
*'(s(z0), z1) → c4(+'(*(z0, z1), z1), *'(z0, z1))
p, fact, *, +
*', FACT, +'
c4, c2, c6