YES(O(1), O(n^2)) 39.72/18.93 YES(O(1), O(n^2)) 39.72/18.95 39.72/18.95 39.72/18.95
39.72/18.95 39.72/18.950 CpxTRS39.72/18.95
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳2 CdtProblem39.72/18.95
↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳4 CdtProblem39.72/18.95
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳6 CdtProblem39.72/18.95
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳8 CdtProblem39.72/18.95
↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳10 CdtProblem39.72/18.95
↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳12 CdtProblem39.72/18.95
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))39.72/18.95
↳14 CdtProblem39.72/18.95
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))39.72/18.95
↳16 CdtProblem39.72/18.95
↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳18 CdtProblem39.72/18.95
↳19 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳20 CdtProblem39.72/18.95
↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳22 CdtProblem39.72/18.95
↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))39.72/18.95
↳24 CdtProblem39.72/18.95
↳25 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳26 CdtProblem39.72/18.95
↳27 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))39.72/18.95
↳28 CdtProblem39.72/18.95
↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))39.72/18.95
↳30 CdtProblem39.72/18.95
↳31 SIsEmptyProof (BOTH BOUNDS(ID, ID))39.72/18.95
↳32 BOUNDS(O(1), O(1))39.72/18.95
le(0, y) → true 39.72/18.95
le(s(x), 0) → false 39.72/18.95
le(s(x), s(y)) → le(x, y) 39.72/18.95
minus(x, 0) → x 39.72/18.95
minus(0, x) → 0 39.72/18.95
minus(s(x), s(y)) → minus(x, y) 39.72/18.95
gcd(0, y) → y 39.72/18.95
gcd(s(x), 0) → s(x) 39.72/18.95
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y)) 39.72/18.95
if_gcd(true, x, y) → gcd(minus(x, y), y) 39.72/18.95
if_gcd(false, x, y) → gcd(minus(y, x), x)
Tuples:
le(0, z0) → true 39.72/18.95
le(s(z0), 0) → false 39.72/18.95
le(s(z0), s(z1)) → le(z0, z1) 39.72/18.95
minus(z0, 0) → z0 39.72/18.95
minus(0, z0) → 0 39.72/18.95
minus(s(z0), s(z1)) → minus(z0, z1) 39.72/18.95
gcd(0, z0) → z0 39.72/18.95
gcd(s(z0), 0) → s(z0) 39.72/18.95
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 39.72/18.95
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 39.72/18.95
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 39.72/18.95
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 39.72/18.95
GCD(s(z0), s(z1)) → c8(IF_GCD(le(z1, z0), s(z0), s(z1)), LE(z1, z0)) 39.72/18.95
IF_GCD(true, z0, z1) → c9(GCD(minus(z0, z1), z1), MINUS(z0, z1)) 39.72/18.95
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0))
K tuples:none
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 39.72/18.95
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 39.72/18.95
GCD(s(z0), s(z1)) → c8(IF_GCD(le(z1, z0), s(z0), s(z1)), LE(z1, z0)) 39.72/18.95
IF_GCD(true, z0, z1) → c9(GCD(minus(z0, z1), z1), MINUS(z0, z1)) 39.72/18.95
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0))
le, minus, gcd, if_gcd
LE, MINUS, GCD, IF_GCD
c2, c5, c8, c9, c10
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0)), LE(0, z0)) 39.72/18.95
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))), LE(s(z0), 0)) 39.72/18.95
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1)))
Tuples:
le(0, z0) → true 39.72/18.95
le(s(z0), 0) → false 39.72/18.95
le(s(z0), s(z1)) → le(z0, z1) 39.72/18.95
minus(z0, 0) → z0 39.72/18.95
minus(0, z0) → 0 39.72/18.95
minus(s(z0), s(z1)) → minus(z0, z1) 39.72/18.95
gcd(0, z0) → z0 39.72/18.95
gcd(s(z0), 0) → s(z0) 39.72/18.95
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 39.72/18.95
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 39.72/18.95
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 39.72/18.95
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 39.72/18.95
IF_GCD(true, z0, z1) → c9(GCD(minus(z0, z1), z1), MINUS(z0, z1)) 39.72/18.95
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 39.72/18.95
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0)), LE(0, z0)) 39.72/18.95
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))), LE(s(z0), 0)) 39.72/18.95
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1)))
K tuples:none
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 39.72/18.95
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 39.72/18.96
IF_GCD(true, z0, z1) → c9(GCD(minus(z0, z1), z1), MINUS(z0, z1)) 39.72/18.96
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 39.72/18.96
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0)), LE(0, z0)) 39.72/18.96
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))), LE(s(z0), 0)) 39.72/18.96
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1)))
le, minus, gcd, if_gcd
LE, MINUS, IF_GCD, GCD
c2, c5, c9, c10, c8
Tuples:
le(0, z0) → true 39.72/18.96
le(s(z0), 0) → false 39.72/18.96
le(s(z0), s(z1)) → le(z0, z1) 39.72/18.96
minus(z0, 0) → z0 39.72/18.96
minus(0, z0) → 0 39.72/18.96
minus(s(z0), s(z1)) → minus(z0, z1) 39.72/18.96
gcd(0, z0) → z0 39.72/18.96
gcd(s(z0), 0) → s(z0) 39.72/18.96
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 39.72/18.96
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 39.72/18.96
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 39.72/18.96
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 39.72/18.96
IF_GCD(true, z0, z1) → c9(GCD(minus(z0, z1), z1), MINUS(z0, z1)) 39.72/18.96
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 39.72/18.96
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 39.72/18.96
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 39.72/18.96
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))))
K tuples:none
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 39.72/18.96
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 39.72/18.96
IF_GCD(true, z0, z1) → c9(GCD(minus(z0, z1), z1), MINUS(z0, z1)) 39.72/18.96
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 39.72/18.96
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 39.72/18.96
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 39.72/18.96
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))))
le, minus, gcd, if_gcd
LE, MINUS, IF_GCD, GCD
c2, c5, c9, c10, c8, c8
IF_GCD(true, z0, 0) → c9(GCD(z0, 0), MINUS(z0, 0)) 39.72/18.96
IF_GCD(true, 0, z0) → c9(GCD(0, z0), MINUS(0, z0)) 39.72/18.96
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
Tuples:
le(0, z0) → true 39.72/18.96
le(s(z0), 0) → false 39.72/18.96
le(s(z0), s(z1)) → le(z0, z1) 39.72/18.96
minus(z0, 0) → z0 39.72/18.96
minus(0, z0) → 0 39.72/18.97
minus(s(z0), s(z1)) → minus(z0, z1) 39.72/18.97
gcd(0, z0) → z0 39.72/18.97
gcd(s(z0), 0) → s(z0) 39.72/18.97
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 39.72/18.97
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 39.72/18.97
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 39.72/18.97
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 39.72/18.97
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 39.72/18.97
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 39.72/18.97
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 39.72/18.97
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 39.72/18.97
IF_GCD(true, z0, 0) → c9(GCD(z0, 0), MINUS(z0, 0)) 39.72/18.97
IF_GCD(true, 0, z0) → c9(GCD(0, z0), MINUS(0, z0)) 39.72/18.97
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:none
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 39.72/18.97
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 39.72/18.97
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 39.72/18.97
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 39.72/18.97
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 39.72/18.97
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.01
IF_GCD(true, z0, 0) → c9(GCD(z0, 0), MINUS(z0, 0)) 40.21/19.01
IF_GCD(true, 0, z0) → c9(GCD(0, z0), MINUS(0, z0)) 40.21/19.01
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
le, minus, gcd, if_gcd
LE, MINUS, IF_GCD, GCD
c2, c5, c10, c8, c8, c9
Tuples:
le(0, z0) → true 40.21/19.01
le(s(z0), 0) → false 40.21/19.01
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.01
minus(z0, 0) → z0 40.21/19.01
minus(0, z0) → 0 40.21/19.01
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.01
gcd(0, z0) → z0 40.21/19.01
gcd(s(z0), 0) → s(z0) 40.21/19.01
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.01
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.01
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.01
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.01
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.01
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.01
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.01
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.01
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.01
IF_GCD(true, z0, 0) → c9 40.21/19.01
IF_GCD(true, 0, z0) → c9
K tuples:none
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.01
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.01
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.01
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.01
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.01
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.01
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.01
IF_GCD(true, z0, 0) → c9 40.21/19.01
IF_GCD(true, 0, z0) → c9
le, minus, gcd, if_gcd
LE, MINUS, IF_GCD, GCD
c2, c5, c10, c8, c8, c9, c9
IF_GCD(true, 0, z0) → c9 40.21/19.01
IF_GCD(true, z0, 0) → c9
Tuples:
le(0, z0) → true 40.21/19.01
le(s(z0), 0) → false 40.21/19.01
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.01
minus(z0, 0) → z0 40.21/19.01
minus(0, z0) → 0 40.21/19.01
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.01
gcd(0, z0) → z0 40.21/19.01
gcd(s(z0), 0) → s(z0) 40.21/19.01
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.01
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.01
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.01
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.01
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.01
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.01
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.01
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.01
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:none
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.01
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.01
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.01
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.01
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.01
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.01
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
le, minus, gcd, if_gcd
LE, MINUS, IF_GCD, GCD
c2, c5, c10, c8, c8, c9
We considered the (Usable) Rules:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
And the Tuples:
minus(z0, 0) → z0 40.21/19.01
minus(0, z0) → 0 40.21/19.01
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.01
le(0, z0) → true 40.21/19.01
le(s(z0), 0) → false 40.21/19.01
le(s(z0), s(z1)) → le(z0, z1)
The order we found is given by the following interpretation:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.01
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.01
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.01
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.01
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.01
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.01
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
POL(0) = 0 40.21/19.01
POL(GCD(x1, x2)) = [4]x1 + [4]x2 40.21/19.01
POL(IF_GCD(x1, x2, x3)) = [4]x2 + [4]x3 40.21/19.01
POL(LE(x1, x2)) = 0 40.21/19.01
POL(MINUS(x1, x2)) = 0 40.21/19.01
POL(c10(x1, x2)) = x1 + x2 40.21/19.01
POL(c2(x1)) = x1 40.21/19.01
POL(c5(x1)) = x1 40.21/19.01
POL(c8(x1)) = x1 40.21/19.01
POL(c8(x1, x2)) = x1 + x2 40.21/19.01
POL(c9(x1, x2)) = x1 + x2 40.21/19.01
POL(false) = 0 40.21/19.01
POL(le(x1, x2)) = 0 40.21/19.01
POL(minus(x1, x2)) = x1 40.21/19.01
POL(s(x1)) = [4] + x1 40.21/19.01
POL(true) = 0
Tuples:
le(0, z0) → true 40.21/19.01
le(s(z0), 0) → false 40.21/19.01
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.01
minus(z0, 0) → z0 40.21/19.01
minus(0, z0) → 0 40.21/19.01
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.02
gcd(0, z0) → z0 40.21/19.02
gcd(s(z0), 0) → s(z0) 40.21/19.02
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.02
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.02
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.02
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))))
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
le, minus, gcd, if_gcd
LE, MINUS, IF_GCD, GCD
c2, c5, c10, c8, c8, c9
We considered the (Usable) Rules:
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0)))
And the Tuples:
minus(z0, 0) → z0 40.21/19.02
minus(0, z0) → 0 40.21/19.02
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.02
le(0, z0) → true 40.21/19.02
le(s(z0), 0) → false 40.21/19.02
le(s(z0), s(z1)) → le(z0, z1)
The order we found is given by the following interpretation:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.02
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
POL(0) = 0 40.21/19.02
POL(GCD(x1, x2)) = [1] + [2]x1 + [2]x2 40.21/19.02
POL(IF_GCD(x1, x2, x3)) = x1 + [2]x2 + [2]x3 40.21/19.02
POL(LE(x1, x2)) = 0 40.21/19.02
POL(MINUS(x1, x2)) = 0 40.21/19.02
POL(c10(x1, x2)) = x1 + x2 40.21/19.02
POL(c2(x1)) = x1 40.21/19.02
POL(c5(x1)) = x1 40.21/19.02
POL(c8(x1)) = x1 40.21/19.02
POL(c8(x1, x2)) = x1 + x2 40.21/19.02
POL(c9(x1, x2)) = x1 + x2 40.21/19.02
POL(false) = [1] 40.21/19.02
POL(le(x1, x2)) = [1] 40.21/19.02
POL(minus(x1, x2)) = x1 40.21/19.02
POL(s(x1)) = [4] + x1 40.21/19.02
POL(true) = 0
Tuples:
le(0, z0) → true 40.21/19.02
le(s(z0), 0) → false 40.21/19.02
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.02
minus(z0, 0) → z0 40.21/19.02
minus(0, z0) → 0 40.21/19.02
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.02
gcd(0, z0) → z0 40.21/19.02
gcd(s(z0), 0) → s(z0) 40.21/19.02
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.02
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.02
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.02
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
IF_GCD(false, z0, z1) → c10(GCD(minus(z1, z0), z0), MINUS(z1, z0)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))))
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0)))
le, minus, gcd, if_gcd
LE, MINUS, IF_GCD, GCD
c2, c5, c10, c8, c8, c9
IF_GCD(false, 0, z0) → c10(GCD(z0, 0), MINUS(z0, 0)) 40.21/19.02
IF_GCD(false, z0, 0) → c10(GCD(0, z0), MINUS(0, z0)) 40.21/19.02
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
Tuples:
le(0, z0) → true 40.21/19.02
le(s(z0), 0) → false 40.21/19.02
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.02
minus(z0, 0) → z0 40.21/19.02
minus(0, z0) → 0 40.21/19.02
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.02
gcd(0, z0) → z0 40.21/19.02
gcd(s(z0), 0) → s(z0) 40.21/19.02
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.02
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.02
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.02
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.02
IF_GCD(false, 0, z0) → c10(GCD(z0, 0), MINUS(z0, 0)) 40.21/19.02
IF_GCD(false, z0, 0) → c10(GCD(0, z0), MINUS(0, z0)) 40.21/19.02
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.02
IF_GCD(false, 0, z0) → c10(GCD(z0, 0), MINUS(z0, 0)) 40.21/19.02
IF_GCD(false, z0, 0) → c10(GCD(0, z0), MINUS(0, z0)) 40.21/19.02
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0)))
le, minus, gcd, if_gcd
LE, MINUS, GCD, IF_GCD
c2, c5, c8, c8, c9, c10
Tuples:
le(0, z0) → true 40.21/19.02
le(s(z0), 0) → false 40.21/19.02
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.02
minus(z0, 0) → z0 40.21/19.02
minus(0, z0) → 0 40.21/19.02
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.02
gcd(0, z0) → z0 40.21/19.02
gcd(s(z0), 0) → s(z0) 40.21/19.02
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.02
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.02
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.02
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.02
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.02
IF_GCD(false, 0, z0) → c10 40.21/19.02
IF_GCD(false, z0, 0) → c10
K tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.02
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.02
IF_GCD(false, 0, z0) → c10 40.21/19.02
IF_GCD(false, z0, 0) → c10
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0)))
le, minus, gcd, if_gcd
LE, MINUS, GCD, IF_GCD
c2, c5, c8, c8, c9, c10, c10
IF_GCD(false, z0, 0) → c10 40.21/19.02
IF_GCD(false, 0, z0) → c10
Tuples:
le(0, z0) → true 40.21/19.02
le(s(z0), 0) → false 40.21/19.02
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.02
minus(z0, 0) → z0 40.21/19.02
minus(0, z0) → 0 40.21/19.02
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.02
gcd(0, z0) → z0 40.21/19.02
gcd(s(z0), 0) → s(z0) 40.21/19.02
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.02
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.02
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.02
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.02
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.02
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.02
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.02
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0)))
le, minus, gcd, if_gcd
LE, MINUS, GCD, IF_GCD
c2, c5, c8, c8, c9, c10
We considered the (Usable) Rules:
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
And the Tuples:
minus(z0, 0) → z0 40.21/19.03
minus(0, z0) → 0 40.21/19.03
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.03
le(0, z0) → true 40.21/19.03
le(s(z0), 0) → false 40.21/19.03
le(s(z0), s(z1)) → le(z0, z1)
The order we found is given by the following interpretation:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
POL(0) = 0 40.21/19.03
POL(GCD(x1, x2)) = [4]x1 + [4]x2 40.21/19.03
POL(IF_GCD(x1, x2, x3)) = [4]x2 + [4]x3 40.21/19.03
POL(LE(x1, x2)) = 0 40.21/19.03
POL(MINUS(x1, x2)) = 0 40.21/19.03
POL(c10(x1, x2)) = x1 + x2 40.21/19.03
POL(c2(x1)) = x1 40.21/19.03
POL(c5(x1)) = x1 40.21/19.03
POL(c8(x1)) = x1 40.21/19.03
POL(c8(x1, x2)) = x1 + x2 40.21/19.03
POL(c9(x1, x2)) = x1 + x2 40.21/19.03
POL(false) = 0 40.21/19.03
POL(le(x1, x2)) = 0 40.21/19.03
POL(minus(x1, x2)) = x1 40.21/19.03
POL(s(x1)) = [2] + x1 40.21/19.03
POL(true) = 0
Tuples:
le(0, z0) → true 40.21/19.03
le(s(z0), 0) → false 40.21/19.03
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.03
minus(z0, 0) → z0 40.21/19.03
minus(0, z0) → 0 40.21/19.03
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.03
gcd(0, z0) → z0 40.21/19.03
gcd(s(z0), 0) → s(z0) 40.21/19.03
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.03
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.03
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))))
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
le, minus, gcd, if_gcd
LE, MINUS, GCD, IF_GCD
c2, c5, c8, c8, c9, c10
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
Tuples:
le(0, z0) → true 40.21/19.03
le(s(z0), 0) → false 40.21/19.03
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.03
minus(z0, 0) → z0 40.21/19.03
minus(0, z0) → 0 40.21/19.03
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.03
gcd(0, z0) → z0 40.21/19.03
gcd(s(z0), 0) → s(z0) 40.21/19.03
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.03
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.03
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1))
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0))))
le, minus, gcd, if_gcd
LE, MINUS, GCD, IF_GCD
c2, c5, c8, c8, c9, c10
We considered the (Usable) Rules:
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1))
And the Tuples:
minus(z0, 0) → z0 40.21/19.03
minus(0, z0) → 0 40.21/19.03
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.03
le(0, z0) → true 40.21/19.03
le(s(z0), 0) → false 40.21/19.03
le(s(z0), s(z1)) → le(z0, z1)
The order we found is given by the following interpretation:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
POL(0) = 0 40.21/19.03
POL(GCD(x1, x2)) = [3] + [2]x1·x2 40.21/19.03
POL(IF_GCD(x1, x2, x3)) = [2]x2·x3 40.21/19.03
POL(LE(x1, x2)) = 0 40.21/19.03
POL(MINUS(x1, x2)) = [3] + x2 40.21/19.03
POL(c10(x1, x2)) = x1 + x2 40.21/19.03
POL(c2(x1)) = x1 40.21/19.03
POL(c5(x1)) = x1 40.21/19.03
POL(c8(x1)) = x1 40.21/19.03
POL(c8(x1, x2)) = x1 + x2 40.21/19.03
POL(c9(x1, x2)) = x1 + x2 40.21/19.03
POL(false) = 0 40.21/19.03
POL(le(x1, x2)) = 0 40.21/19.03
POL(minus(x1, x2)) = x1 40.21/19.03
POL(s(x1)) = [2] + x1 40.21/19.03
POL(true) = 0
Tuples:
le(0, z0) → true 40.21/19.03
le(s(z0), 0) → false 40.21/19.03
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.03
minus(z0, 0) → z0 40.21/19.03
minus(0, z0) → 0 40.21/19.03
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.03
gcd(0, z0) → z0 40.21/19.03
gcd(s(z0), 0) → s(z0) 40.21/19.03
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.03
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.03
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
K tuples:
LE(s(z0), s(z1)) → c2(LE(z0, z1))
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1))
le, minus, gcd, if_gcd
LE, MINUS, GCD, IF_GCD
c2, c5, c8, c8, c9, c10
We considered the (Usable) Rules:
LE(s(z0), s(z1)) → c2(LE(z0, z1))
And the Tuples:
minus(z0, 0) → z0 40.21/19.03
minus(0, z0) → 0 40.21/19.03
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.03
le(0, z0) → true 40.21/19.03
le(s(z0), 0) → false 40.21/19.03
le(s(z0), s(z1)) → le(z0, z1)
The order we found is given by the following interpretation:
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
POL(0) = 0 40.21/19.03
POL(GCD(x1, x2)) = [1] + [2]x2 + [2]x1·x2 40.21/19.03
POL(IF_GCD(x1, x2, x3)) = [1] + [2]x2·x3 40.21/19.03
POL(LE(x1, x2)) = [3] + [2]x1 40.21/19.03
POL(MINUS(x1, x2)) = [2]x2 40.21/19.03
POL(c10(x1, x2)) = x1 + x2 40.21/19.03
POL(c2(x1)) = x1 40.21/19.03
POL(c5(x1)) = x1 40.21/19.03
POL(c8(x1)) = x1 40.21/19.03
POL(c8(x1, x2)) = x1 + x2 40.21/19.03
POL(c9(x1, x2)) = x1 + x2 40.21/19.03
POL(false) = 0 40.21/19.03
POL(le(x1, x2)) = 0 40.21/19.03
POL(minus(x1, x2)) = x1 40.21/19.03
POL(s(x1)) = [2] + x1 40.21/19.03
POL(true) = 0
Tuples:
le(0, z0) → true 40.21/19.03
le(s(z0), 0) → false 40.21/19.03
le(s(z0), s(z1)) → le(z0, z1) 40.21/19.03
minus(z0, 0) → z0 40.21/19.03
minus(0, z0) → 0 40.21/19.03
minus(s(z0), s(z1)) → minus(z0, z1) 40.21/19.03
gcd(0, z0) → z0 40.21/19.03
gcd(s(z0), 0) → s(z0) 40.21/19.03
gcd(s(z0), s(z1)) → if_gcd(le(z1, z0), s(z0), s(z1)) 40.21/19.03
if_gcd(true, z0, z1) → gcd(minus(z0, z1), z1) 40.21/19.03
if_gcd(false, z0, z1) → gcd(minus(z1, z0), z0)
S tuples:none
LE(s(z0), s(z1)) → c2(LE(z0, z1)) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1)))
Defined Rule Symbols:
IF_GCD(true, s(z0), s(z1)) → c9(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
GCD(s(z0), s(0)) → c8(IF_GCD(true, s(z0), s(0))) 40.21/19.03
IF_GCD(false, s(z1), s(z0)) → c10(GCD(minus(z0, z1), s(z1)), MINUS(s(z0), s(z1))) 40.21/19.03
GCD(s(s(z1)), s(s(z0))) → c8(IF_GCD(le(z0, z1), s(s(z1)), s(s(z0))), LE(s(z0), s(z1))) 40.21/19.03
GCD(s(0), s(s(z0))) → c8(IF_GCD(false, s(0), s(s(z0)))) 40.21/19.03
MINUS(s(z0), s(z1)) → c5(MINUS(z0, z1)) 40.21/19.03
LE(s(z0), s(z1)) → c2(LE(z0, z1))
le, minus, gcd, if_gcd
LE, MINUS, GCD, IF_GCD
c2, c5, c8, c8, c9, c10