YES
Problem:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
active(head(cons(X,XS))) -> mark(X)
active(tail(cons(X,XS))) -> mark(XS)
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Proof:
Matrix Interpretation Processor: dim=1
interpretation:
[tail](x0) = x0 + 6,
[head](x0) = 4x0 + 2,
[s](x0) = 2x0,
[odds] = 0,
[pairs] = 0,
[mark](x0) = x0,
[cons](x0, x1) = x0 + x1,
[incr](x0) = 2x0,
[0] = 0,
[active](x0) = x0,
[nats] = 0
orientation:
active(nats()) = 0 >= 0 = mark(cons(0(),incr(nats())))
active(pairs()) = 0 >= 0 = mark(cons(0(),incr(odds())))
active(odds()) = 0 >= 0 = mark(incr(pairs()))
active(incr(cons(X,XS))) = 2X + 2XS >= 2X + 2XS = mark(cons(s(X),incr(XS)))
active(head(cons(X,XS))) = 4X + 4XS + 2 >= X = mark(X)
active(tail(cons(X,XS))) = X + XS + 6 >= XS = mark(XS)
mark(nats()) = 0 >= 0 = active(nats())
mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = active(cons(mark(X1),X2))
mark(0()) = 0 >= 0 = active(0())
mark(incr(X)) = 2X >= 2X = active(incr(mark(X)))
mark(pairs()) = 0 >= 0 = active(pairs())
mark(odds()) = 0 >= 0 = active(odds())
mark(s(X)) = 2X >= 2X = active(s(mark(X)))
mark(head(X)) = 4X + 2 >= 4X + 2 = active(head(mark(X)))
mark(tail(X)) = X + 6 >= X + 6 = active(tail(mark(X)))
cons(mark(X1),X2) = X1 + X2 >= X1 + X2 = cons(X1,X2)
cons(X1,mark(X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
cons(active(X1),X2) = X1 + X2 >= X1 + X2 = cons(X1,X2)
cons(X1,active(X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
incr(mark(X)) = 2X >= 2X = incr(X)
incr(active(X)) = 2X >= 2X = incr(X)
s(mark(X)) = 2X >= 2X = s(X)
s(active(X)) = 2X >= 2X = s(X)
head(mark(X)) = 4X + 2 >= 4X + 2 = head(X)
head(active(X)) = 4X + 2 >= 4X + 2 = head(X)
tail(mark(X)) = X + 6 >= X + 6 = tail(X)
tail(active(X)) = X + 6 >= X + 6 = tail(X)
problem:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
DP Processor:
DPs:
active#(nats()) -> incr#(nats())
active#(nats()) -> cons#(0(),incr(nats()))
active#(nats()) -> mark#(cons(0(),incr(nats())))
active#(pairs()) -> incr#(odds())
active#(pairs()) -> cons#(0(),incr(odds()))
active#(pairs()) -> mark#(cons(0(),incr(odds())))
active#(odds()) -> incr#(pairs())
active#(odds()) -> mark#(incr(pairs()))
active#(incr(cons(X,XS))) -> incr#(XS)
active#(incr(cons(X,XS))) -> s#(X)
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(nats()) -> active#(nats())
mark#(cons(X1,X2)) -> mark#(X1)
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(0()) -> active#(0())
mark#(incr(X)) -> mark#(X)
mark#(incr(X)) -> incr#(mark(X))
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(pairs()) -> active#(pairs())
mark#(odds()) -> active#(odds())
mark#(s(X)) -> mark#(X)
mark#(s(X)) -> s#(mark(X))
mark#(s(X)) -> active#(s(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(head(X)) -> head#(mark(X))
mark#(head(X)) -> active#(head(mark(X)))
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> tail#(mark(X))
mark#(tail(X)) -> active#(tail(mark(X)))
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(X1,mark(X2)) -> cons#(X1,X2)
cons#(active(X1),X2) -> cons#(X1,X2)
cons#(X1,active(X2)) -> cons#(X1,X2)
incr#(mark(X)) -> incr#(X)
incr#(active(X)) -> incr#(X)
s#(mark(X)) -> s#(X)
s#(active(X)) -> s#(X)
head#(mark(X)) -> head#(X)
head#(active(X)) -> head#(X)
tail#(mark(X)) -> tail#(X)
tail#(active(X)) -> tail#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
TDG Processor:
DPs:
active#(nats()) -> incr#(nats())
active#(nats()) -> cons#(0(),incr(nats()))
active#(nats()) -> mark#(cons(0(),incr(nats())))
active#(pairs()) -> incr#(odds())
active#(pairs()) -> cons#(0(),incr(odds()))
active#(pairs()) -> mark#(cons(0(),incr(odds())))
active#(odds()) -> incr#(pairs())
active#(odds()) -> mark#(incr(pairs()))
active#(incr(cons(X,XS))) -> incr#(XS)
active#(incr(cons(X,XS))) -> s#(X)
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(nats()) -> active#(nats())
mark#(cons(X1,X2)) -> mark#(X1)
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(0()) -> active#(0())
mark#(incr(X)) -> mark#(X)
mark#(incr(X)) -> incr#(mark(X))
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(pairs()) -> active#(pairs())
mark#(odds()) -> active#(odds())
mark#(s(X)) -> mark#(X)
mark#(s(X)) -> s#(mark(X))
mark#(s(X)) -> active#(s(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(head(X)) -> head#(mark(X))
mark#(head(X)) -> active#(head(mark(X)))
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> tail#(mark(X))
mark#(tail(X)) -> active#(tail(mark(X)))
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(X1,mark(X2)) -> cons#(X1,X2)
cons#(active(X1),X2) -> cons#(X1,X2)
cons#(X1,active(X2)) -> cons#(X1,X2)
incr#(mark(X)) -> incr#(X)
incr#(active(X)) -> incr#(X)
s#(mark(X)) -> s#(X)
s#(active(X)) -> s#(X)
head#(mark(X)) -> head#(X)
head#(active(X)) -> head#(X)
tail#(mark(X)) -> tail#(X)
tail#(active(X)) -> tail#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
graph:
tail#(mark(X)) -> tail#(X) -> tail#(active(X)) -> tail#(X)
tail#(mark(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
tail#(active(X)) -> tail#(X) -> tail#(active(X)) -> tail#(X)
tail#(active(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
head#(mark(X)) -> head#(X) -> head#(active(X)) -> head#(X)
head#(mark(X)) -> head#(X) -> head#(mark(X)) -> head#(X)
head#(active(X)) -> head#(X) -> head#(active(X)) -> head#(X)
head#(active(X)) -> head#(X) -> head#(mark(X)) -> head#(X)
s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
mark#(tail(X)) -> tail#(mark(X)) ->
tail#(active(X)) -> tail#(X)
mark#(tail(X)) -> tail#(mark(X)) -> tail#(mark(X)) -> tail#(X)
mark#(tail(X)) -> mark#(X) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> mark#(X) ->
mark#(head(X)) -> active#(head(mark(X)))
mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
mark#(tail(X)) -> mark#(X) -> mark#(odds()) -> active#(odds())
mark#(tail(X)) -> mark#(X) -> mark#(pairs()) -> active#(pairs())
mark#(tail(X)) -> mark#(X) ->
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
mark#(tail(X)) -> mark#(X) -> mark#(0()) -> active#(0())
mark#(tail(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(tail(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
mark#(tail(X)) -> mark#(X) ->
mark#(nats()) -> active#(nats())
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(incr(cons(X,XS))) -> s#(X)
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(incr(cons(X,XS))) -> incr#(XS)
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(odds()) -> incr#(pairs())
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(pairs()) -> incr#(odds())
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(nats()) -> incr#(nats())
mark#(head(X)) -> head#(mark(X)) ->
head#(active(X)) -> head#(X)
mark#(head(X)) -> head#(mark(X)) -> head#(mark(X)) -> head#(X)
mark#(head(X)) -> mark#(X) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
mark#(head(X)) -> mark#(X) ->
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
mark#(head(X)) -> mark#(X) -> mark#(odds()) -> active#(odds())
mark#(head(X)) -> mark#(X) -> mark#(pairs()) -> active#(pairs())
mark#(head(X)) -> mark#(X) ->
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
mark#(head(X)) -> mark#(X) -> mark#(0()) -> active#(0())
mark#(head(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(head(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
mark#(head(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
mark#(head(X)) -> mark#(X) ->
mark#(nats()) -> active#(nats())
mark#(head(X)) -> active#(head(mark(X))) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(head(X)) -> active#(head(mark(X))) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(head(X)) -> active#(head(mark(X))) ->
active#(incr(cons(X,XS))) -> s#(X)
mark#(head(X)) -> active#(head(mark(X))) ->
active#(incr(cons(X,XS))) -> incr#(XS)
mark#(head(X)) -> active#(head(mark(X))) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(head(X)) -> active#(head(mark(X))) ->
active#(odds()) -> incr#(pairs())
mark#(head(X)) -> active#(head(mark(X))) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(head(X)) -> active#(head(mark(X))) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(head(X)) -> active#(head(mark(X))) ->
active#(pairs()) -> incr#(odds())
mark#(head(X)) -> active#(head(mark(X))) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(head(X)) -> active#(head(mark(X))) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(head(X)) -> active#(head(mark(X))) ->
active#(nats()) -> incr#(nats())
mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> active#(tail(mark(X)))
mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> active#(head(mark(X)))
mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
mark#(s(X)) -> mark#(X) -> mark#(odds()) -> active#(odds())
mark#(s(X)) -> mark#(X) -> mark#(pairs()) -> active#(pairs())
mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> active#(incr(mark(X)))
mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
mark#(s(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
mark#(s(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
mark#(s(X)) -> active#(s(mark(X))) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(s(X)) -> active#(s(mark(X))) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(s(X)) -> active#(s(mark(X))) ->
active#(incr(cons(X,XS))) -> s#(X)
mark#(s(X)) -> active#(s(mark(X))) ->
active#(incr(cons(X,XS))) -> incr#(XS)
mark#(s(X)) -> active#(s(mark(X))) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(s(X)) -> active#(s(mark(X))) ->
active#(odds()) -> incr#(pairs())
mark#(s(X)) -> active#(s(mark(X))) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(s(X)) -> active#(s(mark(X))) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(s(X)) -> active#(s(mark(X))) ->
active#(pairs()) -> incr#(odds())
mark#(s(X)) -> active#(s(mark(X))) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(s(X)) -> active#(s(mark(X))) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(s(X)) -> active#(s(mark(X))) ->
active#(nats()) -> incr#(nats())
mark#(odds()) -> active#(odds()) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(odds()) -> active#(odds()) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(odds()) -> active#(odds()) ->
active#(incr(cons(X,XS))) -> s#(X)
mark#(odds()) -> active#(odds()) ->
active#(incr(cons(X,XS))) -> incr#(XS)
mark#(odds()) -> active#(odds()) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(odds()) -> active#(odds()) ->
active#(odds()) -> incr#(pairs())
mark#(odds()) -> active#(odds()) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(odds()) -> active#(odds()) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(odds()) -> active#(odds()) ->
active#(pairs()) -> incr#(odds())
mark#(odds()) -> active#(odds()) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(odds()) -> active#(odds()) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(odds()) -> active#(odds()) ->
active#(nats()) -> incr#(nats())
mark#(pairs()) -> active#(pairs()) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(pairs()) -> active#(pairs()) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(pairs()) -> active#(pairs()) ->
active#(incr(cons(X,XS))) -> s#(X)
mark#(pairs()) -> active#(pairs()) ->
active#(incr(cons(X,XS))) -> incr#(XS)
mark#(pairs()) -> active#(pairs()) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(pairs()) -> active#(pairs()) ->
active#(odds()) -> incr#(pairs())
mark#(pairs()) -> active#(pairs()) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(pairs()) -> active#(pairs()) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(pairs()) -> active#(pairs()) ->
active#(pairs()) -> incr#(odds())
mark#(pairs()) -> active#(pairs()) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(pairs()) -> active#(pairs()) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(pairs()) -> active#(pairs()) ->
active#(nats()) -> incr#(nats())
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(tail(X)) -> tail#(mark(X))
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(head(X)) -> active#(head(mark(X)))
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(head(X)) -> head#(mark(X))
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(head(X)) -> mark#(X)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(s(X)) -> active#(s(mark(X)))
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(odds()) -> active#(odds())
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(pairs()) -> active#(pairs())
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(incr(X)) -> incr#(mark(X))
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(incr(X)) -> mark#(X)
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(cons(X1,X2)) -> mark#(X1)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(nats()) -> active#(nats())
mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
cons#(X1,active(X2)) -> cons#(X1,X2)
mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
cons#(active(X1),X2) -> cons#(X1,X2)
mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
cons#(X1,mark(X2)) -> cons#(X1,X2)
mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(incr(cons(X,XS))) -> s#(X)
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(incr(cons(X,XS))) -> incr#(XS)
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(odds()) -> incr#(pairs())
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(pairs()) -> incr#(odds())
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(nats()) -> incr#(nats())
mark#(incr(X)) -> mark#(X) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
mark#(incr(X)) -> mark#(X) ->
mark#(head(X)) -> active#(head(mark(X)))
mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> head#(mark(X))
mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
mark#(incr(X)) -> mark#(X) -> mark#(odds()) -> active#(odds())
mark#(incr(X)) -> mark#(X) -> mark#(pairs()) -> active#(pairs())
mark#(incr(X)) -> mark#(X) ->
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> incr#(mark(X))
mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
mark#(incr(X)) -> mark#(X) -> mark#(0()) -> active#(0())
mark#(incr(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(incr(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
mark#(incr(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
mark#(incr(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
mark#(incr(X)) -> incr#(mark(X)) ->
incr#(active(X)) -> incr#(X)
mark#(incr(X)) -> incr#(mark(X)) ->
incr#(mark(X)) -> incr#(X)
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(incr(cons(X,XS))) -> s#(X)
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(incr(cons(X,XS))) -> incr#(XS)
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(odds()) -> incr#(pairs())
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(pairs()) -> incr#(odds())
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(nats()) -> incr#(nats())
mark#(0()) -> active#(0()) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(0()) -> active#(0()) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(0()) -> active#(0()) -> active#(incr(cons(X,XS))) -> s#(X)
mark#(0()) -> active#(0()) -> active#(incr(cons(X,XS))) -> incr#(XS)
mark#(0()) -> active#(0()) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(0()) -> active#(0()) -> active#(odds()) -> incr#(pairs())
mark#(0()) -> active#(0()) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(0()) -> active#(0()) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(0()) -> active#(0()) -> active#(pairs()) -> incr#(odds())
mark#(0()) -> active#(0()) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(0()) -> active#(0()) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(0()) -> active#(0()) -> active#(nats()) -> incr#(nats())
mark#(nats()) -> active#(nats()) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(nats()) -> active#(nats()) ->
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
mark#(nats()) -> active#(nats()) ->
active#(incr(cons(X,XS))) -> s#(X)
mark#(nats()) -> active#(nats()) ->
active#(incr(cons(X,XS))) -> incr#(XS)
mark#(nats()) -> active#(nats()) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(nats()) -> active#(nats()) ->
active#(odds()) -> incr#(pairs())
mark#(nats()) -> active#(nats()) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(nats()) -> active#(nats()) ->
active#(pairs()) -> cons#(0(),incr(odds()))
mark#(nats()) -> active#(nats()) ->
active#(pairs()) -> incr#(odds())
mark#(nats()) -> active#(nats()) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(nats()) -> active#(nats()) ->
active#(nats()) -> cons#(0(),incr(nats()))
mark#(nats()) -> active#(nats()) ->
active#(nats()) -> incr#(nats())
cons#(mark(X1),X2) -> cons#(X1,X2) ->
cons#(X1,active(X2)) -> cons#(X1,X2)
cons#(mark(X1),X2) -> cons#(X1,X2) ->
cons#(active(X1),X2) -> cons#(X1,X2)
cons#(mark(X1),X2) -> cons#(X1,X2) ->
cons#(X1,mark(X2)) -> cons#(X1,X2)
cons#(mark(X1),X2) -> cons#(X1,X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(active(X1),X2) -> cons#(X1,X2) ->
cons#(X1,active(X2)) -> cons#(X1,X2)
cons#(active(X1),X2) -> cons#(X1,X2) ->
cons#(active(X1),X2) -> cons#(X1,X2)
cons#(active(X1),X2) -> cons#(X1,X2) ->
cons#(X1,mark(X2)) -> cons#(X1,X2)
cons#(active(X1),X2) -> cons#(X1,X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(X1,mark(X2)) -> cons#(X1,X2) ->
cons#(X1,active(X2)) -> cons#(X1,X2)
cons#(X1,mark(X2)) -> cons#(X1,X2) ->
cons#(active(X1),X2) -> cons#(X1,X2)
cons#(X1,mark(X2)) -> cons#(X1,X2) ->
cons#(X1,mark(X2)) -> cons#(X1,X2)
cons#(X1,mark(X2)) -> cons#(X1,X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(X1,active(X2)) -> cons#(X1,X2) ->
cons#(X1,active(X2)) -> cons#(X1,X2)
cons#(X1,active(X2)) -> cons#(X1,X2) ->
cons#(active(X1),X2) -> cons#(X1,X2)
cons#(X1,active(X2)) -> cons#(X1,X2) ->
cons#(X1,mark(X2)) -> cons#(X1,X2)
cons#(X1,active(X2)) -> cons#(X1,X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
incr#(mark(X)) -> incr#(X) -> incr#(active(X)) -> incr#(X)
incr#(mark(X)) -> incr#(X) -> incr#(mark(X)) -> incr#(X)
incr#(active(X)) -> incr#(X) -> incr#(active(X)) -> incr#(X)
incr#(active(X)) -> incr#(X) ->
incr#(mark(X)) -> incr#(X)
active#(odds()) -> mark#(incr(pairs())) ->
mark#(tail(X)) -> active#(tail(mark(X)))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(tail(X)) -> tail#(mark(X))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(tail(X)) -> mark#(X)
active#(odds()) -> mark#(incr(pairs())) ->
mark#(head(X)) -> active#(head(mark(X)))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(head(X)) -> head#(mark(X))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(head(X)) -> mark#(X)
active#(odds()) -> mark#(incr(pairs())) ->
mark#(s(X)) -> active#(s(mark(X)))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(s(X)) -> s#(mark(X))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(s(X)) -> mark#(X)
active#(odds()) -> mark#(incr(pairs())) ->
mark#(odds()) -> active#(odds())
active#(odds()) -> mark#(incr(pairs())) ->
mark#(pairs()) -> active#(pairs())
active#(odds()) -> mark#(incr(pairs())) ->
mark#(incr(X)) -> active#(incr(mark(X)))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(incr(X)) -> incr#(mark(X))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(incr(X)) -> mark#(X)
active#(odds()) -> mark#(incr(pairs())) ->
mark#(0()) -> active#(0())
active#(odds()) -> mark#(incr(pairs())) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
active#(odds()) -> mark#(incr(pairs())) ->
mark#(cons(X1,X2)) -> mark#(X1)
active#(odds()) -> mark#(incr(pairs())) ->
mark#(nats()) -> active#(nats())
active#(odds()) -> incr#(pairs()) ->
incr#(active(X)) -> incr#(X)
active#(odds()) -> incr#(pairs()) ->
incr#(mark(X)) -> incr#(X)
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(tail(X)) -> active#(tail(mark(X)))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(tail(X)) -> tail#(mark(X))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(tail(X)) -> mark#(X)
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(head(X)) -> active#(head(mark(X)))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(head(X)) -> head#(mark(X))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(head(X)) -> mark#(X)
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(s(X)) -> active#(s(mark(X)))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(s(X)) -> s#(mark(X))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(s(X)) -> mark#(X)
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(odds()) -> active#(odds())
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(pairs()) -> active#(pairs())
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(incr(X)) -> active#(incr(mark(X)))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(incr(X)) -> incr#(mark(X))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(incr(X)) -> mark#(X)
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(0()) -> active#(0())
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(cons(X1,X2)) -> mark#(X1)
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(nats()) -> active#(nats())
active#(pairs()) -> cons#(0(),incr(odds())) ->
cons#(X1,active(X2)) -> cons#(X1,X2)
active#(pairs()) -> cons#(0(),incr(odds())) ->
cons#(active(X1),X2) -> cons#(X1,X2)
active#(pairs()) -> cons#(0(),incr(odds())) ->
cons#(X1,mark(X2)) -> cons#(X1,X2)
active#(pairs()) -> cons#(0(),incr(odds())) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
active#(pairs()) -> incr#(odds()) ->
incr#(active(X)) -> incr#(X)
active#(pairs()) -> incr#(odds()) ->
incr#(mark(X)) -> incr#(X)
active#(incr(cons(X,XS))) -> s#(X) -> s#(active(X)) -> s#(X)
active#(incr(cons(X,XS))) -> s#(X) ->
s#(mark(X)) -> s#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(tail(X)) -> active#(tail(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(tail(X)) -> tail#(mark(X))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(tail(X)) -> mark#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(head(X)) -> active#(head(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(head(X)) -> head#(mark(X))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(head(X)) -> mark#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(s(X)) -> active#(s(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(s(X)) -> s#(mark(X))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(s(X)) -> mark#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(odds()) -> active#(odds())
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(pairs()) -> active#(pairs())
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(incr(X)) -> active#(incr(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(incr(X)) -> incr#(mark(X))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(incr(X)) -> mark#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(0()) -> active#(0())
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(cons(X1,X2)) -> mark#(X1)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(nats()) -> active#(nats())
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS)) ->
cons#(X1,active(X2)) -> cons#(X1,X2)
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS)) ->
cons#(active(X1),X2) -> cons#(X1,X2)
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS)) ->
cons#(X1,mark(X2)) -> cons#(X1,X2)
active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS)) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
active#(incr(cons(X,XS))) -> incr#(XS) ->
incr#(active(X)) -> incr#(X)
active#(incr(cons(X,XS))) -> incr#(XS) ->
incr#(mark(X)) -> incr#(X)
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(tail(X)) -> active#(tail(mark(X)))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(tail(X)) -> tail#(mark(X))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(tail(X)) -> mark#(X)
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(head(X)) -> active#(head(mark(X)))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(head(X)) -> head#(mark(X))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(head(X)) -> mark#(X)
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(s(X)) -> active#(s(mark(X)))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(s(X)) -> s#(mark(X))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(s(X)) -> mark#(X)
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(odds()) -> active#(odds())
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(pairs()) -> active#(pairs())
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(incr(X)) -> active#(incr(mark(X)))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(incr(X)) -> incr#(mark(X))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(incr(X)) -> mark#(X)
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(0()) -> active#(0())
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(cons(X1,X2)) -> mark#(X1)
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(nats()) -> active#(nats())
active#(nats()) -> cons#(0(),incr(nats())) ->
cons#(X1,active(X2)) -> cons#(X1,X2)
active#(nats()) -> cons#(0(),incr(nats())) ->
cons#(active(X1),X2) -> cons#(X1,X2)
active#(nats()) -> cons#(0(),incr(nats())) ->
cons#(X1,mark(X2)) -> cons#(X1,X2)
active#(nats()) -> cons#(0(),incr(nats())) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
active#(nats()) -> incr#(nats()) ->
incr#(active(X)) -> incr#(X)
active#(nats()) -> incr#(nats()) -> incr#(mark(X)) -> incr#(X)
SCC Processor:
#sccs: 6
#rules: 30
#arcs: 345/1849
DPs:
mark#(tail(X)) -> mark#(X)
mark#(nats()) -> active#(nats())
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(cons(X1,X2)) -> mark#(X1)
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(0()) -> active#(0())
active#(odds()) -> mark#(incr(pairs()))
mark#(incr(X)) -> mark#(X)
mark#(incr(X)) -> active#(incr(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(pairs()) -> active#(pairs())
mark#(odds()) -> active#(odds())
mark#(s(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(head(X)) -> active#(head(mark(X)))
mark#(tail(X)) -> active#(tail(mark(X)))
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
EDG Processor:
DPs:
mark#(tail(X)) -> mark#(X)
mark#(nats()) -> active#(nats())
active#(nats()) -> mark#(cons(0(),incr(nats())))
mark#(cons(X1,X2)) -> mark#(X1)
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(0()) -> active#(0())
active#(odds()) -> mark#(incr(pairs()))
mark#(incr(X)) -> mark#(X)
mark#(incr(X)) -> active#(incr(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(pairs()) -> active#(pairs())
mark#(odds()) -> active#(odds())
mark#(s(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(head(X)) -> active#(head(mark(X)))
mark#(tail(X)) -> active#(tail(mark(X)))
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
graph:
mark#(tail(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
mark#(tail(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(tail(X)) -> mark#(X) -> mark#(0()) -> active#(0())
mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
mark#(tail(X)) -> mark#(X) ->
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(tail(X)) -> mark#(X) -> mark#(pairs()) -> active#(pairs())
mark#(tail(X)) -> mark#(X) -> mark#(odds()) -> active#(odds())
mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
mark#(tail(X)) -> mark#(X) ->
mark#(head(X)) -> active#(head(mark(X)))
mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> mark#(X) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(tail(X)) -> active#(tail(mark(X))) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(head(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
mark#(head(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
mark#(head(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(head(X)) -> mark#(X) -> mark#(0()) -> active#(0())
mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
mark#(head(X)) -> mark#(X) ->
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(head(X)) -> mark#(X) -> mark#(pairs()) -> active#(pairs())
mark#(head(X)) -> mark#(X) -> mark#(odds()) -> active#(odds())
mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
mark#(head(X)) -> mark#(X) ->
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
mark#(head(X)) -> mark#(X) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(head(X)) -> active#(head(mark(X))) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(s(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
mark#(s(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> active#(incr(mark(X)))
mark#(s(X)) -> mark#(X) -> mark#(pairs()) -> active#(pairs())
mark#(s(X)) -> mark#(X) -> mark#(odds()) -> active#(odds())
mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> active#(head(mark(X)))
mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
mark#(s(X)) -> mark#(X) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(s(X)) -> active#(s(mark(X))) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(odds()) -> active#(odds()) ->
active#(odds()) -> mark#(incr(pairs()))
mark#(pairs()) -> active#(pairs()) ->
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(nats()) -> active#(nats())
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(cons(X1,X2)) -> mark#(X1)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(incr(X)) -> mark#(X)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(pairs()) -> active#(pairs())
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(odds()) -> active#(odds())
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(s(X)) -> active#(s(mark(X)))
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(head(X)) -> mark#(X)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(head(X)) -> active#(head(mark(X)))
mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X)
mark#(cons(X1,X2)) -> mark#(X1) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(incr(X)) -> mark#(X) -> mark#(nats()) -> active#(nats())
mark#(incr(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
mark#(incr(X)) -> mark#(X) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(incr(X)) -> mark#(X) -> mark#(0()) -> active#(0())
mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
mark#(incr(X)) -> mark#(X) ->
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(incr(X)) -> mark#(X) -> mark#(pairs()) -> active#(pairs())
mark#(incr(X)) -> mark#(X) -> mark#(odds()) -> active#(odds())
mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
mark#(incr(X)) -> mark#(X) ->
mark#(head(X)) -> active#(head(mark(X)))
mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
mark#(incr(X)) -> mark#(X) ->
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(incr(X)) -> active#(incr(mark(X))) ->
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(nats()) -> active#(nats()) ->
active#(nats()) -> mark#(cons(0(),incr(nats())))
active#(odds()) -> mark#(incr(pairs())) ->
mark#(incr(X)) -> mark#(X)
active#(odds()) -> mark#(incr(pairs())) ->
mark#(incr(X)) -> active#(incr(mark(X)))
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(cons(X1,X2)) -> mark#(X1)
active#(pairs()) -> mark#(cons(0(),incr(odds()))) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(cons(X1,X2)) -> mark#(X1)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(incr(X)) -> mark#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(incr(X)) -> active#(incr(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(s(X)) -> mark#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(s(X)) -> active#(s(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(head(X)) -> mark#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(head(X)) -> active#(head(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(tail(X)) -> mark#(X)
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS))) ->
mark#(tail(X)) -> active#(tail(mark(X)))
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(cons(X1,X2)) -> mark#(X1)
active#(nats()) -> mark#(cons(0(),incr(nats()))) ->
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
SCC Processor:
#sccs: 1
#rules: 17
#arcs: 94/324
DPs:
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> active#(tail(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X)
mark#(odds()) -> active#(odds())
active#(odds()) -> mark#(incr(pairs()))
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(incr(X)) -> mark#(X)
mark#(pairs()) -> active#(pairs())
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(cons(X1,X2)) -> mark#(X1)
mark#(nats()) -> active#(nats())
active#(nats()) -> mark#(cons(0(),incr(nats())))
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Bounds Processor:
bound: 0
enrichment: match-dp
automaton:
final states: {50}
transitions:
00() -> 53*
mark{#,0}(54) -> 50*
mark{#,0}(53) -> 50*
active{#,0}(81) -> 50*
nats0() -> 51*
active0(53) -> 80*
mark0(53) -> 80*
cons0(53,52) -> 81,54
cons0(80,52) -> 81*
incr0(51) -> 52*
problem:
DPs:
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> active#(tail(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X)
mark#(odds()) -> active#(odds())
active#(odds()) -> mark#(incr(pairs()))
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(incr(X)) -> mark#(X)
mark#(pairs()) -> active#(pairs())
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(cons(X1,X2)) -> mark#(X1)
mark#(nats()) -> active#(nats())
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
SCC Processor:
#sccs: 1
#rules: 15
#arcs: 89/256
DPs:
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> active#(tail(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X)
mark#(odds()) -> active#(odds())
active#(odds()) -> mark#(incr(pairs()))
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(incr(X)) -> mark#(X)
mark#(pairs()) -> active#(pairs())
active#(pairs()) -> mark#(cons(0(),incr(odds())))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(cons(X1,X2)) -> mark#(X1)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Bounds Processor:
bound: 0
enrichment: match-dp
automaton:
final states: {37}
transitions:
00() -> 40*
mark{#,0}(40) -> 37*
mark{#,0}(41) -> 37*
active{#,0}(67) -> 37*
active0(40) -> 66*
mark0(40) -> 66*
cons0(40,39) -> 67,41
cons0(66,39) -> 67*
incr0(38) -> 39*
odds0() -> 38*
problem:
DPs:
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> active#(tail(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X)
mark#(odds()) -> active#(odds())
active#(odds()) -> mark#(incr(pairs()))
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(incr(X)) -> mark#(X)
mark#(pairs()) -> active#(pairs())
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(cons(X1,X2)) -> mark#(X1)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
SCC Processor:
#sccs: 1
#rules: 13
#arcs: 81/196
DPs:
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> active#(tail(mark(X)))
active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X)
mark#(odds()) -> active#(odds())
active#(odds()) -> mark#(incr(pairs()))
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(incr(X)) -> mark#(X)
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
mark#(cons(X1,X2)) -> mark#(X1)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Semantic Labeling Processor:
dimension: 1
usable rules:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
interpretation:
[tail](x0) = x0 + 1,
[head](x0) = 0,
[s](x0) = 0,
[odds] = 0,
[pairs] = 0,
[mark](x0) = x0,
[cons](x0, x1) = 0,
[incr](x0) = 0,
[0] = 0,
[active](x0) = 1,
[nats] = 0
labeled:
odds
pairs
nats
0
usable (for model):
odds
pairs
nats
0
argument filtering:
pi(nats) = []
pi(active) = 0
pi(0) = []
pi(incr) = [0]
pi(cons) = [0]
pi(mark) = 0
pi(pairs) = []
pi(odds) = []
pi(s) = 0
pi(head) = 0
pi(tail) = 0
pi(active#) = 0
pi(mark#) = 0
precedence:
odds > pairs > nats > 0 > incr > mark# ~ active# ~ tail ~
head ~ s ~ mark ~ cons ~ active
problem:
DPs:
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X)
mark#(odds()) -> active#(odds())
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Restore Modifier:
DPs:
mark#(tail(X)) -> mark#(X)
mark#(tail(X)) -> active#(tail(mark(X)))
mark#(head(X)) -> active#(head(mark(X)))
mark#(head(X)) -> mark#(X)
mark#(s(X)) -> active#(s(mark(X)))
mark#(s(X)) -> mark#(X)
mark#(odds()) -> active#(odds())
mark#(incr(X)) -> active#(incr(mark(X)))
mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
SCC Processor:
#sccs: 1
#rules: 3
#arcs: 73/81
DPs:
mark#(tail(X)) -> mark#(X)
mark#(head(X)) -> mark#(X)
mark#(s(X)) -> mark#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Bounds Processor:
bound: 0
enrichment: match-dp
automaton:
final states: {5}
transitions:
f1110() -> 6*
mark{#,0}(6) -> 5*
problem:
DPs:
mark#(tail(X)) -> mark#(X)
mark#(head(X)) -> mark#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Bounds Processor:
bound: 0
enrichment: match-dp
automaton:
final states: {3}
transitions:
mark{#,0}(4) -> 3*
f1130() -> 4*
problem:
DPs:
mark#(tail(X)) -> mark#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Bounds Processor:
bound: 0
enrichment: match-dp
automaton:
final states: {1}
transitions:
mark{#,0}(2) -> 1*
f1150() -> 2*
problem:
DPs:
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Qed
DPs:
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(X1,mark(X2)) -> cons#(X1,X2)
cons#(active(X1),X2) -> cons#(X1,X2)
cons#(X1,active(X2)) -> cons#(X1,X2)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Subterm Criterion Processor:
simple projection:
pi(cons#) = 1
problem:
DPs:
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(active(X1),X2) -> cons#(X1,X2)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Subterm Criterion Processor:
simple projection:
pi(cons#) = 0
problem:
DPs:
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Qed
DPs:
incr#(mark(X)) -> incr#(X)
incr#(active(X)) -> incr#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Subterm Criterion Processor:
simple projection:
pi(incr#) = 0
problem:
DPs:
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Qed
DPs:
s#(mark(X)) -> s#(X)
s#(active(X)) -> s#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Subterm Criterion Processor:
simple projection:
pi(s#) = 0
problem:
DPs:
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Qed
DPs:
head#(mark(X)) -> head#(X)
head#(active(X)) -> head#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Subterm Criterion Processor:
simple projection:
pi(head#) = 0
problem:
DPs:
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Qed
DPs:
tail#(mark(X)) -> tail#(X)
tail#(active(X)) -> tail#(X)
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Subterm Criterion Processor:
simple projection:
pi(tail#) = 0
problem:
DPs:
TRS:
active(nats()) -> mark(cons(0(),incr(nats())))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(odds()) -> mark(incr(pairs()))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
mark(nats()) -> active(nats())
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(0()) -> active(0())
mark(incr(X)) -> active(incr(mark(X)))
mark(pairs()) -> active(pairs())
mark(odds()) -> active(odds())
mark(s(X)) -> active(s(mark(X)))
mark(head(X)) -> active(head(mark(X)))
mark(tail(X)) -> active(tail(mark(X)))
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
incr(mark(X)) -> incr(X)
incr(active(X)) -> incr(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
head(mark(X)) -> head(X)
head(active(X)) -> head(X)
tail(mark(X)) -> tail(X)
tail(active(X)) -> tail(X)
Qed