I already asked this on Math Stack Exchange, but had no response. Now I've figured out it is more appropriate to ask such question on this site, since it is rather about further elaboration on a research paper, not about understanding some topic in general.
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:
Theorem 1. Any simplest normal equivalent of $\Phi$ is an alternation of prime implicants of $\Phi$.
Theorem 5. If $\Psi$ is a simplest normal equivalent of a developed normal formula $\Phi$, then each clause of $\Phi$ subsumes a clause of $\Psi$.
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?
