proposition: Fact ra_compiler_comp : ra_compiler_stm (ra_comp f g).
proof: Proof. Proof using Hf Hg. red; simpl; intros i p o m H1 H2 H3. destruct ra_compiler_vec with (1 := Hg) (i := i) (p := p) (o := m) (m := m+k) as (P & HP1 & HP2); auto. destruct Hf with (i := length P+i) (p := m) (o := o) (m := m+k) as (Q & HQ); try lia; auto. exists (P++Q++mm_multi_erase m (k+m) k (length P+length Q+i)); intros v e H6 H7; split. + intros x; simpl; intros (w & H4 & H8). assert (forall q, ⟦vec_pos g q⟧ v (vec_pos w q)) as H5. { intros q; generalize (H8 q); rewrite vec_pos_set; auto. } clear H8. destruct (HP1 v w e) as (e1 & G1 & G2 & G3); auto. { intros; apply H6; lia. } destruct (HQ w e1) as [ HQ1 _ ]; auto. { intros j Hj; rewrite G1, H6; lia. } destruct (HQ1 x) as (e2 & G4 & G5); auto. destruct mm_multi_erase_compute with (zero := k+m) (dst := m) (k := k) (i := length P+length Q+i) (e := e2) as (e3 & G6 & G7 & G8); try lia; auto. { rewrite G4, get_set_env_neq, G1, H6; lia. } exists e3; split. * intros j. destruct (interval_dec m (k+m) j) as [ H | H ]. - rewrite G6, get_set_env_neq, H6; lia. - rewrite G7, G4; try lia; dest j o. apply G1; lia. * rew length. apply sss_compute_trans with (length P+i,e1). { revert G3; apply subcode_sss_compute; auto. } apply sss_compute_trans with (length P+length Q+i,e2). { revert G5; rewrite Nat.add_assoc, (Nat.add_comm _ (length _)). apply subcode_sss_compute; auto. } replace (length P+(length Q+2*k)+i) with (2*k+(length P+length Q+i)) by lia. revert G8; apply subcode_sss_compute; auto. + intros H4. assert ((i,P) // (i,e) ↓) as H5. { revert H4; apply subcode_sss_terminates; auto. } assert (forall q, ex (⟦vec_pos g q⟧ v)) as H8. { apply HP2 with (1 := H5) (3 := H7). intros; apply H6; lia. } apply vec_reif in H8; destruct H8 as (w & Hw). destruct (HP1 v w e) as (e1 & G1 & G2 & G3); auto. { intros; apply H6; lia. } destruct (HQ w e1) as [ _ (x & Hx) ]; auto. { intros j Hj; rewrite G1, H6; lia. } - apply subcode_sss_terminates with (Q := (i,P++Q++mm_multi_erase m (k + m) k (length P+length Q+i))); auto. apply subcode_sss_terminates_inv with (2 := H4) (P := (i,P)); auto. { apply mm_sss_env_fun. } split; simpl; auto; lia. - exists x, w; split; auto. intros q; rewrite vec_pos_set; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils finite pos vec subcode sss) Undecidability.MinskyMachines(env mme_defs mme_utils) Undecidability.MuRec.Util(recalg)