proposition: Theorem bsm_mm_simulator i (P : list (@bsm_instr m)) : { Q : list (@mm_instr (pos n)) | forall v w, v ⋈ w -> (forall i' v', (i,P) /BSM/ (i,v) ~~> (i',v') -> exists w', (1,Q) /MM/ (1,w) ~~> (1+length Q,w') /\ v' ⋈ w') /\ ((1,Q) /MM/ (1,w) ↓ -> (i,P) /BSM/ (i,v) ↓) }.
proof: Proof. exists (gc_code bsm_mm_compiler (i,P) 1). 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)