proposition: Theorem bsm_mm_simulator i (P : list (@bsm_instr m)) j : { Q : list (@mm_instr (pos n)) | forall v w, bsm_state_enc v w -> (forall i' v', (i,P) /BSM/ (i,v) ~~> (i',v') -> exists w', (j,Q) /MM/ (j,w) ~~> (j+length Q,w') /\ bsm_state_enc v' w') /\ ((j,Q) /MM/ (j,w) ↓ -> (i,P) /BSM/ (i,v) ↓) }.
proof: Proof. Proof using Hvr3 Hvr2 Hvr1 Hv23 Hv13 Hv12 Hreg. exists (gc_code bsm_mm_compiler (i,P) j). intros v w Hw; split. + intros ? ?; now apply (compiler_t_output_sound' bsm_mm_compiler). + apply compiler_t_term_equiv; 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)