YES(?,O(n^2)) 13.18/7.18 YES(?,O(n^2)) 13.18/7.19 13.18/7.19 Problem: 13.18/7.19 or(x,x) -> x 13.18/7.19 and(x,x) -> x 13.18/7.19 not(not(x)) -> x 13.18/7.19 not(and(x,y)) -> or(not(x),not(y)) 13.18/7.19 not(or(x,y)) -> and(not(x),not(y)) 13.18/7.19 13.18/7.19 Proof: 13.18/7.19 Complexity Transformation Processor: 13.18/7.19 strict: 13.18/7.19 or(x,x) -> x 13.18/7.19 and(x,x) -> x 13.18/7.19 not(not(x)) -> x 13.18/7.19 not(and(x,y)) -> or(not(x),not(y)) 13.18/7.19 not(or(x,y)) -> and(not(x),not(y)) 13.18/7.19 weak: 13.18/7.19 13.18/7.19 Matrix Interpretation Processor: dim=1 13.18/7.19 13.18/7.19 max_matrix: 13.18/7.19 1 13.18/7.19 interpretation: 13.18/7.19 [not](x0) = x0 + 6, 13.18/7.19 13.18/7.19 [and](x0, x1) = x0 + x1 + 3, 13.18/7.19 13.18/7.19 [or](x0, x1) = x0 + x1 + 3 13.18/7.19 orientation: 13.18/7.19 or(x,x) = 2x + 3 >= x = x 13.18/7.19 13.18/7.19 and(x,x) = 2x + 3 >= x = x 13.18/7.19 13.18/7.19 not(not(x)) = x + 12 >= x = x 13.18/7.19 13.18/7.19 not(and(x,y)) = x + y + 9 >= x + y + 15 = or(not(x),not(y)) 13.18/7.19 13.18/7.19 not(or(x,y)) = x + y + 9 >= x + y + 15 = and(not(x),not(y)) 13.18/7.19 problem: 13.18/7.19 strict: 13.18/7.19 not(and(x,y)) -> or(not(x),not(y)) 13.18/7.19 not(or(x,y)) -> and(not(x),not(y)) 13.18/7.19 weak: 13.18/7.19 or(x,x) -> x 13.18/7.19 and(x,x) -> x 13.18/7.19 not(not(x)) -> x 13.18/7.19 Matrix Interpretation Processor: dim=1 13.18/7.19 13.18/7.19 max_matrix: 13.18/7.19 1 13.18/7.19 interpretation: 13.18/7.19 [not](x0) = x0 + 2, 13.18/7.19 13.18/7.19 [and](x0, x1) = x0 + x1 + 48, 13.18/7.19 13.18/7.19 [or](x0, x1) = x0 + x1 + 12 13.18/7.19 orientation: 13.18/7.19 not(and(x,y)) = x + y + 50 >= x + y + 16 = or(not(x),not(y)) 13.18/7.19 13.18/7.19 not(or(x,y)) = x + y + 14 >= x + y + 52 = and(not(x),not(y)) 13.18/7.19 13.18/7.19 or(x,x) = 2x + 12 >= x = x 13.18/7.19 13.18/7.19 and(x,x) = 2x + 48 >= x = x 13.18/7.19 13.18/7.19 not(not(x)) = x + 4 >= x = x 13.18/7.19 problem: 13.18/7.19 strict: 13.18/7.19 not(or(x,y)) -> and(not(x),not(y)) 13.18/7.19 weak: 13.18/7.19 not(and(x,y)) -> or(not(x),not(y)) 13.18/7.19 or(x,x) -> x 13.18/7.19 and(x,x) -> x 13.18/7.19 not(not(x)) -> x 13.18/7.19 Matrix Interpretation Processor: dim=2 13.18/7.19 13.18/7.19 max_matrix: 13.18/7.19 [1 2] 13.18/7.19 [0 1] 13.18/7.19 interpretation: 13.18/7.19 [1 2] 13.18/7.19 [not](x0) = [0 1]x0, 13.18/7.19 13.18/7.19 [1 2] [0] 13.18/7.19 [and](x0, x1) = x0 + [0 1]x1 + [1], 13.18/7.19 13.18/7.19 [1 2] [1] 13.18/7.19 [or](x0, x1) = x0 + [0 1]x1 + [1] 13.18/7.19 orientation: 13.18/7.19 [1 2] [1 4] [3] [1 2] [1 4] [0] 13.18/7.19 not(or(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = and(not(x),not(y)) 13.18/7.19 13.18/7.19 [1 2] [1 4] [2] [1 2] [1 4] [1] 13.18/7.19 not(and(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = or(not(x),not(y)) 13.18/7.19 13.18/7.19 [2 2] [1] 13.18/7.19 or(x,x) = [0 2]x + [1] >= x = x 13.18/7.19 13.18/7.19 [2 2] [0] 13.18/7.19 and(x,x) = [0 2]x + [1] >= x = x 13.18/7.19 13.18/7.19 [1 4] 13.18/7.19 not(not(x)) = [0 1]x >= x = x 13.18/7.19 problem: 13.18/7.19 strict: 13.18/7.19 13.18/7.19 weak: 13.18/7.19 not(or(x,y)) -> and(not(x),not(y)) 13.18/7.19 not(and(x,y)) -> or(not(x),not(y)) 13.18/7.19 or(x,x) -> x 13.18/7.19 and(x,x) -> x 13.18/7.19 not(not(x)) -> x 13.18/7.19 Qed 13.18/7.19 EOF