Outline of partial correctness of Armstrong/Virding collector
Prove termination of Armstrong/Virding collector