Before declaring total victory, we should discuss one issue with the do-calculus. Like any other calculus, it enables the construction of a proof, but it does not help us find one. It is an excellent verifier of a solution but not such a good searcher for one. If you know the correct sequence of transformations, it is easy to demonstrate to others (who are familiar with Rules 1 to 3) that the do-operator can be eliminated. However, if you do not know the correct sequence, it is not easy to discover it, or even to determine whether one exists.
