proposition: Theorem compiler_t_term_correct (c : compiler_t) P i j v w : v ⋈ w -> P /X/ (j,v) ↓ <-> (i,gc_code c P i) /Y/ (gc_link c P i j,w) ↓.
proof: Proof. Proof using . destruct c as [ lnk code first out sound complete ]; simpl. intros H; split. + intros ((j',v') & H1 & H2). destruct sound with (1 := conj H H1) (i := i) as (w' & H3 & H4). exists (lnk P i j', w'); split; auto. simpl fst in H2 |- *; rewrite out; simpl; auto. + intros ((j',w') & H1). unfold compiled_complete in complete. generalize (conj H H1); intros H2. apply complete in H2 as (i' & v' & H3 & H4 & H5). exists (i',v'); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Code(subcode sss compiler)