MAYBE 1061.64/298.17 MAYBE 1061.64/298.17 1061.64/298.17 We are left with following problem, upon which TcT provides the 1061.64/298.17 certificate MAYBE. 1061.64/298.17 1061.64/298.17 Strict Trs: 1061.64/298.17 { active(and(X1, X2)) -> and(X1, active(X2)) 1061.64/298.17 , active(and(X1, X2)) -> and(active(X1), X2) 1061.64/298.17 , active(and(tt(), T)) -> mark(T) 1061.64/298.17 , active(isNatIList(IL)) -> mark(isNatList(IL)) 1061.64/298.17 , active(isNatIList(zeros())) -> mark(tt()) 1061.64/298.17 , active(isNatIList(cons(N, IL))) -> 1061.64/298.17 mark(and(isNat(N), isNatIList(IL))) 1061.64/298.17 , active(isNatList(cons(N, L))) -> 1061.64/298.17 mark(and(isNat(N), isNatList(L))) 1061.64/298.17 , active(isNatList(nil())) -> mark(tt()) 1061.64/298.17 , active(isNatList(take(N, IL))) -> 1061.64/298.17 mark(and(isNat(N), isNatIList(IL))) 1061.64/298.17 , active(isNat(0())) -> mark(tt()) 1061.64/298.17 , active(isNat(s(N))) -> mark(isNat(N)) 1061.64/298.17 , active(isNat(length(L))) -> mark(isNatList(L)) 1061.64/298.17 , active(s(X)) -> s(active(X)) 1061.64/298.17 , active(length(X)) -> length(active(X)) 1061.64/298.17 , active(length(cons(N, L))) -> 1061.64/298.17 mark(uLength(and(isNat(N), isNatList(L)), L)) 1061.64/298.17 , active(zeros()) -> mark(cons(0(), zeros())) 1061.64/298.17 , active(cons(X1, X2)) -> cons(active(X1), X2) 1061.64/298.17 , active(take(X1, X2)) -> take(X1, active(X2)) 1061.64/298.17 , active(take(X1, X2)) -> take(active(X1), X2) 1061.64/298.17 , active(take(0(), IL)) -> mark(uTake1(isNatIList(IL))) 1061.64/298.17 , active(take(s(M), cons(N, IL))) -> 1061.64/298.17 mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), 1061.64/298.17 M, 1061.64/298.17 N, 1061.64/298.17 IL)) 1061.64/298.17 , active(uTake1(X)) -> uTake1(active(X)) 1061.64/298.17 , active(uTake1(tt())) -> mark(nil()) 1061.64/298.17 , active(uTake2(X1, X2, X3, X4)) -> uTake2(active(X1), X2, X3, X4) 1061.64/298.17 , active(uTake2(tt(), M, N, IL)) -> mark(cons(N, take(M, IL))) 1061.64/298.17 , active(uLength(X1, X2)) -> uLength(active(X1), X2) 1061.64/298.17 , active(uLength(tt(), L)) -> mark(s(length(L))) 1061.64/298.17 , and(X1, mark(X2)) -> mark(and(X1, X2)) 1061.64/298.17 , and(mark(X1), X2) -> mark(and(X1, X2)) 1061.64/298.17 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 1061.64/298.17 , isNatIList(ok(X)) -> ok(isNatIList(X)) 1061.64/298.17 , isNatList(ok(X)) -> ok(isNatList(X)) 1061.64/298.17 , isNat(ok(X)) -> ok(isNat(X)) 1061.64/298.17 , s(mark(X)) -> mark(s(X)) 1061.64/298.17 , s(ok(X)) -> ok(s(X)) 1061.64/298.17 , length(mark(X)) -> mark(length(X)) 1061.64/298.17 , length(ok(X)) -> ok(length(X)) 1061.64/298.17 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1061.64/298.17 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1061.64/298.17 , take(X1, mark(X2)) -> mark(take(X1, X2)) 1061.64/298.17 , take(mark(X1), X2) -> mark(take(X1, X2)) 1061.64/298.17 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 1061.64/298.17 , uTake1(mark(X)) -> mark(uTake1(X)) 1061.64/298.17 , uTake1(ok(X)) -> ok(uTake1(X)) 1061.64/298.17 , uTake2(mark(X1), X2, X3, X4) -> mark(uTake2(X1, X2, X3, X4)) 1061.64/298.17 , uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.17 ok(uTake2(X1, X2, X3, X4)) 1061.64/298.17 , uLength(mark(X1), X2) -> mark(uLength(X1, X2)) 1061.64/298.17 , uLength(ok(X1), ok(X2)) -> ok(uLength(X1, X2)) 1061.64/298.17 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 1061.64/298.17 , proper(tt()) -> ok(tt()) 1061.64/298.17 , proper(isNatIList(X)) -> isNatIList(proper(X)) 1061.64/298.17 , proper(isNatList(X)) -> isNatList(proper(X)) 1061.64/298.17 , proper(isNat(X)) -> isNat(proper(X)) 1061.64/298.17 , proper(0()) -> ok(0()) 1061.64/298.17 , proper(s(X)) -> s(proper(X)) 1061.64/298.17 , proper(length(X)) -> length(proper(X)) 1061.64/298.17 , proper(zeros()) -> ok(zeros()) 1061.64/298.17 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1061.64/298.17 , proper(nil()) -> ok(nil()) 1061.64/298.17 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 1061.64/298.17 , proper(uTake1(X)) -> uTake1(proper(X)) 1061.64/298.17 , proper(uTake2(X1, X2, X3, X4)) -> 1061.64/298.17 uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) 1061.64/298.17 , proper(uLength(X1, X2)) -> uLength(proper(X1), proper(X2)) 1061.64/298.17 , top(mark(X)) -> top(proper(X)) 1061.64/298.17 , top(ok(X)) -> top(active(X)) } 1061.64/298.17 Obligation: 1061.64/298.17 runtime complexity 1061.64/298.17 Answer: 1061.64/298.17 MAYBE 1061.64/298.17 1061.64/298.17 None of the processors succeeded. 1061.64/298.17 1061.64/298.17 Details of failed attempt(s): 1061.64/298.17 ----------------------------- 1061.64/298.17 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1061.64/298.17 following reason: 1061.64/298.17 1061.64/298.17 Computation stopped due to timeout after 297.0 seconds. 1061.64/298.17 1061.64/298.17 2) 'Best' failed due to the following reason: 1061.64/298.17 1061.64/298.17 None of the processors succeeded. 1061.64/298.17 1061.64/298.17 Details of failed attempt(s): 1061.64/298.17 ----------------------------- 1061.64/298.17 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1061.64/298.17 seconds)' failed due to the following reason: 1061.64/298.17 1061.64/298.17 Computation stopped due to timeout after 148.0 seconds. 1061.64/298.17 1061.64/298.17 2) 'Best' failed due to the following reason: 1061.64/298.17 1061.64/298.17 None of the processors succeeded. 1061.64/298.17 1061.64/298.17 Details of failed attempt(s): 1061.64/298.17 ----------------------------- 1061.64/298.17 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1061.64/298.17 following reason: 1061.64/298.17 1061.64/298.17 The processor is inapplicable, reason: 1061.64/298.17 Processor only applicable for innermost runtime complexity analysis 1061.64/298.17 1061.64/298.17 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1061.64/298.17 to the following reason: 1061.64/298.17 1061.64/298.17 The processor is inapplicable, reason: 1061.64/298.17 Processor only applicable for innermost runtime complexity analysis 1061.64/298.17 1061.64/298.17 1061.64/298.17 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1061.64/298.17 failed due to the following reason: 1061.64/298.17 1061.64/298.17 None of the processors succeeded. 1061.64/298.17 1061.64/298.17 Details of failed attempt(s): 1061.64/298.17 ----------------------------- 1061.64/298.17 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1061.64/298.17 failed due to the following reason: 1061.64/298.17 1061.64/298.17 match-boundness of the problem could not be verified. 1061.64/298.17 1061.64/298.17 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1061.64/298.17 failed due to the following reason: 1061.64/298.17 1061.64/298.17 match-boundness of the problem could not be verified. 1061.64/298.17 1061.64/298.17 1061.64/298.17 1061.64/298.17 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1061.64/298.17 the following reason: 1061.64/298.17 1061.64/298.17 We add the following weak dependency pairs: 1061.64/298.17 1061.64/298.17 Strict DPs: 1061.64/298.17 { active^#(and(X1, X2)) -> c_1(and^#(X1, active(X2))) 1061.64/298.17 , active^#(and(X1, X2)) -> c_2(and^#(active(X1), X2)) 1061.64/298.17 , active^#(and(tt(), T)) -> c_3(T) 1061.64/298.17 , active^#(isNatIList(IL)) -> c_4(isNatList^#(IL)) 1061.64/298.17 , active^#(isNatIList(zeros())) -> c_5() 1061.64/298.17 , active^#(isNatIList(cons(N, IL))) -> 1061.64/298.17 c_6(and^#(isNat(N), isNatIList(IL))) 1061.64/298.17 , active^#(isNatList(cons(N, L))) -> 1061.64/298.17 c_7(and^#(isNat(N), isNatList(L))) 1061.64/298.17 , active^#(isNatList(nil())) -> c_8() 1061.64/298.17 , active^#(isNatList(take(N, IL))) -> 1061.64/298.17 c_9(and^#(isNat(N), isNatIList(IL))) 1061.64/298.17 , active^#(isNat(0())) -> c_10() 1061.64/298.17 , active^#(isNat(s(N))) -> c_11(isNat^#(N)) 1061.64/298.17 , active^#(isNat(length(L))) -> c_12(isNatList^#(L)) 1061.64/298.17 , active^#(s(X)) -> c_13(s^#(active(X))) 1061.64/298.17 , active^#(length(X)) -> c_14(length^#(active(X))) 1061.64/298.17 , active^#(length(cons(N, L))) -> 1061.64/298.17 c_15(uLength^#(and(isNat(N), isNatList(L)), L)) 1061.64/298.17 , active^#(zeros()) -> c_16(cons^#(0(), zeros())) 1061.64/298.17 , active^#(cons(X1, X2)) -> c_17(cons^#(active(X1), X2)) 1061.64/298.17 , active^#(take(X1, X2)) -> c_18(take^#(X1, active(X2))) 1061.64/298.17 , active^#(take(X1, X2)) -> c_19(take^#(active(X1), X2)) 1061.64/298.17 , active^#(take(0(), IL)) -> c_20(uTake1^#(isNatIList(IL))) 1061.64/298.17 , active^#(take(s(M), cons(N, IL))) -> 1061.64/298.17 c_21(uTake2^#(and(isNat(M), and(isNat(N), isNatIList(IL))), 1061.64/298.17 M, 1061.64/298.17 N, 1061.64/298.17 IL)) 1061.64/298.17 , active^#(uTake1(X)) -> c_22(uTake1^#(active(X))) 1061.64/298.17 , active^#(uTake1(tt())) -> c_23() 1061.64/298.17 , active^#(uTake2(X1, X2, X3, X4)) -> 1061.64/298.17 c_24(uTake2^#(active(X1), X2, X3, X4)) 1061.64/298.17 , active^#(uTake2(tt(), M, N, IL)) -> c_25(cons^#(N, take(M, IL))) 1061.64/298.17 , active^#(uLength(X1, X2)) -> c_26(uLength^#(active(X1), X2)) 1061.64/298.17 , active^#(uLength(tt(), L)) -> c_27(s^#(length(L))) 1061.64/298.17 , and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) 1061.64/298.17 , and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) 1061.64/298.17 , and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) 1061.64/298.17 , isNatList^#(ok(X)) -> c_32(isNatList^#(X)) 1061.64/298.17 , isNat^#(ok(X)) -> c_33(isNat^#(X)) 1061.64/298.17 , s^#(mark(X)) -> c_34(s^#(X)) 1061.64/298.17 , s^#(ok(X)) -> c_35(s^#(X)) 1061.64/298.17 , length^#(mark(X)) -> c_36(length^#(X)) 1061.64/298.17 , length^#(ok(X)) -> c_37(length^#(X)) 1061.64/298.17 , uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) 1061.64/298.17 , uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) 1061.64/298.17 , cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) 1061.64/298.17 , cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) 1061.64/298.17 , take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) 1061.64/298.17 , take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) 1061.64/298.17 , take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) 1061.64/298.17 , uTake1^#(mark(X)) -> c_43(uTake1^#(X)) 1061.64/298.17 , uTake1^#(ok(X)) -> c_44(uTake1^#(X)) 1061.64/298.17 , uTake2^#(mark(X1), X2, X3, X4) -> c_45(uTake2^#(X1, X2, X3, X4)) 1061.64/298.17 , uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.17 c_46(uTake2^#(X1, X2, X3, X4)) 1061.64/298.17 , isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) 1061.64/298.17 , proper^#(and(X1, X2)) -> c_49(and^#(proper(X1), proper(X2))) 1061.64/298.17 , proper^#(tt()) -> c_50() 1061.64/298.17 , proper^#(isNatIList(X)) -> c_51(isNatIList^#(proper(X))) 1061.64/298.17 , proper^#(isNatList(X)) -> c_52(isNatList^#(proper(X))) 1061.64/298.17 , proper^#(isNat(X)) -> c_53(isNat^#(proper(X))) 1061.64/298.17 , proper^#(0()) -> c_54() 1061.64/298.17 , proper^#(s(X)) -> c_55(s^#(proper(X))) 1061.64/298.17 , proper^#(length(X)) -> c_56(length^#(proper(X))) 1061.64/298.17 , proper^#(zeros()) -> c_57() 1061.64/298.17 , proper^#(cons(X1, X2)) -> c_58(cons^#(proper(X1), proper(X2))) 1061.64/298.17 , proper^#(nil()) -> c_59() 1061.64/298.17 , proper^#(take(X1, X2)) -> c_60(take^#(proper(X1), proper(X2))) 1061.64/298.17 , proper^#(uTake1(X)) -> c_61(uTake1^#(proper(X))) 1061.64/298.17 , proper^#(uTake2(X1, X2, X3, X4)) -> 1061.64/298.17 c_62(uTake2^#(proper(X1), proper(X2), proper(X3), proper(X4))) 1061.64/298.17 , proper^#(uLength(X1, X2)) -> 1061.64/298.17 c_63(uLength^#(proper(X1), proper(X2))) 1061.64/298.17 , top^#(mark(X)) -> c_64(top^#(proper(X))) 1061.64/298.17 , top^#(ok(X)) -> c_65(top^#(active(X))) } 1061.64/298.17 1061.64/298.17 and mark the set of starting terms. 1061.64/298.17 1061.64/298.17 We are left with following problem, upon which TcT provides the 1061.64/298.17 certificate MAYBE. 1061.64/298.17 1061.64/298.17 Strict DPs: 1061.64/298.17 { active^#(and(X1, X2)) -> c_1(and^#(X1, active(X2))) 1061.64/298.17 , active^#(and(X1, X2)) -> c_2(and^#(active(X1), X2)) 1061.64/298.17 , active^#(and(tt(), T)) -> c_3(T) 1061.64/298.17 , active^#(isNatIList(IL)) -> c_4(isNatList^#(IL)) 1061.64/298.17 , active^#(isNatIList(zeros())) -> c_5() 1061.64/298.17 , active^#(isNatIList(cons(N, IL))) -> 1061.64/298.17 c_6(and^#(isNat(N), isNatIList(IL))) 1061.64/298.17 , active^#(isNatList(cons(N, L))) -> 1061.64/298.17 c_7(and^#(isNat(N), isNatList(L))) 1061.64/298.17 , active^#(isNatList(nil())) -> c_8() 1061.64/298.17 , active^#(isNatList(take(N, IL))) -> 1061.64/298.17 c_9(and^#(isNat(N), isNatIList(IL))) 1061.64/298.17 , active^#(isNat(0())) -> c_10() 1061.64/298.17 , active^#(isNat(s(N))) -> c_11(isNat^#(N)) 1061.64/298.17 , active^#(isNat(length(L))) -> c_12(isNatList^#(L)) 1061.64/298.17 , active^#(s(X)) -> c_13(s^#(active(X))) 1061.64/298.17 , active^#(length(X)) -> c_14(length^#(active(X))) 1061.64/298.17 , active^#(length(cons(N, L))) -> 1061.64/298.17 c_15(uLength^#(and(isNat(N), isNatList(L)), L)) 1061.64/298.17 , active^#(zeros()) -> c_16(cons^#(0(), zeros())) 1061.64/298.17 , active^#(cons(X1, X2)) -> c_17(cons^#(active(X1), X2)) 1061.64/298.17 , active^#(take(X1, X2)) -> c_18(take^#(X1, active(X2))) 1061.64/298.17 , active^#(take(X1, X2)) -> c_19(take^#(active(X1), X2)) 1061.64/298.17 , active^#(take(0(), IL)) -> c_20(uTake1^#(isNatIList(IL))) 1061.64/298.17 , active^#(take(s(M), cons(N, IL))) -> 1061.64/298.17 c_21(uTake2^#(and(isNat(M), and(isNat(N), isNatIList(IL))), 1061.64/298.17 M, 1061.64/298.17 N, 1061.64/298.17 IL)) 1061.64/298.17 , active^#(uTake1(X)) -> c_22(uTake1^#(active(X))) 1061.64/298.17 , active^#(uTake1(tt())) -> c_23() 1061.64/298.17 , active^#(uTake2(X1, X2, X3, X4)) -> 1061.64/298.17 c_24(uTake2^#(active(X1), X2, X3, X4)) 1061.64/298.17 , active^#(uTake2(tt(), M, N, IL)) -> c_25(cons^#(N, take(M, IL))) 1061.64/298.17 , active^#(uLength(X1, X2)) -> c_26(uLength^#(active(X1), X2)) 1061.64/298.17 , active^#(uLength(tt(), L)) -> c_27(s^#(length(L))) 1061.64/298.17 , and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) 1061.64/298.17 , and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) 1061.64/298.17 , and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) 1061.64/298.17 , isNatList^#(ok(X)) -> c_32(isNatList^#(X)) 1061.64/298.17 , isNat^#(ok(X)) -> c_33(isNat^#(X)) 1061.64/298.17 , s^#(mark(X)) -> c_34(s^#(X)) 1061.64/298.17 , s^#(ok(X)) -> c_35(s^#(X)) 1061.64/298.17 , length^#(mark(X)) -> c_36(length^#(X)) 1061.64/298.17 , length^#(ok(X)) -> c_37(length^#(X)) 1061.64/298.17 , uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) 1061.64/298.17 , uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) 1061.64/298.17 , cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) 1061.64/298.17 , cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) 1061.64/298.17 , take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) 1061.64/298.17 , take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) 1061.64/298.17 , take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) 1061.64/298.17 , uTake1^#(mark(X)) -> c_43(uTake1^#(X)) 1061.64/298.17 , uTake1^#(ok(X)) -> c_44(uTake1^#(X)) 1061.64/298.17 , uTake2^#(mark(X1), X2, X3, X4) -> c_45(uTake2^#(X1, X2, X3, X4)) 1061.64/298.17 , uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.17 c_46(uTake2^#(X1, X2, X3, X4)) 1061.64/298.17 , isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) 1061.64/298.17 , proper^#(and(X1, X2)) -> c_49(and^#(proper(X1), proper(X2))) 1061.64/298.17 , proper^#(tt()) -> c_50() 1061.64/298.17 , proper^#(isNatIList(X)) -> c_51(isNatIList^#(proper(X))) 1061.64/298.17 , proper^#(isNatList(X)) -> c_52(isNatList^#(proper(X))) 1061.64/298.17 , proper^#(isNat(X)) -> c_53(isNat^#(proper(X))) 1061.64/298.17 , proper^#(0()) -> c_54() 1061.64/298.17 , proper^#(s(X)) -> c_55(s^#(proper(X))) 1061.64/298.17 , proper^#(length(X)) -> c_56(length^#(proper(X))) 1061.64/298.17 , proper^#(zeros()) -> c_57() 1061.64/298.17 , proper^#(cons(X1, X2)) -> c_58(cons^#(proper(X1), proper(X2))) 1061.64/298.17 , proper^#(nil()) -> c_59() 1061.64/298.17 , proper^#(take(X1, X2)) -> c_60(take^#(proper(X1), proper(X2))) 1061.64/298.17 , proper^#(uTake1(X)) -> c_61(uTake1^#(proper(X))) 1061.64/298.17 , proper^#(uTake2(X1, X2, X3, X4)) -> 1061.64/298.17 c_62(uTake2^#(proper(X1), proper(X2), proper(X3), proper(X4))) 1061.64/298.17 , proper^#(uLength(X1, X2)) -> 1061.64/298.17 c_63(uLength^#(proper(X1), proper(X2))) 1061.64/298.17 , top^#(mark(X)) -> c_64(top^#(proper(X))) 1061.64/298.17 , top^#(ok(X)) -> c_65(top^#(active(X))) } 1061.64/298.17 Strict Trs: 1061.64/298.17 { active(and(X1, X2)) -> and(X1, active(X2)) 1061.64/298.17 , active(and(X1, X2)) -> and(active(X1), X2) 1061.64/298.17 , active(and(tt(), T)) -> mark(T) 1061.64/298.17 , active(isNatIList(IL)) -> mark(isNatList(IL)) 1061.64/298.17 , active(isNatIList(zeros())) -> mark(tt()) 1061.64/298.17 , active(isNatIList(cons(N, IL))) -> 1061.64/298.17 mark(and(isNat(N), isNatIList(IL))) 1061.64/298.17 , active(isNatList(cons(N, L))) -> 1061.64/298.17 mark(and(isNat(N), isNatList(L))) 1061.64/298.17 , active(isNatList(nil())) -> mark(tt()) 1061.64/298.17 , active(isNatList(take(N, IL))) -> 1061.64/298.17 mark(and(isNat(N), isNatIList(IL))) 1061.64/298.17 , active(isNat(0())) -> mark(tt()) 1061.64/298.17 , active(isNat(s(N))) -> mark(isNat(N)) 1061.64/298.17 , active(isNat(length(L))) -> mark(isNatList(L)) 1061.64/298.17 , active(s(X)) -> s(active(X)) 1061.64/298.17 , active(length(X)) -> length(active(X)) 1061.64/298.17 , active(length(cons(N, L))) -> 1061.64/298.17 mark(uLength(and(isNat(N), isNatList(L)), L)) 1061.64/298.17 , active(zeros()) -> mark(cons(0(), zeros())) 1061.64/298.17 , active(cons(X1, X2)) -> cons(active(X1), X2) 1061.64/298.17 , active(take(X1, X2)) -> take(X1, active(X2)) 1061.64/298.17 , active(take(X1, X2)) -> take(active(X1), X2) 1061.64/298.17 , active(take(0(), IL)) -> mark(uTake1(isNatIList(IL))) 1061.64/298.17 , active(take(s(M), cons(N, IL))) -> 1061.64/298.17 mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), 1061.64/298.17 M, 1061.64/298.17 N, 1061.64/298.17 IL)) 1061.64/298.17 , active(uTake1(X)) -> uTake1(active(X)) 1061.64/298.17 , active(uTake1(tt())) -> mark(nil()) 1061.64/298.17 , active(uTake2(X1, X2, X3, X4)) -> uTake2(active(X1), X2, X3, X4) 1061.64/298.17 , active(uTake2(tt(), M, N, IL)) -> mark(cons(N, take(M, IL))) 1061.64/298.17 , active(uLength(X1, X2)) -> uLength(active(X1), X2) 1061.64/298.17 , active(uLength(tt(), L)) -> mark(s(length(L))) 1061.64/298.17 , and(X1, mark(X2)) -> mark(and(X1, X2)) 1061.64/298.17 , and(mark(X1), X2) -> mark(and(X1, X2)) 1061.64/298.17 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 1061.64/298.17 , isNatIList(ok(X)) -> ok(isNatIList(X)) 1061.64/298.17 , isNatList(ok(X)) -> ok(isNatList(X)) 1061.64/298.17 , isNat(ok(X)) -> ok(isNat(X)) 1061.64/298.17 , s(mark(X)) -> mark(s(X)) 1061.64/298.17 , s(ok(X)) -> ok(s(X)) 1061.64/298.17 , length(mark(X)) -> mark(length(X)) 1061.64/298.17 , length(ok(X)) -> ok(length(X)) 1061.64/298.17 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1061.64/298.17 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1061.64/298.17 , take(X1, mark(X2)) -> mark(take(X1, X2)) 1061.64/298.17 , take(mark(X1), X2) -> mark(take(X1, X2)) 1061.64/298.17 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 1061.64/298.17 , uTake1(mark(X)) -> mark(uTake1(X)) 1061.64/298.17 , uTake1(ok(X)) -> ok(uTake1(X)) 1061.64/298.17 , uTake2(mark(X1), X2, X3, X4) -> mark(uTake2(X1, X2, X3, X4)) 1061.64/298.17 , uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.17 ok(uTake2(X1, X2, X3, X4)) 1061.64/298.17 , uLength(mark(X1), X2) -> mark(uLength(X1, X2)) 1061.64/298.17 , uLength(ok(X1), ok(X2)) -> ok(uLength(X1, X2)) 1061.64/298.17 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 1061.64/298.17 , proper(tt()) -> ok(tt()) 1061.64/298.17 , proper(isNatIList(X)) -> isNatIList(proper(X)) 1061.64/298.17 , proper(isNatList(X)) -> isNatList(proper(X)) 1061.64/298.17 , proper(isNat(X)) -> isNat(proper(X)) 1061.64/298.17 , proper(0()) -> ok(0()) 1061.64/298.17 , proper(s(X)) -> s(proper(X)) 1061.64/298.18 , proper(length(X)) -> length(proper(X)) 1061.64/298.18 , proper(zeros()) -> ok(zeros()) 1061.64/298.18 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1061.64/298.18 , proper(nil()) -> ok(nil()) 1061.64/298.18 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 1061.64/298.18 , proper(uTake1(X)) -> uTake1(proper(X)) 1061.64/298.18 , proper(uTake2(X1, X2, X3, X4)) -> 1061.64/298.18 uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) 1061.64/298.18 , proper(uLength(X1, X2)) -> uLength(proper(X1), proper(X2)) 1061.64/298.18 , top(mark(X)) -> top(proper(X)) 1061.64/298.18 , top(ok(X)) -> top(active(X)) } 1061.64/298.18 Obligation: 1061.64/298.18 runtime complexity 1061.64/298.18 Answer: 1061.64/298.18 MAYBE 1061.64/298.18 1061.64/298.18 Consider the dependency graph: 1061.64/298.18 1061.64/298.18 1: active^#(and(X1, X2)) -> c_1(and^#(X1, active(X2))) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 2: active^#(and(X1, X2)) -> c_2(and^#(active(X1), X2)) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 3: active^#(and(tt(), T)) -> c_3(T) 1061.64/298.18 -->_1 top^#(ok(X)) -> c_65(top^#(active(X))) :65 1061.64/298.18 -->_1 top^#(mark(X)) -> c_64(top^#(proper(X))) :64 1061.64/298.18 -->_1 proper^#(uLength(X1, X2)) -> 1061.64/298.18 c_63(uLength^#(proper(X1), proper(X2))) :63 1061.64/298.18 -->_1 proper^#(uTake2(X1, X2, X3, X4)) -> 1061.64/298.18 c_62(uTake2^#(proper(X1), proper(X2), proper(X3), proper(X4))) :62 1061.64/298.18 -->_1 proper^#(uTake1(X)) -> c_61(uTake1^#(proper(X))) :61 1061.64/298.18 -->_1 proper^#(take(X1, X2)) -> 1061.64/298.18 c_60(take^#(proper(X1), proper(X2))) :60 1061.64/298.18 -->_1 proper^#(cons(X1, X2)) -> 1061.64/298.18 c_58(cons^#(proper(X1), proper(X2))) :58 1061.64/298.18 -->_1 proper^#(length(X)) -> c_56(length^#(proper(X))) :56 1061.64/298.18 -->_1 proper^#(s(X)) -> c_55(s^#(proper(X))) :55 1061.64/298.18 -->_1 proper^#(isNat(X)) -> c_53(isNat^#(proper(X))) :53 1061.64/298.18 -->_1 proper^#(isNatList(X)) -> c_52(isNatList^#(proper(X))) :52 1061.64/298.18 -->_1 proper^#(isNatIList(X)) -> c_51(isNatIList^#(proper(X))) :51 1061.64/298.18 -->_1 proper^#(and(X1, X2)) -> 1061.64/298.18 c_49(and^#(proper(X1), proper(X2))) :49 1061.64/298.18 -->_1 isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) :48 1061.64/298.18 -->_1 uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.18 c_46(uTake2^#(X1, X2, X3, X4)) :47 1061.64/298.18 -->_1 uTake2^#(mark(X1), X2, X3, X4) -> 1061.64/298.18 c_45(uTake2^#(X1, X2, X3, X4)) :46 1061.64/298.18 -->_1 uTake1^#(ok(X)) -> c_44(uTake1^#(X)) :45 1061.64/298.18 -->_1 uTake1^#(mark(X)) -> c_43(uTake1^#(X)) :44 1061.64/298.18 -->_1 take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) :43 1061.64/298.18 -->_1 take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) :42 1061.64/298.18 -->_1 take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) :41 1061.64/298.18 -->_1 cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) :40 1061.64/298.18 -->_1 cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) :39 1061.64/298.18 -->_1 uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) :38 1061.64/298.18 -->_1 uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) :37 1061.64/298.18 -->_1 length^#(ok(X)) -> c_37(length^#(X)) :36 1061.64/298.18 -->_1 length^#(mark(X)) -> c_36(length^#(X)) :35 1061.64/298.18 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 1061.64/298.18 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 1061.64/298.18 -->_1 isNat^#(ok(X)) -> c_33(isNat^#(X)) :32 1061.64/298.18 -->_1 isNatList^#(ok(X)) -> c_32(isNatList^#(X)) :31 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 -->_1 active^#(uLength(tt(), L)) -> c_27(s^#(length(L))) :27 1061.64/298.18 -->_1 active^#(uLength(X1, X2)) -> 1061.64/298.18 c_26(uLength^#(active(X1), X2)) :26 1061.64/298.18 -->_1 active^#(uTake2(tt(), M, N, IL)) -> 1061.64/298.18 c_25(cons^#(N, take(M, IL))) :25 1061.64/298.18 -->_1 active^#(uTake2(X1, X2, X3, X4)) -> 1061.64/298.18 c_24(uTake2^#(active(X1), X2, X3, X4)) :24 1061.64/298.18 -->_1 active^#(uTake1(X)) -> c_22(uTake1^#(active(X))) :22 1061.64/298.18 -->_1 active^#(take(s(M), cons(N, IL))) -> 1061.64/298.18 c_21(uTake2^#(and(isNat(M), and(isNat(N), isNatIList(IL))), 1061.64/298.18 M, 1061.64/298.18 N, 1061.64/298.18 IL)) :21 1061.64/298.18 -->_1 active^#(take(0(), IL)) -> c_20(uTake1^#(isNatIList(IL))) :20 1061.64/298.18 -->_1 active^#(take(X1, X2)) -> c_19(take^#(active(X1), X2)) :19 1061.64/298.18 -->_1 active^#(take(X1, X2)) -> c_18(take^#(X1, active(X2))) :18 1061.64/298.18 -->_1 active^#(cons(X1, X2)) -> c_17(cons^#(active(X1), X2)) :17 1061.64/298.18 -->_1 active^#(length(cons(N, L))) -> 1061.64/298.18 c_15(uLength^#(and(isNat(N), isNatList(L)), L)) :15 1061.64/298.18 -->_1 active^#(length(X)) -> c_14(length^#(active(X))) :14 1061.64/298.18 -->_1 active^#(s(X)) -> c_13(s^#(active(X))) :13 1061.64/298.18 -->_1 active^#(isNat(length(L))) -> c_12(isNatList^#(L)) :12 1061.64/298.18 -->_1 active^#(isNat(s(N))) -> c_11(isNat^#(N)) :11 1061.64/298.18 -->_1 active^#(isNatList(take(N, IL))) -> 1061.64/298.18 c_9(and^#(isNat(N), isNatIList(IL))) :9 1061.64/298.18 -->_1 active^#(isNatList(cons(N, L))) -> 1061.64/298.18 c_7(and^#(isNat(N), isNatList(L))) :7 1061.64/298.18 -->_1 active^#(isNatIList(cons(N, IL))) -> 1061.64/298.18 c_6(and^#(isNat(N), isNatIList(IL))) :6 1061.64/298.18 -->_1 active^#(isNatIList(IL)) -> c_4(isNatList^#(IL)) :4 1061.64/298.18 -->_1 proper^#(nil()) -> c_59() :59 1061.64/298.18 -->_1 proper^#(zeros()) -> c_57() :57 1061.64/298.18 -->_1 proper^#(0()) -> c_54() :54 1061.64/298.18 -->_1 proper^#(tt()) -> c_50() :50 1061.64/298.18 -->_1 active^#(uTake1(tt())) -> c_23() :23 1061.64/298.18 -->_1 active^#(zeros()) -> c_16(cons^#(0(), zeros())) :16 1061.64/298.18 -->_1 active^#(isNat(0())) -> c_10() :10 1061.64/298.18 -->_1 active^#(isNatList(nil())) -> c_8() :8 1061.64/298.18 -->_1 active^#(isNatIList(zeros())) -> c_5() :5 1061.64/298.18 -->_1 active^#(and(tt(), T)) -> c_3(T) :3 1061.64/298.18 -->_1 active^#(and(X1, X2)) -> c_2(and^#(active(X1), X2)) :2 1061.64/298.18 -->_1 active^#(and(X1, X2)) -> c_1(and^#(X1, active(X2))) :1 1061.64/298.18 1061.64/298.18 4: active^#(isNatIList(IL)) -> c_4(isNatList^#(IL)) 1061.64/298.18 -->_1 isNatList^#(ok(X)) -> c_32(isNatList^#(X)) :31 1061.64/298.18 1061.64/298.18 5: active^#(isNatIList(zeros())) -> c_5() 1061.64/298.18 1061.64/298.18 6: active^#(isNatIList(cons(N, IL))) -> 1061.64/298.18 c_6(and^#(isNat(N), isNatIList(IL))) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 7: active^#(isNatList(cons(N, L))) -> 1061.64/298.18 c_7(and^#(isNat(N), isNatList(L))) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 8: active^#(isNatList(nil())) -> c_8() 1061.64/298.18 1061.64/298.18 9: active^#(isNatList(take(N, IL))) -> 1061.64/298.18 c_9(and^#(isNat(N), isNatIList(IL))) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 10: active^#(isNat(0())) -> c_10() 1061.64/298.18 1061.64/298.18 11: active^#(isNat(s(N))) -> c_11(isNat^#(N)) 1061.64/298.18 -->_1 isNat^#(ok(X)) -> c_33(isNat^#(X)) :32 1061.64/298.18 1061.64/298.18 12: active^#(isNat(length(L))) -> c_12(isNatList^#(L)) 1061.64/298.18 -->_1 isNatList^#(ok(X)) -> c_32(isNatList^#(X)) :31 1061.64/298.18 1061.64/298.18 13: active^#(s(X)) -> c_13(s^#(active(X))) 1061.64/298.18 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 1061.64/298.18 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 1061.64/298.18 1061.64/298.18 14: active^#(length(X)) -> c_14(length^#(active(X))) 1061.64/298.18 -->_1 length^#(ok(X)) -> c_37(length^#(X)) :36 1061.64/298.18 -->_1 length^#(mark(X)) -> c_36(length^#(X)) :35 1061.64/298.18 1061.64/298.18 15: active^#(length(cons(N, L))) -> 1061.64/298.18 c_15(uLength^#(and(isNat(N), isNatList(L)), L)) 1061.64/298.18 -->_1 uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) :38 1061.64/298.18 -->_1 uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) :37 1061.64/298.18 1061.64/298.18 16: active^#(zeros()) -> c_16(cons^#(0(), zeros())) 1061.64/298.18 1061.64/298.18 17: active^#(cons(X1, X2)) -> c_17(cons^#(active(X1), X2)) 1061.64/298.18 -->_1 cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) :40 1061.64/298.18 -->_1 cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) :39 1061.64/298.18 1061.64/298.18 18: active^#(take(X1, X2)) -> c_18(take^#(X1, active(X2))) 1061.64/298.18 -->_1 take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) :43 1061.64/298.18 -->_1 take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) :42 1061.64/298.18 -->_1 take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) :41 1061.64/298.18 1061.64/298.18 19: active^#(take(X1, X2)) -> c_19(take^#(active(X1), X2)) 1061.64/298.18 -->_1 take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) :43 1061.64/298.18 -->_1 take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) :42 1061.64/298.18 -->_1 take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) :41 1061.64/298.18 1061.64/298.18 20: active^#(take(0(), IL)) -> c_20(uTake1^#(isNatIList(IL))) 1061.64/298.18 -->_1 uTake1^#(ok(X)) -> c_44(uTake1^#(X)) :45 1061.64/298.18 -->_1 uTake1^#(mark(X)) -> c_43(uTake1^#(X)) :44 1061.64/298.18 1061.64/298.18 21: active^#(take(s(M), cons(N, IL))) -> 1061.64/298.18 c_21(uTake2^#(and(isNat(M), and(isNat(N), isNatIList(IL))), 1061.64/298.18 M, 1061.64/298.18 N, 1061.64/298.18 IL)) 1061.64/298.18 -->_1 uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.18 c_46(uTake2^#(X1, X2, X3, X4)) :47 1061.64/298.18 -->_1 uTake2^#(mark(X1), X2, X3, X4) -> 1061.64/298.18 c_45(uTake2^#(X1, X2, X3, X4)) :46 1061.64/298.18 1061.64/298.18 22: active^#(uTake1(X)) -> c_22(uTake1^#(active(X))) 1061.64/298.18 -->_1 uTake1^#(ok(X)) -> c_44(uTake1^#(X)) :45 1061.64/298.18 -->_1 uTake1^#(mark(X)) -> c_43(uTake1^#(X)) :44 1061.64/298.18 1061.64/298.18 23: active^#(uTake1(tt())) -> c_23() 1061.64/298.18 1061.64/298.18 24: active^#(uTake2(X1, X2, X3, X4)) -> 1061.64/298.18 c_24(uTake2^#(active(X1), X2, X3, X4)) 1061.64/298.18 -->_1 uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.18 c_46(uTake2^#(X1, X2, X3, X4)) :47 1061.64/298.18 -->_1 uTake2^#(mark(X1), X2, X3, X4) -> 1061.64/298.18 c_45(uTake2^#(X1, X2, X3, X4)) :46 1061.64/298.18 1061.64/298.18 25: active^#(uTake2(tt(), M, N, IL)) -> 1061.64/298.18 c_25(cons^#(N, take(M, IL))) 1061.64/298.18 -->_1 cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) :40 1061.64/298.18 -->_1 cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) :39 1061.64/298.18 1061.64/298.18 26: active^#(uLength(X1, X2)) -> c_26(uLength^#(active(X1), X2)) 1061.64/298.18 -->_1 uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) :38 1061.64/298.18 -->_1 uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) :37 1061.64/298.18 1061.64/298.18 27: active^#(uLength(tt(), L)) -> c_27(s^#(length(L))) 1061.64/298.18 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 1061.64/298.18 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 1061.64/298.18 1061.64/298.18 28: and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 29: and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 30: and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 31: isNatList^#(ok(X)) -> c_32(isNatList^#(X)) 1061.64/298.18 -->_1 isNatList^#(ok(X)) -> c_32(isNatList^#(X)) :31 1061.64/298.18 1061.64/298.18 32: isNat^#(ok(X)) -> c_33(isNat^#(X)) 1061.64/298.18 -->_1 isNat^#(ok(X)) -> c_33(isNat^#(X)) :32 1061.64/298.18 1061.64/298.18 33: s^#(mark(X)) -> c_34(s^#(X)) 1061.64/298.18 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 1061.64/298.18 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 1061.64/298.18 1061.64/298.18 34: s^#(ok(X)) -> c_35(s^#(X)) 1061.64/298.18 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 1061.64/298.18 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 1061.64/298.18 1061.64/298.18 35: length^#(mark(X)) -> c_36(length^#(X)) 1061.64/298.18 -->_1 length^#(ok(X)) -> c_37(length^#(X)) :36 1061.64/298.18 -->_1 length^#(mark(X)) -> c_36(length^#(X)) :35 1061.64/298.18 1061.64/298.18 36: length^#(ok(X)) -> c_37(length^#(X)) 1061.64/298.18 -->_1 length^#(ok(X)) -> c_37(length^#(X)) :36 1061.64/298.18 -->_1 length^#(mark(X)) -> c_36(length^#(X)) :35 1061.64/298.18 1061.64/298.18 37: uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) 1061.64/298.18 -->_1 uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) :38 1061.64/298.18 -->_1 uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) :37 1061.64/298.18 1061.64/298.18 38: uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) 1061.64/298.18 -->_1 uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) :38 1061.64/298.18 -->_1 uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) :37 1061.64/298.18 1061.64/298.18 39: cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) 1061.64/298.18 -->_1 cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) :40 1061.64/298.18 -->_1 cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) :39 1061.64/298.18 1061.64/298.18 40: cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) 1061.64/298.18 -->_1 cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) :40 1061.64/298.18 -->_1 cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) :39 1061.64/298.18 1061.64/298.18 41: take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) 1061.64/298.18 -->_1 take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) :43 1061.64/298.18 -->_1 take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) :42 1061.64/298.18 -->_1 take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) :41 1061.64/298.18 1061.64/298.18 42: take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) 1061.64/298.18 -->_1 take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) :43 1061.64/298.18 -->_1 take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) :42 1061.64/298.18 -->_1 take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) :41 1061.64/298.18 1061.64/298.18 43: take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) 1061.64/298.18 -->_1 take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) :43 1061.64/298.18 -->_1 take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) :42 1061.64/298.18 -->_1 take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) :41 1061.64/298.18 1061.64/298.18 44: uTake1^#(mark(X)) -> c_43(uTake1^#(X)) 1061.64/298.18 -->_1 uTake1^#(ok(X)) -> c_44(uTake1^#(X)) :45 1061.64/298.18 -->_1 uTake1^#(mark(X)) -> c_43(uTake1^#(X)) :44 1061.64/298.18 1061.64/298.18 45: uTake1^#(ok(X)) -> c_44(uTake1^#(X)) 1061.64/298.18 -->_1 uTake1^#(ok(X)) -> c_44(uTake1^#(X)) :45 1061.64/298.18 -->_1 uTake1^#(mark(X)) -> c_43(uTake1^#(X)) :44 1061.64/298.18 1061.64/298.18 46: uTake2^#(mark(X1), X2, X3, X4) -> 1061.64/298.18 c_45(uTake2^#(X1, X2, X3, X4)) 1061.64/298.18 -->_1 uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.18 c_46(uTake2^#(X1, X2, X3, X4)) :47 1061.64/298.18 -->_1 uTake2^#(mark(X1), X2, X3, X4) -> 1061.64/298.18 c_45(uTake2^#(X1, X2, X3, X4)) :46 1061.64/298.18 1061.64/298.18 47: uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.18 c_46(uTake2^#(X1, X2, X3, X4)) 1061.64/298.18 -->_1 uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.18 c_46(uTake2^#(X1, X2, X3, X4)) :47 1061.64/298.18 -->_1 uTake2^#(mark(X1), X2, X3, X4) -> 1061.64/298.18 c_45(uTake2^#(X1, X2, X3, X4)) :46 1061.64/298.18 1061.64/298.18 48: isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) 1061.64/298.18 -->_1 isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) :48 1061.64/298.18 1061.64/298.18 49: proper^#(and(X1, X2)) -> c_49(and^#(proper(X1), proper(X2))) 1061.64/298.18 -->_1 and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) :30 1061.64/298.18 -->_1 and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) :29 1061.64/298.18 -->_1 and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) :28 1061.64/298.18 1061.64/298.18 50: proper^#(tt()) -> c_50() 1061.64/298.18 1061.64/298.18 51: proper^#(isNatIList(X)) -> c_51(isNatIList^#(proper(X))) 1061.64/298.18 -->_1 isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) :48 1061.64/298.18 1061.64/298.18 52: proper^#(isNatList(X)) -> c_52(isNatList^#(proper(X))) 1061.64/298.18 -->_1 isNatList^#(ok(X)) -> c_32(isNatList^#(X)) :31 1061.64/298.18 1061.64/298.18 53: proper^#(isNat(X)) -> c_53(isNat^#(proper(X))) 1061.64/298.18 -->_1 isNat^#(ok(X)) -> c_33(isNat^#(X)) :32 1061.64/298.18 1061.64/298.18 54: proper^#(0()) -> c_54() 1061.64/298.18 1061.64/298.18 55: proper^#(s(X)) -> c_55(s^#(proper(X))) 1061.64/298.18 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 1061.64/298.18 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 1061.64/298.18 1061.64/298.18 56: proper^#(length(X)) -> c_56(length^#(proper(X))) 1061.64/298.18 -->_1 length^#(ok(X)) -> c_37(length^#(X)) :36 1061.64/298.18 -->_1 length^#(mark(X)) -> c_36(length^#(X)) :35 1061.64/298.18 1061.64/298.18 57: proper^#(zeros()) -> c_57() 1061.64/298.18 1061.64/298.18 58: proper^#(cons(X1, X2)) -> c_58(cons^#(proper(X1), proper(X2))) 1061.64/298.18 -->_1 cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) :40 1061.64/298.18 -->_1 cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) :39 1061.64/298.18 1061.64/298.18 59: proper^#(nil()) -> c_59() 1061.64/298.18 1061.64/298.18 60: proper^#(take(X1, X2)) -> c_60(take^#(proper(X1), proper(X2))) 1061.64/298.18 -->_1 take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) :43 1061.64/298.18 -->_1 take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) :42 1061.64/298.18 -->_1 take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) :41 1061.64/298.18 1061.64/298.18 61: proper^#(uTake1(X)) -> c_61(uTake1^#(proper(X))) 1061.64/298.18 -->_1 uTake1^#(ok(X)) -> c_44(uTake1^#(X)) :45 1061.64/298.18 -->_1 uTake1^#(mark(X)) -> c_43(uTake1^#(X)) :44 1061.64/298.19 1061.64/298.19 62: proper^#(uTake2(X1, X2, X3, X4)) -> 1061.64/298.19 c_62(uTake2^#(proper(X1), proper(X2), proper(X3), proper(X4))) 1061.64/298.19 -->_1 uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.19 c_46(uTake2^#(X1, X2, X3, X4)) :47 1061.64/298.19 -->_1 uTake2^#(mark(X1), X2, X3, X4) -> 1061.64/298.19 c_45(uTake2^#(X1, X2, X3, X4)) :46 1061.64/298.19 1061.64/298.19 63: proper^#(uLength(X1, X2)) -> 1061.64/298.19 c_63(uLength^#(proper(X1), proper(X2))) 1061.64/298.19 -->_1 uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) :38 1061.64/298.19 -->_1 uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) :37 1061.64/298.19 1061.64/298.19 64: top^#(mark(X)) -> c_64(top^#(proper(X))) 1061.64/298.19 -->_1 top^#(ok(X)) -> c_65(top^#(active(X))) :65 1061.64/298.19 -->_1 top^#(mark(X)) -> c_64(top^#(proper(X))) :64 1061.64/298.19 1061.64/298.19 65: top^#(ok(X)) -> c_65(top^#(active(X))) 1061.64/298.19 -->_1 top^#(ok(X)) -> c_65(top^#(active(X))) :65 1061.64/298.19 -->_1 top^#(mark(X)) -> c_64(top^#(proper(X))) :64 1061.64/298.19 1061.64/298.19 1061.64/298.19 Only the nodes 1061.64/298.19 {16,28,30,29,31,32,33,34,35,36,37,38,39,40,41,43,42,44,45,46,47,48,50,54,57,59,64,65} 1061.64/298.19 are reachable from nodes 1061.64/298.19 {16,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,50,54,57,59,64,65} 1061.64/298.19 that start derivation from marked basic terms. The nodes not 1061.64/298.19 reachable are removed from the problem. 1061.64/298.19 1061.64/298.19 We are left with following problem, upon which TcT provides the 1061.64/298.19 certificate MAYBE. 1061.64/298.19 1061.64/298.19 Strict DPs: 1061.64/298.19 { active^#(zeros()) -> c_16(cons^#(0(), zeros())) 1061.64/298.19 , and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) 1061.64/298.19 , and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) 1061.64/298.19 , and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) 1061.64/298.19 , isNatList^#(ok(X)) -> c_32(isNatList^#(X)) 1061.64/298.19 , isNat^#(ok(X)) -> c_33(isNat^#(X)) 1061.64/298.19 , s^#(mark(X)) -> c_34(s^#(X)) 1061.64/298.19 , s^#(ok(X)) -> c_35(s^#(X)) 1061.64/298.19 , length^#(mark(X)) -> c_36(length^#(X)) 1061.64/298.19 , length^#(ok(X)) -> c_37(length^#(X)) 1061.64/298.19 , uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) 1061.64/298.19 , uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) 1061.64/298.19 , cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) 1061.64/298.19 , cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) 1061.64/298.19 , take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) 1061.64/298.19 , take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) 1061.64/298.19 , take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) 1061.64/298.19 , uTake1^#(mark(X)) -> c_43(uTake1^#(X)) 1061.64/298.19 , uTake1^#(ok(X)) -> c_44(uTake1^#(X)) 1061.64/298.19 , uTake2^#(mark(X1), X2, X3, X4) -> c_45(uTake2^#(X1, X2, X3, X4)) 1061.64/298.19 , uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.19 c_46(uTake2^#(X1, X2, X3, X4)) 1061.64/298.19 , isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) 1061.64/298.19 , proper^#(tt()) -> c_50() 1061.64/298.19 , proper^#(0()) -> c_54() 1061.64/298.19 , proper^#(zeros()) -> c_57() 1061.64/298.19 , proper^#(nil()) -> c_59() 1061.64/298.19 , top^#(mark(X)) -> c_64(top^#(proper(X))) 1061.64/298.19 , top^#(ok(X)) -> c_65(top^#(active(X))) } 1061.64/298.19 Strict Trs: 1061.64/298.19 { active(and(X1, X2)) -> and(X1, active(X2)) 1061.64/298.19 , active(and(X1, X2)) -> and(active(X1), X2) 1061.64/298.19 , active(and(tt(), T)) -> mark(T) 1061.64/298.19 , active(isNatIList(IL)) -> mark(isNatList(IL)) 1061.64/298.19 , active(isNatIList(zeros())) -> mark(tt()) 1061.64/298.19 , active(isNatIList(cons(N, IL))) -> 1061.64/298.19 mark(and(isNat(N), isNatIList(IL))) 1061.64/298.19 , active(isNatList(cons(N, L))) -> 1061.64/298.19 mark(and(isNat(N), isNatList(L))) 1061.64/298.19 , active(isNatList(nil())) -> mark(tt()) 1061.64/298.19 , active(isNatList(take(N, IL))) -> 1061.64/298.19 mark(and(isNat(N), isNatIList(IL))) 1061.64/298.19 , active(isNat(0())) -> mark(tt()) 1061.64/298.19 , active(isNat(s(N))) -> mark(isNat(N)) 1061.64/298.19 , active(isNat(length(L))) -> mark(isNatList(L)) 1061.64/298.19 , active(s(X)) -> s(active(X)) 1061.64/298.19 , active(length(X)) -> length(active(X)) 1061.64/298.19 , active(length(cons(N, L))) -> 1061.64/298.19 mark(uLength(and(isNat(N), isNatList(L)), L)) 1061.64/298.19 , active(zeros()) -> mark(cons(0(), zeros())) 1061.64/298.19 , active(cons(X1, X2)) -> cons(active(X1), X2) 1061.64/298.19 , active(take(X1, X2)) -> take(X1, active(X2)) 1061.64/298.19 , active(take(X1, X2)) -> take(active(X1), X2) 1061.64/298.19 , active(take(0(), IL)) -> mark(uTake1(isNatIList(IL))) 1061.64/298.19 , active(take(s(M), cons(N, IL))) -> 1061.64/298.19 mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), 1061.64/298.19 M, 1061.64/298.19 N, 1061.64/298.19 IL)) 1061.64/298.19 , active(uTake1(X)) -> uTake1(active(X)) 1061.64/298.19 , active(uTake1(tt())) -> mark(nil()) 1061.64/298.19 , active(uTake2(X1, X2, X3, X4)) -> uTake2(active(X1), X2, X3, X4) 1061.64/298.19 , active(uTake2(tt(), M, N, IL)) -> mark(cons(N, take(M, IL))) 1061.64/298.19 , active(uLength(X1, X2)) -> uLength(active(X1), X2) 1061.64/298.19 , active(uLength(tt(), L)) -> mark(s(length(L))) 1061.64/298.19 , and(X1, mark(X2)) -> mark(and(X1, X2)) 1061.64/298.19 , and(mark(X1), X2) -> mark(and(X1, X2)) 1061.64/298.19 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 1061.64/298.19 , isNatIList(ok(X)) -> ok(isNatIList(X)) 1061.64/298.19 , isNatList(ok(X)) -> ok(isNatList(X)) 1061.64/298.19 , isNat(ok(X)) -> ok(isNat(X)) 1061.64/298.19 , s(mark(X)) -> mark(s(X)) 1061.64/298.19 , s(ok(X)) -> ok(s(X)) 1061.64/298.19 , length(mark(X)) -> mark(length(X)) 1061.64/298.19 , length(ok(X)) -> ok(length(X)) 1061.64/298.19 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1061.64/298.19 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1061.64/298.19 , take(X1, mark(X2)) -> mark(take(X1, X2)) 1061.64/298.19 , take(mark(X1), X2) -> mark(take(X1, X2)) 1061.64/298.19 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 1061.64/298.19 , uTake1(mark(X)) -> mark(uTake1(X)) 1061.64/298.19 , uTake1(ok(X)) -> ok(uTake1(X)) 1061.64/298.19 , uTake2(mark(X1), X2, X3, X4) -> mark(uTake2(X1, X2, X3, X4)) 1061.64/298.19 , uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.19 ok(uTake2(X1, X2, X3, X4)) 1061.64/298.19 , uLength(mark(X1), X2) -> mark(uLength(X1, X2)) 1061.64/298.19 , uLength(ok(X1), ok(X2)) -> ok(uLength(X1, X2)) 1061.64/298.19 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 1061.64/298.19 , proper(tt()) -> ok(tt()) 1061.64/298.19 , proper(isNatIList(X)) -> isNatIList(proper(X)) 1061.64/298.19 , proper(isNatList(X)) -> isNatList(proper(X)) 1061.64/298.19 , proper(isNat(X)) -> isNat(proper(X)) 1061.64/298.19 , proper(0()) -> ok(0()) 1061.64/298.19 , proper(s(X)) -> s(proper(X)) 1061.64/298.19 , proper(length(X)) -> length(proper(X)) 1061.64/298.19 , proper(zeros()) -> ok(zeros()) 1061.64/298.19 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1061.64/298.19 , proper(nil()) -> ok(nil()) 1061.64/298.19 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 1061.64/298.19 , proper(uTake1(X)) -> uTake1(proper(X)) 1061.64/298.19 , proper(uTake2(X1, X2, X3, X4)) -> 1061.64/298.19 uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) 1061.64/298.19 , proper(uLength(X1, X2)) -> uLength(proper(X1), proper(X2)) 1061.64/298.19 , top(mark(X)) -> top(proper(X)) 1061.64/298.19 , top(ok(X)) -> top(active(X)) } 1061.64/298.19 Obligation: 1061.64/298.19 runtime complexity 1061.64/298.19 Answer: 1061.64/298.19 MAYBE 1061.64/298.19 1061.64/298.19 We estimate the number of application of {1,23,24,25,26} by 1061.64/298.19 applications of Pre({1,23,24,25,26}) = {}. Here rules are labeled 1061.64/298.19 as follows: 1061.64/298.19 1061.64/298.19 DPs: 1061.64/298.19 { 1: active^#(zeros()) -> c_16(cons^#(0(), zeros())) 1061.64/298.19 , 2: and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) 1061.64/298.19 , 3: and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) 1061.64/298.19 , 4: and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) 1061.64/298.19 , 5: isNatList^#(ok(X)) -> c_32(isNatList^#(X)) 1061.64/298.19 , 6: isNat^#(ok(X)) -> c_33(isNat^#(X)) 1061.64/298.19 , 7: s^#(mark(X)) -> c_34(s^#(X)) 1061.64/298.19 , 8: s^#(ok(X)) -> c_35(s^#(X)) 1061.64/298.19 , 9: length^#(mark(X)) -> c_36(length^#(X)) 1061.64/298.19 , 10: length^#(ok(X)) -> c_37(length^#(X)) 1061.64/298.19 , 11: uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) 1061.64/298.19 , 12: uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) 1061.64/298.19 , 13: cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) 1061.64/298.19 , 14: cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) 1061.64/298.19 , 15: take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) 1061.64/298.19 , 16: take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) 1061.64/298.19 , 17: take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) 1061.64/298.19 , 18: uTake1^#(mark(X)) -> c_43(uTake1^#(X)) 1061.64/298.19 , 19: uTake1^#(ok(X)) -> c_44(uTake1^#(X)) 1061.64/298.19 , 20: uTake2^#(mark(X1), X2, X3, X4) -> 1061.64/298.19 c_45(uTake2^#(X1, X2, X3, X4)) 1061.64/298.19 , 21: uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.19 c_46(uTake2^#(X1, X2, X3, X4)) 1061.64/298.19 , 22: isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) 1061.64/298.19 , 23: proper^#(tt()) -> c_50() 1061.64/298.19 , 24: proper^#(0()) -> c_54() 1061.64/298.19 , 25: proper^#(zeros()) -> c_57() 1061.64/298.19 , 26: proper^#(nil()) -> c_59() 1061.64/298.19 , 27: top^#(mark(X)) -> c_64(top^#(proper(X))) 1061.64/298.19 , 28: top^#(ok(X)) -> c_65(top^#(active(X))) } 1061.64/298.19 1061.64/298.19 We are left with following problem, upon which TcT provides the 1061.64/298.19 certificate MAYBE. 1061.64/298.19 1061.64/298.19 Strict DPs: 1061.64/298.19 { and^#(X1, mark(X2)) -> c_28(and^#(X1, X2)) 1061.64/298.19 , and^#(mark(X1), X2) -> c_29(and^#(X1, X2)) 1061.64/298.19 , and^#(ok(X1), ok(X2)) -> c_30(and^#(X1, X2)) 1061.64/298.19 , isNatList^#(ok(X)) -> c_32(isNatList^#(X)) 1061.64/298.19 , isNat^#(ok(X)) -> c_33(isNat^#(X)) 1061.64/298.19 , s^#(mark(X)) -> c_34(s^#(X)) 1061.64/298.19 , s^#(ok(X)) -> c_35(s^#(X)) 1061.64/298.19 , length^#(mark(X)) -> c_36(length^#(X)) 1061.64/298.19 , length^#(ok(X)) -> c_37(length^#(X)) 1061.64/298.19 , uLength^#(mark(X1), X2) -> c_47(uLength^#(X1, X2)) 1061.64/298.19 , uLength^#(ok(X1), ok(X2)) -> c_48(uLength^#(X1, X2)) 1061.64/298.19 , cons^#(mark(X1), X2) -> c_38(cons^#(X1, X2)) 1061.64/298.19 , cons^#(ok(X1), ok(X2)) -> c_39(cons^#(X1, X2)) 1061.64/298.19 , take^#(X1, mark(X2)) -> c_40(take^#(X1, X2)) 1061.64/298.19 , take^#(mark(X1), X2) -> c_41(take^#(X1, X2)) 1061.64/298.19 , take^#(ok(X1), ok(X2)) -> c_42(take^#(X1, X2)) 1061.64/298.19 , uTake1^#(mark(X)) -> c_43(uTake1^#(X)) 1061.64/298.19 , uTake1^#(ok(X)) -> c_44(uTake1^#(X)) 1061.64/298.19 , uTake2^#(mark(X1), X2, X3, X4) -> c_45(uTake2^#(X1, X2, X3, X4)) 1061.64/298.19 , uTake2^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.19 c_46(uTake2^#(X1, X2, X3, X4)) 1061.64/298.19 , isNatIList^#(ok(X)) -> c_31(isNatIList^#(X)) 1061.64/298.19 , top^#(mark(X)) -> c_64(top^#(proper(X))) 1061.64/298.19 , top^#(ok(X)) -> c_65(top^#(active(X))) } 1061.64/298.19 Strict Trs: 1061.64/298.19 { active(and(X1, X2)) -> and(X1, active(X2)) 1061.64/298.19 , active(and(X1, X2)) -> and(active(X1), X2) 1061.64/298.19 , active(and(tt(), T)) -> mark(T) 1061.64/298.19 , active(isNatIList(IL)) -> mark(isNatList(IL)) 1061.64/298.19 , active(isNatIList(zeros())) -> mark(tt()) 1061.64/298.19 , active(isNatIList(cons(N, IL))) -> 1061.64/298.19 mark(and(isNat(N), isNatIList(IL))) 1061.64/298.19 , active(isNatList(cons(N, L))) -> 1061.64/298.19 mark(and(isNat(N), isNatList(L))) 1061.64/298.19 , active(isNatList(nil())) -> mark(tt()) 1061.64/298.19 , active(isNatList(take(N, IL))) -> 1061.64/298.19 mark(and(isNat(N), isNatIList(IL))) 1061.64/298.19 , active(isNat(0())) -> mark(tt()) 1061.64/298.19 , active(isNat(s(N))) -> mark(isNat(N)) 1061.64/298.19 , active(isNat(length(L))) -> mark(isNatList(L)) 1061.64/298.19 , active(s(X)) -> s(active(X)) 1061.64/298.19 , active(length(X)) -> length(active(X)) 1061.64/298.19 , active(length(cons(N, L))) -> 1061.64/298.19 mark(uLength(and(isNat(N), isNatList(L)), L)) 1061.64/298.19 , active(zeros()) -> mark(cons(0(), zeros())) 1061.64/298.19 , active(cons(X1, X2)) -> cons(active(X1), X2) 1061.64/298.19 , active(take(X1, X2)) -> take(X1, active(X2)) 1061.64/298.19 , active(take(X1, X2)) -> take(active(X1), X2) 1061.64/298.19 , active(take(0(), IL)) -> mark(uTake1(isNatIList(IL))) 1061.64/298.19 , active(take(s(M), cons(N, IL))) -> 1061.64/298.19 mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), 1061.64/298.19 M, 1061.64/298.19 N, 1061.64/298.19 IL)) 1061.64/298.19 , active(uTake1(X)) -> uTake1(active(X)) 1061.64/298.19 , active(uTake1(tt())) -> mark(nil()) 1061.64/298.19 , active(uTake2(X1, X2, X3, X4)) -> uTake2(active(X1), X2, X3, X4) 1061.64/298.19 , active(uTake2(tt(), M, N, IL)) -> mark(cons(N, take(M, IL))) 1061.64/298.19 , active(uLength(X1, X2)) -> uLength(active(X1), X2) 1061.64/298.19 , active(uLength(tt(), L)) -> mark(s(length(L))) 1061.64/298.19 , and(X1, mark(X2)) -> mark(and(X1, X2)) 1061.64/298.19 , and(mark(X1), X2) -> mark(and(X1, X2)) 1061.64/298.19 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 1061.64/298.19 , isNatIList(ok(X)) -> ok(isNatIList(X)) 1061.64/298.19 , isNatList(ok(X)) -> ok(isNatList(X)) 1061.64/298.19 , isNat(ok(X)) -> ok(isNat(X)) 1061.64/298.19 , s(mark(X)) -> mark(s(X)) 1061.64/298.19 , s(ok(X)) -> ok(s(X)) 1061.64/298.19 , length(mark(X)) -> mark(length(X)) 1061.64/298.19 , length(ok(X)) -> ok(length(X)) 1061.64/298.19 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1061.64/298.19 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1061.64/298.19 , take(X1, mark(X2)) -> mark(take(X1, X2)) 1061.64/298.19 , take(mark(X1), X2) -> mark(take(X1, X2)) 1061.64/298.19 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 1061.64/298.19 , uTake1(mark(X)) -> mark(uTake1(X)) 1061.64/298.19 , uTake1(ok(X)) -> ok(uTake1(X)) 1061.64/298.19 , uTake2(mark(X1), X2, X3, X4) -> mark(uTake2(X1, X2, X3, X4)) 1061.64/298.19 , uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1061.64/298.19 ok(uTake2(X1, X2, X3, X4)) 1061.64/298.19 , uLength(mark(X1), X2) -> mark(uLength(X1, X2)) 1061.64/298.19 , uLength(ok(X1), ok(X2)) -> ok(uLength(X1, X2)) 1061.64/298.19 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 1061.64/298.19 , proper(tt()) -> ok(tt()) 1061.64/298.19 , proper(isNatIList(X)) -> isNatIList(proper(X)) 1061.64/298.19 , proper(isNatList(X)) -> isNatList(proper(X)) 1061.64/298.19 , proper(isNat(X)) -> isNat(proper(X)) 1061.64/298.19 , proper(0()) -> ok(0()) 1061.64/298.19 , proper(s(X)) -> s(proper(X)) 1061.64/298.19 , proper(length(X)) -> length(proper(X)) 1061.64/298.19 , proper(zeros()) -> ok(zeros()) 1061.64/298.19 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1061.64/298.19 , proper(nil()) -> ok(nil()) 1061.64/298.19 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 1061.64/298.19 , proper(uTake1(X)) -> uTake1(proper(X)) 1061.64/298.19 , proper(uTake2(X1, X2, X3, X4)) -> 1061.64/298.19 uTake2(proper(X1), proper(X2), proper(X3), proper(X4)) 1061.64/298.19 , proper(uLength(X1, X2)) -> uLength(proper(X1), proper(X2)) 1061.64/298.19 , top(mark(X)) -> top(proper(X)) 1061.64/298.19 , top(ok(X)) -> top(active(X)) } 1061.64/298.19 Weak DPs: 1061.64/298.19 { active^#(zeros()) -> c_16(cons^#(0(), zeros())) 1061.64/298.19 , proper^#(tt()) -> c_50() 1061.64/298.19 , proper^#(0()) -> c_54() 1061.64/298.19 , proper^#(zeros()) -> c_57() 1061.64/298.19 , proper^#(nil()) -> c_59() } 1061.64/298.19 Obligation: 1061.64/298.19 runtime complexity 1061.64/298.19 Answer: 1061.64/298.19 MAYBE 1061.64/298.19 1061.64/298.19 Empty strict component of the problem is NOT empty. 1061.64/298.19 1061.64/298.19 1061.64/298.19 Arrrr.. 1062.25/298.56 EOF