Problem:
 active(f(X)) -> mark(if(X,c(),f(true())))
 active(if(true(),X,Y)) -> mark(X)
 active(if(false(),X,Y)) -> mark(Y)
 mark(f(X)) -> active(f(mark(X)))
 mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3))
 mark(c()) -> active(c())
 mark(true()) -> active(true())
 mark(false()) -> active(false())
 f(mark(X)) -> f(X)
 f(active(X)) -> f(X)
 if(mark(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,mark(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,mark(X3)) -> if(X1,X2,X3)
 if(active(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,active(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,active(X3)) -> if(X1,X2,X3)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {7,6,5,4}
   transitions:
    active1(8) -> 5*
    false1() -> 8*
    true1() -> 8*
    c1() -> 8*
    active0(2) -> 4*
    active0(1) -> 4*
    active0(3) -> 4*
    f0(2) -> 6*
    f0(1) -> 6*
    f0(3) -> 6*
    mark0(2) -> 5*
    mark0(1) -> 5*
    mark0(3) -> 5*
    if0(1,1,1) -> 7*
    if0(1,3,1) -> 7*
    if0(1,2,3) -> 7*
    if0(2,2,1) -> 7*
    if0(2,1,3) -> 7*
    if0(2,3,3) -> 7*
    if0(3,1,1) -> 7*
    if0(1,1,2) -> 7*
    if0(3,3,1) -> 7*
    if0(1,3,2) -> 7*
    if0(3,2,3) -> 7*
    if0(2,2,2) -> 7*
    if0(3,1,2) -> 7*
    if0(3,3,2) -> 7*
    if0(1,2,1) -> 7*
    if0(1,1,3) -> 7*
    if0(1,3,3) -> 7*
    if0(2,1,1) -> 7*
    if0(2,3,1) -> 7*
    if0(2,2,3) -> 7*
    if0(3,2,1) -> 7*
    if0(1,2,2) -> 7*
    if0(3,1,3) -> 7*
    if0(3,3,3) -> 7*
    if0(2,1,2) -> 7*
    if0(2,3,2) -> 7*
    if0(3,2,2) -> 7*
    c0() -> 1*
    true0() -> 2*
    false0() -> 3*
  problem:
   
  Qed