proposition: Lemma simulation st1 : (1, M) // st1 ↓ -> exists p ts, TM.eval P (toState (fst st1)) (encode_counters (snd st1)) p ts.
proof: Proof. move=> Hst1. move: (encode_counters (snd st1)) (encodes_countersI (snd st1)). elim /sss_terminates_ind: Hst1. - by apply: mma_sss_fun. - move=> [p1 cs1]. case Hp1: (halt' (toState p1)) (in_out_code_halt p1). + move=> *. do 2 eexists. by apply: eval_halt. + by move=> /in_out_code /[apply]. - move=> [p1 cs1] IH ts Hts. case Hp1: (halt' (toState p1)) (in_out_code_halt p1). { do 2 eexists. by apply: eval_halt. } move=> /in_code_subcode [instr] HQ. have [[p2 cs2] H'p1p2] := mma_sss_total instr (p1, cs1). have /IH {}IH : sss_progress (mma_sss (n:=n)) (p1, [instr]) (p1, cs1) (p2, cs2). { exists 1. split; [done|]. apply: in_sss_steps_S; [|apply: in_sss_steps_0]. exists p1, [], instr, [], cs1. by rewrite /= Nat.add_0_r. } have [ts' [H''p1p2]] := simulation_step HQ H'p1p2 Hts. move=> /(IH HQ) /= [p''] [ts''] /TM_facts.TM_eval_iff [k Hk]. exists p'', ts''. apply /TM_facts.TM_eval_iff. exists (S k). by rewrite /= Hp1 H''p1p2. 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