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