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

add0(x', Cons(x, xs)) → add0(Cons(Cons(Nil, Nil), x'), xs)
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
add0(x, Nil) → x
goal(x, y) → add0(x, y)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

add0'(x', Cons'(x, xs)) → add0'(Cons'(Cons'(Nil', Nil'), x'), xs)
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
add0'(x, Nil') → x
goal'(x, y) → add0'(x, y)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

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

add0'(x', Cons'(xs)) → add0'(Cons'(x'), xs)
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
add0'(x, Nil') → x
goal'(x, y) → add0'(x, y)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
add0'(x', Cons'(xs)) → add0'(Cons'(x'), xs)
notEmpty'(Cons'(xs)) → True'
notEmpty'(Nil') → False'
add0'(x, Nil') → x
goal'(x, y) → add0'(x, y)

Types:
add0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
Nil' :: Cons':Nil'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_True':False'2 :: True':False'
_gen_Cons':Nil'3 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
add0'

Generator Equations:
_gen_Cons':Nil'3(0) ⇔ Nil'
_gen_Cons':Nil'3(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'3(x))

The following defined symbols remain to be analysed:
add0'

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

The following conjecture could not be proven:

add0'(_gen_Cons':Nil'3(a), _gen_Cons':Nil'3(_n5)) →^? _gen_Cons':Nil'3(+(_n5, a))

Generator Equations:
_gen_Cons':Nil'3(0) ⇔ Nil'
_gen_Cons':Nil'3(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'3(x))

No more defined symbols left to analyse.