proposition: Theorem bsm_mm0_sim_spec v w : v ⋈ w -> ((i,P) /BSM/ (i,v) ↓ -> (1,R) /MM/ (1,w) ~~> (0,vec_zero)) /\ ((1,R) /MM/ (1,w) ~~> (0,vec_zero) -> (1,R) /MM/ (1,w) ↓) /\ ((1,R) /MM/ (1,w) ↓ -> (i,P) /BSM/ (i,v) ↓).
proof: Proof. intros Hw; split; [ | split ]. + intros ((i',v') & H). apply (HQ Hw) in H as (w' & (H1 & H2) & H3); fold Q in H1, H2; unfold fst in H2. unfold bsm_mm0_sim; split; [ | simpl; lia ]. apply subcode_sss_compute_trans with (2 := H1); auto. unfold code_end, fst, snd. assert (w'#>tmp1 = 0) by apply H3. apply sss_progress_compute, subcode_sss_progress with (2 := mm_zeroify_spec _ _ _ H); auto. + exists (0,vec_zero); auto. + intros H2; apply HQ with (1 := Hw). revert H2; apply subcode_sss_terminates. unfold R, Q; 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)