The rewrite relation of the following TRS is considered.
| U11(tt) | → | snd(splitAt(N,XS)) | (1) |
| U161(tt) | → | cons(N) | (2) |
| U171(tt) | → | head(afterNth(N,XS)) | (3) |
| U181(tt) | → | Y | (4) |
| U191(tt) | → | pair(nil,XS) | (5) |
| U201(tt) | → | U202(splitAt(N,XS)) | (6) |
| U202(pair(YS,ZS)) | → | pair(cons(X),ZS) | (7) |
| U21(tt) | → | X | (8) |
| U211(tt) | → | XS | (9) |
| U221(tt) | → | fst(splitAt(N,XS)) | (10) |
| U31(tt) | → | N | (11) |
| and(tt) | → | X | (12) |
| U101(tt) | → | U102(isNatural) | (13) |
| U102(tt) | → | U103(isLNat) | (14) |
| U103(tt) | → | tt | (15) |
| U111(tt) | → | U112(isLNat) | (16) |
| U112(tt) | → | tt | (17) |
| U121(tt) | → | U122(isNatural) | (18) |
| U122(tt) | → | tt | (19) |
| U131(tt) | → | U132(isNatural) | (20) |
| U132(tt) | → | U133(isLNat) | (21) |
| U133(tt) | → | tt | (22) |
| U141(tt) | → | U142(isLNat) | (23) |
| U142(tt) | → | U143(isLNat) | (24) |
| U143(tt) | → | tt | (25) |
| U151(tt) | → | U152(isNatural) | (26) |
| U152(tt) | → | U153(isLNat) | (27) |
| U153(tt) | → | tt | (28) |
| U41(tt) | → | U42(isNatural) | (29) |
| U42(tt) | → | U43(isLNat) | (30) |
| U43(tt) | → | tt | (31) |
| U51(tt) | → | U52(isNatural) | (32) |
| U52(tt) | → | U53(isLNat) | (33) |
| U53(tt) | → | tt | (34) |
| U61(tt) | → | U62(isPLNat) | (35) |
| U62(tt) | → | tt | (36) |
| U71(tt) | → | U72(isNatural) | (37) |
| U72(tt) | → | tt | (38) |
| U81(tt) | → | U82(isPLNat) | (39) |
| U82(tt) | → | tt | (40) |
| U91(tt) | → | U92(isLNat) | (41) |
| U92(tt) | → | tt | (42) |
| afterNth(N,XS) | → | U11(and(and(isNatural))) | (43) |
| fst(pair(X,Y)) | → | U21(and(and(isLNat))) | (44) |
| head(cons(N)) | → | U31(and(and(isNatural))) | (45) |
| isLNat | → | tt | (46) |
| isLNat | → | U41(and(isNaturalKind)) | (47) |
| isLNat | → | U51(and(isNaturalKind)) | (48) |
| isLNat | → | U61(isPLNatKind) | (49) |
| isLNat | → | U71(isNaturalKind) | (50) |
| isLNat | → | U81(isPLNatKind) | (51) |
| isLNat | → | U91(isLNatKind) | (52) |
| isLNat | → | U101(and(isNaturalKind)) | (53) |
| isLNatKind | → | tt | (54) |
| isLNatKind | → | and(isNaturalKind) | (55) |
| isLNatKind | → | isPLNatKind | (56) |
| isLNatKind | → | isNaturalKind | (57) |
| isLNatKind | → | isLNatKind | (58) |
| isNatural | → | tt | (59) |
| isNatural | → | U111(isLNatKind) | (60) |
| isNatural | → | U121(isNaturalKind) | (61) |
| isNatural | → | U131(and(isNaturalKind)) | (62) |
| isNaturalKind | → | tt | (63) |
| isNaturalKind | → | isLNatKind | (64) |
| isNaturalKind | → | isNaturalKind | (65) |
| isNaturalKind | → | and(isNaturalKind) | (66) |
| isPLNat | → | U141(and(isLNatKind)) | (67) |
| isPLNat | → | U151(and(isNaturalKind)) | (68) |
| isPLNatKind | → | and(isLNatKind) | (69) |
| isPLNatKind | → | and(isNaturalKind) | (70) |
| natsFrom(N) | → | U161(and(isNatural)) | (71) |
| sel(N,XS) | → | U171(and(and(isNatural))) | (72) |
| snd(pair(X,Y)) | → | U181(and(and(isLNat))) | (73) |
| splitAt(0,XS) | → | U191(and(isLNat)) | (74) |
| splitAt(s(N),cons(X)) | → | U201(and(and(isNatural))) | (75) |
| tail(cons(N)) | → | U211(and(and(isNatural))) | (76) |
| take(N,XS) | → | U221(and(and(isNatural))) | (77) |
The TRS violates one of the two variable conditions. Thus, it is not terminating.