proposition: Lemma length_P' : length P' = 4 + length P.
proof: Proof. rewrite /P' app_length map_length /=. lia. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect