MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { 0(#()) -> #() , +(x, #()) -> x , +(0(x), 0(y)) -> 0(+(x, y)) , +(0(x), 1(y)) -> 1(+(x, y)) , +(#(), x) -> x , +(+(x, y), z) -> +(x, +(y, z)) , +(1(x), 0(y)) -> 1(+(x, y)) , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) , -(x, #()) -> x , -(0(x), 0(y)) -> 0(-(x, y)) , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) , -(#(), x) -> #() , -(1(x), 0(y)) -> 1(-(x, y)) , -(1(x), 1(y)) -> 0(-(x, y)) , not(true()) -> false() , not(false()) -> true() , if(true(), x, y) -> x , if(false(), x, y) -> y , eq(0(x), 0(y)) -> eq(x, y) , eq(0(x), #()) -> eq(x, #()) , eq(0(x), 1(y)) -> false() , eq(#(), 0(y)) -> eq(#(), y) , eq(#(), #()) -> true() , eq(#(), 1(y)) -> false() , eq(1(x), 0(y)) -> false() , eq(1(x), #()) -> false() , eq(1(x), 1(y)) -> eq(x, y) , ge(x, #()) -> true() , ge(0(x), 0(y)) -> ge(x, y) , ge(0(x), 1(y)) -> not(ge(y, x)) , ge(#(), 0(x)) -> ge(#(), x) , ge(#(), 1(x)) -> false() , ge(1(x), 0(y)) -> ge(x, y) , ge(1(x), 1(y)) -> ge(x, y) , log(x) -> -(log'(x), 1(#())) , log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()) , log'(#()) -> #() , log'(1(x)) -> +(log'(x), 1(#())) , *(x, +(y, z)) -> +(*(x, y), *(x, z)) , *(0(x), y) -> 0(*(x, y)) , *(#(), x) -> #() , *(1(x), y) -> +(0(*(x, y)), y) , *(*(x, y), z) -> *(x, *(y, z)) , app(nil(), l) -> l , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) , sum(app(l1, l2)) -> +(sum(l1), sum(l2)) , sum(nil()) -> 0(#()) , sum(cons(x, l)) -> +(x, sum(l)) , prod(app(l1, l2)) -> *(prod(l1), prod(l2)) , prod(nil()) -> 1(#()) , prod(cons(x, l)) -> *(x, prod(l)) , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)) , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) , inter(x, nil()) -> nil() , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) , inter(nil(), x) -> nil() , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) , ifinter(false(), x, l1, l2) -> inter(l1, l2) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { 0^#(#()) -> c_1() , +^#(x, #()) -> c_2(x) , +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) , +^#(0(x), 1(y)) -> c_4(+^#(x, y)) , +^#(#(), x) -> c_5(x) , +^#(+(x, y), z) -> c_6(+^#(x, +(y, z))) , +^#(1(x), 0(y)) -> c_7(+^#(x, y)) , +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) , -^#(x, #()) -> c_9(x) , -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) , -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) , -^#(#(), x) -> c_12() , -^#(1(x), 0(y)) -> c_13(-^#(x, y)) , -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) , not^#(true()) -> c_15() , not^#(false()) -> c_16() , if^#(true(), x, y) -> c_17(x) , if^#(false(), x, y) -> c_18(y) , eq^#(0(x), 0(y)) -> c_19(eq^#(x, y)) , eq^#(0(x), #()) -> c_20(eq^#(x, #())) , eq^#(0(x), 1(y)) -> c_21() , eq^#(#(), 0(y)) -> c_22(eq^#(#(), y)) , eq^#(#(), #()) -> c_23() , eq^#(#(), 1(y)) -> c_24() , eq^#(1(x), 0(y)) -> c_25() , eq^#(1(x), #()) -> c_26() , eq^#(1(x), 1(y)) -> c_27(eq^#(x, y)) , ge^#(x, #()) -> c_28() , ge^#(0(x), 0(y)) -> c_29(ge^#(x, y)) , ge^#(0(x), 1(y)) -> c_30(not^#(ge(y, x))) , ge^#(#(), 0(x)) -> c_31(ge^#(#(), x)) , ge^#(#(), 1(x)) -> c_32() , ge^#(1(x), 0(y)) -> c_33(ge^#(x, y)) , ge^#(1(x), 1(y)) -> c_34(ge^#(x, y)) , log^#(x) -> c_35(-^#(log'(x), 1(#()))) , log'^#(0(x)) -> c_36(if^#(ge(x, 1(#())), +(log'(x), 1(#())), #())) , log'^#(#()) -> c_37() , log'^#(1(x)) -> c_38(+^#(log'(x), 1(#()))) , *^#(x, +(y, z)) -> c_39(+^#(*(x, y), *(x, z))) , *^#(0(x), y) -> c_40(0^#(*(x, y))) , *^#(#(), x) -> c_41() , *^#(1(x), y) -> c_42(+^#(0(*(x, y)), y)) , *^#(*(x, y), z) -> c_43(*^#(x, *(y, z))) , app^#(nil(), l) -> c_44(l) , app^#(cons(x, l1), l2) -> c_45(x, app^#(l1, l2)) , sum^#(app(l1, l2)) -> c_46(+^#(sum(l1), sum(l2))) , sum^#(nil()) -> c_47(0^#(#())) , sum^#(cons(x, l)) -> c_48(+^#(x, sum(l))) , prod^#(app(l1, l2)) -> c_49(*^#(prod(l1), prod(l2))) , prod^#(nil()) -> c_50() , prod^#(cons(x, l)) -> c_51(*^#(x, prod(l))) , mem^#(x, nil()) -> c_52() , mem^#(x, cons(y, l)) -> c_53(if^#(eq(x, y), true(), mem(x, l))) , inter^#(l1, app(l2, l3)) -> c_54(app^#(inter(l1, l2), inter(l1, l3))) , inter^#(x, nil()) -> c_55() , inter^#(l1, cons(x, l2)) -> c_56(ifinter^#(mem(x, l1), x, l2, l1)) , inter^#(app(l1, l2), l3) -> c_57(app^#(inter(l1, l3), inter(l2, l3))) , inter^#(nil(), x) -> c_58() , inter^#(cons(x, l1), l2) -> c_59(ifinter^#(mem(x, l2), x, l1, l2)) , ifinter^#(true(), x, l1, l2) -> c_60(x, inter^#(l1, l2)) , ifinter^#(false(), x, l1, l2) -> c_61(inter^#(l1, l2)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { 0^#(#()) -> c_1() , +^#(x, #()) -> c_2(x) , +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) , +^#(0(x), 1(y)) -> c_4(+^#(x, y)) , +^#(#(), x) -> c_5(x) , +^#(+(x, y), z) -> c_6(+^#(x, +(y, z))) , +^#(1(x), 0(y)) -> c_7(+^#(x, y)) , +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) , -^#(x, #()) -> c_9(x) , -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) , -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) , -^#(#(), x) -> c_12() , -^#(1(x), 0(y)) -> c_13(-^#(x, y)) , -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) , not^#(true()) -> c_15() , not^#(false()) -> c_16() , if^#(true(), x, y) -> c_17(x) , if^#(false(), x, y) -> c_18(y) , eq^#(0(x), 0(y)) -> c_19(eq^#(x, y)) , eq^#(0(x), #()) -> c_20(eq^#(x, #())) , eq^#(0(x), 1(y)) -> c_21() , eq^#(#(), 0(y)) -> c_22(eq^#(#(), y)) , eq^#(#(), #()) -> c_23() , eq^#(#(), 1(y)) -> c_24() , eq^#(1(x), 0(y)) -> c_25() , eq^#(1(x), #()) -> c_26() , eq^#(1(x), 1(y)) -> c_27(eq^#(x, y)) , ge^#(x, #()) -> c_28() , ge^#(0(x), 0(y)) -> c_29(ge^#(x, y)) , ge^#(0(x), 1(y)) -> c_30(not^#(ge(y, x))) , ge^#(#(), 0(x)) -> c_31(ge^#(#(), x)) , ge^#(#(), 1(x)) -> c_32() , ge^#(1(x), 0(y)) -> c_33(ge^#(x, y)) , ge^#(1(x), 1(y)) -> c_34(ge^#(x, y)) , log^#(x) -> c_35(-^#(log'(x), 1(#()))) , log'^#(0(x)) -> c_36(if^#(ge(x, 1(#())), +(log'(x), 1(#())), #())) , log'^#(#()) -> c_37() , log'^#(1(x)) -> c_38(+^#(log'(x), 1(#()))) , *^#(x, +(y, z)) -> c_39(+^#(*(x, y), *(x, z))) , *^#(0(x), y) -> c_40(0^#(*(x, y))) , *^#(#(), x) -> c_41() , *^#(1(x), y) -> c_42(+^#(0(*(x, y)), y)) , *^#(*(x, y), z) -> c_43(*^#(x, *(y, z))) , app^#(nil(), l) -> c_44(l) , app^#(cons(x, l1), l2) -> c_45(x, app^#(l1, l2)) , sum^#(app(l1, l2)) -> c_46(+^#(sum(l1), sum(l2))) , sum^#(nil()) -> c_47(0^#(#())) , sum^#(cons(x, l)) -> c_48(+^#(x, sum(l))) , prod^#(app(l1, l2)) -> c_49(*^#(prod(l1), prod(l2))) , prod^#(nil()) -> c_50() , prod^#(cons(x, l)) -> c_51(*^#(x, prod(l))) , mem^#(x, nil()) -> c_52() , mem^#(x, cons(y, l)) -> c_53(if^#(eq(x, y), true(), mem(x, l))) , inter^#(l1, app(l2, l3)) -> c_54(app^#(inter(l1, l2), inter(l1, l3))) , inter^#(x, nil()) -> c_55() , inter^#(l1, cons(x, l2)) -> c_56(ifinter^#(mem(x, l1), x, l2, l1)) , inter^#(app(l1, l2), l3) -> c_57(app^#(inter(l1, l3), inter(l2, l3))) , inter^#(nil(), x) -> c_58() , inter^#(cons(x, l1), l2) -> c_59(ifinter^#(mem(x, l2), x, l1, l2)) , ifinter^#(true(), x, l1, l2) -> c_60(x, inter^#(l1, l2)) , ifinter^#(false(), x, l1, l2) -> c_61(inter^#(l1, l2)) } Strict Trs: { 0(#()) -> #() , +(x, #()) -> x , +(0(x), 0(y)) -> 0(+(x, y)) , +(0(x), 1(y)) -> 1(+(x, y)) , +(#(), x) -> x , +(+(x, y), z) -> +(x, +(y, z)) , +(1(x), 0(y)) -> 1(+(x, y)) , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) , -(x, #()) -> x , -(0(x), 0(y)) -> 0(-(x, y)) , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) , -(#(), x) -> #() , -(1(x), 0(y)) -> 1(-(x, y)) , -(1(x), 1(y)) -> 0(-(x, y)) , not(true()) -> false() , not(false()) -> true() , if(true(), x, y) -> x , if(false(), x, y) -> y , eq(0(x), 0(y)) -> eq(x, y) , eq(0(x), #()) -> eq(x, #()) , eq(0(x), 1(y)) -> false() , eq(#(), 0(y)) -> eq(#(), y) , eq(#(), #()) -> true() , eq(#(), 1(y)) -> false() , eq(1(x), 0(y)) -> false() , eq(1(x), #()) -> false() , eq(1(x), 1(y)) -> eq(x, y) , ge(x, #()) -> true() , ge(0(x), 0(y)) -> ge(x, y) , ge(0(x), 1(y)) -> not(ge(y, x)) , ge(#(), 0(x)) -> ge(#(), x) , ge(#(), 1(x)) -> false() , ge(1(x), 0(y)) -> ge(x, y) , ge(1(x), 1(y)) -> ge(x, y) , log(x) -> -(log'(x), 1(#())) , log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()) , log'(#()) -> #() , log'(1(x)) -> +(log'(x), 1(#())) , *(x, +(y, z)) -> +(*(x, y), *(x, z)) , *(0(x), y) -> 0(*(x, y)) , *(#(), x) -> #() , *(1(x), y) -> +(0(*(x, y)), y) , *(*(x, y), z) -> *(x, *(y, z)) , app(nil(), l) -> l , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) , sum(app(l1, l2)) -> +(sum(l1), sum(l2)) , sum(nil()) -> 0(#()) , sum(cons(x, l)) -> +(x, sum(l)) , prod(app(l1, l2)) -> *(prod(l1), prod(l2)) , prod(nil()) -> 1(#()) , prod(cons(x, l)) -> *(x, prod(l)) , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)) , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) , inter(x, nil()) -> nil() , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) , inter(nil(), x) -> nil() , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) , ifinter(false(), x, l1, l2) -> inter(l1, l2) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,12,15,16,21,23,24,25,26,28,32,37,41,50,52,55,58} by applications of Pre({1,12,15,16,21,23,24,25,26,28,32,37,41,50,52,55,58}) = {2,3,5,8,9,10,11,13,14,17,18,19,20,22,27,29,30,31,33,34,35,40,43,44,45,47,49,51,60,61}. Here rules are labeled as follows: DPs: { 1: 0^#(#()) -> c_1() , 2: +^#(x, #()) -> c_2(x) , 3: +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) , 4: +^#(0(x), 1(y)) -> c_4(+^#(x, y)) , 5: +^#(#(), x) -> c_5(x) , 6: +^#(+(x, y), z) -> c_6(+^#(x, +(y, z))) , 7: +^#(1(x), 0(y)) -> c_7(+^#(x, y)) , 8: +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) , 9: -^#(x, #()) -> c_9(x) , 10: -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) , 11: -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) , 12: -^#(#(), x) -> c_12() , 13: -^#(1(x), 0(y)) -> c_13(-^#(x, y)) , 14: -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) , 15: not^#(true()) -> c_15() , 16: not^#(false()) -> c_16() , 17: if^#(true(), x, y) -> c_17(x) , 18: if^#(false(), x, y) -> c_18(y) , 19: eq^#(0(x), 0(y)) -> c_19(eq^#(x, y)) , 20: eq^#(0(x), #()) -> c_20(eq^#(x, #())) , 21: eq^#(0(x), 1(y)) -> c_21() , 22: eq^#(#(), 0(y)) -> c_22(eq^#(#(), y)) , 23: eq^#(#(), #()) -> c_23() , 24: eq^#(#(), 1(y)) -> c_24() , 25: eq^#(1(x), 0(y)) -> c_25() , 26: eq^#(1(x), #()) -> c_26() , 27: eq^#(1(x), 1(y)) -> c_27(eq^#(x, y)) , 28: ge^#(x, #()) -> c_28() , 29: ge^#(0(x), 0(y)) -> c_29(ge^#(x, y)) , 30: ge^#(0(x), 1(y)) -> c_30(not^#(ge(y, x))) , 31: ge^#(#(), 0(x)) -> c_31(ge^#(#(), x)) , 32: ge^#(#(), 1(x)) -> c_32() , 33: ge^#(1(x), 0(y)) -> c_33(ge^#(x, y)) , 34: ge^#(1(x), 1(y)) -> c_34(ge^#(x, y)) , 35: log^#(x) -> c_35(-^#(log'(x), 1(#()))) , 36: log'^#(0(x)) -> c_36(if^#(ge(x, 1(#())), +(log'(x), 1(#())), #())) , 37: log'^#(#()) -> c_37() , 38: log'^#(1(x)) -> c_38(+^#(log'(x), 1(#()))) , 39: *^#(x, +(y, z)) -> c_39(+^#(*(x, y), *(x, z))) , 40: *^#(0(x), y) -> c_40(0^#(*(x, y))) , 41: *^#(#(), x) -> c_41() , 42: *^#(1(x), y) -> c_42(+^#(0(*(x, y)), y)) , 43: *^#(*(x, y), z) -> c_43(*^#(x, *(y, z))) , 44: app^#(nil(), l) -> c_44(l) , 45: app^#(cons(x, l1), l2) -> c_45(x, app^#(l1, l2)) , 46: sum^#(app(l1, l2)) -> c_46(+^#(sum(l1), sum(l2))) , 47: sum^#(nil()) -> c_47(0^#(#())) , 48: sum^#(cons(x, l)) -> c_48(+^#(x, sum(l))) , 49: prod^#(app(l1, l2)) -> c_49(*^#(prod(l1), prod(l2))) , 50: prod^#(nil()) -> c_50() , 51: prod^#(cons(x, l)) -> c_51(*^#(x, prod(l))) , 52: mem^#(x, nil()) -> c_52() , 53: mem^#(x, cons(y, l)) -> c_53(if^#(eq(x, y), true(), mem(x, l))) , 54: inter^#(l1, app(l2, l3)) -> c_54(app^#(inter(l1, l2), inter(l1, l3))) , 55: inter^#(x, nil()) -> c_55() , 56: inter^#(l1, cons(x, l2)) -> c_56(ifinter^#(mem(x, l1), x, l2, l1)) , 57: inter^#(app(l1, l2), l3) -> c_57(app^#(inter(l1, l3), inter(l2, l3))) , 58: inter^#(nil(), x) -> c_58() , 59: inter^#(cons(x, l1), l2) -> c_59(ifinter^#(mem(x, l2), x, l1, l2)) , 60: ifinter^#(true(), x, l1, l2) -> c_60(x, inter^#(l1, l2)) , 61: ifinter^#(false(), x, l1, l2) -> c_61(inter^#(l1, l2)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(x, #()) -> c_2(x) , +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) , +^#(0(x), 1(y)) -> c_4(+^#(x, y)) , +^#(#(), x) -> c_5(x) , +^#(+(x, y), z) -> c_6(+^#(x, +(y, z))) , +^#(1(x), 0(y)) -> c_7(+^#(x, y)) , +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) , -^#(x, #()) -> c_9(x) , -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) , -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) , -^#(1(x), 0(y)) -> c_13(-^#(x, y)) , -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) , if^#(true(), x, y) -> c_17(x) , if^#(false(), x, y) -> c_18(y) , eq^#(0(x), 0(y)) -> c_19(eq^#(x, y)) , eq^#(0(x), #()) -> c_20(eq^#(x, #())) , eq^#(#(), 0(y)) -> c_22(eq^#(#(), y)) , eq^#(1(x), 1(y)) -> c_27(eq^#(x, y)) , ge^#(0(x), 0(y)) -> c_29(ge^#(x, y)) , ge^#(0(x), 1(y)) -> c_30(not^#(ge(y, x))) , ge^#(#(), 0(x)) -> c_31(ge^#(#(), x)) , ge^#(1(x), 0(y)) -> c_33(ge^#(x, y)) , ge^#(1(x), 1(y)) -> c_34(ge^#(x, y)) , log^#(x) -> c_35(-^#(log'(x), 1(#()))) , log'^#(0(x)) -> c_36(if^#(ge(x, 1(#())), +(log'(x), 1(#())), #())) , log'^#(1(x)) -> c_38(+^#(log'(x), 1(#()))) , *^#(x, +(y, z)) -> c_39(+^#(*(x, y), *(x, z))) , *^#(0(x), y) -> c_40(0^#(*(x, y))) , *^#(1(x), y) -> c_42(+^#(0(*(x, y)), y)) , *^#(*(x, y), z) -> c_43(*^#(x, *(y, z))) , app^#(nil(), l) -> c_44(l) , app^#(cons(x, l1), l2) -> c_45(x, app^#(l1, l2)) , sum^#(app(l1, l2)) -> c_46(+^#(sum(l1), sum(l2))) , sum^#(nil()) -> c_47(0^#(#())) , sum^#(cons(x, l)) -> c_48(+^#(x, sum(l))) , prod^#(app(l1, l2)) -> c_49(*^#(prod(l1), prod(l2))) , prod^#(cons(x, l)) -> c_51(*^#(x, prod(l))) , mem^#(x, cons(y, l)) -> c_53(if^#(eq(x, y), true(), mem(x, l))) , inter^#(l1, app(l2, l3)) -> c_54(app^#(inter(l1, l2), inter(l1, l3))) , inter^#(l1, cons(x, l2)) -> c_56(ifinter^#(mem(x, l1), x, l2, l1)) , inter^#(app(l1, l2), l3) -> c_57(app^#(inter(l1, l3), inter(l2, l3))) , inter^#(cons(x, l1), l2) -> c_59(ifinter^#(mem(x, l2), x, l1, l2)) , ifinter^#(true(), x, l1, l2) -> c_60(x, inter^#(l1, l2)) , ifinter^#(false(), x, l1, l2) -> c_61(inter^#(l1, l2)) } Strict Trs: { 0(#()) -> #() , +(x, #()) -> x , +(0(x), 0(y)) -> 0(+(x, y)) , +(0(x), 1(y)) -> 1(+(x, y)) , +(#(), x) -> x , +(+(x, y), z) -> +(x, +(y, z)) , +(1(x), 0(y)) -> 1(+(x, y)) , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) , -(x, #()) -> x , -(0(x), 0(y)) -> 0(-(x, y)) , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) , -(#(), x) -> #() , -(1(x), 0(y)) -> 1(-(x, y)) , -(1(x), 1(y)) -> 0(-(x, y)) , not(true()) -> false() , not(false()) -> true() , if(true(), x, y) -> x , if(false(), x, y) -> y , eq(0(x), 0(y)) -> eq(x, y) , eq(0(x), #()) -> eq(x, #()) , eq(0(x), 1(y)) -> false() , eq(#(), 0(y)) -> eq(#(), y) , eq(#(), #()) -> true() , eq(#(), 1(y)) -> false() , eq(1(x), 0(y)) -> false() , eq(1(x), #()) -> false() , eq(1(x), 1(y)) -> eq(x, y) , ge(x, #()) -> true() , ge(0(x), 0(y)) -> ge(x, y) , ge(0(x), 1(y)) -> not(ge(y, x)) , ge(#(), 0(x)) -> ge(#(), x) , ge(#(), 1(x)) -> false() , ge(1(x), 0(y)) -> ge(x, y) , ge(1(x), 1(y)) -> ge(x, y) , log(x) -> -(log'(x), 1(#())) , log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()) , log'(#()) -> #() , log'(1(x)) -> +(log'(x), 1(#())) , *(x, +(y, z)) -> +(*(x, y), *(x, z)) , *(0(x), y) -> 0(*(x, y)) , *(#(), x) -> #() , *(1(x), y) -> +(0(*(x, y)), y) , *(*(x, y), z) -> *(x, *(y, z)) , app(nil(), l) -> l , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) , sum(app(l1, l2)) -> +(sum(l1), sum(l2)) , sum(nil()) -> 0(#()) , sum(cons(x, l)) -> +(x, sum(l)) , prod(app(l1, l2)) -> *(prod(l1), prod(l2)) , prod(nil()) -> 1(#()) , prod(cons(x, l)) -> *(x, prod(l)) , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)) , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) , inter(x, nil()) -> nil() , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) , inter(nil(), x) -> nil() , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) , ifinter(false(), x, l1, l2) -> inter(l1, l2) } Weak DPs: { 0^#(#()) -> c_1() , -^#(#(), x) -> c_12() , not^#(true()) -> c_15() , not^#(false()) -> c_16() , eq^#(0(x), 1(y)) -> c_21() , eq^#(#(), #()) -> c_23() , eq^#(#(), 1(y)) -> c_24() , eq^#(1(x), 0(y)) -> c_25() , eq^#(1(x), #()) -> c_26() , ge^#(x, #()) -> c_28() , ge^#(#(), 1(x)) -> c_32() , log'^#(#()) -> c_37() , *^#(#(), x) -> c_41() , prod^#(nil()) -> c_50() , mem^#(x, nil()) -> c_52() , inter^#(x, nil()) -> c_55() , inter^#(nil(), x) -> c_58() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,7,9,12,20,28,34} by applications of Pre({2,7,9,12,20,28,34}) = {1,3,4,5,6,8,10,11,13,14,19,22,23,24,26,27,29,30,31,32,33,35,36,37,43}. Here rules are labeled as follows: DPs: { 1: +^#(x, #()) -> c_2(x) , 2: +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) , 3: +^#(0(x), 1(y)) -> c_4(+^#(x, y)) , 4: +^#(#(), x) -> c_5(x) , 5: +^#(+(x, y), z) -> c_6(+^#(x, +(y, z))) , 6: +^#(1(x), 0(y)) -> c_7(+^#(x, y)) , 7: +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) , 8: -^#(x, #()) -> c_9(x) , 9: -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) , 10: -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) , 11: -^#(1(x), 0(y)) -> c_13(-^#(x, y)) , 12: -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) , 13: if^#(true(), x, y) -> c_17(x) , 14: if^#(false(), x, y) -> c_18(y) , 15: eq^#(0(x), 0(y)) -> c_19(eq^#(x, y)) , 16: eq^#(0(x), #()) -> c_20(eq^#(x, #())) , 17: eq^#(#(), 0(y)) -> c_22(eq^#(#(), y)) , 18: eq^#(1(x), 1(y)) -> c_27(eq^#(x, y)) , 19: ge^#(0(x), 0(y)) -> c_29(ge^#(x, y)) , 20: ge^#(0(x), 1(y)) -> c_30(not^#(ge(y, x))) , 21: ge^#(#(), 0(x)) -> c_31(ge^#(#(), x)) , 22: ge^#(1(x), 0(y)) -> c_33(ge^#(x, y)) , 23: ge^#(1(x), 1(y)) -> c_34(ge^#(x, y)) , 24: log^#(x) -> c_35(-^#(log'(x), 1(#()))) , 25: log'^#(0(x)) -> c_36(if^#(ge(x, 1(#())), +(log'(x), 1(#())), #())) , 26: log'^#(1(x)) -> c_38(+^#(log'(x), 1(#()))) , 27: *^#(x, +(y, z)) -> c_39(+^#(*(x, y), *(x, z))) , 28: *^#(0(x), y) -> c_40(0^#(*(x, y))) , 29: *^#(1(x), y) -> c_42(+^#(0(*(x, y)), y)) , 30: *^#(*(x, y), z) -> c_43(*^#(x, *(y, z))) , 31: app^#(nil(), l) -> c_44(l) , 32: app^#(cons(x, l1), l2) -> c_45(x, app^#(l1, l2)) , 33: sum^#(app(l1, l2)) -> c_46(+^#(sum(l1), sum(l2))) , 34: sum^#(nil()) -> c_47(0^#(#())) , 35: sum^#(cons(x, l)) -> c_48(+^#(x, sum(l))) , 36: prod^#(app(l1, l2)) -> c_49(*^#(prod(l1), prod(l2))) , 37: prod^#(cons(x, l)) -> c_51(*^#(x, prod(l))) , 38: mem^#(x, cons(y, l)) -> c_53(if^#(eq(x, y), true(), mem(x, l))) , 39: inter^#(l1, app(l2, l3)) -> c_54(app^#(inter(l1, l2), inter(l1, l3))) , 40: inter^#(l1, cons(x, l2)) -> c_56(ifinter^#(mem(x, l1), x, l2, l1)) , 41: inter^#(app(l1, l2), l3) -> c_57(app^#(inter(l1, l3), inter(l2, l3))) , 42: inter^#(cons(x, l1), l2) -> c_59(ifinter^#(mem(x, l2), x, l1, l2)) , 43: ifinter^#(true(), x, l1, l2) -> c_60(x, inter^#(l1, l2)) , 44: ifinter^#(false(), x, l1, l2) -> c_61(inter^#(l1, l2)) , 45: 0^#(#()) -> c_1() , 46: -^#(#(), x) -> c_12() , 47: not^#(true()) -> c_15() , 48: not^#(false()) -> c_16() , 49: eq^#(0(x), 1(y)) -> c_21() , 50: eq^#(#(), #()) -> c_23() , 51: eq^#(#(), 1(y)) -> c_24() , 52: eq^#(1(x), 0(y)) -> c_25() , 53: eq^#(1(x), #()) -> c_26() , 54: ge^#(x, #()) -> c_28() , 55: ge^#(#(), 1(x)) -> c_32() , 56: log'^#(#()) -> c_37() , 57: *^#(#(), x) -> c_41() , 58: prod^#(nil()) -> c_50() , 59: mem^#(x, nil()) -> c_52() , 60: inter^#(x, nil()) -> c_55() , 61: inter^#(nil(), x) -> c_58() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(x, #()) -> c_2(x) , +^#(0(x), 1(y)) -> c_4(+^#(x, y)) , +^#(#(), x) -> c_5(x) , +^#(+(x, y), z) -> c_6(+^#(x, +(y, z))) , +^#(1(x), 0(y)) -> c_7(+^#(x, y)) , -^#(x, #()) -> c_9(x) , -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) , -^#(1(x), 0(y)) -> c_13(-^#(x, y)) , if^#(true(), x, y) -> c_17(x) , if^#(false(), x, y) -> c_18(y) , eq^#(0(x), 0(y)) -> c_19(eq^#(x, y)) , eq^#(0(x), #()) -> c_20(eq^#(x, #())) , eq^#(#(), 0(y)) -> c_22(eq^#(#(), y)) , eq^#(1(x), 1(y)) -> c_27(eq^#(x, y)) , ge^#(0(x), 0(y)) -> c_29(ge^#(x, y)) , ge^#(#(), 0(x)) -> c_31(ge^#(#(), x)) , ge^#(1(x), 0(y)) -> c_33(ge^#(x, y)) , ge^#(1(x), 1(y)) -> c_34(ge^#(x, y)) , log^#(x) -> c_35(-^#(log'(x), 1(#()))) , log'^#(0(x)) -> c_36(if^#(ge(x, 1(#())), +(log'(x), 1(#())), #())) , log'^#(1(x)) -> c_38(+^#(log'(x), 1(#()))) , *^#(x, +(y, z)) -> c_39(+^#(*(x, y), *(x, z))) , *^#(1(x), y) -> c_42(+^#(0(*(x, y)), y)) , *^#(*(x, y), z) -> c_43(*^#(x, *(y, z))) , app^#(nil(), l) -> c_44(l) , app^#(cons(x, l1), l2) -> c_45(x, app^#(l1, l2)) , sum^#(app(l1, l2)) -> c_46(+^#(sum(l1), sum(l2))) , sum^#(cons(x, l)) -> c_48(+^#(x, sum(l))) , prod^#(app(l1, l2)) -> c_49(*^#(prod(l1), prod(l2))) , prod^#(cons(x, l)) -> c_51(*^#(x, prod(l))) , mem^#(x, cons(y, l)) -> c_53(if^#(eq(x, y), true(), mem(x, l))) , inter^#(l1, app(l2, l3)) -> c_54(app^#(inter(l1, l2), inter(l1, l3))) , inter^#(l1, cons(x, l2)) -> c_56(ifinter^#(mem(x, l1), x, l2, l1)) , inter^#(app(l1, l2), l3) -> c_57(app^#(inter(l1, l3), inter(l2, l3))) , inter^#(cons(x, l1), l2) -> c_59(ifinter^#(mem(x, l2), x, l1, l2)) , ifinter^#(true(), x, l1, l2) -> c_60(x, inter^#(l1, l2)) , ifinter^#(false(), x, l1, l2) -> c_61(inter^#(l1, l2)) } Strict Trs: { 0(#()) -> #() , +(x, #()) -> x , +(0(x), 0(y)) -> 0(+(x, y)) , +(0(x), 1(y)) -> 1(+(x, y)) , +(#(), x) -> x , +(+(x, y), z) -> +(x, +(y, z)) , +(1(x), 0(y)) -> 1(+(x, y)) , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) , -(x, #()) -> x , -(0(x), 0(y)) -> 0(-(x, y)) , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) , -(#(), x) -> #() , -(1(x), 0(y)) -> 1(-(x, y)) , -(1(x), 1(y)) -> 0(-(x, y)) , not(true()) -> false() , not(false()) -> true() , if(true(), x, y) -> x , if(false(), x, y) -> y , eq(0(x), 0(y)) -> eq(x, y) , eq(0(x), #()) -> eq(x, #()) , eq(0(x), 1(y)) -> false() , eq(#(), 0(y)) -> eq(#(), y) , eq(#(), #()) -> true() , eq(#(), 1(y)) -> false() , eq(1(x), 0(y)) -> false() , eq(1(x), #()) -> false() , eq(1(x), 1(y)) -> eq(x, y) , ge(x, #()) -> true() , ge(0(x), 0(y)) -> ge(x, y) , ge(0(x), 1(y)) -> not(ge(y, x)) , ge(#(), 0(x)) -> ge(#(), x) , ge(#(), 1(x)) -> false() , ge(1(x), 0(y)) -> ge(x, y) , ge(1(x), 1(y)) -> ge(x, y) , log(x) -> -(log'(x), 1(#())) , log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()) , log'(#()) -> #() , log'(1(x)) -> +(log'(x), 1(#())) , *(x, +(y, z)) -> +(*(x, y), *(x, z)) , *(0(x), y) -> 0(*(x, y)) , *(#(), x) -> #() , *(1(x), y) -> +(0(*(x, y)), y) , *(*(x, y), z) -> *(x, *(y, z)) , app(nil(), l) -> l , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) , sum(app(l1, l2)) -> +(sum(l1), sum(l2)) , sum(nil()) -> 0(#()) , sum(cons(x, l)) -> +(x, sum(l)) , prod(app(l1, l2)) -> *(prod(l1), prod(l2)) , prod(nil()) -> 1(#()) , prod(cons(x, l)) -> *(x, prod(l)) , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)) , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) , inter(x, nil()) -> nil() , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) , inter(nil(), x) -> nil() , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) , ifinter(false(), x, l1, l2) -> inter(l1, l2) } Weak DPs: { 0^#(#()) -> c_1() , +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) , +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) , -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) , -^#(#(), x) -> c_12() , -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) , not^#(true()) -> c_15() , not^#(false()) -> c_16() , eq^#(0(x), 1(y)) -> c_21() , eq^#(#(), #()) -> c_23() , eq^#(#(), 1(y)) -> c_24() , eq^#(1(x), 0(y)) -> c_25() , eq^#(1(x), #()) -> c_26() , ge^#(x, #()) -> c_28() , ge^#(0(x), 1(y)) -> c_30(not^#(ge(y, x))) , ge^#(#(), 1(x)) -> c_32() , log'^#(#()) -> c_37() , *^#(0(x), y) -> c_40(0^#(*(x, y))) , *^#(#(), x) -> c_41() , sum^#(nil()) -> c_47(0^#(#())) , prod^#(nil()) -> c_50() , mem^#(x, nil()) -> c_52() , inter^#(x, nil()) -> c_55() , inter^#(nil(), x) -> c_58() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..