MAYBE 1041.03/297.11 MAYBE 1041.03/297.11 1041.03/297.11 We are left with following problem, upon which TcT provides the 1041.03/297.11 certificate MAYBE. 1041.03/297.11 1041.03/297.11 Strict Trs: 1041.03/297.11 { zeros() -> cons(0(), n__zeros()) 1041.03/297.11 , zeros() -> n__zeros() 1041.03/297.11 , cons(X1, X2) -> n__cons(X1, X2) 1041.03/297.11 , 0() -> n__0() 1041.03/297.11 , U11(tt(), V1) -> U12(isNatList(activate(V1))) 1041.03/297.11 , U12(tt()) -> tt() 1041.03/297.11 , isNatList(n__take(V1, V2)) -> 1041.03/297.11 U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 1041.03/297.11 activate(V1), 1041.03/297.11 activate(V2)) 1041.03/297.11 , isNatList(n__cons(V1, V2)) -> 1041.03/297.11 U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 1041.03/297.11 activate(V1), 1041.03/297.11 activate(V2)) 1041.03/297.11 , isNatList(n__nil()) -> tt() 1041.03/297.11 , activate(X) -> X 1041.03/297.11 , activate(n__zeros()) -> zeros() 1041.03/297.11 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1041.03/297.11 , activate(n__0()) -> 0() 1041.03/297.11 , activate(n__length(X)) -> length(activate(X)) 1041.03/297.11 , activate(n__s(X)) -> s(activate(X)) 1041.03/297.11 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1041.03/297.11 , activate(n__isNatIListKind(X)) -> isNatIListKind(X) 1041.03/297.11 , activate(n__nil()) -> nil() 1041.03/297.11 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 1041.03/297.11 , activate(n__isNat(X)) -> isNat(X) 1041.03/297.11 , activate(n__isNatKind(X)) -> isNatKind(X) 1041.03/297.11 , U21(tt(), V1) -> U22(isNat(activate(V1))) 1041.03/297.11 , U22(tt()) -> tt() 1041.03/297.11 , isNat(X) -> n__isNat(X) 1041.03/297.11 , isNat(n__0()) -> tt() 1041.03/297.11 , isNat(n__length(V1)) -> 1041.03/297.11 U11(isNatIListKind(activate(V1)), activate(V1)) 1041.03/297.11 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 1041.03/297.11 , U31(tt(), V) -> U32(isNatList(activate(V))) 1041.03/297.11 , U32(tt()) -> tt() 1041.03/297.11 , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) 1041.03/297.11 , U42(tt(), V2) -> U43(isNatIList(activate(V2))) 1041.03/297.11 , U43(tt()) -> tt() 1041.03/297.11 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 1041.03/297.11 , isNatIList(n__zeros()) -> tt() 1041.03/297.11 , isNatIList(n__cons(V1, V2)) -> 1041.03/297.11 U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 1041.03/297.11 activate(V1), 1041.03/297.11 activate(V2)) 1041.03/297.11 , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) 1041.03/297.11 , U52(tt(), V2) -> U53(isNatList(activate(V2))) 1041.03/297.11 , U53(tt()) -> tt() 1041.03/297.11 , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) 1041.03/297.11 , U62(tt(), V2) -> U63(isNatIList(activate(V2))) 1041.03/297.11 , U63(tt()) -> tt() 1041.03/297.11 , U71(tt(), L) -> s(length(activate(L))) 1041.03/297.11 , s(X) -> n__s(X) 1041.03/297.11 , length(X) -> n__length(X) 1041.03/297.11 , length(cons(N, L)) -> 1041.03/297.11 U71(and(and(isNatList(activate(L)), 1041.03/297.11 n__isNatIListKind(activate(L))), 1041.03/297.11 n__and(n__isNat(N), n__isNatKind(N))), 1041.03/297.11 activate(L)) 1041.03/297.11 , length(nil()) -> 0() 1041.03/297.11 , U81(tt()) -> nil() 1041.03/297.11 , nil() -> n__nil() 1041.03/297.11 , U91(tt(), IL, M, N) -> 1041.03/297.11 cons(activate(N), n__take(activate(M), activate(IL))) 1041.03/297.11 , and(X1, X2) -> n__and(X1, X2) 1041.03/297.11 , and(tt(), X) -> activate(X) 1041.03/297.11 , isNatIListKind(X) -> n__isNatIListKind(X) 1041.03/297.11 , isNatIListKind(n__zeros()) -> tt() 1041.03/297.11 , isNatIListKind(n__take(V1, V2)) -> 1041.03/297.11 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 1041.03/297.11 , isNatIListKind(n__cons(V1, V2)) -> 1041.03/297.11 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 1041.03/297.11 , isNatIListKind(n__nil()) -> tt() 1041.03/297.11 , isNatKind(X) -> n__isNatKind(X) 1041.03/297.11 , isNatKind(n__0()) -> tt() 1041.03/297.11 , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) 1041.03/297.11 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 1041.03/297.11 , take(X1, X2) -> n__take(X1, X2) 1041.03/297.11 , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) 1041.03/297.11 , take(s(M), cons(N, IL)) -> 1041.03/297.11 U91(and(and(isNatIList(activate(IL)), 1041.03/297.11 n__isNatIListKind(activate(IL))), 1041.03/297.11 n__and(n__and(n__isNat(M), n__isNatKind(M)), 1041.03/297.11 n__and(n__isNat(N), n__isNatKind(N)))), 1041.03/297.11 activate(IL), 1041.03/297.11 M, 1041.03/297.11 N) } 1041.03/297.11 Obligation: 1041.03/297.11 innermost runtime complexity 1041.03/297.11 Answer: 1041.03/297.11 MAYBE 1041.03/297.11 1041.03/297.11 Arguments of following rules are not normal-forms: 1041.03/297.11 1041.03/297.11 { length(cons(N, L)) -> 1041.03/297.11 U71(and(and(isNatList(activate(L)), 1041.03/297.11 n__isNatIListKind(activate(L))), 1041.03/297.11 n__and(n__isNat(N), n__isNatKind(N))), 1041.03/297.11 activate(L)) 1041.03/297.11 , length(nil()) -> 0() 1041.03/297.11 , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) 1041.03/297.11 , take(s(M), cons(N, IL)) -> 1041.03/297.11 U91(and(and(isNatIList(activate(IL)), 1041.03/297.11 n__isNatIListKind(activate(IL))), 1041.03/297.11 n__and(n__and(n__isNat(M), n__isNatKind(M)), 1041.03/297.11 n__and(n__isNat(N), n__isNatKind(N)))), 1041.03/297.11 activate(IL), 1041.03/297.11 M, 1041.03/297.11 N) } 1041.03/297.11 1041.03/297.11 All above mentioned rules can be savely removed. 1041.03/297.11 1041.03/297.11 We are left with following problem, upon which TcT provides the 1041.03/297.11 certificate MAYBE. 1041.03/297.11 1041.03/297.11 Strict Trs: 1041.03/297.11 { zeros() -> cons(0(), n__zeros()) 1041.03/297.11 , zeros() -> n__zeros() 1041.03/297.11 , cons(X1, X2) -> n__cons(X1, X2) 1041.03/297.11 , 0() -> n__0() 1041.03/297.11 , U11(tt(), V1) -> U12(isNatList(activate(V1))) 1041.03/297.11 , U12(tt()) -> tt() 1041.03/297.11 , isNatList(n__take(V1, V2)) -> 1041.03/297.11 U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 1041.03/297.11 activate(V1), 1041.03/297.11 activate(V2)) 1041.03/297.11 , isNatList(n__cons(V1, V2)) -> 1041.03/297.11 U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 1041.03/297.11 activate(V1), 1041.03/297.11 activate(V2)) 1041.03/297.11 , isNatList(n__nil()) -> tt() 1041.03/297.11 , activate(X) -> X 1041.03/297.11 , activate(n__zeros()) -> zeros() 1041.03/297.11 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1041.03/297.11 , activate(n__0()) -> 0() 1041.03/297.11 , activate(n__length(X)) -> length(activate(X)) 1041.03/297.11 , activate(n__s(X)) -> s(activate(X)) 1041.03/297.11 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1041.03/297.11 , activate(n__isNatIListKind(X)) -> isNatIListKind(X) 1041.03/297.11 , activate(n__nil()) -> nil() 1041.03/297.11 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 1041.03/297.11 , activate(n__isNat(X)) -> isNat(X) 1041.03/297.11 , activate(n__isNatKind(X)) -> isNatKind(X) 1041.03/297.11 , U21(tt(), V1) -> U22(isNat(activate(V1))) 1041.03/297.11 , U22(tt()) -> tt() 1041.03/297.11 , isNat(X) -> n__isNat(X) 1041.03/297.11 , isNat(n__0()) -> tt() 1041.03/297.11 , isNat(n__length(V1)) -> 1041.03/297.11 U11(isNatIListKind(activate(V1)), activate(V1)) 1041.03/297.11 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 1041.03/297.11 , U31(tt(), V) -> U32(isNatList(activate(V))) 1041.03/297.11 , U32(tt()) -> tt() 1041.03/297.11 , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) 1041.03/297.11 , U42(tt(), V2) -> U43(isNatIList(activate(V2))) 1041.03/297.11 , U43(tt()) -> tt() 1041.03/297.11 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 1041.03/297.11 , isNatIList(n__zeros()) -> tt() 1041.03/297.11 , isNatIList(n__cons(V1, V2)) -> 1041.03/297.11 U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 1041.03/297.11 activate(V1), 1041.03/297.11 activate(V2)) 1041.03/297.11 , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) 1041.03/297.11 , U52(tt(), V2) -> U53(isNatList(activate(V2))) 1041.03/297.11 , U53(tt()) -> tt() 1041.03/297.11 , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) 1041.03/297.11 , U62(tt(), V2) -> U63(isNatIList(activate(V2))) 1041.03/297.11 , U63(tt()) -> tt() 1041.03/297.11 , U71(tt(), L) -> s(length(activate(L))) 1041.03/297.11 , s(X) -> n__s(X) 1041.03/297.11 , length(X) -> n__length(X) 1041.03/297.11 , U81(tt()) -> nil() 1041.03/297.11 , nil() -> n__nil() 1041.03/297.11 , U91(tt(), IL, M, N) -> 1041.03/297.11 cons(activate(N), n__take(activate(M), activate(IL))) 1041.03/297.11 , and(X1, X2) -> n__and(X1, X2) 1041.03/297.11 , and(tt(), X) -> activate(X) 1041.03/297.11 , isNatIListKind(X) -> n__isNatIListKind(X) 1041.03/297.11 , isNatIListKind(n__zeros()) -> tt() 1041.03/297.11 , isNatIListKind(n__take(V1, V2)) -> 1041.03/297.11 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 1041.03/297.11 , isNatIListKind(n__cons(V1, V2)) -> 1041.03/297.11 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 1041.03/297.11 , isNatIListKind(n__nil()) -> tt() 1041.03/297.11 , isNatKind(X) -> n__isNatKind(X) 1041.03/297.11 , isNatKind(n__0()) -> tt() 1041.03/297.11 , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) 1041.03/297.11 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 1041.03/297.11 , take(X1, X2) -> n__take(X1, X2) } 1041.03/297.11 Obligation: 1041.03/297.11 innermost runtime complexity 1041.03/297.11 Answer: 1041.03/297.11 MAYBE 1041.03/297.11 1041.03/297.11 None of the processors succeeded. 1041.03/297.11 1041.03/297.11 Details of failed attempt(s): 1041.03/297.11 ----------------------------- 1041.03/297.11 1) 'empty' failed due to the following reason: 1041.03/297.11 1041.03/297.11 Empty strict component of the problem is NOT empty. 1041.03/297.11 1041.03/297.11 2) 'Best' failed due to the following reason: 1041.03/297.11 1041.03/297.11 None of the processors succeeded. 1041.03/297.11 1041.03/297.11 Details of failed attempt(s): 1041.03/297.11 ----------------------------- 1041.03/297.11 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1041.03/297.11 following reason: 1041.03/297.11 1041.03/297.11 Computation stopped due to timeout after 297.0 seconds. 1041.03/297.11 1041.03/297.11 2) 'Best' failed due to the following reason: 1041.03/297.11 1041.03/297.11 None of the processors succeeded. 1041.03/297.11 1041.03/297.11 Details of failed attempt(s): 1041.03/297.11 ----------------------------- 1041.03/297.11 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1041.03/297.11 seconds)' failed due to the following reason: 1041.03/297.11 1041.03/297.11 Computation stopped due to timeout after 148.0 seconds. 1041.03/297.11 1041.03/297.11 2) 'Best' failed due to the following reason: 1041.03/297.11 1041.03/297.11 None of the processors succeeded. 1041.03/297.11 1041.03/297.11 Details of failed attempt(s): 1041.03/297.11 ----------------------------- 1041.03/297.11 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1041.03/297.11 following reason: 1041.03/297.11 1041.03/297.11 The input cannot be shown compatible 1041.03/297.11 1041.03/297.11 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1041.03/297.11 to the following reason: 1041.03/297.11 1041.03/297.11 The input cannot be shown compatible 1041.03/297.11 1041.03/297.11 1041.03/297.11 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1041.03/297.11 failed due to the following reason: 1041.03/297.11 1041.03/297.11 None of the processors succeeded. 1041.03/297.11 1041.03/297.11 Details of failed attempt(s): 1041.03/297.11 ----------------------------- 1041.03/297.11 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1041.03/297.11 failed due to the following reason: 1041.03/297.11 1041.03/297.11 match-boundness of the problem could not be verified. 1041.03/297.11 1041.03/297.11 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1041.03/297.11 failed due to the following reason: 1041.03/297.11 1041.03/297.11 match-boundness of the problem could not be verified. 1041.03/297.11 1041.03/297.11 1041.03/297.11 1041.03/297.11 1041.03/297.11 1041.03/297.11 Arrrr.. 1043.67/299.70 EOF