proposition: Theorem SIM_correct t : HaltKOSBTM (M, t) <-> BSM_HALTING (existT _ 4 (existT _ j (existT _ SIM (enc_tape t)))).
proof: Proof. split. - intros (q' & t' & H). eapply SIM_computes in H. unfold BSM_HALTING. eexists. split. rewrite Nat.mul_comm in H. match type of H with _ // (?K, _) ->> _ => replace K with j in H end. 2: cbn; lia. eapply H. unfold out_code. right. unfold fst, code_end, snd, fst. rewrite SIM_length. lia. - intros ([i out] & H1 & H2). pose proof (HS := @SIM_term pos0). cbn [Fin.to_nat proj1_sig] in HS. rewrite NPeano.Nat.mul_0_r, NPeano.Nat.add_0_r in HS. eapply HS in H1 as (q' & t' & -> & -> & H). exists q', t'. eassumption. unfold out_code, code_start, code_end, fst, snd in H2. lia. Qed.
imports: Undecidability.TM.KOSBTM.KOSBTM Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Shared.Libs.PSL.EqDec List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(bsm_defs)