YES(?,O(n^2)) 70.74/21.49 YES(?,O(n^2)) 70.85/21.50 70.85/21.50 Problem: 70.85/21.50 active(f(x)) -> mark(f(f(x))) 70.85/21.50 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.50 chk(no(c())) -> active(c()) 70.85/21.50 mat(f(x),c()) -> no(c()) 70.85/21.50 f(active(x)) -> active(f(x)) 70.85/21.50 f(no(x)) -> no(f(x)) 70.85/21.50 f(mark(x)) -> mark(f(x)) 70.85/21.50 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 70.85/21.50 Proof: 70.85/21.50 Complexity Transformation Processor: 70.85/21.50 strict: 70.85/21.50 active(f(x)) -> mark(f(f(x))) 70.85/21.50 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.50 chk(no(c())) -> active(c()) 70.85/21.50 mat(f(x),c()) -> no(c()) 70.85/21.50 f(active(x)) -> active(f(x)) 70.85/21.50 f(no(x)) -> no(f(x)) 70.85/21.50 f(mark(x)) -> mark(f(x)) 70.85/21.50 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 weak: 70.85/21.50 70.85/21.50 Matrix Interpretation Processor: dim=1 70.85/21.50 70.85/21.50 max_matrix: 70.85/21.50 1 70.85/21.50 interpretation: 70.85/21.50 [tp](x0) = x0 + 42, 70.85/21.50 70.85/21.50 [c] = 56, 70.85/21.50 70.85/21.50 [y] = 96, 70.85/21.50 70.85/21.50 [mat](x0, x1) = x0 + x1 + 82, 70.85/21.50 70.85/21.50 [X] = 0, 70.85/21.50 70.85/21.50 [chk](x0) = x0 + 70, 70.85/21.50 70.85/21.50 [no](x0) = x0 + 226, 70.85/21.50 70.85/21.50 [mark](x0) = x0 + 192, 70.85/21.50 70.85/21.50 [active](x0) = x0 + 8, 70.85/21.50 70.85/21.50 [f](x0) = x0 70.85/21.50 orientation: 70.85/21.50 active(f(x)) = x + 8 >= x + 192 = mark(f(f(x))) 70.85/21.50 70.85/21.50 chk(no(f(x))) = x + 296 >= x + 152 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 70.85/21.50 mat(f(x),f(y())) = x + 178 >= x + 178 = f(mat(x,y())) 70.85/21.50 70.85/21.50 chk(no(c())) = 352 >= 64 = active(c()) 70.85/21.50 70.85/21.50 mat(f(x),c()) = x + 138 >= 282 = no(c()) 70.85/21.50 70.85/21.50 f(active(x)) = x + 8 >= x + 8 = active(f(x)) 70.85/21.50 70.85/21.50 f(no(x)) = x + 226 >= x + 226 = no(f(x)) 70.85/21.50 70.85/21.50 f(mark(x)) = x + 192 >= x + 192 = mark(f(x)) 70.85/21.50 70.85/21.50 tp(mark(x)) = x + 234 >= x + 194 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 problem: 70.85/21.50 strict: 70.85/21.50 active(f(x)) -> mark(f(f(x))) 70.85/21.50 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.50 mat(f(x),c()) -> no(c()) 70.85/21.50 f(active(x)) -> active(f(x)) 70.85/21.50 f(no(x)) -> no(f(x)) 70.85/21.50 f(mark(x)) -> mark(f(x)) 70.85/21.50 weak: 70.85/21.50 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 chk(no(c())) -> active(c()) 70.85/21.50 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 Matrix Interpretation Processor: dim=1 70.85/21.50 70.85/21.50 max_matrix: 70.85/21.50 1 70.85/21.50 interpretation: 70.85/21.50 [tp](x0) = x0 + 2, 70.85/21.50 70.85/21.50 [c] = 4, 70.85/21.50 70.85/21.50 [y] = 120, 70.85/21.50 70.85/21.50 [mat](x0, x1) = x0 + x1 + 8, 70.85/21.50 70.85/21.50 [X] = 4, 70.85/21.50 70.85/21.50 [chk](x0) = x0 + 28, 70.85/21.50 70.85/21.50 [no](x0) = x0 + 52, 70.85/21.50 70.85/21.50 [mark](x0) = x0 + 40, 70.85/21.50 70.85/21.50 [active](x0) = x0 + 80, 70.85/21.50 70.85/21.50 [f](x0) = x0 70.85/21.50 orientation: 70.85/21.50 active(f(x)) = x + 80 >= x + 40 = mark(f(f(x))) 70.85/21.50 70.85/21.50 mat(f(x),f(y())) = x + 128 >= x + 128 = f(mat(x,y())) 70.85/21.50 70.85/21.50 mat(f(x),c()) = x + 12 >= 56 = no(c()) 70.85/21.50 70.85/21.50 f(active(x)) = x + 80 >= x + 80 = active(f(x)) 70.85/21.50 70.85/21.50 f(no(x)) = x + 52 >= x + 52 = no(f(x)) 70.85/21.50 70.85/21.50 f(mark(x)) = x + 40 >= x + 40 = mark(f(x)) 70.85/21.50 70.85/21.50 chk(no(f(x))) = x + 80 >= x + 40 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 70.85/21.50 chk(no(c())) = 84 >= 84 = active(c()) 70.85/21.50 70.85/21.50 tp(mark(x)) = x + 42 >= x + 42 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 problem: 70.85/21.50 strict: 70.85/21.50 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.50 mat(f(x),c()) -> no(c()) 70.85/21.50 f(active(x)) -> active(f(x)) 70.85/21.50 f(no(x)) -> no(f(x)) 70.85/21.50 f(mark(x)) -> mark(f(x)) 70.85/21.50 weak: 70.85/21.50 active(f(x)) -> mark(f(f(x))) 70.85/21.50 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 chk(no(c())) -> active(c()) 70.85/21.50 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 Matrix Interpretation Processor: dim=1 70.85/21.50 70.85/21.50 max_matrix: 70.85/21.50 1 70.85/21.50 interpretation: 70.85/21.50 [tp](x0) = x0, 70.85/21.50 70.85/21.50 [c] = 0, 70.85/21.50 70.85/21.50 [y] = 2, 70.85/21.50 70.85/21.50 [mat](x0, x1) = x0 + x1, 70.85/21.50 70.85/21.50 [X] = 0, 70.85/21.50 70.85/21.50 [chk](x0) = x0 + 4, 70.85/21.50 70.85/21.50 [no](x0) = x0 + 22, 70.85/21.50 70.85/21.50 [mark](x0) = x0 + 24, 70.85/21.50 70.85/21.50 [active](x0) = x0 + 26, 70.85/21.50 70.85/21.50 [f](x0) = x0 + 2 70.85/21.50 orientation: 70.85/21.50 mat(f(x),f(y())) = x + 6 >= x + 4 = f(mat(x,y())) 70.85/21.50 70.85/21.50 mat(f(x),c()) = x + 2 >= 22 = no(c()) 70.85/21.50 70.85/21.50 f(active(x)) = x + 28 >= x + 28 = active(f(x)) 70.85/21.50 70.85/21.50 f(no(x)) = x + 24 >= x + 24 = no(f(x)) 70.85/21.50 70.85/21.50 f(mark(x)) = x + 26 >= x + 26 = mark(f(x)) 70.85/21.50 70.85/21.50 active(f(x)) = x + 28 >= x + 28 = mark(f(f(x))) 70.85/21.50 70.85/21.50 chk(no(f(x))) = x + 28 >= x + 26 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 70.85/21.50 chk(no(c())) = 26 >= 26 = active(c()) 70.85/21.50 70.85/21.50 tp(mark(x)) = x + 24 >= x + 24 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 problem: 70.85/21.50 strict: 70.85/21.50 mat(f(x),c()) -> no(c()) 70.85/21.50 f(active(x)) -> active(f(x)) 70.85/21.50 f(no(x)) -> no(f(x)) 70.85/21.50 f(mark(x)) -> mark(f(x)) 70.85/21.50 weak: 70.85/21.50 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.50 active(f(x)) -> mark(f(f(x))) 70.85/21.50 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 chk(no(c())) -> active(c()) 70.85/21.50 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 Splitting Processor: 70.85/21.50 strict: 70.85/21.50 f(no(x)) -> no(f(x)) 70.85/21.50 weak: 70.85/21.50 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.50 active(f(x)) -> mark(f(f(x))) 70.85/21.50 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 chk(no(c())) -> active(c()) 70.85/21.50 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 mat(f(x),c()) -> no(c()) 70.85/21.50 f(active(x)) -> active(f(x)) 70.85/21.50 f(mark(x)) -> mark(f(x)) 70.85/21.50 Splitting Processor: 70.85/21.50 strict: 70.85/21.50 mat(f(x),c()) -> no(c()) 70.85/21.50 weak: 70.85/21.50 f(no(x)) -> no(f(x)) 70.85/21.50 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.50 active(f(x)) -> mark(f(f(x))) 70.85/21.50 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 chk(no(c())) -> active(c()) 70.85/21.50 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.50 f(active(x)) -> active(f(x)) 70.85/21.50 f(mark(x)) -> mark(f(x)) 70.85/21.50 Bounds Processor: 70.85/21.50 bound: 2 70.85/21.50 enrichment: match 70.85/21.50 automaton: 70.85/21.50 final states: {11} 70.85/21.50 transitions: 70.85/21.50 no1(15) -> 48,15 70.85/21.50 no1(16) -> 16* 70.85/21.50 no1(13) -> 13,16,15,28,11 70.85/21.50 c1() -> 13* 70.85/21.50 tp1(29) -> 11* 70.85/21.50 chk1(28) -> 29* 70.85/21.50 mat1(27,16) -> 28* 70.85/21.50 mat1(29,32) -> 29* 70.85/21.50 mat1(27,11) -> 28* 70.85/21.50 mat1(26,32) -> 33* 70.85/21.50 mat1(27,13) -> 28* 70.85/21.50 mat1(27,15) -> 28* 70.85/21.50 mat1(27,29) -> 28* 70.85/21.50 mat1(27,49) -> 28* 70.85/21.50 mat1(27,69) -> 28* 70.85/21.50 f1(25) -> 26* 70.85/21.50 f1(20) -> 21* 70.85/21.50 f1(15) -> 16* 70.85/21.50 f1(22) -> 23* 70.85/21.50 f1(17) -> 18* 70.85/21.50 f1(69) -> 13* 70.85/21.50 f1(49) -> 13* 70.85/21.50 f1(29) -> 29,11 70.85/21.50 f1(24) -> 25* 70.85/21.50 f1(19) -> 20* 70.85/21.50 f1(26) -> 27* 70.85/21.50 f1(21) -> 22* 70.85/21.50 f1(16) -> 13* 70.85/21.50 f1(11) -> 15* 70.85/21.50 f1(33) -> 28* 70.85/21.50 f1(23) -> 24* 70.85/21.50 f1(18) -> 19* 70.85/21.50 f1(13) -> 13* 70.85/21.50 X1() -> 17* 70.85/21.50 active1(15) -> 48,15 70.85/21.50 active1(16) -> 16* 70.85/21.50 active1(13) -> 13,16,15,29,11 70.85/21.50 mark1(15) -> 48,15,11 70.85/21.50 mark1(16) -> 16,15,11 70.85/21.50 mark1(13) -> 13,16,15,11 70.85/21.50 y1() -> 32* 70.85/21.50 no2(47) -> 61,28 70.85/21.50 no2(49) -> 48,13,49 70.85/21.50 no2(48) -> 49,48 70.85/21.50 mat0(11,11) -> 11* 70.85/21.50 c2() -> 47* 70.85/21.50 f0(11) -> 11* 70.85/21.50 active2(47) -> 62,29 70.85/21.50 active2(69) -> 29,11 70.85/21.50 active2(49) -> 16,13,49,15,11,29,48 70.85/21.50 active2(48) -> 49,48 70.85/21.50 c0() -> 11* 70.85/21.50 f2(55) -> 56* 70.85/21.50 f2(50) -> 51* 70.85/21.50 f2(15) -> 48* 70.85/21.50 f2(62) -> 29* 70.85/21.50 f2(57) -> 58* 70.85/21.50 f2(52) -> 53* 70.85/21.50 f2(47) -> 69* 70.85/21.50 f2(69) -> 49* 70.85/21.50 f2(59) -> 60* 70.85/21.50 f2(54) -> 55* 70.85/21.50 f2(49) -> 49* 70.85/21.50 f2(56) -> 57* 70.85/21.50 f2(51) -> 52* 70.85/21.50 f2(16) -> 48* 70.85/21.50 f2(11) -> 48* 70.85/21.50 f2(68) -> 29* 70.85/21.50 f2(58) -> 59* 70.85/21.50 f2(53) -> 54* 70.85/21.50 f2(48) -> 49* 70.85/21.50 f2(13) -> 48* 70.85/21.50 no0(11) -> 11* 70.85/21.50 chk2(67) -> 68* 70.85/21.50 chk2(61) -> 62* 70.85/21.50 y0() -> 11* 70.85/21.50 mat2(60,13) -> 61* 70.85/21.50 mat2(60,49) -> 67* 70.85/21.50 mat2(60,69) -> 61* 70.85/21.50 mat2(60,16) -> 61* 70.85/21.50 active0(11) -> 11* 70.85/21.50 X2() -> 50* 70.85/21.50 mark0(11) -> 11* 70.85/21.50 mark2(49) -> 49,13,48,16,29,11,15 70.85/21.50 mark2(48) -> 49,48 70.85/21.50 chk0(11) -> 11* 70.85/21.50 tp2(68) -> 11* 70.85/21.51 X0() -> 11* 70.85/21.51 tp0(11) -> 11* 70.85/21.51 problem: 70.85/21.51 strict: 70.85/21.51 70.85/21.51 weak: 70.85/21.51 mat(f(x),c()) -> no(c()) 70.85/21.51 f(no(x)) -> no(f(x)) 70.85/21.51 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.51 active(f(x)) -> mark(f(f(x))) 70.85/21.51 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.51 chk(no(c())) -> active(c()) 70.85/21.51 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.51 f(active(x)) -> active(f(x)) 70.85/21.51 f(mark(x)) -> mark(f(x)) 70.85/21.51 Qed 70.85/21.51 70.85/21.51 strict: 70.85/21.51 f(active(x)) -> active(f(x)) 70.85/21.51 f(mark(x)) -> mark(f(x)) 70.85/21.51 weak: 70.85/21.51 mat(f(x),c()) -> no(c()) 70.85/21.51 f(no(x)) -> no(f(x)) 70.85/21.51 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.51 active(f(x)) -> mark(f(f(x))) 70.85/21.51 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.51 chk(no(c())) -> active(c()) 70.85/21.51 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.51 Matrix Interpretation Processor: dim=3 70.85/21.51 70.85/21.51 max_matrix: 70.85/21.51 [1 1 1] 70.85/21.51 [0 0 1] 70.85/21.51 [0 0 1] 70.85/21.51 interpretation: 70.85/21.51 [1 0 0] [0] 70.85/21.51 [tp](x0) = [0 0 1]x0 + [1] 70.85/21.51 [0 0 0] [1], 70.85/21.51 70.85/21.51 [0] 70.85/21.51 [c] = [0] 70.85/21.51 [0], 70.85/21.51 70.85/21.51 [0] 70.85/21.51 [y] = [0] 70.85/21.51 [1], 70.85/21.51 70.85/21.51 [1 0 0] [1 0 0] [0] 70.85/21.51 [mat](x0, x1) = [0 0 0]x0 + [0 0 1]x1 + [0] 70.85/21.51 [0 0 0] [0 0 0] [1], 70.85/21.51 70.85/21.51 [0] 70.85/21.51 [X] = [0] 70.85/21.51 [0], 70.85/21.51 70.85/21.51 [1 0 0] [1] 70.85/21.51 [chk](x0) = [0 0 0]x0 + [1] 70.85/21.51 [0 0 0] [1], 70.85/21.51 70.85/21.51 [1 1 0] [0] 70.85/21.51 [no](x0) = [0 0 0]x0 + [0] 70.85/21.51 [0 0 1] [1], 70.85/21.51 70.85/21.51 [1 0 0] [1] 70.85/21.51 [mark](x0) = [0 0 0]x0 + [0] 70.85/21.51 [0 0 1] [1], 70.85/21.51 70.85/21.51 [1 1 1] [0] 70.85/21.51 [active](x0) = [0 0 0]x0 + [0] 70.85/21.51 [0 0 1] [1], 70.85/21.51 70.85/21.51 [1 0 1] [0] 70.85/21.51 [f](x0) = [0 0 0]x0 + [1] 70.85/21.51 [0 0 1] [0] 70.85/21.51 orientation: 70.85/21.51 [1 1 2] [1] [1 0 2] [1] 70.85/21.51 f(active(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = active(f(x)) 70.85/21.51 [0 0 1] [1] [0 0 1] [1] 70.85/21.51 70.85/21.51 [1 0 1] [2] [1 0 1] [1] 70.85/21.51 f(mark(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = mark(f(x)) 70.85/21.51 [0 0 1] [1] [0 0 1] [1] 70.85/21.51 70.85/21.51 [1 0 1] [0] [0] 70.85/21.51 mat(f(x),c()) = [0 0 0]x + [0] >= [0] = no(c()) 70.85/21.51 [0 0 0] [1] [1] 70.85/21.51 70.85/21.51 [1 1 1] [1] [1 0 1] [1] 70.85/21.51 f(no(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = no(f(x)) 70.85/21.51 [0 0 1] [1] [0 0 1] [1] 70.85/21.51 70.85/21.51 [1 0 1] [1] [1 0 0] [1] 70.85/21.51 mat(f(x),f(y())) = [0 0 0]x + [1] >= [0 0 0]x + [1] = f(mat(x,y())) 70.85/21.51 [0 0 0] [1] [0 0 0] [1] 70.85/21.51 70.85/21.51 [1 0 2] [1] [1 0 2] [1] 70.85/21.51 active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(f(f(x))) 70.85/21.51 [0 0 1] [1] [0 0 1] [1] 70.85/21.51 70.85/21.51 [1 0 1] [2] [1 0 0] [2] 70.85/21.51 chk(no(f(x))) = [0 0 0]x + [1] >= [0 0 0]x + [1] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.51 [0 0 0] [1] [0 0 0] [1] 70.85/21.51 70.85/21.51 [1] [0] 70.85/21.51 chk(no(c())) = [1] >= [0] = active(c()) 70.85/21.51 [1] [1] 70.85/21.51 70.85/21.51 [1 0 0] [1] [1 0 0] [1] 70.85/21.52 tp(mark(x)) = [0 0 1]x + [2] >= [0 0 0]x + [2] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 [0 0 0] [1] [0 0 0] [1] 70.85/21.52 problem: 70.85/21.52 strict: 70.85/21.52 f(active(x)) -> active(f(x)) 70.85/21.52 weak: 70.85/21.52 f(mark(x)) -> mark(f(x)) 70.85/21.52 mat(f(x),c()) -> no(c()) 70.85/21.52 f(no(x)) -> no(f(x)) 70.85/21.52 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.52 active(f(x)) -> mark(f(f(x))) 70.85/21.52 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 chk(no(c())) -> active(c()) 70.85/21.52 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 Matrix Interpretation Processor: dim=3 70.85/21.52 70.85/21.52 max_matrix: 70.85/21.52 [1 1 1] 70.85/21.52 [0 0 1] 70.85/21.52 [0 0 1] 70.85/21.52 interpretation: 70.85/21.52 [1 0 0] 70.85/21.52 [tp](x0) = [0 0 1]x0 70.85/21.52 [0 0 0] , 70.85/21.52 70.85/21.52 [0] 70.85/21.52 [c] = [0] 70.85/21.52 [0], 70.85/21.52 70.85/21.52 [1] 70.85/21.52 [y] = [0] 70.85/21.52 [1], 70.85/21.52 70.85/21.52 [1 0 0] [1 0 0] [0] 70.85/21.52 [mat](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1] 70.85/21.52 [0 0 0] [0 0 0] [1], 70.85/21.52 70.85/21.52 [0] 70.85/21.52 [X] = [0] 70.85/21.52 [0], 70.85/21.52 70.85/21.52 [1 0 0] 70.85/21.52 [chk](x0) = [0 0 1]x0 70.85/21.52 [0 0 1] , 70.85/21.52 70.85/21.52 [1 1 0] [0] 70.85/21.52 [no](x0) = [0 0 0]x0 + [0] 70.85/21.52 [0 0 1] [1], 70.85/21.52 70.85/21.52 [1 0 0] [0] 70.85/21.52 [mark](x0) = [0 0 0]x0 + [0] 70.85/21.52 [0 0 1] [1], 70.85/21.52 70.85/21.52 [1 0 1] [0] 70.85/21.52 [active](x0) = [0 0 0]x0 + [0] 70.85/21.52 [0 0 1] [1], 70.85/21.52 70.85/21.52 [1 0 1] [0] 70.85/21.52 [f](x0) = [0 0 0]x0 + [1] 70.85/21.52 [0 0 1] [0] 70.85/21.52 orientation: 70.85/21.52 [1 0 2] [1] [1 0 2] [0] 70.85/21.52 f(active(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = active(f(x)) 70.85/21.52 [0 0 1] [1] [0 0 1] [1] 70.85/21.52 70.85/21.52 [1 0 1] [1] [1 0 1] [0] 70.85/21.52 f(mark(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = mark(f(x)) 70.85/21.52 [0 0 1] [1] [0 0 1] [1] 70.85/21.52 70.85/21.52 [1 0 1] [0] [0] 70.85/21.52 mat(f(x),c()) = [0 0 0]x + [1] >= [0] = no(c()) 70.85/21.52 [0 0 0] [1] [1] 70.85/21.52 70.85/21.52 [1 1 1] [1] [1 0 1] [1] 70.85/21.52 f(no(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = no(f(x)) 70.85/21.52 [0 0 1] [1] [0 0 1] [1] 70.85/21.52 70.85/21.52 [1 0 1] [2] [1 0 0] [2] 70.85/21.52 mat(f(x),f(y())) = [0 0 0]x + [1] >= [0 0 0]x + [1] = f(mat(x,y())) 70.85/21.52 [0 0 0] [1] [0 0 0] [1] 70.85/21.52 70.85/21.52 [1 0 2] [0] [1 0 2] [0] 70.85/21.52 active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(f(f(x))) 70.85/21.52 [0 0 1] [1] [0 0 1] [1] 70.85/21.52 70.85/21.52 [1 0 1] [1] [1 0 0] [1] 70.85/21.52 chk(no(f(x))) = [0 0 1]x + [1] >= [0 0 0]x + [1] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 [0 0 1] [1] [0 0 0] [1] 70.85/21.52 70.85/21.52 [0] [0] 70.85/21.52 chk(no(c())) = [1] >= [0] = active(c()) 70.85/21.52 [1] [1] 70.85/21.52 70.85/21.52 [1 0 0] [0] [1 0 0] [0] 70.85/21.52 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))) 70.85/21.52 [0 0 0] [0] [0 0 0] [0] 70.85/21.52 problem: 70.85/21.52 strict: 70.85/21.52 70.85/21.52 weak: 70.85/21.52 f(active(x)) -> active(f(x)) 70.85/21.52 f(mark(x)) -> mark(f(x)) 70.85/21.52 mat(f(x),c()) -> no(c()) 70.85/21.52 f(no(x)) -> no(f(x)) 70.85/21.52 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.52 active(f(x)) -> mark(f(f(x))) 70.85/21.52 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 chk(no(c())) -> active(c()) 70.85/21.52 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 Qed 70.85/21.52 70.85/21.52 strict: 70.85/21.52 mat(f(x),c()) -> no(c()) 70.85/21.52 f(active(x)) -> active(f(x)) 70.85/21.52 f(mark(x)) -> mark(f(x)) 70.85/21.52 weak: 70.85/21.52 f(no(x)) -> no(f(x)) 70.85/21.52 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.52 active(f(x)) -> mark(f(f(x))) 70.85/21.52 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 chk(no(c())) -> active(c()) 70.85/21.52 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 Matrix Interpretation Processor: dim=3 70.85/21.52 70.85/21.52 max_matrix: 70.85/21.52 [1 1 1] 70.85/21.52 [0 0 1] 70.85/21.52 [0 0 1] 70.85/21.52 interpretation: 70.85/21.52 [1 0 0] [1] 70.85/21.52 [tp](x0) = [0 0 0]x0 + [0] 70.85/21.52 [0 0 0] [1], 70.85/21.52 70.85/21.52 [0] 70.85/21.52 [c] = [0] 70.85/21.52 [0], 70.85/21.52 70.85/21.52 [0] 70.85/21.52 [y] = [1] 70.85/21.52 [0], 70.85/21.52 70.85/21.52 [1 1 0] [1 0 0] [0] 70.85/21.52 [mat](x0, x1) = [0 0 1]x0 + [0 0 0]x1 + [1] 70.85/21.52 [0 0 0] [0 0 0] [1], 70.85/21.52 70.85/21.52 [0] 70.85/21.52 [X] = [0] 70.85/21.52 [0], 70.85/21.52 70.85/21.52 [1 1 0] 70.85/21.52 [chk](x0) = [0 0 0]x0 70.85/21.52 [0 0 0] , 70.85/21.52 70.85/21.52 [1 1 0] [0] 70.85/21.52 [no](x0) = [0 0 1]x0 + [1] 70.85/21.52 [0 0 1] [1], 70.85/21.52 70.85/21.52 [1 1 0] [1] 70.85/21.52 [mark](x0) = [0 0 1]x0 + [0] 70.85/21.52 [0 0 1] [0], 70.85/21.52 70.85/21.52 [1 1 1] [1] 70.85/21.52 [active](x0) = [0 0 1]x0 + [0] 70.85/21.52 [0 0 1] [0], 70.85/21.52 70.85/21.52 [1 1 0] 70.85/21.52 [f](x0) = [0 0 1]x0 70.85/21.52 [0 0 1] 70.85/21.52 orientation: 70.85/21.52 [1 1 1] [1] [1 1 1] [0] 70.85/21.52 f(no(x)) = [0 0 1]x + [1] >= [0 0 1]x + [1] = no(f(x)) 70.85/21.52 [0 0 1] [1] [0 0 1] [1] 70.85/21.52 70.85/21.52 [1 1 1] [1] [1 1 1] [1] 70.85/21.52 mat(f(x),f(y())) = [0 0 1]x + [1] >= [0 0 0]x + [1] = f(mat(x,y())) 70.85/21.52 [0 0 0] [1] [0 0 0] [1] 70.85/21.52 70.85/21.52 [1 1 2] [1] [1 1 2] [1] 70.85/21.52 active(f(x)) = [0 0 1]x + [0] >= [0 0 1]x + [0] = mark(f(f(x))) 70.85/21.52 [0 0 1] [0] [0 0 1] [0] 70.85/21.52 70.85/21.52 [1 1 2] [1] [1 0 0] [1] 70.85/21.52 chk(no(f(x))) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 [0 0 0] [0] [0 0 0] [0] 70.85/21.52 70.85/21.52 [1] [1] 70.85/21.52 chk(no(c())) = [0] >= [0] = active(c()) 70.85/21.52 [0] [0] 70.85/21.52 70.85/21.52 [1 1 0] [2] [1 0 0] [2] 70.85/21.52 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))) 70.85/21.52 [0 0 0] [1] [0 0 0] [1] 70.85/21.52 70.85/21.52 [1 1 1] [0] [0] 70.85/21.52 mat(f(x),c()) = [0 0 1]x + [1] >= [1] = no(c()) 70.85/21.52 [0 0 0] [1] [1] 70.85/21.52 70.85/21.52 [1 1 2] [1] [1 1 2] [1] 70.85/21.52 f(active(x)) = [0 0 1]x + [0] >= [0 0 1]x + [0] = active(f(x)) 70.85/21.52 [0 0 1] [0] [0 0 1] [0] 70.85/21.52 70.85/21.52 [1 1 1] [1] [1 1 1] [1] 70.85/21.52 f(mark(x)) = [0 0 1]x + [0] >= [0 0 1]x + [0] = mark(f(x)) 70.85/21.52 [0 0 1] [0] [0 0 1] [0] 70.85/21.52 problem: 70.85/21.52 strict: 70.85/21.52 70.85/21.52 weak: 70.85/21.52 f(no(x)) -> no(f(x)) 70.85/21.52 mat(f(x),f(y())) -> f(mat(x,y())) 70.85/21.52 active(f(x)) -> mark(f(f(x))) 70.85/21.52 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 chk(no(c())) -> active(c()) 70.85/21.52 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) 70.85/21.52 mat(f(x),c()) -> no(c()) 70.85/21.52 f(active(x)) -> active(f(x)) 70.85/21.52 f(mark(x)) -> mark(f(x)) 70.85/21.52 Qed 70.85/21.53 EOF