proposition: Theorem bsm_mma_compiler : compiler_t (@bsm_sss _) (@mma_sss _) bsm_state_equiv.
proof: Proof. apply generic_compiler with (icomp := bsm_instr_compile) (ilen := bsm_instr_compile_length); auto. + apply bsm_sss_total'. + apply mma_sss_fun. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.MinskyMachines.MMA(mma_defs mma_utils_bsm)