YES Problem: or(x,x) -> x and(x,x) -> x not(not(x)) -> x not(and(x,y)) -> or(not(x),not(y)) not(or(x,y)) -> and(not(x),not(y)) Proof: DP Processor: DPs: not#(and(x,y)) -> not#(y) not#(and(x,y)) -> not#(x) not#(and(x,y)) -> or#(not(x),not(y)) not#(or(x,y)) -> not#(y) not#(or(x,y)) -> not#(x) not#(or(x,y)) -> and#(not(x),not(y)) TRS: or(x,x) -> x and(x,x) -> x not(not(x)) -> x not(and(x,y)) -> or(not(x),not(y)) not(or(x,y)) -> and(not(x),not(y)) ADG Processor: DPs: not#(and(x,y)) -> not#(y) not#(and(x,y)) -> not#(x) not#(and(x,y)) -> or#(not(x),not(y)) not#(or(x,y)) -> not#(y) not#(or(x,y)) -> not#(x) not#(or(x,y)) -> and#(not(x),not(y)) TRS: or(x,x) -> x and(x,x) -> x not(not(x)) -> x not(and(x,y)) -> or(not(x),not(y)) not(or(x,y)) -> and(not(x),not(y)) graph: not#(and(x,y)) -> not#(y) -> not#(and(x,y)) -> not#(y) not#(and(x,y)) -> not#(y) -> not#(and(x,y)) -> not#(x) not#(and(x,y)) -> not#(y) -> not#(and(x,y)) -> or#(not(x),not(y)) not#(and(x,y)) -> not#(y) -> not#(or(x,y)) -> not#(y) not#(and(x,y)) -> not#(y) -> not#(or(x,y)) -> not#(x) not#(and(x,y)) -> not#(y) -> not#(or(x,y)) -> and#(not(x),not(y)) not#(and(x,y)) -> not#(x) -> not#(and(x,y)) -> not#(y) not#(and(x,y)) -> not#(x) -> not#(and(x,y)) -> not#(x) not#(and(x,y)) -> not#(x) -> not#(and(x,y)) -> or#(not(x),not(y)) not#(and(x,y)) -> not#(x) -> not#(or(x,y)) -> not#(y) not#(and(x,y)) -> not#(x) -> not#(or(x,y)) -> not#(x) not#(and(x,y)) -> not#(x) -> not#(or(x,y)) -> and#(not(x),not(y)) not#(or(x,y)) -> not#(y) -> not#(and(x,y)) -> not#(y) not#(or(x,y)) -> not#(y) -> not#(and(x,y)) -> not#(x) not#(or(x,y)) -> not#(y) -> not#(and(x,y)) -> or#(not(x),not(y)) not#(or(x,y)) -> not#(y) -> not#(or(x,y)) -> not#(y) not#(or(x,y)) -> not#(y) -> not#(or(x,y)) -> not#(x) not#(or(x,y)) -> not#(y) -> not#(or(x,y)) -> and#(not(x),not(y)) not#(or(x,y)) -> not#(x) -> not#(and(x,y)) -> not#(y) not#(or(x,y)) -> not#(x) -> not#(and(x,y)) -> not#(x) not#(or(x,y)) -> not#(x) -> not#(and(x,y)) -> or#(not(x),not(y)) not#(or(x,y)) -> not#(x) -> not#(or(x,y)) -> not#(y) not#(or(x,y)) -> not#(x) -> not#(or(x,y)) -> not#(x) not#(or(x,y)) -> not#(x) -> not#(or(x,y)) -> and#(not(x),not(y)) Restore Modifier: DPs: not#(and(x,y)) -> not#(y) not#(and(x,y)) -> not#(x) not#(and(x,y)) -> or#(not(x),not(y)) not#(or(x,y)) -> not#(y) not#(or(x,y)) -> not#(x) not#(or(x,y)) -> and#(not(x),not(y)) TRS: or(x,x) -> x and(x,x) -> x not(not(x)) -> x not(and(x,y)) -> or(not(x),not(y)) not(or(x,y)) -> and(not(x),not(y)) SCC Processor: #sccs: 1 #rules: 4 #arcs: 24/36 DPs: not#(and(x,y)) -> not#(y) not#(or(x,y)) -> not#(x) not#(or(x,y)) -> not#(y) not#(and(x,y)) -> not#(x) TRS: or(x,x) -> x and(x,x) -> x not(not(x)) -> x not(and(x,y)) -> or(not(x),not(y)) not(or(x,y)) -> and(not(x),not(y)) Matrix Interpretation Processor: dimension: 1 interpretation: [not#](x0) = x0 + 1, [not](x0) = x0, [and](x0, x1) = x0 + x1 + 1, [or](x0, x1) = x0 + x1 + 1 orientation: not#(and(x,y)) = x + y + 2 >= y + 1 = not#(y) not#(or(x,y)) = x + y + 2 >= x + 1 = not#(x) not#(or(x,y)) = x + y + 2 >= y + 1 = not#(y) not#(and(x,y)) = x + y + 2 >= x + 1 = not#(x) or(x,x) = 2x + 1 >= x = x and(x,x) = 2x + 1 >= x = x not(not(x)) = x >= x = x not(and(x,y)) = x + y + 1 >= x + y + 1 = or(not(x),not(y)) not(or(x,y)) = x + y + 1 >= x + y + 1 = and(not(x),not(y)) problem: DPs: TRS: or(x,x) -> x and(x,x) -> x not(not(x)) -> x not(and(x,y)) -> or(not(x),not(y)) not(or(x,y)) -> and(not(x),not(y)) Qed