The rewrite relation of the following TRS is considered.
U12(tt) | → | snd(splitAt(N,XS)) | (1) |
U161(tt) | → | cons(N) | (2) |
U172(tt) | → | head(afterNth(N,XS)) | (3) |
U182(tt) | → | Y | (4) |
U191(tt) | → | pair(nil,XS) | (5) |
U203(tt) | → | U204(splitAt(N,XS)) | (6) |
U204(pair(YS,ZS)) | → | pair(cons(X),ZS) | (7) |
U212(tt) | → | XS | (8) |
U22(tt) | → | X | (9) |
U222(tt) | → | fst(splitAt(N,XS)) | (10) |
U32(tt) | → | N | (11) |
U101(tt) | → | U102(isLNat) | (12) |
U102(tt) | → | tt | (13) |
U11(tt) | → | U12(isLNat) | (14) |
U111(tt) | → | tt | (15) |
U121(tt) | → | tt | (16) |
U131(tt) | → | U132(isLNat) | (17) |
U132(tt) | → | tt | (18) |
U141(tt) | → | U142(isLNat) | (19) |
U142(tt) | → | tt | (20) |
U151(tt) | → | U152(isLNat) | (21) |
U152(tt) | → | tt | (22) |
U171(tt) | → | U172(isLNat) | (23) |
U181(tt) | → | U182(isLNat) | (24) |
U201(tt) | → | U202(isNatural) | (25) |
U202(tt) | → | U203(isLNat) | (26) |
U21(tt) | → | U22(isLNat) | (27) |
U211(tt) | → | U212(isLNat) | (28) |
U221(tt) | → | U222(isLNat) | (29) |
U31(tt) | → | U32(isLNat) | (30) |
U41(tt) | → | U42(isLNat) | (31) |
U42(tt) | → | tt | (32) |
U51(tt) | → | U52(isLNat) | (33) |
U52(tt) | → | tt | (34) |
U61(tt) | → | tt | (35) |
U71(tt) | → | tt | (36) |
U81(tt) | → | tt | (37) |
U91(tt) | → | tt | (38) |
afterNth(N,XS) | → | U11(isNatural) | (39) |
fst(pair(X,Y)) | → | U21(isLNat) | (40) |
head(cons(N)) | → | U31(isNatural) | (41) |
isLNat | → | tt | (42) |
isLNat | → | U41(isNatural) | (43) |
isLNat | → | U51(isNatural) | (44) |
isLNat | → | U61(isPLNat) | (45) |
isLNat | → | U71(isNatural) | (46) |
isLNat | → | U81(isPLNat) | (47) |
isLNat | → | U91(isLNat) | (48) |
isLNat | → | U101(isNatural) | (49) |
isNatural | → | tt | (50) |
isNatural | → | U111(isLNat) | (51) |
isNatural | → | U121(isNatural) | (52) |
isNatural | → | U131(isNatural) | (53) |
isPLNat | → | U141(isLNat) | (54) |
isPLNat | → | U151(isNatural) | (55) |
natsFrom(N) | → | U161(isNatural) | (56) |
sel(N,XS) | → | U171(isNatural) | (57) |
snd(pair(X,Y)) | → | U181(isLNat) | (58) |
splitAt(0,XS) | → | U191(isLNat) | (59) |
splitAt(s(N),cons(X)) | → | U201(isNatural) | (60) |
tail(cons(N)) | → | U211(isNatural) | (61) |
take(N,XS) | → | U221(isNatural) | (62) |
t0 | = | U12(tt) |
→ | snd(splitAt(U12(tt),U12(tt))) | |
= | t1 |