(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(div, 0), app(s, y)) → 0
app(app(div, app(s, x)), app(s, y)) → app(s, app(app(div, app(app(minus, x), app(id, y))), app(s, y)))
app(id, x) → x
app(id, x) → app(s, app(s, app(s, x)))
app(id, app(p, x)) → app(id, app(s, app(id, x)))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(app(map, z0), nil) → nil
app(app(map, z0), app(app(cons, z1), z2)) → app(app(cons, app(z0, z1)), app(app(map, z0), z2))
app(app(minus, z0), 0) → z0
app(app(minus, app(s, z0)), app(s, z1)) → app(app(minus, app(p, app(s, z0))), app(p, app(s, z1)))
app(p, app(s, z0)) → z0
app(app(div, 0), app(s, z0)) → 0
app(app(div, app(s, z0)), app(s, z1)) → app(s, app(app(div, app(app(minus, z0), app(id, z1))), app(s, z1)))
app(id, z0) → z0
app(id, z0) → app(s, app(s, app(s, z0)))
app(id, app(p, z0)) → app(id, app(s, app(id, z0)))
Tuples:
APP(app(map, z0), app(app(cons, z1), z2)) → c1(APP(app(cons, app(z0, z1)), app(app(map, z0), z2)), APP(cons, app(z0, z1)), APP(z0, z1), APP(app(map, z0), z2), APP(map, z0))
APP(app(minus, app(s, z0)), app(s, z1)) → c3(APP(app(minus, app(p, app(s, z0))), app(p, app(s, z1))), APP(minus, app(p, app(s, z0))), APP(p, app(s, z0)), APP(s, z0), APP(p, app(s, z1)), APP(s, z1))
APP(app(div, app(s, z0)), app(s, z1)) → c6(APP(s, app(app(div, app(app(minus, z0), app(id, z1))), app(s, z1))), APP(app(div, app(app(minus, z0), app(id, z1))), app(s, z1)), APP(div, app(app(minus, z0), app(id, z1))), APP(app(minus, z0), app(id, z1)), APP(minus, z0), APP(id, z1), APP(s, z1))
APP(id, z0) → c8(APP(s, app(s, app(s, z0))), APP(s, app(s, z0)), APP(s, z0))
APP(id, app(p, z0)) → c9(APP(id, app(s, app(id, z0))), APP(s, app(id, z0)), APP(id, z0))
S tuples:
APP(app(map, z0), app(app(cons, z1), z2)) → c1(APP(app(cons, app(z0, z1)), app(app(map, z0), z2)), APP(cons, app(z0, z1)), APP(z0, z1), APP(app(map, z0), z2), APP(map, z0))
APP(app(minus, app(s, z0)), app(s, z1)) → c3(APP(app(minus, app(p, app(s, z0))), app(p, app(s, z1))), APP(minus, app(p, app(s, z0))), APP(p, app(s, z0)), APP(s, z0), APP(p, app(s, z1)), APP(s, z1))
APP(app(div, app(s, z0)), app(s, z1)) → c6(APP(s, app(app(div, app(app(minus, z0), app(id, z1))), app(s, z1))), APP(app(div, app(app(minus, z0), app(id, z1))), app(s, z1)), APP(div, app(app(minus, z0), app(id, z1))), APP(app(minus, z0), app(id, z1)), APP(minus, z0), APP(id, z1), APP(s, z1))
APP(id, z0) → c8(APP(s, app(s, app(s, z0))), APP(s, app(s, z0)), APP(s, z0))
APP(id, app(p, z0)) → c9(APP(id, app(s, app(id, z0))), APP(s, app(id, z0)), APP(id, z0))
K tuples:none
Defined Rule Symbols:
app
Defined Pair Symbols:
APP
Compound Symbols:
c1, c3, c6, c8, c9
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
APP(app(map, z0), app(app(cons, z1), z2)) → c1(APP(app(cons, app(z0, z1)), app(app(map, z0), z2)), APP(cons, app(z0, z1)), APP(z0, z1), APP(app(map, z0), z2), APP(map, z0))
APP(app(minus, app(s, z0)), app(s, z1)) → c3(APP(app(minus, app(p, app(s, z0))), app(p, app(s, z1))), APP(minus, app(p, app(s, z0))), APP(p, app(s, z0)), APP(s, z0), APP(p, app(s, z1)), APP(s, z1))
APP(app(div, app(s, z0)), app(s, z1)) → c6(APP(s, app(app(div, app(app(minus, z0), app(id, z1))), app(s, z1))), APP(app(div, app(app(minus, z0), app(id, z1))), app(s, z1)), APP(div, app(app(minus, z0), app(id, z1))), APP(app(minus, z0), app(id, z1)), APP(minus, z0), APP(id, z1), APP(s, z1))
APP(id, app(p, z0)) → c9(APP(id, app(s, app(id, z0))), APP(s, app(id, z0)), APP(id, z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(app(map, z0), nil) → nil
app(app(map, z0), app(app(cons, z1), z2)) → app(app(cons, app(z0, z1)), app(app(map, z0), z2))
app(app(minus, z0), 0) → z0
app(app(minus, app(s, z0)), app(s, z1)) → app(app(minus, app(p, app(s, z0))), app(p, app(s, z1)))
app(p, app(s, z0)) → z0
app(app(div, 0), app(s, z0)) → 0
app(app(div, app(s, z0)), app(s, z1)) → app(s, app(app(div, app(app(minus, z0), app(id, z1))), app(s, z1)))
app(id, z0) → z0
app(id, z0) → app(s, app(s, app(s, z0)))
app(id, app(p, z0)) → app(id, app(s, app(id, z0)))
Tuples:
APP(id, z0) → c8(APP(s, app(s, app(s, z0))), APP(s, app(s, z0)), APP(s, z0))
S tuples:
APP(id, z0) → c8(APP(s, app(s, app(s, z0))), APP(s, app(s, z0)), APP(s, z0))
K tuples:none
Defined Rule Symbols:
app
Defined Pair Symbols:
APP
Compound Symbols:
c8
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
APP(id, z0) → c8(APP(s, app(s, app(s, z0))), APP(s, app(s, z0)), APP(s, z0))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
app(app(map, z0), nil) → nil
app(app(map, z0), app(app(cons, z1), z2)) → app(app(cons, app(z0, z1)), app(app(map, z0), z2))
app(app(minus, z0), 0) → z0
app(app(minus, app(s, z0)), app(s, z1)) → app(app(minus, app(p, app(s, z0))), app(p, app(s, z1)))
app(p, app(s, z0)) → z0
app(app(div, 0), app(s, z0)) → 0
app(app(div, app(s, z0)), app(s, z1)) → app(s, app(app(div, app(app(minus, z0), app(id, z1))), app(s, z1)))
app(id, z0) → z0
app(id, z0) → app(s, app(s, app(s, z0)))
app(id, app(p, z0)) → app(id, app(s, app(id, z0)))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
app
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))