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