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, V)) → mark(U12(isNeList(V)))
active(U12(tt)) → mark(tt)
active(U21(tt, V1, V2)) → mark(U22(isList(V1), V2))
active(U22(tt, V2)) → mark(U23(isList(V2)))
active(U23(tt)) → mark(tt)
active(U31(tt, V)) → mark(U32(isQid(V)))
active(U32(tt)) → mark(tt)
active(U41(tt, V1, V2)) → mark(U42(isList(V1), V2))
active(U42(tt, V2)) → mark(U43(isNeList(V2)))
active(U43(tt)) → mark(tt)
active(U51(tt, V1, V2)) → mark(U52(isNeList(V1), V2))
active(U52(tt, V2)) → mark(U53(isList(V2)))
active(U53(tt)) → mark(tt)
active(U61(tt, V)) → mark(U62(isQid(V)))
active(U62(tt)) → mark(tt)
active(U71(tt, V)) → mark(U72(isNePal(V)))
active(U72(tt)) → mark(tt)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(U11(isPalListKind(V), V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNeList(V)) → mark(U31(isPalListKind(V), V))
active(isNeList(__(V1, V2))) → mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNeList(__(V1, V2))) → mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNePal(V)) → mark(U61(isPalListKind(V), V))
active(isNePal(__(I, __(P, I)))) → mark(and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))))
active(isPal(V)) → mark(U71(isPalListKind(V), V))
active(isPal(nil)) → mark(tt)
active(isPalListKind(a)) → mark(tt)
active(isPalListKind(e)) → mark(tt)
active(isPalListKind(i)) → mark(tt)
active(isPalListKind(nil)) → mark(tt)
active(isPalListKind(o)) → mark(tt)
active(isPalListKind(u)) → mark(tt)
active(isPalListKind(__(V1, V2))) → mark(and(isPalListKind(V1), isPalListKind(V2)))
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(X1, X2)) → U11(active(X1), X2)
active(U12(X)) → U12(active(X))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2)) → U22(active(X1), X2)
active(U23(X)) → U23(active(X))
active(U31(X1, X2)) → U31(active(X1), X2)
active(U32(X)) → U32(active(X))
active(U41(X1, X2, X3)) → U41(active(X1), X2, X3)
active(U42(X1, X2)) → U42(active(X1), X2)
active(U43(X)) → U43(active(X))
active(U51(X1, X2, X3)) → U51(active(X1), X2, X3)
active(U52(X1, X2)) → U52(active(X1), X2)
active(U53(X)) → U53(active(X))
active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))
active(U71(X1, X2)) → U71(active(X1), X2)
active(U72(X)) → U72(active(X))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
U12(mark(X)) → mark(U12(X))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2) → mark(U22(X1, X2))
U23(mark(X)) → mark(U23(X))
U31(mark(X1), X2) → mark(U31(X1, X2))
U32(mark(X)) → mark(U32(X))
U41(mark(X1), X2, X3) → mark(U41(X1, X2, X3))
U42(mark(X1), X2) → mark(U42(X1, X2))
U43(mark(X)) → mark(U43(X))
U51(mark(X1), X2, X3) → mark(U51(X1, X2, X3))
U52(mark(X1), X2) → mark(U52(X1, X2))
U53(mark(X)) → mark(U53(X))
U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))
U71(mark(X1), X2) → mark(U71(X1, X2))
U72(mark(X)) → mark(U72(X))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(U12(X)) → U12(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2)) → U22(proper(X1), proper(X2))
proper(isList(X)) → isList(proper(X))
proper(U23(X)) → U23(proper(X))
proper(U31(X1, X2)) → U31(proper(X1), proper(X2))
proper(U32(X)) → U32(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(U41(X1, X2, X3)) → U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2)) → U42(proper(X1), proper(X2))
proper(U43(X)) → U43(proper(X))
proper(U51(X1, X2, X3)) → U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2)) → U52(proper(X1), proper(X2))
proper(U53(X)) → U53(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))
proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2)) → U71(proper(X1), proper(X2))
proper(U72(X)) → U72(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isPalListKind(X)) → isPalListKind(proper(X))
proper(isPal(X)) → isPal(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(X1), ok(X2)) → ok(U11(X1, X2))
U12(ok(X)) → ok(U12(X))
isNeList(ok(X)) → ok(isNeList(X))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2)) → ok(U22(X1, X2))
isList(ok(X)) → ok(isList(X))
U23(ok(X)) → ok(U23(X))
U31(ok(X1), ok(X2)) → ok(U31(X1, X2))
U32(ok(X)) → ok(U32(X))
isQid(ok(X)) → ok(isQid(X))
U41(ok(X1), ok(X2), ok(X3)) → ok(U41(X1, X2, X3))
U42(ok(X1), ok(X2)) → ok(U42(X1, X2))
U43(ok(X)) → ok(U43(X))
U51(ok(X1), ok(X2), ok(X3)) → ok(U51(X1, X2, X3))
U52(ok(X1), ok(X2)) → ok(U52(X1, X2))
U53(ok(X)) → ok(U53(X))
U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))
U71(ok(X1), ok(X2)) → ok(U71(X1, X2))
U72(ok(X)) → ok(U72(X))
isNePal(ok(X)) → ok(isNePal(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isPalListKind(ok(X)) → ok(isPalListKind(X))
isPal(ok(X)) → ok(isPal(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', V)) → mark'(U12'(isNeList'(V)))
active'(U12'(tt')) → mark'(tt')
active'(U21'(tt', V1, V2)) → mark'(U22'(isList'(V1), V2))
active'(U22'(tt', V2)) → mark'(U23'(isList'(V2)))
active'(U23'(tt')) → mark'(tt')
active'(U31'(tt', V)) → mark'(U32'(isQid'(V)))
active'(U32'(tt')) → mark'(tt')
active'(U41'(tt', V1, V2)) → mark'(U42'(isList'(V1), V2))
active'(U42'(tt', V2)) → mark'(U43'(isNeList'(V2)))
active'(U43'(tt')) → mark'(tt')
active'(U51'(tt', V1, V2)) → mark'(U52'(isNeList'(V1), V2))
active'(U52'(tt', V2)) → mark'(U53'(isList'(V2)))
active'(U53'(tt')) → mark'(tt')
active'(U61'(tt', V)) → mark'(U62'(isQid'(V)))
active'(U62'(tt')) → mark'(tt')
active'(U71'(tt', V)) → mark'(U72'(isNePal'(V)))
active'(U72'(tt')) → mark'(tt')
active'(and'(tt', X)) → mark'(X)
active'(isList'(V)) → mark'(U11'(isPalListKind'(V), V))
active'(isList'(nil')) → mark'(tt')
active'(isList'(__'(V1, V2))) → mark'(U21'(and'(isPalListKind'(V1), isPalListKind'(V2)), V1, V2))
active'(isNeList'(V)) → mark'(U31'(isPalListKind'(V), V))
active'(isNeList'(__'(V1, V2))) → mark'(U41'(and'(isPalListKind'(V1), isPalListKind'(V2)), V1, V2))
active'(isNeList'(__'(V1, V2))) → mark'(U51'(and'(isPalListKind'(V1), isPalListKind'(V2)), V1, V2))
active'(isNePal'(V)) → mark'(U61'(isPalListKind'(V), V))
active'(isNePal'(__'(I, __'(P, I)))) → mark'(and'(and'(isQid'(I), isPalListKind'(I)), and'(isPal'(P), isPalListKind'(P))))
active'(isPal'(V)) → mark'(U71'(isPalListKind'(V), V))
active'(isPal'(nil')) → mark'(tt')
active'(isPalListKind'(a')) → mark'(tt')
active'(isPalListKind'(e')) → mark'(tt')
active'(isPalListKind'(i')) → mark'(tt')
active'(isPalListKind'(nil')) → mark'(tt')
active'(isPalListKind'(o')) → mark'(tt')
active'(isPalListKind'(u')) → mark'(tt')
active'(isPalListKind'(__'(V1, V2))) → mark'(and'(isPalListKind'(V1), isPalListKind'(V2)))
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'(X1, X2)) → U11'(active'(X1), X2)
active'(U12'(X)) → U12'(active'(X))
active'(U21'(X1, X2, X3)) → U21'(active'(X1), X2, X3)
active'(U22'(X1, X2)) → U22'(active'(X1), X2)
active'(U23'(X)) → U23'(active'(X))
active'(U31'(X1, X2)) → U31'(active'(X1), X2)
active'(U32'(X)) → U32'(active'(X))
active'(U41'(X1, X2, X3)) → U41'(active'(X1), X2, X3)
active'(U42'(X1, X2)) → U42'(active'(X1), X2)
active'(U43'(X)) → U43'(active'(X))
active'(U51'(X1, X2, X3)) → U51'(active'(X1), X2, X3)
active'(U52'(X1, X2)) → U52'(active'(X1), X2)
active'(U53'(X)) → U53'(active'(X))
active'(U61'(X1, X2)) → U61'(active'(X1), X2)
active'(U62'(X)) → U62'(active'(X))
active'(U71'(X1, X2)) → U71'(active'(X1), X2)
active'(U72'(X)) → U72'(active'(X))
active'(and'(X1, X2)) → and'(active'(X1), X2)
__'(mark'(X1), X2) → mark'(__'(X1, X2))
__'(X1, mark'(X2)) → mark'(__'(X1, X2))
U11'(mark'(X1), X2) → mark'(U11'(X1, X2))
U12'(mark'(X)) → mark'(U12'(X))
U21'(mark'(X1), X2, X3) → mark'(U21'(X1, X2, X3))
U22'(mark'(X1), X2) → mark'(U22'(X1, X2))
U23'(mark'(X)) → mark'(U23'(X))
U31'(mark'(X1), X2) → mark'(U31'(X1, X2))
U32'(mark'(X)) → mark'(U32'(X))
U41'(mark'(X1), X2, X3) → mark'(U41'(X1, X2, X3))
U42'(mark'(X1), X2) → mark'(U42'(X1, X2))
U43'(mark'(X)) → mark'(U43'(X))
U51'(mark'(X1), X2, X3) → mark'(U51'(X1, X2, X3))
U52'(mark'(X1), X2) → mark'(U52'(X1, X2))
U53'(mark'(X)) → mark'(U53'(X))
U61'(mark'(X1), X2) → mark'(U61'(X1, X2))
U62'(mark'(X)) → mark'(U62'(X))
U71'(mark'(X1), X2) → mark'(U71'(X1, X2))
U72'(mark'(X)) → mark'(U72'(X))
and'(mark'(X1), X2) → mark'(and'(X1, X2))
proper'(__'(X1, X2)) → __'(proper'(X1), proper'(X2))
proper'(nil') → ok'(nil')
proper'(U11'(X1, X2)) → U11'(proper'(X1), proper'(X2))
proper'(tt') → ok'(tt')
proper'(U12'(X)) → U12'(proper'(X))
proper'(isNeList'(X)) → isNeList'(proper'(X))
proper'(U21'(X1, X2, X3)) → U21'(proper'(X1), proper'(X2), proper'(X3))
proper'(U22'(X1, X2)) → U22'(proper'(X1), proper'(X2))
proper'(isList'(X)) → isList'(proper'(X))
proper'(U23'(X)) → U23'(proper'(X))
proper'(U31'(X1, X2)) → U31'(proper'(X1), proper'(X2))
proper'(U32'(X)) → U32'(proper'(X))
proper'(isQid'(X)) → isQid'(proper'(X))
proper'(U41'(X1, X2, X3)) → U41'(proper'(X1), proper'(X2), proper'(X3))
proper'(U42'(X1, X2)) → U42'(proper'(X1), proper'(X2))
proper'(U43'(X)) → U43'(proper'(X))
proper'(U51'(X1, X2, X3)) → U51'(proper'(X1), proper'(X2), proper'(X3))
proper'(U52'(X1, X2)) → U52'(proper'(X1), proper'(X2))
proper'(U53'(X)) → U53'(proper'(X))
proper'(U61'(X1, X2)) → U61'(proper'(X1), proper'(X2))
proper'(U62'(X)) → U62'(proper'(X))
proper'(U71'(X1, X2)) → U71'(proper'(X1), proper'(X2))
proper'(U72'(X)) → U72'(proper'(X))
proper'(isNePal'(X)) → isNePal'(proper'(X))
proper'(and'(X1, X2)) → and'(proper'(X1), proper'(X2))
proper'(isPalListKind'(X)) → isPalListKind'(proper'(X))
proper'(isPal'(X)) → isPal'(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'(X1), ok'(X2)) → ok'(U11'(X1, X2))
U12'(ok'(X)) → ok'(U12'(X))
isNeList'(ok'(X)) → ok'(isNeList'(X))
U21'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U21'(X1, X2, X3))
U22'(ok'(X1), ok'(X2)) → ok'(U22'(X1, X2))
isList'(ok'(X)) → ok'(isList'(X))
U23'(ok'(X)) → ok'(U23'(X))
U31'(ok'(X1), ok'(X2)) → ok'(U31'(X1, X2))
U32'(ok'(X)) → ok'(U32'(X))
isQid'(ok'(X)) → ok'(isQid'(X))
U41'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U41'(X1, X2, X3))
U42'(ok'(X1), ok'(X2)) → ok'(U42'(X1, X2))
U43'(ok'(X)) → ok'(U43'(X))
U51'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U51'(X1, X2, X3))
U52'(ok'(X1), ok'(X2)) → ok'(U52'(X1, X2))
U53'(ok'(X)) → ok'(U53'(X))
U61'(ok'(X1), ok'(X2)) → ok'(U61'(X1, X2))
U62'(ok'(X)) → ok'(U62'(X))
U71'(ok'(X1), ok'(X2)) → ok'(U71'(X1, X2))
U72'(ok'(X)) → ok'(U72'(X))
isNePal'(ok'(X)) → ok'(isNePal'(X))
and'(ok'(X1), ok'(X2)) → ok'(and'(X1, X2))
isPalListKind'(ok'(X)) → ok'(isPalListKind'(X))
isPal'(ok'(X)) → ok'(isPal'(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', V)) → mark'(U12'(isNeList'(V)))
active'(U12'(tt')) → mark'(tt')
active'(U21'(tt', V1, V2)) → mark'(U22'(isList'(V1), V2))
active'(U22'(tt', V2)) → mark'(U23'(isList'(V2)))
active'(U23'(tt')) → mark'(tt')
active'(U31'(tt', V)) → mark'(U32'(isQid'(V)))
active'(U32'(tt')) → mark'(tt')
active'(U41'(tt', V1, V2)) → mark'(U42'(isList'(V1), V2))
active'(U42'(tt', V2)) → mark'(U43'(isNeList'(V2)))
active'(U43'(tt')) → mark'(tt')
active'(U51'(tt', V1, V2)) → mark'(U52'(isNeList'(V1), V2))
active'(U52'(tt', V2)) → mark'(U53'(isList'(V2)))
active'(U53'(tt')) → mark'(tt')
active'(U61'(tt', V)) → mark'(U62'(isQid'(V)))
active'(U62'(tt')) → mark'(tt')
active'(U71'(tt', V)) → mark'(U72'(isNePal'(V)))
active'(U72'(tt')) → mark'(tt')
active'(and'(tt', X)) → mark'(X)
active'(isList'(V)) → mark'(U11'(isPalListKind'(V), V))
active'(isList'(nil')) → mark'(tt')
active'(isList'(__'(V1, V2))) → mark'(U21'(and'(isPalListKind'(V1), isPalListKind'(V2)), V1, V2))
active'(isNeList'(V)) → mark'(U31'(isPalListKind'(V), V))
active'(isNeList'(__'(V1, V2))) → mark'(U41'(and'(isPalListKind'(V1), isPalListKind'(V2)), V1, V2))
active'(isNeList'(__'(V1, V2))) → mark'(U51'(and'(isPalListKind'(V1), isPalListKind'(V2)), V1, V2))
active'(isNePal'(V)) → mark'(U61'(isPalListKind'(V), V))
active'(isNePal'(__'(I, __'(P, I)))) → mark'(and'(and'(isQid'(I), isPalListKind'(I)), and'(isPal'(P), isPalListKind'(P))))
active'(isPal'(V)) → mark'(U71'(isPalListKind'(V), V))
active'(isPal'(nil')) → mark'(tt')
active'(isPalListKind'(a')) → mark'(tt')
active'(isPalListKind'(e')) → mark'(tt')
active'(isPalListKind'(i')) → mark'(tt')
active'(isPalListKind'(nil')) → mark'(tt')
active'(isPalListKind'(o')) → mark'(tt')
active'(isPalListKind'(u')) → mark'(tt')
active'(isPalListKind'(__'(V1, V2))) → mark'(and'(isPalListKind'(V1), isPalListKind'(V2)))
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'(X1, X2)) → U11'(active'(X1), X2)
active'(U12'(X)) → U12'(active'(X))
active'(U21'(X1, X2, X3)) → U21'(active'(X1), X2, X3)
active'(U22'(X1, X2)) → U22'(active'(X1), X2)
active'(U23'(X)) → U23'(active'(X))
active'(U31'(X1, X2)) → U31'(active'(X1), X2)
active'(U32'(X)) → U32'(active'(X))
active'(U41'(X1, X2, X3)) → U41'(active'(X1), X2, X3)
active'(U42'(X1, X2)) → U42'(active'(X1), X2)
active'(U43'(X)) → U43'(active'(X))
active'(U51'(X1, X2, X3)) → U51'(active'(X1), X2, X3)
active'(U52'(X1, X2)) → U52'(active'(X1), X2)
active'(U53'(X)) → U53'(active'(X))
active'(U61'(X1, X2)) → U61'(active'(X1), X2)
active'(U62'(X)) → U62'(active'(X))
active'(U71'(X1, X2)) → U71'(active'(X1), X2)
active'(U72'(X)) → U72'(active'(X))
active'(and'(X1, X2)) → and'(active'(X1), X2)
__'(mark'(X1), X2) → mark'(__'(X1, X2))
__'(X1, mark'(X2)) → mark'(__'(X1, X2))
U11'(mark'(X1), X2) → mark'(U11'(X1, X2))
U12'(mark'(X)) → mark'(U12'(X))
U21'(mark'(X1), X2, X3) → mark'(U21'(X1, X2, X3))
U22'(mark'(X1), X2) → mark'(U22'(X1, X2))
U23'(mark'(X)) → mark'(U23'(X))
U31'(mark'(X1), X2) → mark'(U31'(X1, X2))
U32'(mark'(X)) → mark'(U32'(X))
U41'(mark'(X1), X2, X3) → mark'(U41'(X1, X2, X3))
U42'(mark'(X1), X2) → mark'(U42'(X1, X2))
U43'(mark'(X)) → mark'(U43'(X))
U51'(mark'(X1), X2, X3) → mark'(U51'(X1, X2, X3))
U52'(mark'(X1), X2) → mark'(U52'(X1, X2))
U53'(mark'(X)) → mark'(U53'(X))
U61'(mark'(X1), X2) → mark'(U61'(X1, X2))
U62'(mark'(X)) → mark'(U62'(X))
U71'(mark'(X1), X2) → mark'(U71'(X1, X2))
U72'(mark'(X)) → mark'(U72'(X))
and'(mark'(X1), X2) → mark'(and'(X1, X2))
proper'(__'(X1, X2)) → __'(proper'(X1), proper'(X2))
proper'(nil') → ok'(nil')
proper'(U11'(X1, X2)) → U11'(proper'(X1), proper'(X2))
proper'(tt') → ok'(tt')
proper'(U12'(X)) → U12'(proper'(X))
proper'(isNeList'(X)) → isNeList'(proper'(X))
proper'(U21'(X1, X2, X3)) → U21'(proper'(X1), proper'(X2), proper'(X3))
proper'(U22'(X1, X2)) → U22'(proper'(X1), proper'(X2))
proper'(isList'(X)) → isList'(proper'(X))
proper'(U23'(X)) → U23'(proper'(X))
proper'(U31'(X1, X2)) → U31'(proper'(X1), proper'(X2))
proper'(U32'(X)) → U32'(proper'(X))
proper'(isQid'(X)) → isQid'(proper'(X))
proper'(U41'(X1, X2, X3)) → U41'(proper'(X1), proper'(X2), proper'(X3))
proper'(U42'(X1, X2)) → U42'(proper'(X1), proper'(X2))
proper'(U43'(X)) → U43'(proper'(X))
proper'(U51'(X1, X2, X3)) → U51'(proper'(X1), proper'(X2), proper'(X3))
proper'(U52'(X1, X2)) → U52'(proper'(X1), proper'(X2))
proper'(U53'(X)) → U53'(proper'(X))
proper'(U61'(X1, X2)) → U61'(proper'(X1), proper'(X2))
proper'(U62'(X)) → U62'(proper'(X))
proper'(U71'(X1, X2)) → U71'(proper'(X1), proper'(X2))
proper'(U72'(X)) → U72'(proper'(X))
proper'(isNePal'(X)) → isNePal'(proper'(X))
proper'(and'(X1, X2)) → and'(proper'(X1), proper'(X2))
proper'(isPalListKind'(X)) → isPalListKind'(proper'(X))
proper'(isPal'(X)) → isPal'(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'(X1), ok'(X2)) → ok'(U11'(X1, X2))
U12'(ok'(X)) → ok'(U12'(X))
isNeList'(ok'(X)) → ok'(isNeList'(X))
U21'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U21'(X1, X2, X3))
U22'(ok'(X1), ok'(X2)) → ok'(U22'(X1, X2))
isList'(ok'(X)) → ok'(isList'(X))
U23'(ok'(X)) → ok'(U23'(X))
U31'(ok'(X1), ok'(X2)) → ok'(U31'(X1, X2))
U32'(ok'(X)) → ok'(U32'(X))
isQid'(ok'(X)) → ok'(isQid'(X))
U41'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U41'(X1, X2, X3))
U42'(ok'(X1), ok'(X2)) → ok'(U42'(X1, X2))
U43'(ok'(X)) → ok'(U43'(X))
U51'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U51'(X1, X2, X3))
U52'(ok'(X1), ok'(X2)) → ok'(U52'(X1, X2))
U53'(ok'(X)) → ok'(U53'(X))
U61'(ok'(X1), ok'(X2)) → ok'(U61'(X1, X2))
U62'(ok'(X)) → ok'(U62'(X))
U71'(ok'(X1), ok'(X2)) → ok'(U71'(X1, X2))
U72'(ok'(X)) → ok'(U72'(X))
isNePal'(ok'(X)) → ok'(isNePal'(X))
and'(ok'(X1), ok'(X2)) → ok'(and'(X1, X2))
isPalListKind'(ok'(X)) → ok'(isPalListKind'(X))
isPal'(ok'(X)) → ok'(isPal'(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' → mark':nil':tt':a':e':i':o':u':ok'
tt' :: mark':nil':tt':a':e':i':o':u':ok'
U12' :: 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'
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' → 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' → 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'
U23' :: 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' → mark':nil':tt':a':e':i':o':u':ok'
U32' :: 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'
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' → 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' → mark':nil':tt':a':e':i':o':u':ok'
U43' :: 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' → 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' → mark':nil':tt':a':e':i':o':u':ok'
U53' :: 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' → mark':nil':tt':a':e':i':o':u':ok'
U62' :: 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'
isNePal' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
and' :: 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'
isPalListKind' :: 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'
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', __', U12', isNeList', U22', isList', U23', U32', isQid', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
__' < active'
U12' < active'
isNeList' < active'
U22' < active'
isList' < active'
U23' < active'
U32' < active'
isQid' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
__' < proper'
U12' < proper'
isNeList' < proper'
U22' < proper'
isList' < proper'
U23' < proper'
U32' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < 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', U12', isNeList', U22', isList', U23', U32', isQid', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', 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:
U12', active', isNeList', U22', isList', U23', U32', isQid', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
U12' < active'
isNeList' < active'
U22' < active'
isList' < active'
U23' < active'
U32' < active'
isQid' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
U12' < proper'
isNeList' < proper'
U22' < proper'
isList' < proper'
U23' < proper'
U32' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < proper'
proper' < top'

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

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

Induction Step:
U12'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n6468, 1)))) →_R^Ω(1)
mark'(U12'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n6468)))) →_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', U22', isList', U23', U32', isQid', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
isNeList' < active'
U22' < active'
isList' < active'
U23' < active'
U32' < active'
isQid' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
isNeList' < proper'
U22' < proper'
isList' < proper'
U23' < proper'
U32' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < 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:
U22', active', isList', U23', U32', isQid', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
U22' < active'
isList' < active'
U23' < active'
U32' < active'
isQid' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
U22' < proper'
isList' < proper'
U23' < proper'
U32' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < proper'
proper' < top'

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

Induction Base:
U22'(___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:
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n10646, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b11790)) →_R^Ω(1)
mark'(U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n10646)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b11790))) →_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', U23', U32', isQid', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
isList' < active'
U23' < active'
U32' < active'
isQid' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
isList' < proper'
U23' < proper'
U32' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < 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:
U23', active', U32', isQid', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
U23' < active'
U32' < active'
isQid' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
U23' < proper'
U32' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < proper'
proper' < top'

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

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

Induction Step:
U23'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n17530, 1)))) →_R^Ω(1)
mark'(U23'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n17530)))) →_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:
U32', active', isQid', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
U32' < active'
isQid' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
U32' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < proper'
proper' < top'

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

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

Induction Step:
U32'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n22001, 1)))) →_R^Ω(1)
mark'(U32'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n22001)))) →_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', U42', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
isQid' < active'
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
isQid' < proper'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < 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:
U42', active', U43', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
U42' < active'
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
U42' < proper'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < proper'
proper' < top'

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

Induction Base:
U42'(___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:
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n26640, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b28540)) →_R^Ω(1)
mark'(U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n26640)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b28540))) →_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:
U43', active', U52', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
U43' < active'
U52' < active'
U53' < active'
U62' < active'
U72' < active'
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
U43' < proper'
U52' < proper'
U53' < proper'
U62' < proper'
U72' < proper'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < proper'
proper' < top'

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

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

Induction Step:
U43'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n34342, 1)))) →_R^Ω(1)
mark'(U43'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n34342)))) →_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:
U52', active', U53', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

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

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

Induction Base:
U52'(___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:
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n39252, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b41692)) →_R^Ω(1)
mark'(U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n39252)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b41692))) →_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:
U53', active', U62', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

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

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

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

Induction Step:
U53'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n47563, 1)))) →_R^Ω(1)
mark'(U53'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n47563)))) →_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:
U62', active', U72', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

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

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

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

Induction Step:
U62'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n52788, 1)))) →_R^Ω(1)
mark'(U62'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n52788)))) →_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', isNePal', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

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

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

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, +(___$n58137, 1)))) →_R^Ω(1)
mark'(U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n58137)))) →_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', U11', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
isNePal' < active'
U11' < active'
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
isNePal' < proper'
U11' < proper'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < 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:
U11', active', isPalListKind', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

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

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

Induction Base:
U11'(___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:
U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n63698, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b67110)) →_R^Ω(1)
mark'(U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n63698)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b67110))) →_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:
isPalListKind', active', U21', and', U31', U41', U51', U61', isPal', U71', proper', top'

They will be analysed ascendingly in the following order:
isPalListKind' < active'
U21' < active'
and' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
isPal' < active'
U71' < active'
active' < top'
isPalListKind' < proper'
U21' < proper'
and' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
isPal' < proper'
U71' < proper'
proper' < top'

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

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', and', U31', U41', U51', U61', isPal', U71', proper', top'

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

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

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), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(c))

Induction Step:
U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n73198, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b78908), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c78909)) →_R^Ω(1)
mark'(U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n73198)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b78908), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c78909))) →_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:
and', active', U31', U41', U51', U61', isPal', U71', proper', top'

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

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

Induction Base:
and'(___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:
and'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n87064, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b91232)) →_R^Ω(1)
mark'(and'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n87064)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b91232))) →_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', U41', U51', U61', isPal', U71', proper', top'

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

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

Induction Base:
U31'(___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:
U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n97329, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b101821)) →_R^Ω(1)
mark'(U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n97329)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b101821))) →_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})
U12'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n6467))) → ___*4, rt ∈ Ω(_{__n6467})
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n10645)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n10645})
U23'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n17529))) → ___*4, rt ∈ Ω(_{__n17529})
U32'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n22000))) → ___*4, rt ∈ Ω(_{__n22000})
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n26639)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n26639})
U43'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n34341))) → ___*4, rt ∈ Ω(_{__n34341})
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n39251)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n39251})
U53'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n47562))) → ___*4, rt ∈ Ω(_{__n47562})
U62'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n52787))) → ___*4, rt ∈ Ω(_{__n52787})
U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n58136))) → ___*4, rt ∈ Ω(_{__n58136})
U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n63697)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n63697})
U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n73197)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(c)) → ___*4, rt ∈ Ω(_{__n73197})
and'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n87063)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n87063})
U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n97328)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n97328})

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', isPal', U71', proper', top'

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

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

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), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(c))

Induction Step:
U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n107962, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b115292), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c115293)) →_R^Ω(1)
mark'(U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n107962)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b115292), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c115293))) →_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', isPal', U71', proper', top'

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

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

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), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(c))

Induction Step:
U51'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n123650, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b131628), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c131629)) →_R^Ω(1)
mark'(U51'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n123650)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b131628), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c131629))) →_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:
U61', active', isPal', U71', proper', top'

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

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

Induction Base:
U61'(___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:
U61'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n140070, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b145750)) →_R^Ω(1)
mark'(U61'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n140070)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b145750))) →_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', U71', proper', top'

They will be analysed ascendingly in the following order:
isPal' < active'
U71' < active'
active' < top'
isPal' < proper'
U71' < 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:
U71', active', proper', top'

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

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

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, +(___$n152231, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b158235)) →_R^Ω(1)
mark'(U71'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n152231)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b158235))) →_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:
active', proper', top'

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