proof of soundness
added a bunch of definitions
started on soundness
not sure