proposition: Lemma inverse_simulation p cs p' ts' : TM.eval P (toState p) (encode_counters cs) p' ts' -> (1, M) // (p, cs) ↓.
proof: Proof. move: (encode_counters _) (encodes_countersI cs) => ts Hcsts. move=> /TM_facts.TM_eval_iff [k]. have HM : forall p cs, out_code p (1, M) -> (1, M) // (p, cs) ↓. { move=> ???. eexists (_, _). split; [|by eassumption]. exists 0. by apply: sss_steps_0. } elim: k p cs p' ts' ts Hcsts. - move=> p > ? /=. by move: (halt' (toState p)) (in_out_code_halt p) => [/HM|]. - move=> k IH p1 cs1 p' ts' ts Hcsts /=. case: (halt' (toState p1)) (in_out_code_halt p1). { by move=> /HM. } move=> /in_code_subcode [instr] HQ. have [[p2 cs2] H'p1p2] := mma_sss_total instr (p1, cs1). have [ts'' [-> /IH /[apply]]] := simulation_step HQ H'p1p2 Hcsts. apply: subcode_sss_terminates_instr; by eassumption. Qed.
imports: Undecidability.MinskyMachines(MM MMA.mma_defs) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL.EqDec List Vector Lia PeanoNat Compare_dec ssreflect ssrbool ssrfun