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())
 mark(f(X)) -> active(f(mark(X)))
 mark(0()) -> active(0())
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(s(X)) -> active(s(mark(X)))
 mark(p(X)) -> active(p(mark(X)))
 f(mark(X)) -> f(X)
 f(active(X)) -> f(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)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 p(mark(X)) -> p(X)
 p(active(X)) -> p(X)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {7,6,5,4,3,2}
   transitions:
    active1(8) -> 3*
    01() -> 8*
    active0(1) -> 2*
    f0(1) -> 4*
    00() -> 1*
    mark0(1) -> 3*
    cons0(1,1) -> 5*
    s0(1) -> 6*
    p0(1) -> 7*
  problem:
   
  Qed