MAYBE 931.67/297.04 MAYBE 931.67/297.04 931.67/297.04 We are left with following problem, upon which TcT provides the 931.67/297.04 certificate MAYBE. 931.67/297.04 931.67/297.04 Strict Trs: 931.67/297.04 { a__and(X1, X2) -> and(X1, X2) 931.67/297.04 , a__and(tt(), T) -> mark(T) 931.67/297.04 , mark(tt()) -> tt() 931.67/297.04 , mark(0()) -> 0() 931.67/297.04 , mark(s(X)) -> s(mark(X)) 931.67/297.04 , mark(length(X)) -> a__length(mark(X)) 931.67/297.04 , mark(zeros()) -> a__zeros() 931.67/297.04 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 931.67/297.04 , mark(nil()) -> nil() 931.67/297.04 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 931.67/297.04 , mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)) 931.67/297.04 , mark(isNatIList(X)) -> a__isNatIList(X) 931.67/297.04 , mark(isNatList(X)) -> a__isNatList(X) 931.67/297.04 , mark(isNat(X)) -> a__isNat(X) 931.67/297.04 , mark(uTake1(X)) -> a__uTake1(mark(X)) 931.67/297.04 , mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4) 931.67/297.04 , mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2) 931.67/297.04 , a__isNatIList(IL) -> a__isNatList(IL) 931.67/297.04 , a__isNatIList(X) -> isNatIList(X) 931.67/297.04 , a__isNatIList(zeros()) -> tt() 931.67/297.04 , a__isNatIList(cons(N, IL)) -> 931.67/297.04 a__and(a__isNat(N), a__isNatIList(IL)) 931.67/297.04 , a__isNatList(X) -> isNatList(X) 931.67/297.04 , a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)) 931.67/297.04 , a__isNatList(nil()) -> tt() 931.67/297.04 , a__isNatList(take(N, IL)) -> 931.67/297.04 a__and(a__isNat(N), a__isNatIList(IL)) 931.67/297.04 , a__isNat(X) -> isNat(X) 931.67/297.04 , a__isNat(0()) -> tt() 931.67/297.04 , a__isNat(s(N)) -> a__isNat(N) 931.67/297.04 , a__isNat(length(L)) -> a__isNatList(L) 931.67/297.04 , a__zeros() -> zeros() 931.67/297.04 , a__zeros() -> cons(0(), zeros()) 931.67/297.04 , a__take(X1, X2) -> take(X1, X2) 931.67/297.04 , a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)) 931.67/297.04 , a__take(s(M), cons(N, IL)) -> 931.67/297.04 a__uTake2(a__and(a__isNat(M), 931.67/297.04 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.04 M, 931.67/297.04 N, 931.67/297.04 IL) 931.67/297.04 , a__uTake1(X) -> uTake1(X) 931.67/297.04 , a__uTake1(tt()) -> nil() 931.67/297.04 , a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4) 931.67/297.04 , a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)) 931.67/297.04 , a__length(X) -> length(X) 931.67/297.04 , a__length(cons(N, L)) -> 931.67/297.04 a__uLength(a__and(a__isNat(N), a__isNatList(L)), L) 931.67/297.04 , a__uLength(X1, X2) -> uLength(X1, X2) 931.67/297.04 , a__uLength(tt(), L) -> s(a__length(mark(L))) } 931.67/297.04 Obligation: 931.67/297.04 runtime complexity 931.67/297.04 Answer: 931.67/297.04 MAYBE 931.67/297.04 931.67/297.04 None of the processors succeeded. 931.67/297.04 931.67/297.04 Details of failed attempt(s): 931.67/297.04 ----------------------------- 931.67/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 931.67/297.04 following reason: 931.67/297.04 931.67/297.04 Computation stopped due to timeout after 297.0 seconds. 931.67/297.04 931.67/297.04 2) 'Best' failed due to the following reason: 931.67/297.04 931.67/297.04 None of the processors succeeded. 931.67/297.04 931.67/297.04 Details of failed attempt(s): 931.67/297.04 ----------------------------- 931.67/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 931.67/297.04 seconds)' failed due to the following reason: 931.67/297.04 931.67/297.04 Computation stopped due to timeout after 148.0 seconds. 931.67/297.04 931.67/297.04 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 931.67/297.04 failed due to the following reason: 931.67/297.04 931.67/297.04 None of the processors succeeded. 931.67/297.04 931.67/297.04 Details of failed attempt(s): 931.67/297.04 ----------------------------- 931.67/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 931.67/297.04 failed due to the following reason: 931.67/297.04 931.67/297.04 match-boundness of the problem could not be verified. 931.67/297.04 931.67/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 931.67/297.04 failed due to the following reason: 931.67/297.04 931.67/297.04 match-boundness of the problem could not be verified. 931.67/297.04 931.67/297.04 931.67/297.04 3) 'Best' failed due to the following reason: 931.67/297.04 931.67/297.04 None of the processors succeeded. 931.67/297.04 931.67/297.04 Details of failed attempt(s): 931.67/297.04 ----------------------------- 931.67/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 931.67/297.04 following reason: 931.67/297.04 931.67/297.04 The processor is inapplicable, reason: 931.67/297.04 Processor only applicable for innermost runtime complexity analysis 931.67/297.04 931.67/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 931.67/297.04 to the following reason: 931.67/297.04 931.67/297.04 The processor is inapplicable, reason: 931.67/297.04 Processor only applicable for innermost runtime complexity analysis 931.67/297.04 931.67/297.04 931.67/297.04 931.67/297.04 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 931.67/297.04 the following reason: 931.67/297.04 931.67/297.04 We add the following weak dependency pairs: 931.67/297.04 931.67/297.04 Strict DPs: 931.67/297.04 { a__and^#(X1, X2) -> c_1(X1, X2) 931.67/297.04 , a__and^#(tt(), T) -> c_2(mark^#(T)) 931.67/297.04 , mark^#(tt()) -> c_3() 931.67/297.04 , mark^#(0()) -> c_4() 931.67/297.04 , mark^#(s(X)) -> c_5(mark^#(X)) 931.67/297.04 , mark^#(length(X)) -> c_6(a__length^#(mark(X))) 931.67/297.04 , mark^#(zeros()) -> c_7(a__zeros^#()) 931.67/297.04 , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2) 931.67/297.04 , mark^#(nil()) -> c_9() 931.67/297.04 , mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2))) 931.67/297.04 , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2))) 931.67/297.04 , mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X)) 931.67/297.04 , mark^#(isNatList(X)) -> c_13(a__isNatList^#(X)) 931.67/297.04 , mark^#(isNat(X)) -> c_14(a__isNat^#(X)) 931.67/297.04 , mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X))) 931.67/297.04 , mark^#(uTake2(X1, X2, X3, X4)) -> 931.67/297.04 c_16(a__uTake2^#(mark(X1), X2, X3, X4)) 931.67/297.04 , mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2)) 931.67/297.04 , a__length^#(X) -> c_39(X) 931.67/297.04 , a__length^#(cons(N, L)) -> 931.67/297.04 c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L)) 931.67/297.04 , a__zeros^#() -> c_30() 931.67/297.04 , a__zeros^#() -> c_31() 931.67/297.04 , a__take^#(X1, X2) -> c_32(X1, X2) 931.67/297.04 , a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL))) 931.67/297.04 , a__take^#(s(M), cons(N, IL)) -> 931.67/297.04 c_34(a__uTake2^#(a__and(a__isNat(M), 931.67/297.04 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.04 M, 931.67/297.04 N, 931.67/297.04 IL)) 931.67/297.04 , a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL)) 931.67/297.04 , a__isNatIList^#(X) -> c_19(X) 931.67/297.04 , a__isNatIList^#(zeros()) -> c_20() 931.67/297.04 , a__isNatIList^#(cons(N, IL)) -> 931.67/297.04 c_21(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.04 , a__isNatList^#(X) -> c_22(X) 931.67/297.04 , a__isNatList^#(cons(N, L)) -> 931.67/297.04 c_23(a__and^#(a__isNat(N), a__isNatList(L))) 931.67/297.04 , a__isNatList^#(nil()) -> c_24() 931.67/297.04 , a__isNatList^#(take(N, IL)) -> 931.67/297.04 c_25(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.04 , a__isNat^#(X) -> c_26(X) 931.67/297.04 , a__isNat^#(0()) -> c_27() 931.67/297.04 , a__isNat^#(s(N)) -> c_28(a__isNat^#(N)) 931.67/297.04 , a__isNat^#(length(L)) -> c_29(a__isNatList^#(L)) 931.67/297.04 , a__uTake1^#(X) -> c_35(X) 931.67/297.04 , a__uTake1^#(tt()) -> c_36() 931.67/297.04 , a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4) 931.67/297.04 , a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL) 931.67/297.04 , a__uLength^#(X1, X2) -> c_41(X1, X2) 931.67/297.04 , a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) } 931.67/297.04 931.67/297.04 and mark the set of starting terms. 931.67/297.04 931.67/297.04 We are left with following problem, upon which TcT provides the 931.67/297.04 certificate MAYBE. 931.67/297.04 931.67/297.04 Strict DPs: 931.67/297.04 { a__and^#(X1, X2) -> c_1(X1, X2) 931.67/297.04 , a__and^#(tt(), T) -> c_2(mark^#(T)) 931.67/297.04 , mark^#(tt()) -> c_3() 931.67/297.04 , mark^#(0()) -> c_4() 931.67/297.04 , mark^#(s(X)) -> c_5(mark^#(X)) 931.67/297.04 , mark^#(length(X)) -> c_6(a__length^#(mark(X))) 931.67/297.04 , mark^#(zeros()) -> c_7(a__zeros^#()) 931.67/297.04 , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2) 931.67/297.04 , mark^#(nil()) -> c_9() 931.67/297.04 , mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2))) 931.67/297.04 , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2))) 931.67/297.04 , mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X)) 931.67/297.04 , mark^#(isNatList(X)) -> c_13(a__isNatList^#(X)) 931.67/297.04 , mark^#(isNat(X)) -> c_14(a__isNat^#(X)) 931.67/297.04 , mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X))) 931.67/297.04 , mark^#(uTake2(X1, X2, X3, X4)) -> 931.67/297.04 c_16(a__uTake2^#(mark(X1), X2, X3, X4)) 931.67/297.04 , mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2)) 931.67/297.04 , a__length^#(X) -> c_39(X) 931.67/297.04 , a__length^#(cons(N, L)) -> 931.67/297.04 c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L)) 931.67/297.04 , a__zeros^#() -> c_30() 931.67/297.04 , a__zeros^#() -> c_31() 931.67/297.04 , a__take^#(X1, X2) -> c_32(X1, X2) 931.67/297.04 , a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL))) 931.67/297.04 , a__take^#(s(M), cons(N, IL)) -> 931.67/297.04 c_34(a__uTake2^#(a__and(a__isNat(M), 931.67/297.04 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.04 M, 931.67/297.04 N, 931.67/297.04 IL)) 931.67/297.04 , a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL)) 931.67/297.04 , a__isNatIList^#(X) -> c_19(X) 931.67/297.05 , a__isNatIList^#(zeros()) -> c_20() 931.67/297.05 , a__isNatIList^#(cons(N, IL)) -> 931.67/297.05 c_21(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , a__isNatList^#(X) -> c_22(X) 931.67/297.05 , a__isNatList^#(cons(N, L)) -> 931.67/297.05 c_23(a__and^#(a__isNat(N), a__isNatList(L))) 931.67/297.05 , a__isNatList^#(nil()) -> c_24() 931.67/297.05 , a__isNatList^#(take(N, IL)) -> 931.67/297.05 c_25(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , a__isNat^#(X) -> c_26(X) 931.67/297.05 , a__isNat^#(0()) -> c_27() 931.67/297.05 , a__isNat^#(s(N)) -> c_28(a__isNat^#(N)) 931.67/297.05 , a__isNat^#(length(L)) -> c_29(a__isNatList^#(L)) 931.67/297.05 , a__uTake1^#(X) -> c_35(X) 931.67/297.05 , a__uTake1^#(tt()) -> c_36() 931.67/297.05 , a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4) 931.67/297.05 , a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL) 931.67/297.05 , a__uLength^#(X1, X2) -> c_41(X1, X2) 931.67/297.05 , a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) } 931.67/297.05 Strict Trs: 931.67/297.05 { a__and(X1, X2) -> and(X1, X2) 931.67/297.05 , a__and(tt(), T) -> mark(T) 931.67/297.05 , mark(tt()) -> tt() 931.67/297.05 , mark(0()) -> 0() 931.67/297.05 , mark(s(X)) -> s(mark(X)) 931.67/297.05 , mark(length(X)) -> a__length(mark(X)) 931.67/297.05 , mark(zeros()) -> a__zeros() 931.67/297.05 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 931.67/297.05 , mark(nil()) -> nil() 931.67/297.05 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 931.67/297.05 , mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)) 931.67/297.05 , mark(isNatIList(X)) -> a__isNatIList(X) 931.67/297.05 , mark(isNatList(X)) -> a__isNatList(X) 931.67/297.05 , mark(isNat(X)) -> a__isNat(X) 931.67/297.05 , mark(uTake1(X)) -> a__uTake1(mark(X)) 931.67/297.05 , mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4) 931.67/297.05 , mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2) 931.67/297.05 , a__isNatIList(IL) -> a__isNatList(IL) 931.67/297.05 , a__isNatIList(X) -> isNatIList(X) 931.67/297.05 , a__isNatIList(zeros()) -> tt() 931.67/297.05 , a__isNatIList(cons(N, IL)) -> 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL)) 931.67/297.05 , a__isNatList(X) -> isNatList(X) 931.67/297.05 , a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)) 931.67/297.05 , a__isNatList(nil()) -> tt() 931.67/297.05 , a__isNatList(take(N, IL)) -> 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL)) 931.67/297.05 , a__isNat(X) -> isNat(X) 931.67/297.05 , a__isNat(0()) -> tt() 931.67/297.05 , a__isNat(s(N)) -> a__isNat(N) 931.67/297.05 , a__isNat(length(L)) -> a__isNatList(L) 931.67/297.05 , a__zeros() -> zeros() 931.67/297.05 , a__zeros() -> cons(0(), zeros()) 931.67/297.05 , a__take(X1, X2) -> take(X1, X2) 931.67/297.05 , a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)) 931.67/297.05 , a__take(s(M), cons(N, IL)) -> 931.67/297.05 a__uTake2(a__and(a__isNat(M), 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.05 M, 931.67/297.05 N, 931.67/297.05 IL) 931.67/297.05 , a__uTake1(X) -> uTake1(X) 931.67/297.05 , a__uTake1(tt()) -> nil() 931.67/297.05 , a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4) 931.67/297.05 , a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)) 931.67/297.05 , a__length(X) -> length(X) 931.67/297.05 , a__length(cons(N, L)) -> 931.67/297.05 a__uLength(a__and(a__isNat(N), a__isNatList(L)), L) 931.67/297.05 , a__uLength(X1, X2) -> uLength(X1, X2) 931.67/297.05 , a__uLength(tt(), L) -> s(a__length(mark(L))) } 931.67/297.05 Obligation: 931.67/297.05 runtime complexity 931.67/297.05 Answer: 931.67/297.05 MAYBE 931.67/297.05 931.67/297.05 We estimate the number of application of {3,4,9,20,21,27,31,34,38} 931.67/297.05 by applications of Pre({3,4,9,20,21,27,31,34,38}) = 931.67/297.05 {1,2,5,7,8,12,13,14,15,18,22,23,25,26,29,33,35,36,37,39,40,41}. 931.67/297.05 Here rules are labeled as follows: 931.67/297.05 931.67/297.05 DPs: 931.67/297.05 { 1: a__and^#(X1, X2) -> c_1(X1, X2) 931.67/297.05 , 2: a__and^#(tt(), T) -> c_2(mark^#(T)) 931.67/297.05 , 3: mark^#(tt()) -> c_3() 931.67/297.05 , 4: mark^#(0()) -> c_4() 931.67/297.05 , 5: mark^#(s(X)) -> c_5(mark^#(X)) 931.67/297.05 , 6: mark^#(length(X)) -> c_6(a__length^#(mark(X))) 931.67/297.05 , 7: mark^#(zeros()) -> c_7(a__zeros^#()) 931.67/297.05 , 8: mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2) 931.67/297.05 , 9: mark^#(nil()) -> c_9() 931.67/297.05 , 10: mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2))) 931.67/297.05 , 11: mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2))) 931.67/297.05 , 12: mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X)) 931.67/297.05 , 13: mark^#(isNatList(X)) -> c_13(a__isNatList^#(X)) 931.67/297.05 , 14: mark^#(isNat(X)) -> c_14(a__isNat^#(X)) 931.67/297.05 , 15: mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X))) 931.67/297.05 , 16: mark^#(uTake2(X1, X2, X3, X4)) -> 931.67/297.05 c_16(a__uTake2^#(mark(X1), X2, X3, X4)) 931.67/297.05 , 17: mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2)) 931.67/297.05 , 18: a__length^#(X) -> c_39(X) 931.67/297.05 , 19: a__length^#(cons(N, L)) -> 931.67/297.05 c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L)) 931.67/297.05 , 20: a__zeros^#() -> c_30() 931.67/297.05 , 21: a__zeros^#() -> c_31() 931.67/297.05 , 22: a__take^#(X1, X2) -> c_32(X1, X2) 931.67/297.05 , 23: a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL))) 931.67/297.05 , 24: a__take^#(s(M), cons(N, IL)) -> 931.67/297.05 c_34(a__uTake2^#(a__and(a__isNat(M), 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.05 M, 931.67/297.05 N, 931.67/297.05 IL)) 931.67/297.05 , 25: a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL)) 931.67/297.05 , 26: a__isNatIList^#(X) -> c_19(X) 931.67/297.05 , 27: a__isNatIList^#(zeros()) -> c_20() 931.67/297.05 , 28: a__isNatIList^#(cons(N, IL)) -> 931.67/297.05 c_21(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , 29: a__isNatList^#(X) -> c_22(X) 931.67/297.05 , 30: a__isNatList^#(cons(N, L)) -> 931.67/297.05 c_23(a__and^#(a__isNat(N), a__isNatList(L))) 931.67/297.05 , 31: a__isNatList^#(nil()) -> c_24() 931.67/297.05 , 32: a__isNatList^#(take(N, IL)) -> 931.67/297.05 c_25(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , 33: a__isNat^#(X) -> c_26(X) 931.67/297.05 , 34: a__isNat^#(0()) -> c_27() 931.67/297.05 , 35: a__isNat^#(s(N)) -> c_28(a__isNat^#(N)) 931.67/297.05 , 36: a__isNat^#(length(L)) -> c_29(a__isNatList^#(L)) 931.67/297.05 , 37: a__uTake1^#(X) -> c_35(X) 931.67/297.05 , 38: a__uTake1^#(tt()) -> c_36() 931.67/297.05 , 39: a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4) 931.67/297.05 , 40: a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL) 931.67/297.05 , 41: a__uLength^#(X1, X2) -> c_41(X1, X2) 931.67/297.05 , 42: a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) } 931.67/297.05 931.67/297.05 We are left with following problem, upon which TcT provides the 931.67/297.05 certificate MAYBE. 931.67/297.05 931.67/297.05 Strict DPs: 931.67/297.05 { a__and^#(X1, X2) -> c_1(X1, X2) 931.67/297.05 , a__and^#(tt(), T) -> c_2(mark^#(T)) 931.67/297.05 , mark^#(s(X)) -> c_5(mark^#(X)) 931.67/297.05 , mark^#(length(X)) -> c_6(a__length^#(mark(X))) 931.67/297.05 , mark^#(zeros()) -> c_7(a__zeros^#()) 931.67/297.05 , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2) 931.67/297.05 , mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2))) 931.67/297.05 , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2))) 931.67/297.05 , mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X)) 931.67/297.05 , mark^#(isNatList(X)) -> c_13(a__isNatList^#(X)) 931.67/297.05 , mark^#(isNat(X)) -> c_14(a__isNat^#(X)) 931.67/297.05 , mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X))) 931.67/297.05 , mark^#(uTake2(X1, X2, X3, X4)) -> 931.67/297.05 c_16(a__uTake2^#(mark(X1), X2, X3, X4)) 931.67/297.05 , mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2)) 931.67/297.05 , a__length^#(X) -> c_39(X) 931.67/297.05 , a__length^#(cons(N, L)) -> 931.67/297.05 c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L)) 931.67/297.05 , a__take^#(X1, X2) -> c_32(X1, X2) 931.67/297.05 , a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL))) 931.67/297.05 , a__take^#(s(M), cons(N, IL)) -> 931.67/297.05 c_34(a__uTake2^#(a__and(a__isNat(M), 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.05 M, 931.67/297.05 N, 931.67/297.05 IL)) 931.67/297.05 , a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL)) 931.67/297.05 , a__isNatIList^#(X) -> c_19(X) 931.67/297.05 , a__isNatIList^#(cons(N, IL)) -> 931.67/297.05 c_21(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , a__isNatList^#(X) -> c_22(X) 931.67/297.05 , a__isNatList^#(cons(N, L)) -> 931.67/297.05 c_23(a__and^#(a__isNat(N), a__isNatList(L))) 931.67/297.05 , a__isNatList^#(take(N, IL)) -> 931.67/297.05 c_25(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , a__isNat^#(X) -> c_26(X) 931.67/297.05 , a__isNat^#(s(N)) -> c_28(a__isNat^#(N)) 931.67/297.05 , a__isNat^#(length(L)) -> c_29(a__isNatList^#(L)) 931.67/297.05 , a__uTake1^#(X) -> c_35(X) 931.67/297.05 , a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4) 931.67/297.05 , a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL) 931.67/297.05 , a__uLength^#(X1, X2) -> c_41(X1, X2) 931.67/297.05 , a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) } 931.67/297.05 Strict Trs: 931.67/297.05 { a__and(X1, X2) -> and(X1, X2) 931.67/297.05 , a__and(tt(), T) -> mark(T) 931.67/297.05 , mark(tt()) -> tt() 931.67/297.05 , mark(0()) -> 0() 931.67/297.05 , mark(s(X)) -> s(mark(X)) 931.67/297.05 , mark(length(X)) -> a__length(mark(X)) 931.67/297.05 , mark(zeros()) -> a__zeros() 931.67/297.05 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 931.67/297.05 , mark(nil()) -> nil() 931.67/297.05 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 931.67/297.05 , mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)) 931.67/297.05 , mark(isNatIList(X)) -> a__isNatIList(X) 931.67/297.05 , mark(isNatList(X)) -> a__isNatList(X) 931.67/297.05 , mark(isNat(X)) -> a__isNat(X) 931.67/297.05 , mark(uTake1(X)) -> a__uTake1(mark(X)) 931.67/297.05 , mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4) 931.67/297.05 , mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2) 931.67/297.05 , a__isNatIList(IL) -> a__isNatList(IL) 931.67/297.05 , a__isNatIList(X) -> isNatIList(X) 931.67/297.05 , a__isNatIList(zeros()) -> tt() 931.67/297.05 , a__isNatIList(cons(N, IL)) -> 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL)) 931.67/297.05 , a__isNatList(X) -> isNatList(X) 931.67/297.05 , a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)) 931.67/297.05 , a__isNatList(nil()) -> tt() 931.67/297.05 , a__isNatList(take(N, IL)) -> 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL)) 931.67/297.05 , a__isNat(X) -> isNat(X) 931.67/297.05 , a__isNat(0()) -> tt() 931.67/297.05 , a__isNat(s(N)) -> a__isNat(N) 931.67/297.05 , a__isNat(length(L)) -> a__isNatList(L) 931.67/297.05 , a__zeros() -> zeros() 931.67/297.05 , a__zeros() -> cons(0(), zeros()) 931.67/297.05 , a__take(X1, X2) -> take(X1, X2) 931.67/297.05 , a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)) 931.67/297.05 , a__take(s(M), cons(N, IL)) -> 931.67/297.05 a__uTake2(a__and(a__isNat(M), 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.05 M, 931.67/297.05 N, 931.67/297.05 IL) 931.67/297.05 , a__uTake1(X) -> uTake1(X) 931.67/297.05 , a__uTake1(tt()) -> nil() 931.67/297.05 , a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4) 931.67/297.05 , a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)) 931.67/297.05 , a__length(X) -> length(X) 931.67/297.05 , a__length(cons(N, L)) -> 931.67/297.05 a__uLength(a__and(a__isNat(N), a__isNatList(L)), L) 931.67/297.05 , a__uLength(X1, X2) -> uLength(X1, X2) 931.67/297.05 , a__uLength(tt(), L) -> s(a__length(mark(L))) } 931.67/297.05 Weak DPs: 931.67/297.05 { mark^#(tt()) -> c_3() 931.67/297.05 , mark^#(0()) -> c_4() 931.67/297.05 , mark^#(nil()) -> c_9() 931.67/297.05 , a__zeros^#() -> c_30() 931.67/297.05 , a__zeros^#() -> c_31() 931.67/297.05 , a__isNatIList^#(zeros()) -> c_20() 931.67/297.05 , a__isNatList^#(nil()) -> c_24() 931.67/297.05 , a__isNat^#(0()) -> c_27() 931.67/297.05 , a__uTake1^#(tt()) -> c_36() } 931.67/297.05 Obligation: 931.67/297.05 runtime complexity 931.67/297.05 Answer: 931.67/297.05 MAYBE 931.67/297.05 931.67/297.05 We estimate the number of application of {5} by applications of 931.67/297.05 Pre({5}) = {1,2,3,6,15,17,21,23,26,29,30,31,32}. Here rules are 931.67/297.05 labeled as follows: 931.67/297.05 931.67/297.05 DPs: 931.67/297.05 { 1: a__and^#(X1, X2) -> c_1(X1, X2) 931.67/297.05 , 2: a__and^#(tt(), T) -> c_2(mark^#(T)) 931.67/297.05 , 3: mark^#(s(X)) -> c_5(mark^#(X)) 931.67/297.05 , 4: mark^#(length(X)) -> c_6(a__length^#(mark(X))) 931.67/297.05 , 5: mark^#(zeros()) -> c_7(a__zeros^#()) 931.67/297.05 , 6: mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2) 931.67/297.05 , 7: mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2))) 931.67/297.05 , 8: mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2))) 931.67/297.05 , 9: mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X)) 931.67/297.05 , 10: mark^#(isNatList(X)) -> c_13(a__isNatList^#(X)) 931.67/297.05 , 11: mark^#(isNat(X)) -> c_14(a__isNat^#(X)) 931.67/297.05 , 12: mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X))) 931.67/297.05 , 13: mark^#(uTake2(X1, X2, X3, X4)) -> 931.67/297.05 c_16(a__uTake2^#(mark(X1), X2, X3, X4)) 931.67/297.05 , 14: mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2)) 931.67/297.05 , 15: a__length^#(X) -> c_39(X) 931.67/297.05 , 16: a__length^#(cons(N, L)) -> 931.67/297.05 c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L)) 931.67/297.05 , 17: a__take^#(X1, X2) -> c_32(X1, X2) 931.67/297.05 , 18: a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL))) 931.67/297.05 , 19: a__take^#(s(M), cons(N, IL)) -> 931.67/297.05 c_34(a__uTake2^#(a__and(a__isNat(M), 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.05 M, 931.67/297.05 N, 931.67/297.05 IL)) 931.67/297.05 , 20: a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL)) 931.67/297.05 , 21: a__isNatIList^#(X) -> c_19(X) 931.67/297.05 , 22: a__isNatIList^#(cons(N, IL)) -> 931.67/297.05 c_21(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , 23: a__isNatList^#(X) -> c_22(X) 931.67/297.05 , 24: a__isNatList^#(cons(N, L)) -> 931.67/297.05 c_23(a__and^#(a__isNat(N), a__isNatList(L))) 931.67/297.05 , 25: a__isNatList^#(take(N, IL)) -> 931.67/297.05 c_25(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , 26: a__isNat^#(X) -> c_26(X) 931.67/297.05 , 27: a__isNat^#(s(N)) -> c_28(a__isNat^#(N)) 931.67/297.05 , 28: a__isNat^#(length(L)) -> c_29(a__isNatList^#(L)) 931.67/297.05 , 29: a__uTake1^#(X) -> c_35(X) 931.67/297.05 , 30: a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4) 931.67/297.05 , 31: a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL) 931.67/297.05 , 32: a__uLength^#(X1, X2) -> c_41(X1, X2) 931.67/297.05 , 33: a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) 931.67/297.05 , 34: mark^#(tt()) -> c_3() 931.67/297.05 , 35: mark^#(0()) -> c_4() 931.67/297.05 , 36: mark^#(nil()) -> c_9() 931.67/297.05 , 37: a__zeros^#() -> c_30() 931.67/297.05 , 38: a__zeros^#() -> c_31() 931.67/297.05 , 39: a__isNatIList^#(zeros()) -> c_20() 931.67/297.05 , 40: a__isNatList^#(nil()) -> c_24() 931.67/297.05 , 41: a__isNat^#(0()) -> c_27() 931.67/297.05 , 42: a__uTake1^#(tt()) -> c_36() } 931.67/297.05 931.67/297.05 We are left with following problem, upon which TcT provides the 931.67/297.05 certificate MAYBE. 931.67/297.05 931.67/297.05 Strict DPs: 931.67/297.05 { a__and^#(X1, X2) -> c_1(X1, X2) 931.67/297.05 , a__and^#(tt(), T) -> c_2(mark^#(T)) 931.67/297.05 , mark^#(s(X)) -> c_5(mark^#(X)) 931.67/297.05 , mark^#(length(X)) -> c_6(a__length^#(mark(X))) 931.67/297.05 , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2) 931.67/297.05 , mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2))) 931.67/297.05 , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2))) 931.67/297.05 , mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X)) 931.67/297.05 , mark^#(isNatList(X)) -> c_13(a__isNatList^#(X)) 931.67/297.05 , mark^#(isNat(X)) -> c_14(a__isNat^#(X)) 931.67/297.05 , mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X))) 931.67/297.05 , mark^#(uTake2(X1, X2, X3, X4)) -> 931.67/297.05 c_16(a__uTake2^#(mark(X1), X2, X3, X4)) 931.67/297.05 , mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2)) 931.67/297.05 , a__length^#(X) -> c_39(X) 931.67/297.05 , a__length^#(cons(N, L)) -> 931.67/297.05 c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L)) 931.67/297.05 , a__take^#(X1, X2) -> c_32(X1, X2) 931.67/297.05 , a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL))) 931.67/297.05 , a__take^#(s(M), cons(N, IL)) -> 931.67/297.05 c_34(a__uTake2^#(a__and(a__isNat(M), 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.05 M, 931.67/297.05 N, 931.67/297.05 IL)) 931.67/297.05 , a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL)) 931.67/297.05 , a__isNatIList^#(X) -> c_19(X) 931.67/297.05 , a__isNatIList^#(cons(N, IL)) -> 931.67/297.05 c_21(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , a__isNatList^#(X) -> c_22(X) 931.67/297.05 , a__isNatList^#(cons(N, L)) -> 931.67/297.05 c_23(a__and^#(a__isNat(N), a__isNatList(L))) 931.67/297.05 , a__isNatList^#(take(N, IL)) -> 931.67/297.05 c_25(a__and^#(a__isNat(N), a__isNatIList(IL))) 931.67/297.05 , a__isNat^#(X) -> c_26(X) 931.67/297.05 , a__isNat^#(s(N)) -> c_28(a__isNat^#(N)) 931.67/297.05 , a__isNat^#(length(L)) -> c_29(a__isNatList^#(L)) 931.67/297.05 , a__uTake1^#(X) -> c_35(X) 931.67/297.05 , a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4) 931.67/297.05 , a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL) 931.67/297.05 , a__uLength^#(X1, X2) -> c_41(X1, X2) 931.67/297.05 , a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) } 931.67/297.05 Strict Trs: 931.67/297.05 { a__and(X1, X2) -> and(X1, X2) 931.67/297.05 , a__and(tt(), T) -> mark(T) 931.67/297.05 , mark(tt()) -> tt() 931.67/297.05 , mark(0()) -> 0() 931.67/297.05 , mark(s(X)) -> s(mark(X)) 931.67/297.05 , mark(length(X)) -> a__length(mark(X)) 931.67/297.05 , mark(zeros()) -> a__zeros() 931.67/297.05 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 931.67/297.05 , mark(nil()) -> nil() 931.67/297.05 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 931.67/297.05 , mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)) 931.67/297.05 , mark(isNatIList(X)) -> a__isNatIList(X) 931.67/297.05 , mark(isNatList(X)) -> a__isNatList(X) 931.67/297.05 , mark(isNat(X)) -> a__isNat(X) 931.67/297.05 , mark(uTake1(X)) -> a__uTake1(mark(X)) 931.67/297.05 , mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4) 931.67/297.05 , mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2) 931.67/297.05 , a__isNatIList(IL) -> a__isNatList(IL) 931.67/297.05 , a__isNatIList(X) -> isNatIList(X) 931.67/297.05 , a__isNatIList(zeros()) -> tt() 931.67/297.05 , a__isNatIList(cons(N, IL)) -> 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL)) 931.67/297.05 , a__isNatList(X) -> isNatList(X) 931.67/297.05 , a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)) 931.67/297.05 , a__isNatList(nil()) -> tt() 931.67/297.05 , a__isNatList(take(N, IL)) -> 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL)) 931.67/297.05 , a__isNat(X) -> isNat(X) 931.67/297.05 , a__isNat(0()) -> tt() 931.67/297.05 , a__isNat(s(N)) -> a__isNat(N) 931.67/297.05 , a__isNat(length(L)) -> a__isNatList(L) 931.67/297.05 , a__zeros() -> zeros() 931.67/297.05 , a__zeros() -> cons(0(), zeros()) 931.67/297.05 , a__take(X1, X2) -> take(X1, X2) 931.67/297.05 , a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)) 931.67/297.05 , a__take(s(M), cons(N, IL)) -> 931.67/297.05 a__uTake2(a__and(a__isNat(M), 931.67/297.05 a__and(a__isNat(N), a__isNatIList(IL))), 931.67/297.05 M, 931.67/297.05 N, 931.67/297.05 IL) 931.67/297.05 , a__uTake1(X) -> uTake1(X) 931.67/297.05 , a__uTake1(tt()) -> nil() 931.67/297.05 , a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4) 931.67/297.05 , a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)) 931.67/297.05 , a__length(X) -> length(X) 931.67/297.05 , a__length(cons(N, L)) -> 931.67/297.05 a__uLength(a__and(a__isNat(N), a__isNatList(L)), L) 931.67/297.05 , a__uLength(X1, X2) -> uLength(X1, X2) 931.67/297.05 , a__uLength(tt(), L) -> s(a__length(mark(L))) } 931.67/297.05 Weak DPs: 931.67/297.05 { mark^#(tt()) -> c_3() 931.67/297.05 , mark^#(0()) -> c_4() 931.67/297.05 , mark^#(zeros()) -> c_7(a__zeros^#()) 931.67/297.05 , mark^#(nil()) -> c_9() 931.67/297.05 , a__zeros^#() -> c_30() 931.67/297.05 , a__zeros^#() -> c_31() 931.67/297.05 , a__isNatIList^#(zeros()) -> c_20() 931.67/297.05 , a__isNatList^#(nil()) -> c_24() 931.67/297.05 , a__isNat^#(0()) -> c_27() 931.67/297.05 , a__uTake1^#(tt()) -> c_36() } 931.67/297.05 Obligation: 931.67/297.05 runtime complexity 931.67/297.05 Answer: 931.67/297.05 MAYBE 931.67/297.05 931.67/297.05 Empty strict component of the problem is NOT empty. 931.67/297.05 931.67/297.05 931.67/297.05 Arrrr.. 931.67/297.07 EOF