YES
Problem:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Proof:
DP Processor:
DPs:
active#(f(0())) -> s#(0())
active#(f(0())) -> f#(s(0()))
active#(f(0())) -> cons#(0(),f(s(0())))
active#(f(s(0()))) -> p#(s(0()))
active#(f(s(0()))) -> f#(p(s(0())))
active#(f(X)) -> active#(X)
active#(f(X)) -> f#(active(X))
active#(cons(X1,X2)) -> active#(X1)
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(s(X)) -> active#(X)
active#(s(X)) -> s#(active(X))
active#(p(X)) -> active#(X)
active#(p(X)) -> p#(active(X))
f#(mark(X)) -> f#(X)
cons#(mark(X1),X2) -> cons#(X1,X2)
s#(mark(X)) -> s#(X)
p#(mark(X)) -> p#(X)
proper#(f(X)) -> proper#(X)
proper#(f(X)) -> f#(proper(X))
proper#(cons(X1,X2)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X1)
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(s(X)) -> proper#(X)
proper#(s(X)) -> s#(proper(X))
proper#(p(X)) -> proper#(X)
proper#(p(X)) -> p#(proper(X))
f#(ok(X)) -> f#(X)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
s#(ok(X)) -> s#(X)
p#(ok(X)) -> p#(X)
top#(mark(X)) -> proper#(X)
top#(mark(X)) -> top#(proper(X))
top#(ok(X)) -> active#(X)
top#(ok(X)) -> top#(active(X))
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
TDG Processor:
DPs:
active#(f(0())) -> s#(0())
active#(f(0())) -> f#(s(0()))
active#(f(0())) -> cons#(0(),f(s(0())))
active#(f(s(0()))) -> p#(s(0()))
active#(f(s(0()))) -> f#(p(s(0())))
active#(f(X)) -> active#(X)
active#(f(X)) -> f#(active(X))
active#(cons(X1,X2)) -> active#(X1)
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(s(X)) -> active#(X)
active#(s(X)) -> s#(active(X))
active#(p(X)) -> active#(X)
active#(p(X)) -> p#(active(X))
f#(mark(X)) -> f#(X)
cons#(mark(X1),X2) -> cons#(X1,X2)
s#(mark(X)) -> s#(X)
p#(mark(X)) -> p#(X)
proper#(f(X)) -> proper#(X)
proper#(f(X)) -> f#(proper(X))
proper#(cons(X1,X2)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X1)
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(s(X)) -> proper#(X)
proper#(s(X)) -> s#(proper(X))
proper#(p(X)) -> proper#(X)
proper#(p(X)) -> p#(proper(X))
f#(ok(X)) -> f#(X)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
s#(ok(X)) -> s#(X)
p#(ok(X)) -> p#(X)
top#(mark(X)) -> proper#(X)
top#(mark(X)) -> top#(proper(X))
top#(ok(X)) -> active#(X)
top#(ok(X)) -> top#(active(X))
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
graph:
top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X))
top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
top#(ok(X)) -> top#(active(X)) ->
top#(mark(X)) -> top#(proper(X))
top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
top#(ok(X)) -> active#(X) -> active#(p(X)) -> p#(active(X))
top#(ok(X)) -> active#(X) -> active#(p(X)) -> active#(X)
top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X)
top#(ok(X)) -> active#(X) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
top#(ok(X)) -> active#(X) -> active#(f(X)) -> f#(active(X))
top#(ok(X)) -> active#(X) -> active#(f(X)) -> active#(X)
top#(ok(X)) -> active#(X) -> active#(f(s(0()))) -> f#(p(s(0())))
top#(ok(X)) -> active#(X) -> active#(f(s(0()))) -> p#(s(0()))
top#(ok(X)) -> active#(X) -> active#(f(0())) -> cons#(0(),f(s(0())))
top#(ok(X)) -> active#(X) -> active#(f(0())) -> f#(s(0()))
top#(ok(X)) -> active#(X) -> active#(f(0())) -> s#(0())
top#(mark(X)) -> top#(proper(X)) ->
top#(ok(X)) -> top#(active(X))
top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
top#(mark(X)) -> top#(proper(X)) ->
top#(mark(X)) -> top#(proper(X))
top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
top#(mark(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X))
top#(mark(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X)
top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
top#(mark(X)) -> proper#(X) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
top#(mark(X)) -> proper#(X) -> proper#(f(X)) -> f#(proper(X))
top#(mark(X)) -> proper#(X) -> proper#(f(X)) -> proper#(X)
proper#(p(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X))
proper#(p(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X)
proper#(p(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
proper#(p(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
proper#(p(X)) -> proper#(X) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(p(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
proper#(p(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
proper#(p(X)) -> proper#(X) -> proper#(f(X)) -> f#(proper(X))
proper#(p(X)) -> proper#(X) -> proper#(f(X)) -> proper#(X)
proper#(p(X)) -> p#(proper(X)) -> p#(ok(X)) -> p#(X)
proper#(p(X)) -> p#(proper(X)) -> p#(mark(X)) -> p#(X)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(p(X)) -> p#(proper(X))
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(p(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(s(X)) -> s#(proper(X))
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(s(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> proper#(X1)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(f(X)) -> f#(proper(X))
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(f(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(p(X)) -> p#(proper(X))
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(p(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(s(X)) -> s#(proper(X))
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(s(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(cons(X1,X2)) -> proper#(X1)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(cons(X1,X2)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(f(X)) -> f#(proper(X))
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(f(X)) -> proper#(X)
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
proper#(s(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X))
proper#(s(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X)
proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
proper#(s(X)) -> proper#(X) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
proper#(s(X)) -> proper#(X) -> proper#(f(X)) -> f#(proper(X))
proper#(s(X)) -> proper#(X) -> proper#(f(X)) -> proper#(X)
proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
proper#(f(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X))
proper#(f(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X)
proper#(f(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
proper#(f(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
proper#(f(X)) -> proper#(X) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(f(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
proper#(f(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
proper#(f(X)) -> proper#(X) -> proper#(f(X)) -> f#(proper(X))
proper#(f(X)) -> proper#(X) -> proper#(f(X)) -> proper#(X)
proper#(f(X)) -> f#(proper(X)) -> f#(ok(X)) -> f#(X)
proper#(f(X)) -> f#(proper(X)) -> f#(mark(X)) -> f#(X)
p#(ok(X)) -> p#(X) -> p#(ok(X)) -> p#(X)
p#(ok(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
p#(mark(X)) -> p#(X) -> p#(ok(X)) -> p#(X)
p#(mark(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(mark(X1),X2) -> cons#(X1,X2) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2)
f#(ok(X)) -> f#(X) -> f#(ok(X)) -> f#(X)
f#(ok(X)) -> f#(X) -> f#(mark(X)) -> f#(X)
f#(mark(X)) -> f#(X) -> f#(ok(X)) -> f#(X)
f#(mark(X)) -> f#(X) -> f#(mark(X)) -> f#(X)
s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
active#(p(X)) -> p#(active(X)) -> p#(ok(X)) -> p#(X)
active#(p(X)) -> p#(active(X)) -> p#(mark(X)) -> p#(X)
active#(p(X)) -> active#(X) -> active#(p(X)) -> p#(active(X))
active#(p(X)) -> active#(X) -> active#(p(X)) -> active#(X)
active#(p(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
active#(p(X)) -> active#(X) -> active#(s(X)) -> active#(X)
active#(p(X)) -> active#(X) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(p(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
active#(p(X)) -> active#(X) -> active#(f(X)) -> f#(active(X))
active#(p(X)) -> active#(X) -> active#(f(X)) -> active#(X)
active#(p(X)) -> active#(X) -> active#(f(s(0()))) -> f#(p(s(0())))
active#(p(X)) -> active#(X) -> active#(f(s(0()))) -> p#(s(0()))
active#(p(X)) -> active#(X) ->
active#(f(0())) -> cons#(0(),f(s(0())))
active#(p(X)) -> active#(X) -> active#(f(0())) -> f#(s(0()))
active#(p(X)) -> active#(X) ->
active#(f(0())) -> s#(0())
active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
active#(cons(X1,X2)) -> active#(X1) ->
active#(p(X)) -> p#(active(X))
active#(cons(X1,X2)) -> active#(X1) ->
active#(p(X)) -> active#(X)
active#(cons(X1,X2)) -> active#(X1) ->
active#(s(X)) -> s#(active(X))
active#(cons(X1,X2)) -> active#(X1) ->
active#(s(X)) -> active#(X)
active#(cons(X1,X2)) -> active#(X1) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(cons(X1,X2)) -> active#(X1) ->
active#(cons(X1,X2)) -> active#(X1)
active#(cons(X1,X2)) -> active#(X1) ->
active#(f(X)) -> f#(active(X))
active#(cons(X1,X2)) -> active#(X1) ->
active#(f(X)) -> active#(X)
active#(cons(X1,X2)) -> active#(X1) ->
active#(f(s(0()))) -> f#(p(s(0())))
active#(cons(X1,X2)) -> active#(X1) ->
active#(f(s(0()))) -> p#(s(0()))
active#(cons(X1,X2)) -> active#(X1) ->
active#(f(0())) -> cons#(0(),f(s(0())))
active#(cons(X1,X2)) -> active#(X1) ->
active#(f(0())) -> f#(s(0()))
active#(cons(X1,X2)) -> active#(X1) -> active#(f(0())) -> s#(0())
active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
active#(s(X)) -> active#(X) -> active#(p(X)) -> p#(active(X))
active#(s(X)) -> active#(X) -> active#(p(X)) -> active#(X)
active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X)
active#(s(X)) -> active#(X) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(s(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
active#(s(X)) -> active#(X) -> active#(f(X)) -> f#(active(X))
active#(s(X)) -> active#(X) -> active#(f(X)) -> active#(X)
active#(s(X)) -> active#(X) -> active#(f(s(0()))) -> f#(p(s(0())))
active#(s(X)) -> active#(X) -> active#(f(s(0()))) -> p#(s(0()))
active#(s(X)) -> active#(X) ->
active#(f(0())) -> cons#(0(),f(s(0())))
active#(s(X)) -> active#(X) -> active#(f(0())) -> f#(s(0()))
active#(s(X)) -> active#(X) -> active#(f(0())) -> s#(0())
active#(f(s(0()))) -> p#(s(0())) -> p#(ok(X)) -> p#(X)
active#(f(s(0()))) -> p#(s(0())) -> p#(mark(X)) -> p#(X)
active#(f(s(0()))) -> f#(p(s(0()))) -> f#(ok(X)) -> f#(X)
active#(f(s(0()))) -> f#(p(s(0()))) ->
f#(mark(X)) -> f#(X)
active#(f(0())) -> cons#(0(),f(s(0()))) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
active#(f(0())) -> cons#(0(),f(s(0()))) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
active#(f(0())) -> f#(s(0())) -> f#(ok(X)) -> f#(X)
active#(f(0())) -> f#(s(0())) -> f#(mark(X)) -> f#(X)
active#(f(0())) -> s#(0()) -> s#(ok(X)) -> s#(X)
active#(f(0())) -> s#(0()) -> s#(mark(X)) -> s#(X)
active#(f(X)) -> f#(active(X)) -> f#(ok(X)) -> f#(X)
active#(f(X)) -> f#(active(X)) -> f#(mark(X)) -> f#(X)
active#(f(X)) -> active#(X) -> active#(p(X)) -> p#(active(X))
active#(f(X)) -> active#(X) -> active#(p(X)) -> active#(X)
active#(f(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
active#(f(X)) -> active#(X) -> active#(s(X)) -> active#(X)
active#(f(X)) -> active#(X) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(f(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
active#(f(X)) -> active#(X) -> active#(f(X)) -> f#(active(X))
active#(f(X)) -> active#(X) -> active#(f(X)) -> active#(X)
active#(f(X)) -> active#(X) -> active#(f(s(0()))) -> f#(p(s(0())))
active#(f(X)) -> active#(X) -> active#(f(s(0()))) -> p#(s(0()))
active#(f(X)) -> active#(X) ->
active#(f(0())) -> cons#(0(),f(s(0())))
active#(f(X)) -> active#(X) -> active#(f(0())) -> f#(s(0()))
active#(f(X)) -> active#(X) -> active#(f(0())) -> s#(0())
SCC Processor:
#sccs: 7
#rules: 19
#arcs: 169/1156
DPs:
top#(ok(X)) -> top#(active(X))
top#(mark(X)) -> top#(proper(X))
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Matrix Interpretation Processor: dim=3
interpretation:
[top#](x0) = [1 1 0]x0,
[0 1 0] [1]
[top](x0) = [1 0 1]x0 + [0]
[0 0 0] [0],
[ok](x0) = x0
,
[proper](x0) = x0
,
[1 0 0]
[p](x0) = [0 1 0]x0
[0 1 0] ,
[0 0 0] [1]
[mark](x0) = [1 1 0]x0 + [0]
[1 0 1] [0],
[1 0 0]
[cons](x0, x1) = [0 0 1]x0
[0 1 0] ,
[0 0 0] [1]
[s](x0) = [1 1 0]x0 + [0]
[1 0 1] [1],
[active](x0) = x0
,
[0 0 0] [1]
[f](x0) = [1 0 1]x0 + [0]
[1 0 1] [0],
[0]
[0] = [0]
[0]
orientation:
top#(ok(X)) = [1 1 0]X >= [1 1 0]X = top#(active(X))
top#(mark(X)) = [1 1 0]X + [1] >= [1 1 0]X = top#(proper(X))
[1] [1]
active(f(0())) = [0] >= [0] = mark(cons(0(),f(s(0()))))
[0] [0]
[1] [1]
active(f(s(0()))) = [2] >= [2] = mark(f(p(s(0()))))
[2] [2]
[1] [1]
active(p(s(0()))) = [0] >= [0] = mark(0())
[0] [0]
[0 0 0] [1] [0 0 0] [1]
active(f(X)) = [1 0 1]X + [0] >= [1 0 1]X + [0] = f(active(X))
[1 0 1] [0] [1 0 1] [0]
[1 0 0] [1 0 0]
active(cons(X1,X2)) = [0 0 1]X1 >= [0 0 1]X1 = cons(active(X1),X2)
[0 1 0] [0 1 0]
[0 0 0] [1] [0 0 0] [1]
active(s(X)) = [1 1 0]X + [0] >= [1 1 0]X + [0] = s(active(X))
[1 0 1] [1] [1 0 1] [1]
[1 0 0] [1 0 0]
active(p(X)) = [0 1 0]X >= [0 1 0]X = p(active(X))
[0 1 0] [0 1 0]
[0 0 0] [1] [0 0 0] [1]
f(mark(X)) = [1 0 1]X + [1] >= [1 0 1]X + [1] = mark(f(X))
[1 0 1] [1] [1 0 1] [1]
[0 0 0] [1] [0 0 0] [1]
cons(mark(X1),X2) = [1 0 1]X1 + [0] >= [1 0 1]X1 + [0] = mark(cons(X1,X2))
[1 1 0] [0] [1 1 0] [0]
[0 0 0] [1] [0 0 0] [1]
s(mark(X)) = [1 1 0]X + [1] >= [1 1 0]X + [1] = mark(s(X))
[1 0 1] [2] [1 0 1] [2]
[0 0 0] [1] [0 0 0] [1]
p(mark(X)) = [1 1 0]X + [0] >= [1 1 0]X + [0] = mark(p(X))
[1 1 0] [0] [1 1 0] [0]
[0 0 0] [1] [0 0 0] [1]
proper(f(X)) = [1 0 1]X + [0] >= [1 0 1]X + [0] = f(proper(X))
[1 0 1] [0] [1 0 1] [0]
[0] [0]
proper(0()) = [0] >= [0] = ok(0())
[0] [0]
[1 0 0] [1 0 0]
proper(cons(X1,X2)) = [0 0 1]X1 >= [0 0 1]X1 = cons(proper(X1),proper(X2))
[0 1 0] [0 1 0]
[0 0 0] [1] [0 0 0] [1]
proper(s(X)) = [1 1 0]X + [0] >= [1 1 0]X + [0] = s(proper(X))
[1 0 1] [1] [1 0 1] [1]
[1 0 0] [1 0 0]
proper(p(X)) = [0 1 0]X >= [0 1 0]X = p(proper(X))
[0 1 0] [0 1 0]
[0 0 0] [1] [0 0 0] [1]
f(ok(X)) = [1 0 1]X + [0] >= [1 0 1]X + [0] = ok(f(X))
[1 0 1] [0] [1 0 1] [0]
[1 0 0] [1 0 0]
cons(ok(X1),ok(X2)) = [0 0 1]X1 >= [0 0 1]X1 = ok(cons(X1,X2))
[0 1 0] [0 1 0]
[0 0 0] [1] [0 0 0] [1]
s(ok(X)) = [1 1 0]X + [0] >= [1 1 0]X + [0] = ok(s(X))
[1 0 1] [1] [1 0 1] [1]
[1 0 0] [1 0 0]
p(ok(X)) = [0 1 0]X >= [0 1 0]X = ok(p(X))
[0 1 0] [0 1 0]
[1 1 0] [1] [0 1 0] [1]
top(mark(X)) = [1 0 1]X + [1] >= [1 0 1]X + [0] = top(proper(X))
[0 0 0] [0] [0 0 0] [0]
[0 1 0] [1] [0 1 0] [1]
top(ok(X)) = [1 0 1]X + [0] >= [1 0 1]X + [0] = top(active(X))
[0 0 0] [0] [0 0 0] [0]
problem:
DPs:
top#(ok(X)) -> top#(active(X))
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
KBO Processor:
argument filtering:
pi(0) = []
pi(f) = 0
pi(active) = []
pi(s) = 0
pi(cons) = 0
pi(mark) = []
pi(p) = 0
pi(proper) = [0]
pi(ok) = []
pi(top) = []
pi(top#) = 0
weight function:
w0 = 1
w(top#) = w(top) = w(ok) = w(mark) = w(s) = w(active) = w(0) = 1
w(proper) = w(p) = w(cons) = w(f) = 0
precedence:
top ~ proper > ok > active > top# ~ p ~ mark ~ cons ~ s ~ f ~ 0
problem:
DPs:
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Qed
DPs:
active#(f(X)) -> active#(X)
active#(cons(X1,X2)) -> active#(X1)
active#(s(X)) -> active#(X)
active#(p(X)) -> active#(X)
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Subterm Criterion Processor:
simple projection:
pi(active#) = 0
problem:
DPs:
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Qed
DPs:
proper#(f(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X1)
proper#(s(X)) -> proper#(X)
proper#(p(X)) -> proper#(X)
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Subterm Criterion Processor:
simple projection:
pi(proper#) = 0
problem:
DPs:
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Qed
DPs:
p#(mark(X)) -> p#(X)
p#(ok(X)) -> p#(X)
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Subterm Criterion Processor:
simple projection:
pi(p#) = 0
problem:
DPs:
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Qed
DPs:
s#(mark(X)) -> s#(X)
s#(ok(X)) -> s#(X)
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Subterm Criterion Processor:
simple projection:
pi(s#) = 0
problem:
DPs:
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Qed
DPs:
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Subterm Criterion Processor:
simple projection:
pi(cons#) = 1
problem:
DPs:
cons#(mark(X1),X2) -> cons#(X1,X2)
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Subterm Criterion Processor:
simple projection:
pi(cons#) = 0
problem:
DPs:
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Qed
DPs:
f#(mark(X)) -> f#(X)
f#(ok(X)) -> f#(X)
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Subterm Criterion Processor:
simple projection:
pi(f#) = 0
problem:
DPs:
TRS:
active(f(0())) -> mark(cons(0(),f(s(0()))))
active(f(s(0()))) -> mark(f(p(s(0()))))
active(p(s(0()))) -> mark(0())
active(f(X)) -> f(active(X))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(p(X)) -> p(active(X))
f(mark(X)) -> mark(f(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
p(mark(X)) -> mark(p(X))
proper(f(X)) -> f(proper(X))
proper(0()) -> ok(0())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(s(X)) -> s(proper(X))
proper(p(X)) -> p(proper(X))
f(ok(X)) -> ok(f(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
p(ok(X)) -> ok(p(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Qed