YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ a__minus(X1, X2) -> minus(X1, X2)
, a__minus(0(), Y) -> 0()
, a__minus(s(X), s(Y)) -> a__minus(X, Y)
, a__geq(X1, X2) -> geq(X1, X2)
, a__geq(X, 0()) -> true()
, a__geq(0(), s(Y)) -> false()
, a__geq(s(X), s(Y)) -> a__geq(X, Y)
, a__div(X1, X2) -> div(X1, X2)
, a__div(0(), s(Y)) -> 0()
, a__div(s(X), s(Y)) ->
a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, a__if(X1, X2, X3) -> if(X1, X2, X3)
, a__if(true(), X, Y) -> mark(X)
, a__if(false(), X, Y) -> mark(Y)
, mark(0()) -> 0()
, mark(s(X)) -> s(mark(X))
, mark(true()) -> true()
, mark(false()) -> false()
, mark(div(X1, X2)) -> a__div(mark(X1), X2)
, mark(minus(X1, X2)) -> a__minus(X1, X2)
, mark(geq(X1, X2)) -> a__geq(X1, X2)
, mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We add following dependency tuples:
Strict DPs:
{ a__minus^#(X1, X2) -> c_1()
, a__minus^#(0(), Y) -> c_2()
, a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y))
, a__geq^#(X1, X2) -> c_4()
, a__geq^#(X, 0()) -> c_5()
, a__geq^#(0(), s(Y)) -> c_6()
, a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y))
, a__div^#(X1, X2) -> c_8()
, a__div^#(0(), s(Y)) -> c_9()
, a__div^#(s(X), s(Y)) ->
c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()),
a__geq^#(X, Y))
, a__if^#(X1, X2, X3) -> c_11()
, a__if^#(true(), X, Y) -> c_12(mark^#(X))
, a__if^#(false(), X, Y) -> c_13(mark^#(Y))
, mark^#(0()) -> c_14()
, mark^#(s(X)) -> c_15(mark^#(X))
, mark^#(true()) -> c_16()
, mark^#(false()) -> c_17()
, mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1))
, mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2))
, mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2))
, mark^#(if(X1, X2, X3)) ->
c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ a__minus^#(X1, X2) -> c_1()
, a__minus^#(0(), Y) -> c_2()
, a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y))
, a__geq^#(X1, X2) -> c_4()
, a__geq^#(X, 0()) -> c_5()
, a__geq^#(0(), s(Y)) -> c_6()
, a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y))
, a__div^#(X1, X2) -> c_8()
, a__div^#(0(), s(Y)) -> c_9()
, a__div^#(s(X), s(Y)) ->
c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()),
a__geq^#(X, Y))
, a__if^#(X1, X2, X3) -> c_11()
, a__if^#(true(), X, Y) -> c_12(mark^#(X))
, a__if^#(false(), X, Y) -> c_13(mark^#(Y))
, mark^#(0()) -> c_14()
, mark^#(s(X)) -> c_15(mark^#(X))
, mark^#(true()) -> c_16()
, mark^#(false()) -> c_17()
, mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1))
, mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2))
, mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2))
, mark^#(if(X1, X2, X3)) ->
c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) }
Weak Trs:
{ a__minus(X1, X2) -> minus(X1, X2)
, a__minus(0(), Y) -> 0()
, a__minus(s(X), s(Y)) -> a__minus(X, Y)
, a__geq(X1, X2) -> geq(X1, X2)
, a__geq(X, 0()) -> true()
, a__geq(0(), s(Y)) -> false()
, a__geq(s(X), s(Y)) -> a__geq(X, Y)
, a__div(X1, X2) -> div(X1, X2)
, a__div(0(), s(Y)) -> 0()
, a__div(s(X), s(Y)) ->
a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, a__if(X1, X2, X3) -> if(X1, X2, X3)
, a__if(true(), X, Y) -> mark(X)
, a__if(false(), X, Y) -> mark(Y)
, mark(0()) -> 0()
, mark(s(X)) -> s(mark(X))
, mark(true()) -> true()
, mark(false()) -> false()
, mark(div(X1, X2)) -> a__div(mark(X1), X2)
, mark(minus(X1, X2)) -> a__minus(X1, X2)
, mark(geq(X1, X2)) -> a__geq(X1, X2)
, mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We estimate the number of application of
{1,2,4,5,6,8,9,11,14,16,17} by applications of
Pre({1,2,4,5,6,8,9,11,14,16,17}) = {3,7,10,12,13,15,18,19,20,21}.
Here rules are labeled as follows:
DPs:
{ 1: a__minus^#(X1, X2) -> c_1()
, 2: a__minus^#(0(), Y) -> c_2()
, 3: a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y))
, 4: a__geq^#(X1, X2) -> c_4()
, 5: a__geq^#(X, 0()) -> c_5()
, 6: a__geq^#(0(), s(Y)) -> c_6()
, 7: a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y))
, 8: a__div^#(X1, X2) -> c_8()
, 9: a__div^#(0(), s(Y)) -> c_9()
, 10: a__div^#(s(X), s(Y)) ->
c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()),
a__geq^#(X, Y))
, 11: a__if^#(X1, X2, X3) -> c_11()
, 12: a__if^#(true(), X, Y) -> c_12(mark^#(X))
, 13: a__if^#(false(), X, Y) -> c_13(mark^#(Y))
, 14: mark^#(0()) -> c_14()
, 15: mark^#(s(X)) -> c_15(mark^#(X))
, 16: mark^#(true()) -> c_16()
, 17: mark^#(false()) -> c_17()
, 18: mark^#(div(X1, X2)) ->
c_18(a__div^#(mark(X1), X2), mark^#(X1))
, 19: mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2))
, 20: mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2))
, 21: mark^#(if(X1, X2, X3)) ->
c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y))
, a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y))
, a__div^#(s(X), s(Y)) ->
c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()),
a__geq^#(X, Y))
, a__if^#(true(), X, Y) -> c_12(mark^#(X))
, a__if^#(false(), X, Y) -> c_13(mark^#(Y))
, mark^#(s(X)) -> c_15(mark^#(X))
, mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1))
, mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2))
, mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2))
, mark^#(if(X1, X2, X3)) ->
c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) }
Weak DPs:
{ a__minus^#(X1, X2) -> c_1()
, a__minus^#(0(), Y) -> c_2()
, a__geq^#(X1, X2) -> c_4()
, a__geq^#(X, 0()) -> c_5()
, a__geq^#(0(), s(Y)) -> c_6()
, a__div^#(X1, X2) -> c_8()
, a__div^#(0(), s(Y)) -> c_9()
, a__if^#(X1, X2, X3) -> c_11()
, mark^#(0()) -> c_14()
, mark^#(true()) -> c_16()
, mark^#(false()) -> c_17() }
Weak Trs:
{ a__minus(X1, X2) -> minus(X1, X2)
, a__minus(0(), Y) -> 0()
, a__minus(s(X), s(Y)) -> a__minus(X, Y)
, a__geq(X1, X2) -> geq(X1, X2)
, a__geq(X, 0()) -> true()
, a__geq(0(), s(Y)) -> false()
, a__geq(s(X), s(Y)) -> a__geq(X, Y)
, a__div(X1, X2) -> div(X1, X2)
, a__div(0(), s(Y)) -> 0()
, a__div(s(X), s(Y)) ->
a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, a__if(X1, X2, X3) -> if(X1, X2, X3)
, a__if(true(), X, Y) -> mark(X)
, a__if(false(), X, Y) -> mark(Y)
, mark(0()) -> 0()
, mark(s(X)) -> s(mark(X))
, mark(true()) -> true()
, mark(false()) -> false()
, mark(div(X1, X2)) -> a__div(mark(X1), X2)
, mark(minus(X1, X2)) -> a__minus(X1, X2)
, mark(geq(X1, X2)) -> a__geq(X1, X2)
, mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ a__minus^#(X1, X2) -> c_1()
, a__minus^#(0(), Y) -> c_2()
, a__geq^#(X1, X2) -> c_4()
, a__geq^#(X, 0()) -> c_5()
, a__geq^#(0(), s(Y)) -> c_6()
, a__div^#(X1, X2) -> c_8()
, a__div^#(0(), s(Y)) -> c_9()
, a__if^#(X1, X2, X3) -> c_11()
, mark^#(0()) -> c_14()
, mark^#(true()) -> c_16()
, mark^#(false()) -> c_17() }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ a__minus^#(s(X), s(Y)) -> c_3(a__minus^#(X, Y))
, a__geq^#(s(X), s(Y)) -> c_7(a__geq^#(X, Y))
, a__div^#(s(X), s(Y)) ->
c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()),
a__geq^#(X, Y))
, a__if^#(true(), X, Y) -> c_12(mark^#(X))
, a__if^#(false(), X, Y) -> c_13(mark^#(Y))
, mark^#(s(X)) -> c_15(mark^#(X))
, mark^#(div(X1, X2)) -> c_18(a__div^#(mark(X1), X2), mark^#(X1))
, mark^#(minus(X1, X2)) -> c_19(a__minus^#(X1, X2))
, mark^#(geq(X1, X2)) -> c_20(a__geq^#(X1, X2))
, mark^#(if(X1, X2, X3)) ->
c_21(a__if^#(mark(X1), X2, X3), mark^#(X1)) }
Weak Trs:
{ a__minus(X1, X2) -> minus(X1, X2)
, a__minus(0(), Y) -> 0()
, a__minus(s(X), s(Y)) -> a__minus(X, Y)
, a__geq(X1, X2) -> geq(X1, X2)
, a__geq(X, 0()) -> true()
, a__geq(0(), s(Y)) -> false()
, a__geq(s(X), s(Y)) -> a__geq(X, Y)
, a__div(X1, X2) -> div(X1, X2)
, a__div(0(), s(Y)) -> 0()
, a__div(s(X), s(Y)) ->
a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, a__if(X1, X2, X3) -> if(X1, X2, X3)
, a__if(true(), X, Y) -> mark(X)
, a__if(false(), X, Y) -> mark(Y)
, mark(0()) -> 0()
, mark(s(X)) -> s(mark(X))
, mark(true()) -> true()
, mark(false()) -> false()
, mark(div(X1, X2)) -> a__div(mark(X1), X2)
, mark(minus(X1, X2)) -> a__minus(X1, X2)
, mark(geq(X1, X2)) -> a__geq(X1, X2)
, mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following argument positions are usable:
Uargs(c_3) = {1}, Uargs(c_7) = {1}, Uargs(c_10) = {1, 2},
Uargs(c_12) = {1}, Uargs(c_13) = {1}, Uargs(c_15) = {1},
Uargs(c_18) = {1, 2}, Uargs(c_19) = {1}, Uargs(c_20) = {1},
Uargs(c_21) = {1, 2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[a__minus](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[0] = [0]
[0]
[s](x1) = [1 0] x1 + [0]
[0 1] [2]
[a__geq](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[true] = [0]
[0]
[false] = [0]
[0]
[a__div](x1, x2) = [1 3] x1 + [0]
[0 1] [1]
[a__if](x1, x2, x3) = [1 2] x1 + [2 0] x2 + [2 2] x3 + [3]
[0 0] [0 1] [0 1] [0]
[div](x1, x2) = [1 3] x1 + [0]
[0 1] [1]
[minus](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[mark](x1) = [2 0] x1 + [0]
[0 1] [0]
[geq](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[if](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 2] x3 + [3]
[0 0] [0 1] [0 1] [0]
[a__minus^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[c_3](x1) = [1 0] x1 + [1]
[0 0] [0]
[a__geq^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[c_7](x1) = [1 0] x1 + [1]
[0 0] [0]
[a__div^#](x1, x2) = [0 3] x1 + [0]
[0 0] [0]
[c_10](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[a__if^#](x1, x2, x3) = [2 1] x2 + [2 1] x3 + [2]
[0 0] [0 0] [0]
[c_12](x1) = [1 0] x1 + [0]
[0 0] [0]
[mark^#](x1) = [2 1] x1 + [1]
[0 1] [1]
[c_13](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_15](x1) = [1 0] x1 + [1]
[0 0] [3]
[c_18](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
[c_19](x1) = [2 0] x1 + [0]
[0 0] [1]
[c_20](x1) = [1 0] x1 + [0]
[0 0] [1]
[c_21](x1, x2) = [1 0] x1 + [1 3] x2 + [0]
[0 0] [0 0] [1]
This order satisfies following ordering constraints:
[a__minus(X1, X2)] = [0 1] X1 + [0]
[0 0] [0]
>= [0 1] X1 + [0]
[0 0] [0]
= [minus(X1, X2)]
[a__minus(0(), Y)] = [0]
[0]
>= [0]
[0]
= [0()]
[a__minus(s(X), s(Y))] = [0 1] X + [2]
[0 0] [0]
> [0 1] X + [0]
[0 0] [0]
= [a__minus(X, Y)]
[a__geq(X1, X2)] = [0 1] X1 + [0]
[0 0] [0]
>= [0 1] X1 + [0]
[0 0] [0]
= [geq(X1, X2)]
[a__geq(X, 0())] = [0 1] X + [0]
[0 0] [0]
>= [0]
[0]
= [true()]
[a__geq(0(), s(Y))] = [0]
[0]
>= [0]
[0]
= [false()]
[a__geq(s(X), s(Y))] = [0 1] X + [2]
[0 0] [0]
> [0 1] X + [0]
[0 0] [0]
= [a__geq(X, Y)]
[a__div(X1, X2)] = [1 3] X1 + [0]
[0 1] [1]
>= [1 3] X1 + [0]
[0 1] [1]
= [div(X1, X2)]
[a__div(0(), s(Y))] = [0]
[1]
>= [0]
[0]
= [0()]
[a__div(s(X), s(Y))] = [1 3] X + [6]
[0 1] [3]
> [0 3] X + [3]
[0 0] [3]
= [a__if(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0())]
[a__if(X1, X2, X3)] = [1 2] X1 + [2 0] X2 + [2 2] X3 + [3]
[0 0] [0 1] [0 1] [0]
>= [1 2] X1 + [1 0] X2 + [1 2] X3 + [3]
[0 0] [0 1] [0 1] [0]
= [if(X1, X2, X3)]
[a__if(true(), X, Y)] = [2 2] Y + [2 0] X + [3]
[0 1] [0 1] [0]
> [2 0] X + [0]
[0 1] [0]
= [mark(X)]
[a__if(false(), X, Y)] = [2 2] Y + [2 0] X + [3]
[0 1] [0 1] [0]
> [2 0] Y + [0]
[0 1] [0]
= [mark(Y)]
[mark(0())] = [0]
[0]
>= [0]
[0]
= [0()]
[mark(s(X))] = [2 0] X + [0]
[0 1] [2]
>= [2 0] X + [0]
[0 1] [2]
= [s(mark(X))]
[mark(true())] = [0]
[0]
>= [0]
[0]
= [true()]
[mark(false())] = [0]
[0]
>= [0]
[0]
= [false()]
[mark(div(X1, X2))] = [2 6] X1 + [0]
[0 1] [1]
>= [2 3] X1 + [0]
[0 1] [1]
= [a__div(mark(X1), X2)]
[mark(minus(X1, X2))] = [0 2] X1 + [0]
[0 0] [0]
>= [0 1] X1 + [0]
[0 0] [0]
= [a__minus(X1, X2)]
[mark(geq(X1, X2))] = [0 2] X1 + [0]
[0 0] [0]
>= [0 1] X1 + [0]
[0 0] [0]
= [a__geq(X1, X2)]
[mark(if(X1, X2, X3))] = [2 4] X1 + [2 0] X2 + [2 4] X3 + [6]
[0 0] [0 1] [0 1] [0]
> [2 2] X1 + [2 0] X2 + [2 2] X3 + [3]
[0 0] [0 1] [0 1] [0]
= [a__if(mark(X1), X2, X3)]
[a__minus^#(s(X), s(Y))] = [0 1] X + [2]
[0 0] [0]
> [0 1] X + [1]
[0 0] [0]
= [c_3(a__minus^#(X, Y))]
[a__geq^#(s(X), s(Y))] = [0 1] X + [2]
[0 0] [0]
> [0 1] X + [1]
[0 0] [0]
= [c_7(a__geq^#(X, Y))]
[a__div^#(s(X), s(Y))] = [0 3] X + [6]
[0 0] [0]
> [0 3] X + [5]
[0 0] [0]
= [c_10(a__if^#(a__geq(X, Y), s(div(minus(X, Y), s(Y))), 0()),
a__geq^#(X, Y))]
[a__if^#(true(), X, Y)] = [2 1] Y + [2 1] X + [2]
[0 0] [0 0] [0]
> [2 1] X + [1]
[0 0] [0]
= [c_12(mark^#(X))]
[a__if^#(false(), X, Y)] = [2 1] Y + [2 1] X + [2]
[0 0] [0 0] [0]
> [2 1] Y + [1]
[0 0] [0]
= [c_13(mark^#(Y))]
[mark^#(s(X))] = [2 1] X + [3]
[0 1] [3]
> [2 1] X + [2]
[0 0] [3]
= [c_15(mark^#(X))]
[mark^#(div(X1, X2))] = [2 7] X1 + [2]
[0 1] [2]
> [2 7] X1 + [1]
[0 0] [1]
= [c_18(a__div^#(mark(X1), X2), mark^#(X1))]
[mark^#(minus(X1, X2))] = [0 2] X1 + [1]
[0 0] [1]
> [0 2] X1 + [0]
[0 0] [1]
= [c_19(a__minus^#(X1, X2))]
[mark^#(geq(X1, X2))] = [0 2] X1 + [1]
[0 0] [1]
> [0 1] X1 + [0]
[0 0] [1]
= [c_20(a__geq^#(X1, X2))]
[mark^#(if(X1, X2, X3))] = [2 4] X1 + [2 1] X2 + [2 5] X3 + [7]
[0 0] [0 1] [0 1] [1]
> [2 4] X1 + [2 1] X2 + [2 1] X3 + [6]
[0 0] [0 0] [0 0] [1]
= [c_21(a__if^#(mark(X1), X2, X3), mark^#(X1))]
Hurray, we answered YES(?,O(n^2))