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

merge(x, nil) → x
merge(nil, y) → y
merge(++(x, y), ++(u, v)) → ++(x, merge(y, ++(u, v)))
merge(++(x, y), ++(u, v)) → ++(u, merge(++(x, y), v))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

merge'(x, nil') → x
merge'(nil', y) → y
merge'(++'(x, y), ++'(u', v')) → ++'(x, merge'(y, ++'(u', v')))
merge'(++'(x, y), ++'(u', v')) → ++'(u', merge'(++'(x, y), v'))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
merge'(x, nil') → x
merge'(nil', y) → y
merge'(++'(x, y), ++'(u', v')) → ++'(x, merge'(y, ++'(u', v')))
merge'(++'(x, y), ++'(u', v')) → ++'(u', merge'(++'(x, y), v'))

Types:
merge' :: nil':++':v' → nil':++':v' → nil':++':v'
nil' :: nil':++':v'
++' :: u' → nil':++':v' → nil':++':v'
u' :: u'
v' :: nil':++':v'
_hole_nil':++':v'1 :: nil':++':v'
_hole_u'2 :: u'
_gen_nil':++':v'3 :: Nat → nil':++':v'

Heuristically decided to analyse the following defined symbols:
merge'

Generator Equations:
_gen_nil':++':v'3(0) ⇔ nil'
_gen_nil':++':v'3(+(x, 1)) ⇔ ++'(u', _gen_nil':++':v'3(x))

The following defined symbols remain to be analysed:
merge'

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

Generator Equations:
_gen_nil':++':v'3(0) ⇔ nil'
_gen_nil':++':v'3(+(x, 1)) ⇔ ++'(u', _gen_nil':++':v'3(x))

No more defined symbols left to analyse.