Refactored the semantics.
One direction proven.
Added the structure of the second proof.