proposition: Fact PROG_length i : length (PROG i) = c.
proof: Proof. unfold PROG. rewrite !app_length, !length_cons. rewrite !uniform_match_option; [reflexivity|..]. all: now intros [[??][]]; rewrite repeat_length. 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)