proposition: Lemma PROG_sim_sc q n (H : n <= S (num_states M)) : ! q < n -> (j + 76 * ! q, PROG q) <sc (j, sim n H).
proof: Proof. revert q. induction n as [n IH] using lt_wf_ind; intros q. destruct n. - intros. lia. - intros H0. eapply Nat.lt_eq_cases in H0 as [H0 | H0]. + unfold sim. fold sim. eapply subcode_app_end. eapply IH. lia. lia. + inversion H0. subst. clear H0. unfold sim. fold sim. revert H IH. eapply (Fin.caseS' q). * intros H IH. cbn [Fin.to_nat proj1_sig sim]. rewrite of_nat_lt_0. cbn - [PROG]. eexists [], []. split. rewrite app_nil_r. reflexivity. reflexivity. * clear q. intros q H IH. erewrite Fin.of_nat_ext. rewrite Fin.of_nat_to_nat_inv. eapply subcode_right. rewrite sim_length. reflexivity. 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)