YES(?,O(n^2)) 67.36/33.62 YES(?,O(n^2)) 67.36/33.63 67.36/33.63 Problem: 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 67.36/33.63 Proof: 67.36/33.63 Complexity Transformation Processor: 67.36/33.63 strict: 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 weak: 67.36/33.63 67.36/33.63 Splitting Processor: 67.36/33.63 strict: 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 weak: 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 Matrix Interpretation Processor: dim=4 67.36/33.63 67.36/33.63 max_matrix: 67.36/33.63 [1 0 0 1] 67.36/33.63 [0 0 1 1] 67.36/33.63 [0 0 0 0] 67.36/33.63 [0 0 0 1] 67.36/33.63 interpretation: 67.36/33.63 [1 0 0 1] [0] 67.36/33.63 [0 0 0 1] [1] 67.36/33.63 [b](x0) = [0 0 0 0]x0 + [1] 67.36/33.63 [0 0 0 1] [0], 67.36/33.63 67.36/33.63 [1 0 0 1] 67.36/33.63 [0 0 1 1] 67.36/33.63 [w](x0) = [0 0 0 0]x0 67.36/33.63 [0 0 0 1] , 67.36/33.63 67.36/33.63 [1 0 0 0] [1] 67.36/33.63 [0 0 0 0] [0] 67.36/33.63 [r](x0) = [0 0 0 0]x0 + [0] 67.36/33.63 [0 0 0 1] [1] 67.36/33.63 orientation: 67.36/33.63 [1 0 0 1] [2] [1 0 0 1] [1] 67.36/33.63 [0 0 0 1] [1] [0 0 0 0] [0] 67.36/33.63 w(r(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = r(w(x)) 67.36/33.63 [0 0 0 1] [1] [0 0 0 1] [1] 67.36/33.63 67.36/33.63 [1 0 0 1] [2] [1 0 0 1] [1] 67.36/33.63 [0 0 0 1] [2] [0 0 0 0] [0] 67.36/33.63 b(r(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [0] = r(b(x)) 67.36/33.63 [0 0 0 1] [1] [0 0 0 1] [1] 67.36/33.63 67.36/33.63 [1 0 0 2] [0] [1 0 0 2] [0] 67.36/33.63 [0 0 0 1] [1] [0 0 0 1] [1] 67.36/33.63 b(w(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [0] = w(b(x)) 67.36/33.63 [0 0 0 1] [0] [0 0 0 1] [0] 67.36/33.63 problem: 67.36/33.63 strict: 67.36/33.63 67.36/33.63 weak: 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 Qed 67.36/33.63 67.36/33.63 strict: 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 weak: 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 Splitting Processor: 67.36/33.63 strict: 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 weak: 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 Matrix Interpretation Processor: dim=2 67.36/33.63 67.36/33.63 max_matrix: 67.36/33.63 [1 4] 67.36/33.63 [0 1] 67.36/33.63 interpretation: 67.36/33.63 [1 1] [5] 67.36/33.63 [b](x0) = [0 1]x0 + [0], 67.36/33.63 67.36/33.63 [1 4] [1] 67.36/33.63 [w](x0) = [0 1]x0 + [2], 67.36/33.63 67.36/33.63 [3] 67.36/33.63 [r](x0) = x0 + [1] 67.36/33.63 orientation: 67.36/33.63 [1 5] [8] [1 5] [6] 67.36/33.63 b(w(x)) = [0 1]x + [2] >= [0 1]x + [2] = w(b(x)) 67.36/33.63 67.36/33.63 [1 1] [9] [1 1] [8] 67.36/33.63 b(r(x)) = [0 1]x + [1] >= [0 1]x + [1] = r(b(x)) 67.36/33.63 67.36/33.63 [1 4] [8] [1 4] [4] 67.36/33.63 w(r(x)) = [0 1]x + [3] >= [0 1]x + [3] = r(w(x)) 67.36/33.63 problem: 67.36/33.63 strict: 67.36/33.63 67.36/33.63 weak: 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 Qed 67.36/33.63 67.36/33.63 strict: 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 weak: 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 Matrix Interpretation Processor: dim=4 67.36/33.63 67.36/33.63 max_matrix: 67.36/33.63 [1 1 0 1] 67.36/33.63 [0 1 0 1] 67.36/33.63 [0 0 0 0] 67.36/33.63 [0 0 0 0] 67.36/33.63 interpretation: 67.36/33.63 [1 1 0 1] [0] 67.36/33.63 [0 1 0 1] [0] 67.36/33.63 [b](x0) = [0 0 0 0]x0 + [1] 67.36/33.63 [0 0 0 0] [0], 67.36/33.63 67.36/33.63 [1 1 0 1] [0] 67.36/33.63 [0 1 0 1] [1] 67.36/33.63 [w](x0) = [0 0 0 0]x0 + [0] 67.36/33.63 [0 0 0 0] [0], 67.36/33.63 67.36/33.63 [1 1 0 1] [0] 67.36/33.63 [0 1 0 1] [1] 67.36/33.63 [r](x0) = [0 0 0 0]x0 + [0] 67.36/33.63 [0 0 0 0] [0] 67.36/33.63 orientation: 67.36/33.63 [1 2 0 2] [1] [1 2 0 2] [0] 67.36/33.63 [0 1 0 1] [1] [0 1 0 1] [1] 67.36/33.63 b(r(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [0] = r(b(x)) 67.36/33.63 [0 0 0 0] [0] [0 0 0 0] [0] 67.36/33.63 67.36/33.63 [1 2 0 2] [1] [1 2 0 2] [1] 67.36/33.63 [0 1 0 1] [2] [0 1 0 1] [2] 67.36/33.63 w(r(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = r(w(x)) 67.36/33.63 [0 0 0 0] [0] [0 0 0 0] [0] 67.36/33.63 67.36/33.63 [1 2 0 2] [1] [1 2 0 2] [0] 67.36/33.63 [0 1 0 1] [1] [0 1 0 1] [1] 67.36/33.63 b(w(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [0] = w(b(x)) 67.36/33.63 [0 0 0 0] [0] [0 0 0 0] [0] 67.36/33.63 problem: 67.36/33.63 strict: 67.36/33.63 67.36/33.63 weak: 67.36/33.63 b(r(x)) -> r(b(x)) 67.36/33.63 w(r(x)) -> r(w(x)) 67.36/33.63 b(w(x)) -> w(b(x)) 67.36/33.63 Qed 67.36/33.63 EOF