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

notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

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

Rewrite Strategy: INNERMOST

Infered types.

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

Types:
addlist' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_0':S'2 :: 0':S'
_hole_True':False'3 :: True':False'
_gen_Cons':Nil'4 :: Nat → Cons':Nil'
_gen_0':S'5 :: Nat → 0':S'

Heuristically decided to analyse the following defined symbols:

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

Types:
addlist' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_0':S'2 :: 0':S'
_hole_True':False'3 :: True':False'
_gen_Cons':Nil'4 :: Nat → Cons':Nil'
_gen_0':S'5 :: Nat → 0':S'

Generator Equations:
_gen_Cons':Nil'4(0) ⇔ Nil'
_gen_Cons':Nil'4(+(x, 1)) ⇔ Cons'(0', _gen_Cons':Nil'4(x))
_gen_0':S'5(0) ⇔ 0'
_gen_0':S'5(+(x, 1)) ⇔ S'(_gen_0':S'5(x))

The following defined symbols remain to be analysed:

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

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

Types:
addlist' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_0':S'2 :: 0':S'
_hole_True':False'3 :: True':False'
_gen_Cons':Nil'4 :: Nat → Cons':Nil'
_gen_0':S'5 :: Nat → 0':S'

Generator Equations:
_gen_Cons':Nil'4(0) ⇔ Nil'
_gen_Cons':Nil'4(+(x, 1)) ⇔ Cons'(0', _gen_Cons':Nil'4(x))
_gen_0':S'5(0) ⇔ 0'
_gen_0':S'5(+(x, 1)) ⇔ S'(_gen_0':S'5(x))

No more defined symbols left to analyse.