Translator Correctness
	• Defined an inverse function untranslate, and prove that no information is lost w.r.t. to a specialized equivalence relation (equal* (untranslate (translate S)) S) • Trivial for process translation • Tricky for network translation