proposition: Corollary bsm_mm0_terminates_on_zero v w : v ⋈ w -> (i,P) /BSM/ (i,v) ↓ <-> (1,R) /MM/ (1,w) ~~> (0,vec_zero).
proof: Proof. intros Hw; split; intro; repeat (apply bsm_mm0_sim_spec with (1 := Hw); 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)