proposition: Lemma out_code_iff {n s P} : subcode.out_code (fst s) P <-> Sim.stuck (sss_step (@mma_sss n) P) s.
proof: Proof. split. - move=> /sss_steps_stall H t /in_sss_steps_S H'. by have /H' /H [] : sss_steps (mma_sss (n:=n)) P 0 t t by apply: in_sss_steps_0. - have [|] := subcode.in_out_code_dec (fst s) P; [|done]. move=> /in_code_step [t] ? Hs. exfalso. by apply: (Hs t). 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