soundness and completeness of reduction semantics

I formulated the reduction semantics as a relation (which is fitting but
also simplifies the proof). I had to correct the semantics in one little
detail.