In the previous post we described how the garbage collection works however we did not explain the second attempt or provide proof of correctness. We will look into that now. Remember that for our jargon a vertex is food if it can be reached from the root. If it is not a food, it is garbage. Now onto garbage collection.
The mutator and the marker program superimpose their actions. The mutator actions are not affected and it can continue to add and remove the edges. However we cannot say the same for the marker because the mutator actions can frustrate the marker. For example, marking a single vertex as food could depend on the edges added or removed. To fix this difficulty,  we may have to take another step.
We modify the mutator program from the original where it maintained that a vertex that is food is connected to the root and a vertex that is not food is garbage. In the original program, it assigned  an edge between x and y if y was food and set the edge to true. If this was not the case, it would delete the edge.
Now we add an extra step that we set y as root when y is food. Also, if x is root and adding an edge to x,y implies only y is root.  This is called the propagator step How do we know that this program is correct ? Because we now work off of a root. Two vertices will not satisfy the propagator step only when x is manure. We know the marker has terminated  when we mark the root and for all edges we have completed the propagator.
Note that we mentioned that manure vertices need not be marked. Since they were marked earlier and we will collect them in the next iteration. As an aside, some of the properties that remain true are as follows: a garbage remains a garbage, a food remains a food, a manure is a garbage. Each of the category can only be reached from themselves.
Now we discuss the proof of correctness. Here we have to prove the invariant that if x is manure then x cannot be root. For all vertex, each is neither a manure nor a root.
There are two actions that can modify the root property.
First is the action step we discussed. That is, if x is added to y and y is food, then edge exists between x and y and y is root. Since y is food, y cannot be manure. For all x that is not y, if x is not manure or x is not root and y is not manure, we maintain the invariant.
For the other action where x is root and the edge between x,y is added with y becoming root, the invariant is maintained because x is not a manure. That and y not being a manure implies y can remain a root. Thus maintaining the invariant.