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__U11(tt) → a__U12(tt)
a__U12(tt) → tt
a__isNePal(__(I, __(P, I))) → a__U11(tt)
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U12(X)) → a__U12(mark(X))
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U12(X) → U12(X)
a__isNePal(X) → isNePal(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__U11'(tt') → a__U12'(tt')
a__U12'(tt') → tt'
a__isNePal'(__'(I, __'(P, I))) → a__U11'(tt')
mark'(__'(X1, X2)) → a____'(mark'(X1), mark'(X2))
mark'(U11'(X)) → a__U11'(mark'(X))
mark'(U12'(X)) → a__U12'(mark'(X))
mark'(isNePal'(X)) → a__isNePal'(mark'(X))
mark'(nil') → nil'
mark'(tt') → tt'
a____'(X1, X2) → __'(X1, X2)
a__U11'(X) → U11'(X)
a__U12'(X) → U12'(X)
a__isNePal'(X) → isNePal'(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__U11'(tt') → a__U12'(tt')
a__U12'(tt') → tt'
a__isNePal'(__'(I, __'(P, I))) → a__U11'(tt')
mark'(__'(X1, X2)) → a____'(mark'(X1), mark'(X2))
mark'(U11'(X)) → a__U11'(mark'(X))
mark'(U12'(X)) → a__U12'(mark'(X))
mark'(isNePal'(X)) → a__isNePal'(mark'(X))
mark'(nil') → nil'
mark'(tt') → tt'
a____'(X1, X2) → __'(X1, X2)
a__U11'(X) → U11'(X)
a__U12'(X) → U12'(X)
a__isNePal'(X) → isNePal'(X)

Types:
a____' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
__' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
mark' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
nil' :: __':nil':tt':U11':U12':isNePal'
a__U11' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
tt' :: __':nil':tt':U11':U12':isNePal'
a__U12' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
a__isNePal' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
U11' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
U12' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
isNePal' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
___hole___':nil':tt':U11':U12':isNePal'1 :: __':nil':tt':U11':U12':isNePal'
___gen___':nil':tt':U11':U12':isNePal'2 :: Nat → __':nil':tt':U11':U12':isNePal'

Heuristically decided to analyse the following defined symbols:
a____', mark'

They will be analysed ascendingly in the following order:
a____' = mark'

Rules:
a____'(__'(X, Y), Z) → a____'(mark'(X), a____'(mark'(Y), mark'(Z)))
a____'(X, nil') → mark'(X)
a____'(nil', X) → mark'(X)
a__U11'(tt') → a__U12'(tt')
a__U12'(tt') → tt'
a__isNePal'(__'(I, __'(P, I))) → a__U11'(tt')
mark'(__'(X1, X2)) → a____'(mark'(X1), mark'(X2))
mark'(U11'(X)) → a__U11'(mark'(X))
mark'(U12'(X)) → a__U12'(mark'(X))
mark'(isNePal'(X)) → a__isNePal'(mark'(X))
mark'(nil') → nil'
mark'(tt') → tt'
a____'(X1, X2) → __'(X1, X2)
a__U11'(X) → U11'(X)
a__U12'(X) → U12'(X)
a__isNePal'(X) → isNePal'(X)

Types:
a____' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
__' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
mark' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
nil' :: __':nil':tt':U11':U12':isNePal'
a__U11' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
tt' :: __':nil':tt':U11':U12':isNePal'
a__U12' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
a__isNePal' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
U11' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
U12' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
isNePal' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
___hole___':nil':tt':U11':U12':isNePal'1 :: __':nil':tt':U11':U12':isNePal'
___gen___':nil':tt':U11':U12':isNePal'2 :: Nat → __':nil':tt':U11':U12':isNePal'

Generator Equations:
___gen___':nil':tt':U11':U12':isNePal'2(0) ⇔ nil'
___gen___':nil':tt':U11':U12':isNePal'2(+(x, 1)) ⇔ __'(nil', ___gen___':nil':tt':U11':U12':isNePal'2(x))

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

They will be analysed ascendingly in the following order:
a____' = mark'

Proved the following rewrite lemma:
mark'(___gen___':nil':tt':U11':U12':isNePal'2(___n4)) → ___gen___':nil':tt':U11':U12':isNePal'2(0), rt ∈ Ω(1 + __n4)

Induction Base:
mark'(___gen___':nil':tt':U11':U12':isNePal'2(0)) →RΩ(1)
nil'

Induction Step:
mark'(___gen___':nil':tt':U11':U12':isNePal'2(+(___$n5, 1))) →RΩ(1)
a____'(mark'(nil'), mark'(___gen___':nil':tt':U11':U12':isNePal'2(___$n5))) →RΩ(1)
a____'(nil', mark'(___gen___':nil':tt':U11':U12':isNePal'2(___$n5))) →IH
a____'(nil', ___gen___':nil':tt':U11':U12':isNePal'2(0)) →RΩ(1)
mark'(nil') →RΩ(1)
nil'

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

Rules:
a____'(__'(X, Y), Z) → a____'(mark'(X), a____'(mark'(Y), mark'(Z)))
a____'(X, nil') → mark'(X)
a____'(nil', X) → mark'(X)
a__U11'(tt') → a__U12'(tt')
a__U12'(tt') → tt'
a__isNePal'(__'(I, __'(P, I))) → a__U11'(tt')
mark'(__'(X1, X2)) → a____'(mark'(X1), mark'(X2))
mark'(U11'(X)) → a__U11'(mark'(X))
mark'(U12'(X)) → a__U12'(mark'(X))
mark'(isNePal'(X)) → a__isNePal'(mark'(X))
mark'(nil') → nil'
mark'(tt') → tt'
a____'(X1, X2) → __'(X1, X2)
a__U11'(X) → U11'(X)
a__U12'(X) → U12'(X)
a__isNePal'(X) → isNePal'(X)

Types:
a____' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
__' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
mark' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
nil' :: __':nil':tt':U11':U12':isNePal'
a__U11' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
tt' :: __':nil':tt':U11':U12':isNePal'
a__U12' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
a__isNePal' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
U11' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
U12' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
isNePal' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
___hole___':nil':tt':U11':U12':isNePal'1 :: __':nil':tt':U11':U12':isNePal'
___gen___':nil':tt':U11':U12':isNePal'2 :: Nat → __':nil':tt':U11':U12':isNePal'

Lemmas:
mark'(___gen___':nil':tt':U11':U12':isNePal'2(___n4)) → ___gen___':nil':tt':U11':U12':isNePal'2(0), rt ∈ Ω(1 + __n4)

Generator Equations:
___gen___':nil':tt':U11':U12':isNePal'2(0) ⇔ nil'
___gen___':nil':tt':U11':U12':isNePal'2(+(x, 1)) ⇔ __'(nil', ___gen___':nil':tt':U11':U12':isNePal'2(x))

The following defined symbols remain to be analysed:
a____'

They will be analysed ascendingly in the following order:
a____' = mark'

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

Rules:
a____'(__'(X, Y), Z) → a____'(mark'(X), a____'(mark'(Y), mark'(Z)))
a____'(X, nil') → mark'(X)
a____'(nil', X) → mark'(X)
a__U11'(tt') → a__U12'(tt')
a__U12'(tt') → tt'
a__isNePal'(__'(I, __'(P, I))) → a__U11'(tt')
mark'(__'(X1, X2)) → a____'(mark'(X1), mark'(X2))
mark'(U11'(X)) → a__U11'(mark'(X))
mark'(U12'(X)) → a__U12'(mark'(X))
mark'(isNePal'(X)) → a__isNePal'(mark'(X))
mark'(nil') → nil'
mark'(tt') → tt'
a____'(X1, X2) → __'(X1, X2)
a__U11'(X) → U11'(X)
a__U12'(X) → U12'(X)
a__isNePal'(X) → isNePal'(X)

Types:
a____' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
__' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
mark' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
nil' :: __':nil':tt':U11':U12':isNePal'
a__U11' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
tt' :: __':nil':tt':U11':U12':isNePal'
a__U12' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
a__isNePal' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
U11' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
U12' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
isNePal' :: __':nil':tt':U11':U12':isNePal' → __':nil':tt':U11':U12':isNePal'
___hole___':nil':tt':U11':U12':isNePal'1 :: __':nil':tt':U11':U12':isNePal'
___gen___':nil':tt':U11':U12':isNePal'2 :: Nat → __':nil':tt':U11':U12':isNePal'

Lemmas:
mark'(___gen___':nil':tt':U11':U12':isNePal'2(___n4)) → ___gen___':nil':tt':U11':U12':isNePal'2(0), rt ∈ Ω(1 + __n4)

Generator Equations:
___gen___':nil':tt':U11':U12':isNePal'2(0) ⇔ nil'
___gen___':nil':tt':U11':U12':isNePal'2(+(x, 1)) ⇔ __'(nil', ___gen___':nil':tt':U11':U12':isNePal'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
mark'(___gen___':nil':tt':U11':U12':isNePal'2(___n4)) → ___gen___':nil':tt':U11':U12':isNePal'2(0), rt ∈ Ω(1 + __n4)