The rewrite relation of the following TRS is considered.
zeros | → | cons(0,n__zeros) | (1) |
U11(tt) | → | tt | (2) |
U21(tt) | → | tt | (3) |
U31(tt) | → | tt | (4) |
U41(tt,V2) | → | U42(isNatIList(activate(V2))) | (5) |
U42(tt) | → | tt | (6) |
U51(tt,V2) | → | U52(isNatList(activate(V2))) | (7) |
U52(tt) | → | tt | (8) |
U61(tt,V2) | → | U62(isNatIList(activate(V2))) | (9) |
U62(tt) | → | tt | (10) |
U71(tt,L,N) | → | U72(isNat(activate(N)),activate(L)) | (11) |
U72(tt,L) | → | s(length(activate(L))) | (12) |
U81(tt) | → | nil | (13) |
U91(tt,IL,M,N) | → | U92(isNat(activate(M)),activate(IL),activate(M),activate(N)) | (14) |
U92(tt,IL,M,N) | → | U93(isNat(activate(N)),activate(IL),activate(M),activate(N)) | (15) |
U93(tt,IL,M,N) | → | cons(activate(N),n__take(activate(M),activate(IL))) | (16) |
isNat(n__0) | → | tt | (17) |
isNat(n__length(V1)) | → | U11(isNatList(activate(V1))) | (18) |
isNat(n__s(V1)) | → | U21(isNat(activate(V1))) | (19) |
isNatIList(V) | → | U31(isNatList(activate(V))) | (20) |
isNatIList(n__zeros) | → | tt | (21) |
isNatIList(n__cons(V1,V2)) | → | U41(isNat(activate(V1)),activate(V2)) | (22) |
isNatList(n__nil) | → | tt | (23) |
isNatList(n__cons(V1,V2)) | → | U51(isNat(activate(V1)),activate(V2)) | (24) |
isNatList(n__take(V1,V2)) | → | U61(isNat(activate(V1)),activate(V2)) | (25) |
length(nil) | → | 0 | (26) |
length(cons(N,L)) | → | U71(isNatList(activate(L)),activate(L),N) | (27) |
take(0,IL) | → | U81(isNatIList(IL)) | (28) |
take(s(M),cons(N,IL)) | → | U91(isNatIList(activate(IL)),activate(IL),M,N) | (29) |
zeros | → | n__zeros | (30) |
take(X1,X2) | → | n__take(X1,X2) | (31) |
0 | → | n__0 | (32) |
length(X) | → | n__length(X) | (33) |
s(X) | → | n__s(X) | (34) |
cons(X1,X2) | → | n__cons(X1,X2) | (35) |
nil | → | n__nil | (36) |
activate(n__zeros) | → | zeros | (37) |
activate(n__take(X1,X2)) | → | take(X1,X2) | (38) |
activate(n__0) | → | 0 | (39) |
activate(n__length(X)) | → | length(X) | (40) |
activate(n__s(X)) | → | s(X) | (41) |
activate(n__cons(X1,X2)) | → | cons(X1,X2) | (42) |
activate(n__nil) | → | nil | (43) |
activate(X) | → | X | (44) |
zeros# | → | cons#(0,n__zeros) | (45) |
zeros# | → | 0# | (46) |
U41#(tt,V2) | → | U42#(isNatIList(activate(V2))) | (47) |
U41#(tt,V2) | → | isNatIList#(activate(V2)) | (48) |
U41#(tt,V2) | → | activate#(V2) | (49) |
U51#(tt,V2) | → | U52#(isNatList(activate(V2))) | (50) |
U51#(tt,V2) | → | isNatList#(activate(V2)) | (51) |
U51#(tt,V2) | → | activate#(V2) | (52) |
U61#(tt,V2) | → | U62#(isNatIList(activate(V2))) | (53) |
U61#(tt,V2) | → | isNatIList#(activate(V2)) | (54) |
U61#(tt,V2) | → | activate#(V2) | (55) |
U71#(tt,L,N) | → | U72#(isNat(activate(N)),activate(L)) | (56) |
U71#(tt,L,N) | → | isNat#(activate(N)) | (57) |
U71#(tt,L,N) | → | activate#(N) | (58) |
U71#(tt,L,N) | → | activate#(L) | (59) |
U72#(tt,L) | → | s#(length(activate(L))) | (60) |
U72#(tt,L) | → | length#(activate(L)) | (61) |
U72#(tt,L) | → | activate#(L) | (62) |
U81#(tt) | → | nil# | (63) |
U91#(tt,IL,M,N) | → | U92#(isNat(activate(M)),activate(IL),activate(M),activate(N)) | (64) |
U91#(tt,IL,M,N) | → | isNat#(activate(M)) | (65) |
U91#(tt,IL,M,N) | → | activate#(M) | (66) |
U91#(tt,IL,M,N) | → | activate#(IL) | (67) |
U91#(tt,IL,M,N) | → | activate#(N) | (68) |
U92#(tt,IL,M,N) | → | U93#(isNat(activate(N)),activate(IL),activate(M),activate(N)) | (69) |
U92#(tt,IL,M,N) | → | isNat#(activate(N)) | (70) |
U92#(tt,IL,M,N) | → | activate#(N) | (71) |
U92#(tt,IL,M,N) | → | activate#(IL) | (72) |
U92#(tt,IL,M,N) | → | activate#(M) | (73) |
U93#(tt,IL,M,N) | → | cons#(activate(N),n__take(activate(M),activate(IL))) | (74) |
U93#(tt,IL,M,N) | → | activate#(N) | (75) |
U93#(tt,IL,M,N) | → | activate#(M) | (76) |
U93#(tt,IL,M,N) | → | activate#(IL) | (77) |
isNat#(n__length(V1)) | → | U11#(isNatList(activate(V1))) | (78) |
isNat#(n__length(V1)) | → | isNatList#(activate(V1)) | (79) |
isNat#(n__length(V1)) | → | activate#(V1) | (80) |
isNat#(n__s(V1)) | → | U21#(isNat(activate(V1))) | (81) |
isNat#(n__s(V1)) | → | isNat#(activate(V1)) | (82) |
isNat#(n__s(V1)) | → | activate#(V1) | (83) |
isNatIList#(V) | → | U31#(isNatList(activate(V))) | (84) |
isNatIList#(V) | → | isNatList#(activate(V)) | (85) |
isNatIList#(V) | → | activate#(V) | (86) |
isNatIList#(n__cons(V1,V2)) | → | U41#(isNat(activate(V1)),activate(V2)) | (87) |
isNatIList#(n__cons(V1,V2)) | → | isNat#(activate(V1)) | (88) |
isNatIList#(n__cons(V1,V2)) | → | activate#(V1) | (89) |
isNatIList#(n__cons(V1,V2)) | → | activate#(V2) | (90) |
isNatList#(n__cons(V1,V2)) | → | U51#(isNat(activate(V1)),activate(V2)) | (91) |
isNatList#(n__cons(V1,V2)) | → | isNat#(activate(V1)) | (92) |
isNatList#(n__cons(V1,V2)) | → | activate#(V1) | (93) |
isNatList#(n__cons(V1,V2)) | → | activate#(V2) | (94) |
isNatList#(n__take(V1,V2)) | → | U61#(isNat(activate(V1)),activate(V2)) | (95) |
isNatList#(n__take(V1,V2)) | → | isNat#(activate(V1)) | (96) |
isNatList#(n__take(V1,V2)) | → | activate#(V1) | (97) |
isNatList#(n__take(V1,V2)) | → | activate#(V2) | (98) |
length#(nil) | → | 0# | (99) |
length#(cons(N,L)) | → | U71#(isNatList(activate(L)),activate(L),N) | (100) |
length#(cons(N,L)) | → | isNatList#(activate(L)) | (101) |
length#(cons(N,L)) | → | activate#(L) | (102) |
take#(0,IL) | → | U81#(isNatIList(IL)) | (103) |
take#(0,IL) | → | isNatIList#(IL) | (104) |
take#(s(M),cons(N,IL)) | → | U91#(isNatIList(activate(IL)),activate(IL),M,N) | (105) |
take#(s(M),cons(N,IL)) | → | isNatIList#(activate(IL)) | (106) |
take#(s(M),cons(N,IL)) | → | activate#(IL) | (107) |
activate#(n__zeros) | → | zeros# | (108) |
activate#(n__take(X1,X2)) | → | take#(X1,X2) | (109) |
activate#(n__0) | → | 0# | (110) |
activate#(n__length(X)) | → | length#(X) | (111) |
activate#(n__s(X)) | → | s#(X) | (112) |
activate#(n__cons(X1,X2)) | → | cons#(X1,X2) | (113) |
activate#(n__nil) | → | nil# | (114) |
zeros# | → | cons#(0,n__zeros) | (45) |
zeros# | → | 0# | (46) |
U41#(tt,V2) | → | U42#(isNatIList(activate(V2))) | (47) |
U51#(tt,V2) | → | U52#(isNatList(activate(V2))) | (50) |
U61#(tt,V2) | → | U62#(isNatIList(activate(V2))) | (53) |
U72#(tt,L) | → | s#(length(activate(L))) | (60) |
U81#(tt) | → | nil# | (63) |
U93#(tt,IL,M,N) | → | cons#(activate(N),n__take(activate(M),activate(IL))) | (74) |
isNat#(n__length(V1)) | → | U11#(isNatList(activate(V1))) | (78) |
isNat#(n__s(V1)) | → | U21#(isNat(activate(V1))) | (81) |
isNatIList#(V) | → | U31#(isNatList(activate(V))) | (84) |
length#(nil) | → | 0# | (99) |
take#(0,IL) | → | U81#(isNatIList(IL)) | (103) |
activate#(n__zeros) | → | zeros# | (108) |
activate#(n__0) | → | 0# | (110) |
activate#(n__s(X)) | → | s#(X) | (112) |
activate#(n__cons(X1,X2)) | → | cons#(X1,X2) | (113) |
activate#(n__nil) | → | nil# | (114) |
take#(0,IL) | → | isNatIList#(IL) | (104) |
isNatIList#(V) | → | isNatList#(activate(V)) | (85) |
isNat#(n__length(V1)) | → | isNatList#(activate(V1)) | (79) |
length#(cons(N,L)) | → | isNatList#(activate(L)) | (101) |
isNatList#(n__take(V1,V2)) | → | U61#(isNat(activate(V1)),activate(V2)) | (95) |
isNatIList#(V) | → | activate#(V) | (86) |
isNatIList#(n__cons(V1,V2)) | → | isNat#(activate(V1)) | (88) |
isNat#(n__length(V1)) | → | activate#(V1) | (80) |
isNatIList#(n__cons(V1,V2)) | → | activate#(V1) | (89) |
isNatIList#(n__cons(V1,V2)) | → | activate#(V2) | (90) |
U41#(tt,V2) | → | activate#(V2) | (49) |
U61#(tt,V2) | → | activate#(V2) | (55) |
isNatList#(n__take(V1,V2)) | → | isNat#(activate(V1)) | (96) |
isNatList#(n__take(V1,V2)) | → | activate#(V1) | (97) |
isNatList#(n__take(V1,V2)) | → | activate#(V2) | (98) |
length#(cons(N,L)) | → | activate#(L) | (102) |
U72#(tt,L) | → | activate#(L) | (62) |
U71#(tt,L,N) | → | isNat#(activate(N)) | (57) |
U71#(tt,L,N) | → | activate#(N) | (58) |
U71#(tt,L,N) | → | activate#(L) | (59) |
take#(s(M),cons(N,IL)) | → | U91#(isNatIList(activate(IL)),activate(IL),M,N) | (105) |
take#(s(M),cons(N,IL)) | → | isNatIList#(activate(IL)) | (106) |
take#(s(M),cons(N,IL)) | → | activate#(IL) | (107) |
activate#(n__take(X1,X2)) | → | take#(X1,X2) | (109) |
isNatList#(n__cons(V1,V2)) | → | U51#(isNat(activate(V1)),activate(V2)) | (91) |
U51#(tt,V2) | → | isNatList#(activate(V2)) | (51) |
isNatList#(n__cons(V1,V2)) | → | isNat#(activate(V1)) | (92) |
isNatList#(n__cons(V1,V2)) | → | activate#(V1) | (93) |
activate#(n__length(X)) | → | length#(X) | (111) |
length#(cons(N,L)) | → | U71#(isNatList(activate(L)),activate(L),N) | (100) |
U71#(tt,L,N) | → | U72#(isNat(activate(N)),activate(L)) | (56) |
U72#(tt,L) | → | length#(activate(L)) | (61) |
isNatList#(n__cons(V1,V2)) | → | activate#(V2) | (94) |
U61#(tt,V2) | → | isNatIList#(activate(V2)) | (54) |
isNat#(n__s(V1)) | → | isNat#(activate(V1)) | (82) |
isNat#(n__s(V1)) | → | activate#(V1) | (83) |
U51#(tt,V2) | → | activate#(V2) | (52) |
U91#(tt,IL,M,N) | → | U92#(isNat(activate(M)),activate(IL),activate(M),activate(N)) | (64) |
U92#(tt,IL,M,N) | → | U93#(isNat(activate(N)),activate(IL),activate(M),activate(N)) | (69) |
U93#(tt,IL,M,N) | → | activate#(N) | (75) |
U93#(tt,IL,M,N) | → | activate#(M) | (76) |
U93#(tt,IL,M,N) | → | activate#(IL) | (77) |
U92#(tt,IL,M,N) | → | isNat#(activate(N)) | (70) |
U92#(tt,IL,M,N) | → | activate#(N) | (71) |
U92#(tt,IL,M,N) | → | activate#(IL) | (72) |
U92#(tt,IL,M,N) | → | activate#(M) | (73) |
U91#(tt,IL,M,N) | → | isNat#(activate(M)) | (65) |
U91#(tt,IL,M,N) | → | activate#(M) | (66) |
U91#(tt,IL,M,N) | → | activate#(IL) | (67) |
U91#(tt,IL,M,N) | → | activate#(N) | (68) |
U41#(tt,n__zeros) | → | isNatIList#(zeros) | (115) |
U41#(tt,n__take(x0,x1)) | → | isNatIList#(take(x0,x1)) | (116) |
U41#(tt,n__0) | → | isNatIList#(0) | (117) |
U41#(tt,n__length(x0)) | → | isNatIList#(length(x0)) | (118) |
U41#(tt,n__s(x0)) | → | isNatIList#(s(x0)) | (119) |
U41#(tt,n__cons(x0,x1)) | → | isNatIList#(cons(x0,x1)) | (120) |
U41#(tt,n__nil) | → | isNatIList#(nil) | (121) |
U41#(tt,x0) | → | isNatIList#(x0) | (122) |
isNatIList#(n__cons(n__zeros,y1)) | → | U41#(isNat(zeros),activate(y1)) | (123) |
isNatIList#(n__cons(n__take(x0,x1),y1)) | → | U41#(isNat(take(x0,x1)),activate(y1)) | (124) |
isNatIList#(n__cons(n__0,y1)) | → | U41#(isNat(0),activate(y1)) | (125) |
isNatIList#(n__cons(n__length(x0),y1)) | → | U41#(isNat(length(x0)),activate(y1)) | (126) |
isNatIList#(n__cons(n__s(x0),y1)) | → | U41#(isNat(s(x0)),activate(y1)) | (127) |
isNatIList#(n__cons(n__cons(x0,x1),y1)) | → | U41#(isNat(cons(x0,x1)),activate(y1)) | (128) |
isNatIList#(n__cons(n__nil,y1)) | → | U41#(isNat(nil),activate(y1)) | (129) |
isNatIList#(n__cons(x0,y1)) | → | U41#(isNat(x0),activate(y1)) | (130) |
U41#(tt,n__zeros) | → | isNatIList#(cons(0,n__zeros)) | (131) |
U41#(tt,n__zeros) | → | isNatIList#(n__zeros) | (132) |
U41#(tt,n__zeros) | → | isNatIList#(n__zeros) | (132) |
isNatIList#(n__cons(n__zeros,y0)) | → | U41#(isNat(cons(0,n__zeros)),activate(y0)) | (133) |
isNatIList#(n__cons(n__zeros,y0)) | → | U41#(isNat(n__zeros),activate(y0)) | (134) |
isNatIList#(n__cons(n__zeros,y0)) | → | U41#(isNat(n__zeros),activate(y0)) | (134) |
isNatIList#(n__cons(n__0,y0)) | → | U41#(isNat(n__0),activate(y0)) | (135) |
U41#(tt,n__0) | → | isNatIList#(n__0) | (136) |
U41#(tt,n__0) | → | isNatIList#(n__0) | (136) |
U41#(tt,n__s(x0)) | → | isNatIList#(n__s(x0)) | (137) |
U41#(tt,n__s(x0)) | → | isNatIList#(n__s(x0)) | (137) |
isNatIList#(n__cons(n__s(x0),y1)) | → | U41#(isNat(n__s(x0)),activate(y1)) | (138) |
U41#(tt,n__cons(x0,x1)) | → | isNatIList#(n__cons(x0,x1)) | (139) |
isNatIList#(n__cons(n__cons(x0,x1),y2)) | → | U41#(isNat(n__cons(x0,x1)),activate(y2)) | (140) |
isNatIList#(n__cons(n__cons(x0,x1),y2)) | → | U41#(isNat(n__cons(x0,x1)),activate(y2)) | (140) |
U41#(tt,n__nil) | → | isNatIList#(n__nil) | (141) |
U41#(tt,n__nil) | → | isNatIList#(n__nil) | (141) |
isNatIList#(n__cons(n__nil,y0)) | → | U41#(isNat(n__nil),activate(y0)) | (142) |
isNatIList#(n__cons(n__nil,y0)) | → | U41#(isNat(n__nil),activate(y0)) | (142) |
U41#(tt,n__zeros) | → | isNatIList#(n__cons(0,n__zeros)) | (143) |
U41#(tt,n__zeros) | → | isNatIList#(cons(n__0,n__zeros)) | (144) |
isNatIList#(n__cons(n__zeros,y0)) | → | U41#(isNat(n__cons(0,n__zeros)),activate(y0)) | (145) |
isNatIList#(n__cons(n__zeros,y0)) | → | U41#(isNat(cons(n__0,n__zeros)),activate(y0)) | (146) |
isNatIList#(n__cons(n__zeros,y0)) | → | U41#(isNat(n__cons(0,n__zeros)),activate(y0)) | (145) |
isNatIList#(n__cons(n__zeros,y0)) | → | U41#(isNat(n__cons(n__0,n__zeros)),activate(y0)) | (147) |
isNatIList#(n__cons(n__zeros,y0)) | → | U41#(isNat(n__cons(n__0,n__zeros)),activate(y0)) | (147) |
U41#(tt,n__zeros) | → | isNatIList#(n__cons(n__0,n__zeros)) | (148) |
U41#(tt,n__length(x0)) | → | isNatIList#(length(x0)) | (118) |
isNatIList#(n__cons(n__take(x0,x1),y1)) | → | U41#(isNat(take(x0,x1)),activate(y1)) | (124) |
isNatIList#(n__cons(n__length(x0),y1)) | → | U41#(isNat(length(x0)),activate(y1)) | (126) |
isNatIList#(n__cons(n__s(x0),y1)) | → | U41#(isNat(n__s(x0)),activate(y1)) | (138) |
U41#(tt,n__take(x0,x1)) | → | isNatIList#(take(x0,x1)) | (116) |
t0 | = | U41#(isNat(n__0),activate(n__zeros)) |
→R | U41#(isNat(n__0),n__zeros) | |
→R | U41#(tt,n__zeros) | |
→P | isNatIList#(n__cons(n__0,n__zeros)) | |
→P | U41#(isNat(n__0),activate(n__zeros)) | |
= | t4 |