The rewrite relation of the following TRS is considered.
zeros# |
→ |
cons#(0,n__zeros) |
(33) |
zeros# |
→ |
0# |
(34) |
U11#(tt,L) |
→ |
s#(length(activate(L))) |
(35) |
U11#(tt,L) |
→ |
length#(activate(L)) |
(36) |
U11#(tt,L) |
→ |
activate#(L) |
(37) |
and#(tt,X) |
→ |
activate#(X) |
(38) |
isNat#(n__s(V1)) |
→ |
isNat#(activate(V1)) |
(39) |
isNat#(n__s(V1)) |
→ |
activate#(V1) |
(40) |
isNatIList#(n__cons(V1,V2)) |
→ |
and#(isNat(activate(V1)),n__isNatIList(activate(V2))) |
(41) |
isNatIList#(n__cons(V1,V2)) |
→ |
isNat#(activate(V1)) |
(42) |
isNatIList#(n__cons(V1,V2)) |
→ |
activate#(V1) |
(43) |
isNatIList#(n__cons(V1,V2)) |
→ |
activate#(V2) |
(44) |
isNatList#(n__cons(V1,V2)) |
→ |
and#(isNat(activate(V1)),n__isNatList(activate(V2))) |
(45) |
isNatList#(n__cons(V1,V2)) |
→ |
isNat#(activate(V1)) |
(46) |
isNatList#(n__cons(V1,V2)) |
→ |
activate#(V1) |
(47) |
isNatList#(n__cons(V1,V2)) |
→ |
activate#(V2) |
(48) |
length#(cons(N,L)) |
→ |
U11#(and(isNatList(activate(L)),n__isNat(N)),activate(L)) |
(49) |
length#(cons(N,L)) |
→ |
and#(isNatList(activate(L)),n__isNat(N)) |
(50) |
length#(cons(N,L)) |
→ |
isNatList#(activate(L)) |
(51) |
length#(cons(N,L)) |
→ |
activate#(L) |
(52) |
activate#(n__zeros) |
→ |
zeros# |
(53) |
activate#(n__0) |
→ |
0# |
(54) |
activate#(n__length(X)) |
→ |
length#(X) |
(55) |
activate#(n__s(X)) |
→ |
s#(X) |
(56) |
activate#(n__cons(X1,X2)) |
→ |
cons#(X1,X2) |
(57) |
activate#(n__isNatIList(X)) |
→ |
isNatIList#(X) |
(58) |
activate#(n__nil) |
→ |
nil# |
(59) |
activate#(n__isNatList(X)) |
→ |
isNatList#(X) |
(60) |
activate#(n__isNat(X)) |
→ |
isNat#(X) |
(61) |
It remains to prove infiniteness of the resulting DP problem.
isNatIList#(n__cons(y0,y1)) |
→ |
and#(n__isNat(activate(y0)),n__isNatIList(activate(y1))) |
(62) |
isNatIList#(n__cons(n__zeros,y1)) |
→ |
and#(isNat(zeros),n__isNatIList(activate(y1))) |
(63) |
isNatIList#(n__cons(n__0,y1)) |
→ |
and#(isNat(0),n__isNatIList(activate(y1))) |
(64) |
isNatIList#(n__cons(n__length(x0),y1)) |
→ |
and#(isNat(length(x0)),n__isNatIList(activate(y1))) |
(65) |
isNatIList#(n__cons(n__s(x0),y1)) |
→ |
and#(isNat(s(x0)),n__isNatIList(activate(y1))) |
(66) |
isNatIList#(n__cons(n__cons(x0,x1),y1)) |
→ |
and#(isNat(cons(x0,x1)),n__isNatIList(activate(y1))) |
(67) |
isNatIList#(n__cons(n__isNatIList(x0),y1)) |
→ |
and#(isNat(isNatIList(x0)),n__isNatIList(activate(y1))) |
(68) |
isNatIList#(n__cons(n__nil,y1)) |
→ |
and#(isNat(nil),n__isNatIList(activate(y1))) |
(69) |
isNatIList#(n__cons(n__isNatList(x0),y1)) |
→ |
and#(isNat(isNatList(x0)),n__isNatIList(activate(y1))) |
(70) |
isNatIList#(n__cons(n__isNat(x0),y1)) |
→ |
and#(isNat(isNat(x0)),n__isNatIList(activate(y1))) |
(71) |
isNatIList#(n__cons(x0,y1)) |
→ |
and#(isNat(x0),n__isNatIList(activate(y1))) |
(72) |
isNatList#(n__cons(y0,y1)) |
→ |
and#(n__isNat(activate(y0)),n__isNatList(activate(y1))) |
(73) |
isNatList#(n__cons(n__zeros,y1)) |
→ |
and#(isNat(zeros),n__isNatList(activate(y1))) |
(74) |
isNatList#(n__cons(n__0,y1)) |
→ |
and#(isNat(0),n__isNatList(activate(y1))) |
(75) |
isNatList#(n__cons(n__length(x0),y1)) |
→ |
and#(isNat(length(x0)),n__isNatList(activate(y1))) |
(76) |
isNatList#(n__cons(n__s(x0),y1)) |
→ |
and#(isNat(s(x0)),n__isNatList(activate(y1))) |
(77) |
isNatList#(n__cons(n__cons(x0,x1),y1)) |
→ |
and#(isNat(cons(x0,x1)),n__isNatList(activate(y1))) |
(78) |
isNatList#(n__cons(n__isNatIList(x0),y1)) |
→ |
and#(isNat(isNatIList(x0)),n__isNatList(activate(y1))) |
(79) |
isNatList#(n__cons(n__nil,y1)) |
→ |
and#(isNat(nil),n__isNatList(activate(y1))) |
(80) |
isNatList#(n__cons(n__isNatList(x0),y1)) |
→ |
and#(isNat(isNatList(x0)),n__isNatList(activate(y1))) |
(81) |
isNatList#(n__cons(n__isNat(x0),y1)) |
→ |
and#(isNat(isNat(x0)),n__isNatList(activate(y1))) |
(82) |
isNatList#(n__cons(x0,y1)) |
→ |
and#(isNat(x0),n__isNatList(activate(y1))) |
(83) |
isNatIList#(n__cons(n__zeros,y1)) |
→ |
and#(isNat(zeros),n__isNatIList(activate(y1))) |
(63) |
activate#(n__isNatIList(X)) |
→ |
isNatIList#(X) |
(58) |
isNatIList#(n__cons(n__0,y1)) |
→ |
and#(isNat(0),n__isNatIList(activate(y1))) |
(64) |
isNatIList#(n__cons(n__length(x0),y1)) |
→ |
and#(isNat(length(x0)),n__isNatIList(activate(y1))) |
(65) |
isNatIList#(n__cons(n__s(x0),y1)) |
→ |
and#(isNat(s(x0)),n__isNatIList(activate(y1))) |
(66) |
isNatIList#(n__cons(n__cons(x0,x1),y1)) |
→ |
and#(isNat(cons(x0,x1)),n__isNatIList(activate(y1))) |
(67) |
isNatIList#(n__cons(n__isNatIList(x0),y1)) |
→ |
and#(isNat(isNatIList(x0)),n__isNatIList(activate(y1))) |
(68) |
isNatIList#(n__cons(n__nil,y1)) |
→ |
and#(isNat(nil),n__isNatIList(activate(y1))) |
(69) |
isNatIList#(n__cons(n__isNatList(x0),y1)) |
→ |
and#(isNat(isNatList(x0)),n__isNatIList(activate(y1))) |
(70) |
isNatIList#(n__cons(n__isNat(x0),y1)) |
→ |
and#(isNat(isNat(x0)),n__isNatIList(activate(y1))) |
(71) |
isNatIList#(n__cons(x0,y1)) |
→ |
and#(isNat(x0),n__isNatIList(activate(y1))) |
(72) |
activate#(n__isNatList(X)) |
→ |
isNatList#(X) |
(60) |
isNatList#(n__cons(n__zeros,y1)) |
→ |
and#(isNat(zeros),n__isNatList(activate(y1))) |
(74) |
isNatList#(n__cons(n__0,y1)) |
→ |
and#(isNat(0),n__isNatList(activate(y1))) |
(75) |
isNatList#(n__cons(n__length(x0),y1)) |
→ |
and#(isNat(length(x0)),n__isNatList(activate(y1))) |
(76) |
isNatList#(n__cons(n__s(x0),y1)) |
→ |
and#(isNat(s(x0)),n__isNatList(activate(y1))) |
(77) |
isNatList#(n__cons(n__cons(x0,x1),y1)) |
→ |
and#(isNat(cons(x0,x1)),n__isNatList(activate(y1))) |
(78) |
isNatList#(n__cons(n__isNatIList(x0),y1)) |
→ |
and#(isNat(isNatIList(x0)),n__isNatList(activate(y1))) |
(79) |
isNatList#(n__cons(n__nil,y1)) |
→ |
and#(isNat(nil),n__isNatList(activate(y1))) |
(80) |
isNatList#(n__cons(n__isNatList(x0),y1)) |
→ |
and#(isNat(isNatList(x0)),n__isNatList(activate(y1))) |
(81) |
isNatList#(n__cons(n__isNat(x0),y1)) |
→ |
and#(isNat(isNat(x0)),n__isNatList(activate(y1))) |
(82) |
isNatList#(n__cons(x0,y1)) |
→ |
and#(isNat(x0),n__isNatList(activate(y1))) |
(83) |
and#(tt,n__isNatIList(y_3)) |
→ |
activate#(n__isNatIList(y_3)) |
(84) |
and#(tt,n__isNatList(y_3)) |
→ |
activate#(n__isNatList(y_3)) |
(85) |
isNatIList#(n__cons(n__zeros,y1)) |
→ |
and#(isNat(zeros),n__isNatIList(activate(y1))) |
(63) |
activate#(n__isNatIList(X)) |
→ |
isNatIList#(X) |
(58) |
isNatIList#(n__cons(n__0,y1)) |
→ |
and#(isNat(0),n__isNatIList(activate(y1))) |
(64) |
isNatIList#(n__cons(n__length(x0),y1)) |
→ |
and#(isNat(length(x0)),n__isNatIList(activate(y1))) |
(65) |
isNatIList#(n__cons(n__s(x0),y1)) |
→ |
and#(isNat(s(x0)),n__isNatIList(activate(y1))) |
(66) |
isNatIList#(n__cons(n__cons(x0,x1),y1)) |
→ |
and#(isNat(cons(x0,x1)),n__isNatIList(activate(y1))) |
(67) |
isNatIList#(n__cons(n__isNatIList(x0),y1)) |
→ |
and#(isNat(isNatIList(x0)),n__isNatIList(activate(y1))) |
(68) |
isNatIList#(n__cons(n__nil,y1)) |
→ |
and#(isNat(nil),n__isNatIList(activate(y1))) |
(69) |
isNatIList#(n__cons(n__isNatList(x0),y1)) |
→ |
and#(isNat(isNatList(x0)),n__isNatIList(activate(y1))) |
(70) |
isNatIList#(n__cons(n__isNat(x0),y1)) |
→ |
and#(isNat(isNat(x0)),n__isNatIList(activate(y1))) |
(71) |
isNatIList#(n__cons(x0,y1)) |
→ |
and#(isNat(x0),n__isNatIList(activate(y1))) |
(72) |
and#(tt,n__isNatIList(y_3)) |
→ |
activate#(n__isNatIList(y_3)) |
(84) |
and the following rules have been deleted.