MAYBE Problem: nats() -> adx(zeros()) zeros() -> cons(n__0(),n__zeros()) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) -> activate(X) tl(cons(X,Y)) -> activate(Y) 0() -> n__0() zeros() -> n__zeros() s(X) -> n__s(X) incr(X) -> n__incr(X) adx(X) -> n__adx(X) activate(n__0()) -> 0() activate(n__zeros()) -> zeros() activate(n__s(X)) -> s(X) activate(n__incr(X)) -> incr(X) activate(n__adx(X)) -> adx(X) activate(X) -> X Proof: DP Processor: DPs: nats#() -> zeros#() nats#() -> adx#(zeros()) incr#(cons(X,Y)) -> activate#(Y) incr#(cons(X,Y)) -> activate#(X) adx#(cons(X,Y)) -> activate#(Y) adx#(cons(X,Y)) -> activate#(X) adx#(cons(X,Y)) -> incr#(cons(activate(X),n__adx(activate(Y)))) hd#(cons(X,Y)) -> activate#(X) tl#(cons(X,Y)) -> activate#(Y) activate#(n__0()) -> 0#() activate#(n__zeros()) -> zeros#() activate#(n__s(X)) -> s#(X) activate#(n__incr(X)) -> incr#(X) activate#(n__adx(X)) -> adx#(X) TRS: nats() -> adx(zeros()) zeros() -> cons(n__0(),n__zeros()) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) -> activate(X) tl(cons(X,Y)) -> activate(Y) 0() -> n__0() zeros() -> n__zeros() s(X) -> n__s(X) incr(X) -> n__incr(X) adx(X) -> n__adx(X) activate(n__0()) -> 0() activate(n__zeros()) -> zeros() activate(n__s(X)) -> s(X) activate(n__incr(X)) -> incr(X) activate(n__adx(X)) -> adx(X) activate(X) -> X TDG Processor: DPs: nats#() -> zeros#() nats#() -> adx#(zeros()) incr#(cons(X,Y)) -> activate#(Y) incr#(cons(X,Y)) -> activate#(X) adx#(cons(X,Y)) -> activate#(Y) adx#(cons(X,Y)) -> activate#(X) adx#(cons(X,Y)) -> incr#(cons(activate(X),n__adx(activate(Y)))) hd#(cons(X,Y)) -> activate#(X) tl#(cons(X,Y)) -> activate#(Y) activate#(n__0()) -> 0#() activate#(n__zeros()) -> zeros#() activate#(n__s(X)) -> s#(X) activate#(n__incr(X)) -> incr#(X) activate#(n__adx(X)) -> adx#(X) TRS: nats() -> adx(zeros()) zeros() -> cons(n__0(),n__zeros()) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) -> activate(X) tl(cons(X,Y)) -> activate(Y) 0() -> n__0() zeros() -> n__zeros() s(X) -> n__s(X) incr(X) -> n__incr(X) adx(X) -> n__adx(X) activate(n__0()) -> 0() activate(n__zeros()) -> zeros() activate(n__s(X)) -> s(X) activate(n__incr(X)) -> incr(X) activate(n__adx(X)) -> adx(X) activate(X) -> X graph: tl#(cons(X,Y)) -> activate#(Y) -> activate#(n__adx(X)) -> adx#(X) tl#(cons(X,Y)) -> activate#(Y) -> activate#(n__incr(X)) -> incr#(X) tl#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) tl#(cons(X,Y)) -> activate#(Y) -> activate#(n__zeros()) -> zeros#() tl#(cons(X,Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() hd#(cons(X,Y)) -> activate#(X) -> activate#(n__adx(X)) -> adx#(X) hd#(cons(X,Y)) -> activate#(X) -> activate#(n__incr(X)) -> incr#(X) hd#(cons(X,Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) hd#(cons(X,Y)) -> activate#(X) -> activate#(n__zeros()) -> zeros#() hd#(cons(X,Y)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__adx(X)) -> adx#(X) -> adx#(cons(X,Y)) -> incr#(cons(activate(X),n__adx(activate(Y)))) activate#(n__adx(X)) -> adx#(X) -> adx#(cons(X,Y)) -> activate#(X) activate#(n__adx(X)) -> adx#(X) -> adx#(cons(X,Y)) -> activate#(Y) activate#(n__incr(X)) -> incr#(X) -> incr#(cons(X,Y)) -> activate#(X) activate#(n__incr(X)) -> incr#(X) -> incr#(cons(X,Y)) -> activate#(Y) incr#(cons(X,Y)) -> activate#(Y) -> activate#(n__adx(X)) -> adx#(X) incr#(cons(X,Y)) -> activate#(Y) -> activate#(n__incr(X)) -> incr#(X) incr#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) incr#(cons(X,Y)) -> activate#(Y) -> activate#(n__zeros()) -> zeros#() incr#(cons(X,Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() incr#(cons(X,Y)) -> activate#(X) -> activate#(n__adx(X)) -> adx#(X) incr#(cons(X,Y)) -> activate#(X) -> activate#(n__incr(X)) -> incr#(X) incr#(cons(X,Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) incr#(cons(X,Y)) -> activate#(X) -> activate#(n__zeros()) -> zeros#() incr#(cons(X,Y)) -> activate#(X) -> activate#(n__0()) -> 0#() adx#(cons(X,Y)) -> activate#(Y) -> activate#(n__adx(X)) -> adx#(X) adx#(cons(X,Y)) -> activate#(Y) -> activate#(n__incr(X)) -> incr#(X) adx#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) adx#(cons(X,Y)) -> activate#(Y) -> activate#(n__zeros()) -> zeros#() adx#(cons(X,Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() adx#(cons(X,Y)) -> activate#(X) -> activate#(n__adx(X)) -> adx#(X) adx#(cons(X,Y)) -> activate#(X) -> activate#(n__incr(X)) -> incr#(X) adx#(cons(X,Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) adx#(cons(X,Y)) -> activate#(X) -> activate#(n__zeros()) -> zeros#() adx#(cons(X,Y)) -> activate#(X) -> activate#(n__0()) -> 0#() adx#(cons(X,Y)) -> incr#(cons(activate(X),n__adx(activate(Y)))) -> incr#(cons(X,Y)) -> activate#(X) adx#(cons(X,Y)) -> incr#(cons(activate(X),n__adx(activate(Y)))) -> incr#(cons(X,Y)) -> activate#(Y) nats#() -> adx#(zeros()) -> adx#(cons(X,Y)) -> incr#(cons(activate(X),n__adx(activate(Y)))) nats#() -> adx#(zeros()) -> adx#(cons(X,Y)) -> activate#(X) nats#() -> adx#(zeros()) -> adx#(cons(X,Y)) -> activate#(Y) SCC Processor: #sccs: 1 #rules: 7 #arcs: 40/196 DPs: activate#(n__incr(X)) -> incr#(X) incr#(cons(X,Y)) -> activate#(Y) activate#(n__adx(X)) -> adx#(X) adx#(cons(X,Y)) -> activate#(Y) adx#(cons(X,Y)) -> activate#(X) adx#(cons(X,Y)) -> incr#(cons(activate(X),n__adx(activate(Y)))) incr#(cons(X,Y)) -> activate#(X) TRS: nats() -> adx(zeros()) zeros() -> cons(n__0(),n__zeros()) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) -> activate(X) tl(cons(X,Y)) -> activate(Y) 0() -> n__0() zeros() -> n__zeros() s(X) -> n__s(X) incr(X) -> n__incr(X) adx(X) -> n__adx(X) activate(n__0()) -> 0() activate(n__zeros()) -> zeros() activate(n__s(X)) -> s(X) activate(n__incr(X)) -> incr(X) activate(n__adx(X)) -> adx(X) activate(X) -> X Open