Change Lemma 8 to use an algorithm. Hopefully this is clearer than it was before. Lemma 8 is definitely still a bit rough around the edges even given that it doesn't work