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