proposition: Theorem SIM_computes q t q' t' : KOSBTM.eval M q t q' t' -> (j,SIM) // (j + c * !q, enc_tape t) ->> (END, enc_tape t').
proof: Proof. induction 1. - eapply subcode_sss_compute_trans with (P := (j + 76 * !q, PROG q)). eapply PROG_sc. eapply sss_progress_compute. eapply PROG_spec. rewrite H. bsm sss stop. - eapply subcode_sss_compute_trans with (P := (j + 76 * !q, PROG q)). eapply PROG_sc. eapply sss_progress_compute. eapply PROG_spec. rewrite H. eapply IHeval. 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)