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(isPalListKind(V), V))
active(U12(tt, V)) → mark(U13(isNeList(V)))
active(U13(tt)) → mark(tt)
active(U21(tt, V1, V2)) → mark(U22(isPalListKind(V1), V1, V2))
active(U22(tt, V1, V2)) → mark(U23(isPalListKind(V2), V1, V2))
active(U23(tt, V1, V2)) → mark(U24(isPalListKind(V2), V1, V2))
active(U24(tt, V1, V2)) → mark(U25(isList(V1), V2))
active(U25(tt, V2)) → mark(U26(isList(V2)))
active(U26(tt)) → mark(tt)
active(U31(tt, V)) → mark(U32(isPalListKind(V), V))
active(U32(tt, V)) → mark(U33(isQid(V)))
active(U33(tt)) → mark(tt)
active(U41(tt, V1, V2)) → mark(U42(isPalListKind(V1), V1, V2))
active(U42(tt, V1, V2)) → mark(U43(isPalListKind(V2), V1, V2))
active(U43(tt, V1, V2)) → mark(U44(isPalListKind(V2), V1, V2))
active(U44(tt, V1, V2)) → mark(U45(isList(V1), V2))
active(U45(tt, V2)) → mark(U46(isNeList(V2)))
active(U46(tt)) → mark(tt)
active(U51(tt, V1, V2)) → mark(U52(isPalListKind(V1), V1, V2))
active(U52(tt, V1, V2)) → mark(U53(isPalListKind(V2), V1, V2))
active(U53(tt, V1, V2)) → mark(U54(isPalListKind(V2), V1, V2))
active(U54(tt, V1, V2)) → mark(U55(isNeList(V1), V2))
active(U55(tt, V2)) → mark(U56(isList(V2)))
active(U56(tt)) → mark(tt)
active(U61(tt, V)) → mark(U62(isPalListKind(V), V))
active(U62(tt, V)) → mark(U63(isQid(V)))
active(U63(tt)) → mark(tt)
active(U71(tt, I, P)) → mark(U72(isPalListKind(I), P))
active(U72(tt, P)) → mark(U73(isPal(P), P))
active(U73(tt, P)) → mark(U74(isPalListKind(P)))
active(U74(tt)) → mark(tt)
active(U81(tt, V)) → mark(U82(isPalListKind(V), V))
active(U82(tt, V)) → mark(U83(isNePal(V)))
active(U83(tt)) → mark(tt)
active(U91(tt, V2)) → mark(U92(isPalListKind(V2)))
active(U92(tt)) → mark(tt)
active(isList(V)) → mark(U11(isPalListKind(V), V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(U21(isPalListKind(V1), V1, V2))
active(isNeList(V)) → mark(U31(isPalListKind(V), V))
active(isNeList(__(V1, V2))) → mark(U41(isPalListKind(V1), V1, V2))
active(isNeList(__(V1, V2))) → mark(U51(isPalListKind(V1), V1, V2))
active(isNePal(V)) → mark(U61(isPalListKind(V), V))
active(isNePal(__(I, __(P, I)))) → mark(U71(isQid(I), I, P))
active(isPal(V)) → mark(U81(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(U91(isPalListKind(V1), 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(X1, X2)) → U12(active(X1), X2)
active(U13(X)) → U13(active(X))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(U23(X1, X2, X3)) → U23(active(X1), X2, X3)
active(U24(X1, X2, X3)) → U24(active(X1), X2, X3)
active(U25(X1, X2)) → U25(active(X1), X2)
active(U26(X)) → U26(active(X))
active(U31(X1, X2)) → U31(active(X1), X2)
active(U32(X1, X2)) → U32(active(X1), X2)
active(U33(X)) → U33(active(X))
active(U41(X1, X2, X3)) → U41(active(X1), X2, X3)
active(U42(X1, X2, X3)) → U42(active(X1), X2, X3)
active(U43(X1, X2, X3)) → U43(active(X1), X2, X3)
active(U44(X1, X2, X3)) → U44(active(X1), X2, X3)
active(U45(X1, X2)) → U45(active(X1), X2)
active(U46(X)) → U46(active(X))
active(U51(X1, X2, X3)) → U51(active(X1), X2, X3)
active(U52(X1, X2, X3)) → U52(active(X1), X2, X3)
active(U53(X1, X2, X3)) → U53(active(X1), X2, X3)
active(U54(X1, X2, X3)) → U54(active(X1), X2, X3)
active(U55(X1, X2)) → U55(active(X1), X2)
active(U56(X)) → U56(active(X))
active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X1, X2)) → U62(active(X1), X2)
active(U63(X)) → U63(active(X))
active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)
active(U73(X1, X2)) → U73(active(X1), X2)
active(U74(X)) → U74(active(X))
active(U81(X1, X2)) → U81(active(X1), X2)
active(U82(X1, X2)) → U82(active(X1), X2)
active(U83(X)) → U83(active(X))
active(U91(X1, X2)) → U91(active(X1), X2)
active(U92(X)) → U92(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
U12(mark(X1), X2) → mark(U12(X1, X2))
U13(mark(X)) → mark(U13(X))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
U23(mark(X1), X2, X3) → mark(U23(X1, X2, X3))
U24(mark(X1), X2, X3) → mark(U24(X1, X2, X3))
U25(mark(X1), X2) → mark(U25(X1, X2))
U26(mark(X)) → mark(U26(X))
U31(mark(X1), X2) → mark(U31(X1, X2))
U32(mark(X1), X2) → mark(U32(X1, X2))
U33(mark(X)) → mark(U33(X))
U41(mark(X1), X2, X3) → mark(U41(X1, X2, X3))
U42(mark(X1), X2, X3) → mark(U42(X1, X2, X3))
U43(mark(X1), X2, X3) → mark(U43(X1, X2, X3))
U44(mark(X1), X2, X3) → mark(U44(X1, X2, X3))
U45(mark(X1), X2) → mark(U45(X1, X2))
U46(mark(X)) → mark(U46(X))
U51(mark(X1), X2, X3) → mark(U51(X1, X2, X3))
U52(mark(X1), X2, X3) → mark(U52(X1, X2, X3))
U53(mark(X1), X2, X3) → mark(U53(X1, X2, X3))
U54(mark(X1), X2, X3) → mark(U54(X1, X2, X3))
U55(mark(X1), X2) → mark(U55(X1, X2))
U56(mark(X)) → mark(U56(X))
U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X1), X2) → mark(U62(X1, X2))
U63(mark(X)) → mark(U63(X))
U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))
U73(mark(X1), X2) → mark(U73(X1, X2))
U74(mark(X)) → mark(U74(X))
U81(mark(X1), X2) → mark(U81(X1, X2))
U82(mark(X1), X2) → mark(U82(X1, X2))
U83(mark(X)) → mark(U83(X))
U91(mark(X1), X2) → mark(U91(X1, X2))
U92(mark(X)) → mark(U92(X))
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(X1, X2)) → U12(proper(X1), proper(X2))
proper(isPalListKind(X)) → isPalListKind(proper(X))
proper(U13(X)) → U13(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(U23(X1, X2, X3)) → U23(proper(X1), proper(X2), proper(X3))
proper(U24(X1, X2, X3)) → U24(proper(X1), proper(X2), proper(X3))
proper(U25(X1, X2)) → U25(proper(X1), proper(X2))
proper(isList(X)) → isList(proper(X))
proper(U26(X)) → U26(proper(X))
proper(U31(X1, X2)) → U31(proper(X1), proper(X2))
proper(U32(X1, X2)) → U32(proper(X1), proper(X2))
proper(U33(X)) → U33(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(U41(X1, X2, X3)) → U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2, X3)) → U42(proper(X1), proper(X2), proper(X3))
proper(U43(X1, X2, X3)) → U43(proper(X1), proper(X2), proper(X3))
proper(U44(X1, X2, X3)) → U44(proper(X1), proper(X2), proper(X3))
proper(U45(X1, X2)) → U45(proper(X1), proper(X2))
proper(U46(X)) → U46(proper(X))
proper(U51(X1, X2, X3)) → U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2, X3)) → U52(proper(X1), proper(X2), proper(X3))
proper(U53(X1, X2, X3)) → U53(proper(X1), proper(X2), proper(X3))
proper(U54(X1, X2, X3)) → U54(proper(X1), proper(X2), proper(X3))
proper(U55(X1, X2)) → U55(proper(X1), proper(X2))
proper(U56(X)) → U56(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))
proper(U62(X1, X2)) → U62(proper(X1), proper(X2))
proper(U63(X)) → U63(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))
proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(U73(X1, X2)) → U73(proper(X1), proper(X2))
proper(isPal(X)) → isPal(proper(X))
proper(U74(X)) → U74(proper(X))
proper(U81(X1, X2)) → U81(proper(X1), proper(X2))
proper(U82(X1, X2)) → U82(proper(X1), proper(X2))
proper(U83(X)) → U83(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(U91(X1, X2)) → U91(proper(X1), proper(X2))
proper(U92(X)) → U92(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(X1), ok(X2)) → ok(U12(X1, X2))
isPalListKind(ok(X)) → ok(isPalListKind(X))
U13(ok(X)) → ok(U13(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(X3)) → ok(U22(X1, X2, X3))
U23(ok(X1), ok(X2), ok(X3)) → ok(U23(X1, X2, X3))
U24(ok(X1), ok(X2), ok(X3)) → ok(U24(X1, X2, X3))
U25(ok(X1), ok(X2)) → ok(U25(X1, X2))
isList(ok(X)) → ok(isList(X))
U26(ok(X)) → ok(U26(X))
U31(ok(X1), ok(X2)) → ok(U31(X1, X2))
U32(ok(X1), ok(X2)) → ok(U32(X1, X2))
U33(ok(X)) → ok(U33(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(X3)) → ok(U42(X1, X2, X3))
U43(ok(X1), ok(X2), ok(X3)) → ok(U43(X1, X2, X3))
U44(ok(X1), ok(X2), ok(X3)) → ok(U44(X1, X2, X3))
U45(ok(X1), ok(X2)) → ok(U45(X1, X2))
U46(ok(X)) → ok(U46(X))
U51(ok(X1), ok(X2), ok(X3)) → ok(U51(X1, X2, X3))
U52(ok(X1), ok(X2), ok(X3)) → ok(U52(X1, X2, X3))
U53(ok(X1), ok(X2), ok(X3)) → ok(U53(X1, X2, X3))
U54(ok(X1), ok(X2), ok(X3)) → ok(U54(X1, X2, X3))
U55(ok(X1), ok(X2)) → ok(U55(X1, X2))
U56(ok(X)) → ok(U56(X))
U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X1), ok(X2)) → ok(U62(X1, X2))
U63(ok(X)) → ok(U63(X))
U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))
U73(ok(X1), ok(X2)) → ok(U73(X1, X2))
isPal(ok(X)) → ok(isPal(X))
U74(ok(X)) → ok(U74(X))
U81(ok(X1), ok(X2)) → ok(U81(X1, X2))
U82(ok(X1), ok(X2)) → ok(U82(X1, X2))
U83(ok(X)) → ok(U83(X))
isNePal(ok(X)) → ok(isNePal(X))
U91(ok(X1), ok(X2)) → ok(U91(X1, X2))
U92(ok(X)) → ok(U92(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'(isPalListKind'(V), V))
active'(U12'(tt', V)) → mark'(U13'(isNeList'(V)))
active'(U13'(tt')) → mark'(tt')
active'(U21'(tt', V1, V2)) → mark'(U22'(isPalListKind'(V1), V1, V2))
active'(U22'(tt', V1, V2)) → mark'(U23'(isPalListKind'(V2), V1, V2))
active'(U23'(tt', V1, V2)) → mark'(U24'(isPalListKind'(V2), V1, V2))
active'(U24'(tt', V1, V2)) → mark'(U25'(isList'(V1), V2))
active'(U25'(tt', V2)) → mark'(U26'(isList'(V2)))
active'(U26'(tt')) → mark'(tt')
active'(U31'(tt', V)) → mark'(U32'(isPalListKind'(V), V))
active'(U32'(tt', V)) → mark'(U33'(isQid'(V)))
active'(U33'(tt')) → mark'(tt')
active'(U41'(tt', V1, V2)) → mark'(U42'(isPalListKind'(V1), V1, V2))
active'(U42'(tt', V1, V2)) → mark'(U43'(isPalListKind'(V2), V1, V2))
active'(U43'(tt', V1, V2)) → mark'(U44'(isPalListKind'(V2), V1, V2))
active'(U44'(tt', V1, V2)) → mark'(U45'(isList'(V1), V2))
active'(U45'(tt', V2)) → mark'(U46'(isNeList'(V2)))
active'(U46'(tt')) → mark'(tt')
active'(U51'(tt', V1, V2)) → mark'(U52'(isPalListKind'(V1), V1, V2))
active'(U52'(tt', V1, V2)) → mark'(U53'(isPalListKind'(V2), V1, V2))
active'(U53'(tt', V1, V2)) → mark'(U54'(isPalListKind'(V2), V1, V2))
active'(U54'(tt', V1, V2)) → mark'(U55'(isNeList'(V1), V2))
active'(U55'(tt', V2)) → mark'(U56'(isList'(V2)))
active'(U56'(tt')) → mark'(tt')
active'(U61'(tt', V)) → mark'(U62'(isPalListKind'(V), V))
active'(U62'(tt', V)) → mark'(U63'(isQid'(V)))
active'(U63'(tt')) → mark'(tt')
active'(U71'(tt', I, P)) → mark'(U72'(isPalListKind'(I), P))
active'(U72'(tt', P)) → mark'(U73'(isPal'(P), P))
active'(U73'(tt', P)) → mark'(U74'(isPalListKind'(P)))
active'(U74'(tt')) → mark'(tt')
active'(U81'(tt', V)) → mark'(U82'(isPalListKind'(V), V))
active'(U82'(tt', V)) → mark'(U83'(isNePal'(V)))
active'(U83'(tt')) → mark'(tt')
active'(U91'(tt', V2)) → mark'(U92'(isPalListKind'(V2)))
active'(U92'(tt')) → mark'(tt')
active'(isList'(V)) → mark'(U11'(isPalListKind'(V), V))
active'(isList'(nil')) → mark'(tt')
active'(isList'(__'(V1, V2))) → mark'(U21'(isPalListKind'(V1), V1, V2))
active'(isNeList'(V)) → mark'(U31'(isPalListKind'(V), V))
active'(isNeList'(__'(V1, V2))) → mark'(U41'(isPalListKind'(V1), V1, V2))
active'(isNeList'(__'(V1, V2))) → mark'(U51'(isPalListKind'(V1), V1, V2))
active'(isNePal'(V)) → mark'(U61'(isPalListKind'(V), V))
active'(isNePal'(__'(I, __'(P, I)))) → mark'(U71'(isQid'(I), I, P))
active'(isPal'(V)) → mark'(U81'(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'(U91'(isPalListKind'(V1), 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'(X1, X2)) → U12'(active'(X1), X2)
active'(U13'(X)) → U13'(active'(X))
active'(U21'(X1, X2, X3)) → U21'(active'(X1), X2, X3)
active'(U22'(X1, X2, X3)) → U22'(active'(X1), X2, X3)
active'(U23'(X1, X2, X3)) → U23'(active'(X1), X2, X3)
active'(U24'(X1, X2, X3)) → U24'(active'(X1), X2, X3)
active'(U25'(X1, X2)) → U25'(active'(X1), X2)
active'(U26'(X)) → U26'(active'(X))
active'(U31'(X1, X2)) → U31'(active'(X1), X2)
active'(U32'(X1, X2)) → U32'(active'(X1), X2)
active'(U33'(X)) → U33'(active'(X))
active'(U41'(X1, X2, X3)) → U41'(active'(X1), X2, X3)
active'(U42'(X1, X2, X3)) → U42'(active'(X1), X2, X3)
active'(U43'(X1, X2, X3)) → U43'(active'(X1), X2, X3)
active'(U44'(X1, X2, X3)) → U44'(active'(X1), X2, X3)
active'(U45'(X1, X2)) → U45'(active'(X1), X2)
active'(U46'(X)) → U46'(active'(X))
active'(U51'(X1, X2, X3)) → U51'(active'(X1), X2, X3)
active'(U52'(X1, X2, X3)) → U52'(active'(X1), X2, X3)
active'(U53'(X1, X2, X3)) → U53'(active'(X1), X2, X3)
active'(U54'(X1, X2, X3)) → U54'(active'(X1), X2, X3)
active'(U55'(X1, X2)) → U55'(active'(X1), X2)
active'(U56'(X)) → U56'(active'(X))
active'(U61'(X1, X2)) → U61'(active'(X1), X2)
active'(U62'(X1, X2)) → U62'(active'(X1), X2)
active'(U63'(X)) → U63'(active'(X))
active'(U71'(X1, X2, X3)) → U71'(active'(X1), X2, X3)
active'(U72'(X1, X2)) → U72'(active'(X1), X2)
active'(U73'(X1, X2)) → U73'(active'(X1), X2)
active'(U74'(X)) → U74'(active'(X))
active'(U81'(X1, X2)) → U81'(active'(X1), X2)
active'(U82'(X1, X2)) → U82'(active'(X1), X2)
active'(U83'(X)) → U83'(active'(X))
active'(U91'(X1, X2)) → U91'(active'(X1), X2)
active'(U92'(X)) → U92'(active'(X))
__'(mark'(X1), X2) → mark'(__'(X1, X2))
__'(X1, mark'(X2)) → mark'(__'(X1, X2))
U11'(mark'(X1), X2) → mark'(U11'(X1, X2))
U12'(mark'(X1), X2) → mark'(U12'(X1, X2))
U13'(mark'(X)) → mark'(U13'(X))
U21'(mark'(X1), X2, X3) → mark'(U21'(X1, X2, X3))
U22'(mark'(X1), X2, X3) → mark'(U22'(X1, X2, X3))
U23'(mark'(X1), X2, X3) → mark'(U23'(X1, X2, X3))
U24'(mark'(X1), X2, X3) → mark'(U24'(X1, X2, X3))
U25'(mark'(X1), X2) → mark'(U25'(X1, X2))
U26'(mark'(X)) → mark'(U26'(X))
U31'(mark'(X1), X2) → mark'(U31'(X1, X2))
U32'(mark'(X1), X2) → mark'(U32'(X1, X2))
U33'(mark'(X)) → mark'(U33'(X))
U41'(mark'(X1), X2, X3) → mark'(U41'(X1, X2, X3))
U42'(mark'(X1), X2, X3) → mark'(U42'(X1, X2, X3))
U43'(mark'(X1), X2, X3) → mark'(U43'(X1, X2, X3))
U44'(mark'(X1), X2, X3) → mark'(U44'(X1, X2, X3))
U45'(mark'(X1), X2) → mark'(U45'(X1, X2))
U46'(mark'(X)) → mark'(U46'(X))
U51'(mark'(X1), X2, X3) → mark'(U51'(X1, X2, X3))
U52'(mark'(X1), X2, X3) → mark'(U52'(X1, X2, X3))
U53'(mark'(X1), X2, X3) → mark'(U53'(X1, X2, X3))
U54'(mark'(X1), X2, X3) → mark'(U54'(X1, X2, X3))
U55'(mark'(X1), X2) → mark'(U55'(X1, X2))
U56'(mark'(X)) → mark'(U56'(X))
U61'(mark'(X1), X2) → mark'(U61'(X1, X2))
U62'(mark'(X1), X2) → mark'(U62'(X1, X2))
U63'(mark'(X)) → mark'(U63'(X))
U71'(mark'(X1), X2, X3) → mark'(U71'(X1, X2, X3))
U72'(mark'(X1), X2) → mark'(U72'(X1, X2))
U73'(mark'(X1), X2) → mark'(U73'(X1, X2))
U74'(mark'(X)) → mark'(U74'(X))
U81'(mark'(X1), X2) → mark'(U81'(X1, X2))
U82'(mark'(X1), X2) → mark'(U82'(X1, X2))
U83'(mark'(X)) → mark'(U83'(X))
U91'(mark'(X1), X2) → mark'(U91'(X1, X2))
U92'(mark'(X)) → mark'(U92'(X))
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'(X1, X2)) → U12'(proper'(X1), proper'(X2))
proper'(isPalListKind'(X)) → isPalListKind'(proper'(X))
proper'(U13'(X)) → U13'(proper'(X))
proper'(isNeList'(X)) → isNeList'(proper'(X))
proper'(U21'(X1, X2, X3)) → U21'(proper'(X1), proper'(X2), proper'(X3))
proper'(U22'(X1, X2, X3)) → U22'(proper'(X1), proper'(X2), proper'(X3))
proper'(U23'(X1, X2, X3)) → U23'(proper'(X1), proper'(X2), proper'(X3))
proper'(U24'(X1, X2, X3)) → U24'(proper'(X1), proper'(X2), proper'(X3))
proper'(U25'(X1, X2)) → U25'(proper'(X1), proper'(X2))
proper'(isList'(X)) → isList'(proper'(X))
proper'(U26'(X)) → U26'(proper'(X))
proper'(U31'(X1, X2)) → U31'(proper'(X1), proper'(X2))
proper'(U32'(X1, X2)) → U32'(proper'(X1), proper'(X2))
proper'(U33'(X)) → U33'(proper'(X))
proper'(isQid'(X)) → isQid'(proper'(X))
proper'(U41'(X1, X2, X3)) → U41'(proper'(X1), proper'(X2), proper'(X3))
proper'(U42'(X1, X2, X3)) → U42'(proper'(X1), proper'(X2), proper'(X3))
proper'(U43'(X1, X2, X3)) → U43'(proper'(X1), proper'(X2), proper'(X3))
proper'(U44'(X1, X2, X3)) → U44'(proper'(X1), proper'(X2), proper'(X3))
proper'(U45'(X1, X2)) → U45'(proper'(X1), proper'(X2))
proper'(U46'(X)) → U46'(proper'(X))
proper'(U51'(X1, X2, X3)) → U51'(proper'(X1), proper'(X2), proper'(X3))
proper'(U52'(X1, X2, X3)) → U52'(proper'(X1), proper'(X2), proper'(X3))
proper'(U53'(X1, X2, X3)) → U53'(proper'(X1), proper'(X2), proper'(X3))
proper'(U54'(X1, X2, X3)) → U54'(proper'(X1), proper'(X2), proper'(X3))
proper'(U55'(X1, X2)) → U55'(proper'(X1), proper'(X2))
proper'(U56'(X)) → U56'(proper'(X))
proper'(U61'(X1, X2)) → U61'(proper'(X1), proper'(X2))
proper'(U62'(X1, X2)) → U62'(proper'(X1), proper'(X2))
proper'(U63'(X)) → U63'(proper'(X))
proper'(U71'(X1, X2, X3)) → U71'(proper'(X1), proper'(X2), proper'(X3))
proper'(U72'(X1, X2)) → U72'(proper'(X1), proper'(X2))
proper'(U73'(X1, X2)) → U73'(proper'(X1), proper'(X2))
proper'(isPal'(X)) → isPal'(proper'(X))
proper'(U74'(X)) → U74'(proper'(X))
proper'(U81'(X1, X2)) → U81'(proper'(X1), proper'(X2))
proper'(U82'(X1, X2)) → U82'(proper'(X1), proper'(X2))
proper'(U83'(X)) → U83'(proper'(X))
proper'(isNePal'(X)) → isNePal'(proper'(X))
proper'(U91'(X1, X2)) → U91'(proper'(X1), proper'(X2))
proper'(U92'(X)) → U92'(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'(X1), ok'(X2)) → ok'(U12'(X1, X2))
isPalListKind'(ok'(X)) → ok'(isPalListKind'(X))
U13'(ok'(X)) → ok'(U13'(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'(X3)) → ok'(U22'(X1, X2, X3))
U23'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U23'(X1, X2, X3))
U24'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U24'(X1, X2, X3))
U25'(ok'(X1), ok'(X2)) → ok'(U25'(X1, X2))
isList'(ok'(X)) → ok'(isList'(X))
U26'(ok'(X)) → ok'(U26'(X))
U31'(ok'(X1), ok'(X2)) → ok'(U31'(X1, X2))
U32'(ok'(X1), ok'(X2)) → ok'(U32'(X1, X2))
U33'(ok'(X)) → ok'(U33'(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'(X3)) → ok'(U42'(X1, X2, X3))
U43'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U43'(X1, X2, X3))
U44'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U44'(X1, X2, X3))
U45'(ok'(X1), ok'(X2)) → ok'(U45'(X1, X2))
U46'(ok'(X)) → ok'(U46'(X))
U51'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U51'(X1, X2, X3))
U52'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U52'(X1, X2, X3))
U53'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U53'(X1, X2, X3))
U54'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U54'(X1, X2, X3))
U55'(ok'(X1), ok'(X2)) → ok'(U55'(X1, X2))
U56'(ok'(X)) → ok'(U56'(X))
U61'(ok'(X1), ok'(X2)) → ok'(U61'(X1, X2))
U62'(ok'(X1), ok'(X2)) → ok'(U62'(X1, X2))
U63'(ok'(X)) → ok'(U63'(X))
U71'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U71'(X1, X2, X3))
U72'(ok'(X1), ok'(X2)) → ok'(U72'(X1, X2))
U73'(ok'(X1), ok'(X2)) → ok'(U73'(X1, X2))
isPal'(ok'(X)) → ok'(isPal'(X))
U74'(ok'(X)) → ok'(U74'(X))
U81'(ok'(X1), ok'(X2)) → ok'(U81'(X1, X2))
U82'(ok'(X1), ok'(X2)) → ok'(U82'(X1, X2))
U83'(ok'(X)) → ok'(U83'(X))
isNePal'(ok'(X)) → ok'(isNePal'(X))
U91'(ok'(X1), ok'(X2)) → ok'(U91'(X1, X2))
U92'(ok'(X)) → ok'(U92'(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'(isPalListKind'(V), V))
active'(U12'(tt', V)) → mark'(U13'(isNeList'(V)))
active'(U13'(tt')) → mark'(tt')
active'(U21'(tt', V1, V2)) → mark'(U22'(isPalListKind'(V1), V1, V2))
active'(U22'(tt', V1, V2)) → mark'(U23'(isPalListKind'(V2), V1, V2))
active'(U23'(tt', V1, V2)) → mark'(U24'(isPalListKind'(V2), V1, V2))
active'(U24'(tt', V1, V2)) → mark'(U25'(isList'(V1), V2))
active'(U25'(tt', V2)) → mark'(U26'(isList'(V2)))
active'(U26'(tt')) → mark'(tt')
active'(U31'(tt', V)) → mark'(U32'(isPalListKind'(V), V))
active'(U32'(tt', V)) → mark'(U33'(isQid'(V)))
active'(U33'(tt')) → mark'(tt')
active'(U41'(tt', V1, V2)) → mark'(U42'(isPalListKind'(V1), V1, V2))
active'(U42'(tt', V1, V2)) → mark'(U43'(isPalListKind'(V2), V1, V2))
active'(U43'(tt', V1, V2)) → mark'(U44'(isPalListKind'(V2), V1, V2))
active'(U44'(tt', V1, V2)) → mark'(U45'(isList'(V1), V2))
active'(U45'(tt', V2)) → mark'(U46'(isNeList'(V2)))
active'(U46'(tt')) → mark'(tt')
active'(U51'(tt', V1, V2)) → mark'(U52'(isPalListKind'(V1), V1, V2))
active'(U52'(tt', V1, V2)) → mark'(U53'(isPalListKind'(V2), V1, V2))
active'(U53'(tt', V1, V2)) → mark'(U54'(isPalListKind'(V2), V1, V2))
active'(U54'(tt', V1, V2)) → mark'(U55'(isNeList'(V1), V2))
active'(U55'(tt', V2)) → mark'(U56'(isList'(V2)))
active'(U56'(tt')) → mark'(tt')
active'(U61'(tt', V)) → mark'(U62'(isPalListKind'(V), V))
active'(U62'(tt', V)) → mark'(U63'(isQid'(V)))
active'(U63'(tt')) → mark'(tt')
active'(U71'(tt', I, P)) → mark'(U72'(isPalListKind'(I), P))
active'(U72'(tt', P)) → mark'(U73'(isPal'(P), P))
active'(U73'(tt', P)) → mark'(U74'(isPalListKind'(P)))
active'(U74'(tt')) → mark'(tt')
active'(U81'(tt', V)) → mark'(U82'(isPalListKind'(V), V))
active'(U82'(tt', V)) → mark'(U83'(isNePal'(V)))
active'(U83'(tt')) → mark'(tt')
active'(U91'(tt', V2)) → mark'(U92'(isPalListKind'(V2)))
active'(U92'(tt')) → mark'(tt')
active'(isList'(V)) → mark'(U11'(isPalListKind'(V), V))
active'(isList'(nil')) → mark'(tt')
active'(isList'(__'(V1, V2))) → mark'(U21'(isPalListKind'(V1), V1, V2))
active'(isNeList'(V)) → mark'(U31'(isPalListKind'(V), V))
active'(isNeList'(__'(V1, V2))) → mark'(U41'(isPalListKind'(V1), V1, V2))
active'(isNeList'(__'(V1, V2))) → mark'(U51'(isPalListKind'(V1), V1, V2))
active'(isNePal'(V)) → mark'(U61'(isPalListKind'(V), V))
active'(isNePal'(__'(I, __'(P, I)))) → mark'(U71'(isQid'(I), I, P))
active'(isPal'(V)) → mark'(U81'(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'(U91'(isPalListKind'(V1), 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'(X1, X2)) → U12'(active'(X1), X2)
active'(U13'(X)) → U13'(active'(X))
active'(U21'(X1, X2, X3)) → U21'(active'(X1), X2, X3)
active'(U22'(X1, X2, X3)) → U22'(active'(X1), X2, X3)
active'(U23'(X1, X2, X3)) → U23'(active'(X1), X2, X3)
active'(U24'(X1, X2, X3)) → U24'(active'(X1), X2, X3)
active'(U25'(X1, X2)) → U25'(active'(X1), X2)
active'(U26'(X)) → U26'(active'(X))
active'(U31'(X1, X2)) → U31'(active'(X1), X2)
active'(U32'(X1, X2)) → U32'(active'(X1), X2)
active'(U33'(X)) → U33'(active'(X))
active'(U41'(X1, X2, X3)) → U41'(active'(X1), X2, X3)
active'(U42'(X1, X2, X3)) → U42'(active'(X1), X2, X3)
active'(U43'(X1, X2, X3)) → U43'(active'(X1), X2, X3)
active'(U44'(X1, X2, X3)) → U44'(active'(X1), X2, X3)
active'(U45'(X1, X2)) → U45'(active'(X1), X2)
active'(U46'(X)) → U46'(active'(X))
active'(U51'(X1, X2, X3)) → U51'(active'(X1), X2, X3)
active'(U52'(X1, X2, X3)) → U52'(active'(X1), X2, X3)
active'(U53'(X1, X2, X3)) → U53'(active'(X1), X2, X3)
active'(U54'(X1, X2, X3)) → U54'(active'(X1), X2, X3)
active'(U55'(X1, X2)) → U55'(active'(X1), X2)
active'(U56'(X)) → U56'(active'(X))
active'(U61'(X1, X2)) → U61'(active'(X1), X2)
active'(U62'(X1, X2)) → U62'(active'(X1), X2)
active'(U63'(X)) → U63'(active'(X))
active'(U71'(X1, X2, X3)) → U71'(active'(X1), X2, X3)
active'(U72'(X1, X2)) → U72'(active'(X1), X2)
active'(U73'(X1, X2)) → U73'(active'(X1), X2)
active'(U74'(X)) → U74'(active'(X))
active'(U81'(X1, X2)) → U81'(active'(X1), X2)
active'(U82'(X1, X2)) → U82'(active'(X1), X2)
active'(U83'(X)) → U83'(active'(X))
active'(U91'(X1, X2)) → U91'(active'(X1), X2)
active'(U92'(X)) → U92'(active'(X))
__'(mark'(X1), X2) → mark'(__'(X1, X2))
__'(X1, mark'(X2)) → mark'(__'(X1, X2))
U11'(mark'(X1), X2) → mark'(U11'(X1, X2))
U12'(mark'(X1), X2) → mark'(U12'(X1, X2))
U13'(mark'(X)) → mark'(U13'(X))
U21'(mark'(X1), X2, X3) → mark'(U21'(X1, X2, X3))
U22'(mark'(X1), X2, X3) → mark'(U22'(X1, X2, X3))
U23'(mark'(X1), X2, X3) → mark'(U23'(X1, X2, X3))
U24'(mark'(X1), X2, X3) → mark'(U24'(X1, X2, X3))
U25'(mark'(X1), X2) → mark'(U25'(X1, X2))
U26'(mark'(X)) → mark'(U26'(X))
U31'(mark'(X1), X2) → mark'(U31'(X1, X2))
U32'(mark'(X1), X2) → mark'(U32'(X1, X2))
U33'(mark'(X)) → mark'(U33'(X))
U41'(mark'(X1), X2, X3) → mark'(U41'(X1, X2, X3))
U42'(mark'(X1), X2, X3) → mark'(U42'(X1, X2, X3))
U43'(mark'(X1), X2, X3) → mark'(U43'(X1, X2, X3))
U44'(mark'(X1), X2, X3) → mark'(U44'(X1, X2, X3))
U45'(mark'(X1), X2) → mark'(U45'(X1, X2))
U46'(mark'(X)) → mark'(U46'(X))
U51'(mark'(X1), X2, X3) → mark'(U51'(X1, X2, X3))
U52'(mark'(X1), X2, X3) → mark'(U52'(X1, X2, X3))
U53'(mark'(X1), X2, X3) → mark'(U53'(X1, X2, X3))
U54'(mark'(X1), X2, X3) → mark'(U54'(X1, X2, X3))
U55'(mark'(X1), X2) → mark'(U55'(X1, X2))
U56'(mark'(X)) → mark'(U56'(X))
U61'(mark'(X1), X2) → mark'(U61'(X1, X2))
U62'(mark'(X1), X2) → mark'(U62'(X1, X2))
U63'(mark'(X)) → mark'(U63'(X))
U71'(mark'(X1), X2, X3) → mark'(U71'(X1, X2, X3))
U72'(mark'(X1), X2) → mark'(U72'(X1, X2))
U73'(mark'(X1), X2) → mark'(U73'(X1, X2))
U74'(mark'(X)) → mark'(U74'(X))
U81'(mark'(X1), X2) → mark'(U81'(X1, X2))
U82'(mark'(X1), X2) → mark'(U82'(X1, X2))
U83'(mark'(X)) → mark'(U83'(X))
U91'(mark'(X1), X2) → mark'(U91'(X1, X2))
U92'(mark'(X)) → mark'(U92'(X))
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'(X1, X2)) → U12'(proper'(X1), proper'(X2))
proper'(isPalListKind'(X)) → isPalListKind'(proper'(X))
proper'(U13'(X)) → U13'(proper'(X))
proper'(isNeList'(X)) → isNeList'(proper'(X))
proper'(U21'(X1, X2, X3)) → U21'(proper'(X1), proper'(X2), proper'(X3))
proper'(U22'(X1, X2, X3)) → U22'(proper'(X1), proper'(X2), proper'(X3))
proper'(U23'(X1, X2, X3)) → U23'(proper'(X1), proper'(X2), proper'(X3))
proper'(U24'(X1, X2, X3)) → U24'(proper'(X1), proper'(X2), proper'(X3))
proper'(U25'(X1, X2)) → U25'(proper'(X1), proper'(X2))
proper'(isList'(X)) → isList'(proper'(X))
proper'(U26'(X)) → U26'(proper'(X))
proper'(U31'(X1, X2)) → U31'(proper'(X1), proper'(X2))
proper'(U32'(X1, X2)) → U32'(proper'(X1), proper'(X2))
proper'(U33'(X)) → U33'(proper'(X))
proper'(isQid'(X)) → isQid'(proper'(X))
proper'(U41'(X1, X2, X3)) → U41'(proper'(X1), proper'(X2), proper'(X3))
proper'(U42'(X1, X2, X3)) → U42'(proper'(X1), proper'(X2), proper'(X3))
proper'(U43'(X1, X2, X3)) → U43'(proper'(X1), proper'(X2), proper'(X3))
proper'(U44'(X1, X2, X3)) → U44'(proper'(X1), proper'(X2), proper'(X3))
proper'(U45'(X1, X2)) → U45'(proper'(X1), proper'(X2))
proper'(U46'(X)) → U46'(proper'(X))
proper'(U51'(X1, X2, X3)) → U51'(proper'(X1), proper'(X2), proper'(X3))
proper'(U52'(X1, X2, X3)) → U52'(proper'(X1), proper'(X2), proper'(X3))
proper'(U53'(X1, X2, X3)) → U53'(proper'(X1), proper'(X2), proper'(X3))
proper'(U54'(X1, X2, X3)) → U54'(proper'(X1), proper'(X2), proper'(X3))
proper'(U55'(X1, X2)) → U55'(proper'(X1), proper'(X2))
proper'(U56'(X)) → U56'(proper'(X))
proper'(U61'(X1, X2)) → U61'(proper'(X1), proper'(X2))
proper'(U62'(X1, X2)) → U62'(proper'(X1), proper'(X2))
proper'(U63'(X)) → U63'(proper'(X))
proper'(U71'(X1, X2, X3)) → U71'(proper'(X1), proper'(X2), proper'(X3))
proper'(U72'(X1, X2)) → U72'(proper'(X1), proper'(X2))
proper'(U73'(X1, X2)) → U73'(proper'(X1), proper'(X2))
proper'(isPal'(X)) → isPal'(proper'(X))
proper'(U74'(X)) → U74'(proper'(X))
proper'(U81'(X1, X2)) → U81'(proper'(X1), proper'(X2))
proper'(U82'(X1, X2)) → U82'(proper'(X1), proper'(X2))
proper'(U83'(X)) → U83'(proper'(X))
proper'(isNePal'(X)) → isNePal'(proper'(X))
proper'(U91'(X1, X2)) → U91'(proper'(X1), proper'(X2))
proper'(U92'(X)) → U92'(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'(X1), ok'(X2)) → ok'(U12'(X1, X2))
isPalListKind'(ok'(X)) → ok'(isPalListKind'(X))
U13'(ok'(X)) → ok'(U13'(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'(X3)) → ok'(U22'(X1, X2, X3))
U23'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U23'(X1, X2, X3))
U24'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U24'(X1, X2, X3))
U25'(ok'(X1), ok'(X2)) → ok'(U25'(X1, X2))
isList'(ok'(X)) → ok'(isList'(X))
U26'(ok'(X)) → ok'(U26'(X))
U31'(ok'(X1), ok'(X2)) → ok'(U31'(X1, X2))
U32'(ok'(X1), ok'(X2)) → ok'(U32'(X1, X2))
U33'(ok'(X)) → ok'(U33'(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'(X3)) → ok'(U42'(X1, X2, X3))
U43'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U43'(X1, X2, X3))
U44'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U44'(X1, X2, X3))
U45'(ok'(X1), ok'(X2)) → ok'(U45'(X1, X2))
U46'(ok'(X)) → ok'(U46'(X))
U51'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U51'(X1, X2, X3))
U52'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U52'(X1, X2, X3))
U53'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U53'(X1, X2, X3))
U54'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U54'(X1, X2, X3))
U55'(ok'(X1), ok'(X2)) → ok'(U55'(X1, X2))
U56'(ok'(X)) → ok'(U56'(X))
U61'(ok'(X1), ok'(X2)) → ok'(U61'(X1, X2))
U62'(ok'(X1), ok'(X2)) → ok'(U62'(X1, X2))
U63'(ok'(X)) → ok'(U63'(X))
U71'(ok'(X1), ok'(X2), ok'(X3)) → ok'(U71'(X1, X2, X3))
U72'(ok'(X1), ok'(X2)) → ok'(U72'(X1, X2))
U73'(ok'(X1), ok'(X2)) → ok'(U73'(X1, X2))
isPal'(ok'(X)) → ok'(isPal'(X))
U74'(ok'(X)) → ok'(U74'(X))
U81'(ok'(X1), ok'(X2)) → ok'(U81'(X1, X2))
U82'(ok'(X1), ok'(X2)) → ok'(U82'(X1, X2))
U83'(ok'(X)) → ok'(U83'(X))
isNePal'(ok'(X)) → ok'(isNePal'(X))
U91'(ok'(X1), ok'(X2)) → ok'(U91'(X1, X2))
U92'(ok'(X)) → ok'(U92'(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' → 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'
U13' :: 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' → 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' → mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U24' :: 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'
U25' :: 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'
U26' :: 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' → mark':nil':tt':a':e':i':o':u':ok'
U33' :: 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' → 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' → mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U44' :: 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'
U45' :: 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'
U46' :: 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' → 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' → mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U54' :: 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'
U55' :: 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'
U56' :: 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' → mark':nil':tt':a':e':i':o':u':ok'
U63' :: 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' → 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' → mark':nil':tt':a':e':i':o':u':ok'
U73' :: 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'
isPal' :: mark':nil':tt':a':e':i':o':u':ok' → mark':nil':tt':a':e':i':o':u':ok'
U74' :: 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' → mark':nil':tt':a':e':i':o':u':ok'
U82' :: 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'
U83' :: 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'
U91' :: 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'
U92' :: 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', isPalListKind', U13', isNeList', U22', U23', U24', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
__' < active'
U12' < active'
isPalListKind' < active'
U13' < active'
isNeList' < active'
U22' < active'
U23' < active'
U24' < active'
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
__' < proper'
U12' < proper'
isPalListKind' < proper'
U13' < proper'
isNeList' < proper'
U22' < proper'
U23' < proper'
U24' < proper'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < 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', isPalListKind', U13', isNeList', U22', U23', U24', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', 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', isPalListKind', U13', isNeList', U22', U23', U24', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U12' < active'
isPalListKind' < active'
U13' < active'
isNeList' < active'
U22' < active'
U23' < active'
U24' < active'
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U12' < proper'
isPalListKind' < proper'
U13' < proper'
isNeList' < proper'
U22' < proper'
U23' < proper'
U24' < proper'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

Induction Base:
U12'(___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:
U12'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n11790, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b12718)) →_R^Ω(1)
mark'(U12'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n11790)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b12718))) →_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', U13', isNeList', U22', U23', U24', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
isPalListKind' < active'
U13' < active'
isNeList' < active'
U22' < active'
U23' < active'
U24' < active'
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
isPalListKind' < proper'
U13' < proper'
isNeList' < proper'
U22' < proper'
U23' < proper'
U24' < proper'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < 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:
U13', active', isNeList', U22', U23', U24', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U13' < active'
isNeList' < active'
U22' < active'
U23' < active'
U24' < active'
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U13' < proper'
isNeList' < proper'
U22' < proper'
U23' < proper'
U24' < proper'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

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

Induction Step:
U13'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n23749, 1)))) →_R^Ω(1)
mark'(U13'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n23749)))) →_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', U23', U24', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
isNeList' < active'
U22' < active'
U23' < active'
U24' < active'
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
isNeList' < proper'
U22' < proper'
U23' < proper'
U24' < proper'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < 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', U23', U24', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U22' < active'
U23' < active'
U24' < active'
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U22' < proper'
U23' < proper'
U24' < proper'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n31697)), ___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 ∈ Ω(_{__n31697})

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

Induction Step:
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n31698, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b34006), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c34007)) →_R^Ω(1)
mark'(U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n31698)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b34006), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c34007))) →_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:
U23', active', U24', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U23' < active'
U24' < active'
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U23' < proper'
U24' < proper'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U23'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n48854)), ___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 ∈ Ω(_{__n48854})

Induction Base:
U23'(___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:
U23'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n48855, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b51811), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c51812)) →_R^Ω(1)
mark'(U23'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n48855)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b51811), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c51812))) →_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:
U24', active', U25', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U24' < active'
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U24' < proper'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U24'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n66743)), ___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 ∈ Ω(_{__n66743})

Induction Base:
U24'(___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:
U24'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n66744, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b70348), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c70349)) →_R^Ω(1)
mark'(U24'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n66744)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b70348), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c70349))) →_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:
U25', active', isList', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U25' < active'
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U25' < proper'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

Induction Base:
U25'(___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:
U25'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n85365, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b88129)) →_R^Ω(1)
mark'(U25'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n85365)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b88129))) →_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', U26', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
isList' < active'
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
isList' < proper'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < 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:
U26', active', U32', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U26' < active'
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U26' < proper'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

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

Induction Step:
U26'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n99476, 1)))) →_R^Ω(1)
mark'(U26'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n99476)))) →_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', U33', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U32' < active'
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U32' < proper'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

Induction Base:
U32'(___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:
U32'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n108482, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b111786)) →_R^Ω(1)
mark'(U32'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n108482)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b111786))) →_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:
U33', active', isQid', U42', U43', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U33' < active'
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U33' < proper'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

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

Induction Step:
U33'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n123118, 1)))) →_R^Ω(1)
mark'(U33'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n123118)))) →_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', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
isQid' < active'
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
isQid' < proper'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < 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', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U42' < active'
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U42' < proper'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n132544)), ___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 ∈ Ω(_{__n132544})

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

Induction Step:
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n132545, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b138417), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c138418)) →_R^Ω(1)
mark'(U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n132545)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b138417), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c138418))) →_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', U44', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U43' < active'
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U43' < proper'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U43'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n153703)), ___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 ∈ Ω(_{__n153703})

Induction Base:
U43'(___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:
U43'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n153704, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b160224), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c160225)) →_R^Ω(1)
mark'(U43'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n153704)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b160224), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c160225))) →_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:
U44', active', U45', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U44' < active'
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U44' < proper'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U44'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n175594)), ___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 ∈ Ω(_{__n175594})

Induction Base:
U44'(___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:
U44'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n175595, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b182763), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c182764)) →_R^Ω(1)
mark'(U44'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n175595)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b182763), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c182764))) →_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:
U45', active', U46', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U45' < active'
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U45' < proper'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

Induction Base:
U45'(___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:
U45'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n198218, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b203358)) →_R^Ω(1)
mark'(U45'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n198218)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b203358))) →_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:
U46', active', U52', U53', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U46' < active'
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U46' < proper'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

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

Induction Step:
U46'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n214948, 1)))) →_R^Ω(1)
mark'(U46'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n214948)))) →_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', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U52' < active'
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U52' < proper'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n225357)), ___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 ∈ Ω(_{__n225357})

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

Induction Step:
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n225358, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b233984), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c233985)) →_R^Ω(1)
mark'(U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n225358)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b233984), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c233985))) →_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', U54', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U53' < active'
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U53' < proper'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U53'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n249615)), ___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 ∈ Ω(_{__n249615})

Induction Base:
U53'(___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:
U53'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n249616, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b258890), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c258891)) →_R^Ω(1)
mark'(U53'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n249616)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b258890), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c258891))) →_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:
U54', active', U55', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U54' < active'
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U54' < proper'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

Proved the following rewrite lemma:
U54'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n274605)), ___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 ∈ Ω(_{__n274605})

Induction Base:
U54'(___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:
U54'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n274606, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b284528), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c284529)) →_R^Ω(1)
mark'(U54'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n274606)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b284528), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c284529))) →_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:
U55', active', U56', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U55' < active'
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U55' < proper'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

Induction Base:
U55'(___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:
U55'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n300328, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b307304)) →_R^Ω(1)
mark'(U55'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n300328)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b307304))) →_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:
U56', active', U62', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U56' < active'
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U56' < proper'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

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

Induction Step:
U56'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n319152, 1)))) →_R^Ω(1)
mark'(U56'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n319152)))) →_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', U63', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U62' < active'
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U62' < proper'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

Induction Base:
U62'(___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:
U62'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n330651, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b338167)) →_R^Ω(1)
mark'(U62'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n330651)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b338167))) →_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:
U63', active', U72', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U63' < active'
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U63' < proper'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

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

Induction Step:
U63'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n350084, 1)))) →_R^Ω(1)
mark'(U63'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n350084)))) →_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', U73', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U72' < active'
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U72' < proper'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

Induction Base:
U72'(___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:
U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n361898, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b369954)) →_R^Ω(1)
mark'(U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n361898)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b369954))) →_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:
U73', active', isPal', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

They will be analysed ascendingly in the following order:
U73' < active'
isPal' < active'
U74' < active'
U82' < active'
U83' < active'
isNePal' < active'
U92' < active'
U11' < active'
U21' < active'
U31' < active'
U41' < active'
U51' < active'
U61' < active'
U71' < active'
U81' < active'
U91' < active'
active' < top'
U73' < proper'
isPal' < proper'
U74' < proper'
U82' < proper'
U83' < proper'
isNePal' < proper'
U92' < proper'
U11' < proper'
U21' < proper'
U31' < proper'
U41' < proper'
U51' < proper'
U61' < proper'
U71' < proper'
U81' < proper'
U91' < proper'
proper' < top'

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

Induction Base:
U73'(___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:
U73'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n381940, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b390320)) →_R^Ω(1)
mark'(U73'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n381940)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b390320))) →_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', U74', U82', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

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

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

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

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

Induction Step:
U74'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n402608, 1)))) →_R^Ω(1)
mark'(U74'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n402608)))) →_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:
U82', active', U83', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

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

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

Induction Base:
U82'(___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:
U82'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n414928, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b423848)) →_R^Ω(1)
mark'(U82'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n414928)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b423848))) →_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:
U83', active', isNePal', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

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

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

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

Induction Step:
U83'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n435947, 1)))) →_R^Ω(1)
mark'(U83'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n435947)))) →_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, ___n11789)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n11789})
U13'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n23748))) → ___*4, rt ∈ Ω(_{__n23748})
U22'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n31697)), ___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 ∈ Ω(_{__n31697})
U23'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n48854)), ___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 ∈ Ω(_{__n48854})
U24'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n66743)), ___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 ∈ Ω(_{__n66743})
U25'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n85364)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n85364})
U26'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n99475))) → ___*4, rt ∈ Ω(_{__n99475})
U32'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n108481)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n108481})
U33'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n123117))) → ___*4, rt ∈ Ω(_{__n123117})
U42'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n132544)), ___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 ∈ Ω(_{__n132544})
U43'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n153703)), ___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 ∈ Ω(_{__n153703})
U44'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n175594)), ___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 ∈ Ω(_{__n175594})
U45'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n198217)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n198217})
U46'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n214947))) → ___*4, rt ∈ Ω(_{__n214947})
U52'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n225357)), ___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 ∈ Ω(_{__n225357})
U53'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n249615)), ___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 ∈ Ω(_{__n249615})
U54'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n274605)), ___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 ∈ Ω(_{__n274605})
U55'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n300327)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n300327})
U56'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n319151))) → ___*4, rt ∈ Ω(_{__n319151})
U62'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n330650)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n330650})
U63'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n350083))) → ___*4, rt ∈ Ω(_{__n350083})
U72'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n361897)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n361897})
U73'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n381939)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n381939})
U74'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n402607))) → ___*4, rt ∈ Ω(_{__n402607})
U82'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n414927)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(b)) → ___*4, rt ∈ Ω(_{__n414927})
U83'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n435946))) → ___*4, rt ∈ Ω(_{__n435946})

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', U92', U11', U21', U31', U41', U51', U61', U71', U81', U91', proper', top'

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

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

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

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

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

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

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

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, +(___$n461621, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b471297)) →_R^Ω(1)
mark'(U11'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n461621)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b471297))) →_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', U41', U51', U61', U71', U81', U91', proper', top'

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

Proved the following rewrite lemma:
U21'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n483489)), ___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 ∈ Ω(_{__n483489})

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

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

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

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, +(___$n515004, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b525436)) →_R^Ω(1)
mark'(U31'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n515004)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b525436))) →_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:
U41', active', U51', U61', U71', U81', U91', proper', top'

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

Proved the following rewrite lemma:
U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n537735)), ___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 ∈ Ω(_{__n537735})

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, +(___$n537736, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b553976), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c553977)) →_R^Ω(1)
mark'(U41'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n537736)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b553976), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___c553977))) →_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', U91', proper', top'

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

Proved the following rewrite lemma:
U51'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n570526)), ___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 ∈ Ω(_{__n570526})

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

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

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

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

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

Proved the following rewrite lemma:
U71'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___n628139)), ___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 ∈ Ω(_{__n628139})

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

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

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

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

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

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

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

Induction Base:
U91'(___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:
U91'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, +(___$n687893, 1))), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b700593)) →_R^Ω(1)
mark'(U91'(___gen_mark':nil':tt':a':e':i':o':u':ok'3(+(1, ___$n687893)), ___gen_mark':nil':tt':a':e':i':o':u':ok'3(___b700593))) →_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'