MAYBE 1089.15/297.16 MAYBE 1089.15/297.16 1089.15/297.16 We are left with following problem, upon which TcT provides the 1089.15/297.16 certificate MAYBE. 1089.15/297.16 1089.15/297.16 Strict Trs: 1089.15/297.16 { U101(tt(), V2) -> U102(isLNat(activate(V2))) 1089.15/297.16 , U102(tt()) -> tt() 1089.15/297.16 , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1))) 1089.15/297.16 , isLNat(n__nil()) -> tt() 1089.15/297.16 , isLNat(n__afterNth(V1, V2)) -> 1089.15/297.16 U41(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , isLNat(n__cons(V1, V2)) -> 1089.15/297.16 U51(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1))) 1089.15/297.16 , isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1))) 1089.15/297.16 , isLNat(n__tail(V1)) -> U91(isLNat(activate(V1))) 1089.15/297.16 , isLNat(n__take(V1, V2)) -> 1089.15/297.16 U101(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , activate(X) -> X 1089.15/297.16 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 1089.15/297.16 , activate(n__s(X)) -> s(activate(X)) 1089.15/297.16 , activate(n__nil()) -> nil() 1089.15/297.16 , activate(n__afterNth(X1, X2)) -> 1089.15/297.16 afterNth(activate(X1), activate(X2)) 1089.15/297.16 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1089.15/297.16 , activate(n__fst(X)) -> fst(activate(X)) 1089.15/297.16 , activate(n__snd(X)) -> snd(activate(X)) 1089.15/297.16 , activate(n__tail(X)) -> tail(activate(X)) 1089.15/297.16 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1089.15/297.16 , activate(n__0()) -> 0() 1089.15/297.16 , activate(n__head(X)) -> head(activate(X)) 1089.15/297.16 , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) 1089.15/297.16 , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) 1089.15/297.16 , activate(n__splitAt(X1, X2)) -> 1089.15/297.16 splitAt(activate(X1), activate(X2)) 1089.15/297.16 , U11(tt(), N, XS) -> 1089.15/297.16 U12(isLNat(activate(XS)), activate(N), activate(XS)) 1089.15/297.16 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 1089.15/297.16 , U111(tt()) -> tt() 1089.15/297.16 , snd(X) -> n__snd(X) 1089.15/297.16 , snd(pair(X, Y)) -> U181(isLNat(X), Y) 1089.15/297.16 , splitAt(X1, X2) -> n__splitAt(X1, X2) 1089.15/297.16 , splitAt(0(), XS) -> U191(isLNat(XS), XS) 1089.15/297.16 , splitAt(s(N), cons(X, XS)) -> 1089.15/297.16 U201(isNatural(N), N, X, activate(XS)) 1089.15/297.16 , U121(tt()) -> tt() 1089.15/297.16 , U131(tt(), V2) -> U132(isLNat(activate(V2))) 1089.15/297.16 , U132(tt()) -> tt() 1089.15/297.16 , U141(tt(), V2) -> U142(isLNat(activate(V2))) 1089.15/297.16 , U142(tt()) -> tt() 1089.15/297.16 , U151(tt(), V2) -> U152(isLNat(activate(V2))) 1089.15/297.16 , U152(tt()) -> tt() 1089.15/297.16 , U161(tt(), N) -> 1089.15/297.16 cons(activate(N), n__natsFrom(n__s(activate(N)))) 1089.15/297.16 , cons(X1, X2) -> n__cons(X1, X2) 1089.15/297.16 , U171(tt(), N, XS) -> 1089.15/297.16 U172(isLNat(activate(XS)), activate(N), activate(XS)) 1089.15/297.16 , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 1089.15/297.16 , head(X) -> n__head(X) 1089.15/297.16 , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS)) 1089.15/297.16 , afterNth(N, XS) -> U11(isNatural(N), N, XS) 1089.15/297.16 , afterNth(X1, X2) -> n__afterNth(X1, X2) 1089.15/297.16 , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y)) 1089.15/297.16 , U182(tt(), Y) -> activate(Y) 1089.15/297.16 , U191(tt(), XS) -> pair(nil(), activate(XS)) 1089.15/297.16 , pair(X1, X2) -> n__pair(X1, X2) 1089.15/297.16 , nil() -> n__nil() 1089.15/297.16 , U201(tt(), N, X, XS) -> 1089.15/297.16 U202(isNatural(activate(X)), 1089.15/297.16 activate(N), 1089.15/297.16 activate(X), 1089.15/297.16 activate(XS)) 1089.15/297.16 , U202(tt(), N, X, XS) -> 1089.15/297.16 U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) 1089.15/297.16 , isNatural(n__s(V1)) -> U121(isNatural(activate(V1))) 1089.15/297.16 , isNatural(n__0()) -> tt() 1089.15/297.16 , isNatural(n__head(V1)) -> U111(isLNat(activate(V1))) 1089.15/297.16 , isNatural(n__sel(V1, V2)) -> 1089.15/297.16 U131(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , U203(tt(), N, X, XS) -> 1089.15/297.16 U204(splitAt(activate(N), activate(XS)), activate(X)) 1089.15/297.16 , U204(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 1089.15/297.16 , U21(tt(), X, Y) -> U22(isLNat(activate(Y)), activate(X)) 1089.15/297.16 , U22(tt(), X) -> activate(X) 1089.15/297.16 , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS)) 1089.15/297.16 , U212(tt(), XS) -> activate(XS) 1089.15/297.16 , U221(tt(), N, XS) -> 1089.15/297.16 U222(isLNat(activate(XS)), activate(N), activate(XS)) 1089.15/297.16 , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 1089.15/297.16 , fst(X) -> n__fst(X) 1089.15/297.16 , fst(pair(X, Y)) -> U21(isLNat(X), X, Y) 1089.15/297.16 , U31(tt(), N, XS) -> U32(isLNat(activate(XS)), activate(N)) 1089.15/297.16 , U32(tt(), N) -> activate(N) 1089.15/297.16 , U41(tt(), V2) -> U42(isLNat(activate(V2))) 1089.15/297.16 , U42(tt()) -> tt() 1089.15/297.16 , U51(tt(), V2) -> U52(isLNat(activate(V2))) 1089.15/297.16 , U52(tt()) -> tt() 1089.15/297.16 , U61(tt()) -> tt() 1089.15/297.16 , U71(tt()) -> tt() 1089.15/297.16 , U81(tt()) -> tt() 1089.15/297.16 , U91(tt()) -> tt() 1089.15/297.16 , isPLNat(n__pair(V1, V2)) -> 1089.15/297.16 U141(isLNat(activate(V1)), activate(V2)) 1089.15/297.16 , isPLNat(n__splitAt(V1, V2)) -> 1089.15/297.16 U151(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , natsFrom(N) -> U161(isNatural(N), N) 1089.15/297.16 , natsFrom(X) -> n__natsFrom(X) 1089.15/297.16 , sel(N, XS) -> U171(isNatural(N), N, XS) 1089.15/297.16 , sel(X1, X2) -> n__sel(X1, X2) 1089.15/297.16 , 0() -> n__0() 1089.15/297.16 , s(X) -> n__s(X) 1089.15/297.16 , tail(X) -> n__tail(X) 1089.15/297.16 , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS)) 1089.15/297.16 , take(N, XS) -> U221(isNatural(N), N, XS) 1089.15/297.16 , take(X1, X2) -> n__take(X1, X2) } 1089.15/297.16 Obligation: 1089.15/297.16 innermost runtime complexity 1089.15/297.16 Answer: 1089.15/297.16 MAYBE 1089.15/297.16 1089.15/297.16 Arguments of following rules are not normal-forms: 1089.15/297.16 1089.15/297.16 { snd(pair(X, Y)) -> U181(isLNat(X), Y) 1089.15/297.16 , splitAt(0(), XS) -> U191(isLNat(XS), XS) 1089.15/297.16 , splitAt(s(N), cons(X, XS)) -> 1089.15/297.16 U201(isNatural(N), N, X, activate(XS)) 1089.15/297.16 , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS)) 1089.15/297.16 , U204(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 1089.15/297.16 , fst(pair(X, Y)) -> U21(isLNat(X), X, Y) 1089.15/297.16 , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS)) } 1089.15/297.16 1089.15/297.16 All above mentioned rules can be savely removed. 1089.15/297.16 1089.15/297.16 We are left with following problem, upon which TcT provides the 1089.15/297.16 certificate MAYBE. 1089.15/297.16 1089.15/297.16 Strict Trs: 1089.15/297.16 { U101(tt(), V2) -> U102(isLNat(activate(V2))) 1089.15/297.16 , U102(tt()) -> tt() 1089.15/297.16 , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1))) 1089.15/297.16 , isLNat(n__nil()) -> tt() 1089.15/297.16 , isLNat(n__afterNth(V1, V2)) -> 1089.15/297.16 U41(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , isLNat(n__cons(V1, V2)) -> 1089.15/297.16 U51(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1))) 1089.15/297.16 , isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1))) 1089.15/297.16 , isLNat(n__tail(V1)) -> U91(isLNat(activate(V1))) 1089.15/297.16 , isLNat(n__take(V1, V2)) -> 1089.15/297.16 U101(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , activate(X) -> X 1089.15/297.16 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 1089.15/297.16 , activate(n__s(X)) -> s(activate(X)) 1089.15/297.16 , activate(n__nil()) -> nil() 1089.15/297.16 , activate(n__afterNth(X1, X2)) -> 1089.15/297.16 afterNth(activate(X1), activate(X2)) 1089.15/297.16 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1089.15/297.16 , activate(n__fst(X)) -> fst(activate(X)) 1089.15/297.16 , activate(n__snd(X)) -> snd(activate(X)) 1089.15/297.16 , activate(n__tail(X)) -> tail(activate(X)) 1089.15/297.16 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1089.15/297.16 , activate(n__0()) -> 0() 1089.15/297.16 , activate(n__head(X)) -> head(activate(X)) 1089.15/297.16 , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) 1089.15/297.16 , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) 1089.15/297.16 , activate(n__splitAt(X1, X2)) -> 1089.15/297.16 splitAt(activate(X1), activate(X2)) 1089.15/297.16 , U11(tt(), N, XS) -> 1089.15/297.16 U12(isLNat(activate(XS)), activate(N), activate(XS)) 1089.15/297.16 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 1089.15/297.16 , U111(tt()) -> tt() 1089.15/297.16 , snd(X) -> n__snd(X) 1089.15/297.16 , splitAt(X1, X2) -> n__splitAt(X1, X2) 1089.15/297.16 , U121(tt()) -> tt() 1089.15/297.16 , U131(tt(), V2) -> U132(isLNat(activate(V2))) 1089.15/297.16 , U132(tt()) -> tt() 1089.15/297.16 , U141(tt(), V2) -> U142(isLNat(activate(V2))) 1089.15/297.16 , U142(tt()) -> tt() 1089.15/297.16 , U151(tt(), V2) -> U152(isLNat(activate(V2))) 1089.15/297.16 , U152(tt()) -> tt() 1089.15/297.16 , U161(tt(), N) -> 1089.15/297.16 cons(activate(N), n__natsFrom(n__s(activate(N)))) 1089.15/297.16 , cons(X1, X2) -> n__cons(X1, X2) 1089.15/297.16 , U171(tt(), N, XS) -> 1089.15/297.16 U172(isLNat(activate(XS)), activate(N), activate(XS)) 1089.15/297.16 , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 1089.15/297.16 , head(X) -> n__head(X) 1089.15/297.16 , afterNth(N, XS) -> U11(isNatural(N), N, XS) 1089.15/297.16 , afterNth(X1, X2) -> n__afterNth(X1, X2) 1089.15/297.16 , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y)) 1089.15/297.16 , U182(tt(), Y) -> activate(Y) 1089.15/297.16 , U191(tt(), XS) -> pair(nil(), activate(XS)) 1089.15/297.16 , pair(X1, X2) -> n__pair(X1, X2) 1089.15/297.16 , nil() -> n__nil() 1089.15/297.16 , U201(tt(), N, X, XS) -> 1089.15/297.16 U202(isNatural(activate(X)), 1089.15/297.16 activate(N), 1089.15/297.16 activate(X), 1089.15/297.16 activate(XS)) 1089.15/297.16 , U202(tt(), N, X, XS) -> 1089.15/297.16 U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) 1089.15/297.16 , isNatural(n__s(V1)) -> U121(isNatural(activate(V1))) 1089.15/297.16 , isNatural(n__0()) -> tt() 1089.15/297.16 , isNatural(n__head(V1)) -> U111(isLNat(activate(V1))) 1089.15/297.16 , isNatural(n__sel(V1, V2)) -> 1089.15/297.16 U131(isNatural(activate(V1)), activate(V2)) 1089.15/297.16 , U203(tt(), N, X, XS) -> 1089.15/297.16 U204(splitAt(activate(N), activate(XS)), activate(X)) 1089.15/297.16 , U21(tt(), X, Y) -> U22(isLNat(activate(Y)), activate(X)) 1089.15/297.17 , U22(tt(), X) -> activate(X) 1089.15/297.17 , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS)) 1089.15/297.17 , U212(tt(), XS) -> activate(XS) 1089.15/297.17 , U221(tt(), N, XS) -> 1089.15/297.17 U222(isLNat(activate(XS)), activate(N), activate(XS)) 1089.15/297.17 , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 1089.15/297.17 , fst(X) -> n__fst(X) 1089.15/297.17 , U31(tt(), N, XS) -> U32(isLNat(activate(XS)), activate(N)) 1089.15/297.17 , U32(tt(), N) -> activate(N) 1089.15/297.17 , U41(tt(), V2) -> U42(isLNat(activate(V2))) 1089.15/297.17 , U42(tt()) -> tt() 1089.15/297.17 , U51(tt(), V2) -> U52(isLNat(activate(V2))) 1089.15/297.17 , U52(tt()) -> tt() 1089.15/297.17 , U61(tt()) -> tt() 1089.15/297.17 , U71(tt()) -> tt() 1089.15/297.17 , U81(tt()) -> tt() 1089.15/297.17 , U91(tt()) -> tt() 1089.15/297.17 , isPLNat(n__pair(V1, V2)) -> 1089.15/297.17 U141(isLNat(activate(V1)), activate(V2)) 1089.15/297.17 , isPLNat(n__splitAt(V1, V2)) -> 1089.15/297.17 U151(isNatural(activate(V1)), activate(V2)) 1089.15/297.17 , natsFrom(N) -> U161(isNatural(N), N) 1089.15/297.17 , natsFrom(X) -> n__natsFrom(X) 1089.15/297.17 , sel(N, XS) -> U171(isNatural(N), N, XS) 1089.15/297.17 , sel(X1, X2) -> n__sel(X1, X2) 1089.15/297.17 , 0() -> n__0() 1089.15/297.17 , s(X) -> n__s(X) 1089.15/297.17 , tail(X) -> n__tail(X) 1089.15/297.17 , take(N, XS) -> U221(isNatural(N), N, XS) 1089.15/297.17 , take(X1, X2) -> n__take(X1, X2) } 1089.15/297.17 Obligation: 1089.15/297.17 innermost runtime complexity 1089.15/297.17 Answer: 1089.15/297.17 MAYBE 1089.15/297.17 1089.15/297.17 None of the processors succeeded. 1089.15/297.17 1089.15/297.17 Details of failed attempt(s): 1089.15/297.17 ----------------------------- 1089.15/297.17 1) 'empty' failed due to the following reason: 1089.15/297.17 1089.15/297.17 Empty strict component of the problem is NOT empty. 1089.15/297.17 1089.15/297.17 2) 'Best' failed due to the following reason: 1089.15/297.17 1089.15/297.17 None of the processors succeeded. 1089.15/297.17 1089.15/297.17 Details of failed attempt(s): 1089.15/297.17 ----------------------------- 1089.15/297.17 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1089.15/297.17 following reason: 1089.15/297.17 1089.15/297.17 Computation stopped due to timeout after 297.0 seconds. 1089.15/297.17 1089.15/297.17 2) 'Best' failed due to the following reason: 1089.15/297.17 1089.15/297.17 None of the processors succeeded. 1089.15/297.17 1089.15/297.17 Details of failed attempt(s): 1089.15/297.17 ----------------------------- 1089.15/297.17 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1089.15/297.17 seconds)' failed due to the following reason: 1089.15/297.17 1089.15/297.17 Computation stopped due to timeout after 148.0 seconds. 1089.15/297.17 1089.15/297.17 2) 'Best' failed due to the following reason: 1089.15/297.17 1089.15/297.17 None of the processors succeeded. 1089.15/297.17 1089.15/297.17 Details of failed attempt(s): 1089.15/297.17 ----------------------------- 1089.15/297.17 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1089.15/297.17 to the following reason: 1089.15/297.17 1089.15/297.17 The input cannot be shown compatible 1089.15/297.17 1089.15/297.17 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1089.15/297.17 following reason: 1089.15/297.17 1089.15/297.17 The input cannot be shown compatible 1089.15/297.17 1089.15/297.17 1089.15/297.17 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1089.15/297.17 failed due to the following reason: 1089.15/297.17 1089.15/297.17 None of the processors succeeded. 1089.15/297.17 1089.15/297.17 Details of failed attempt(s): 1089.15/297.17 ----------------------------- 1089.15/297.17 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1089.15/297.17 failed due to the following reason: 1089.15/297.17 1089.15/297.17 match-boundness of the problem could not be verified. 1089.15/297.17 1089.15/297.17 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1089.15/297.17 failed due to the following reason: 1089.15/297.17 1089.15/297.17 match-boundness of the problem could not be verified. 1089.15/297.17 1089.15/297.17 1089.15/297.17 1089.15/297.17 1089.15/297.17 1089.15/297.17 Arrrr.. 1089.15/297.17 EOF