Updated soundness portion of the field write proof.
Added definition for bisimulation. Re-wrote the main theorem to be a bisimulation proof instead of a trace-based proof. Restructured the supporting lemmas to support the main coinductive bisimulation proof.