We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ number42() ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Nil(), b1, a2, b2, a3, b3) ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) ->
nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)
, goal(a1, b1, a2, b2, a3, b3) ->
nolexicord(a1, b1, a2, b2, a3, b3) }
Weak Trs:
{ nolexicord[Ite][False][Ite](True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, nolexicord[Ite][False][Ite](False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following dependency tuples:
Strict DPs:
{ number42^#() -> c_1()
, nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2()
, nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3),
eqNatList^#(Cons(x, xs), b1))
, eqNatList^#(Nil(), Nil()) -> c_4()
, eqNatList^#(Nil(), Cons(y, ys)) -> c_5()
, eqNatList^#(Cons(x, xs), Nil()) -> c_6()
, eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y))
, goal^#(a1, b1, a2, b2, a3, b3) ->
c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) }
Weak DPs:
{ nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs))
, !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y))
, !EQ^#(S(x), 0()) -> c_12()
, !EQ^#(0(), S(y)) -> c_13()
, !EQ^#(0(), 0()) -> c_14() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ number42^#() -> c_1()
, nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2()
, nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3),
eqNatList^#(Cons(x, xs), b1))
, eqNatList^#(Nil(), Nil()) -> c_4()
, eqNatList^#(Nil(), Cons(y, ys)) -> c_5()
, eqNatList^#(Cons(x, xs), Nil()) -> c_6()
, eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y))
, goal^#(a1, b1, a2, b2, a3, b3) ->
c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) }
Weak DPs:
{ nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs))
, !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y))
, !EQ^#(S(x), 0()) -> c_12()
, !EQ^#(0(), S(y)) -> c_13()
, !EQ^#(0(), 0()) -> c_14() }
Weak Trs:
{ nolexicord[Ite][False][Ite](True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, nolexicord[Ite][False][Ite](False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, number42() ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Nil(), b1, a2, b2, a3, b3) ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) ->
nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)
, !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)
, goal(a1, b1, a2, b2, a3, b3) ->
nolexicord(a1, b1, a2, b2, a3, b3) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {1,4,5,6,7} by
applications of Pre({1,4,5,6,7}) = {3}. Here rules are labeled as
follows:
DPs:
{ 1: number42^#() -> c_1()
, 2: nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2()
, 3: nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3),
eqNatList^#(Cons(x, xs), b1))
, 4: eqNatList^#(Nil(), Nil()) -> c_4()
, 5: eqNatList^#(Nil(), Cons(y, ys)) -> c_5()
, 6: eqNatList^#(Cons(x, xs), Nil()) -> c_6()
, 7: eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y))
, 8: goal^#(a1, b1, a2, b2, a3, b3) ->
c_8(nolexicord^#(a1, b1, a2, b2, a3, b3))
, 9: nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs))
, 10: nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs))
, 11: !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y))
, 12: !EQ^#(S(x), 0()) -> c_12()
, 13: !EQ^#(0(), S(y)) -> c_13()
, 14: !EQ^#(0(), 0()) -> c_14() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2()
, nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3),
eqNatList^#(Cons(x, xs), b1))
, goal^#(a1, b1, a2, b2, a3, b3) ->
c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) }
Weak DPs:
{ number42^#() -> c_1()
, nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs))
, eqNatList^#(Nil(), Nil()) -> c_4()
, eqNatList^#(Nil(), Cons(y, ys)) -> c_5()
, eqNatList^#(Cons(x, xs), Nil()) -> c_6()
, eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y))
, !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y))
, !EQ^#(S(x), 0()) -> c_12()
, !EQ^#(0(), S(y)) -> c_13()
, !EQ^#(0(), 0()) -> c_14() }
Weak Trs:
{ nolexicord[Ite][False][Ite](True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, nolexicord[Ite][False][Ite](False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, number42() ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Nil(), b1, a2, b2, a3, b3) ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) ->
nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)
, !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)
, goal(a1, b1, a2, b2, a3, b3) ->
nolexicord(a1, b1, a2, b2, a3, b3) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ number42^#() -> c_1()
, eqNatList^#(Nil(), Nil()) -> c_4()
, eqNatList^#(Nil(), Cons(y, ys)) -> c_5()
, eqNatList^#(Cons(x, xs), Nil()) -> c_6()
, eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y))
, !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y))
, !EQ^#(S(x), 0()) -> c_12()
, !EQ^#(0(), S(y)) -> c_13()
, !EQ^#(0(), 0()) -> c_14() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2()
, nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3),
eqNatList^#(Cons(x, xs), b1))
, goal^#(a1, b1, a2, b2, a3, b3) ->
c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) }
Weak DPs:
{ nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
Weak Trs:
{ nolexicord[Ite][False][Ite](True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, nolexicord[Ite][False][Ite](False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, number42() ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Nil(), b1, a2, b2, a3, b3) ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) ->
nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)
, !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)
, goal(a1, b1, a2, b2, a3, b3) ->
nolexicord(a1, b1, a2, b2, a3, b3) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3),
eqNatList^#(Cons(x, xs), b1)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1()
, nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3))
, goal^#(a1, b1, a2, b2, a3, b3) ->
c_3(nolexicord^#(a1, b1, a2, b2, a3, b3)) }
Weak DPs:
{ nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
Weak Trs:
{ nolexicord[Ite][False][Ite](True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, nolexicord[Ite][False][Ite](False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> nolexicord(xs', xs', xs', xs', xs', xs)
, number42() ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Nil(), b1, a2, b2, a3, b3) ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) ->
nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)
, !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)
, goal(a1, b1, a2, b2, a3, b3) ->
nolexicord(a1, b1, a2, b2, a3, b3) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1()
, nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3))
, goal^#(a1, b1, a2, b2, a3, b3) ->
c_3(nolexicord^#(a1, b1, a2, b2, a3, b3)) }
Weak DPs:
{ nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
Weak Trs:
{ !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Consider the dependency graph
1: nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1()
2: nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3))
-->_1 nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) :5
-->_1 nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs)) :4
3: goal^#(a1, b1, a2, b2, a3, b3) ->
c_3(nolexicord^#(a1, b1, a2, b2, a3, b3))
-->_1 nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)) :2
-->_1 nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1() :1
4: nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
-->_1 nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)) :2
-->_1 nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1() :1
5: nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs))
-->_1 nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)) :2
-->_1 nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1() :1
Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).
{ goal^#(a1, b1, a2, b2, a3, b3) ->
c_3(nolexicord^#(a1, b1, a2, b2, a3, b3)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1()
, nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)) }
Weak DPs:
{ nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
Weak Trs:
{ !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}
TcT has computed the following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 0
non-zero entries.
[True] = [0]
[Nil] = [0]
[eqNatList[Match][Cons][Match][Cons][Ite]](x1, x2, x3, x4, x5) = [0]
[!EQ](x1, x2) = [0]
[S](x1) = [0]
[Cons](x1, x2) = [0]
[0] = [0]
[eqNatList](x1, x2) = [0]
[False] = [0]
[nolexicord^#](x1, x2, x3, x4, x5, x6) = [1]
[nolexicord[Ite][False][Ite]^#](x1, x2, x3, x4, x5, x6, x7) = [1]
[c_1] = [0]
[c_2](x1) = [1] x1 + [0]
[c_4](x1) = [1] x1 + [0]
[c_5](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[!EQ(S(x), S(y))] = [0]
>= [0]
= [!EQ(x, y)]
[!EQ(S(x), 0())] = [0]
>= [0]
= [False()]
[!EQ(0(), S(y))] = [0]
>= [0]
= [False()]
[!EQ(0(), 0())] = [0]
>= [0]
= [True()]
[eqNatList(Nil(), Nil())] = [0]
>= [0]
= [True()]
[eqNatList(Nil(), Cons(y, ys))] = [0]
>= [0]
= [False()]
[eqNatList(Cons(x, xs), Nil())] = [0]
>= [0]
= [False()]
[eqNatList(Cons(x, xs), Cons(y, ys))] = [0]
>= [0]
= [eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)]
[nolexicord^#(Nil(), b1, a2, b2, a3, b3)] = [1]
> [0]
= [c_1()]
[nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3)] = [1]
>= [1]
= [c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3))]
[nolexicord[Ite][False][Ite]^#(True(), = [1]
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))]
>= [1]
= [c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))]
[nolexicord[Ite][False][Ite]^#(False(), = [1]
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))]
>= [1]
= [c_5(nolexicord^#(xs', xs', xs', xs', xs', xs))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)) }
Weak DPs:
{ nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1()
, nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
Weak Trs:
{ !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_1() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3)) }
Weak DPs:
{ nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
Weak Trs:
{ !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3))
, 2: nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
, 3: nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[True] = [0]
[Nil] = [0]
[eqNatList[Match][Cons][Match][Cons][Ite]](x1, x2, x3, x4, x5) = [0]
[!EQ](x1, x2) = [0]
[S](x1) = [1] x1 + [0]
[Cons](x1, x2) = [1] x2 + [1]
[0] = [0]
[eqNatList](x1, x2) = [0]
[False] = [0]
[nolexicord^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [6] x2 + [5] x3 + [1] x4 + [4]
[nolexicord[Ite][False][Ite]^#](x1, x2, x3, x4, x5, x6, x7) = [5] x1 + [3] x2 + [6] x3 + [5] x4 + [1] x5 + [0]
[c_1] = [0]
[c_2](x1) = [1] x1 + [1]
[c_4](x1) = [1] x1 + [1]
[c_5](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[!EQ(S(x), S(y))] = [0]
>= [0]
= [!EQ(x, y)]
[!EQ(S(x), 0())] = [0]
>= [0]
= [False()]
[!EQ(0(), S(y))] = [0]
>= [0]
= [False()]
[!EQ(0(), 0())] = [0]
>= [0]
= [True()]
[eqNatList(Nil(), Nil())] = [0]
>= [0]
= [True()]
[eqNatList(Nil(), Cons(y, ys))] = [0]
>= [0]
= [False()]
[eqNatList(Cons(x, xs), Nil())] = [0]
>= [0]
= [False()]
[eqNatList(Cons(x, xs), Cons(y, ys))] = [0]
>= [0]
= [eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)]
[nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3)] = [6] b1 + [5] a2 + [1] b2 + [3] xs + [7]
> [6] b1 + [5] a2 + [1] b2 + [3] xs + [4]
= [c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3))]
[nolexicord[Ite][False][Ite]^#(True(), = [15] xs' + [15]
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))]
> [15] xs' + [5]
= [c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))]
[nolexicord[Ite][False][Ite]^#(False(), = [15] xs' + [15]
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))]
> [15] xs' + [5]
= [c_5(nolexicord^#(xs', xs', xs', xs', xs', xs))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3))
, nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
Weak Trs:
{ !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) ->
c_2(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1),
Cons(x, xs),
b1,
a2,
b2,
a3,
b3))
, nolexicord[Ite][False][Ite]^#(True(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs),
Cons(x', xs'))
-> c_4(nolexicord^#(xs', xs', xs', xs', xs', xs))
, nolexicord[Ite][False][Ite]^#(False(),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x', xs'),
Cons(x, xs))
-> c_5(nolexicord^#(xs', xs', xs', xs', xs', xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ !EQ(S(x), S(y)) -> !EQ(x, y)
, !EQ(S(x), 0()) -> False()
, !EQ(0(), S(y)) -> False()
, !EQ(0(), 0()) -> True()
, eqNatList(Nil(), Nil()) -> True()
, eqNatList(Nil(), Cons(y, ys)) -> False()
, eqNatList(Cons(x, xs), Nil()) -> False()
, eqNatList(Cons(x, xs), Cons(y, ys)) ->
eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))