MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { active(zeros()) -> mark(cons(0(), zeros())) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(U11(X)) -> U11(active(X)) , active(U11(tt())) -> mark(tt()) , active(U21(X)) -> U21(active(X)) , active(U21(tt())) -> mark(tt()) , active(U31(X)) -> U31(active(X)) , active(U31(tt())) -> mark(tt()) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), V2)) -> mark(U42(isNatIList(V2))) , active(U42(X)) -> U42(active(X)) , active(U42(tt())) -> mark(tt()) , active(isNatIList(V)) -> mark(U31(isNatList(V))) , active(isNatIList(zeros())) -> mark(tt()) , active(isNatIList(cons(V1, V2))) -> mark(U41(isNat(V1), V2)) , active(U51(X1, X2)) -> U51(active(X1), X2) , active(U51(tt(), V2)) -> mark(U52(isNatList(V2))) , active(U52(X)) -> U52(active(X)) , active(U52(tt())) -> mark(tt()) , active(isNatList(cons(V1, V2))) -> mark(U51(isNat(V1), V2)) , active(isNatList(nil())) -> mark(tt()) , active(isNatList(take(V1, V2))) -> mark(U61(isNat(V1), V2)) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V2)) -> mark(U62(isNatIList(V2))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), L, N)) -> mark(U72(isNat(N), L)) , active(U72(X1, X2)) -> U72(active(X1), X2) , active(U72(tt(), L)) -> mark(s(length(L))) , active(isNat(0())) -> mark(tt()) , active(isNat(s(V1))) -> mark(U21(isNat(V1))) , active(isNat(length(V1))) -> mark(U11(isNatList(V1))) , active(s(X)) -> s(active(X)) , active(length(X)) -> length(active(X)) , active(length(cons(N, L))) -> mark(U71(isNatList(L), L, N)) , active(length(nil())) -> mark(0()) , active(U81(X)) -> U81(active(X)) , active(U81(tt())) -> mark(nil()) , active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4) , active(U91(tt(), IL, M, N)) -> mark(U92(isNat(M), IL, M, N)) , active(U92(X1, X2, X3, X4)) -> U92(active(X1), X2, X3, X4) , active(U92(tt(), IL, M, N)) -> mark(U93(isNat(N), IL, M, N)) , active(U93(X1, X2, X3, X4)) -> U93(active(X1), X2, X3, X4) , active(U93(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(take(0(), IL)) -> mark(U81(isNatIList(IL))) , active(take(s(M), cons(N, IL))) -> mark(U91(isNatIList(IL), IL, M, N)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , U11(mark(X)) -> mark(U11(X)) , U11(ok(X)) -> ok(U11(X)) , U21(mark(X)) -> mark(U21(X)) , U21(ok(X)) -> ok(U21(X)) , U31(mark(X)) -> mark(U31(X)) , U31(ok(X)) -> ok(U31(X)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , U42(mark(X)) -> mark(U42(X)) , U42(ok(X)) -> ok(U42(X)) , isNatIList(ok(X)) -> ok(isNatIList(X)) , U51(mark(X1), X2) -> mark(U51(X1, X2)) , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) , U52(mark(X)) -> mark(U52(X)) , U52(ok(X)) -> ok(U52(X)) , isNatList(ok(X)) -> ok(isNatList(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , U72(mark(X1), X2) -> mark(U72(X1, X2)) , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , length(mark(X)) -> mark(length(X)) , length(ok(X)) -> ok(length(X)) , U81(mark(X)) -> mark(U81(X)) , U81(ok(X)) -> ok(U81(X)) , U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)) , U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)) , U92(mark(X1), X2, X3, X4) -> mark(U92(X1, X2, X3, X4)) , U92(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U92(X1, X2, X3, X4)) , U93(mark(X1), X2, X3, X4) -> mark(U93(X1, X2, X3, X4)) , U93(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U93(X1, X2, X3, X4)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , proper(zeros()) -> ok(zeros()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(U11(X)) -> U11(proper(X)) , proper(tt()) -> ok(tt()) , proper(U21(X)) -> U21(proper(X)) , proper(U31(X)) -> U31(proper(X)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(U42(X)) -> U42(proper(X)) , proper(isNatIList(X)) -> isNatIList(proper(X)) , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) , proper(U52(X)) -> U52(proper(X)) , proper(isNatList(X)) -> isNatList(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(length(X)) -> length(proper(X)) , proper(U81(X)) -> U81(proper(X)) , proper(nil()) -> ok(nil()) , proper(U91(X1, X2, X3, X4)) -> U91(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U92(X1, X2, X3, X4)) -> U92(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U93(X1, X2, X3, X4)) -> U93(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { active^#(zeros()) -> c_1(cons^#(0(), zeros())) , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) , active^#(U11(X)) -> c_3(U11^#(active(X))) , active^#(U11(tt())) -> c_4() , active^#(U21(X)) -> c_5(U21^#(active(X))) , active^#(U21(tt())) -> c_6() , active^#(U31(X)) -> c_7(U31^#(active(X))) , active^#(U31(tt())) -> c_8() , active^#(U41(X1, X2)) -> c_9(U41^#(active(X1), X2)) , active^#(U41(tt(), V2)) -> c_10(U42^#(isNatIList(V2))) , active^#(U42(X)) -> c_11(U42^#(active(X))) , active^#(U42(tt())) -> c_12() , active^#(isNatIList(V)) -> c_13(U31^#(isNatList(V))) , active^#(isNatIList(zeros())) -> c_14() , active^#(isNatIList(cons(V1, V2))) -> c_15(U41^#(isNat(V1), V2)) , active^#(U51(X1, X2)) -> c_16(U51^#(active(X1), X2)) , active^#(U51(tt(), V2)) -> c_17(U52^#(isNatList(V2))) , active^#(U52(X)) -> c_18(U52^#(active(X))) , active^#(U52(tt())) -> c_19() , active^#(isNatList(cons(V1, V2))) -> c_20(U51^#(isNat(V1), V2)) , active^#(isNatList(nil())) -> c_21() , active^#(isNatList(take(V1, V2))) -> c_22(U61^#(isNat(V1), V2)) , active^#(U61(X1, X2)) -> c_23(U61^#(active(X1), X2)) , active^#(U61(tt(), V2)) -> c_24(U62^#(isNatIList(V2))) , active^#(U62(X)) -> c_25(U62^#(active(X))) , active^#(U62(tt())) -> c_26() , active^#(U71(X1, X2, X3)) -> c_27(U71^#(active(X1), X2, X3)) , active^#(U71(tt(), L, N)) -> c_28(U72^#(isNat(N), L)) , active^#(U72(X1, X2)) -> c_29(U72^#(active(X1), X2)) , active^#(U72(tt(), L)) -> c_30(s^#(length(L))) , active^#(isNat(0())) -> c_31() , active^#(isNat(s(V1))) -> c_32(U21^#(isNat(V1))) , active^#(isNat(length(V1))) -> c_33(U11^#(isNatList(V1))) , active^#(s(X)) -> c_34(s^#(active(X))) , active^#(length(X)) -> c_35(length^#(active(X))) , active^#(length(cons(N, L))) -> c_36(U71^#(isNatList(L), L, N)) , active^#(length(nil())) -> c_37() , active^#(U81(X)) -> c_38(U81^#(active(X))) , active^#(U81(tt())) -> c_39() , active^#(U91(X1, X2, X3, X4)) -> c_40(U91^#(active(X1), X2, X3, X4)) , active^#(U91(tt(), IL, M, N)) -> c_41(U92^#(isNat(M), IL, M, N)) , active^#(U92(X1, X2, X3, X4)) -> c_42(U92^#(active(X1), X2, X3, X4)) , active^#(U92(tt(), IL, M, N)) -> c_43(U93^#(isNat(N), IL, M, N)) , active^#(U93(X1, X2, X3, X4)) -> c_44(U93^#(active(X1), X2, X3, X4)) , active^#(U93(tt(), IL, M, N)) -> c_45(cons^#(N, take(M, IL))) , active^#(take(X1, X2)) -> c_46(take^#(X1, active(X2))) , active^#(take(X1, X2)) -> c_47(take^#(active(X1), X2)) , active^#(take(0(), IL)) -> c_48(U81^#(isNatIList(IL))) , active^#(take(s(M), cons(N, IL))) -> c_49(U91^#(isNatIList(IL), IL, M, N)) , cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) , U11^#(mark(X)) -> c_52(U11^#(X)) , U11^#(ok(X)) -> c_53(U11^#(X)) , U21^#(mark(X)) -> c_54(U21^#(X)) , U21^#(ok(X)) -> c_55(U21^#(X)) , U31^#(mark(X)) -> c_56(U31^#(X)) , U31^#(ok(X)) -> c_57(U31^#(X)) , U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) , U42^#(mark(X)) -> c_60(U42^#(X)) , U42^#(ok(X)) -> c_61(U42^#(X)) , U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) , U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) , U52^#(mark(X)) -> c_65(U52^#(X)) , U52^#(ok(X)) -> c_66(U52^#(X)) , U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) , U62^#(mark(X)) -> c_70(U62^#(X)) , U62^#(ok(X)) -> c_71(U62^#(X)) , U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) , U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) , s^#(mark(X)) -> c_77(s^#(X)) , s^#(ok(X)) -> c_78(s^#(X)) , length^#(mark(X)) -> c_79(length^#(X)) , length^#(ok(X)) -> c_80(length^#(X)) , U81^#(mark(X)) -> c_81(U81^#(X)) , U81^#(ok(X)) -> c_82(U81^#(X)) , U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) , U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) , U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) , U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) , U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) , U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) , take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) , isNatIList^#(ok(X)) -> c_62(isNatIList^#(X)) , isNatList^#(ok(X)) -> c_67(isNatList^#(X)) , isNat^#(ok(X)) -> c_76(isNat^#(X)) , proper^#(zeros()) -> c_92() , proper^#(cons(X1, X2)) -> c_93(cons^#(proper(X1), proper(X2))) , proper^#(0()) -> c_94() , proper^#(U11(X)) -> c_95(U11^#(proper(X))) , proper^#(tt()) -> c_96() , proper^#(U21(X)) -> c_97(U21^#(proper(X))) , proper^#(U31(X)) -> c_98(U31^#(proper(X))) , proper^#(U41(X1, X2)) -> c_99(U41^#(proper(X1), proper(X2))) , proper^#(U42(X)) -> c_100(U42^#(proper(X))) , proper^#(isNatIList(X)) -> c_101(isNatIList^#(proper(X))) , proper^#(U51(X1, X2)) -> c_102(U51^#(proper(X1), proper(X2))) , proper^#(U52(X)) -> c_103(U52^#(proper(X))) , proper^#(isNatList(X)) -> c_104(isNatList^#(proper(X))) , proper^#(U61(X1, X2)) -> c_105(U61^#(proper(X1), proper(X2))) , proper^#(U62(X)) -> c_106(U62^#(proper(X))) , proper^#(U71(X1, X2, X3)) -> c_107(U71^#(proper(X1), proper(X2), proper(X3))) , proper^#(U72(X1, X2)) -> c_108(U72^#(proper(X1), proper(X2))) , proper^#(isNat(X)) -> c_109(isNat^#(proper(X))) , proper^#(s(X)) -> c_110(s^#(proper(X))) , proper^#(length(X)) -> c_111(length^#(proper(X))) , proper^#(U81(X)) -> c_112(U81^#(proper(X))) , proper^#(nil()) -> c_113() , proper^#(U91(X1, X2, X3, X4)) -> c_114(U91^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U92(X1, X2, X3, X4)) -> c_115(U92^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U93(X1, X2, X3, X4)) -> c_116(U93^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(take(X1, X2)) -> c_117(take^#(proper(X1), proper(X2))) , top^#(mark(X)) -> c_118(top^#(proper(X))) , top^#(ok(X)) -> c_119(top^#(active(X))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(zeros()) -> c_1(cons^#(0(), zeros())) , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) , active^#(U11(X)) -> c_3(U11^#(active(X))) , active^#(U11(tt())) -> c_4() , active^#(U21(X)) -> c_5(U21^#(active(X))) , active^#(U21(tt())) -> c_6() , active^#(U31(X)) -> c_7(U31^#(active(X))) , active^#(U31(tt())) -> c_8() , active^#(U41(X1, X2)) -> c_9(U41^#(active(X1), X2)) , active^#(U41(tt(), V2)) -> c_10(U42^#(isNatIList(V2))) , active^#(U42(X)) -> c_11(U42^#(active(X))) , active^#(U42(tt())) -> c_12() , active^#(isNatIList(V)) -> c_13(U31^#(isNatList(V))) , active^#(isNatIList(zeros())) -> c_14() , active^#(isNatIList(cons(V1, V2))) -> c_15(U41^#(isNat(V1), V2)) , active^#(U51(X1, X2)) -> c_16(U51^#(active(X1), X2)) , active^#(U51(tt(), V2)) -> c_17(U52^#(isNatList(V2))) , active^#(U52(X)) -> c_18(U52^#(active(X))) , active^#(U52(tt())) -> c_19() , active^#(isNatList(cons(V1, V2))) -> c_20(U51^#(isNat(V1), V2)) , active^#(isNatList(nil())) -> c_21() , active^#(isNatList(take(V1, V2))) -> c_22(U61^#(isNat(V1), V2)) , active^#(U61(X1, X2)) -> c_23(U61^#(active(X1), X2)) , active^#(U61(tt(), V2)) -> c_24(U62^#(isNatIList(V2))) , active^#(U62(X)) -> c_25(U62^#(active(X))) , active^#(U62(tt())) -> c_26() , active^#(U71(X1, X2, X3)) -> c_27(U71^#(active(X1), X2, X3)) , active^#(U71(tt(), L, N)) -> c_28(U72^#(isNat(N), L)) , active^#(U72(X1, X2)) -> c_29(U72^#(active(X1), X2)) , active^#(U72(tt(), L)) -> c_30(s^#(length(L))) , active^#(isNat(0())) -> c_31() , active^#(isNat(s(V1))) -> c_32(U21^#(isNat(V1))) , active^#(isNat(length(V1))) -> c_33(U11^#(isNatList(V1))) , active^#(s(X)) -> c_34(s^#(active(X))) , active^#(length(X)) -> c_35(length^#(active(X))) , active^#(length(cons(N, L))) -> c_36(U71^#(isNatList(L), L, N)) , active^#(length(nil())) -> c_37() , active^#(U81(X)) -> c_38(U81^#(active(X))) , active^#(U81(tt())) -> c_39() , active^#(U91(X1, X2, X3, X4)) -> c_40(U91^#(active(X1), X2, X3, X4)) , active^#(U91(tt(), IL, M, N)) -> c_41(U92^#(isNat(M), IL, M, N)) , active^#(U92(X1, X2, X3, X4)) -> c_42(U92^#(active(X1), X2, X3, X4)) , active^#(U92(tt(), IL, M, N)) -> c_43(U93^#(isNat(N), IL, M, N)) , active^#(U93(X1, X2, X3, X4)) -> c_44(U93^#(active(X1), X2, X3, X4)) , active^#(U93(tt(), IL, M, N)) -> c_45(cons^#(N, take(M, IL))) , active^#(take(X1, X2)) -> c_46(take^#(X1, active(X2))) , active^#(take(X1, X2)) -> c_47(take^#(active(X1), X2)) , active^#(take(0(), IL)) -> c_48(U81^#(isNatIList(IL))) , active^#(take(s(M), cons(N, IL))) -> c_49(U91^#(isNatIList(IL), IL, M, N)) , cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) , U11^#(mark(X)) -> c_52(U11^#(X)) , U11^#(ok(X)) -> c_53(U11^#(X)) , U21^#(mark(X)) -> c_54(U21^#(X)) , U21^#(ok(X)) -> c_55(U21^#(X)) , U31^#(mark(X)) -> c_56(U31^#(X)) , U31^#(ok(X)) -> c_57(U31^#(X)) , U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) , U42^#(mark(X)) -> c_60(U42^#(X)) , U42^#(ok(X)) -> c_61(U42^#(X)) , U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) , U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) , U52^#(mark(X)) -> c_65(U52^#(X)) , U52^#(ok(X)) -> c_66(U52^#(X)) , U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) , U62^#(mark(X)) -> c_70(U62^#(X)) , U62^#(ok(X)) -> c_71(U62^#(X)) , U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) , U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) , s^#(mark(X)) -> c_77(s^#(X)) , s^#(ok(X)) -> c_78(s^#(X)) , length^#(mark(X)) -> c_79(length^#(X)) , length^#(ok(X)) -> c_80(length^#(X)) , U81^#(mark(X)) -> c_81(U81^#(X)) , U81^#(ok(X)) -> c_82(U81^#(X)) , U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) , U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) , U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) , U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) , U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) , U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) , take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) , isNatIList^#(ok(X)) -> c_62(isNatIList^#(X)) , isNatList^#(ok(X)) -> c_67(isNatList^#(X)) , isNat^#(ok(X)) -> c_76(isNat^#(X)) , proper^#(zeros()) -> c_92() , proper^#(cons(X1, X2)) -> c_93(cons^#(proper(X1), proper(X2))) , proper^#(0()) -> c_94() , proper^#(U11(X)) -> c_95(U11^#(proper(X))) , proper^#(tt()) -> c_96() , proper^#(U21(X)) -> c_97(U21^#(proper(X))) , proper^#(U31(X)) -> c_98(U31^#(proper(X))) , proper^#(U41(X1, X2)) -> c_99(U41^#(proper(X1), proper(X2))) , proper^#(U42(X)) -> c_100(U42^#(proper(X))) , proper^#(isNatIList(X)) -> c_101(isNatIList^#(proper(X))) , proper^#(U51(X1, X2)) -> c_102(U51^#(proper(X1), proper(X2))) , proper^#(U52(X)) -> c_103(U52^#(proper(X))) , proper^#(isNatList(X)) -> c_104(isNatList^#(proper(X))) , proper^#(U61(X1, X2)) -> c_105(U61^#(proper(X1), proper(X2))) , proper^#(U62(X)) -> c_106(U62^#(proper(X))) , proper^#(U71(X1, X2, X3)) -> c_107(U71^#(proper(X1), proper(X2), proper(X3))) , proper^#(U72(X1, X2)) -> c_108(U72^#(proper(X1), proper(X2))) , proper^#(isNat(X)) -> c_109(isNat^#(proper(X))) , proper^#(s(X)) -> c_110(s^#(proper(X))) , proper^#(length(X)) -> c_111(length^#(proper(X))) , proper^#(U81(X)) -> c_112(U81^#(proper(X))) , proper^#(nil()) -> c_113() , proper^#(U91(X1, X2, X3, X4)) -> c_114(U91^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U92(X1, X2, X3, X4)) -> c_115(U92^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U93(X1, X2, X3, X4)) -> c_116(U93^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(take(X1, X2)) -> c_117(take^#(proper(X1), proper(X2))) , top^#(mark(X)) -> c_118(top^#(proper(X))) , top^#(ok(X)) -> c_119(top^#(active(X))) } Strict Trs: { active(zeros()) -> mark(cons(0(), zeros())) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(U11(X)) -> U11(active(X)) , active(U11(tt())) -> mark(tt()) , active(U21(X)) -> U21(active(X)) , active(U21(tt())) -> mark(tt()) , active(U31(X)) -> U31(active(X)) , active(U31(tt())) -> mark(tt()) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), V2)) -> mark(U42(isNatIList(V2))) , active(U42(X)) -> U42(active(X)) , active(U42(tt())) -> mark(tt()) , active(isNatIList(V)) -> mark(U31(isNatList(V))) , active(isNatIList(zeros())) -> mark(tt()) , active(isNatIList(cons(V1, V2))) -> mark(U41(isNat(V1), V2)) , active(U51(X1, X2)) -> U51(active(X1), X2) , active(U51(tt(), V2)) -> mark(U52(isNatList(V2))) , active(U52(X)) -> U52(active(X)) , active(U52(tt())) -> mark(tt()) , active(isNatList(cons(V1, V2))) -> mark(U51(isNat(V1), V2)) , active(isNatList(nil())) -> mark(tt()) , active(isNatList(take(V1, V2))) -> mark(U61(isNat(V1), V2)) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V2)) -> mark(U62(isNatIList(V2))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), L, N)) -> mark(U72(isNat(N), L)) , active(U72(X1, X2)) -> U72(active(X1), X2) , active(U72(tt(), L)) -> mark(s(length(L))) , active(isNat(0())) -> mark(tt()) , active(isNat(s(V1))) -> mark(U21(isNat(V1))) , active(isNat(length(V1))) -> mark(U11(isNatList(V1))) , active(s(X)) -> s(active(X)) , active(length(X)) -> length(active(X)) , active(length(cons(N, L))) -> mark(U71(isNatList(L), L, N)) , active(length(nil())) -> mark(0()) , active(U81(X)) -> U81(active(X)) , active(U81(tt())) -> mark(nil()) , active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4) , active(U91(tt(), IL, M, N)) -> mark(U92(isNat(M), IL, M, N)) , active(U92(X1, X2, X3, X4)) -> U92(active(X1), X2, X3, X4) , active(U92(tt(), IL, M, N)) -> mark(U93(isNat(N), IL, M, N)) , active(U93(X1, X2, X3, X4)) -> U93(active(X1), X2, X3, X4) , active(U93(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(take(0(), IL)) -> mark(U81(isNatIList(IL))) , active(take(s(M), cons(N, IL))) -> mark(U91(isNatIList(IL), IL, M, N)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , U11(mark(X)) -> mark(U11(X)) , U11(ok(X)) -> ok(U11(X)) , U21(mark(X)) -> mark(U21(X)) , U21(ok(X)) -> ok(U21(X)) , U31(mark(X)) -> mark(U31(X)) , U31(ok(X)) -> ok(U31(X)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , U42(mark(X)) -> mark(U42(X)) , U42(ok(X)) -> ok(U42(X)) , isNatIList(ok(X)) -> ok(isNatIList(X)) , U51(mark(X1), X2) -> mark(U51(X1, X2)) , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) , U52(mark(X)) -> mark(U52(X)) , U52(ok(X)) -> ok(U52(X)) , isNatList(ok(X)) -> ok(isNatList(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , U72(mark(X1), X2) -> mark(U72(X1, X2)) , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , length(mark(X)) -> mark(length(X)) , length(ok(X)) -> ok(length(X)) , U81(mark(X)) -> mark(U81(X)) , U81(ok(X)) -> ok(U81(X)) , U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)) , U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)) , U92(mark(X1), X2, X3, X4) -> mark(U92(X1, X2, X3, X4)) , U92(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U92(X1, X2, X3, X4)) , U93(mark(X1), X2, X3, X4) -> mark(U93(X1, X2, X3, X4)) , U93(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U93(X1, X2, X3, X4)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , proper(zeros()) -> ok(zeros()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(U11(X)) -> U11(proper(X)) , proper(tt()) -> ok(tt()) , proper(U21(X)) -> U21(proper(X)) , proper(U31(X)) -> U31(proper(X)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(U42(X)) -> U42(proper(X)) , proper(isNatIList(X)) -> isNatIList(proper(X)) , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) , proper(U52(X)) -> U52(proper(X)) , proper(isNatList(X)) -> isNatList(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(length(X)) -> length(proper(X)) , proper(U81(X)) -> U81(proper(X)) , proper(nil()) -> ok(nil()) , proper(U91(X1, X2, X3, X4)) -> U91(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U92(X1, X2, X3, X4)) -> U92(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U93(X1, X2, X3, X4)) -> U93(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE Consider the dependency graph: 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) 2: active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) :51 -->_1 cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) :50 3: active^#(U11(X)) -> c_3(U11^#(active(X))) -->_1 U11^#(ok(X)) -> c_53(U11^#(X)) :53 -->_1 U11^#(mark(X)) -> c_52(U11^#(X)) :52 4: active^#(U11(tt())) -> c_4() 5: active^#(U21(X)) -> c_5(U21^#(active(X))) -->_1 U21^#(ok(X)) -> c_55(U21^#(X)) :55 -->_1 U21^#(mark(X)) -> c_54(U21^#(X)) :54 6: active^#(U21(tt())) -> c_6() 7: active^#(U31(X)) -> c_7(U31^#(active(X))) -->_1 U31^#(ok(X)) -> c_57(U31^#(X)) :57 -->_1 U31^#(mark(X)) -> c_56(U31^#(X)) :56 8: active^#(U31(tt())) -> c_8() 9: active^#(U41(X1, X2)) -> c_9(U41^#(active(X1), X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) :59 -->_1 U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) :58 10: active^#(U41(tt(), V2)) -> c_10(U42^#(isNatIList(V2))) -->_1 U42^#(ok(X)) -> c_61(U42^#(X)) :61 -->_1 U42^#(mark(X)) -> c_60(U42^#(X)) :60 11: active^#(U42(X)) -> c_11(U42^#(active(X))) -->_1 U42^#(ok(X)) -> c_61(U42^#(X)) :61 -->_1 U42^#(mark(X)) -> c_60(U42^#(X)) :60 12: active^#(U42(tt())) -> c_12() 13: active^#(isNatIList(V)) -> c_13(U31^#(isNatList(V))) -->_1 U31^#(ok(X)) -> c_57(U31^#(X)) :57 -->_1 U31^#(mark(X)) -> c_56(U31^#(X)) :56 14: active^#(isNatIList(zeros())) -> c_14() 15: active^#(isNatIList(cons(V1, V2))) -> c_15(U41^#(isNat(V1), V2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) :59 -->_1 U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) :58 16: active^#(U51(X1, X2)) -> c_16(U51^#(active(X1), X2)) -->_1 U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) :63 -->_1 U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) :62 17: active^#(U51(tt(), V2)) -> c_17(U52^#(isNatList(V2))) -->_1 U52^#(ok(X)) -> c_66(U52^#(X)) :65 -->_1 U52^#(mark(X)) -> c_65(U52^#(X)) :64 18: active^#(U52(X)) -> c_18(U52^#(active(X))) -->_1 U52^#(ok(X)) -> c_66(U52^#(X)) :65 -->_1 U52^#(mark(X)) -> c_65(U52^#(X)) :64 19: active^#(U52(tt())) -> c_19() 20: active^#(isNatList(cons(V1, V2))) -> c_20(U51^#(isNat(V1), V2)) -->_1 U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) :63 -->_1 U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) :62 21: active^#(isNatList(nil())) -> c_21() 22: active^#(isNatList(take(V1, V2))) -> c_22(U61^#(isNat(V1), V2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) :67 -->_1 U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) :66 23: active^#(U61(X1, X2)) -> c_23(U61^#(active(X1), X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) :67 -->_1 U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) :66 24: active^#(U61(tt(), V2)) -> c_24(U62^#(isNatIList(V2))) -->_1 U62^#(ok(X)) -> c_71(U62^#(X)) :69 -->_1 U62^#(mark(X)) -> c_70(U62^#(X)) :68 25: active^#(U62(X)) -> c_25(U62^#(active(X))) -->_1 U62^#(ok(X)) -> c_71(U62^#(X)) :69 -->_1 U62^#(mark(X)) -> c_70(U62^#(X)) :68 26: active^#(U62(tt())) -> c_26() 27: active^#(U71(X1, X2, X3)) -> c_27(U71^#(active(X1), X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :71 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :70 28: active^#(U71(tt(), L, N)) -> c_28(U72^#(isNat(N), L)) -->_1 U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) :73 -->_1 U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) :72 29: active^#(U72(X1, X2)) -> c_29(U72^#(active(X1), X2)) -->_1 U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) :73 -->_1 U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) :72 30: active^#(U72(tt(), L)) -> c_30(s^#(length(L))) -->_1 s^#(ok(X)) -> c_78(s^#(X)) :75 -->_1 s^#(mark(X)) -> c_77(s^#(X)) :74 31: active^#(isNat(0())) -> c_31() 32: active^#(isNat(s(V1))) -> c_32(U21^#(isNat(V1))) -->_1 U21^#(ok(X)) -> c_55(U21^#(X)) :55 -->_1 U21^#(mark(X)) -> c_54(U21^#(X)) :54 33: active^#(isNat(length(V1))) -> c_33(U11^#(isNatList(V1))) -->_1 U11^#(ok(X)) -> c_53(U11^#(X)) :53 -->_1 U11^#(mark(X)) -> c_52(U11^#(X)) :52 34: active^#(s(X)) -> c_34(s^#(active(X))) -->_1 s^#(ok(X)) -> c_78(s^#(X)) :75 -->_1 s^#(mark(X)) -> c_77(s^#(X)) :74 35: active^#(length(X)) -> c_35(length^#(active(X))) -->_1 length^#(ok(X)) -> c_80(length^#(X)) :77 -->_1 length^#(mark(X)) -> c_79(length^#(X)) :76 36: active^#(length(cons(N, L))) -> c_36(U71^#(isNatList(L), L, N)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :71 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :70 37: active^#(length(nil())) -> c_37() 38: active^#(U81(X)) -> c_38(U81^#(active(X))) -->_1 U81^#(ok(X)) -> c_82(U81^#(X)) :79 -->_1 U81^#(mark(X)) -> c_81(U81^#(X)) :78 39: active^#(U81(tt())) -> c_39() 40: active^#(U91(X1, X2, X3, X4)) -> c_40(U91^#(active(X1), X2, X3, X4)) -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) :81 -->_1 U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) :80 41: active^#(U91(tt(), IL, M, N)) -> c_41(U92^#(isNat(M), IL, M, N)) -->_1 U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) :83 -->_1 U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) :82 42: active^#(U92(X1, X2, X3, X4)) -> c_42(U92^#(active(X1), X2, X3, X4)) -->_1 U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) :83 -->_1 U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) :82 43: active^#(U92(tt(), IL, M, N)) -> c_43(U93^#(isNat(N), IL, M, N)) -->_1 U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) :85 -->_1 U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) :84 44: active^#(U93(X1, X2, X3, X4)) -> c_44(U93^#(active(X1), X2, X3, X4)) -->_1 U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) :85 -->_1 U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) :84 45: active^#(U93(tt(), IL, M, N)) -> c_45(cons^#(N, take(M, IL))) -->_1 cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) :51 -->_1 cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) :50 46: active^#(take(X1, X2)) -> c_46(take^#(X1, active(X2))) -->_1 take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) :88 -->_1 take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) :87 -->_1 take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) :86 47: active^#(take(X1, X2)) -> c_47(take^#(active(X1), X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) :88 -->_1 take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) :87 -->_1 take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) :86 48: active^#(take(0(), IL)) -> c_48(U81^#(isNatIList(IL))) -->_1 U81^#(ok(X)) -> c_82(U81^#(X)) :79 -->_1 U81^#(mark(X)) -> c_81(U81^#(X)) :78 49: active^#(take(s(M), cons(N, IL))) -> c_49(U91^#(isNatIList(IL), IL, M, N)) -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) :81 -->_1 U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) :80 50: cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) :51 -->_1 cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) :50 51: cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) :51 -->_1 cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) :50 52: U11^#(mark(X)) -> c_52(U11^#(X)) -->_1 U11^#(ok(X)) -> c_53(U11^#(X)) :53 -->_1 U11^#(mark(X)) -> c_52(U11^#(X)) :52 53: U11^#(ok(X)) -> c_53(U11^#(X)) -->_1 U11^#(ok(X)) -> c_53(U11^#(X)) :53 -->_1 U11^#(mark(X)) -> c_52(U11^#(X)) :52 54: U21^#(mark(X)) -> c_54(U21^#(X)) -->_1 U21^#(ok(X)) -> c_55(U21^#(X)) :55 -->_1 U21^#(mark(X)) -> c_54(U21^#(X)) :54 55: U21^#(ok(X)) -> c_55(U21^#(X)) -->_1 U21^#(ok(X)) -> c_55(U21^#(X)) :55 -->_1 U21^#(mark(X)) -> c_54(U21^#(X)) :54 56: U31^#(mark(X)) -> c_56(U31^#(X)) -->_1 U31^#(ok(X)) -> c_57(U31^#(X)) :57 -->_1 U31^#(mark(X)) -> c_56(U31^#(X)) :56 57: U31^#(ok(X)) -> c_57(U31^#(X)) -->_1 U31^#(ok(X)) -> c_57(U31^#(X)) :57 -->_1 U31^#(mark(X)) -> c_56(U31^#(X)) :56 58: U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) :59 -->_1 U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) :58 59: U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) :59 -->_1 U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) :58 60: U42^#(mark(X)) -> c_60(U42^#(X)) -->_1 U42^#(ok(X)) -> c_61(U42^#(X)) :61 -->_1 U42^#(mark(X)) -> c_60(U42^#(X)) :60 61: U42^#(ok(X)) -> c_61(U42^#(X)) -->_1 U42^#(ok(X)) -> c_61(U42^#(X)) :61 -->_1 U42^#(mark(X)) -> c_60(U42^#(X)) :60 62: U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) -->_1 U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) :63 -->_1 U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) :62 63: U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) -->_1 U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) :63 -->_1 U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) :62 64: U52^#(mark(X)) -> c_65(U52^#(X)) -->_1 U52^#(ok(X)) -> c_66(U52^#(X)) :65 -->_1 U52^#(mark(X)) -> c_65(U52^#(X)) :64 65: U52^#(ok(X)) -> c_66(U52^#(X)) -->_1 U52^#(ok(X)) -> c_66(U52^#(X)) :65 -->_1 U52^#(mark(X)) -> c_65(U52^#(X)) :64 66: U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) :67 -->_1 U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) :66 67: U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) :67 -->_1 U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) :66 68: U62^#(mark(X)) -> c_70(U62^#(X)) -->_1 U62^#(ok(X)) -> c_71(U62^#(X)) :69 -->_1 U62^#(mark(X)) -> c_70(U62^#(X)) :68 69: U62^#(ok(X)) -> c_71(U62^#(X)) -->_1 U62^#(ok(X)) -> c_71(U62^#(X)) :69 -->_1 U62^#(mark(X)) -> c_70(U62^#(X)) :68 70: U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :71 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :70 71: U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :71 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :70 72: U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) -->_1 U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) :73 -->_1 U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) :72 73: U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) -->_1 U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) :73 -->_1 U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) :72 74: s^#(mark(X)) -> c_77(s^#(X)) -->_1 s^#(ok(X)) -> c_78(s^#(X)) :75 -->_1 s^#(mark(X)) -> c_77(s^#(X)) :74 75: s^#(ok(X)) -> c_78(s^#(X)) -->_1 s^#(ok(X)) -> c_78(s^#(X)) :75 -->_1 s^#(mark(X)) -> c_77(s^#(X)) :74 76: length^#(mark(X)) -> c_79(length^#(X)) -->_1 length^#(ok(X)) -> c_80(length^#(X)) :77 -->_1 length^#(mark(X)) -> c_79(length^#(X)) :76 77: length^#(ok(X)) -> c_80(length^#(X)) -->_1 length^#(ok(X)) -> c_80(length^#(X)) :77 -->_1 length^#(mark(X)) -> c_79(length^#(X)) :76 78: U81^#(mark(X)) -> c_81(U81^#(X)) -->_1 U81^#(ok(X)) -> c_82(U81^#(X)) :79 -->_1 U81^#(mark(X)) -> c_81(U81^#(X)) :78 79: U81^#(ok(X)) -> c_82(U81^#(X)) -->_1 U81^#(ok(X)) -> c_82(U81^#(X)) :79 -->_1 U81^#(mark(X)) -> c_81(U81^#(X)) :78 80: U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) :81 -->_1 U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) :80 81: U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) :81 -->_1 U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) :80 82: U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) -->_1 U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) :83 -->_1 U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) :82 83: U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) -->_1 U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) :83 -->_1 U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) :82 84: U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) -->_1 U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) :85 -->_1 U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) :84 85: U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) -->_1 U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) :85 -->_1 U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) :84 86: take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) :88 -->_1 take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) :87 -->_1 take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) :86 87: take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) :88 -->_1 take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) :87 -->_1 take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) :86 88: take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) :88 -->_1 take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) :87 -->_1 take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) :86 89: isNatIList^#(ok(X)) -> c_62(isNatIList^#(X)) -->_1 isNatIList^#(ok(X)) -> c_62(isNatIList^#(X)) :89 90: isNatList^#(ok(X)) -> c_67(isNatList^#(X)) -->_1 isNatList^#(ok(X)) -> c_67(isNatList^#(X)) :90 91: isNat^#(ok(X)) -> c_76(isNat^#(X)) -->_1 isNat^#(ok(X)) -> c_76(isNat^#(X)) :91 92: proper^#(zeros()) -> c_92() 93: proper^#(cons(X1, X2)) -> c_93(cons^#(proper(X1), proper(X2))) -->_1 cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) :51 -->_1 cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) :50 94: proper^#(0()) -> c_94() 95: proper^#(U11(X)) -> c_95(U11^#(proper(X))) -->_1 U11^#(ok(X)) -> c_53(U11^#(X)) :53 -->_1 U11^#(mark(X)) -> c_52(U11^#(X)) :52 96: proper^#(tt()) -> c_96() 97: proper^#(U21(X)) -> c_97(U21^#(proper(X))) -->_1 U21^#(ok(X)) -> c_55(U21^#(X)) :55 -->_1 U21^#(mark(X)) -> c_54(U21^#(X)) :54 98: proper^#(U31(X)) -> c_98(U31^#(proper(X))) -->_1 U31^#(ok(X)) -> c_57(U31^#(X)) :57 -->_1 U31^#(mark(X)) -> c_56(U31^#(X)) :56 99: proper^#(U41(X1, X2)) -> c_99(U41^#(proper(X1), proper(X2))) -->_1 U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) :59 -->_1 U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) :58 100: proper^#(U42(X)) -> c_100(U42^#(proper(X))) -->_1 U42^#(ok(X)) -> c_61(U42^#(X)) :61 -->_1 U42^#(mark(X)) -> c_60(U42^#(X)) :60 101: proper^#(isNatIList(X)) -> c_101(isNatIList^#(proper(X))) -->_1 isNatIList^#(ok(X)) -> c_62(isNatIList^#(X)) :89 102: proper^#(U51(X1, X2)) -> c_102(U51^#(proper(X1), proper(X2))) -->_1 U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) :63 -->_1 U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) :62 103: proper^#(U52(X)) -> c_103(U52^#(proper(X))) -->_1 U52^#(ok(X)) -> c_66(U52^#(X)) :65 -->_1 U52^#(mark(X)) -> c_65(U52^#(X)) :64 104: proper^#(isNatList(X)) -> c_104(isNatList^#(proper(X))) -->_1 isNatList^#(ok(X)) -> c_67(isNatList^#(X)) :90 105: proper^#(U61(X1, X2)) -> c_105(U61^#(proper(X1), proper(X2))) -->_1 U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) :67 -->_1 U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) :66 106: proper^#(U62(X)) -> c_106(U62^#(proper(X))) -->_1 U62^#(ok(X)) -> c_71(U62^#(X)) :69 -->_1 U62^#(mark(X)) -> c_70(U62^#(X)) :68 107: proper^#(U71(X1, X2, X3)) -> c_107(U71^#(proper(X1), proper(X2), proper(X3))) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :71 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :70 108: proper^#(U72(X1, X2)) -> c_108(U72^#(proper(X1), proper(X2))) -->_1 U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) :73 -->_1 U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) :72 109: proper^#(isNat(X)) -> c_109(isNat^#(proper(X))) -->_1 isNat^#(ok(X)) -> c_76(isNat^#(X)) :91 110: proper^#(s(X)) -> c_110(s^#(proper(X))) -->_1 s^#(ok(X)) -> c_78(s^#(X)) :75 -->_1 s^#(mark(X)) -> c_77(s^#(X)) :74 111: proper^#(length(X)) -> c_111(length^#(proper(X))) -->_1 length^#(ok(X)) -> c_80(length^#(X)) :77 -->_1 length^#(mark(X)) -> c_79(length^#(X)) :76 112: proper^#(U81(X)) -> c_112(U81^#(proper(X))) -->_1 U81^#(ok(X)) -> c_82(U81^#(X)) :79 -->_1 U81^#(mark(X)) -> c_81(U81^#(X)) :78 113: proper^#(nil()) -> c_113() 114: proper^#(U91(X1, X2, X3, X4)) -> c_114(U91^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) :81 -->_1 U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) :80 115: proper^#(U92(X1, X2, X3, X4)) -> c_115(U92^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) :83 -->_1 U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) :82 116: proper^#(U93(X1, X2, X3, X4)) -> c_116(U93^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) :85 -->_1 U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) :84 117: proper^#(take(X1, X2)) -> c_117(take^#(proper(X1), proper(X2))) -->_1 take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) :88 -->_1 take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) :87 -->_1 take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) :86 118: top^#(mark(X)) -> c_118(top^#(proper(X))) -->_1 top^#(ok(X)) -> c_119(top^#(active(X))) :119 -->_1 top^#(mark(X)) -> c_118(top^#(proper(X))) :118 119: top^#(ok(X)) -> c_119(top^#(active(X))) -->_1 top^#(ok(X)) -> c_119(top^#(active(X))) :119 -->_1 top^#(mark(X)) -> c_118(top^#(proper(X))) :118 Only the nodes {1,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,88,87,89,90,91,92,94,96,113,118,119} are reachable from nodes {1,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,94,96,113,118,119} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(zeros()) -> c_1(cons^#(0(), zeros())) , cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) , U11^#(mark(X)) -> c_52(U11^#(X)) , U11^#(ok(X)) -> c_53(U11^#(X)) , U21^#(mark(X)) -> c_54(U21^#(X)) , U21^#(ok(X)) -> c_55(U21^#(X)) , U31^#(mark(X)) -> c_56(U31^#(X)) , U31^#(ok(X)) -> c_57(U31^#(X)) , U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) , U42^#(mark(X)) -> c_60(U42^#(X)) , U42^#(ok(X)) -> c_61(U42^#(X)) , U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) , U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) , U52^#(mark(X)) -> c_65(U52^#(X)) , U52^#(ok(X)) -> c_66(U52^#(X)) , U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) , U62^#(mark(X)) -> c_70(U62^#(X)) , U62^#(ok(X)) -> c_71(U62^#(X)) , U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) , U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) , s^#(mark(X)) -> c_77(s^#(X)) , s^#(ok(X)) -> c_78(s^#(X)) , length^#(mark(X)) -> c_79(length^#(X)) , length^#(ok(X)) -> c_80(length^#(X)) , U81^#(mark(X)) -> c_81(U81^#(X)) , U81^#(ok(X)) -> c_82(U81^#(X)) , U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) , U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) , U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) , U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) , U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) , U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) , take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) , isNatIList^#(ok(X)) -> c_62(isNatIList^#(X)) , isNatList^#(ok(X)) -> c_67(isNatList^#(X)) , isNat^#(ok(X)) -> c_76(isNat^#(X)) , proper^#(zeros()) -> c_92() , proper^#(0()) -> c_94() , proper^#(tt()) -> c_96() , proper^#(nil()) -> c_113() , top^#(mark(X)) -> c_118(top^#(proper(X))) , top^#(ok(X)) -> c_119(top^#(active(X))) } Strict Trs: { active(zeros()) -> mark(cons(0(), zeros())) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(U11(X)) -> U11(active(X)) , active(U11(tt())) -> mark(tt()) , active(U21(X)) -> U21(active(X)) , active(U21(tt())) -> mark(tt()) , active(U31(X)) -> U31(active(X)) , active(U31(tt())) -> mark(tt()) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), V2)) -> mark(U42(isNatIList(V2))) , active(U42(X)) -> U42(active(X)) , active(U42(tt())) -> mark(tt()) , active(isNatIList(V)) -> mark(U31(isNatList(V))) , active(isNatIList(zeros())) -> mark(tt()) , active(isNatIList(cons(V1, V2))) -> mark(U41(isNat(V1), V2)) , active(U51(X1, X2)) -> U51(active(X1), X2) , active(U51(tt(), V2)) -> mark(U52(isNatList(V2))) , active(U52(X)) -> U52(active(X)) , active(U52(tt())) -> mark(tt()) , active(isNatList(cons(V1, V2))) -> mark(U51(isNat(V1), V2)) , active(isNatList(nil())) -> mark(tt()) , active(isNatList(take(V1, V2))) -> mark(U61(isNat(V1), V2)) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V2)) -> mark(U62(isNatIList(V2))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), L, N)) -> mark(U72(isNat(N), L)) , active(U72(X1, X2)) -> U72(active(X1), X2) , active(U72(tt(), L)) -> mark(s(length(L))) , active(isNat(0())) -> mark(tt()) , active(isNat(s(V1))) -> mark(U21(isNat(V1))) , active(isNat(length(V1))) -> mark(U11(isNatList(V1))) , active(s(X)) -> s(active(X)) , active(length(X)) -> length(active(X)) , active(length(cons(N, L))) -> mark(U71(isNatList(L), L, N)) , active(length(nil())) -> mark(0()) , active(U81(X)) -> U81(active(X)) , active(U81(tt())) -> mark(nil()) , active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4) , active(U91(tt(), IL, M, N)) -> mark(U92(isNat(M), IL, M, N)) , active(U92(X1, X2, X3, X4)) -> U92(active(X1), X2, X3, X4) , active(U92(tt(), IL, M, N)) -> mark(U93(isNat(N), IL, M, N)) , active(U93(X1, X2, X3, X4)) -> U93(active(X1), X2, X3, X4) , active(U93(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(take(0(), IL)) -> mark(U81(isNatIList(IL))) , active(take(s(M), cons(N, IL))) -> mark(U91(isNatIList(IL), IL, M, N)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , U11(mark(X)) -> mark(U11(X)) , U11(ok(X)) -> ok(U11(X)) , U21(mark(X)) -> mark(U21(X)) , U21(ok(X)) -> ok(U21(X)) , U31(mark(X)) -> mark(U31(X)) , U31(ok(X)) -> ok(U31(X)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , U42(mark(X)) -> mark(U42(X)) , U42(ok(X)) -> ok(U42(X)) , isNatIList(ok(X)) -> ok(isNatIList(X)) , U51(mark(X1), X2) -> mark(U51(X1, X2)) , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) , U52(mark(X)) -> mark(U52(X)) , U52(ok(X)) -> ok(U52(X)) , isNatList(ok(X)) -> ok(isNatList(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , U72(mark(X1), X2) -> mark(U72(X1, X2)) , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , length(mark(X)) -> mark(length(X)) , length(ok(X)) -> ok(length(X)) , U81(mark(X)) -> mark(U81(X)) , U81(ok(X)) -> ok(U81(X)) , U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)) , U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)) , U92(mark(X1), X2, X3, X4) -> mark(U92(X1, X2, X3, X4)) , U92(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U92(X1, X2, X3, X4)) , U93(mark(X1), X2, X3, X4) -> mark(U93(X1, X2, X3, X4)) , U93(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U93(X1, X2, X3, X4)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , proper(zeros()) -> ok(zeros()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(U11(X)) -> U11(proper(X)) , proper(tt()) -> ok(tt()) , proper(U21(X)) -> U21(proper(X)) , proper(U31(X)) -> U31(proper(X)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(U42(X)) -> U42(proper(X)) , proper(isNatIList(X)) -> isNatIList(proper(X)) , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) , proper(U52(X)) -> U52(proper(X)) , proper(isNatList(X)) -> isNatList(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(length(X)) -> length(proper(X)) , proper(U81(X)) -> U81(proper(X)) , proper(nil()) -> ok(nil()) , proper(U91(X1, X2, X3, X4)) -> U91(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U92(X1, X2, X3, X4)) -> U92(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U93(X1, X2, X3, X4)) -> U93(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,44,45,46,47} by applications of Pre({1,44,45,46,47}) = {}. Here rules are labeled as follows: DPs: { 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) , 2: cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) , 3: cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) , 4: U11^#(mark(X)) -> c_52(U11^#(X)) , 5: U11^#(ok(X)) -> c_53(U11^#(X)) , 6: U21^#(mark(X)) -> c_54(U21^#(X)) , 7: U21^#(ok(X)) -> c_55(U21^#(X)) , 8: U31^#(mark(X)) -> c_56(U31^#(X)) , 9: U31^#(ok(X)) -> c_57(U31^#(X)) , 10: U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) , 11: U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) , 12: U42^#(mark(X)) -> c_60(U42^#(X)) , 13: U42^#(ok(X)) -> c_61(U42^#(X)) , 14: U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) , 15: U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) , 16: U52^#(mark(X)) -> c_65(U52^#(X)) , 17: U52^#(ok(X)) -> c_66(U52^#(X)) , 18: U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) , 19: U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) , 20: U62^#(mark(X)) -> c_70(U62^#(X)) , 21: U62^#(ok(X)) -> c_71(U62^#(X)) , 22: U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , 23: U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , 24: U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) , 25: U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) , 26: s^#(mark(X)) -> c_77(s^#(X)) , 27: s^#(ok(X)) -> c_78(s^#(X)) , 28: length^#(mark(X)) -> c_79(length^#(X)) , 29: length^#(ok(X)) -> c_80(length^#(X)) , 30: U81^#(mark(X)) -> c_81(U81^#(X)) , 31: U81^#(ok(X)) -> c_82(U81^#(X)) , 32: U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) , 33: U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) , 34: U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) , 35: U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) , 36: U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) , 37: U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) , 38: take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) , 39: take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) , 40: take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) , 41: isNatIList^#(ok(X)) -> c_62(isNatIList^#(X)) , 42: isNatList^#(ok(X)) -> c_67(isNatList^#(X)) , 43: isNat^#(ok(X)) -> c_76(isNat^#(X)) , 44: proper^#(zeros()) -> c_92() , 45: proper^#(0()) -> c_94() , 46: proper^#(tt()) -> c_96() , 47: proper^#(nil()) -> c_113() , 48: top^#(mark(X)) -> c_118(top^#(proper(X))) , 49: top^#(ok(X)) -> c_119(top^#(active(X))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { cons^#(mark(X1), X2) -> c_50(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_51(cons^#(X1, X2)) , U11^#(mark(X)) -> c_52(U11^#(X)) , U11^#(ok(X)) -> c_53(U11^#(X)) , U21^#(mark(X)) -> c_54(U21^#(X)) , U21^#(ok(X)) -> c_55(U21^#(X)) , U31^#(mark(X)) -> c_56(U31^#(X)) , U31^#(ok(X)) -> c_57(U31^#(X)) , U41^#(mark(X1), X2) -> c_58(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_59(U41^#(X1, X2)) , U42^#(mark(X)) -> c_60(U42^#(X)) , U42^#(ok(X)) -> c_61(U42^#(X)) , U51^#(mark(X1), X2) -> c_63(U51^#(X1, X2)) , U51^#(ok(X1), ok(X2)) -> c_64(U51^#(X1, X2)) , U52^#(mark(X)) -> c_65(U52^#(X)) , U52^#(ok(X)) -> c_66(U52^#(X)) , U61^#(mark(X1), X2) -> c_68(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_69(U61^#(X1, X2)) , U62^#(mark(X)) -> c_70(U62^#(X)) , U62^#(ok(X)) -> c_71(U62^#(X)) , U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , U72^#(mark(X1), X2) -> c_74(U72^#(X1, X2)) , U72^#(ok(X1), ok(X2)) -> c_75(U72^#(X1, X2)) , s^#(mark(X)) -> c_77(s^#(X)) , s^#(ok(X)) -> c_78(s^#(X)) , length^#(mark(X)) -> c_79(length^#(X)) , length^#(ok(X)) -> c_80(length^#(X)) , U81^#(mark(X)) -> c_81(U81^#(X)) , U81^#(ok(X)) -> c_82(U81^#(X)) , U91^#(mark(X1), X2, X3, X4) -> c_83(U91^#(X1, X2, X3, X4)) , U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_84(U91^#(X1, X2, X3, X4)) , U92^#(mark(X1), X2, X3, X4) -> c_85(U92^#(X1, X2, X3, X4)) , U92^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_86(U92^#(X1, X2, X3, X4)) , U93^#(mark(X1), X2, X3, X4) -> c_87(U93^#(X1, X2, X3, X4)) , U93^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_88(U93^#(X1, X2, X3, X4)) , take^#(X1, mark(X2)) -> c_89(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_90(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_91(take^#(X1, X2)) , isNatIList^#(ok(X)) -> c_62(isNatIList^#(X)) , isNatList^#(ok(X)) -> c_67(isNatList^#(X)) , isNat^#(ok(X)) -> c_76(isNat^#(X)) , top^#(mark(X)) -> c_118(top^#(proper(X))) , top^#(ok(X)) -> c_119(top^#(active(X))) } Strict Trs: { active(zeros()) -> mark(cons(0(), zeros())) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(U11(X)) -> U11(active(X)) , active(U11(tt())) -> mark(tt()) , active(U21(X)) -> U21(active(X)) , active(U21(tt())) -> mark(tt()) , active(U31(X)) -> U31(active(X)) , active(U31(tt())) -> mark(tt()) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), V2)) -> mark(U42(isNatIList(V2))) , active(U42(X)) -> U42(active(X)) , active(U42(tt())) -> mark(tt()) , active(isNatIList(V)) -> mark(U31(isNatList(V))) , active(isNatIList(zeros())) -> mark(tt()) , active(isNatIList(cons(V1, V2))) -> mark(U41(isNat(V1), V2)) , active(U51(X1, X2)) -> U51(active(X1), X2) , active(U51(tt(), V2)) -> mark(U52(isNatList(V2))) , active(U52(X)) -> U52(active(X)) , active(U52(tt())) -> mark(tt()) , active(isNatList(cons(V1, V2))) -> mark(U51(isNat(V1), V2)) , active(isNatList(nil())) -> mark(tt()) , active(isNatList(take(V1, V2))) -> mark(U61(isNat(V1), V2)) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V2)) -> mark(U62(isNatIList(V2))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), L, N)) -> mark(U72(isNat(N), L)) , active(U72(X1, X2)) -> U72(active(X1), X2) , active(U72(tt(), L)) -> mark(s(length(L))) , active(isNat(0())) -> mark(tt()) , active(isNat(s(V1))) -> mark(U21(isNat(V1))) , active(isNat(length(V1))) -> mark(U11(isNatList(V1))) , active(s(X)) -> s(active(X)) , active(length(X)) -> length(active(X)) , active(length(cons(N, L))) -> mark(U71(isNatList(L), L, N)) , active(length(nil())) -> mark(0()) , active(U81(X)) -> U81(active(X)) , active(U81(tt())) -> mark(nil()) , active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4) , active(U91(tt(), IL, M, N)) -> mark(U92(isNat(M), IL, M, N)) , active(U92(X1, X2, X3, X4)) -> U92(active(X1), X2, X3, X4) , active(U92(tt(), IL, M, N)) -> mark(U93(isNat(N), IL, M, N)) , active(U93(X1, X2, X3, X4)) -> U93(active(X1), X2, X3, X4) , active(U93(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(take(0(), IL)) -> mark(U81(isNatIList(IL))) , active(take(s(M), cons(N, IL))) -> mark(U91(isNatIList(IL), IL, M, N)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , U11(mark(X)) -> mark(U11(X)) , U11(ok(X)) -> ok(U11(X)) , U21(mark(X)) -> mark(U21(X)) , U21(ok(X)) -> ok(U21(X)) , U31(mark(X)) -> mark(U31(X)) , U31(ok(X)) -> ok(U31(X)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , U42(mark(X)) -> mark(U42(X)) , U42(ok(X)) -> ok(U42(X)) , isNatIList(ok(X)) -> ok(isNatIList(X)) , U51(mark(X1), X2) -> mark(U51(X1, X2)) , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) , U52(mark(X)) -> mark(U52(X)) , U52(ok(X)) -> ok(U52(X)) , isNatList(ok(X)) -> ok(isNatList(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , U72(mark(X1), X2) -> mark(U72(X1, X2)) , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , length(mark(X)) -> mark(length(X)) , length(ok(X)) -> ok(length(X)) , U81(mark(X)) -> mark(U81(X)) , U81(ok(X)) -> ok(U81(X)) , U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)) , U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)) , U92(mark(X1), X2, X3, X4) -> mark(U92(X1, X2, X3, X4)) , U92(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U92(X1, X2, X3, X4)) , U93(mark(X1), X2, X3, X4) -> mark(U93(X1, X2, X3, X4)) , U93(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U93(X1, X2, X3, X4)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , proper(zeros()) -> ok(zeros()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(U11(X)) -> U11(proper(X)) , proper(tt()) -> ok(tt()) , proper(U21(X)) -> U21(proper(X)) , proper(U31(X)) -> U31(proper(X)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(U42(X)) -> U42(proper(X)) , proper(isNatIList(X)) -> isNatIList(proper(X)) , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) , proper(U52(X)) -> U52(proper(X)) , proper(isNatList(X)) -> isNatList(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(length(X)) -> length(proper(X)) , proper(U81(X)) -> U81(proper(X)) , proper(nil()) -> ok(nil()) , proper(U91(X1, X2, X3, X4)) -> U91(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U92(X1, X2, X3, X4)) -> U92(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U93(X1, X2, X3, X4)) -> U93(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Weak DPs: { active^#(zeros()) -> c_1(cons^#(0(), zeros())) , proper^#(zeros()) -> c_92() , proper^#(0()) -> c_94() , proper^#(tt()) -> c_96() , proper^#(nil()) -> c_113() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..