proposition: Theorem compiler_complete i1 v1 w1 : v1 ⋈ w1 -> Q /Y/ (linker i1,w1) ↓ -> P /X/ (i1,v1) ↓.
proof: Proof. Proof using HPQ Hicomp Hilen step_Y_fun step_X_tot. intros H1 (st & (q & H2) & H3). revert i1 v1 w1 H1 H2 H3. induction q as [ q IHq ] using (well_founded_induction lt_wf). intros i1 v1 w1 H1 H2 H3. destruct (in_out_code_dec i1 P) as [ H4 | H4 ]. + destruct compiler_complete_step with (5 := H2) (st1 := (i1,v1)) as (p & (i2,v2) & (j2,w2) & G1 & G2 & G3 & G4 & G5); auto; simpl in *; subst j2. destruct IHq with (1 := G5) (2 := G1) (3 := G4) as ((i3 & v3) & F3 & F4); auto. exists (i3,v3); repeat (split; auto). apply sss_compute_trans with (1 := G3); auto. + exists (i1,v1); repeat (split; auto). exists 0; constructor. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Code(subcode sss compiler)