added missing accumulation lemma equalities. visual-pleasing spacing. considering changing names for accumulations and reductions to "given" names (top, bot, lef, rig)