(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(a(divides, 0), a(s, y)) → true
a(a(divides, a(s, x)), a(s, y)) → a(a(a(div2, x), a(s, y)), y)
a(a(a(div2, x), y), 0) → a(a(divides, x), y)
a(a(a(div2, 0), y), a(s, z)) → false
a(a(a(div2, a(s, x)), y), a(s, z)) → a(a(a(div2, x), y), z)
a(a(filter, f), nil) → nil
a(a(filter, f), a(a(cons, x), xs)) → a(a(a(if, a(f, x)), x), a(a(filter, f), xs))
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), x) → a(not2, a(f, x))
a(not2, true) → false
a(not2, false) → true
a(sieve, nil) → nil
a(sieve, a(a(cons, x), xs)) → a(a(cons, x), a(sieve, a(a(filter, a(not, a(divides, x))), xs)))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(divides, 0), a(s, z0)) → true
a(a(divides, a(s, z0)), a(s, z1)) → a(a(a(div2, z0), a(s, z1)), z1)
a(a(a(div2, z0), z1), 0) → a(a(divides, z0), z1)
a(a(a(div2, 0), z0), a(s, z1)) → false
a(a(a(div2, a(s, z0)), z1), a(s, z2)) → a(a(a(div2, z0), z1), z2)
a(a(filter, z0), nil) → nil
a(a(filter, z0), a(a(cons, z1), z2)) → a(a(a(if, a(z0, z1)), z1), a(a(filter, z0), z2))
a(a(a(if, true), z0), z1) → a(a(cons, z0), z1)
a(a(a(if, false), z0), z1) → z1
a(a(not, z0), z1) → a(not2, a(z0, z1))
a(not2, true) → false
a(not2, false) → true
a(sieve, nil) → nil
a(sieve, a(a(cons, z0), z1)) → a(a(cons, z0), a(sieve, a(a(filter, a(not, a(divides, z0))), z1)))
Tuples:
A(a(divides, a(s, z0)), a(s, z1)) → c1(A(a(a(div2, z0), a(s, z1)), z1), A(a(div2, z0), a(s, z1)), A(div2, z0), A(s, z1))
A(a(a(div2, z0), z1), 0) → c2(A(a(divides, z0), z1), A(divides, z0))
A(a(a(div2, a(s, z0)), z1), a(s, z2)) → c4(A(a(a(div2, z0), z1), z2), A(a(div2, z0), z1), A(div2, z0))
A(a(filter, z0), a(a(cons, z1), z2)) → c6(A(a(a(if, a(z0, z1)), z1), a(a(filter, z0), z2)), A(a(if, a(z0, z1)), z1), A(if, a(z0, z1)), A(z0, z1), A(a(filter, z0), z2), A(filter, z0))
A(a(a(if, true), z0), z1) → c7(A(a(cons, z0), z1), A(cons, z0))
A(a(not, z0), z1) → c9(A(not2, a(z0, z1)), A(z0, z1))
A(sieve, a(a(cons, z0), z1)) → c13(A(a(cons, z0), a(sieve, a(a(filter, a(not, a(divides, z0))), z1))), A(cons, z0), A(sieve, a(a(filter, a(not, a(divides, z0))), z1)), A(a(filter, a(not, a(divides, z0))), z1), A(filter, a(not, a(divides, z0))), A(not, a(divides, z0)), A(divides, z0))
S tuples:
A(a(divides, a(s, z0)), a(s, z1)) → c1(A(a(a(div2, z0), a(s, z1)), z1), A(a(div2, z0), a(s, z1)), A(div2, z0), A(s, z1))
A(a(a(div2, z0), z1), 0) → c2(A(a(divides, z0), z1), A(divides, z0))
A(a(a(div2, a(s, z0)), z1), a(s, z2)) → c4(A(a(a(div2, z0), z1), z2), A(a(div2, z0), z1), A(div2, z0))
A(a(filter, z0), a(a(cons, z1), z2)) → c6(A(a(a(if, a(z0, z1)), z1), a(a(filter, z0), z2)), A(a(if, a(z0, z1)), z1), A(if, a(z0, z1)), A(z0, z1), A(a(filter, z0), z2), A(filter, z0))
A(a(a(if, true), z0), z1) → c7(A(a(cons, z0), z1), A(cons, z0))
A(a(not, z0), z1) → c9(A(not2, a(z0, z1)), A(z0, z1))
A(sieve, a(a(cons, z0), z1)) → c13(A(a(cons, z0), a(sieve, a(a(filter, a(not, a(divides, z0))), z1))), A(cons, z0), A(sieve, a(a(filter, a(not, a(divides, z0))), z1)), A(a(filter, a(not, a(divides, z0))), z1), A(filter, a(not, a(divides, z0))), A(not, a(divides, z0)), A(divides, z0))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c1, c2, c4, c6, c7, c9, c13
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
A(a(divides, a(s, z0)), a(s, z1)) → c1(A(a(a(div2, z0), a(s, z1)), z1), A(a(div2, z0), a(s, z1)), A(div2, z0), A(s, z1))
A(a(a(div2, z0), z1), 0) → c2(A(a(divides, z0), z1), A(divides, z0))
A(a(a(div2, a(s, z0)), z1), a(s, z2)) → c4(A(a(a(div2, z0), z1), z2), A(a(div2, z0), z1), A(div2, z0))
A(a(filter, z0), a(a(cons, z1), z2)) → c6(A(a(a(if, a(z0, z1)), z1), a(a(filter, z0), z2)), A(a(if, a(z0, z1)), z1), A(if, a(z0, z1)), A(z0, z1), A(a(filter, z0), z2), A(filter, z0))
A(a(a(if, true), z0), z1) → c7(A(a(cons, z0), z1), A(cons, z0))
A(a(not, z0), z1) → c9(A(not2, a(z0, z1)), A(z0, z1))
A(sieve, a(a(cons, z0), z1)) → c13(A(a(cons, z0), a(sieve, a(a(filter, a(not, a(divides, z0))), z1))), A(cons, z0), A(sieve, a(a(filter, a(not, a(divides, z0))), z1)), A(a(filter, a(not, a(divides, z0))), z1), A(filter, a(not, a(divides, z0))), A(not, a(divides, z0)), A(divides, z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(divides, 0), a(s, z0)) → true
a(a(divides, a(s, z0)), a(s, z1)) → a(a(a(div2, z0), a(s, z1)), z1)
a(a(a(div2, z0), z1), 0) → a(a(divides, z0), z1)
a(a(a(div2, 0), z0), a(s, z1)) → false
a(a(a(div2, a(s, z0)), z1), a(s, z2)) → a(a(a(div2, z0), z1), z2)
a(a(filter, z0), nil) → nil
a(a(filter, z0), a(a(cons, z1), z2)) → a(a(a(if, a(z0, z1)), z1), a(a(filter, z0), z2))
a(a(a(if, true), z0), z1) → a(a(cons, z0), z1)
a(a(a(if, false), z0), z1) → z1
a(a(not, z0), z1) → a(not2, a(z0, z1))
a(not2, true) → false
a(not2, false) → true
a(sieve, nil) → nil
a(sieve, a(a(cons, z0), z1)) → a(a(cons, z0), a(sieve, a(a(filter, a(not, a(divides, z0))), z1)))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:none
Compound Symbols:none
(5) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(6) BOUNDS(O(1), O(1))