proposition: Lemma P_length : length P = 1 + num_states M * c.
proof: Proof. rewrite /P /=. congr S. have := PROG_length. elim: (num_states M) (PROG); first done. move=> n IH PROG' H. have ->: S n * c = n * c + c by lia. rewrite /= app_length flat_map_concat_map map_map -flat_map_concat_map H. by rewrite IH; [|lia]. Qed.
imports: Undecidability.StackMachines(BSM BSM.bsm_defs) Undecidability.TM(SBTM Util.SBTM_facts) Undecidability.Shared.Libs.DLW(vec subcode sss) PeanoNat List Lia ssreflect ssrbool ssrfun