YES(?,O(n^1)) 0.16/0.21 YES(?,O(n^1)) 0.16/0.21 0.16/0.21 Problem: 0.16/0.21 -(-(neg(x),neg(x)),-(neg(y),neg(y))) -> -(-(x,y),-(x,y)) 0.16/0.21 0.16/0.21 Proof: 0.16/0.21 Bounds Processor: 0.16/0.21 bound: 1 0.16/0.21 enrichment: match 0.16/0.21 automaton: 0.16/0.21 final states: {2,1} 0.16/0.21 transitions: 0.16/0.21 -0(1,2) -> 1* 0.16/0.21 -0(2,1) -> 1* 0.16/0.21 -0(1,1) -> 1* 0.16/0.21 -0(2,2) -> 1* 0.16/0.21 neg0(2) -> 2* 0.16/0.21 neg0(1) -> 2* 0.16/0.21 -1(1,2) -> 1* 0.16/0.21 -1(2,1) -> 1* 0.16/0.21 -1(1,1) -> 1* 0.16/0.21 -1(2,2) -> 1* 0.16/0.21 problem: 0.16/0.21 0.16/0.21 Qed 0.16/0.21 EOF