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