MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ O(0()) -> 0()
, +(x, 0()) -> x
, +(x, +(y, z)) -> +(+(x, y), z)
, +(O(x), O(y)) -> O(+(x, y))
, +(O(x), I(y)) -> I(+(x, y))
, +(0(), x) -> x
, +(I(x), O(y)) -> I(+(x, y))
, +(I(x), I(y)) -> O(+(+(x, y), I(0())))
, -(x, 0()) -> x
, -(O(x), O(y)) -> O(-(x, y))
, -(O(x), I(y)) -> I(-(-(x, y), I(1())))
, -(0(), x) -> 0()
, -(I(x), O(y)) -> I(-(x, y))
, -(I(x), I(y)) -> O(-(x, y))
, not(true()) -> false()
, not(false()) -> true()
, and(x, true()) -> x
, and(x, false()) -> false()
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, ge(x, 0()) -> true()
, ge(O(x), O(y)) -> ge(x, y)
, ge(O(x), I(y)) -> not(ge(y, x))
, ge(0(), O(x)) -> ge(0(), x)
, ge(0(), I(x)) -> false()
, ge(I(x), O(y)) -> ge(x, y)
, ge(I(x), I(y)) -> ge(x, y)
, Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0())
, Log'(0()) -> 0()
, Log'(I(x)) -> +(Log'(x), I(0()))
, Log(x) -> -(Log'(x), I(0()))
, Val(L(x)) -> x
, Val(N(x, l(), r())) -> x
, Min(L(x)) -> x
, Min(N(x, l(), r())) -> Min(l())
, Max(L(x)) -> x
, Max(N(x, l(), r())) -> Max(r())
, BS(L(x)) -> true()
, BS(N(x, l(), r())) ->
and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r())))
, Size(L(x)) -> I(0())
, Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1()))
, WB(L(x)) -> true()
, WB(N(x, l(), r())) ->
and(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r()))) }
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) '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
2) '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
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:
{ O^#(0()) -> c_1()
, +^#(x, 0()) -> c_2(x)
, +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z))
, +^#(O(x), O(y)) -> c_4(O^#(+(x, y)))
, +^#(O(x), I(y)) -> c_5(+^#(x, y))
, +^#(0(), x) -> c_6(x)
, +^#(I(x), O(y)) -> c_7(+^#(x, y))
, +^#(I(x), I(y)) -> c_8(O^#(+(+(x, y), I(0()))))
, -^#(x, 0()) -> c_9(x)
, -^#(O(x), O(y)) -> c_10(O^#(-(x, y)))
, -^#(O(x), I(y)) -> c_11(-^#(-(x, y), I(1())))
, -^#(0(), x) -> c_12()
, -^#(I(x), O(y)) -> c_13(-^#(x, y))
, -^#(I(x), I(y)) -> c_14(O^#(-(x, y)))
, not^#(true()) -> c_15()
, not^#(false()) -> c_16()
, and^#(x, true()) -> c_17(x)
, and^#(x, false()) -> c_18()
, if^#(true(), x, y) -> c_19(x)
, if^#(false(), x, y) -> c_20(y)
, ge^#(x, 0()) -> c_21()
, ge^#(O(x), O(y)) -> c_22(ge^#(x, y))
, ge^#(O(x), I(y)) -> c_23(not^#(ge(y, x)))
, ge^#(0(), O(x)) -> c_24(ge^#(0(), x))
, ge^#(0(), I(x)) -> c_25()
, ge^#(I(x), O(y)) -> c_26(ge^#(x, y))
, ge^#(I(x), I(y)) -> c_27(ge^#(x, y))
, Log'^#(O(x)) ->
c_28(if^#(ge(x, I(0())), +(Log'(x), I(0())), 0()))
, Log'^#(0()) -> c_29()
, Log'^#(I(x)) -> c_30(+^#(Log'(x), I(0())))
, Log^#(x) -> c_31(-^#(Log'(x), I(0())))
, Val^#(L(x)) -> c_32(x)
, Val^#(N(x, l(), r())) -> c_33(x)
, Min^#(L(x)) -> c_34(x)
, Min^#(N(x, l(), r())) -> c_35(Min^#(l()))
, Max^#(L(x)) -> c_36(x)
, Max^#(N(x, l(), r())) -> c_37(Max^#(r()))
, BS^#(L(x)) -> c_38()
, BS^#(N(x, l(), r())) ->
c_39(and^#(and(ge(x, Max(l())), ge(Min(r()), x)),
and(BS(l()), BS(r()))))
, Size^#(L(x)) -> c_40()
, Size^#(N(x, l(), r())) ->
c_41(+^#(+(Size(l()), Size(r())), I(1())))
, WB^#(L(x)) -> c_42()
, WB^#(N(x, l(), r())) ->
c_43(and^#(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r())))) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ O^#(0()) -> c_1()
, +^#(x, 0()) -> c_2(x)
, +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z))
, +^#(O(x), O(y)) -> c_4(O^#(+(x, y)))
, +^#(O(x), I(y)) -> c_5(+^#(x, y))
, +^#(0(), x) -> c_6(x)
, +^#(I(x), O(y)) -> c_7(+^#(x, y))
, +^#(I(x), I(y)) -> c_8(O^#(+(+(x, y), I(0()))))
, -^#(x, 0()) -> c_9(x)
, -^#(O(x), O(y)) -> c_10(O^#(-(x, y)))
, -^#(O(x), I(y)) -> c_11(-^#(-(x, y), I(1())))
, -^#(0(), x) -> c_12()
, -^#(I(x), O(y)) -> c_13(-^#(x, y))
, -^#(I(x), I(y)) -> c_14(O^#(-(x, y)))
, not^#(true()) -> c_15()
, not^#(false()) -> c_16()
, and^#(x, true()) -> c_17(x)
, and^#(x, false()) -> c_18()
, if^#(true(), x, y) -> c_19(x)
, if^#(false(), x, y) -> c_20(y)
, ge^#(x, 0()) -> c_21()
, ge^#(O(x), O(y)) -> c_22(ge^#(x, y))
, ge^#(O(x), I(y)) -> c_23(not^#(ge(y, x)))
, ge^#(0(), O(x)) -> c_24(ge^#(0(), x))
, ge^#(0(), I(x)) -> c_25()
, ge^#(I(x), O(y)) -> c_26(ge^#(x, y))
, ge^#(I(x), I(y)) -> c_27(ge^#(x, y))
, Log'^#(O(x)) ->
c_28(if^#(ge(x, I(0())), +(Log'(x), I(0())), 0()))
, Log'^#(0()) -> c_29()
, Log'^#(I(x)) -> c_30(+^#(Log'(x), I(0())))
, Log^#(x) -> c_31(-^#(Log'(x), I(0())))
, Val^#(L(x)) -> c_32(x)
, Val^#(N(x, l(), r())) -> c_33(x)
, Min^#(L(x)) -> c_34(x)
, Min^#(N(x, l(), r())) -> c_35(Min^#(l()))
, Max^#(L(x)) -> c_36(x)
, Max^#(N(x, l(), r())) -> c_37(Max^#(r()))
, BS^#(L(x)) -> c_38()
, BS^#(N(x, l(), r())) ->
c_39(and^#(and(ge(x, Max(l())), ge(Min(r()), x)),
and(BS(l()), BS(r()))))
, Size^#(L(x)) -> c_40()
, Size^#(N(x, l(), r())) ->
c_41(+^#(+(Size(l()), Size(r())), I(1())))
, WB^#(L(x)) -> c_42()
, WB^#(N(x, l(), r())) ->
c_43(and^#(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r())))) }
Strict Trs:
{ O(0()) -> 0()
, +(x, 0()) -> x
, +(x, +(y, z)) -> +(+(x, y), z)
, +(O(x), O(y)) -> O(+(x, y))
, +(O(x), I(y)) -> I(+(x, y))
, +(0(), x) -> x
, +(I(x), O(y)) -> I(+(x, y))
, +(I(x), I(y)) -> O(+(+(x, y), I(0())))
, -(x, 0()) -> x
, -(O(x), O(y)) -> O(-(x, y))
, -(O(x), I(y)) -> I(-(-(x, y), I(1())))
, -(0(), x) -> 0()
, -(I(x), O(y)) -> I(-(x, y))
, -(I(x), I(y)) -> O(-(x, y))
, not(true()) -> false()
, not(false()) -> true()
, and(x, true()) -> x
, and(x, false()) -> false()
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, ge(x, 0()) -> true()
, ge(O(x), O(y)) -> ge(x, y)
, ge(O(x), I(y)) -> not(ge(y, x))
, ge(0(), O(x)) -> ge(0(), x)
, ge(0(), I(x)) -> false()
, ge(I(x), O(y)) -> ge(x, y)
, ge(I(x), I(y)) -> ge(x, y)
, Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0())
, Log'(0()) -> 0()
, Log'(I(x)) -> +(Log'(x), I(0()))
, Log(x) -> -(Log'(x), I(0()))
, Val(L(x)) -> x
, Val(N(x, l(), r())) -> x
, Min(L(x)) -> x
, Min(N(x, l(), r())) -> Min(l())
, Max(L(x)) -> x
, Max(N(x, l(), r())) -> Max(r())
, BS(L(x)) -> true()
, BS(N(x, l(), r())) ->
and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r())))
, Size(L(x)) -> I(0())
, Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1()))
, WB(L(x)) -> true()
, WB(N(x, l(), r())) ->
and(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r()))) }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of
{1,12,15,16,18,21,25,29,35,37,38,39,40,41,42,43} by applications of
Pre({1,12,15,16,18,21,25,29,35,37,38,39,40,41,42,43}) =
{2,4,6,8,9,10,11,13,14,17,19,20,22,23,24,26,27,31,32,33,34,36}.
Here rules are labeled as follows:
DPs:
{ 1: O^#(0()) -> c_1()
, 2: +^#(x, 0()) -> c_2(x)
, 3: +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z))
, 4: +^#(O(x), O(y)) -> c_4(O^#(+(x, y)))
, 5: +^#(O(x), I(y)) -> c_5(+^#(x, y))
, 6: +^#(0(), x) -> c_6(x)
, 7: +^#(I(x), O(y)) -> c_7(+^#(x, y))
, 8: +^#(I(x), I(y)) -> c_8(O^#(+(+(x, y), I(0()))))
, 9: -^#(x, 0()) -> c_9(x)
, 10: -^#(O(x), O(y)) -> c_10(O^#(-(x, y)))
, 11: -^#(O(x), I(y)) -> c_11(-^#(-(x, y), I(1())))
, 12: -^#(0(), x) -> c_12()
, 13: -^#(I(x), O(y)) -> c_13(-^#(x, y))
, 14: -^#(I(x), I(y)) -> c_14(O^#(-(x, y)))
, 15: not^#(true()) -> c_15()
, 16: not^#(false()) -> c_16()
, 17: and^#(x, true()) -> c_17(x)
, 18: and^#(x, false()) -> c_18()
, 19: if^#(true(), x, y) -> c_19(x)
, 20: if^#(false(), x, y) -> c_20(y)
, 21: ge^#(x, 0()) -> c_21()
, 22: ge^#(O(x), O(y)) -> c_22(ge^#(x, y))
, 23: ge^#(O(x), I(y)) -> c_23(not^#(ge(y, x)))
, 24: ge^#(0(), O(x)) -> c_24(ge^#(0(), x))
, 25: ge^#(0(), I(x)) -> c_25()
, 26: ge^#(I(x), O(y)) -> c_26(ge^#(x, y))
, 27: ge^#(I(x), I(y)) -> c_27(ge^#(x, y))
, 28: Log'^#(O(x)) ->
c_28(if^#(ge(x, I(0())), +(Log'(x), I(0())), 0()))
, 29: Log'^#(0()) -> c_29()
, 30: Log'^#(I(x)) -> c_30(+^#(Log'(x), I(0())))
, 31: Log^#(x) -> c_31(-^#(Log'(x), I(0())))
, 32: Val^#(L(x)) -> c_32(x)
, 33: Val^#(N(x, l(), r())) -> c_33(x)
, 34: Min^#(L(x)) -> c_34(x)
, 35: Min^#(N(x, l(), r())) -> c_35(Min^#(l()))
, 36: Max^#(L(x)) -> c_36(x)
, 37: Max^#(N(x, l(), r())) -> c_37(Max^#(r()))
, 38: BS^#(L(x)) -> c_38()
, 39: BS^#(N(x, l(), r())) ->
c_39(and^#(and(ge(x, Max(l())), ge(Min(r()), x)),
and(BS(l()), BS(r()))))
, 40: Size^#(L(x)) -> c_40()
, 41: Size^#(N(x, l(), r())) ->
c_41(+^#(+(Size(l()), Size(r())), I(1())))
, 42: WB^#(L(x)) -> c_42()
, 43: WB^#(N(x, l(), r())) ->
c_43(and^#(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r())))) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ +^#(x, 0()) -> c_2(x)
, +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z))
, +^#(O(x), O(y)) -> c_4(O^#(+(x, y)))
, +^#(O(x), I(y)) -> c_5(+^#(x, y))
, +^#(0(), x) -> c_6(x)
, +^#(I(x), O(y)) -> c_7(+^#(x, y))
, +^#(I(x), I(y)) -> c_8(O^#(+(+(x, y), I(0()))))
, -^#(x, 0()) -> c_9(x)
, -^#(O(x), O(y)) -> c_10(O^#(-(x, y)))
, -^#(O(x), I(y)) -> c_11(-^#(-(x, y), I(1())))
, -^#(I(x), O(y)) -> c_13(-^#(x, y))
, -^#(I(x), I(y)) -> c_14(O^#(-(x, y)))
, and^#(x, true()) -> c_17(x)
, if^#(true(), x, y) -> c_19(x)
, if^#(false(), x, y) -> c_20(y)
, ge^#(O(x), O(y)) -> c_22(ge^#(x, y))
, ge^#(O(x), I(y)) -> c_23(not^#(ge(y, x)))
, ge^#(0(), O(x)) -> c_24(ge^#(0(), x))
, ge^#(I(x), O(y)) -> c_26(ge^#(x, y))
, ge^#(I(x), I(y)) -> c_27(ge^#(x, y))
, Log'^#(O(x)) ->
c_28(if^#(ge(x, I(0())), +(Log'(x), I(0())), 0()))
, Log'^#(I(x)) -> c_30(+^#(Log'(x), I(0())))
, Log^#(x) -> c_31(-^#(Log'(x), I(0())))
, Val^#(L(x)) -> c_32(x)
, Val^#(N(x, l(), r())) -> c_33(x)
, Min^#(L(x)) -> c_34(x)
, Max^#(L(x)) -> c_36(x) }
Strict Trs:
{ O(0()) -> 0()
, +(x, 0()) -> x
, +(x, +(y, z)) -> +(+(x, y), z)
, +(O(x), O(y)) -> O(+(x, y))
, +(O(x), I(y)) -> I(+(x, y))
, +(0(), x) -> x
, +(I(x), O(y)) -> I(+(x, y))
, +(I(x), I(y)) -> O(+(+(x, y), I(0())))
, -(x, 0()) -> x
, -(O(x), O(y)) -> O(-(x, y))
, -(O(x), I(y)) -> I(-(-(x, y), I(1())))
, -(0(), x) -> 0()
, -(I(x), O(y)) -> I(-(x, y))
, -(I(x), I(y)) -> O(-(x, y))
, not(true()) -> false()
, not(false()) -> true()
, and(x, true()) -> x
, and(x, false()) -> false()
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, ge(x, 0()) -> true()
, ge(O(x), O(y)) -> ge(x, y)
, ge(O(x), I(y)) -> not(ge(y, x))
, ge(0(), O(x)) -> ge(0(), x)
, ge(0(), I(x)) -> false()
, ge(I(x), O(y)) -> ge(x, y)
, ge(I(x), I(y)) -> ge(x, y)
, Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0())
, Log'(0()) -> 0()
, Log'(I(x)) -> +(Log'(x), I(0()))
, Log(x) -> -(Log'(x), I(0()))
, Val(L(x)) -> x
, Val(N(x, l(), r())) -> x
, Min(L(x)) -> x
, Min(N(x, l(), r())) -> Min(l())
, Max(L(x)) -> x
, Max(N(x, l(), r())) -> Max(r())
, BS(L(x)) -> true()
, BS(N(x, l(), r())) ->
and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r())))
, Size(L(x)) -> I(0())
, Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1()))
, WB(L(x)) -> true()
, WB(N(x, l(), r())) ->
and(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r()))) }
Weak DPs:
{ O^#(0()) -> c_1()
, -^#(0(), x) -> c_12()
, not^#(true()) -> c_15()
, not^#(false()) -> c_16()
, and^#(x, false()) -> c_18()
, ge^#(x, 0()) -> c_21()
, ge^#(0(), I(x)) -> c_25()
, Log'^#(0()) -> c_29()
, Min^#(N(x, l(), r())) -> c_35(Min^#(l()))
, Max^#(N(x, l(), r())) -> c_37(Max^#(r()))
, BS^#(L(x)) -> c_38()
, BS^#(N(x, l(), r())) ->
c_39(and^#(and(ge(x, Max(l())), ge(Min(r()), x)),
and(BS(l()), BS(r()))))
, Size^#(L(x)) -> c_40()
, Size^#(N(x, l(), r())) ->
c_41(+^#(+(Size(l()), Size(r())), I(1())))
, WB^#(L(x)) -> c_42()
, WB^#(N(x, l(), r())) ->
c_43(and^#(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r())))) }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {3,7,9,12,17} by
applications of Pre({3,7,9,12,17}) =
{1,2,4,5,6,8,10,11,13,14,15,16,19,20,22,23,24,25,26,27}. Here rules
are labeled as follows:
DPs:
{ 1: +^#(x, 0()) -> c_2(x)
, 2: +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z))
, 3: +^#(O(x), O(y)) -> c_4(O^#(+(x, y)))
, 4: +^#(O(x), I(y)) -> c_5(+^#(x, y))
, 5: +^#(0(), x) -> c_6(x)
, 6: +^#(I(x), O(y)) -> c_7(+^#(x, y))
, 7: +^#(I(x), I(y)) -> c_8(O^#(+(+(x, y), I(0()))))
, 8: -^#(x, 0()) -> c_9(x)
, 9: -^#(O(x), O(y)) -> c_10(O^#(-(x, y)))
, 10: -^#(O(x), I(y)) -> c_11(-^#(-(x, y), I(1())))
, 11: -^#(I(x), O(y)) -> c_13(-^#(x, y))
, 12: -^#(I(x), I(y)) -> c_14(O^#(-(x, y)))
, 13: and^#(x, true()) -> c_17(x)
, 14: if^#(true(), x, y) -> c_19(x)
, 15: if^#(false(), x, y) -> c_20(y)
, 16: ge^#(O(x), O(y)) -> c_22(ge^#(x, y))
, 17: ge^#(O(x), I(y)) -> c_23(not^#(ge(y, x)))
, 18: ge^#(0(), O(x)) -> c_24(ge^#(0(), x))
, 19: ge^#(I(x), O(y)) -> c_26(ge^#(x, y))
, 20: ge^#(I(x), I(y)) -> c_27(ge^#(x, y))
, 21: Log'^#(O(x)) ->
c_28(if^#(ge(x, I(0())), +(Log'(x), I(0())), 0()))
, 22: Log'^#(I(x)) -> c_30(+^#(Log'(x), I(0())))
, 23: Log^#(x) -> c_31(-^#(Log'(x), I(0())))
, 24: Val^#(L(x)) -> c_32(x)
, 25: Val^#(N(x, l(), r())) -> c_33(x)
, 26: Min^#(L(x)) -> c_34(x)
, 27: Max^#(L(x)) -> c_36(x)
, 28: O^#(0()) -> c_1()
, 29: -^#(0(), x) -> c_12()
, 30: not^#(true()) -> c_15()
, 31: not^#(false()) -> c_16()
, 32: and^#(x, false()) -> c_18()
, 33: ge^#(x, 0()) -> c_21()
, 34: ge^#(0(), I(x)) -> c_25()
, 35: Log'^#(0()) -> c_29()
, 36: Min^#(N(x, l(), r())) -> c_35(Min^#(l()))
, 37: Max^#(N(x, l(), r())) -> c_37(Max^#(r()))
, 38: BS^#(L(x)) -> c_38()
, 39: BS^#(N(x, l(), r())) ->
c_39(and^#(and(ge(x, Max(l())), ge(Min(r()), x)),
and(BS(l()), BS(r()))))
, 40: Size^#(L(x)) -> c_40()
, 41: Size^#(N(x, l(), r())) ->
c_41(+^#(+(Size(l()), Size(r())), I(1())))
, 42: WB^#(L(x)) -> c_42()
, 43: WB^#(N(x, l(), r())) ->
c_43(and^#(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r())))) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ +^#(x, 0()) -> c_2(x)
, +^#(x, +(y, z)) -> c_3(+^#(+(x, y), z))
, +^#(O(x), I(y)) -> c_5(+^#(x, y))
, +^#(0(), x) -> c_6(x)
, +^#(I(x), O(y)) -> c_7(+^#(x, y))
, -^#(x, 0()) -> c_9(x)
, -^#(O(x), I(y)) -> c_11(-^#(-(x, y), I(1())))
, -^#(I(x), O(y)) -> c_13(-^#(x, y))
, and^#(x, true()) -> c_17(x)
, if^#(true(), x, y) -> c_19(x)
, if^#(false(), x, y) -> c_20(y)
, ge^#(O(x), O(y)) -> c_22(ge^#(x, y))
, ge^#(0(), O(x)) -> c_24(ge^#(0(), x))
, ge^#(I(x), O(y)) -> c_26(ge^#(x, y))
, ge^#(I(x), I(y)) -> c_27(ge^#(x, y))
, Log'^#(O(x)) ->
c_28(if^#(ge(x, I(0())), +(Log'(x), I(0())), 0()))
, Log'^#(I(x)) -> c_30(+^#(Log'(x), I(0())))
, Log^#(x) -> c_31(-^#(Log'(x), I(0())))
, Val^#(L(x)) -> c_32(x)
, Val^#(N(x, l(), r())) -> c_33(x)
, Min^#(L(x)) -> c_34(x)
, Max^#(L(x)) -> c_36(x) }
Strict Trs:
{ O(0()) -> 0()
, +(x, 0()) -> x
, +(x, +(y, z)) -> +(+(x, y), z)
, +(O(x), O(y)) -> O(+(x, y))
, +(O(x), I(y)) -> I(+(x, y))
, +(0(), x) -> x
, +(I(x), O(y)) -> I(+(x, y))
, +(I(x), I(y)) -> O(+(+(x, y), I(0())))
, -(x, 0()) -> x
, -(O(x), O(y)) -> O(-(x, y))
, -(O(x), I(y)) -> I(-(-(x, y), I(1())))
, -(0(), x) -> 0()
, -(I(x), O(y)) -> I(-(x, y))
, -(I(x), I(y)) -> O(-(x, y))
, not(true()) -> false()
, not(false()) -> true()
, and(x, true()) -> x
, and(x, false()) -> false()
, if(true(), x, y) -> x
, if(false(), x, y) -> y
, ge(x, 0()) -> true()
, ge(O(x), O(y)) -> ge(x, y)
, ge(O(x), I(y)) -> not(ge(y, x))
, ge(0(), O(x)) -> ge(0(), x)
, ge(0(), I(x)) -> false()
, ge(I(x), O(y)) -> ge(x, y)
, ge(I(x), I(y)) -> ge(x, y)
, Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0())
, Log'(0()) -> 0()
, Log'(I(x)) -> +(Log'(x), I(0()))
, Log(x) -> -(Log'(x), I(0()))
, Val(L(x)) -> x
, Val(N(x, l(), r())) -> x
, Min(L(x)) -> x
, Min(N(x, l(), r())) -> Min(l())
, Max(L(x)) -> x
, Max(N(x, l(), r())) -> Max(r())
, BS(L(x)) -> true()
, BS(N(x, l(), r())) ->
and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r())))
, Size(L(x)) -> I(0())
, Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1()))
, WB(L(x)) -> true()
, WB(N(x, l(), r())) ->
and(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r()))) }
Weak DPs:
{ O^#(0()) -> c_1()
, +^#(O(x), O(y)) -> c_4(O^#(+(x, y)))
, +^#(I(x), I(y)) -> c_8(O^#(+(+(x, y), I(0()))))
, -^#(O(x), O(y)) -> c_10(O^#(-(x, y)))
, -^#(0(), x) -> c_12()
, -^#(I(x), I(y)) -> c_14(O^#(-(x, y)))
, not^#(true()) -> c_15()
, not^#(false()) -> c_16()
, and^#(x, false()) -> c_18()
, ge^#(x, 0()) -> c_21()
, ge^#(O(x), I(y)) -> c_23(not^#(ge(y, x)))
, ge^#(0(), I(x)) -> c_25()
, Log'^#(0()) -> c_29()
, Min^#(N(x, l(), r())) -> c_35(Min^#(l()))
, Max^#(N(x, l(), r())) -> c_37(Max^#(r()))
, BS^#(L(x)) -> c_38()
, BS^#(N(x, l(), r())) ->
c_39(and^#(and(ge(x, Max(l())), ge(Min(r()), x)),
and(BS(l()), BS(r()))))
, Size^#(L(x)) -> c_40()
, Size^#(N(x, l(), r())) ->
c_41(+^#(+(Size(l()), Size(r())), I(1())))
, WB^#(L(x)) -> c_42()
, WB^#(N(x, l(), r())) ->
c_43(and^#(if(ge(Size(l()), Size(r())),
ge(I(0()), -(Size(l()), Size(r()))),
ge(I(0()), -(Size(r()), Size(l())))),
and(WB(l()), WB(r())))) }
Obligation:
runtime complexity
Answer:
MAYBE
Empty strict component of the problem is NOT empty.
Arrrr..