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

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isList(V) → a__isNeList(V)
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__and(a__isList(V1), isList(V2))
a__isNeList(V) → a__isQid(V)
a__isNeList(__(V1, V2)) → a__and(a__isList(V1), isNeList(V2))
a__isNeList(__(V1, V2)) → a__and(a__isNeList(V1), isList(V2))
a__isNePal(V) → a__isQid(V)
a__isNePal(__(I, __(P, I))) → a__and(a__isQid(I), isPal(P))
a__isPal(V) → a__isNePal(V)
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isList(X)) → a__isList(X)
mark(isNeList(X)) → a__isNeList(X)
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(isPal(X)) → a__isPal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isList(X) → isList(X)
a__isNeList(X) → isNeList(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)
a__isPal(X) → isPal(X)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

a____'(__'(X, Y), Z) → a____'(mark'(X), a____'(mark'(Y), mark'(Z)))
a____'(X, nil') → mark'(X)
a____'(nil', X) → mark'(X)
a__and'(tt', X) → mark'(X)
a__isList'(V) → a__isNeList'(V)
a__isList'(nil') → tt'
a__isList'(__'(V1, V2)) → a__and'(a__isList'(V1), isList'(V2))
a__isNeList'(V) → a__isQid'(V)
a__isNeList'(__'(V1, V2)) → a__and'(a__isList'(V1), isNeList'(V2))
a__isNeList'(__'(V1, V2)) → a__and'(a__isNeList'(V1), isList'(V2))
a__isNePal'(V) → a__isQid'(V)
a__isNePal'(__'(I, __'(P, I))) → a__and'(a__isQid'(I), isPal'(P))
a__isPal'(V) → a__isNePal'(V)
a__isPal'(nil') → tt'
a__isQid'(a') → tt'
a__isQid'(e') → tt'
a__isQid'(i') → tt'
a__isQid'(o') → tt'
a__isQid'(u') → tt'
mark'(__'(X1, X2)) → a____'(mark'(X1), mark'(X2))
mark'(and'(X1, X2)) → a__and'(mark'(X1), X2)
mark'(isList'(X)) → a__isList'(X)
mark'(isNeList'(X)) → a__isNeList'(X)
mark'(isQid'(X)) → a__isQid'(X)
mark'(isNePal'(X)) → a__isNePal'(X)
mark'(isPal'(X)) → a__isPal'(X)
mark'(nil') → nil'
mark'(tt') → tt'
mark'(a') → a'
mark'(e') → e'
mark'(i') → i'
mark'(o') → o'
mark'(u') → u'
a____'(X1, X2) → __'(X1, X2)
a__and'(X1, X2) → and'(X1, X2)
a__isList'(X) → isList'(X)
a__isNeList'(X) → isNeList'(X)
a__isQid'(X) → isQid'(X)
a__isNePal'(X) → isNePal'(X)
a__isPal'(X) → isPal'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a____'(__'(X, Y), Z) → a____'(mark'(X), a____'(mark'(Y), mark'(Z)))
a____'(X, nil') → mark'(X)
a____'(nil', X) → mark'(X)
a__and'(tt', X) → mark'(X)
a__isList'(V) → a__isNeList'(V)
a__isList'(nil') → tt'
a__isList'(__'(V1, V2)) → a__and'(a__isList'(V1), isList'(V2))
a__isNeList'(V) → a__isQid'(V)
a__isNeList'(__'(V1, V2)) → a__and'(a__isList'(V1), isNeList'(V2))
a__isNeList'(__'(V1, V2)) → a__and'(a__isNeList'(V1), isList'(V2))
a__isNePal'(V) → a__isQid'(V)
a__isNePal'(__'(I, __'(P, I))) → a__and'(a__isQid'(I), isPal'(P))
a__isPal'(V) → a__isNePal'(V)
a__isPal'(nil') → tt'
a__isQid'(a') → tt'
a__isQid'(e') → tt'
a__isQid'(i') → tt'
a__isQid'(o') → tt'
a__isQid'(u') → tt'
mark'(__'(X1, X2)) → a____'(mark'(X1), mark'(X2))
mark'(and'(X1, X2)) → a__and'(mark'(X1), X2)
mark'(isList'(X)) → a__isList'(X)
mark'(isNeList'(X)) → a__isNeList'(X)
mark'(isQid'(X)) → a__isQid'(X)
mark'(isNePal'(X)) → a__isNePal'(X)
mark'(isPal'(X)) → a__isPal'(X)
mark'(nil') → nil'
mark'(tt') → tt'
mark'(a') → a'
mark'(e') → e'
mark'(i') → i'
mark'(o') → o'
mark'(u') → u'
a____'(X1, X2) → __'(X1, X2)
a__and'(X1, X2) → and'(X1, X2)
a__isList'(X) → isList'(X)
a__isNeList'(X) → isNeList'(X)
a__isQid'(X) → isQid'(X)
a__isNePal'(X) → isNePal'(X)
a__isPal'(X) → isPal'(X)

Types:
a____' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
__' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
mark' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
nil' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
a__and' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
tt' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
a__isList' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
a__isNeList' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
isList' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
a__isQid' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
isNeList' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
a__isNePal' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
isPal' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
a__isPal' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
a' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
e' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
i' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
o' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
u' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
and' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
isQid' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
isNePal' :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal' → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
___hole___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'1 :: __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'
___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2 :: Nat → __':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'

Heuristically decided to analyse the following defined symbols:
a____', mark', a__and', a__isList', a__isNeList', a__isNePal', a__isPal'

They will be analysed ascendingly in the following order:
a____' = mark'
a____' = a__and'
a____' = a__isList'
a____' = a__isNeList'
a____' = a__isNePal'
a____' = a__isPal'
mark' = a__and'
mark' = a__isList'
mark' = a__isNeList'
mark' = a__isNePal'
mark' = a__isPal'
a__and' = a__isList'
a__and' = a__isNeList'
a__and' = a__isNePal'
a__and' = a__isPal'
a__isList' = a__isNeList'
a__isList' = a__isNePal'
a__isList' = a__isPal'
a__isNeList' = a__isNePal'
a__isNeList' = a__isPal'
a__isNePal' = a__isPal'

Generator Equations:
___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0) ⇔ nil'
___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(+(x, 1)) ⇔ __'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(x), nil')

The following defined symbols remain to be analysed:
mark', a____', a__and', a__isList', a__isNeList', a__isNePal', a__isPal'

Proved the following rewrite lemma:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___n4)) → ___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), rt ∈ Ω(1 + _{__n4})

Induction Base:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0)) →_R^Ω(1)
nil'

Induction Step:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(+(___$n5, 1))) →_R^Ω(1)
a____'(mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___$n5)), mark'(nil')) →_IH
a____'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), mark'(nil')) →_R^Ω(1)
a____'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), nil') →_R^Ω(1)
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0)) →_R^Ω(1)
nil'

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

The following defined symbols remain to be analysed:
a____', a__and', a__isList', a__isNeList', a__isNePal', a__isPal'

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

The following defined symbols remain to be analysed:
a__and', a__isList', a__isNeList', a__isNePal', a__isPal'

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

The following defined symbols remain to be analysed:
a__isList', a__isNeList', a__isNePal', a__isPal'

Proved the following rewrite lemma:
a__isList'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___n21417)) → tt', rt ∈ Ω(1 + _{__n21417})

Induction Base:
a__isList'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0)) →_R^Ω(1)
tt'

Induction Step:
a__isList'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(+(___$n21418, 1))) →_R^Ω(1)
a__and'(a__isList'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___$n21418)), isList'(nil')) →_IH
a__and'(tt', isList'(nil')) →_R^Ω(1)
mark'(isList'(nil')) →_R^Ω(1)
a__isList'(nil') →_R^Ω(1)
tt'

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

Lemmas:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___n4)) → ___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), rt ∈ Ω(1 + _{__n4})
a__isList'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___n21417)) → tt', rt ∈ Ω(1 + _{__n21417})

The following defined symbols remain to be analysed:
a__isNeList', a____', mark', a__and', a__isNePal', a__isPal'

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

The following defined symbols remain to be analysed:
a__isNePal', a____', mark', a__and', a__isPal'

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

The following defined symbols remain to be analysed:
a__isPal', a____', mark', a__and'

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

The following defined symbols remain to be analysed:
mark', a____', a__and'

Proved the following rewrite lemma:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___n33326)) → ___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), rt ∈ Ω(1 + _{__n33326})

Induction Base:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0)) →_R^Ω(1)
nil'

Induction Step:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(+(___$n33327, 1))) →_R^Ω(1)
a____'(mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___$n33327)), mark'(nil')) →_IH
a____'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), mark'(nil')) →_R^Ω(1)
a____'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), nil') →_R^Ω(1)
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0)) →_R^Ω(1)
nil'

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

Lemmas:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___n33326)) → ___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), rt ∈ Ω(1 + _{__n33326})
a__isList'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___n21417)) → tt', rt ∈ Ω(1 + _{__n21417})

The following defined symbols remain to be analysed:
a____', a__and'

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

The following defined symbols remain to be analysed:
a__and'

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
mark'(___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(___n33326)) → ___gen___':nil':tt':isList':isNeList':isPal':a':e':i':o':u':and':isQid':isNePal'2(0), rt ∈ Ω(1 + _{__n33326})