proposition: Theorem SIM_term q t i out : i < j \/ i >= j + length SIM -> (j,SIM) // (j + c * !q, enc_tape t) ->> (i, out) -> exists q' t', i = END /\ out = enc_tape t' /\ KOSBTM.eval M q t q' t'.
proof: Proof. intros Hout [k H]. revert q t H. induction k as [k IH] using lt_wf_ind; intros q t H. edestruct PROG_spec as [k' H']. eapply subcode_sss_subcode_inv in H. 4: eapply PROG_sc. 4: eapply H'. 2:{ apply bsm_sss_fun. } - destruct H as (k'' & -> & HH). destruct (δ (q, curr t)) as [ [[q' w] m] | ] eqn:Eq_nxt. + eapply IH in HH. * destruct HH as (q'' & t'' & -> & -> & HH). exists q'', t''; repeat split. econstructor. eassumption. eassumption. * destruct H'. lia. + eapply sss_steps_stop in HH as [= <- <-]. exists q, t. repeat split. econstructor. easy. unfold out_code. right. unfold fst, code_end, snd, fst, plus. rewrite SIM_length. fold plus. lia. - unfold out_code. destruct Hout. + left. cbn. lia. + right. unfold fst, code_end, snd, fst. rewrite PROG_length. transitivity (j + length SIM). rewrite SIM_length. destruct (Fin.to_nat q). cbn - [plus mult]. lia. 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)