proposition: Lemma BSM_complete_simulation' n Σ (M : TM Σ n) m i : { P | (forall q t t', TM.eval M (TM.start M) t q t' -> forall v'', BSM.eval (m + (4)) (i, P) (i, Vector.append v'' ((encode_bsm t))) (i + length P, Vector.append v'' ((encode_bsm t')))) /\ (forall t v'', (exists out, BSM.eval (m + (4)) (i, P) (i, Vector.append v'' ((encode_bsm t))) out) -> (exists q' t', TM.eval M (TM.start M) t q' t'))}.
proof: Proof. destruct (KOSBTM_complete_simulation M) as (M1 & Hf1 & Hb1). destruct (BSM_addstacks i (SIM M1 i) m ) as (M2 & Hl & Hf2 & Hb2). exists M2. split. - intros q t t' [q1 H % (SIM_computes i) ] % Hf1. intros. eapply Hf2. eapply BSM_sss.eval_iff. split. 1: cbn [Fin.to_nat proj1_sig mult] in H. 1: rewrite !NPeano.Nat.add_0_l, NPeano.Nat.add_0_r in H. 1: rewrite <- Hl. 1: rewrite SIM_length. 1: rewrite Nat.mul_comm. 1: eapply H. right. unfold fst, subcode.code_end, snd, fst. rewrite <- Hl. lia. - intros t v'' (out & [[out1 out2] [Ho1 Ho2]% BSM_sss.eval_iff] % Hb2). eapply Hb1. eapply SIM_term with (q := Fin.F1) in Ho2 . 2:{ cbn [Fin.to_nat proj1_sig mult]. rewrite !NPeano.Nat.add_0_l, NPeano.Nat.add_0_r. eapply Ho1. } destruct Ho2 as (q' & t' & H1 & -> & H2). eauto. Qed.
imports: Undecidability.StackMachines.BSM Undecidability.StackMachines.Util.BSM_computable Undecidability.TM.TM Undecidability.TM.Util.TM_facts Undecidability.TM.Util.TM_computable Undecidability.TM(TM Arbitrary_to_Binary mTM_to_TM HaltTM_1_to_HaltKOSBTM HaltKOSBTM_to_HaltBSM) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Undecidability(bsm_utils bsm_defs) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes)