proposition: Fact compiler_subcode j x : (j,x::nil) <sc P -> (linker j, c linker j x) <sc (i,compiler) /\ linker (1+j) = lc x + linker j.
proof: Proof. Proof using Hc. case_eq P; intros iP lP HP (l & r & H1 & H2); simpl in H1. assert (linker j = lsum l + i) as Hj. { generalize (linker_app l (x::r)). rewrite HP; simpl; intros E. rewrite <- E; auto; f_equal; lia. } assert (linker (1+j) = lc x + linker j) as HSj. { generalize (linker_app (l++x::nil) r). rewrite HP, <- app_assoc; simpl; intros H3. specialize (H3 H1). eq goal H3; f_equal. f_equal. rew length; lia. rewrite length_compiler_app; simpl; lia. } split; auto. unfold compiler; rewrite HP, H1; simpl. exists (comp linker iP l i), (comp linker (1+length l+iP) r (lc x+lsum l+i)); split. rewrite comp_app; simpl; do 3 f_equal; lia. rewrite comp_length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)