Runtime Complexity TRS:
The TRS R consists of the following rules:

r(xs, ys, zs, nil) → xs
r(xs, nil, zs, cons(w, ws)) → r(xs, xs, cons(succ(zero), zs), ws)
r(xs, cons(y, ys), nil, cons(w, ws)) → r(xs, xs, cons(succ(zero), nil), ws)
r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) → r(ys, cons(y, ys), zs, cons(succ(zero), cons(w, ws)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


r'(xs, ys, zs, nil') → xs
r'(xs, nil', zs, cons'(w, ws)) → r'(xs, xs, cons'(succ'(zero'), zs), ws)
r'(xs, cons'(y, ys), nil', cons'(w, ws)) → r'(xs, xs, cons'(succ'(zero'), nil'), ws)
r'(xs, cons'(y, ys), cons'(z, zs), cons'(w, ws)) → r'(ys, cons'(y, ys), zs, cons'(succ'(zero'), cons'(w, ws)))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
cons'/0
succ'/0

Runtime Complexity TRS:
The TRS R consists of the following rules:


r'(xs, ys, zs, nil') → xs
r'(xs, nil', zs, cons'(ws)) → r'(xs, xs, cons'(zs), ws)
r'(xs, cons'(ys), nil', cons'(ws)) → r'(xs, xs, cons'(nil'), ws)
r'(xs, cons'(ys), cons'(zs), cons'(ws)) → r'(ys, cons'(ys), zs, cons'(cons'(ws)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
r'(xs, ys, zs, nil') → xs
r'(xs, nil', zs, cons'(ws)) → r'(xs, xs, cons'(zs), ws)
r'(xs, cons'(ys), nil', cons'(ws)) → r'(xs, xs, cons'(nil'), ws)
r'(xs, cons'(ys), cons'(zs), cons'(ws)) → r'(ys, cons'(ys), zs, cons'(cons'(ws)))

Types:
r' :: nil':cons' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: nil':cons' → nil':cons'
_hole_nil':cons'1 :: nil':cons'
_gen_nil':cons'2 :: Nat → nil':cons'

Heuristically decided to analyse the following defined symbols:
r'

Rules:
r'(xs, ys, zs, nil') → xs
r'(xs, nil', zs, cons'(ws)) → r'(xs, xs, cons'(zs), ws)
r'(xs, cons'(ys), nil', cons'(ws)) → r'(xs, xs, cons'(nil'), ws)
r'(xs, cons'(ys), cons'(zs), cons'(ws)) → r'(ys, cons'(ys), zs, cons'(cons'(ws)))

Types:
r' :: nil':cons' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: nil':cons' → nil':cons'
_hole_nil':cons'1 :: nil':cons'
_gen_nil':cons'2 :: Nat → nil':cons'

Generator Equations:
_gen_nil':cons'2(0) ⇔ nil'
_gen_nil':cons'2(+(x, 1)) ⇔ cons'(_gen_nil':cons'2(x))

The following defined symbols remain to be analysed:
r'

Could not prove a rewrite lemma for the defined symbol r'.

The following conjecture could not be proven:

r'(_gen_nil':cons'2(0), _gen_nil':cons'2(0), _gen_nil':cons'2(c), _gen_nil':cons'2(_n4)) →? _gen_nil':cons'2(0)

Rules:
r'(xs, ys, zs, nil') → xs
r'(xs, nil', zs, cons'(ws)) → r'(xs, xs, cons'(zs), ws)
r'(xs, cons'(ys), nil', cons'(ws)) → r'(xs, xs, cons'(nil'), ws)
r'(xs, cons'(ys), cons'(zs), cons'(ws)) → r'(ys, cons'(ys), zs, cons'(cons'(ws)))

Types:
r' :: nil':cons' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: nil':cons' → nil':cons'
_hole_nil':cons'1 :: nil':cons'
_gen_nil':cons'2 :: Nat → nil':cons'

Generator Equations:
_gen_nil':cons'2(0) ⇔ nil'
_gen_nil':cons'2(+(x, 1)) ⇔ cons'(_gen_nil':cons'2(x))

No more defined symbols left to analyse.