Problem: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(tt()) -> active(tt()) mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) mark(0()) -> active(0()) mark(s(X)) -> active(s(mark(X))) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) plus(mark(X1),X2) -> plus(X1,X2) plus(X1,mark(X2)) -> plus(X1,X2) plus(active(X1),X2) -> plus(X1,X2) plus(X1,active(X2)) -> plus(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {7,6,5,4,3} transitions: active1(9) -> 4* 01() -> 9* tt1() -> 9* active0(2) -> 3* active0(1) -> 3* and0(1,2) -> 5* and0(2,1) -> 5* and0(1,1) -> 5* and0(2,2) -> 5* tt0() -> 1* mark0(2) -> 4* mark0(1) -> 4* plus0(1,2) -> 6* plus0(2,1) -> 6* plus0(1,1) -> 6* plus0(2,2) -> 6* 00() -> 2* s0(2) -> 7* s0(1) -> 7* problem: Qed