In 1952 the following paper called "The Problem of Simplifying Truth Functions" was published. Quine developed the method of simplifying a truth function based on the following two theorems:
The idea is to make a table of clauses of the dnf as abscissas and prime implicants as ordinates. Then we put a cross in entries where the corresponding prime implicant is subsumed by the corresponding clause. This way, if we were to choose all possible combinations of rows whose crosses in total cover all the clauses of a dnf, the minimal dnf(i.e. the simplest normal equivalent) definitely will be among the disjunctions of prime implicants corresponding to each row of each selected combination of rows. Here's an example:
Right now, according to the theorems stated above, minimal dnf has to be among $p\bar{q} \lor \bar{p}r \lor q\bar{r}$, $\bar{q}r \lor p\bar{r} \lor \bar{p}q$.
But here's the thing: Quine didn't prove that the disjunction of the prime implicants we've constructed using this method will even be equivalent to our function. All we know is any other function cannot be a minimal dnf. But Quine stated in all his examples that all disjunctions he`d obtained were the simplest equivalents, although without any proof they'll always be such. And also I see practically everywhere where the method is used nobody bothers to check whether the obtained disjunctions of prime implicates were indeed equivalent to the function.
So is there a theorem (if there is I would like to see the proof) that all such expressions are always equivalent to the initial function, or it is not always the case and we have to check each of them?