proposition: Theorem mma_k_mma_2_compiler : compiler_t (@mma_sss (k+n)) (@mma_sss (2+n)) simul.
proof: Proof. apply generic_compiler with icomp ilen. + intros; now rewrite icomp_length_eq. + apply mma_sss_total_ni. + apply mma_sss_fun. + apply icomp_sound. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils godel_coding pos vec subcode sss compiler_correction) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)