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