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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(tt)
active(U21(tt, V2)) → mark(U22(isList(V2)))
active(U22(tt)) → mark(tt)
active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNeList(V2)))
active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isList(V2)))
active(U52(tt)) → mark(tt)
active(U61(tt)) → mark(tt)
active(U71(tt, P)) → mark(U72(isPal(P)))
active(U72(tt)) → mark(tt)
active(U81(tt)) → mark(tt)
active(isList(V)) → mark(U11(isNeList(V)))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(U21(isList(V1), V2))
active(isNeList(V)) → mark(U31(isQid(V)))
active(isNeList(__(V1, V2))) → mark(U41(isList(V1), V2))
active(isNeList(__(V1, V2))) → mark(U51(isNeList(V1), V2))
active(isNePal(V)) → mark(U61(isQid(V)))
active(isNePal(__(I, __(P, I)))) → mark(U71(isQid(I), P))
active(isPal(V)) → mark(U81(isNePal(V)))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(U11(X)) → U11(active(X))
active(U21(X1, X2)) → U21(active(X1), X2)
active(U22(X)) → U22(active(X))
active(U31(X)) → U31(active(X))
active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))
active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))
active(U61(X)) → U61(active(X))
active(U71(X1, X2)) → U71(active(X1), X2)
active(U72(X)) → U72(active(X))
active(U81(X)) → U81(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
U11(mark(X)) → mark(U11(X))
U21(mark(X1), X2) → mark(U21(X1, X2))
U22(mark(X)) → mark(U22(X))
U31(mark(X)) → mark(U31(X))
U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))
U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))
U61(mark(X)) → mark(U61(X))
U71(mark(X1), X2) → mark(U71(X1, X2))
U72(mark(X)) → mark(U72(X))
U81(mark(X)) → mark(U81(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(U11(X)) → U11(proper(X))
proper(tt) → ok(tt)
proper(U21(X1, X2)) → U21(proper(X1), proper(X2))
proper(U22(X)) → U22(proper(X))
proper(isList(X)) → isList(proper(X))
proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))
proper(U42(X)) → U42(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))
proper(U61(X)) → U61(proper(X))
proper(U71(X1, X2)) → U71(proper(X1), proper(X2))
proper(U72(X)) → U72(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(U81(X)) → U81(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
U11(ok(X)) → ok(U11(X))
U21(ok(X1), ok(X2)) → ok(U21(X1, X2))
U22(ok(X)) → ok(U22(X))
isList(ok(X)) → ok(isList(X))
U31(ok(X)) → ok(U31(X))
U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))
isNeList(ok(X)) → ok(isNeList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))
U52(ok(X)) → ok(U52(X))
U61(ok(X)) → ok(U61(X))
U71(ok(X1), ok(X2)) → ok(U71(X1, X2))
U72(ok(X)) → ok(U72(X))
isPal(ok(X)) → ok(isPal(X))
U81(ok(X)) → ok(U81(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

active'(__'(__'(X, Y), Z)) → mark'(__'(X, __'(Y, Z)))
active'(__'(X, nil')) → mark'(X)
active'(__'(nil', X)) → mark'(X)
active'(U11'(tt')) → mark'(tt')
active'(U21'(tt', V2)) → mark'(U22'(isList'(V2)))
active'(U22'(tt')) → mark'(tt')
active'(U31'(tt')) → mark'(tt')
active'(U41'(tt', V2)) → mark'(U42'(isNeList'(V2)))
active'(U42'(tt')) → mark'(tt')
active'(U51'(tt', V2)) → mark'(U52'(isList'(V2)))
active'(U52'(tt')) → mark'(tt')
active'(U61'(tt')) → mark'(tt')
active'(U71'(tt', P)) → mark'(U72'(isPal'(P)))
active'(U72'(tt')) → mark'(tt')
active'(U81'(tt')) → mark'(tt')
active'(isList'(V)) → mark'(U11'(isNeList'(V)))
active'(isList'(nil')) → mark'(tt')
active'(isList'(__'(V1, V2))) → mark'(U21'(isList'(V1), V2))
active'(isNeList'(V)) → mark'(U31'(isQid'(V)))
active'(isNeList'(__'(V1, V2))) → mark'(U41'(isList'(V1), V2))
active'(isNeList'(__'(V1, V2))) → mark'(U51'(isNeList'(V1), V2))
active'(isNePal'(V)) → mark'(U61'(isQid'(V)))
active'(isNePal'(__'(I, __'(P, I)))) → mark'(U71'(isQid'(I), P))
active'(isPal'(V)) → mark'(U81'(isNePal'(V)))
active'(isPal'(nil')) → mark'(tt')
active'(isQid'(a')) → mark'(tt')
active'(isQid'(e')) → mark'(tt')
active'(isQid'(i')) → mark'(tt')
active'(isQid'(o')) → mark'(tt')
active'(isQid'(u')) → mark'(tt')
active'(__'(X1, X2)) → __'(active'(X1), X2)
active'(__'(X1, X2)) → __'(X1, active'(X2))
active'(U11'(X)) → U11'(active'(X))
active'(U21'(X1, X2)) → U21'(active'(X1), X2)
active'(U22'(X)) → U22'(active'(X))
active'(U31'(X)) → U31'(active'(X))
active'(U41'(X1, X2)) → U41'(active'(X1), X2)
active'(U42'(X)) → U42'(active'(X))
active'(U51'(X1, X2)) → U51'(active'(X1), X2)
active'(U52'(X)) → U52'(active'(X))
active'(U61'(X)) → U61'(active'(X))
active'(U71'(X1, X2)) → U71'(active'(X1), X2)
active'(U72'(X)) → U72'(active'(X))
active'(U81'(X)) → U81'(active'(X))
__'(mark'(X1), X2) → mark'(__'(X1, X2))
__'(X1, mark'(X2)) → mark'(__'(X1, X2))
U11'(mark'(X)) → mark'(U11'(X))
U21'(mark'(X1), X2) → mark'(U21'(X1, X2))
U22'(mark'(X)) → mark'(U22'(X))
U31'(mark'(X)) → mark'(U31'(X))
U41'(mark'(X1), X2) → mark'(U41'(X1, X2))
U42'(mark'(X)) → mark'(U42'(X))
U51'(mark'(X1), X2) → mark'(U51'(X1, X2))
U52'(mark'(X)) → mark'(U52'(X))
U61'(mark'(X)) → mark'(U61'(X))
U71'(mark'(X1), X2) → mark'(U71'(X1, X2))
U72'(mark'(X)) → mark'(U72'(X))
U81'(mark'(X)) → mark'(U81'(X))
proper'(__'(X1, X2)) → __'(proper'(X1), proper'(X2))
proper'(nil') → ok'(nil')
proper'(U11'(X)) → U11'(proper'(X))
proper'(tt') → ok'(tt')
proper'(U21'(X1, X2)) → U21'(proper'(X1), proper'(X2))
proper'(U22'(X)) → U22'(proper'(X))
proper'(isList'(X)) → isList'(proper'(X))
proper'(U31'(X)) → U31'(proper'(X))
proper'(U41'(X1, X2)) → U41'(proper'(X1), proper'(X2))
proper'(U42'(X)) → U42'(proper'(X))
proper'(isNeList'(X)) → isNeList'(proper'(X))
proper'(U51'(X1, X2)) → U51'(proper'(X1), proper'(X2))
proper'(U52'(X)) → U52'(proper'(X))
proper'(U61'(X)) → U61'(proper'(X))
proper'(U71'(X1, X2)) → U71'(proper'(X1), proper'(X2))
proper'(U72'(X)) → U72'(proper'(X))
proper'(isPal'(X)) → isPal'(proper'(X))
proper'(U81'(X)) → U81'(proper'(X))
proper'(isQid'(X)) → isQid'(proper'(X))
proper'(isNePal'(X)) → isNePal'(proper'(X))
proper'(a') → ok'(a')
proper'(e') → ok'(e')
proper'(i') → ok'(i')
proper'(o') → ok'(o')
proper'(u') → ok'(u')
__'(ok'(X1), ok'(X2)) → ok'(__'(X1, X2))
U11'(ok'(X)) → ok'(U11'(X))
U21'(ok'(X1), ok'(X2)) → ok'(U21'(X1, X2))
U22'(ok'(X)) → ok'(U22'(X))
isList'(ok'(X)) → ok'(isList'(X))
U31'(ok'(X)) → ok'(U31'(X))
U41'(ok'(X1), ok'(X2)) → ok'(U41'(X1, X2))
U42'(ok'(X)) → ok'(U42'(X))
isNeList'(ok'(X)) → ok'(isNeList'(X))
U51'(ok'(X1), ok'(X2)) → ok'(U51'(X1, X2))
U52'(ok'(X)) → ok'(U52'(X))
U61'(ok'(X)) → ok'(U61'(X))
U71'(ok'(X1), ok'(X2)) → ok'(U71'(X1, X2))
U72'(ok'(X)) → ok'(U72'(X))
isPal'(ok'(X)) → ok'(isPal'(X))
U81'(ok'(X)) → ok'(U81'(X))
isQid'(ok'(X)) → ok'(isQid'(X))
isNePal'(ok'(X)) → ok'(isNePal'(X))
top'(mark'(X)) → top'(proper'(X))
top'(ok'(X)) → top'(active'(X))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
active'(__'(__'(X, Y), Z)) → mark'(__'(X, __'(Y, Z)))
active'(__'(X, nil')) → mark'(X)
active'(__'(nil', X)) → mark'(X)
active'(U11'(tt')) → mark'(tt')
active'(U21'(tt', V2)) → mark'(U22'(isList'(V2)))
active'(U22'(tt')) → mark'(tt')
active'(U31'(tt')) → mark'(tt')
active'(U41'(tt', V2)) → mark'(U42'(isNeList'(V2)))
active'(U42'(tt')) → mark'(tt')
active'(U51'(tt', V2)) → mark'(U52'(isList'(V2)))
active'(U52'(tt')) → mark'(tt')
active'(U61'(tt')) → mark'(tt')
active'(U71'(tt', P)) → mark'(U72'(isPal'(P)))
active'(U72'(tt')) → mark'(tt')
active'(U81'(tt')) → mark'(tt')
active'(isList'(V)) → mark'(U11'(isNeList'(V)))
active'(isList'(nil')) → mark'(tt')
active'(isList'(__'(V1, V2))) → mark'(U21'(isList'(V1), V2))
active'(isNeList'(V)) → mark'(U31'(isQid'(V)))
active'(isNeList'(__'(V1, V2))) → mark'(U41'(isList'(V1), V2))
active'(isNeList'(__'(V1, V2))) → mark'(U51'(isNeList'(V1), V2))
active'(isNePal'(V)) → mark'(U61'(isQid'(V)))
active'(isNePal'(__'(I, __'(P, I)))) → mark'(U71'(isQid'(I), P))
active'(isPal'(V)) → mark'(U81'(isNePal'(V)))
active'(isPal'(nil')) → mark'(tt')
active'(isQid'(a')) → mark'(tt')
active'(isQid'(e')) → mark'(tt')
active'(isQid'(i')) → mark'(tt')
active'(isQid'(o')) → mark'(tt')
active'(isQid'(u')) → mark'(tt')
active'(__'(X1, X2)) → __'(active'(X1), X2)
active'(__'(X1, X2)) → __'(X1, active'(X2))
active'(U11'(X)) → U11'(active'(X))
active'(U21'(X1, X2)) → U21'(active'(X1), X2)
active'(U22'(X)) → U22'(active'(X))
active'(U31'(X)) → U31'(active'(X))
active'(U41'(X1, X2)) → U41'(active'(X1), X2)
active'(U42'(X)) → U42'(active'(X))
active'(U51'(X1, X2)) → U51'(active'(X1), X2)
active'(U52'(X)) → U52'(active'(X))
active'(U61'(X)) → U61'(active'(X))
active'(U71'(X1, X2)) → U71'(active'(X1), X2)
active'(U72'(X)) → U72'(active'(X))
active'(U81'(X)) → U81'(active'(X))
__'(mark'(X1), X2) → mark'(__'(X1, X2))
__'(X1, mark'(X2)) → mark'(__'(X1, X2))
U11'(mark'(X)) → mark'(U11'(X))
U21'(mark'(X1), X2) → mark'(U21'(X1, X2))
U22'(mark'(X)) → mark'(U22'(X))
U31'(mark'(X)) → mark'(U31'(X))
U41'(mark'(X1), X2) → mark'(U41'(X1, X2))
U42'(mark'(X)) → mark'(U42'(X))
U51'(mark'(X1), X2) → mark'(U51'(X1, X2))
U52'(mark'(X)) → mark'(U52'(X))
U61'(mark'(X)) → mark'(U61'(X))
U71'(mark'(X1), X2) → mark'(U71'(X1, X2))
U72'(mark'(X)) → mark'(U72'(X))
U81'(mark'(X)) → mark'(U81'(X))
proper'(__'(X1, X2)) → __'(proper'(X1), proper'(X2))
proper'(nil') → ok'(nil')
proper'(U11'(X)) → U11'(proper'(X))
proper'(tt') → ok'(tt')
proper'(U21'(X1, X2)) → U21'(proper'(X1), proper'(X2))
proper'(U22'(X)) → U22'(proper'(X))
proper'(isList'(X)) → isList'(proper'(X))
proper'(U31'(X)) → U31'(proper'(X))
proper'(U41'(X1, X2)) → U41'(proper'(X1), proper'(X2))
proper'(U42'(X)) → U42'(proper'(X))
proper'(isNeList'(X)) → isNeList'(proper'(X))
proper'(U51'(X1, X2)) → U51'(proper'(X1), proper'(X2))
proper'(U52'(X)) → U52'(proper'(X))
proper'(U61'(X)) → U61'(proper'(X))
proper'(U71'(X1, X2)) → U71'(proper'(X1), proper'(X2))
proper'(U72'(X)) → U72'(proper'(X))
proper'(isPal'(X)) → isPal'(proper'(X))
proper'(U81'(X)) → U81'(proper'(X))
proper'(isQid'(X)) → isQid'(proper'(X))
proper'(isNePal'(X)) → isNePal'(proper'(X))
proper'(a') → ok'(a')
proper'(e') → ok'(e')
proper'(i') → ok'(i')
proper'(o') → ok'(o')
proper'(u') → ok'(u')
__'(ok'(X1), ok'(X2)) → ok'(__'(X1, X2))
U11'(ok'(X)) → ok'(U11'(X))
U21'(ok'(X1), ok'(X2)) → ok'(U21'(X1, X2))
U22'(ok'(X)) → ok'(U22'(X))
isList'(ok'(X)) → ok'(isList'(X))
U31'(ok'(X)) → ok'(U31'(X))
U41'(ok'(X1), ok'(X2)) → ok'(U41'(X1, X2))
U42'(ok'(X)) → ok'(U42'(X))
isNeList'(ok'(X)) → ok'(isNeList'(X))
U51'(ok'(X1), ok'(X2)) → ok'(U51'(X1, X2))
U52'(ok'(X)) → ok'(U52'(X))
U61'(ok'(X)) → ok'(U61'(X))
U71'(ok'(X1), ok'(X2)) → ok'(U71'(X1, X2))
U72'(ok'(X)) → ok'(U72'(X))
isPal'(ok'(X)) → ok'(isPal'(X))
U81'(ok'(X)) → ok'(U81'(X))
isQid'(ok'(X)) → ok'(isQid'(X))
isNePal'(ok'(X)) → ok'(isNePal'(X))
top'(mark'(X)) → top'(proper'(X))
top'(ok'(X)) → top'(active'(X))

Types:
active' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
__' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
mark' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
nil' :: mark':nil':tt':a':e':i':o':u':ok'
U11' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
tt' :: mark':nil':tt':a':e':i':o':u':ok'
U21' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U22' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
isList' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U31' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U41' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U42' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
isNeList' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U51' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U52' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U61' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U71' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U72' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
isPal' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U81' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
isQid' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
isNePal' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
a' :: mark':nil':tt':a':e':i':o':u':ok'
e' :: mark':nil':tt':a':e':i':o':u':ok'
i' :: mark':nil':tt':a':e':i':o':u':ok'
o' :: mark':nil':tt':a':e':i':o':u':ok'
u' :: mark':nil':tt':a':e':i':o':u':ok'
proper' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
ok' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
top' :: mark':nil':tt':a':e':i':o':u':ok' → top'
___hole_mark':nil':tt':a':e':i':o':u':ok'1 :: mark':nil':tt':a':e':i':o':u':ok'
___hole_top'2 :: top'
___gen_mark':nil':tt':a':e':i':o':u':ok'3 :: Nat → mark':nil':tt':a':e':i':o':u':ok'

Heuristically decided to analyse the following defined symbols:
active', __', U22', isList', U42', isNeList', U52', U72', isPal', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
__' < active'
U22' < active'
isList' < active'
U42' < active'
isNeList' < active'
U52' < active'
U72' < active'
isPal' < active'
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
__' < proper'
U22' < proper'
isList' < proper'
U42' < proper'
isNeList' < proper'
U52' < proper'
U72' < proper'
isPal' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
__', active', U22', isList', U42', isNeList', U52', U72', isPal', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

Proved the following rewrite lemma:
__'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n5)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n5})

Induction Base:
__'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b))

Induction Step:
__'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n6, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b826)) →_R^Ω(1)
mark'(__'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n6)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b826))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
__'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n5)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n5})

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U22', active', isList', U42', isNeList', U52', U72', isPal', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U22' < active'
isList' < active'
U42' < active'
isNeList' < active'
U52' < active'
U72' < active'
isPal' < active'
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U22' < proper'
isList' < proper'
U42' < proper'
isNeList' < proper'
U52' < proper'
U72' < proper'
isPal' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n4361))) → ___*4, rt ∈ Ω(_{__n4361})

Induction Base:
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)))

Induction Step:
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n4362, 1)))) →_R^Ω(1)
mark'(U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n4362)))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
isList', active', U42', isNeList', U52', U72', isPal', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
isList' < active'
U42' < active'
isNeList' < active'
U52' < active'
U72' < active'
isPal' < active'
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
isList' < proper'
U42' < proper'
isNeList' < proper'
U52' < proper'
U72' < proper'
isPal' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

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

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U42', active', isNeList', U52', U72', isPal', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U42' < active'
isNeList' < active'
U52' < active'
U72' < active'
isPal' < active'
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U42' < proper'
isNeList' < proper'
U52' < proper'
U72' < proper'
isPal' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n7135))) → ___*4, rt ∈ Ω(_{__n7135})

Induction Base:
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)))

Induction Step:
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n7136, 1)))) →_R^Ω(1)
mark'(U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n7136)))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
isNeList', active', U52', U72', isPal', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
isNeList' < active'
U52' < active'
U72' < active'
isPal' < active'
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
isNeList' < proper'
U52' < proper'
U72' < proper'
isPal' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

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

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U52', active', U72', isPal', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U52' < active'
U72' < active'
isPal' < active'
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U52' < proper'
U72' < proper'
isPal' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n10039))) → ___*4, rt ∈ Ω(_{__n10039})

Induction Base:
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)))

Induction Step:
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n10040, 1)))) →_R^Ω(1)
mark'(U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n10040)))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U72', active', isPal', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U72' < active'
isPal' < active'
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U72' < proper'
isPal' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n13039))) → ___*4, rt ∈ Ω(_{__n13039})

Induction Base:
U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)))

Induction Step:
U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n13040, 1)))) →_R^Ω(1)
mark'(U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n13040)))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
isPal', active', U11', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
isPal' < active'
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
isPal' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

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

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U11', active', U21', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U11' < active'
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U11' < proper'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n16203))) → ___*4, rt ∈ Ω(_{__n16203})

Induction Base:
U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)))

Induction Step:
U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n16204, 1)))) →_R^Ω(1)
mark'(U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n16204)))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U21', active', U31', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U21' < active'
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U21' < proper'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n19451)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n19451})

Induction Base:
U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b))

Induction Step:
U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n19452, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b21460)) →_R^Ω(1)
mark'(U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n19452)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b21460))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U31', active', isQid', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U31' < active'
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U31' < proper'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n25161))) → ___*4, rt ∈ Ω(_{__n25161})

Induction Base:
U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)))

Induction Step:
U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n25162, 1)))) →_R^Ω(1)
mark'(U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n25162)))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
isQid', active', U41', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
isQid' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
isQid' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

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

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U41', active', U51', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n28786)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n28786})

Induction Base:
U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b))

Induction Step:
U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n28787, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b31335)) →_R^Ω(1)
mark'(U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n28787)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b31335))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U51', active', U61', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U51' < active'
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U51'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n35105)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n35105})

Induction Base:
U51'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b))

Induction Step:
U51'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n35106, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b37978)) →_R^Ω(1)
mark'(U51'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n35106)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b37978))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
__'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n5)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n5})
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n4361))) → ___*4, rt ∈ Ω(_{__n4361})
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n7135))) → ___*4, rt ∈ Ω(_{__n7135})
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n10039))) → ___*4, rt ∈ Ω(_{__n10039})
U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n13039))) → ___*4, rt ∈ Ω(_{__n13039})
U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n16203))) → ___*4, rt ∈ Ω(_{__n16203})
U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n19451)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n19451})
U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n25161))) → ___*4, rt ∈ Ω(_{__n25161})
U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n28786)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n28786})
U51'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n35105)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n35105})

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U61', active', U71', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U61' < active'
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U61' < proper'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U61'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n41792))) → ___*4, rt ∈ Ω(_{__n41792})

Induction Base:
U61'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)))

Induction Step:
U61'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n41793, 1)))) →_R^Ω(1)
mark'(U61'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n41793)))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U71', active', U81', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U71' < active'
U81' < active'
isNePal' < active'
active' < top'
U71' < proper'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U71'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n45861)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n45861})

Induction Base:
U71'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b))

Induction Step:
U71'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n45862, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b49274)) →_R^Ω(1)
mark'(U71'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n45862)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b49274))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
U81', active', isNePal', proper', top'

They will be analysed ascendingly in the following order:
U81' < active'
isNePal' < active'
active' < top'
U81' < proper'
isNePal' < proper'
proper' < top'

Proved the following rewrite lemma:
U81'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n53157))) → ___*4, rt ∈ Ω(_{__n53157})

Induction Base:
U81'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, 0)))

Induction Step:
U81'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n53158, 1)))) →_R^Ω(1)
mark'(U81'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n53158)))) →_IH
mark'(___*4)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
isNePal', active', proper', top'

They will be analysed ascendingly in the following order:
isNePal' < active'
active' < top'
isNePal' < proper'
proper' < top'

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

Generator Equations:
___gen_mark':nil':tt':a':e':i':o':u':ok'3(0) ⇔ nil'
___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(x, 1)) ⇔ mark'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(x))

The following defined symbols remain to be analysed:
active', proper', top'

They will be analysed ascendingly in the following order:
active' < top'
proper' < top'