proposition: Theorem bsm_mm_compiler : compiler_t (@bsm_sss _) (@mm_sss _) bsm_state_enc.
proof: Proof. Proof using Hvr3 Hvr2 Hvr1 Hv23 Hv13 Hv12 Hreg. apply generic_compiler with (icomp := bsm_instr_compile) (ilen := bsm_instr_compile_length); auto. + apply bsm_sss_total'. + apply mm_sss_fun. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.MinskyMachines.MM(mm_defs mm_utils)