(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(a(append, nil), ys) → ys
a(a(append, a(a(cons, x), xs)), ys) → a(a(cons, x), a(a(append, xs), ys))
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(le, 0), y) → true
a(a(le, a(s, x)), 0) → false
a(a(le, a(s, x)), a(s, y)) → a(a(le, x), y)
a(a(a(if, true), x), xs) → a(a(cons, x), xs)
a(a(a(if, false), x), xs) → xs
a(a(not, f), b) → a(not2, a(f, b))
a(not2, true) → false
a(not2, false) → true
a(qs, nil) → nil
a(qs, a(a(cons, x), xs)) → a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, 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(append, nil), z0) → z0
a(a(append, a(a(cons, z0), z1)), z2) → a(a(cons, z0), a(a(append, 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(le, 0), z0) → true
a(a(le, a(s, z0)), 0) → false
a(a(le, a(s, z0)), a(s, z1)) → a(a(le, z0), z1)
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(qs, nil) → nil
a(qs, a(a(cons, z0), z1)) → a(a(append, a(qs, a(a(filter, a(le, z0)), z1))), a(a(cons, z0), a(qs, a(a(filter, a(not, a(le, z0))), z1))))
Tuples:
A(a(append, a(a(cons, z0), z1)), z2) → c1(A(a(cons, z0), a(a(append, z1), z2)), A(cons, z0), A(a(append, z1), z2), A(append, z1))
A(a(filter, z0), a(a(cons, z1), z2)) → c3(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(le, a(s, z0)), a(s, z1)) → c6(A(a(le, z0), z1), A(le, 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(qs, a(a(cons, z0), z1)) → c13(A(a(append, a(qs, a(a(filter, a(le, z0)), z1))), a(a(cons, z0), a(qs, a(a(filter, a(not, a(le, z0))), z1)))), A(append, a(qs, a(a(filter, a(le, z0)), z1))), A(qs, a(a(filter, a(le, z0)), z1)), A(a(filter, a(le, z0)), z1), A(filter, a(le, z0)), A(le, z0), A(a(cons, z0), a(qs, a(a(filter, a(not, a(le, z0))), z1))), A(cons, z0), A(qs, a(a(filter, a(not, a(le, z0))), z1)), A(a(filter, a(not, a(le, z0))), z1), A(filter, a(not, a(le, z0))), A(not, a(le, z0)), A(le, z0))
S tuples:
A(a(append, a(a(cons, z0), z1)), z2) → c1(A(a(cons, z0), a(a(append, z1), z2)), A(cons, z0), A(a(append, z1), z2), A(append, z1))
A(a(filter, z0), a(a(cons, z1), z2)) → c3(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(le, a(s, z0)), a(s, z1)) → c6(A(a(le, z0), z1), A(le, 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(qs, a(a(cons, z0), z1)) → c13(A(a(append, a(qs, a(a(filter, a(le, z0)), z1))), a(a(cons, z0), a(qs, a(a(filter, a(not, a(le, z0))), z1)))), A(append, a(qs, a(a(filter, a(le, z0)), z1))), A(qs, a(a(filter, a(le, z0)), z1)), A(a(filter, a(le, z0)), z1), A(filter, a(le, z0)), A(le, z0), A(a(cons, z0), a(qs, a(a(filter, a(not, a(le, z0))), z1))), A(cons, z0), A(qs, a(a(filter, a(not, a(le, z0))), z1)), A(a(filter, a(not, a(le, z0))), z1), A(filter, a(not, a(le, z0))), A(not, a(le, z0)), A(le, z0))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c1, c3, 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(append, a(a(cons, z0), z1)), z2) → c1(A(a(cons, z0), a(a(append, z1), z2)), A(cons, z0), A(a(append, z1), z2), A(append, z1))
A(a(filter, z0), a(a(cons, z1), z2)) → c3(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(le, a(s, z0)), a(s, z1)) → c6(A(a(le, z0), z1), A(le, 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(qs, a(a(cons, z0), z1)) → c13(A(a(append, a(qs, a(a(filter, a(le, z0)), z1))), a(a(cons, z0), a(qs, a(a(filter, a(not, a(le, z0))), z1)))), A(append, a(qs, a(a(filter, a(le, z0)), z1))), A(qs, a(a(filter, a(le, z0)), z1)), A(a(filter, a(le, z0)), z1), A(filter, a(le, z0)), A(le, z0), A(a(cons, z0), a(qs, a(a(filter, a(not, a(le, z0))), z1))), A(cons, z0), A(qs, a(a(filter, a(not, a(le, z0))), z1)), A(a(filter, a(not, a(le, z0))), z1), A(filter, a(not, a(le, z0))), A(not, a(le, z0)), A(le, z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(a(append, nil), z0) → z0
a(a(append, a(a(cons, z0), z1)), z2) → a(a(cons, z0), a(a(append, 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(le, 0), z0) → true
a(a(le, a(s, z0)), 0) → false
a(a(le, a(s, z0)), a(s, z1)) → a(a(le, z0), z1)
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(qs, nil) → nil
a(qs, a(a(cons, z0), z1)) → a(a(append, a(qs, a(a(filter, a(le, z0)), z1))), a(a(cons, z0), a(qs, a(a(filter, a(not, a(le, 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))