proposition: Lemma sim_length (n : nat) (H : n <= S (num_states M)) : @length (bsm_instr 4) (@sim n H) = c * n.
proof: Proof. induction n. - unfold sim. cbn. lia. - unfold sim. fold sim. rewrite app_length. rewrite PROG_length. rewrite IHn. 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)