implementation of partial reduction semantics

- uses (axiomatic) finite maps
- proof of soundness and completeness w.r.t. inductive definition of
  partial reduction