proposition: Corollary compiler_complete' : forall i₁ v₁ w₁ st, v₁ ⋈ w₁ /\ Q /Y/ (linker i₁,w₁) ~~> st -> exists i₂ v₂ w₂, v₂ ⋈ w₂ /\ P /X/ (i₁,v₁) ~~> (i₂,v₂) /\ Q /Y/ (linker i₂,w₂) ~~> st.
proof: Proof. Proof using HPQ Hicomp Hilen step_Y_fun step_X_tot. intros i1 v1 w1 st (H1 & H2). destruct compiler_complete with (1 := H1) (2 := ex_intro (fun x => Q /Y/ (linker i1, w1) ~~> x) _ H2) as ((i2,v2) & H3 & H4). exists i2, v2. destruct (compiler_sound (conj H1 H3)) as (w2 & H5 & H6). exists w2; do 2 (split; auto). 1: split; auto. destruct H2 as (H2 & H0); split; auto. apply sss_compute_inv with (3 := H6); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Code(subcode sss compiler)