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