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

revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r))
deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest))
deeprevapp(V(n), rest) → revconsapp(rest, V(n))
deeprevapp(N, rest) → rest
revconsapp(V(n), r) → r
revconsapp(N, r) → r
deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N)
deeprev(V(n)) → V(n)
deeprev(N) → N
second(V(n)) → N
second(C(x1, x2)) → x2
isVal(C(x1, x2)) → False
isVal(V(n)) → True
isVal(N) → False
isNotEmptyT(C(x1, x2)) → True
isNotEmptyT(V(n)) → False
isNotEmptyT(N) → False
isEmptyT(C(x1, x2)) → False
isEmptyT(V(n)) → False
isEmptyT(N) → True
first(V(n)) → N
first(C(x1, x2)) → x1
goal(x) → deeprev(x)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

revconsapp'(C'(x1, x2), r) → revconsapp'(x2, C'(x1, r))
deeprevapp'(C'(x1, x2), rest) → deeprevapp'(x2, C'(x1, rest))
deeprevapp'(V'(n), rest) → revconsapp'(rest, V'(n))
deeprevapp'(N', rest) → rest
revconsapp'(V'(n), r) → r
revconsapp'(N', r) → r
deeprev'(C'(x1, x2)) → deeprevapp'(C'(x1, x2), N')
deeprev'(V'(n)) → V'(n)
deeprev'(N') → N'
second'(V'(n)) → N'
second'(C'(x1, x2)) → x2
isVal'(C'(x1, x2)) → False'
isVal'(V'(n)) → True'
isVal'(N') → False'
isNotEmptyT'(C'(x1, x2)) → True'
isNotEmptyT'(V'(n)) → False'
isNotEmptyT'(N') → False'
isEmptyT'(C'(x1, x2)) → False'
isEmptyT'(V'(n)) → False'
isEmptyT'(N') → True'
first'(V'(n)) → N'
first'(C'(x1, x2)) → x1
goal'(x) → deeprev'(x)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
V'/0

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

revconsapp'(C'(x1, x2), r) → revconsapp'(x2, C'(x1, r))
deeprevapp'(C'(x1, x2), rest) → deeprevapp'(x2, C'(x1, rest))
deeprevapp'(V', rest) → revconsapp'(rest, V')
deeprevapp'(N', rest) → rest
revconsapp'(V', r) → r
revconsapp'(N', r) → r
deeprev'(C'(x1, x2)) → deeprevapp'(C'(x1, x2), N')
deeprev'(V') → V'
deeprev'(N') → N'
second'(V') → N'
second'(C'(x1, x2)) → x2
isVal'(C'(x1, x2)) → False'
isVal'(V') → True'
isVal'(N') → False'
isNotEmptyT'(C'(x1, x2)) → True'
isNotEmptyT'(V') → False'
isNotEmptyT'(N') → False'
isEmptyT'(C'(x1, x2)) → False'
isEmptyT'(V') → False'
isEmptyT'(N') → True'
first'(V') → N'
first'(C'(x1, x2)) → x1
goal'(x) → deeprev'(x)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
revconsapp'(C'(x1, x2), r) → revconsapp'(x2, C'(x1, r))
deeprevapp'(C'(x1, x2), rest) → deeprevapp'(x2, C'(x1, rest))
deeprevapp'(V', rest) → revconsapp'(rest, V')
deeprevapp'(N', rest) → rest
revconsapp'(V', r) → r
revconsapp'(N', r) → r
deeprev'(C'(x1, x2)) → deeprevapp'(C'(x1, x2), N')
deeprev'(V') → V'
deeprev'(N') → N'
second'(V') → N'
second'(C'(x1, x2)) → x2
isVal'(C'(x1, x2)) → False'
isVal'(V') → True'
isVal'(N') → False'
isNotEmptyT'(C'(x1, x2)) → True'
isNotEmptyT'(V') → False'
isNotEmptyT'(N') → False'
isEmptyT'(C'(x1, x2)) → False'
isEmptyT'(V') → False'
isEmptyT'(N') → True'
first'(V') → N'
first'(C'(x1, x2)) → x1
goal'(x) → deeprev'(x)

Types:
revconsapp' :: C':V':N' → C':V':N' → C':V':N'
C' :: C':V':N' → C':V':N' → C':V':N'
deeprevapp' :: C':V':N' → C':V':N' → C':V':N'
V' :: C':V':N'
N' :: C':V':N'
deeprev' :: C':V':N' → C':V':N'
second' :: C':V':N' → C':V':N'
isVal' :: C':V':N' → False':True'
False' :: False':True'
True' :: False':True'
isNotEmptyT' :: C':V':N' → False':True'
isEmptyT' :: C':V':N' → False':True'
first' :: C':V':N' → C':V':N'
goal' :: C':V':N' → C':V':N'
_hole_C':V':N'1 :: C':V':N'
_hole_False':True'2 :: False':True'
_gen_C':V':N'3 :: Nat → C':V':N'

Heuristically decided to analyse the following defined symbols:
revconsapp', deeprevapp'

They will be analysed ascendingly in the following order:
revconsapp' < deeprevapp'

Generator Equations:
_gen_C':V':N'3(0) ⇔ V'
_gen_C':V':N'3(+(x, 1)) ⇔ C'(V', _gen_C':V':N'3(x))

The following defined symbols remain to be analysed:
revconsapp', deeprevapp'

They will be analysed ascendingly in the following order:
revconsapp' < deeprevapp'

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

The following conjecture could not be proven:

revconsapp'(_gen_C':V':N'3(_n5), _gen_C':V':N'3(b)) →^? _gen_C':V':N'3(+(_n5, b))

Generator Equations:
_gen_C':V':N'3(0) ⇔ V'
_gen_C':V':N'3(+(x, 1)) ⇔ C'(V', _gen_C':V':N'3(x))

The following defined symbols remain to be analysed:
deeprevapp'

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

The following conjecture could not be proven:

deeprevapp'(_gen_C':V':N'3(+(1, _n2212)), _gen_C':V':N'3(b)) →^? _*4

Generator Equations:
_gen_C':V':N'3(0) ⇔ V'
_gen_C':V':N'3(+(x, 1)) ⇔ C'(V', _gen_C':V':N'3(x))

No more defined symbols left to analyse.