finished proof of theorem 21 (I think)
Merge branch 'esop2015' of github.com:jgbm/cpgv into esop2015
tidy up notation in Section 4.3 a bit