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

Sliced the following arguments:
Cons'/0

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

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

Rewrite Strategy: INNERMOST

Infered types.

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

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:

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

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'

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:

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

The following conjecture could not be proven:

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

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'

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.