YES(O(1), O(n^1)) 6.91/2.34 YES(O(1), O(n^1)) 6.91/2.36 6.91/2.36 6.91/2.36
6.91/2.36 6.91/2.360 CpxTRS6.91/2.36
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳2 CdtProblem6.91/2.36
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳4 CdtProblem6.91/2.36
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)6.91/2.36
↳6 CdtProblem6.91/2.36
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳8 CdtProblem6.91/2.36
↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳10 CdtProblem6.91/2.36
↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳12 CdtProblem6.91/2.36
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))6.91/2.36
↳14 CdtProblem6.91/2.36
↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳16 CdtProblem6.91/2.36
↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳18 CdtProblem6.91/2.36
↳19 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳20 CdtProblem6.91/2.36
↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))6.91/2.36
↳22 CdtProblem6.91/2.36
↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳24 CdtProblem6.91/2.36
↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳26 CdtProblem6.91/2.36
↳27 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))6.91/2.36
↳28 CdtProblem6.91/2.36
↳29 CdtNarrowingProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳30 CdtProblem6.91/2.36
↳31 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))6.91/2.36
↳32 CdtProblem6.91/2.36
↳33 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))6.91/2.36
↳34 CdtProblem6.91/2.36
↳35 CdtKnowledgeProof (⇔)6.91/2.36
↳36 BOUNDS(O(1), O(1))6.91/2.36
nonZero(0) → false 6.91/2.36
nonZero(s(x)) → true 6.91/2.36
p(0) → 0 6.91/2.36
p(s(x)) → x 6.91/2.36
id_inc(x) → x 6.91/2.36
id_inc(x) → s(x) 6.91/2.36
random(x) → rand(x, 0) 6.91/2.36
rand(x, y) → if(nonZero(x), x, y) 6.91/2.36
if(false, x, y) → y 6.91/2.36
if(true, x, y) → rand(p(x), id_inc(y))
Tuples:
nonZero(0) → false 6.91/2.36
nonZero(s(z0)) → true 6.91/2.36
p(0) → 0 6.91/2.36
p(s(z0)) → z0 6.91/2.36
id_inc(z0) → z0 6.91/2.36
id_inc(z0) → s(z0) 6.91/2.36
random(z0) → rand(z0, 0) 7.28/2.40
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.40
if(false, z0, z1) → z1 7.28/2.40
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RANDOM(z0) → c6(RAND(z0, 0)) 7.28/2.40
RAND(z0, z1) → c7(IF(nonZero(z0), z0, z1), NONZERO(z0)) 7.28/2.40
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1)), P(z0), ID_INC(z1))
K tuples:none
RANDOM(z0) → c6(RAND(z0, 0)) 7.28/2.40
RAND(z0, z1) → c7(IF(nonZero(z0), z0, z1), NONZERO(z0)) 7.28/2.40
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1)), P(z0), ID_INC(z1))
nonZero, p, id_inc, random, rand, if
RANDOM, RAND, IF
c6, c7, c9
Tuples:
nonZero(0) → false 7.28/2.40
nonZero(s(z0)) → true 7.28/2.40
p(0) → 0 7.28/2.40
p(s(z0)) → z0 7.28/2.40
id_inc(z0) → z0 7.28/2.40
id_inc(z0) → s(z0) 7.28/2.40
random(z0) → rand(z0, 0) 7.28/2.40
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.40
if(false, z0, z1) → z1 7.28/2.40
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RANDOM(z0) → c6(RAND(z0, 0)) 7.28/2.40
RAND(z0, z1) → c7(IF(nonZero(z0), z0, z1)) 7.28/2.40
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1)))
K tuples:none
RANDOM(z0) → c6(RAND(z0, 0)) 7.28/2.40
RAND(z0, z1) → c7(IF(nonZero(z0), z0, z1)) 7.28/2.40
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1)))
nonZero, p, id_inc, random, rand, if
RANDOM, RAND, IF
c6, c7, c9
RANDOM(z0) → c6(RAND(z0, 0))
Tuples:
nonZero(0) → false 7.28/2.40
nonZero(s(z0)) → true 7.28/2.40
p(0) → 0 7.28/2.40
p(s(z0)) → z0 7.28/2.40
id_inc(z0) → z0 7.28/2.40
id_inc(z0) → s(z0) 7.28/2.40
random(z0) → rand(z0, 0) 7.28/2.40
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.40
if(false, z0, z1) → z1 7.28/2.40
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(z0, z1) → c7(IF(nonZero(z0), z0, z1)) 7.28/2.40
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1)))
K tuples:none
RAND(z0, z1) → c7(IF(nonZero(z0), z0, z1)) 7.28/2.40
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1)))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c9
RAND(0, x1) → c7(IF(false, 0, x1)) 7.28/2.40
RAND(s(z0), x1) → c7(IF(true, s(z0), x1))
Tuples:
nonZero(0) → false 7.28/2.40
nonZero(s(z0)) → true 7.28/2.40
p(0) → 0 7.28/2.40
p(s(z0)) → z0 7.28/2.40
id_inc(z0) → z0 7.28/2.40
id_inc(z0) → s(z0) 7.28/2.40
random(z0) → rand(z0, 0) 7.28/2.40
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.40
if(false, z0, z1) → z1 7.28/2.40
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.40
RAND(0, x1) → c7(IF(false, 0, x1)) 7.28/2.40
RAND(s(z0), x1) → c7(IF(true, s(z0), x1))
K tuples:none
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.40
RAND(0, x1) → c7(IF(false, 0, x1)) 7.28/2.40
RAND(s(z0), x1) → c7(IF(true, s(z0), x1))
nonZero, p, id_inc, random, rand, if
IF, RAND
c9, c7
Tuples:
nonZero(0) → false 7.28/2.40
nonZero(s(z0)) → true 7.28/2.40
p(0) → 0 7.28/2.40
p(s(z0)) → z0 7.28/2.40
id_inc(z0) → z0 7.28/2.40
id_inc(z0) → s(z0) 7.28/2.40
random(z0) → rand(z0, 0) 7.28/2.40
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.40
if(false, z0, z1) → z1 7.28/2.40
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.40
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.40
RAND(0, x1) → c7
K tuples:none
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.40
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.40
RAND(0, x1) → c7
nonZero, p, id_inc, random, rand, if
IF, RAND
c9, c7, c7
RAND(0, x1) → c7
Tuples:
nonZero(0) → false 7.28/2.40
nonZero(s(z0)) → true 7.28/2.40
p(0) → 0 7.28/2.40
p(s(z0)) → z0 7.28/2.40
id_inc(z0) → z0 7.28/2.40
id_inc(z0) → s(z0) 7.28/2.40
random(z0) → rand(z0, 0) 7.28/2.40
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.40
if(false, z0, z1) → z1 7.28/2.40
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.42
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7
K tuples:none
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.42
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7
nonZero, p, id_inc, random, rand, if
IF, RAND
c9, c7, c7
We considered the (Usable) Rules:
RAND(0, x1) → c7
And the Tuples:
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0)
The order we found is given by the following interpretation:
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.42
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7
POL(0) = 0 7.28/2.42
POL(IF(x1, x2, x3)) = [1] + x1 7.28/2.42
POL(RAND(x1, x2)) = [1] 7.28/2.42
POL(c7) = 0 7.28/2.42
POL(c7(x1)) = x1 7.28/2.42
POL(c9(x1)) = x1 7.28/2.42
POL(id_inc(x1)) = [2] + [2]x1 7.28/2.42
POL(p(x1)) = 0 7.28/2.42
POL(s(x1)) = 0 7.28/2.42
POL(true) = 0
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.42
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7
K tuples:
IF(true, z0, z1) → c9(RAND(p(z0), id_inc(z1))) 7.28/2.42
RAND(s(z0), x1) → c7(IF(true, s(z0), x1))
Defined Rule Symbols:
RAND(0, x1) → c7
nonZero, p, id_inc, random, rand, if
IF, RAND
c9, c7, c7
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
Defined Rule Symbols:
RAND(0, x1) → c7
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1)))
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
Defined Rule Symbols:
RAND(0, x1) → c7
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
RAND(0, x1) → c7
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
Defined Rule Symbols:
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1)))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
We considered the (Usable) Rules:
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
And the Tuples:
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0
The order we found is given by the following interpretation:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
POL(0) = 0 7.28/2.42
POL(IF(x1, x2, x3)) = [2]x2 7.28/2.42
POL(RAND(x1, x2)) = [2]x1 7.28/2.42
POL(c7) = 0 7.28/2.42
POL(c7(x1)) = x1 7.28/2.42
POL(c9(x1)) = x1 7.28/2.42
POL(id_inc(x1)) = x1 7.28/2.42
POL(p(x1)) = x1 7.28/2.42
POL(s(x1)) = [2] + x1 7.28/2.42
POL(true) = [1]
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), z0)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0)))
Defined Rule Symbols:
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
IF(true, 0, x1) → c9(RAND(0, x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
Defined Rule Symbols:
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, x1)) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1)))
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
Defined Rule Symbols:
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1)))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
We considered the (Usable) Rules:
IF(true, s(z0), x1) → c9(RAND(z0, x1))
And the Tuples:
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0
The order we found is given by the following interpretation:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
POL(0) = 0 7.28/2.42
POL(IF(x1, x2, x3)) = [4]x2 7.28/2.42
POL(RAND(x1, x2)) = [4]x1 7.28/2.42
POL(c7) = 0 7.28/2.42
POL(c7(x1)) = x1 7.28/2.42
POL(c9(x1)) = x1 7.28/2.42
POL(id_inc(x1)) = [4] + x1 7.28/2.42
POL(p(x1)) = x1 7.28/2.42
POL(s(x1)) = [2] + x1 7.28/2.42
POL(true) = [1]
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0))) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, x0, z0) → c9(RAND(p(x0), s(z0)))
Defined Rule Symbols:
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
IF(true, 0, x1) → c9(RAND(0, s(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1)) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, s(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, s(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
Defined Rule Symbols:
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
IF(true, 0, x1) → c9(RAND(0, s(x1))) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1)))
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
Defined Rule Symbols:
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
We considered the (Usable) Rules:
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
And the Tuples:
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0)
The order we found is given by the following interpretation:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
POL(0) = 0 7.28/2.42
POL(IF(x1, x2, x3)) = [2]x2 7.28/2.42
POL(RAND(x1, x2)) = [2]x1 7.28/2.42
POL(c7) = 0 7.28/2.42
POL(c7(x1)) = x1 7.28/2.42
POL(c9(x1)) = x1 7.28/2.42
POL(id_inc(x1)) = x1 7.28/2.42
POL(s(x1)) = [1] + x1 7.28/2.42
POL(true) = [1]
Tuples:
nonZero(0) → false 7.28/2.42
nonZero(s(z0)) → true 7.28/2.42
p(0) → 0 7.28/2.42
p(s(z0)) → z0 7.28/2.42
id_inc(z0) → z0 7.28/2.42
id_inc(z0) → s(z0) 7.28/2.42
random(z0) → rand(z0, 0) 7.28/2.42
rand(z0, z1) → if(nonZero(z0), z0, z1) 7.28/2.42
if(false, z0, z1) → z1 7.28/2.42
if(true, z0, z1) → rand(p(z0), id_inc(z1))
S tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
K tuples:
RAND(s(z0), x1) → c7(IF(true, s(z0), x1))
Defined Rule Symbols:
RAND(0, x1) → c7 7.28/2.42
IF(true, 0, x1) → c9(RAND(0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))
nonZero, p, id_inc, random, rand, if
RAND, IF
c7, c7, c9
Now S is empty
RAND(s(z0), x1) → c7(IF(true, s(z0), x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, id_inc(x1))) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, x1)) 7.28/2.42
IF(true, s(z0), x1) → c9(RAND(z0, s(x1)))