A Proof Theory for Loop-Parallelizing Transformations