MAYBE 1093.92/297.09 MAYBE 1093.92/297.09 1093.92/297.09 We are left with following problem, upon which TcT provides the 1093.92/297.09 certificate MAYBE. 1093.92/297.09 1093.92/297.09 Strict Trs: 1093.92/297.09 { zeros() -> cons(0(), n__zeros()) 1093.92/297.09 , zeros() -> n__zeros() 1093.92/297.09 , cons(X1, X2) -> n__cons(X1, X2) 1093.92/297.09 , 0() -> n__0() 1093.92/297.09 , U101(tt(), V1, V2) -> 1093.92/297.09 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.09 , U102(tt(), V1, V2) -> 1093.92/297.09 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1093.92/297.09 , isNatKind(n__0()) -> tt() 1093.92/297.09 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 1093.92/297.09 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 1093.92/297.09 , activate(X) -> X 1093.92/297.09 , activate(n__zeros()) -> zeros() 1093.92/297.09 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1093.92/297.09 , activate(n__0()) -> 0() 1093.92/297.09 , activate(n__length(X)) -> length(activate(X)) 1093.92/297.09 , activate(n__s(X)) -> s(activate(X)) 1093.92/297.09 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1093.92/297.09 , activate(n__nil()) -> nil() 1093.92/297.09 , U103(tt(), V1, V2) -> 1093.92/297.09 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1093.92/297.09 , isNatIListKind(n__zeros()) -> tt() 1093.92/297.09 , isNatIListKind(n__take(V1, V2)) -> 1093.92/297.10 U61(isNatKind(activate(V1)), activate(V2)) 1093.92/297.10 , isNatIListKind(n__cons(V1, V2)) -> 1093.92/297.10 U51(isNatKind(activate(V1)), activate(V2)) 1093.92/297.10 , isNatIListKind(n__nil()) -> tt() 1093.92/297.10 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 1093.92/297.10 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 1093.92/297.10 , isNat(n__0()) -> tt() 1093.92/297.10 , isNat(n__length(V1)) -> 1093.92/297.10 U11(isNatIListKind(activate(V1)), activate(V1)) 1093.92/297.10 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 1093.92/297.10 , U106(tt()) -> tt() 1093.92/297.10 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 1093.92/297.10 , isNatIList(n__zeros()) -> tt() 1093.92/297.10 , isNatIList(n__cons(V1, V2)) -> 1093.92/297.10 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 1093.92/297.10 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 1093.92/297.10 , U111(tt(), L, N) -> 1093.92/297.10 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 1093.92/297.10 , U112(tt(), L, N) -> 1093.92/297.10 U113(isNat(activate(N)), activate(L), activate(N)) 1093.92/297.10 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 1093.92/297.10 , U114(tt(), L) -> s(length(activate(L))) 1093.92/297.10 , s(X) -> n__s(X) 1093.92/297.10 , length(X) -> n__length(X) 1093.92/297.10 , length(cons(N, L)) -> 1093.92/297.10 U111(isNatList(activate(L)), activate(L), N) 1093.92/297.10 , length(nil()) -> 0() 1093.92/297.10 , U13(tt()) -> tt() 1093.92/297.10 , isNatList(n__take(V1, V2)) -> 1093.92/297.10 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , isNatList(n__cons(V1, V2)) -> 1093.92/297.10 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , isNatList(n__nil()) -> tt() 1093.92/297.10 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 1093.92/297.10 , U122(tt()) -> nil() 1093.92/297.10 , nil() -> n__nil() 1093.92/297.10 , U131(tt(), IL, M, N) -> 1093.92/297.10 U132(isNatIListKind(activate(IL)), 1093.92/297.10 activate(IL), 1093.92/297.10 activate(M), 1093.92/297.10 activate(N)) 1093.92/297.10 , U132(tt(), IL, M, N) -> 1093.92/297.10 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 1093.92/297.10 , U133(tt(), IL, M, N) -> 1093.92/297.10 U134(isNatKind(activate(M)), 1093.92/297.10 activate(IL), 1093.92/297.10 activate(M), 1093.92/297.10 activate(N)) 1093.92/297.10 , U134(tt(), IL, M, N) -> 1093.92/297.10 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 1093.92/297.10 , U135(tt(), IL, M, N) -> 1093.92/297.10 U136(isNatKind(activate(N)), 1093.92/297.10 activate(IL), 1093.92/297.10 activate(M), 1093.92/297.10 activate(N)) 1093.92/297.10 , U136(tt(), IL, M, N) -> 1093.92/297.10 cons(activate(N), n__take(activate(M), activate(IL))) 1093.92/297.10 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 1093.92/297.10 , U22(tt(), V1) -> U23(isNat(activate(V1))) 1093.92/297.10 , U23(tt()) -> tt() 1093.92/297.10 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 1093.92/297.10 , U32(tt(), V) -> U33(isNatList(activate(V))) 1093.92/297.10 , U33(tt()) -> tt() 1093.92/297.10 , U41(tt(), V1, V2) -> 1093.92/297.10 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , U42(tt(), V1, V2) -> 1093.92/297.10 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1093.92/297.10 , U43(tt(), V1, V2) -> 1093.92/297.10 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1093.92/297.10 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 1093.92/297.10 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 1093.92/297.10 , U46(tt()) -> tt() 1093.92/297.10 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 1093.92/297.10 , U52(tt()) -> tt() 1093.92/297.10 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 1093.92/297.10 , U62(tt()) -> tt() 1093.92/297.10 , U71(tt()) -> tt() 1093.92/297.10 , U81(tt()) -> tt() 1093.92/297.10 , U91(tt(), V1, V2) -> 1093.92/297.10 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , U92(tt(), V1, V2) -> 1093.92/297.10 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1093.92/297.10 , U93(tt(), V1, V2) -> 1093.92/297.10 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1093.92/297.10 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 1093.92/297.10 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 1093.92/297.10 , U96(tt()) -> tt() 1093.92/297.10 , take(X1, X2) -> n__take(X1, X2) 1093.92/297.10 , take(0(), IL) -> U121(isNatIList(IL), IL) 1093.92/297.10 , take(s(M), cons(N, IL)) -> 1093.92/297.10 U131(isNatIList(activate(IL)), activate(IL), M, N) } 1093.92/297.10 Obligation: 1093.92/297.10 innermost runtime complexity 1093.92/297.10 Answer: 1093.92/297.10 MAYBE 1093.92/297.10 1093.92/297.10 Arguments of following rules are not normal-forms: 1093.92/297.10 1093.92/297.10 { length(cons(N, L)) -> 1093.92/297.10 U111(isNatList(activate(L)), activate(L), N) 1093.92/297.10 , length(nil()) -> 0() 1093.92/297.10 , take(0(), IL) -> U121(isNatIList(IL), IL) 1093.92/297.10 , take(s(M), cons(N, IL)) -> 1093.92/297.10 U131(isNatIList(activate(IL)), activate(IL), M, N) } 1093.92/297.10 1093.92/297.10 All above mentioned rules can be savely removed. 1093.92/297.10 1093.92/297.10 We are left with following problem, upon which TcT provides the 1093.92/297.10 certificate MAYBE. 1093.92/297.10 1093.92/297.10 Strict Trs: 1093.92/297.10 { zeros() -> cons(0(), n__zeros()) 1093.92/297.10 , zeros() -> n__zeros() 1093.92/297.10 , cons(X1, X2) -> n__cons(X1, X2) 1093.92/297.10 , 0() -> n__0() 1093.92/297.10 , U101(tt(), V1, V2) -> 1093.92/297.10 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , U102(tt(), V1, V2) -> 1093.92/297.10 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1093.92/297.10 , isNatKind(n__0()) -> tt() 1093.92/297.10 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 1093.92/297.10 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 1093.92/297.10 , activate(X) -> X 1093.92/297.10 , activate(n__zeros()) -> zeros() 1093.92/297.10 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1093.92/297.10 , activate(n__0()) -> 0() 1093.92/297.10 , activate(n__length(X)) -> length(activate(X)) 1093.92/297.10 , activate(n__s(X)) -> s(activate(X)) 1093.92/297.10 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1093.92/297.10 , activate(n__nil()) -> nil() 1093.92/297.10 , U103(tt(), V1, V2) -> 1093.92/297.10 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1093.92/297.10 , isNatIListKind(n__zeros()) -> tt() 1093.92/297.10 , isNatIListKind(n__take(V1, V2)) -> 1093.92/297.10 U61(isNatKind(activate(V1)), activate(V2)) 1093.92/297.10 , isNatIListKind(n__cons(V1, V2)) -> 1093.92/297.10 U51(isNatKind(activate(V1)), activate(V2)) 1093.92/297.10 , isNatIListKind(n__nil()) -> tt() 1093.92/297.10 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 1093.92/297.10 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 1093.92/297.10 , isNat(n__0()) -> tt() 1093.92/297.10 , isNat(n__length(V1)) -> 1093.92/297.10 U11(isNatIListKind(activate(V1)), activate(V1)) 1093.92/297.10 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 1093.92/297.10 , U106(tt()) -> tt() 1093.92/297.10 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 1093.92/297.10 , isNatIList(n__zeros()) -> tt() 1093.92/297.10 , isNatIList(n__cons(V1, V2)) -> 1093.92/297.10 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 1093.92/297.10 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 1093.92/297.10 , U111(tt(), L, N) -> 1093.92/297.10 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 1093.92/297.10 , U112(tt(), L, N) -> 1093.92/297.10 U113(isNat(activate(N)), activate(L), activate(N)) 1093.92/297.10 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 1093.92/297.10 , U114(tt(), L) -> s(length(activate(L))) 1093.92/297.10 , s(X) -> n__s(X) 1093.92/297.10 , length(X) -> n__length(X) 1093.92/297.10 , U13(tt()) -> tt() 1093.92/297.10 , isNatList(n__take(V1, V2)) -> 1093.92/297.10 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , isNatList(n__cons(V1, V2)) -> 1093.92/297.10 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 1093.92/297.10 , isNatList(n__nil()) -> tt() 1093.92/297.10 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 1093.92/297.10 , U122(tt()) -> nil() 1093.92/297.10 , nil() -> n__nil() 1093.92/297.10 , U131(tt(), IL, M, N) -> 1093.92/297.10 U132(isNatIListKind(activate(IL)), 1093.92/297.10 activate(IL), 1093.92/297.10 activate(M), 1093.92/297.10 activate(N)) 1093.92/297.10 , U132(tt(), IL, M, N) -> 1093.92/297.10 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 1093.92/297.10 , U133(tt(), IL, M, N) -> 1093.92/297.10 U134(isNatKind(activate(M)), 1093.92/297.10 activate(IL), 1093.92/297.10 activate(M), 1093.92/297.10 activate(N)) 1093.92/297.10 , U134(tt(), IL, M, N) -> 1093.92/297.10 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 1094.24/297.10 , U135(tt(), IL, M, N) -> 1094.24/297.10 U136(isNatKind(activate(N)), 1094.24/297.10 activate(IL), 1094.24/297.10 activate(M), 1094.24/297.10 activate(N)) 1094.24/297.10 , U136(tt(), IL, M, N) -> 1094.24/297.10 cons(activate(N), n__take(activate(M), activate(IL))) 1094.24/297.10 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 1094.24/297.10 , U22(tt(), V1) -> U23(isNat(activate(V1))) 1094.24/297.10 , U23(tt()) -> tt() 1094.24/297.10 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 1094.24/297.10 , U32(tt(), V) -> U33(isNatList(activate(V))) 1094.24/297.10 , U33(tt()) -> tt() 1094.24/297.10 , U41(tt(), V1, V2) -> 1094.24/297.10 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 1094.24/297.10 , U42(tt(), V1, V2) -> 1094.24/297.10 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1094.24/297.10 , U43(tt(), V1, V2) -> 1094.24/297.10 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1094.24/297.10 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 1094.24/297.10 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 1094.24/297.10 , U46(tt()) -> tt() 1094.24/297.10 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 1094.24/297.10 , U52(tt()) -> tt() 1094.24/297.10 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 1094.24/297.10 , U62(tt()) -> tt() 1094.24/297.10 , U71(tt()) -> tt() 1094.24/297.10 , U81(tt()) -> tt() 1094.24/297.10 , U91(tt(), V1, V2) -> 1094.24/297.10 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 1094.24/297.10 , U92(tt(), V1, V2) -> 1094.24/297.10 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1094.24/297.10 , U93(tt(), V1, V2) -> 1094.24/297.10 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 1094.24/297.10 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 1094.24/297.10 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 1094.24/297.10 , U96(tt()) -> tt() 1094.24/297.10 , take(X1, X2) -> n__take(X1, X2) } 1094.24/297.10 Obligation: 1094.24/297.10 innermost runtime complexity 1094.24/297.10 Answer: 1094.24/297.10 MAYBE 1094.24/297.10 1094.24/297.10 None of the processors succeeded. 1094.24/297.10 1094.24/297.10 Details of failed attempt(s): 1094.24/297.10 ----------------------------- 1094.24/297.10 1) 'empty' failed due to the following reason: 1094.24/297.10 1094.24/297.10 Empty strict component of the problem is NOT empty. 1094.24/297.10 1094.24/297.10 2) 'Best' failed due to the following reason: 1094.24/297.10 1094.24/297.10 None of the processors succeeded. 1094.24/297.10 1094.24/297.10 Details of failed attempt(s): 1094.24/297.10 ----------------------------- 1094.24/297.10 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1094.24/297.10 following reason: 1094.24/297.10 1094.24/297.10 Computation stopped due to timeout after 297.0 seconds. 1094.24/297.10 1094.24/297.10 2) 'Best' failed due to the following reason: 1094.24/297.10 1094.24/297.10 None of the processors succeeded. 1094.24/297.10 1094.24/297.10 Details of failed attempt(s): 1094.24/297.10 ----------------------------- 1094.24/297.10 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1094.24/297.10 seconds)' failed due to the following reason: 1094.24/297.10 1094.24/297.10 Computation stopped due to timeout after 148.0 seconds. 1094.24/297.10 1094.24/297.10 2) 'Best' failed due to the following reason: 1094.24/297.10 1094.24/297.10 None of the processors succeeded. 1094.24/297.10 1094.24/297.10 Details of failed attempt(s): 1094.24/297.10 ----------------------------- 1094.24/297.10 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1094.24/297.10 to the following reason: 1094.24/297.10 1094.24/297.10 The input cannot be shown compatible 1094.24/297.10 1094.24/297.10 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1094.24/297.10 following reason: 1094.24/297.10 1094.24/297.10 The input cannot be shown compatible 1094.24/297.10 1094.24/297.10 1094.24/297.10 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1094.24/297.10 failed due to the following reason: 1094.24/297.10 1094.24/297.10 None of the processors succeeded. 1094.24/297.10 1094.24/297.10 Details of failed attempt(s): 1094.24/297.10 ----------------------------- 1094.24/297.10 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1094.24/297.10 failed due to the following reason: 1094.24/297.10 1094.24/297.10 match-boundness of the problem could not be verified. 1094.24/297.10 1094.24/297.10 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1094.24/297.10 failed due to the following reason: 1094.24/297.10 1094.24/297.10 match-boundness of the problem could not be verified. 1094.24/297.10 1094.24/297.10 1094.24/297.10 1094.24/297.10 1094.24/297.10 1094.24/297.10 Arrrr.. 1094.24/297.10 EOF