Represent the polynomial binary certificate by two guessed relation tables. A concrete polynomial preprocessor and the original NP verifier decide the expanded ordered query. Reuse the Immerman–Vardi computation rules, eliminate their least fixed point by exact iteration tables, project the certificate relations, patch the two smallest domains, and remove the guessed order using isomorphism invariance of the original property.