proposition: Theorem mma3_mma2_compiler : compiler_t (@mma_sss _) (@mma_sss _) simul.
proof: Proof. generalize (mma_k_mma_2_compiler godel_coding_235 n). apply compiler_t_simul_equiv. intros v w. generalize (vec_app_split _ _ v) (vec_app_split _ _ w). destruct (vec_split _ _ v) as (v1,v2). destruct (vec_split _ _ w) as (w1,w2). intros <- <-. assert (v1 = v1#>pos0##v1#>pos1##v1#>pos2##vec_nil) as E. 1: apply vec_pos_ext; intros p; repeat invert pos p; auto. unfold simul; split; simpl. + intros (-> & ->); msplit 2; rew vec; simpl; f_equal; auto. + intros (H1 & H2 & H3); split. * apply vec_pos_ext; intros p; repeat invert pos p; auto. rewrite H2; f_equal; auto. * apply vec_pos_ext; intros p. generalize (H3 p); rew vec. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils godel_coding pos vec sss compiler_correction) Undecidability.MinskyMachines.MMA(mma_defs mma_k_mma_2_compiler)