MAYBE Problem: zeros() -> cons(0(),n__zeros()) U11(tt(),V1) -> U12(isNatIListKind(activate(V1)),activate(V1)) U12(tt(),V1) -> U13(isNatList(activate(V1))) U13(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V) -> U32(isNatIListKind(activate(V)),activate(V)) U32(tt(),V) -> U33(isNatList(activate(V))) U33(tt()) -> tt() U41(tt(),V1,V2) -> U42(isNatKind(activate(V1)),activate(V1),activate(V2)) U42(tt(),V1,V2) -> U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43(tt(),V1,V2) -> U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44(tt(),V1,V2) -> U45(isNat(activate(V1)),activate(V2)) U45(tt(),V2) -> U46(isNatIList(activate(V2))) U46(tt()) -> tt() U51(tt(),V2) -> U52(isNatIListKind(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt()) -> tt() U81(tt(),V1,V2) -> U82(isNatKind(activate(V1)),activate(V1),activate(V2)) U82(tt(),V1,V2) -> U83(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83(tt(),V1,V2) -> U84(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84(tt(),V1,V2) -> U85(isNat(activate(V1)),activate(V2)) U85(tt(),V2) -> U86(isNatList(activate(V2))) U86(tt()) -> tt() U91(tt(),L,N) -> U92(isNatIListKind(activate(L)),activate(L),activate(N)) U92(tt(),L,N) -> U93(isNat(activate(N)),activate(L),activate(N)) U93(tt(),L,N) -> U94(isNatKind(activate(N)),activate(L)) U94(tt(),L) -> s(length(activate(L))) isNat(n__0()) -> tt() isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind(n__nil()) -> tt() isNatIListKind(n__zeros()) -> tt() isNatIListKind(n__cons(V1,V2)) -> U51(isNatKind(activate(V1)),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__length(V1)) -> U61(isNatIListKind(activate(V1))) isNatKind(n__s(V1)) -> U71(isNatKind(activate(V1))) isNatList(n__nil()) -> tt() isNatList(n__cons(V1,V2)) -> U81(isNatKind(activate(V1)),activate(V1),activate(V2)) length(nil()) -> 0() length(cons(N,L)) -> U91(isNatList(activate(L)),activate(L),N) zeros() -> n__zeros() 0() -> n__0() length(X) -> n__length(X) s(X) -> n__s(X) cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() activate(n__zeros()) -> zeros() activate(n__0()) -> 0() activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(X) -> X Proof: DP Processor: DPs: zeros#() -> 0#() zeros#() -> cons#(0(),n__zeros()) U11#(tt(),V1) -> activate#(V1) U11#(tt(),V1) -> isNatIListKind#(activate(V1)) U11#(tt(),V1) -> U12#(isNatIListKind(activate(V1)),activate(V1)) U12#(tt(),V1) -> activate#(V1) U12#(tt(),V1) -> isNatList#(activate(V1)) U12#(tt(),V1) -> U13#(isNatList(activate(V1))) U21#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) U22#(tt(),V1) -> U23#(isNat(activate(V1))) U31#(tt(),V) -> activate#(V) U31#(tt(),V) -> isNatIListKind#(activate(V)) U31#(tt(),V) -> U32#(isNatIListKind(activate(V)),activate(V)) U32#(tt(),V) -> activate#(V) U32#(tt(),V) -> isNatList#(activate(V)) U32#(tt(),V) -> U33#(isNatList(activate(V))) U41#(tt(),V1,V2) -> activate#(V2) U41#(tt(),V1,V2) -> activate#(V1) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) U42#(tt(),V1,V2) -> activate#(V1) U42#(tt(),V1,V2) -> activate#(V2) U42#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43#(tt(),V1,V2) -> activate#(V1) U43#(tt(),V1,V2) -> activate#(V2) U43#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44#(tt(),V1,V2) -> activate#(V2) U44#(tt(),V1,V2) -> activate#(V1) U44#(tt(),V1,V2) -> isNat#(activate(V1)) U44#(tt(),V1,V2) -> U45#(isNat(activate(V1)),activate(V2)) U45#(tt(),V2) -> activate#(V2) U45#(tt(),V2) -> isNatIList#(activate(V2)) U45#(tt(),V2) -> U46#(isNatIList(activate(V2))) U51#(tt(),V2) -> activate#(V2) U51#(tt(),V2) -> isNatIListKind#(activate(V2)) U51#(tt(),V2) -> U52#(isNatIListKind(activate(V2))) U81#(tt(),V1,V2) -> activate#(V2) U81#(tt(),V1,V2) -> activate#(V1) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) U82#(tt(),V1,V2) -> activate#(V1) U82#(tt(),V1,V2) -> activate#(V2) U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83#(tt(),V1,V2) -> activate#(V1) U83#(tt(),V1,V2) -> activate#(V2) U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84#(tt(),V1,V2) -> activate#(V2) U84#(tt(),V1,V2) -> activate#(V1) U84#(tt(),V1,V2) -> isNat#(activate(V1)) U84#(tt(),V1,V2) -> U85#(isNat(activate(V1)),activate(V2)) U85#(tt(),V2) -> activate#(V2) U85#(tt(),V2) -> isNatList#(activate(V2)) U85#(tt(),V2) -> U86#(isNatList(activate(V2))) U91#(tt(),L,N) -> activate#(N) U91#(tt(),L,N) -> activate#(L) U91#(tt(),L,N) -> isNatIListKind#(activate(L)) U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) U92#(tt(),L,N) -> activate#(L) U92#(tt(),L,N) -> activate#(N) U92#(tt(),L,N) -> isNat#(activate(N)) U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) U93#(tt(),L,N) -> activate#(L) U93#(tt(),L,N) -> activate#(N) U93#(tt(),L,N) -> isNatKind#(activate(N)) U93#(tt(),L,N) -> U94#(isNatKind(activate(N)),activate(L)) U94#(tt(),L) -> activate#(L) U94#(tt(),L) -> length#(activate(L)) U94#(tt(),L) -> s#(length(activate(L))) isNat#(n__length(V1)) -> activate#(V1) isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) isNat#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) isNatIList#(V) -> activate#(V) isNatIList#(V) -> isNatIListKind#(activate(V)) isNatIList#(V) -> U31#(isNatIListKind(activate(V)),activate(V)) isNatIList#(n__cons(V1,V2)) -> activate#(V2) isNatIList#(n__cons(V1,V2)) -> activate#(V1) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__length(V1)) -> activate#(V1) isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) isNatList#(n__cons(V1,V2)) -> activate#(V2) isNatList#(n__cons(V1,V2)) -> activate#(V1) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) length#(nil()) -> 0#() length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> isNatList#(activate(L)) length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) activate#(n__zeros()) -> zeros#() activate#(n__0()) -> 0#() activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() TRS: zeros() -> cons(0(),n__zeros()) U11(tt(),V1) -> U12(isNatIListKind(activate(V1)),activate(V1)) U12(tt(),V1) -> U13(isNatList(activate(V1))) U13(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V) -> U32(isNatIListKind(activate(V)),activate(V)) U32(tt(),V) -> U33(isNatList(activate(V))) U33(tt()) -> tt() U41(tt(),V1,V2) -> U42(isNatKind(activate(V1)),activate(V1),activate(V2)) U42(tt(),V1,V2) -> U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43(tt(),V1,V2) -> U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44(tt(),V1,V2) -> U45(isNat(activate(V1)),activate(V2)) U45(tt(),V2) -> U46(isNatIList(activate(V2))) U46(tt()) -> tt() U51(tt(),V2) -> U52(isNatIListKind(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt()) -> tt() U81(tt(),V1,V2) -> U82(isNatKind(activate(V1)),activate(V1),activate(V2)) U82(tt(),V1,V2) -> U83(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83(tt(),V1,V2) -> U84(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84(tt(),V1,V2) -> U85(isNat(activate(V1)),activate(V2)) U85(tt(),V2) -> U86(isNatList(activate(V2))) U86(tt()) -> tt() U91(tt(),L,N) -> U92(isNatIListKind(activate(L)),activate(L),activate(N)) U92(tt(),L,N) -> U93(isNat(activate(N)),activate(L),activate(N)) U93(tt(),L,N) -> U94(isNatKind(activate(N)),activate(L)) U94(tt(),L) -> s(length(activate(L))) isNat(n__0()) -> tt() isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind(n__nil()) -> tt() isNatIListKind(n__zeros()) -> tt() isNatIListKind(n__cons(V1,V2)) -> U51(isNatKind(activate(V1)),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__length(V1)) -> U61(isNatIListKind(activate(V1))) isNatKind(n__s(V1)) -> U71(isNatKind(activate(V1))) isNatList(n__nil()) -> tt() isNatList(n__cons(V1,V2)) -> U81(isNatKind(activate(V1)),activate(V1),activate(V2)) length(nil()) -> 0() length(cons(N,L)) -> U91(isNatList(activate(L)),activate(L),N) zeros() -> n__zeros() 0() -> n__0() length(X) -> n__length(X) s(X) -> n__s(X) cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() activate(n__zeros()) -> zeros() activate(n__0()) -> 0() activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(X) -> X TDG Processor: DPs: zeros#() -> 0#() zeros#() -> cons#(0(),n__zeros()) U11#(tt(),V1) -> activate#(V1) U11#(tt(),V1) -> isNatIListKind#(activate(V1)) U11#(tt(),V1) -> U12#(isNatIListKind(activate(V1)),activate(V1)) U12#(tt(),V1) -> activate#(V1) U12#(tt(),V1) -> isNatList#(activate(V1)) U12#(tt(),V1) -> U13#(isNatList(activate(V1))) U21#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) U22#(tt(),V1) -> U23#(isNat(activate(V1))) U31#(tt(),V) -> activate#(V) U31#(tt(),V) -> isNatIListKind#(activate(V)) U31#(tt(),V) -> U32#(isNatIListKind(activate(V)),activate(V)) U32#(tt(),V) -> activate#(V) U32#(tt(),V) -> isNatList#(activate(V)) U32#(tt(),V) -> U33#(isNatList(activate(V))) U41#(tt(),V1,V2) -> activate#(V2) U41#(tt(),V1,V2) -> activate#(V1) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) U42#(tt(),V1,V2) -> activate#(V1) U42#(tt(),V1,V2) -> activate#(V2) U42#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43#(tt(),V1,V2) -> activate#(V1) U43#(tt(),V1,V2) -> activate#(V2) U43#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44#(tt(),V1,V2) -> activate#(V2) U44#(tt(),V1,V2) -> activate#(V1) U44#(tt(),V1,V2) -> isNat#(activate(V1)) U44#(tt(),V1,V2) -> U45#(isNat(activate(V1)),activate(V2)) U45#(tt(),V2) -> activate#(V2) U45#(tt(),V2) -> isNatIList#(activate(V2)) U45#(tt(),V2) -> U46#(isNatIList(activate(V2))) U51#(tt(),V2) -> activate#(V2) U51#(tt(),V2) -> isNatIListKind#(activate(V2)) U51#(tt(),V2) -> U52#(isNatIListKind(activate(V2))) U81#(tt(),V1,V2) -> activate#(V2) U81#(tt(),V1,V2) -> activate#(V1) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) U82#(tt(),V1,V2) -> activate#(V1) U82#(tt(),V1,V2) -> activate#(V2) U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83#(tt(),V1,V2) -> activate#(V1) U83#(tt(),V1,V2) -> activate#(V2) U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84#(tt(),V1,V2) -> activate#(V2) U84#(tt(),V1,V2) -> activate#(V1) U84#(tt(),V1,V2) -> isNat#(activate(V1)) U84#(tt(),V1,V2) -> U85#(isNat(activate(V1)),activate(V2)) U85#(tt(),V2) -> activate#(V2) U85#(tt(),V2) -> isNatList#(activate(V2)) U85#(tt(),V2) -> U86#(isNatList(activate(V2))) U91#(tt(),L,N) -> activate#(N) U91#(tt(),L,N) -> activate#(L) U91#(tt(),L,N) -> isNatIListKind#(activate(L)) U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) U92#(tt(),L,N) -> activate#(L) U92#(tt(),L,N) -> activate#(N) U92#(tt(),L,N) -> isNat#(activate(N)) U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) U93#(tt(),L,N) -> activate#(L) U93#(tt(),L,N) -> activate#(N) U93#(tt(),L,N) -> isNatKind#(activate(N)) U93#(tt(),L,N) -> U94#(isNatKind(activate(N)),activate(L)) U94#(tt(),L) -> activate#(L) U94#(tt(),L) -> length#(activate(L)) U94#(tt(),L) -> s#(length(activate(L))) isNat#(n__length(V1)) -> activate#(V1) isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) isNat#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) isNatIList#(V) -> activate#(V) isNatIList#(V) -> isNatIListKind#(activate(V)) isNatIList#(V) -> U31#(isNatIListKind(activate(V)),activate(V)) isNatIList#(n__cons(V1,V2)) -> activate#(V2) isNatIList#(n__cons(V1,V2)) -> activate#(V1) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__length(V1)) -> activate#(V1) isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) isNatList#(n__cons(V1,V2)) -> activate#(V2) isNatList#(n__cons(V1,V2)) -> activate#(V1) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) length#(nil()) -> 0#() length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> isNatList#(activate(L)) length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) activate#(n__zeros()) -> zeros#() activate#(n__0()) -> 0#() activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() TRS: zeros() -> cons(0(),n__zeros()) U11(tt(),V1) -> U12(isNatIListKind(activate(V1)),activate(V1)) U12(tt(),V1) -> U13(isNatList(activate(V1))) U13(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V) -> U32(isNatIListKind(activate(V)),activate(V)) U32(tt(),V) -> U33(isNatList(activate(V))) U33(tt()) -> tt() U41(tt(),V1,V2) -> U42(isNatKind(activate(V1)),activate(V1),activate(V2)) U42(tt(),V1,V2) -> U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43(tt(),V1,V2) -> U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44(tt(),V1,V2) -> U45(isNat(activate(V1)),activate(V2)) U45(tt(),V2) -> U46(isNatIList(activate(V2))) U46(tt()) -> tt() U51(tt(),V2) -> U52(isNatIListKind(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt()) -> tt() U81(tt(),V1,V2) -> U82(isNatKind(activate(V1)),activate(V1),activate(V2)) U82(tt(),V1,V2) -> U83(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83(tt(),V1,V2) -> U84(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84(tt(),V1,V2) -> U85(isNat(activate(V1)),activate(V2)) U85(tt(),V2) -> U86(isNatList(activate(V2))) U86(tt()) -> tt() U91(tt(),L,N) -> U92(isNatIListKind(activate(L)),activate(L),activate(N)) U92(tt(),L,N) -> U93(isNat(activate(N)),activate(L),activate(N)) U93(tt(),L,N) -> U94(isNatKind(activate(N)),activate(L)) U94(tt(),L) -> s(length(activate(L))) isNat(n__0()) -> tt() isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind(n__nil()) -> tt() isNatIListKind(n__zeros()) -> tt() isNatIListKind(n__cons(V1,V2)) -> U51(isNatKind(activate(V1)),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__length(V1)) -> U61(isNatIListKind(activate(V1))) isNatKind(n__s(V1)) -> U71(isNatKind(activate(V1))) isNatList(n__nil()) -> tt() isNatList(n__cons(V1,V2)) -> U81(isNatKind(activate(V1)),activate(V1),activate(V2)) length(nil()) -> 0() length(cons(N,L)) -> U91(isNatList(activate(L)),activate(L),N) zeros() -> n__zeros() 0() -> n__0() length(X) -> n__length(X) s(X) -> n__s(X) cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() activate(n__zeros()) -> zeros() activate(n__0()) -> 0() activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(X) -> X graph: length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) -> U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) -> U91#(tt(),L,N) -> isNatIListKind#(activate(L)) length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) -> U91#(tt(),L,N) -> activate#(L) length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) -> U91#(tt(),L,N) -> activate#(N) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(V1,V2)) -> activate#(V1) length#(cons(N,L)) -> isNatList#(activate(L)) -> isNatList#(n__cons(V1,V2)) -> activate#(V2) length#(cons(N,L)) -> activate#(L) -> activate#(n__nil()) -> nil#() length#(cons(N,L)) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) length#(cons(N,L)) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) length#(cons(N,L)) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) length#(cons(N,L)) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) length#(cons(N,L)) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) length#(cons(N,L)) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) length#(cons(N,L)) -> activate#(L) -> activate#(n__0()) -> 0#() length#(cons(N,L)) -> activate#(L) -> activate#(n__zeros()) -> zeros#() U94#(tt(),L) -> length#(activate(L)) -> length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) U94#(tt(),L) -> length#(activate(L)) -> length#(cons(N,L)) -> isNatList#(activate(L)) U94#(tt(),L) -> length#(activate(L)) -> length#(cons(N,L)) -> activate#(L) U94#(tt(),L) -> length#(activate(L)) -> length#(nil()) -> 0#() U94#(tt(),L) -> activate#(L) -> activate#(n__nil()) -> nil#() U94#(tt(),L) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U94#(tt(),L) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) U94#(tt(),L) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) U94#(tt(),L) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) U94#(tt(),L) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) U94#(tt(),L) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) U94#(tt(),L) -> activate#(L) -> activate#(n__0()) -> 0#() U94#(tt(),L) -> activate#(L) -> activate#(n__zeros()) -> zeros#() U93#(tt(),L,N) -> U94#(isNatKind(activate(N)),activate(L)) -> U94#(tt(),L) -> s#(length(activate(L))) U93#(tt(),L,N) -> U94#(isNatKind(activate(N)),activate(L)) -> U94#(tt(),L) -> length#(activate(L)) U93#(tt(),L,N) -> U94#(isNatKind(activate(N)),activate(L)) -> U94#(tt(),L) -> activate#(L) U93#(tt(),L,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) U93#(tt(),L,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U93#(tt(),L,N) -> isNatKind#(activate(N)) -> isNatKind#(n__s(V1)) -> activate#(V1) U93#(tt(),L,N) -> isNatKind#(activate(N)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) U93#(tt(),L,N) -> isNatKind#(activate(N)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) U93#(tt(),L,N) -> isNatKind#(activate(N)) -> isNatKind#(n__length(V1)) -> activate#(V1) U93#(tt(),L,N) -> activate#(N) -> activate#(n__nil()) -> nil#() U93#(tt(),L,N) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U93#(tt(),L,N) -> activate#(N) -> activate#(n__cons(X1,X2)) -> activate#(X1) U93#(tt(),L,N) -> activate#(N) -> activate#(n__s(X)) -> s#(activate(X)) U93#(tt(),L,N) -> activate#(N) -> activate#(n__s(X)) -> activate#(X) U93#(tt(),L,N) -> activate#(N) -> activate#(n__length(X)) -> length#(activate(X)) U93#(tt(),L,N) -> activate#(N) -> activate#(n__length(X)) -> activate#(X) U93#(tt(),L,N) -> activate#(N) -> activate#(n__0()) -> 0#() U93#(tt(),L,N) -> activate#(N) -> activate#(n__zeros()) -> zeros#() U93#(tt(),L,N) -> activate#(L) -> activate#(n__nil()) -> nil#() U93#(tt(),L,N) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U93#(tt(),L,N) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) U93#(tt(),L,N) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) U93#(tt(),L,N) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) U93#(tt(),L,N) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) U93#(tt(),L,N) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) U93#(tt(),L,N) -> activate#(L) -> activate#(n__0()) -> 0#() U93#(tt(),L,N) -> activate#(L) -> activate#(n__zeros()) -> zeros#() U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) -> U93#(tt(),L,N) -> U94#(isNatKind(activate(N)),activate(L)) U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) -> U93#(tt(),L,N) -> isNatKind#(activate(N)) U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) -> U93#(tt(),L,N) -> activate#(N) U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) -> U93#(tt(),L,N) -> activate#(L) U92#(tt(),L,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U92#(tt(),L,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U92#(tt(),L,N) -> isNat#(activate(N)) -> isNat#(n__s(V1)) -> activate#(V1) U92#(tt(),L,N) -> isNat#(activate(N)) -> isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) U92#(tt(),L,N) -> isNat#(activate(N)) -> isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) U92#(tt(),L,N) -> isNat#(activate(N)) -> isNat#(n__length(V1)) -> activate#(V1) U92#(tt(),L,N) -> activate#(N) -> activate#(n__nil()) -> nil#() U92#(tt(),L,N) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U92#(tt(),L,N) -> activate#(N) -> activate#(n__cons(X1,X2)) -> activate#(X1) U92#(tt(),L,N) -> activate#(N) -> activate#(n__s(X)) -> s#(activate(X)) U92#(tt(),L,N) -> activate#(N) -> activate#(n__s(X)) -> activate#(X) U92#(tt(),L,N) -> activate#(N) -> activate#(n__length(X)) -> length#(activate(X)) U92#(tt(),L,N) -> activate#(N) -> activate#(n__length(X)) -> activate#(X) U92#(tt(),L,N) -> activate#(N) -> activate#(n__0()) -> 0#() U92#(tt(),L,N) -> activate#(N) -> activate#(n__zeros()) -> zeros#() U92#(tt(),L,N) -> activate#(L) -> activate#(n__nil()) -> nil#() U92#(tt(),L,N) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U92#(tt(),L,N) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) U92#(tt(),L,N) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) U92#(tt(),L,N) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) U92#(tt(),L,N) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) U92#(tt(),L,N) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) U92#(tt(),L,N) -> activate#(L) -> activate#(n__0()) -> 0#() U92#(tt(),L,N) -> activate#(L) -> activate#(n__zeros()) -> zeros#() U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) -> U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) -> U92#(tt(),L,N) -> isNat#(activate(N)) U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) -> U92#(tt(),L,N) -> activate#(N) U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) -> U92#(tt(),L,N) -> activate#(L) U91#(tt(),L,N) -> isNatIListKind#(activate(L)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U91#(tt(),L,N) -> isNatIListKind#(activate(L)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U91#(tt(),L,N) -> isNatIListKind#(activate(L)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) U91#(tt(),L,N) -> isNatIListKind#(activate(L)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) U91#(tt(),L,N) -> activate#(N) -> activate#(n__nil()) -> nil#() U91#(tt(),L,N) -> activate#(N) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U91#(tt(),L,N) -> activate#(N) -> activate#(n__cons(X1,X2)) -> activate#(X1) U91#(tt(),L,N) -> activate#(N) -> activate#(n__s(X)) -> s#(activate(X)) U91#(tt(),L,N) -> activate#(N) -> activate#(n__s(X)) -> activate#(X) U91#(tt(),L,N) -> activate#(N) -> activate#(n__length(X)) -> length#(activate(X)) U91#(tt(),L,N) -> activate#(N) -> activate#(n__length(X)) -> activate#(X) U91#(tt(),L,N) -> activate#(N) -> activate#(n__0()) -> 0#() U91#(tt(),L,N) -> activate#(N) -> activate#(n__zeros()) -> zeros#() U91#(tt(),L,N) -> activate#(L) -> activate#(n__nil()) -> nil#() U91#(tt(),L,N) -> activate#(L) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U91#(tt(),L,N) -> activate#(L) -> activate#(n__cons(X1,X2)) -> activate#(X1) U91#(tt(),L,N) -> activate#(L) -> activate#(n__s(X)) -> s#(activate(X)) U91#(tt(),L,N) -> activate#(L) -> activate#(n__s(X)) -> activate#(X) U91#(tt(),L,N) -> activate#(L) -> activate#(n__length(X)) -> length#(activate(X)) U91#(tt(),L,N) -> activate#(L) -> activate#(n__length(X)) -> activate#(X) U91#(tt(),L,N) -> activate#(L) -> activate#(n__0()) -> 0#() U91#(tt(),L,N) -> activate#(L) -> activate#(n__zeros()) -> zeros#() U85#(tt(),V2) -> isNatList#(activate(V2)) -> isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) U85#(tt(),V2) -> isNatList#(activate(V2)) -> isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U85#(tt(),V2) -> isNatList#(activate(V2)) -> isNatList#(n__cons(V1,V2)) -> activate#(V1) U85#(tt(),V2) -> isNatList#(activate(V2)) -> isNatList#(n__cons(V1,V2)) -> activate#(V2) U85#(tt(),V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U85#(tt(),V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U85#(tt(),V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U85#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U85#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U85#(tt(),V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U85#(tt(),V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U85#(tt(),V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U85#(tt(),V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U84#(tt(),V1,V2) -> U85#(isNat(activate(V1)),activate(V2)) -> U85#(tt(),V2) -> U86#(isNatList(activate(V2))) U84#(tt(),V1,V2) -> U85#(isNat(activate(V1)),activate(V2)) -> U85#(tt(),V2) -> isNatList#(activate(V2)) U84#(tt(),V1,V2) -> U85#(isNat(activate(V1)),activate(V2)) -> U85#(tt(),V2) -> activate#(V2) U84#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U84#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U84#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> activate#(V1) U84#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) U84#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) U84#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> activate#(V1) U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U84#(tt(),V1,V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__nil()) -> nil#() U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U84#(tt(),V1,V2) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U84#(tt(),V1,V2) -> U85#(isNat(activate(V1)),activate(V2)) U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U84#(tt(),V1,V2) -> isNat#(activate(V1)) U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U84#(tt(),V1,V2) -> activate#(V1) U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U84#(tt(),V1,V2) -> activate#(V2) U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U83#(tt(),V1,V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__nil()) -> nil#() U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U83#(tt(),V1,V2) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U83#(tt(),V1,V2) -> activate#(V2) U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U83#(tt(),V1,V2) -> activate#(V1) U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U82#(tt(),V1,V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__nil()) -> nil#() U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U82#(tt(),V1,V2) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U82#(tt(),V1,V2) -> activate#(V2) U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U82#(tt(),V1,V2) -> activate#(V1) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> activate#(V1) U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U81#(tt(),V1,V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__nil()) -> nil#() U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U81#(tt(),V1,V2) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U51#(tt(),V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U51#(tt(),V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U51#(tt(),V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) U51#(tt(),V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) U51#(tt(),V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U51#(tt(),V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U51#(tt(),V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U51#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U51#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U51#(tt(),V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U51#(tt(),V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U51#(tt(),V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U51#(tt(),V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U41#(tt(),V1,V2) -> activate#(V1) isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U41#(tt(),V1,V2) -> activate#(V2) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> activate#(V1) isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isNatIList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatIList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() isNatIList#(V) -> U31#(isNatIListKind(activate(V)),activate(V)) -> U31#(tt(),V) -> U32#(isNatIListKind(activate(V)),activate(V)) isNatIList#(V) -> U31#(isNatIListKind(activate(V)),activate(V)) -> U31#(tt(),V) -> isNatIListKind#(activate(V)) isNatIList#(V) -> U31#(isNatIListKind(activate(V)),activate(V)) -> U31#(tt(),V) -> activate#(V) isNatIList#(V) -> isNatIListKind#(activate(V)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) isNatIList#(V) -> isNatIListKind#(activate(V)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatIList#(V) -> isNatIListKind#(activate(V)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) isNatIList#(V) -> isNatIListKind#(activate(V)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) isNatIList#(V) -> activate#(V) -> activate#(n__nil()) -> nil#() isNatIList#(V) -> activate#(V) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatIList#(V) -> activate#(V) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatIList#(V) -> activate#(V) -> activate#(n__s(X)) -> s#(activate(X)) isNatIList#(V) -> activate#(V) -> activate#(n__s(X)) -> activate#(X) isNatIList#(V) -> activate#(V) -> activate#(n__length(X)) -> length#(activate(X)) isNatIList#(V) -> activate#(V) -> activate#(n__length(X)) -> activate#(X) isNatIList#(V) -> activate#(V) -> activate#(n__0()) -> 0#() isNatIList#(V) -> activate#(V) -> activate#(n__zeros()) -> zeros#() U45#(tt(),V2) -> isNatIList#(activate(V2)) -> isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) U45#(tt(),V2) -> isNatIList#(activate(V2)) -> isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U45#(tt(),V2) -> isNatIList#(activate(V2)) -> isNatIList#(n__cons(V1,V2)) -> activate#(V1) U45#(tt(),V2) -> isNatIList#(activate(V2)) -> isNatIList#(n__cons(V1,V2)) -> activate#(V2) U45#(tt(),V2) -> isNatIList#(activate(V2)) -> isNatIList#(V) -> U31#(isNatIListKind(activate(V)),activate(V)) U45#(tt(),V2) -> isNatIList#(activate(V2)) -> isNatIList#(V) -> isNatIListKind#(activate(V)) U45#(tt(),V2) -> isNatIList#(activate(V2)) -> isNatIList#(V) -> activate#(V) U45#(tt(),V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U45#(tt(),V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U45#(tt(),V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U45#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U45#(tt(),V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U45#(tt(),V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U45#(tt(),V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U45#(tt(),V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U45#(tt(),V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U44#(tt(),V1,V2) -> U45#(isNat(activate(V1)),activate(V2)) -> U45#(tt(),V2) -> U46#(isNatIList(activate(V2))) U44#(tt(),V1,V2) -> U45#(isNat(activate(V1)),activate(V2)) -> U45#(tt(),V2) -> isNatIList#(activate(V2)) U44#(tt(),V1,V2) -> U45#(isNat(activate(V1)),activate(V2)) -> U45#(tt(),V2) -> activate#(V2) U44#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U44#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U44#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> activate#(V1) U44#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) U44#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) U44#(tt(),V1,V2) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> activate#(V1) U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U44#(tt(),V1,V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__nil()) -> nil#() U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U44#(tt(),V1,V2) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U44#(tt(),V1,V2) -> U45#(isNat(activate(V1)),activate(V2)) U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U44#(tt(),V1,V2) -> isNat#(activate(V1)) U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U44#(tt(),V1,V2) -> activate#(V1) U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U44#(tt(),V1,V2) -> activate#(V2) U43#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U43#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U43#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) U43#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U43#(tt(),V1,V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__nil()) -> nil#() U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U43#(tt(),V1,V2) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U43#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U43#(tt(),V1,V2) -> activate#(V2) U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) -> U43#(tt(),V1,V2) -> activate#(V1) U42#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U42#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U42#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) U42#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U42#(tt(),V1,V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__nil()) -> nil#() U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U42#(tt(),V1,V2) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U42#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U42#(tt(),V1,V2) -> activate#(V2) U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U42#(tt(),V1,V2) -> activate#(V1) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> activate#(V1) U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__nil()) -> nil#() U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__0()) -> 0#() U41#(tt(),V1,V2) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__nil()) -> nil#() U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__0()) -> 0#() U41#(tt(),V1,V2) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U32#(tt(),V) -> isNatList#(activate(V)) -> isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) U32#(tt(),V) -> isNatList#(activate(V)) -> isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U32#(tt(),V) -> isNatList#(activate(V)) -> isNatList#(n__cons(V1,V2)) -> activate#(V1) U32#(tt(),V) -> isNatList#(activate(V)) -> isNatList#(n__cons(V1,V2)) -> activate#(V2) U32#(tt(),V) -> activate#(V) -> activate#(n__nil()) -> nil#() U32#(tt(),V) -> activate#(V) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U32#(tt(),V) -> activate#(V) -> activate#(n__cons(X1,X2)) -> activate#(X1) U32#(tt(),V) -> activate#(V) -> activate#(n__s(X)) -> s#(activate(X)) U32#(tt(),V) -> activate#(V) -> activate#(n__s(X)) -> activate#(X) U32#(tt(),V) -> activate#(V) -> activate#(n__length(X)) -> length#(activate(X)) U32#(tt(),V) -> activate#(V) -> activate#(n__length(X)) -> activate#(X) U32#(tt(),V) -> activate#(V) -> activate#(n__0()) -> 0#() U32#(tt(),V) -> activate#(V) -> activate#(n__zeros()) -> zeros#() U31#(tt(),V) -> U32#(isNatIListKind(activate(V)),activate(V)) -> U32#(tt(),V) -> U33#(isNatList(activate(V))) U31#(tt(),V) -> U32#(isNatIListKind(activate(V)),activate(V)) -> U32#(tt(),V) -> isNatList#(activate(V)) U31#(tt(),V) -> U32#(isNatIListKind(activate(V)),activate(V)) -> U32#(tt(),V) -> activate#(V) U31#(tt(),V) -> isNatIListKind#(activate(V)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U31#(tt(),V) -> isNatIListKind#(activate(V)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U31#(tt(),V) -> isNatIListKind#(activate(V)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) U31#(tt(),V) -> isNatIListKind#(activate(V)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) U31#(tt(),V) -> activate#(V) -> activate#(n__nil()) -> nil#() U31#(tt(),V) -> activate#(V) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U31#(tt(),V) -> activate#(V) -> activate#(n__cons(X1,X2)) -> activate#(X1) U31#(tt(),V) -> activate#(V) -> activate#(n__s(X)) -> s#(activate(X)) U31#(tt(),V) -> activate#(V) -> activate#(n__s(X)) -> activate#(X) U31#(tt(),V) -> activate#(V) -> activate#(n__length(X)) -> length#(activate(X)) U31#(tt(),V) -> activate#(V) -> activate#(n__length(X)) -> activate#(X) U31#(tt(),V) -> activate#(V) -> activate#(n__0()) -> 0#() U31#(tt(),V) -> activate#(V) -> activate#(n__zeros()) -> zeros#() isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> activate#(V1) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) -> U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) -> U21#(tt(),V1) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) -> U21#(tt(),V1) -> activate#(V1) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNat#(n__s(V1)) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNat#(n__length(V1)) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) -> U11#(tt(),V1) -> U12#(isNatIListKind(activate(V1)),activate(V1)) isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) -> U11#(tt(),V1) -> isNatIListKind#(activate(V1)) isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) -> U11#(tt(),V1) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> isNatKind#(activate(V1)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__s(V1)) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) U22#(tt(),V1) -> isNat#(activate(V1)) -> isNat#(n__length(V1)) -> activate#(V1) U22#(tt(),V1) -> activate#(V1) -> activate#(n__nil()) -> nil#() U22#(tt(),V1) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U22#(tt(),V1) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U22#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U22#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U22#(tt(),V1) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U22#(tt(),V1) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U22#(tt(),V1) -> activate#(V1) -> activate#(n__0()) -> 0#() U22#(tt(),V1) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatKind#(n__s(V1)) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatKind#(n__length(V1)) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) -> U22#(tt(),V1) -> U23#(isNat(activate(V1))) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) -> U22#(tt(),V1) -> isNat#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) -> U22#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) U21#(tt(),V1) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> activate#(V1) U21#(tt(),V1) -> activate#(V1) -> activate#(n__nil()) -> nil#() U21#(tt(),V1) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U21#(tt(),V1) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U21#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U21#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U21#(tt(),V1) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U21#(tt(),V1) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U21#(tt(),V1) -> activate#(V1) -> activate#(n__0()) -> 0#() U21#(tt(),V1) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U81#(tt(),V1,V2) -> activate#(V1) isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) -> U81#(tt(),V1,V2) -> activate#(V2) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> activate#(V1) isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isNatList#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatList#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() U12#(tt(),V1) -> isNatList#(activate(V1)) -> isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) U12#(tt(),V1) -> isNatList#(activate(V1)) -> isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U12#(tt(),V1) -> isNatList#(activate(V1)) -> isNatList#(n__cons(V1,V2)) -> activate#(V1) U12#(tt(),V1) -> isNatList#(activate(V1)) -> isNatList#(n__cons(V1,V2)) -> activate#(V2) U12#(tt(),V1) -> activate#(V1) -> activate#(n__nil()) -> nil#() U12#(tt(),V1) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U12#(tt(),V1) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U12#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U12#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U12#(tt(),V1) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U12#(tt(),V1) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U12#(tt(),V1) -> activate#(V1) -> activate#(n__0()) -> 0#() U12#(tt(),V1) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) -> U51#(tt(),V2) -> U52#(isNatIListKind(activate(V2))) isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) -> U51#(tt(),V2) -> isNatIListKind#(activate(V2)) isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) -> U51#(tt(),V2) -> activate#(V2) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__s(V1)) -> activate#(V1) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) -> isNatKind#(n__length(V1)) -> activate#(V1) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> s#(activate(X)) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__s(X)) -> activate#(X) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__length(X)) -> length#(activate(X)) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__length(X)) -> activate#(X) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__0()) -> 0#() isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) -> activate#(n__zeros()) -> zeros#() isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__0()) -> 0#() isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__nil()) -> nil#() activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__length(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__zeros()) -> zeros#() activate#(n__s(X)) -> activate#(X) -> activate#(n__nil()) -> nil#() activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__length(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) -> activate#(n__zeros()) -> zeros#() activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(N,L)) -> isNatList#(activate(L)) activate#(n__length(X)) -> length#(activate(X)) -> length#(cons(N,L)) -> activate#(L) activate#(n__length(X)) -> length#(activate(X)) -> length#(nil()) -> 0#() activate#(n__length(X)) -> activate#(X) -> activate#(n__nil()) -> nil#() activate#(n__length(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__length(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__length(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__length(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__length(X)) -> activate#(X) -> activate#(n__length(X)) -> length#(activate(X)) activate#(n__length(X)) -> activate#(X) -> activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__length(X)) -> activate#(X) -> activate#(n__zeros()) -> zeros#() activate#(n__zeros()) -> zeros#() -> zeros#() -> cons#(0(),n__zeros()) activate#(n__zeros()) -> zeros#() -> zeros#() -> 0#() U11#(tt(),V1) -> U12#(isNatIListKind(activate(V1)),activate(V1)) -> U12#(tt(),V1) -> U13#(isNatList(activate(V1))) U11#(tt(),V1) -> U12#(isNatIListKind(activate(V1)),activate(V1)) -> U12#(tt(),V1) -> isNatList#(activate(V1)) U11#(tt(),V1) -> U12#(isNatIListKind(activate(V1)),activate(V1)) -> U12#(tt(),V1) -> activate#(V1) U11#(tt(),V1) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U11#(tt(),V1) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) U11#(tt(),V1) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) U11#(tt(),V1) -> isNatIListKind#(activate(V1)) -> isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) U11#(tt(),V1) -> activate#(V1) -> activate#(n__nil()) -> nil#() U11#(tt(),V1) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) U11#(tt(),V1) -> activate#(V1) -> activate#(n__cons(X1,X2)) -> activate#(X1) U11#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> s#(activate(X)) U11#(tt(),V1) -> activate#(V1) -> activate#(n__s(X)) -> activate#(X) U11#(tt(),V1) -> activate#(V1) -> activate#(n__length(X)) -> length#(activate(X)) U11#(tt(),V1) -> activate#(V1) -> activate#(n__length(X)) -> activate#(X) U11#(tt(),V1) -> activate#(V1) -> activate#(n__0()) -> 0#() U11#(tt(),V1) -> activate#(V1) -> activate#(n__zeros()) -> zeros#() Restore Modifier: DPs: zeros#() -> 0#() zeros#() -> cons#(0(),n__zeros()) U11#(tt(),V1) -> activate#(V1) U11#(tt(),V1) -> isNatIListKind#(activate(V1)) U11#(tt(),V1) -> U12#(isNatIListKind(activate(V1)),activate(V1)) U12#(tt(),V1) -> activate#(V1) U12#(tt(),V1) -> isNatList#(activate(V1)) U12#(tt(),V1) -> U13#(isNatList(activate(V1))) U21#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) U22#(tt(),V1) -> U23#(isNat(activate(V1))) U31#(tt(),V) -> activate#(V) U31#(tt(),V) -> isNatIListKind#(activate(V)) U31#(tt(),V) -> U32#(isNatIListKind(activate(V)),activate(V)) U32#(tt(),V) -> activate#(V) U32#(tt(),V) -> isNatList#(activate(V)) U32#(tt(),V) -> U33#(isNatList(activate(V))) U41#(tt(),V1,V2) -> activate#(V2) U41#(tt(),V1,V2) -> activate#(V1) U41#(tt(),V1,V2) -> isNatKind#(activate(V1)) U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) U42#(tt(),V1,V2) -> activate#(V1) U42#(tt(),V1,V2) -> activate#(V2) U42#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43#(tt(),V1,V2) -> activate#(V1) U43#(tt(),V1,V2) -> activate#(V2) U43#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44#(tt(),V1,V2) -> activate#(V2) U44#(tt(),V1,V2) -> activate#(V1) U44#(tt(),V1,V2) -> isNat#(activate(V1)) U44#(tt(),V1,V2) -> U45#(isNat(activate(V1)),activate(V2)) U45#(tt(),V2) -> activate#(V2) U45#(tt(),V2) -> isNatIList#(activate(V2)) U45#(tt(),V2) -> U46#(isNatIList(activate(V2))) U51#(tt(),V2) -> activate#(V2) U51#(tt(),V2) -> isNatIListKind#(activate(V2)) U51#(tt(),V2) -> U52#(isNatIListKind(activate(V2))) U81#(tt(),V1,V2) -> activate#(V2) U81#(tt(),V1,V2) -> activate#(V1) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) U82#(tt(),V1,V2) -> activate#(V1) U82#(tt(),V1,V2) -> activate#(V2) U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83#(tt(),V1,V2) -> activate#(V1) U83#(tt(),V1,V2) -> activate#(V2) U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84#(tt(),V1,V2) -> activate#(V2) U84#(tt(),V1,V2) -> activate#(V1) U84#(tt(),V1,V2) -> isNat#(activate(V1)) U84#(tt(),V1,V2) -> U85#(isNat(activate(V1)),activate(V2)) U85#(tt(),V2) -> activate#(V2) U85#(tt(),V2) -> isNatList#(activate(V2)) U85#(tt(),V2) -> U86#(isNatList(activate(V2))) U91#(tt(),L,N) -> activate#(N) U91#(tt(),L,N) -> activate#(L) U91#(tt(),L,N) -> isNatIListKind#(activate(L)) U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) U92#(tt(),L,N) -> activate#(L) U92#(tt(),L,N) -> activate#(N) U92#(tt(),L,N) -> isNat#(activate(N)) U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) U93#(tt(),L,N) -> activate#(L) U93#(tt(),L,N) -> activate#(N) U93#(tt(),L,N) -> isNatKind#(activate(N)) U93#(tt(),L,N) -> U94#(isNatKind(activate(N)),activate(L)) U94#(tt(),L) -> activate#(L) U94#(tt(),L) -> length#(activate(L)) U94#(tt(),L) -> s#(length(activate(L))) isNat#(n__length(V1)) -> activate#(V1) isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) isNat#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) isNatIList#(V) -> activate#(V) isNatIList#(V) -> isNatIListKind#(activate(V)) isNatIList#(V) -> U31#(isNatIListKind(activate(V)),activate(V)) isNatIList#(n__cons(V1,V2)) -> activate#(V2) isNatIList#(n__cons(V1,V2)) -> activate#(V1) isNatIList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) isNatKind#(n__length(V1)) -> activate#(V1) isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNatKind#(n__length(V1)) -> U61#(isNatIListKind(activate(V1))) isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> U71#(isNatKind(activate(V1))) isNatList#(n__cons(V1,V2)) -> activate#(V2) isNatList#(n__cons(V1,V2)) -> activate#(V1) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) length#(nil()) -> 0#() length#(cons(N,L)) -> activate#(L) length#(cons(N,L)) -> isNatList#(activate(L)) length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) activate#(n__zeros()) -> zeros#() activate#(n__0()) -> 0#() activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__nil()) -> nil#() TRS: zeros() -> cons(0(),n__zeros()) U11(tt(),V1) -> U12(isNatIListKind(activate(V1)),activate(V1)) U12(tt(),V1) -> U13(isNatList(activate(V1))) U13(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V) -> U32(isNatIListKind(activate(V)),activate(V)) U32(tt(),V) -> U33(isNatList(activate(V))) U33(tt()) -> tt() U41(tt(),V1,V2) -> U42(isNatKind(activate(V1)),activate(V1),activate(V2)) U42(tt(),V1,V2) -> U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43(tt(),V1,V2) -> U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44(tt(),V1,V2) -> U45(isNat(activate(V1)),activate(V2)) U45(tt(),V2) -> U46(isNatIList(activate(V2))) U46(tt()) -> tt() U51(tt(),V2) -> U52(isNatIListKind(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt()) -> tt() U81(tt(),V1,V2) -> U82(isNatKind(activate(V1)),activate(V1),activate(V2)) U82(tt(),V1,V2) -> U83(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83(tt(),V1,V2) -> U84(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84(tt(),V1,V2) -> U85(isNat(activate(V1)),activate(V2)) U85(tt(),V2) -> U86(isNatList(activate(V2))) U86(tt()) -> tt() U91(tt(),L,N) -> U92(isNatIListKind(activate(L)),activate(L),activate(N)) U92(tt(),L,N) -> U93(isNat(activate(N)),activate(L),activate(N)) U93(tt(),L,N) -> U94(isNatKind(activate(N)),activate(L)) U94(tt(),L) -> s(length(activate(L))) isNat(n__0()) -> tt() isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind(n__nil()) -> tt() isNatIListKind(n__zeros()) -> tt() isNatIListKind(n__cons(V1,V2)) -> U51(isNatKind(activate(V1)),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__length(V1)) -> U61(isNatIListKind(activate(V1))) isNatKind(n__s(V1)) -> U71(isNatKind(activate(V1))) isNatList(n__nil()) -> tt() isNatList(n__cons(V1,V2)) -> U81(isNatKind(activate(V1)),activate(V1),activate(V2)) length(nil()) -> 0() length(cons(N,L)) -> U91(isNatList(activate(L)),activate(L),N) zeros() -> n__zeros() 0() -> n__0() length(X) -> n__length(X) s(X) -> n__s(X) cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() activate(n__zeros()) -> zeros() activate(n__0()) -> 0() activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(X) -> X SCC Processor: #sccs: 2 #rules: 75 #arcs: 652/13456 DPs: isNatIList#(n__cons(V1,V2)) -> U41#(isNatKind(activate(V1)),activate(V1),activate(V2)) U41#(tt(),V1,V2) -> U42#(isNatKind(activate(V1)),activate(V1),activate(V2)) U42#(tt(),V1,V2) -> U43#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43#(tt(),V1,V2) -> U44#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44#(tt(),V1,V2) -> U45#(isNat(activate(V1)),activate(V2)) U45#(tt(),V2) -> isNatIList#(activate(V2)) TRS: zeros() -> cons(0(),n__zeros()) U11(tt(),V1) -> U12(isNatIListKind(activate(V1)),activate(V1)) U12(tt(),V1) -> U13(isNatList(activate(V1))) U13(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V) -> U32(isNatIListKind(activate(V)),activate(V)) U32(tt(),V) -> U33(isNatList(activate(V))) U33(tt()) -> tt() U41(tt(),V1,V2) -> U42(isNatKind(activate(V1)),activate(V1),activate(V2)) U42(tt(),V1,V2) -> U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43(tt(),V1,V2) -> U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44(tt(),V1,V2) -> U45(isNat(activate(V1)),activate(V2)) U45(tt(),V2) -> U46(isNatIList(activate(V2))) U46(tt()) -> tt() U51(tt(),V2) -> U52(isNatIListKind(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt()) -> tt() U81(tt(),V1,V2) -> U82(isNatKind(activate(V1)),activate(V1),activate(V2)) U82(tt(),V1,V2) -> U83(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83(tt(),V1,V2) -> U84(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84(tt(),V1,V2) -> U85(isNat(activate(V1)),activate(V2)) U85(tt(),V2) -> U86(isNatList(activate(V2))) U86(tt()) -> tt() U91(tt(),L,N) -> U92(isNatIListKind(activate(L)),activate(L),activate(N)) U92(tt(),L,N) -> U93(isNat(activate(N)),activate(L),activate(N)) U93(tt(),L,N) -> U94(isNatKind(activate(N)),activate(L)) U94(tt(),L) -> s(length(activate(L))) isNat(n__0()) -> tt() isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind(n__nil()) -> tt() isNatIListKind(n__zeros()) -> tt() isNatIListKind(n__cons(V1,V2)) -> U51(isNatKind(activate(V1)),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__length(V1)) -> U61(isNatIListKind(activate(V1))) isNatKind(n__s(V1)) -> U71(isNatKind(activate(V1))) isNatList(n__nil()) -> tt() isNatList(n__cons(V1,V2)) -> U81(isNatKind(activate(V1)),activate(V1),activate(V2)) length(nil()) -> 0() length(cons(N,L)) -> U91(isNatList(activate(L)),activate(L),N) zeros() -> n__zeros() 0() -> n__0() length(X) -> n__length(X) s(X) -> n__s(X) cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() activate(n__zeros()) -> zeros() activate(n__0()) -> 0() activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(X) -> X Open DPs: length#(cons(N,L)) -> U91#(isNatList(activate(L)),activate(L),N) U91#(tt(),L,N) -> activate#(N) activate#(n__length(X)) -> activate#(X) activate#(n__length(X)) -> length#(activate(X)) length#(cons(N,L)) -> activate#(L) activate#(n__s(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) length#(cons(N,L)) -> isNatList#(activate(L)) isNatList#(n__cons(V1,V2)) -> activate#(V2) isNatList#(n__cons(V1,V2)) -> activate#(V1) isNatList#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__length(V1)) -> activate#(V1) isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNatIListKind#(n__cons(V1,V2)) -> activate#(V2) isNatIListKind#(n__cons(V1,V2)) -> activate#(V1) isNatIListKind#(n__cons(V1,V2)) -> isNatKind#(activate(V1)) isNatKind#(n__s(V1)) -> activate#(V1) isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) isNatIListKind#(n__cons(V1,V2)) -> U51#(isNatKind(activate(V1)),activate(V2)) U51#(tt(),V2) -> activate#(V2) U51#(tt(),V2) -> isNatIListKind#(activate(V2)) isNatList#(n__cons(V1,V2)) -> U81#(isNatKind(activate(V1)),activate(V1),activate(V2)) U81#(tt(),V1,V2) -> activate#(V2) U81#(tt(),V1,V2) -> activate#(V1) U81#(tt(),V1,V2) -> isNatKind#(activate(V1)) U81#(tt(),V1,V2) -> U82#(isNatKind(activate(V1)),activate(V1),activate(V2)) U82#(tt(),V1,V2) -> activate#(V1) U82#(tt(),V1,V2) -> activate#(V2) U82#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U82#(tt(),V1,V2) -> U83#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83#(tt(),V1,V2) -> activate#(V1) U83#(tt(),V1,V2) -> activate#(V2) U83#(tt(),V1,V2) -> isNatIListKind#(activate(V2)) U83#(tt(),V1,V2) -> U84#(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84#(tt(),V1,V2) -> activate#(V2) U84#(tt(),V1,V2) -> activate#(V1) U84#(tt(),V1,V2) -> isNat#(activate(V1)) isNat#(n__length(V1)) -> activate#(V1) isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)) isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)),activate(V1)) U11#(tt(),V1) -> activate#(V1) U11#(tt(),V1) -> isNatIListKind#(activate(V1)) U11#(tt(),V1) -> U12#(isNatIListKind(activate(V1)),activate(V1)) U12#(tt(),V1) -> activate#(V1) U12#(tt(),V1) -> isNatList#(activate(V1)) isNat#(n__s(V1)) -> activate#(V1) isNat#(n__s(V1)) -> isNatKind#(activate(V1)) isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) U21#(tt(),V1) -> activate#(V1) U21#(tt(),V1) -> isNatKind#(activate(V1)) U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) U22#(tt(),V1) -> activate#(V1) U22#(tt(),V1) -> isNat#(activate(V1)) U84#(tt(),V1,V2) -> U85#(isNat(activate(V1)),activate(V2)) U85#(tt(),V2) -> activate#(V2) U85#(tt(),V2) -> isNatList#(activate(V2)) U91#(tt(),L,N) -> activate#(L) U91#(tt(),L,N) -> isNatIListKind#(activate(L)) U91#(tt(),L,N) -> U92#(isNatIListKind(activate(L)),activate(L),activate(N)) U92#(tt(),L,N) -> activate#(L) U92#(tt(),L,N) -> activate#(N) U92#(tt(),L,N) -> isNat#(activate(N)) U92#(tt(),L,N) -> U93#(isNat(activate(N)),activate(L),activate(N)) U93#(tt(),L,N) -> activate#(L) U93#(tt(),L,N) -> activate#(N) U93#(tt(),L,N) -> isNatKind#(activate(N)) U93#(tt(),L,N) -> U94#(isNatKind(activate(N)),activate(L)) U94#(tt(),L) -> activate#(L) U94#(tt(),L) -> length#(activate(L)) TRS: zeros() -> cons(0(),n__zeros()) U11(tt(),V1) -> U12(isNatIListKind(activate(V1)),activate(V1)) U12(tt(),V1) -> U13(isNatList(activate(V1))) U13(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V) -> U32(isNatIListKind(activate(V)),activate(V)) U32(tt(),V) -> U33(isNatList(activate(V))) U33(tt()) -> tt() U41(tt(),V1,V2) -> U42(isNatKind(activate(V1)),activate(V1),activate(V2)) U42(tt(),V1,V2) -> U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U43(tt(),V1,V2) -> U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U44(tt(),V1,V2) -> U45(isNat(activate(V1)),activate(V2)) U45(tt(),V2) -> U46(isNatIList(activate(V2))) U46(tt()) -> tt() U51(tt(),V2) -> U52(isNatIListKind(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt()) -> tt() U81(tt(),V1,V2) -> U82(isNatKind(activate(V1)),activate(V1),activate(V2)) U82(tt(),V1,V2) -> U83(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U83(tt(),V1,V2) -> U84(isNatIListKind(activate(V2)),activate(V1),activate(V2)) U84(tt(),V1,V2) -> U85(isNat(activate(V1)),activate(V2)) U85(tt(),V2) -> U86(isNatList(activate(V2))) U86(tt()) -> tt() U91(tt(),L,N) -> U92(isNatIListKind(activate(L)),activate(L),activate(N)) U92(tt(),L,N) -> U93(isNat(activate(N)),activate(L),activate(N)) U93(tt(),L,N) -> U94(isNatKind(activate(N)),activate(L)) U94(tt(),L) -> s(length(activate(L))) isNat(n__0()) -> tt() isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V)) isNatIList(n__zeros()) -> tt() isNatIList(n__cons(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V1),activate(V2)) isNatIListKind(n__nil()) -> tt() isNatIListKind(n__zeros()) -> tt() isNatIListKind(n__cons(V1,V2)) -> U51(isNatKind(activate(V1)),activate(V2)) isNatKind(n__0()) -> tt() isNatKind(n__length(V1)) -> U61(isNatIListKind(activate(V1))) isNatKind(n__s(V1)) -> U71(isNatKind(activate(V1))) isNatList(n__nil()) -> tt() isNatList(n__cons(V1,V2)) -> U81(isNatKind(activate(V1)),activate(V1),activate(V2)) length(nil()) -> 0() length(cons(N,L)) -> U91(isNatList(activate(L)),activate(L),N) zeros() -> n__zeros() 0() -> n__0() length(X) -> n__length(X) s(X) -> n__s(X) cons(X1,X2) -> n__cons(X1,X2) nil() -> n__nil() activate(n__zeros()) -> zeros() activate(n__0()) -> 0() activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__nil()) -> nil() activate(X) -> X Open