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

revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
goal(xs, ys) → revapp(xs, ys)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

revapp'(Cons'(x, xs), rest) → revapp'(xs, Cons'(x, rest))
revapp'(Nil', rest) → rest
goal'(xs, ys) → revapp'(xs, ys)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

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

revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
revapp'(Nil', rest) → rest
goal'(xs, ys) → revapp'(xs, ys)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
revapp'(Nil', rest) → rest
goal'(xs, ys) → revapp'(xs, ys)

Types:
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
revapp'

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

The following defined symbols remain to be analysed:
revapp'

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

The following conjecture could not be proven:

revapp'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) →^? _gen_Cons':Nil'2(+(_n4, b))

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

No more defined symbols left to analyse.