MAYBE 919.41/297.14 MAYBE 919.41/297.14 919.41/297.14 We are left with following problem, upon which TcT provides the 919.41/297.14 certificate MAYBE. 919.41/297.14 919.41/297.14 Strict Trs: 919.41/297.14 { 0(#()) -> #() 919.41/297.14 , +(x, #()) -> x 919.41/297.14 , +(x, +(y, z)) -> +(+(x, y), z) 919.41/297.14 , +(0(x), 0(y)) -> 0(+(x, y)) 919.41/297.14 , +(0(x), 1(y)) -> 1(+(x, y)) 919.41/297.14 , +(#(), x) -> x 919.41/297.14 , +(1(x), 0(y)) -> 1(+(x, y)) 919.41/297.14 , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) 919.41/297.14 , -(x, #()) -> x 919.41/297.14 , -(0(x), 0(y)) -> 0(-(x, y)) 919.41/297.14 , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) 919.41/297.14 , -(#(), x) -> #() 919.41/297.14 , -(1(x), 0(y)) -> 1(-(x, y)) 919.41/297.14 , -(1(x), 1(y)) -> 0(-(x, y)) 919.41/297.14 , not(false()) -> true() 919.41/297.14 , not(true()) -> false() 919.41/297.14 , and(x, false()) -> false() 919.41/297.14 , and(x, true()) -> x 919.41/297.14 , if(false(), x, y) -> y 919.41/297.14 , if(true(), x, y) -> x 919.41/297.14 , ge(x, #()) -> true() 919.41/297.14 , ge(0(x), 0(y)) -> ge(x, y) 919.41/297.14 , ge(0(x), 1(y)) -> not(ge(y, x)) 919.41/297.14 , ge(#(), 0(x)) -> ge(#(), x) 919.41/297.14 , ge(#(), 1(x)) -> false() 919.41/297.14 , ge(1(x), 0(y)) -> ge(x, y) 919.41/297.14 , ge(1(x), 1(y)) -> ge(x, y) 919.41/297.14 , val(l(x)) -> x 919.41/297.14 , val(n(x, y, z)) -> x 919.41/297.14 , min(l(x)) -> x 919.41/297.14 , min(n(x, y, z)) -> min(y) 919.41/297.14 , max(l(x)) -> x 919.41/297.14 , max(n(x, y, z)) -> max(z) 919.41/297.14 , bs(l(x)) -> true() 919.41/297.14 , bs(n(x, y, z)) -> 919.41/297.14 and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))) 919.41/297.14 , size(l(x)) -> 1(#()) 919.41/297.14 , size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())) 919.41/297.14 , wb(l(x)) -> true() 919.41/297.14 , wb(n(x, y, z)) -> 919.41/297.14 and(if(ge(size(y), size(z)), 919.41/297.14 ge(1(#()), -(size(y), size(z))), 919.41/297.14 ge(1(#()), -(size(z), size(y)))), 919.41/297.14 and(wb(y), wb(z))) } 919.41/297.14 Obligation: 919.41/297.14 runtime complexity 919.41/297.14 Answer: 919.41/297.14 MAYBE 919.41/297.14 919.41/297.14 None of the processors succeeded. 919.41/297.14 919.41/297.14 Details of failed attempt(s): 919.41/297.14 ----------------------------- 919.41/297.14 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 919.41/297.14 following reason: 919.41/297.14 919.41/297.14 Computation stopped due to timeout after 297.0 seconds. 919.41/297.14 919.41/297.14 2) 'Best' failed due to the following reason: 919.41/297.14 919.41/297.14 None of the processors succeeded. 919.41/297.14 919.41/297.14 Details of failed attempt(s): 919.41/297.14 ----------------------------- 919.41/297.14 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 919.41/297.14 seconds)' failed due to the following reason: 919.41/297.14 919.41/297.14 Computation stopped due to timeout after 148.0 seconds. 919.41/297.14 919.41/297.14 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 919.41/297.14 failed due to the following reason: 919.41/297.14 919.41/297.14 None of the processors succeeded. 919.41/297.14 919.41/297.14 Details of failed attempt(s): 919.41/297.14 ----------------------------- 919.41/297.14 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 919.41/297.14 failed due to the following reason: 919.41/297.14 919.41/297.14 match-boundness of the problem could not be verified. 919.41/297.14 919.41/297.14 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 919.41/297.14 failed due to the following reason: 919.41/297.14 919.41/297.14 match-boundness of the problem could not be verified. 919.41/297.14 919.41/297.14 919.41/297.14 3) 'Best' failed due to the following reason: 919.41/297.14 919.41/297.14 None of the processors succeeded. 919.41/297.14 919.41/297.14 Details of failed attempt(s): 919.41/297.14 ----------------------------- 919.41/297.14 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 919.41/297.14 to the following reason: 919.41/297.14 919.41/297.14 The processor is inapplicable, reason: 919.41/297.14 Processor only applicable for innermost runtime complexity analysis 919.41/297.14 919.41/297.14 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 919.41/297.14 following reason: 919.41/297.14 919.41/297.14 The processor is inapplicable, reason: 919.41/297.14 Processor only applicable for innermost runtime complexity analysis 919.41/297.14 919.41/297.14 919.41/297.14 919.41/297.14 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 919.41/297.14 the following reason: 919.41/297.14 919.41/297.14 We add the following weak dependency pairs: 919.41/297.14 919.41/297.14 Strict DPs: 919.41/297.14 { 0^#(#()) -> c_1() 919.41/297.14 , +^#(x, #()) -> c_2(x) 919.41/297.14 , +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z)) 919.41/297.14 , +^#(0(x), 0(y)) -> c_4(0^#(+(x, y))) 919.41/297.14 , +^#(0(x), 1(y)) -> c_5(+^#(x, y)) 919.41/297.14 , +^#(#(), x) -> c_6(x) 919.41/297.14 , +^#(1(x), 0(y)) -> c_7(+^#(x, y)) 919.41/297.14 , +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) 919.41/297.14 , -^#(x, #()) -> c_9(x) 919.41/297.14 , -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) 919.41/297.14 , -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) 919.41/297.14 , -^#(#(), x) -> c_12() 919.41/297.14 , -^#(1(x), 0(y)) -> c_13(-^#(x, y)) 919.41/297.14 , -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) 919.41/297.14 , not^#(false()) -> c_15() 919.41/297.14 , not^#(true()) -> c_16() 919.41/297.14 , and^#(x, false()) -> c_17() 919.41/297.14 , and^#(x, true()) -> c_18(x) 919.41/297.14 , if^#(false(), x, y) -> c_19(y) 919.41/297.14 , if^#(true(), x, y) -> c_20(x) 919.41/297.14 , ge^#(x, #()) -> c_21() 919.41/297.14 , ge^#(0(x), 0(y)) -> c_22(ge^#(x, y)) 919.41/297.14 , ge^#(0(x), 1(y)) -> c_23(not^#(ge(y, x))) 919.41/297.14 , ge^#(#(), 0(x)) -> c_24(ge^#(#(), x)) 919.41/297.14 , ge^#(#(), 1(x)) -> c_25() 919.41/297.14 , ge^#(1(x), 0(y)) -> c_26(ge^#(x, y)) 919.41/297.14 , ge^#(1(x), 1(y)) -> c_27(ge^#(x, y)) 919.41/297.14 , val^#(l(x)) -> c_28(x) 919.41/297.14 , val^#(n(x, y, z)) -> c_29(x) 919.41/297.14 , min^#(l(x)) -> c_30(x) 919.41/297.14 , min^#(n(x, y, z)) -> c_31(min^#(y)) 919.41/297.14 , max^#(l(x)) -> c_32(x) 919.41/297.14 , max^#(n(x, y, z)) -> c_33(max^#(z)) 919.41/297.14 , bs^#(l(x)) -> c_34() 919.41/297.14 , bs^#(n(x, y, z)) -> 919.41/297.14 c_35(and^#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))) 919.41/297.14 , size^#(l(x)) -> c_36() 919.41/297.14 , size^#(n(x, y, z)) -> c_37(+^#(+(size(x), size(y)), 1(#()))) 919.41/297.14 , wb^#(l(x)) -> c_38() 919.41/297.14 , wb^#(n(x, y, z)) -> 919.41/297.14 c_39(and^#(if(ge(size(y), size(z)), 919.41/297.14 ge(1(#()), -(size(y), size(z))), 919.41/297.14 ge(1(#()), -(size(z), size(y)))), 919.41/297.14 and(wb(y), wb(z)))) } 919.41/297.14 919.41/297.14 and mark the set of starting terms. 919.41/297.14 919.41/297.14 We are left with following problem, upon which TcT provides the 919.41/297.14 certificate MAYBE. 919.41/297.14 919.41/297.14 Strict DPs: 919.41/297.14 { 0^#(#()) -> c_1() 919.41/297.14 , +^#(x, #()) -> c_2(x) 919.41/297.14 , +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z)) 919.41/297.14 , +^#(0(x), 0(y)) -> c_4(0^#(+(x, y))) 919.41/297.14 , +^#(0(x), 1(y)) -> c_5(+^#(x, y)) 919.41/297.14 , +^#(#(), x) -> c_6(x) 919.41/297.14 , +^#(1(x), 0(y)) -> c_7(+^#(x, y)) 919.41/297.14 , +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) 919.41/297.14 , -^#(x, #()) -> c_9(x) 919.41/297.14 , -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) 919.41/297.14 , -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) 919.41/297.14 , -^#(#(), x) -> c_12() 919.41/297.14 , -^#(1(x), 0(y)) -> c_13(-^#(x, y)) 919.41/297.14 , -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) 919.41/297.14 , not^#(false()) -> c_15() 919.41/297.14 , not^#(true()) -> c_16() 919.41/297.14 , and^#(x, false()) -> c_17() 919.41/297.14 , and^#(x, true()) -> c_18(x) 919.41/297.14 , if^#(false(), x, y) -> c_19(y) 919.41/297.14 , if^#(true(), x, y) -> c_20(x) 919.41/297.14 , ge^#(x, #()) -> c_21() 919.41/297.14 , ge^#(0(x), 0(y)) -> c_22(ge^#(x, y)) 919.41/297.14 , ge^#(0(x), 1(y)) -> c_23(not^#(ge(y, x))) 919.41/297.14 , ge^#(#(), 0(x)) -> c_24(ge^#(#(), x)) 919.41/297.14 , ge^#(#(), 1(x)) -> c_25() 919.41/297.14 , ge^#(1(x), 0(y)) -> c_26(ge^#(x, y)) 919.41/297.14 , ge^#(1(x), 1(y)) -> c_27(ge^#(x, y)) 919.41/297.14 , val^#(l(x)) -> c_28(x) 919.41/297.14 , val^#(n(x, y, z)) -> c_29(x) 919.41/297.14 , min^#(l(x)) -> c_30(x) 919.41/297.14 , min^#(n(x, y, z)) -> c_31(min^#(y)) 919.41/297.14 , max^#(l(x)) -> c_32(x) 919.41/297.14 , max^#(n(x, y, z)) -> c_33(max^#(z)) 919.41/297.14 , bs^#(l(x)) -> c_34() 919.41/297.14 , bs^#(n(x, y, z)) -> 919.41/297.14 c_35(and^#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))) 919.41/297.14 , size^#(l(x)) -> c_36() 919.41/297.14 , size^#(n(x, y, z)) -> c_37(+^#(+(size(x), size(y)), 1(#()))) 919.41/297.14 , wb^#(l(x)) -> c_38() 919.41/297.14 , wb^#(n(x, y, z)) -> 919.41/297.14 c_39(and^#(if(ge(size(y), size(z)), 919.41/297.14 ge(1(#()), -(size(y), size(z))), 919.41/297.14 ge(1(#()), -(size(z), size(y)))), 919.41/297.14 and(wb(y), wb(z)))) } 919.41/297.14 Strict Trs: 919.41/297.14 { 0(#()) -> #() 919.41/297.14 , +(x, #()) -> x 919.41/297.14 , +(x, +(y, z)) -> +(+(x, y), z) 919.41/297.14 , +(0(x), 0(y)) -> 0(+(x, y)) 919.41/297.14 , +(0(x), 1(y)) -> 1(+(x, y)) 919.41/297.14 , +(#(), x) -> x 919.41/297.14 , +(1(x), 0(y)) -> 1(+(x, y)) 919.41/297.14 , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) 919.41/297.14 , -(x, #()) -> x 919.41/297.14 , -(0(x), 0(y)) -> 0(-(x, y)) 919.41/297.14 , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) 919.41/297.14 , -(#(), x) -> #() 919.41/297.14 , -(1(x), 0(y)) -> 1(-(x, y)) 919.41/297.14 , -(1(x), 1(y)) -> 0(-(x, y)) 919.41/297.14 , not(false()) -> true() 919.41/297.14 , not(true()) -> false() 919.41/297.14 , and(x, false()) -> false() 919.41/297.14 , and(x, true()) -> x 919.41/297.14 , if(false(), x, y) -> y 919.41/297.14 , if(true(), x, y) -> x 919.41/297.14 , ge(x, #()) -> true() 919.41/297.14 , ge(0(x), 0(y)) -> ge(x, y) 919.41/297.14 , ge(0(x), 1(y)) -> not(ge(y, x)) 919.41/297.14 , ge(#(), 0(x)) -> ge(#(), x) 919.41/297.14 , ge(#(), 1(x)) -> false() 919.41/297.14 , ge(1(x), 0(y)) -> ge(x, y) 919.41/297.14 , ge(1(x), 1(y)) -> ge(x, y) 919.41/297.14 , val(l(x)) -> x 919.41/297.14 , val(n(x, y, z)) -> x 919.41/297.14 , min(l(x)) -> x 919.41/297.14 , min(n(x, y, z)) -> min(y) 919.41/297.14 , max(l(x)) -> x 919.41/297.14 , max(n(x, y, z)) -> max(z) 919.41/297.14 , bs(l(x)) -> true() 919.41/297.14 , bs(n(x, y, z)) -> 919.41/297.14 and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))) 919.41/297.14 , size(l(x)) -> 1(#()) 919.41/297.14 , size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())) 919.41/297.14 , wb(l(x)) -> true() 919.41/297.14 , wb(n(x, y, z)) -> 919.41/297.14 and(if(ge(size(y), size(z)), 919.41/297.14 ge(1(#()), -(size(y), size(z))), 919.41/297.14 ge(1(#()), -(size(z), size(y)))), 919.41/297.14 and(wb(y), wb(z))) } 919.41/297.14 Obligation: 919.41/297.14 runtime complexity 919.41/297.14 Answer: 919.41/297.14 MAYBE 919.41/297.14 919.41/297.14 We estimate the number of application of 919.41/297.14 {1,12,15,16,17,21,25,34,36,38} by applications of 919.41/297.14 Pre({1,12,15,16,17,21,25,34,36,38}) = 919.41/297.14 {2,4,6,8,9,10,11,13,14,18,19,20,22,23,24,26,27,28,29,30,32,35,39}. 919.41/297.14 Here rules are labeled as follows: 919.41/297.14 919.41/297.14 DPs: 919.41/297.14 { 1: 0^#(#()) -> c_1() 919.41/297.14 , 2: +^#(x, #()) -> c_2(x) 919.41/297.14 , 3: +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z)) 919.41/297.14 , 4: +^#(0(x), 0(y)) -> c_4(0^#(+(x, y))) 919.41/297.14 , 5: +^#(0(x), 1(y)) -> c_5(+^#(x, y)) 919.41/297.14 , 6: +^#(#(), x) -> c_6(x) 919.41/297.14 , 7: +^#(1(x), 0(y)) -> c_7(+^#(x, y)) 919.41/297.14 , 8: +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) 919.41/297.14 , 9: -^#(x, #()) -> c_9(x) 919.41/297.14 , 10: -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) 919.41/297.14 , 11: -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) 919.41/297.14 , 12: -^#(#(), x) -> c_12() 919.41/297.14 , 13: -^#(1(x), 0(y)) -> c_13(-^#(x, y)) 919.41/297.14 , 14: -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) 919.41/297.14 , 15: not^#(false()) -> c_15() 919.41/297.14 , 16: not^#(true()) -> c_16() 919.41/297.14 , 17: and^#(x, false()) -> c_17() 919.41/297.14 , 18: and^#(x, true()) -> c_18(x) 919.41/297.14 , 19: if^#(false(), x, y) -> c_19(y) 919.41/297.14 , 20: if^#(true(), x, y) -> c_20(x) 919.41/297.14 , 21: ge^#(x, #()) -> c_21() 919.41/297.14 , 22: ge^#(0(x), 0(y)) -> c_22(ge^#(x, y)) 919.41/297.14 , 23: ge^#(0(x), 1(y)) -> c_23(not^#(ge(y, x))) 919.41/297.14 , 24: ge^#(#(), 0(x)) -> c_24(ge^#(#(), x)) 919.41/297.14 , 25: ge^#(#(), 1(x)) -> c_25() 919.41/297.14 , 26: ge^#(1(x), 0(y)) -> c_26(ge^#(x, y)) 919.41/297.14 , 27: ge^#(1(x), 1(y)) -> c_27(ge^#(x, y)) 919.41/297.14 , 28: val^#(l(x)) -> c_28(x) 919.41/297.14 , 29: val^#(n(x, y, z)) -> c_29(x) 919.41/297.14 , 30: min^#(l(x)) -> c_30(x) 919.41/297.14 , 31: min^#(n(x, y, z)) -> c_31(min^#(y)) 919.41/297.14 , 32: max^#(l(x)) -> c_32(x) 919.41/297.14 , 33: max^#(n(x, y, z)) -> c_33(max^#(z)) 919.41/297.14 , 34: bs^#(l(x)) -> c_34() 919.41/297.14 , 35: bs^#(n(x, y, z)) -> 919.41/297.14 c_35(and^#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))) 919.41/297.14 , 36: size^#(l(x)) -> c_36() 919.41/297.14 , 37: size^#(n(x, y, z)) -> c_37(+^#(+(size(x), size(y)), 1(#()))) 919.41/297.14 , 38: wb^#(l(x)) -> c_38() 919.41/297.14 , 39: wb^#(n(x, y, z)) -> 919.41/297.14 c_39(and^#(if(ge(size(y), size(z)), 919.41/297.14 ge(1(#()), -(size(y), size(z))), 919.41/297.14 ge(1(#()), -(size(z), size(y)))), 919.41/297.14 and(wb(y), wb(z)))) } 919.41/297.14 919.41/297.14 We are left with following problem, upon which TcT provides the 919.41/297.14 certificate MAYBE. 919.41/297.14 919.41/297.14 Strict DPs: 919.41/297.14 { +^#(x, #()) -> c_2(x) 919.41/297.14 , +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z)) 919.41/297.14 , +^#(0(x), 0(y)) -> c_4(0^#(+(x, y))) 919.41/297.14 , +^#(0(x), 1(y)) -> c_5(+^#(x, y)) 919.41/297.14 , +^#(#(), x) -> c_6(x) 919.41/297.14 , +^#(1(x), 0(y)) -> c_7(+^#(x, y)) 919.41/297.14 , +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) 919.41/297.14 , -^#(x, #()) -> c_9(x) 919.41/297.14 , -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) 919.41/297.14 , -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) 919.41/297.14 , -^#(1(x), 0(y)) -> c_13(-^#(x, y)) 919.41/297.14 , -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) 919.41/297.14 , and^#(x, true()) -> c_18(x) 919.41/297.14 , if^#(false(), x, y) -> c_19(y) 919.41/297.14 , if^#(true(), x, y) -> c_20(x) 919.41/297.14 , ge^#(0(x), 0(y)) -> c_22(ge^#(x, y)) 919.41/297.14 , ge^#(0(x), 1(y)) -> c_23(not^#(ge(y, x))) 919.41/297.14 , ge^#(#(), 0(x)) -> c_24(ge^#(#(), x)) 919.41/297.14 , ge^#(1(x), 0(y)) -> c_26(ge^#(x, y)) 919.41/297.14 , ge^#(1(x), 1(y)) -> c_27(ge^#(x, y)) 919.41/297.14 , val^#(l(x)) -> c_28(x) 919.41/297.14 , val^#(n(x, y, z)) -> c_29(x) 919.41/297.14 , min^#(l(x)) -> c_30(x) 919.41/297.14 , min^#(n(x, y, z)) -> c_31(min^#(y)) 919.41/297.14 , max^#(l(x)) -> c_32(x) 919.41/297.14 , max^#(n(x, y, z)) -> c_33(max^#(z)) 919.41/297.14 , bs^#(n(x, y, z)) -> 919.41/297.14 c_35(and^#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))) 919.41/297.14 , size^#(n(x, y, z)) -> c_37(+^#(+(size(x), size(y)), 1(#()))) 919.41/297.14 , wb^#(n(x, y, z)) -> 919.41/297.14 c_39(and^#(if(ge(size(y), size(z)), 919.41/297.14 ge(1(#()), -(size(y), size(z))), 919.41/297.14 ge(1(#()), -(size(z), size(y)))), 919.41/297.14 and(wb(y), wb(z)))) } 919.41/297.14 Strict Trs: 919.41/297.14 { 0(#()) -> #() 919.41/297.14 , +(x, #()) -> x 919.41/297.14 , +(x, +(y, z)) -> +(+(x, y), z) 919.41/297.14 , +(0(x), 0(y)) -> 0(+(x, y)) 919.41/297.14 , +(0(x), 1(y)) -> 1(+(x, y)) 919.41/297.14 , +(#(), x) -> x 919.41/297.14 , +(1(x), 0(y)) -> 1(+(x, y)) 919.41/297.14 , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) 919.41/297.14 , -(x, #()) -> x 919.41/297.14 , -(0(x), 0(y)) -> 0(-(x, y)) 919.41/297.14 , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) 919.41/297.14 , -(#(), x) -> #() 919.41/297.14 , -(1(x), 0(y)) -> 1(-(x, y)) 919.41/297.14 , -(1(x), 1(y)) -> 0(-(x, y)) 919.41/297.14 , not(false()) -> true() 919.41/297.14 , not(true()) -> false() 919.41/297.14 , and(x, false()) -> false() 919.41/297.14 , and(x, true()) -> x 919.41/297.14 , if(false(), x, y) -> y 919.41/297.14 , if(true(), x, y) -> x 919.41/297.14 , ge(x, #()) -> true() 919.41/297.14 , ge(0(x), 0(y)) -> ge(x, y) 919.41/297.14 , ge(0(x), 1(y)) -> not(ge(y, x)) 919.41/297.15 , ge(#(), 0(x)) -> ge(#(), x) 919.41/297.15 , ge(#(), 1(x)) -> false() 919.41/297.15 , ge(1(x), 0(y)) -> ge(x, y) 919.41/297.15 , ge(1(x), 1(y)) -> ge(x, y) 919.41/297.15 , val(l(x)) -> x 919.41/297.15 , val(n(x, y, z)) -> x 919.41/297.15 , min(l(x)) -> x 919.41/297.15 , min(n(x, y, z)) -> min(y) 919.41/297.15 , max(l(x)) -> x 919.41/297.15 , max(n(x, y, z)) -> max(z) 919.41/297.15 , bs(l(x)) -> true() 919.41/297.15 , bs(n(x, y, z)) -> 919.41/297.15 and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))) 919.41/297.15 , size(l(x)) -> 1(#()) 919.41/297.15 , size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())) 919.41/297.15 , wb(l(x)) -> true() 919.41/297.15 , wb(n(x, y, z)) -> 919.41/297.15 and(if(ge(size(y), size(z)), 919.41/297.15 ge(1(#()), -(size(y), size(z))), 919.41/297.15 ge(1(#()), -(size(z), size(y)))), 919.41/297.15 and(wb(y), wb(z))) } 919.41/297.15 Weak DPs: 919.41/297.15 { 0^#(#()) -> c_1() 919.41/297.15 , -^#(#(), x) -> c_12() 919.41/297.15 , not^#(false()) -> c_15() 919.41/297.15 , not^#(true()) -> c_16() 919.41/297.15 , and^#(x, false()) -> c_17() 919.41/297.15 , ge^#(x, #()) -> c_21() 919.41/297.15 , ge^#(#(), 1(x)) -> c_25() 919.41/297.15 , bs^#(l(x)) -> c_34() 919.41/297.15 , size^#(l(x)) -> c_36() 919.41/297.15 , wb^#(l(x)) -> c_38() } 919.41/297.15 Obligation: 919.41/297.15 runtime complexity 919.41/297.15 Answer: 919.41/297.15 MAYBE 919.41/297.15 919.41/297.15 We estimate the number of application of {3,7,9,12,17} by 919.41/297.15 applications of Pre({3,7,9,12,17}) = 919.41/297.15 {1,2,4,5,6,8,10,11,13,14,15,16,19,20,21,22,23,25,28}. Here rules 919.41/297.15 are labeled as follows: 919.41/297.15 919.41/297.15 DPs: 919.41/297.15 { 1: +^#(x, #()) -> c_2(x) 919.41/297.15 , 2: +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z)) 919.41/297.15 , 3: +^#(0(x), 0(y)) -> c_4(0^#(+(x, y))) 919.41/297.15 , 4: +^#(0(x), 1(y)) -> c_5(+^#(x, y)) 919.41/297.15 , 5: +^#(#(), x) -> c_6(x) 919.41/297.15 , 6: +^#(1(x), 0(y)) -> c_7(+^#(x, y)) 919.41/297.15 , 7: +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) 919.41/297.15 , 8: -^#(x, #()) -> c_9(x) 919.41/297.15 , 9: -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) 919.41/297.15 , 10: -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) 919.41/297.15 , 11: -^#(1(x), 0(y)) -> c_13(-^#(x, y)) 919.41/297.15 , 12: -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) 919.41/297.15 , 13: and^#(x, true()) -> c_18(x) 919.41/297.15 , 14: if^#(false(), x, y) -> c_19(y) 919.41/297.15 , 15: if^#(true(), x, y) -> c_20(x) 919.41/297.15 , 16: ge^#(0(x), 0(y)) -> c_22(ge^#(x, y)) 919.41/297.15 , 17: ge^#(0(x), 1(y)) -> c_23(not^#(ge(y, x))) 919.41/297.15 , 18: ge^#(#(), 0(x)) -> c_24(ge^#(#(), x)) 919.41/297.15 , 19: ge^#(1(x), 0(y)) -> c_26(ge^#(x, y)) 919.41/297.15 , 20: ge^#(1(x), 1(y)) -> c_27(ge^#(x, y)) 919.41/297.15 , 21: val^#(l(x)) -> c_28(x) 919.41/297.15 , 22: val^#(n(x, y, z)) -> c_29(x) 919.41/297.15 , 23: min^#(l(x)) -> c_30(x) 919.41/297.15 , 24: min^#(n(x, y, z)) -> c_31(min^#(y)) 919.41/297.15 , 25: max^#(l(x)) -> c_32(x) 919.41/297.15 , 26: max^#(n(x, y, z)) -> c_33(max^#(z)) 919.41/297.15 , 27: bs^#(n(x, y, z)) -> 919.41/297.15 c_35(and^#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))) 919.41/297.15 , 28: size^#(n(x, y, z)) -> c_37(+^#(+(size(x), size(y)), 1(#()))) 919.41/297.15 , 29: wb^#(n(x, y, z)) -> 919.41/297.15 c_39(and^#(if(ge(size(y), size(z)), 919.41/297.15 ge(1(#()), -(size(y), size(z))), 919.41/297.15 ge(1(#()), -(size(z), size(y)))), 919.41/297.15 and(wb(y), wb(z)))) 919.41/297.15 , 30: 0^#(#()) -> c_1() 919.41/297.15 , 31: -^#(#(), x) -> c_12() 919.41/297.15 , 32: not^#(false()) -> c_15() 919.41/297.15 , 33: not^#(true()) -> c_16() 919.41/297.15 , 34: and^#(x, false()) -> c_17() 919.41/297.15 , 35: ge^#(x, #()) -> c_21() 919.41/297.15 , 36: ge^#(#(), 1(x)) -> c_25() 919.41/297.15 , 37: bs^#(l(x)) -> c_34() 919.41/297.15 , 38: size^#(l(x)) -> c_36() 919.41/297.15 , 39: wb^#(l(x)) -> c_38() } 919.41/297.15 919.41/297.15 We are left with following problem, upon which TcT provides the 919.41/297.15 certificate MAYBE. 919.41/297.15 919.41/297.15 Strict DPs: 919.41/297.15 { +^#(x, #()) -> c_2(x) 919.41/297.15 , +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z)) 919.41/297.15 , +^#(0(x), 1(y)) -> c_5(+^#(x, y)) 919.41/297.15 , +^#(#(), x) -> c_6(x) 919.41/297.15 , +^#(1(x), 0(y)) -> c_7(+^#(x, y)) 919.41/297.15 , -^#(x, #()) -> c_9(x) 919.41/297.15 , -^#(0(x), 1(y)) -> c_11(-^#(-(x, y), 1(#()))) 919.41/297.15 , -^#(1(x), 0(y)) -> c_13(-^#(x, y)) 919.41/297.15 , and^#(x, true()) -> c_18(x) 919.41/297.15 , if^#(false(), x, y) -> c_19(y) 919.41/297.15 , if^#(true(), x, y) -> c_20(x) 919.41/297.15 , ge^#(0(x), 0(y)) -> c_22(ge^#(x, y)) 919.41/297.15 , ge^#(#(), 0(x)) -> c_24(ge^#(#(), x)) 919.41/297.15 , ge^#(1(x), 0(y)) -> c_26(ge^#(x, y)) 919.41/297.15 , ge^#(1(x), 1(y)) -> c_27(ge^#(x, y)) 919.41/297.15 , val^#(l(x)) -> c_28(x) 919.41/297.15 , val^#(n(x, y, z)) -> c_29(x) 919.41/297.15 , min^#(l(x)) -> c_30(x) 919.41/297.15 , min^#(n(x, y, z)) -> c_31(min^#(y)) 919.41/297.15 , max^#(l(x)) -> c_32(x) 919.41/297.15 , max^#(n(x, y, z)) -> c_33(max^#(z)) 919.41/297.15 , bs^#(n(x, y, z)) -> 919.41/297.15 c_35(and^#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))) 919.41/297.15 , size^#(n(x, y, z)) -> c_37(+^#(+(size(x), size(y)), 1(#()))) 919.41/297.15 , wb^#(n(x, y, z)) -> 919.41/297.15 c_39(and^#(if(ge(size(y), size(z)), 919.41/297.15 ge(1(#()), -(size(y), size(z))), 919.41/297.15 ge(1(#()), -(size(z), size(y)))), 919.41/297.15 and(wb(y), wb(z)))) } 919.41/297.15 Strict Trs: 919.41/297.15 { 0(#()) -> #() 919.41/297.15 , +(x, #()) -> x 919.41/297.15 , +(x, +(y, z)) -> +(+(x, y), z) 919.41/297.15 , +(0(x), 0(y)) -> 0(+(x, y)) 919.41/297.15 , +(0(x), 1(y)) -> 1(+(x, y)) 919.41/297.15 , +(#(), x) -> x 919.41/297.15 , +(1(x), 0(y)) -> 1(+(x, y)) 919.41/297.15 , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) 919.41/297.15 , -(x, #()) -> x 919.41/297.15 , -(0(x), 0(y)) -> 0(-(x, y)) 919.41/297.15 , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) 919.41/297.15 , -(#(), x) -> #() 919.41/297.15 , -(1(x), 0(y)) -> 1(-(x, y)) 919.41/297.15 , -(1(x), 1(y)) -> 0(-(x, y)) 919.41/297.15 , not(false()) -> true() 919.41/297.15 , not(true()) -> false() 919.41/297.15 , and(x, false()) -> false() 919.41/297.15 , and(x, true()) -> x 919.41/297.15 , if(false(), x, y) -> y 919.41/297.15 , if(true(), x, y) -> x 919.41/297.15 , ge(x, #()) -> true() 919.41/297.15 , ge(0(x), 0(y)) -> ge(x, y) 919.41/297.15 , ge(0(x), 1(y)) -> not(ge(y, x)) 919.41/297.15 , ge(#(), 0(x)) -> ge(#(), x) 919.41/297.15 , ge(#(), 1(x)) -> false() 919.41/297.15 , ge(1(x), 0(y)) -> ge(x, y) 919.41/297.15 , ge(1(x), 1(y)) -> ge(x, y) 919.41/297.15 , val(l(x)) -> x 919.41/297.15 , val(n(x, y, z)) -> x 919.41/297.15 , min(l(x)) -> x 919.41/297.15 , min(n(x, y, z)) -> min(y) 919.41/297.15 , max(l(x)) -> x 919.41/297.15 , max(n(x, y, z)) -> max(z) 919.41/297.15 , bs(l(x)) -> true() 919.41/297.15 , bs(n(x, y, z)) -> 919.41/297.15 and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))) 919.41/297.15 , size(l(x)) -> 1(#()) 919.41/297.15 , size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())) 919.41/297.15 , wb(l(x)) -> true() 919.41/297.15 , wb(n(x, y, z)) -> 919.41/297.15 and(if(ge(size(y), size(z)), 919.41/297.15 ge(1(#()), -(size(y), size(z))), 919.41/297.15 ge(1(#()), -(size(z), size(y)))), 919.41/297.15 and(wb(y), wb(z))) } 919.41/297.15 Weak DPs: 919.41/297.15 { 0^#(#()) -> c_1() 919.41/297.15 , +^#(0(x), 0(y)) -> c_4(0^#(+(x, y))) 919.41/297.15 , +^#(1(x), 1(y)) -> c_8(0^#(+(+(x, y), 1(#())))) 919.41/297.15 , -^#(0(x), 0(y)) -> c_10(0^#(-(x, y))) 919.41/297.15 , -^#(#(), x) -> c_12() 919.41/297.15 , -^#(1(x), 1(y)) -> c_14(0^#(-(x, y))) 919.41/297.15 , not^#(false()) -> c_15() 919.41/297.15 , not^#(true()) -> c_16() 919.41/297.15 , and^#(x, false()) -> c_17() 919.41/297.15 , ge^#(x, #()) -> c_21() 919.41/297.15 , ge^#(0(x), 1(y)) -> c_23(not^#(ge(y, x))) 919.41/297.15 , ge^#(#(), 1(x)) -> c_25() 919.41/297.15 , bs^#(l(x)) -> c_34() 919.41/297.15 , size^#(l(x)) -> c_36() 919.41/297.15 , wb^#(l(x)) -> c_38() } 919.41/297.15 Obligation: 919.41/297.15 runtime complexity 919.41/297.15 Answer: 919.41/297.15 MAYBE 919.41/297.15 919.41/297.15 Empty strict component of the problem is NOT empty. 919.41/297.15 919.41/297.15 919.41/297.15 Arrrr.. 919.56/297.25 EOF