proposition: Theorem bsm_mm_compiler_2 n i (P : list (bsm_instr n)) : { Q : list (mm_instr (pos (2+n))) | forall v, (i,P) /BSM/ (i,v) ↓ <-> (1,Q) /MM/ (1,bsm_state_enc v) ~~> (0,vec_zero) }.
proof: Proof. exists (bsm_mm0_sim i P); intro; apply bsm_mm0_terminates_on_zero; auto. 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)