Problem:
 a(f(),0()) -> a(s(),0())
 a(d(),0()) -> 0()
 a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x)))))
 a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x))))
 a(p(),a(s(),x)) -> x

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6}
   transitions:
    01() -> 6,9
    a1(10,9) -> 6*
    s1() -> 10*
    a0(3,1) -> 6*
    a0(3,3) -> 6*
    a0(3,5) -> 6*
    a0(4,2) -> 6*
    a0(4,4) -> 6*
    a0(5,1) -> 6*
    a0(5,3) -> 6*
    a0(5,5) -> 6*
    a0(1,2) -> 6*
    a0(1,4) -> 6*
    a0(2,1) -> 6*
    a0(2,3) -> 6*
    a0(2,5) -> 6*
    a0(3,2) -> 6*
    a0(3,4) -> 6*
    a0(4,1) -> 6*
    a0(4,3) -> 6*
    a0(4,5) -> 6*
    a0(5,2) -> 6*
    a0(5,4) -> 6*
    a0(1,1) -> 6*
    a0(1,3) -> 6*
    a0(1,5) -> 6*
    a0(2,2) -> 6*
    a0(2,4) -> 6*
    f0() -> 1*
    00() -> 2*
    s0() -> 3*
    d0() -> 4*
    p0() -> 5*
  problem:
   
  Qed