proposition: Theorem compiler_t_output_sound c P i i₁ v₁ i₂ v₂ w₁ : v₁ ⋈ w₁ /\ P /X/ (i₁,v₁) ~~> (i₂,v₂) -> exists w₂, v₂ ⋈ w₂ /\ (i,gc_code c P i) /Y/ (gc_link c P i i₁,w₁) ~~> (gc_link c P i i₂,w₂).
proof: Proof. Proof using . destruct c as [ lnk code first out sound complete ]; simpl. intros (H1 & H2 & H3). destruct (sound P i i₁ v₁ i₂ v₂ w₁) as (w2 & H4 & H5); auto. exists w2; split; auto; split; auto. apply out with (i := i) in H3. unfold fst in H3 |- *. rewrite H3; right; simpl; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Code(subcode sss compiler)