Sure it does, and it's actually easy to demonstrate. :) That's the power of limiting yourself to a regular language. I started typing out psuedo-code, but it's

Sure it does, and it's actually easy to demonstrate. :) That's the power of limiting yourself to a regular language. I started typing out psuedo-code, but it's easier to be informal. Consider: - It's easy to prove that one terminal (character, char-range, etc) is a subset of another. - It's easy to prove that a sequence of terminals is a subset of another. - If there's a disjunction, you just need to prove both branches. If the disjunction is on the "less-than" side, check both branches with AND; if it's on the "greater-than" side, check with OR -- this is because `(A|B) > A` and `(A|B) > B`, but `C > (A|B)` iff `C > A` and `C > B`. - For non-recursive nonterminals, just expand them as they're encountered. - Which only leaves recursion, which is surprisingly easy to deal with as well: If you're trying to prove `A > B`, it amounts to expanding A and B into their right-hand sides and proving those; at some point due to recursion you'll need to prove `A > B` again -- which seems tricky! However, recursion can only happen in a limited manner in a regular language. Being very handwavy because explaining it this way seems most intuitive to me: Recursion can only happen in 'tail' position in a regular language. Thus, by the time you encounter `A > B` for the second time, it happens to be the very last thing which needs to be demonstrated in order for `A > B` to be true -- you've already checked, as it were, one full round of the repetition/looping. Thus the rule is easy: if you encounter `A > B` for a second time, you can just accept it as true! Hopefully that makes sense. Edit for the fun of it (n.b. that I'm using `>` instead of `>=` out of laziness): prove(A > B) -> if seen(A > B): True else: add_to_seen(A > B); prove(rhs(A) > rhs(B)) prove(xA > yB) -> prove_terminal(x > y) && prove(A > B) prove( A|B > C ) -> prove(A > C) || prove(B > C) prove( C > A|B ) -> prove(C > A) && prove(C > B)