As stated in the title, I need a decision procedure for the problem of regular expression equivalence with not. Wikipedia states the problem is in the NONELEMENTARY complexity class. All I really need is link to the paper that describes the problem and its solution. This is NOT a homework problem. I need the procedure for a program static analysis tool.