(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
leq(0, z0) → true
leq(s(z0), 0) → false
leq(s(z0), s(z1)) → leq(z0, z1)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
-(z0, 0) → z0
-(s(z0), s(z1)) → -(z0, z1)
mod(0, z0) → 0
mod(s(z0), 0) → 0
mod(s(z0), s(z1)) → if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))
Tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
S tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
K tuples:none
Defined Rule Symbols:
leq, if, -, mod
Defined Pair Symbols:
LEQ, -', MOD
Compound Symbols:
c2, c6, c9
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
leq(0, z0) → true
leq(s(z0), 0) → false
leq(s(z0), s(z1)) → leq(z0, z1)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
-(z0, 0) → z0
-(s(z0), s(z1)) → -(z0, z1)
mod(0, z0) → 0
mod(s(z0), 0) → 0
mod(s(z0), s(z1)) → if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))
Tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
S tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
K tuples:none
Defined Rule Symbols:
leq, if, -, mod
Defined Pair Symbols:
LEQ, -', MOD
Compound Symbols:
c2, c6, c9
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MOD(
s(
z0),
s(
z1)) →
c9(
LEQ(
z1,
z0),
MOD(
-(
s(
z0),
s(
z1)),
s(
z1)),
-'(
s(
z0),
s(
z1))) by
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
MOD(s(x0), s(x1)) → c9
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
leq(0, z0) → true
leq(s(z0), 0) → false
leq(s(z0), s(z1)) → leq(z0, z1)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
-(z0, 0) → z0
-(s(z0), s(z1)) → -(z0, z1)
mod(0, z0) → 0
mod(s(z0), 0) → 0
mod(s(z0), s(z1)) → if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))
Tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
MOD(s(x0), s(x1)) → c9
S tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
MOD(s(x0), s(x1)) → c9
K tuples:none
Defined Rule Symbols:
leq, if, -, mod
Defined Pair Symbols:
LEQ, -', MOD
Compound Symbols:
c2, c6, c9, c9
(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
MOD(s(x0), s(x1)) → c9
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
leq(0, z0) → true
leq(s(z0), 0) → false
leq(s(z0), s(z1)) → leq(z0, z1)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
-(z0, 0) → z0
-(s(z0), s(z1)) → -(z0, z1)
mod(0, z0) → 0
mod(s(z0), 0) → 0
mod(s(z0), s(z1)) → if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))
Tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
S tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
K tuples:none
Defined Rule Symbols:
leq, if, -, mod
Defined Pair Symbols:
LEQ, -', MOD
Compound Symbols:
c2, c6, c9
(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
We considered the (Usable) Rules:
-(z0, 0) → z0
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(-(x1, x2)) = x1
POL(-'(x1, x2)) = [4]
POL(0) = 0
POL(LEQ(x1, x2)) = [3]
POL(MOD(x1, x2)) = [4]x1
POL(c2(x1)) = x1
POL(c6(x1)) = x1
POL(c9(x1, x2, x3)) = x1 + x2 + x3
POL(s(x1)) = [2] + x1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
leq(0, z0) → true
leq(s(z0), 0) → false
leq(s(z0), s(z1)) → leq(z0, z1)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
-(z0, 0) → z0
-(s(z0), s(z1)) → -(z0, z1)
mod(0, z0) → 0
mod(s(z0), 0) → 0
mod(s(z0), s(z1)) → if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))
Tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
S tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
K tuples:
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
Defined Rule Symbols:
leq, if, -, mod
Defined Pair Symbols:
LEQ, -', MOD
Compound Symbols:
c2, c6, c9
(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
We considered the (Usable) Rules:
-(z0, 0) → z0
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(-(x1, x2)) = x1
POL(-'(x1, x2)) = x1
POL(0) = 0
POL(LEQ(x1, x2)) = x2
POL(MOD(x1, x2)) = x12
POL(c2(x1)) = x1
POL(c6(x1)) = x1
POL(c9(x1, x2, x3)) = x1 + x2 + x3
POL(s(x1)) = [1] + x1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
leq(0, z0) → true
leq(s(z0), 0) → false
leq(s(z0), s(z1)) → leq(z0, z1)
if(true, z0, z1) → z0
if(false, z0, z1) → z1
-(z0, 0) → z0
-(s(z0), s(z1)) → -(z0, z1)
mod(0, z0) → 0
mod(s(z0), 0) → 0
mod(s(z0), s(z1)) → if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))
Tuples:
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
S tuples:none
K tuples:
MOD(s(z0), s(z1)) → c9(LEQ(z1, z0), MOD(-(z0, z1), s(z1)), -'(s(z0), s(z1)))
LEQ(s(z0), s(z1)) → c2(LEQ(z0, z1))
-'(s(z0), s(z1)) → c6(-'(z0, z1))
Defined Rule Symbols:
leq, if, -, mod
Defined Pair Symbols:
LEQ, -', MOD
Compound Symbols:
c2, c6, c9
(13) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(14) BOUNDS(O(1), O(1))