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