YES Problem: active(f(X,X)) -> mark(f(a(),b())) active(b()) -> mark(a()) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(a()) -> active(a()) mark(b()) -> active(b()) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Proof: Matrix Interpretation Processor: dim=3 interpretation: [1 0 1] [mark](x0) = [0 1 0]x0 [0 0 0] , [0] [b] = [0] [1], [0] [a] = [0] [0], [1 0 1] [active](x0) = [0 1 0]x0 [0 0 0] , [1 0 1] [1 0 0] [0] [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0] [0 0 0] [0 1 0] [1] orientation: [2 1 1] [1] [1] active(f(X,X)) = [0 0 0]X + [0] >= [0] = mark(f(a(),b())) [0 0 0] [0] [0] [1] [0] active(b()) = [0] >= [0] = mark(a()) [0] [0] [1 0 1] [1 1 0] [1] [1 0 1] [1 1 0] [1] mark(f(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = active(f(mark(X1),X2)) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] [0] [0] mark(a()) = [0] >= [0] = active(a()) [0] [0] [1] [1] mark(b()) = [0] >= [0] = active(b()) [0] [0] [1 0 1] [1 0 0] [0] [1 0 1] [1 0 0] [0] f(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = f(X1,X2) [0 0 0] [0 1 0] [1] [0 0 0] [0 1 0] [1] [1 0 1] [1 0 1] [0] [1 0 1] [1 0 0] [0] f(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = f(X1,X2) [0 0 0] [0 1 0] [1] [0 0 0] [0 1 0] [1] [1 0 1] [1 0 0] [0] [1 0 1] [1 0 0] [0] f(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = f(X1,X2) [0 0 0] [0 1 0] [1] [0 0 0] [0 1 0] [1] [1 0 1] [1 0 1] [0] [1 0 1] [1 0 0] [0] f(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = f(X1,X2) [0 0 0] [0 1 0] [1] [0 0 0] [0 1 0] [1] problem: active(f(X,X)) -> mark(f(a(),b())) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(a()) -> active(a()) mark(b()) -> active(b()) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Matrix Interpretation Processor: dim=3 interpretation: [1 0 1] [0] [mark](x0) = [0 0 0]x0 + [1] [0 0 1] [0], [0] [b] = [0] [1], [0] [a] = [0] [0], [1 1 0] [active](x0) = [0 1 0]x0 [0 0 1] , [1 0 0] [1 0 0] [0] [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1] [0 0 1] [0 0 0] [1] orientation: [2 0 0] [1] [1] active(f(X,X)) = [0 0 0]X + [1] >= [1] = mark(f(a(),b())) [0 0 1] [1] [1] [1 0 1] [1 0 0] [1] [1 0 1] [1 0 0] [1] mark(f(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = active(f(mark(X1),X2)) [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] [0] [0] mark(a()) = [1] >= [0] = active(a()) [0] [0] [1] [0] mark(b()) = [1] >= [0] = active(b()) [1] [1] [1 0 1] [1 0 0] [0] [1 0 0] [1 0 0] [0] f(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = f(X1,X2) [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] [1 0 0] [1 0 1] [0] [1 0 0] [1 0 0] [0] f(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = f(X1,X2) [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] [1 1 0] [1 0 0] [0] [1 0 0] [1 0 0] [0] f(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = f(X1,X2) [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] [1 0 0] [1 1 0] [0] [1 0 0] [1 0 0] [0] f(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = f(X1,X2) [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] problem: active(f(X,X)) -> mark(f(a(),b())) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(a()) -> active(a()) f(mark(X1),X2) -> f(X1,X2) f(X1,mark(X2)) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) f(X1,active(X2)) -> f(X1,X2) Matrix Interpretation Processor: dim=3 interpretation: [0] [mark](x0) = x0 + [0] [1], [0] [b] = [0] [0], [0] [a] = [0] [0], [0] [active](x0) = x0 + [0] [1], [1 0 0] [1 0 1] [0] [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1] [0 0 0] [0 0 0] [0] orientation: [2 0 1] [0] [0] active(f(X,X)) = [0 0 0]X + [1] >= [1] = mark(f(a(),b())) [0 0 0] [1] [1] [1 0 0] [1 0 1] [0] [1 0 0] [1 0 1] [0] mark(f(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = active(f(mark(X1),X2)) [0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] [1] [0] [0] mark(a()) = [0] >= [0] = active(a()) [1] [1] [1 0 0] [1 0 1] [0] [1 0 0] [1 0 1] [0] f(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = f(X1,X2) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] [1 0 0] [1 0 1] [1] [1 0 0] [1 0 1] [0] f(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = f(X1,X2) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] [1 0 0] [1 0 1] [0] [1 0 0] [1 0 1] [0] f(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = f(X1,X2) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] [1 0 0] [1 0 1] [1] [1 0 0] [1 0 1] [0] f(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = f(X1,X2) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] problem: active(f(X,X)) -> mark(f(a(),b())) mark(f(X1,X2)) -> active(f(mark(X1),X2)) mark(a()) -> active(a()) f(mark(X1),X2) -> f(X1,X2) f(active(X1),X2) -> f(X1,X2) Bounds Processor: bound: 3 enrichment: match automaton: final states: {49,19,18,16,15,10,9,5,1} transitions: f50() -> 6* mark0(47) -> 15* mark0(17) -> 15* mark0(4) -> 15*,7,5,1 mark0(6) -> 7* f0(49,6) -> 8* f0(19,6) -> 8* f0(18,6) -> 8* f0(15,6) -> 8* f0(7,6) -> 8* active0(16) -> 18* active0(8) -> 18*,7,5 f1(49,2) -> 12* f1(44,6) -> 8* f1(19,2) -> 12* f1(4,6) -> 8* f1(11,2) -> 12* f1(16,6) -> 8* f1(6,6) -> 10,16*,8 f1(43,2) -> 12* f1(48,6) -> 8* f1(38,6) -> 8* f1(8,6) -> 8* f1(3,6) -> 8* f1(47,6) -> 8* f1(42,6) -> 8* f1(17,6) -> 8* f1(12,6) -> 8* active1(47) -> 15* active1(42) -> 19* active1(17) -> 15* active1(12) -> 1,5,7,15* active1(44) -> 15* active1(48) -> 19* active1(3) -> 9,7,19*,11 mark1(47) -> 15* mark1(17) -> 18,15* b1() -> 2* f2(49,2) -> 12,44*,38 f2(39,2) -> 12* f2(48,2) -> 12* f2(43,2) -> 44*,12,38 f2(42,2) -> 12* f2(37,2) -> 38* active2(47) -> 15* active2(42) -> 19*,11 active2(44) -> 15* active2(39) -> 11* active2(48) -> 11* active2(38) -> 15* mark2(42) -> 43* mark2(48) -> 43* mark2(3) -> 43*,11,37 f3(48,2) -> 44,12,47* f3(3,2) -> 44,17,47*,12,4 f3(45,2) -> 12,44* f3(42,2) -> 44,17,47*,12 active3(45) -> 43* active3(48) -> 43,19,49*,11 a3() -> 42,48*,39,3,45 5 -> 7* 9 -> 7* problem: Qed