proposition: Lemma PROG_sc (q : state M) : (!q, PROG q) <sc (1, P).
proof: Proof. apply: subcode_cons. rewrite /P /encode_state [1+1]/=. suff: forall n, (n + sval (Fin.to_nat q) * c, PROG q) <sc (n, flat_map PROG (all_fins (num_states M))) by done. have := PROG_length. move: (num_states M) q (PROG) => ?. elim. { move=> /= *. by eexists [], _. } move=> m q IH PROG' H' n. have := IH (fun q => PROG' (Fin.FS q)) => /(_ ltac:(done) (n+c)). rewrite /= !flat_map_concat_map map_map -!flat_map_concat_map. move=> [l] [r] [{}IH {}IH']. exists (PROG' Fin.F1 ++ l), r. split. - by rewrite IH -app_assoc. - move: (Fin.to_nat q) IH' => [? ?] /=. rewrite app_length H'. 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