YES(?,O(n^3)) Problem: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) Proof: RT Transformation Processor: strict: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) weak: Matrix Interpretation Processor: dimension: 1 interpretation: [tp](x0) = x0, [c] = 0, [y] = 25, [mat](x0, x1) = x0 + x1 + 19, [X] = 7, [chk](x0) = x0 + 13, [no](x0) = x0 + 1, [mark](x0) = x0 + 4, [active](x0) = x0 + 2, [f](x0) = x0 + 1 orientation: active(f(x)) = x + 3 >= x + 6 = mark(f(f(x))) chk(no(f(x))) = x + 15 >= x + 50 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) = x + 46 >= x + 45 = f(mat(x,y())) chk(no(c())) = 14 >= 2 = active(c()) mat(f(x),c()) = x + 20 >= 1 = no(c()) f(active(x)) = x + 3 >= x + 3 = active(f(x)) f(no(x)) = x + 2 >= x + 2 = no(f(x)) f(mark(x)) = x + 5 >= x + 5 = mark(f(x)) tp(mark(x)) = x + 4 >= x + 49 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) problem: strict: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) weak: mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) Matrix Interpretation Processor: dimension: 1 interpretation: [tp](x0) = x0 + 1, [c] = 16, [y] = 12, [mat](x0, x1) = x0 + x1 + 4, [X] = 5, [chk](x0) = x0 + 16, [no](x0) = x0 + 1, [mark](x0) = x0 + 26, [active](x0) = x0 + 4, [f](x0) = x0 orientation: active(f(x)) = x + 4 >= x + 26 = mark(f(f(x))) chk(no(f(x))) = x + 17 >= x + 25 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) f(active(x)) = x + 4 >= x + 4 = active(f(x)) f(no(x)) = x + 1 >= x + 1 = no(f(x)) f(mark(x)) = x + 26 >= x + 26 = mark(f(x)) tp(mark(x)) = x + 27 >= x + 26 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) = x + 16 >= x + 16 = f(mat(x,y())) chk(no(c())) = 33 >= 20 = active(c()) mat(f(x),c()) = x + 20 >= 17 = no(c()) problem: strict: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) weak: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) Matrix Interpretation Processor: dimension: 2 interpretation: [1 0] [1] [tp](x0) = [0 0]x0 + [8], [4] [c] = [0], [2] [y] = [9], [1 7] [1 0] [0] [mat](x0, x1) = [0 0]x0 + [0 0]x1 + [9], [0] [X] = [0], [1 0] [chk](x0) = [0 0]x0, [1 1] [0] [no](x0) = [0 1]x0 + [4], [mark](x0) = x0, [1 2] [active](x0) = [0 1]x0, [1 2] [f](x0) = [0 1]x0 orientation: [1 4] [1 4] active(f(x)) = [0 1]x >= [0 1]x = mark(f(f(x))) [1 3] [1 0] chk(no(f(x))) = [0 0]x >= [0 0]x = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [1 4] [1 4] f(active(x)) = [0 1]x >= [0 1]x = active(f(x)) [1 3] [8] [1 3] [0] f(no(x)) = [0 1]x + [4] >= [0 1]x + [4] = no(f(x)) [1 2] [1 2] f(mark(x)) = [0 1]x >= [0 1]x = mark(f(x)) [1 0] [1] [1 0] [1] tp(mark(x)) = [0 0]x + [8] >= [0 0]x + [8] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [1 9] [20] [1 7] [20] mat(f(x),f(y())) = [0 0]x + [9 ] >= [0 0]x + [9 ] = f(mat(x,y())) [4] [4] chk(no(c())) = [0] >= [0] = active(c()) [1 9] [4] [4] mat(f(x),c()) = [0 0]x + [9] >= [4] = no(c()) problem: strict: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) f(active(x)) -> active(f(x)) f(mark(x)) -> mark(f(x)) weak: f(no(x)) -> no(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) Matrix Interpretation Processor: dimension: 3 interpretation: [1 0 0] [tp](x0) = [0 0 4]x0 [0 0 0] , [6] [c] = [0] [1], [4] [y] = [0] [0], [1 0 0] [1 0 0] [mat](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 1] , [0] [X] = [0] [0], [1 1 6] [0] [chk](x0) = [0 0 5]x0 + [1] [0 0 0] [0], [no](x0) = x0 , [1 0 6] [mark](x0) = [0 1 0]x0 [0 0 1] , [1 0 0] [1] [active](x0) = [0 0 6]x0 + [0] [0 0 0] [0], [1 0 0] [f](x0) = [0 0 6]x0 [0 0 0] orientation: [1 0 0] [1] [1 0 0] active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x = mark(f(f(x))) [0 0 0] [0] [0 0 0] [1 0 6] [0] [1 0 6] chk(no(f(x))) = [0 0 0]x + [1] >= [0 0 0]x = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] [1] f(active(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = active(f(x)) [0 0 0] [0] [0 0 0] [0] [1 0 6] [1 0 0] f(mark(x)) = [0 0 6]x >= [0 0 6]x = mark(f(x)) [0 0 0] [0 0 0] [1 0 0] [1 0 0] f(no(x)) = [0 0 6]x >= [0 0 6]x = no(f(x)) [0 0 0] [0 0 0] [1 0 6] [1 0 6] tp(mark(x)) = [0 0 4]x >= [0 0 0]x = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0] [0 0 0] [1 0 0] [4] [1 0 0] [4] mat(f(x),f(y())) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(mat(x,y())) [0 0 0] [0] [0 0 0] [0] [12] [7] chk(no(c())) = [6 ] >= [6] = active(c()) [0 ] [0] [1 0 0] [6] [6] mat(f(x),c()) = [0 0 0]x + [0] >= [0] = no(c()) [0 0 0] [1] [1] problem: strict: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) f(active(x)) -> active(f(x)) f(mark(x)) -> mark(f(x)) weak: active(f(x)) -> mark(f(f(x))) f(no(x)) -> no(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) Matrix Interpretation Processor: dimension: 3 interpretation: [1 0 0] [0] [tp](x0) = [0 0 0]x0 + [0] [0 0 0] [7], [0] [c] = [3] [5], [5] [y] = [0] [0], [1 0 0] [1 0 1] [mat](x0, x1) = [0 0 0]x0 + [0 0 2]x1 [0 0 0] [0 0 1] , [4] [X] = [0] [0], [1 1 1] [0] [chk](x0) = [0 0 1]x0 + [5] [0 0 0] [1], [5] [no](x0) = x0 + [0] [0], [1 0 4] [4] [mark](x0) = [0 0 0]x0 + [0] [0 0 1] [0], [1 0 0] [6] [active](x0) = [0 0 2]x0 + [0] [0 0 0] [0], [1 0 0] [f](x0) = [0 0 4]x0 [0 0 0] orientation: [1 0 4] [5] [1 0 4] [4] chk(no(f(x))) = [0 0 0]x + [5] >= [0 0 0]x + [4] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0] [1] [0 0 0] [0] [1 0 0] [6] [1 0 0] [6] f(active(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = active(f(x)) [0 0 0] [0] [0 0 0] [0] [1 0 4] [4] [1 0 0] [4] f(mark(x)) = [0 0 4]x + [0] >= [0 0 0]x + [0] = mark(f(x)) [0 0 0] [0] [0 0 0] [0] [1 0 0] [6] [1 0 0] [4] active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(f(f(x))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [5] [1 0 0] [5] f(no(x)) = [0 0 4]x + [0] >= [0 0 4]x + [0] = no(f(x)) [0 0 0] [0] [0 0 0] [0] [1 0 4] [4] [1 0 4] [4] tp(mark(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0] [7] [0 0 0] [7] [1 0 0] [5] [1 0 0] [5] mat(f(x),f(y())) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(mat(x,y())) [0 0 0] [0] [0 0 0] [0] [13] [6 ] chk(no(c())) = [10] >= [10] = active(c()) [1 ] [0 ] [1 0 0] [5 ] [5] mat(f(x),c()) = [0 0 0]x + [10] >= [3] = no(c()) [0 0 0] [5 ] [5] problem: strict: f(active(x)) -> active(f(x)) f(mark(x)) -> mark(f(x)) weak: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) active(f(x)) -> mark(f(f(x))) f(no(x)) -> no(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) Matrix Interpretation Processor: dimension: 3 interpretation: [1 0 7] [0] [tp](x0) = [0 0 5]x0 + [1] [0 0 0] [0], [0] [c] = [0] [1], [6] [y] = [0] [0], [1 0 4] [1 0 2] [mat](x0, x1) = [0 0 0]x0 + [0 0 3]x1 [0 0 0] [0 0 1] , [2] [X] = [0] [0], [1 4 0] [0] [chk](x0) = [0 0 0]x0 + [4] [0 0 0] [0], [1 1 0] [2] [no](x0) = [0 1 1]x0 + [2] [0 0 1] [0], [1 0 7] [2] [mark](x0) = [0 1 0]x0 + [0] [0 0 1] [0], [1 2 5] [2] [active](x0) = [0 1 2]x0 + [2] [0 0 0] [0], [1 2 4] [f](x0) = [0 1 2]x0 [0 0 0] orientation: [1 4 9] [6] [1 4 8] [2] f(active(x)) = [0 1 2]x + [2] >= [0 1 2]x + [2] = active(f(x)) [0 0 0] [0] [0 0 0] [0] [1 2 11] [2] [1 2 4] [2] f(mark(x)) = [0 1 2 ]x + [0] >= [0 1 2]x + [0] = mark(f(x)) [0 0 0 ] [0] [0 0 0] [0] [1 7 14] [10] [1 0 14] [10] chk(no(f(x))) = [0 0 0 ]x + [4 ] >= [0 0 0 ]x + [4 ] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0 ] [0 ] [0 0 0 ] [0 ] [1 4 8] [2] [1 4 8] [2] active(f(x)) = [0 1 2]x + [2] >= [0 1 2]x + [0] = mark(f(f(x))) [0 0 0] [0] [0 0 0] [0] [1 3 6] [6] [1 3 6] [2] f(no(x)) = [0 1 3]x + [2] >= [0 1 2]x + [2] = no(f(x)) [0 0 0] [0] [0 0 0] [0] [1 0 14] [2] [1 0 14] [2] tp(mark(x)) = [0 0 5 ]x + [1] >= [0 0 0 ]x + [1] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0 ] [0] [0 0 0 ] [0] [1 2 4] [6] [1 0 4] [6] mat(f(x),f(y())) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(mat(x,y())) [0 0 0] [0] [0 0 0] [0] [14] [7] chk(no(c())) = [4 ] >= [4] = active(c()) [0 ] [0] [1 2 4] [2] [2] mat(f(x),c()) = [0 0 0]x + [3] >= [3] = no(c()) [0 0 0] [1] [1] problem: strict: f(mark(x)) -> mark(f(x)) weak: f(active(x)) -> active(f(x)) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) active(f(x)) -> mark(f(f(x))) f(no(x)) -> no(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) Matrix Interpretation Processor: dimension: 3 interpretation: [1 0 1] [0] [tp](x0) = [0 0 1]x0 + [0] [0 0 1] [1], [0] [c] = [0] [0], [0] [y] = [0] [1], [1 0 0] [1 0 0] [0] [mat](x0, x1) = [0 0 0]x0 + [0 0 1]x1 + [0] [0 0 0] [0 0 0] [1], [0] [X] = [0] [0], [1 1 0] [6] [chk](x0) = [0 0 4]x0 + [1] [0 0 0] [1], [no](x0) = x0 , [1 0 0] [6] [mark](x0) = [0 0 0]x0 + [0] [0 0 1] [1], [1 1 4] [6] [active](x0) = [0 0 0]x0 + [0] [0 0 1] [1], [1 0 1] [0] [f](x0) = [0 0 0]x0 + [1] [0 0 1] [0] orientation: [1 0 1] [7] [1 0 1] [6] f(mark(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = mark(f(x)) [0 0 1] [1] [0 0 1] [1] [1 1 5] [7] [1 0 5] [7] f(active(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = active(f(x)) [0 0 1] [1] [0 0 1] [1] [1 0 1] [7] [1 0 1] [7] chk(no(f(x))) = [0 0 4]x + [1] >= [0 0 0]x + [1] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0] [1] [0 0 0] [1] [1 0 5] [7] [1 0 2] [6] active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(f(f(x))) [0 0 1] [1] [0 0 1] [1] [1 0 1] [0] [1 0 1] [0] f(no(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = no(f(x)) [0 0 1] [0] [0 0 1] [0] [1 0 1] [7] [1 0 1] [7] tp(mark(x)) = [0 0 1]x + [1] >= [0 0 0]x + [1] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 1] [2] [0 0 0] [2] [1 0 1] [1] [1 0 0] [1] mat(f(x),f(y())) = [0 0 0]x + [1] >= [0 0 0]x + [1] = f(mat(x,y())) [0 0 0] [1] [0 0 0] [1] [6] [6] chk(no(c())) = [1] >= [0] = active(c()) [1] [1] [1 0 1] [0] [0] mat(f(x),c()) = [0 0 0]x + [0] >= [0] = no(c()) [0 0 0] [1] [0] problem: strict: weak: f(mark(x)) -> mark(f(x)) f(active(x)) -> active(f(x)) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) active(f(x)) -> mark(f(f(x))) f(no(x)) -> no(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) Qed