Innermost Termination of the following Term Rewriting System could be disproven:

Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:

U101(tt) → fst(splitAt(N, XS))
U11(tt) → snd(splitAt(N, XS))
U21(tt) → X
U31(tt) → N
U41(tt) → cons(N)
U51(tt) → head(afterNth(N, XS))
U61(tt) → Y
U71(tt) → pair(nil, XS)
U81(tt) → U82(splitAt(N, XS))
U82(pair(YS, ZS)) → pair(cons(X), ZS)
U91(tt) → XS
and(tt) → X
afterNth(N, XS) → U11(and(isNatural))
fst(pair(X, Y)) → U21(and(isLNat))
head(cons(N)) → U31(and(isNatural))
isLNat → tt
isLNat → and(isNatural)
isLNat → isPLNat
isLNat → isNatural
isLNat → isLNat
isNatural → tt
isNatural → isLNat
isNatural → isNatural
isNatural → and(isNatural)
isPLNat → and(isLNat)
isPLNat → and(isNatural)
natsFrom(N) → U41(isNatural)
sel(N, XS) → U51(and(isNatural))
snd(pair(X, Y)) → U61(and(isLNat))
splitAt(0, XS) → U71(isLNat)
splitAt(s(N), cons(X)) → U81(and(isNatural))
tail(cons(N)) → U91(and(isNatural))
take(N, XS) → U101(and(isNatural))

Innermost Strategy.


↳ GTRS
  ↳ CritRuleProof

Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:

U101(tt) → fst(splitAt(N, XS))
U11(tt) → snd(splitAt(N, XS))
U21(tt) → X
U31(tt) → N
U41(tt) → cons(N)
U51(tt) → head(afterNth(N, XS))
U61(tt) → Y
U71(tt) → pair(nil, XS)
U81(tt) → U82(splitAt(N, XS))
U82(pair(YS, ZS)) → pair(cons(X), ZS)
U91(tt) → XS
and(tt) → X
afterNth(N, XS) → U11(and(isNatural))
fst(pair(X, Y)) → U21(and(isLNat))
head(cons(N)) → U31(and(isNatural))
isLNat → tt
isLNat → and(isNatural)
isLNat → isPLNat
isLNat → isNatural
isLNat → isLNat
isNatural → tt
isNatural → isLNat
isNatural → isNatural
isNatural → and(isNatural)
isPLNat → and(isLNat)
isPLNat → and(isNatural)
natsFrom(N) → U41(isNatural)
sel(N, XS) → U51(and(isNatural))
snd(pair(X, Y)) → U61(and(isLNat))
splitAt(0, XS) → U71(isLNat)
splitAt(s(N), cons(X)) → U81(and(isNatural))
tail(cons(N)) → U91(and(isNatural))
take(N, XS) → U101(and(isNatural))

Innermost Strategy.

The rule U101(tt) → fst(splitAt(N, XS)) contains free variables in its right-hand side. Hence the TRS is not-terminating.