proposition: Lemma P_to_M_step (x y: mm2_state) (x': CM1.Config) : mm2_step P x y -> encodes_config x x' -> exists y' : CM1.Config, clos_trans CM1.Config (fun x y => CM1.step M x = y /\ x <> y) x' y' /\ encodes_config y y'.
proof: Proof. move=> Hxy Hxx'. suff: exists n, encodes_config y (Nat.iter (n+1) (CM1.step M) x'). { move=> [n Hyy']. exists (Nat.iter (n+1) (CM1.step M) x'). split; [|done]. have : x' <> (Nat.iter (n+1) (CM1.step M) x'). { move: Hxy => /mm2_step_neq_encodes. by apply. } elim: n x' {Hxx' Hyy'}. { move=> ? ?. by apply: t_step. } move=> n IH x' /=. have [<-|/IH] := Config_eq_dec x' (Nat.iter (n + 1) (CM1.step M) x'). { move=> ?. by apply: t_step. } have [<-|] := Config_eq_dec (Nat.iter (n + 1) (CM1.step M) x') (CM1.step M (Nat.iter (n + 1) (CM1.step M) x')). { done. } move=> ???. apply: t_trans; [eassumption|]. by apply: t_step. } move: Hxy Hxx' => [?] [+ Hxy]. move: x' Hxy=> [p c] [] /= > Hinstr [-> [n ->]]. - exists 0 => /=. rewrite (seek_M 0 Hinstr) ?κ_norm. constructor; [done|by eexists]. - exists 1 => /=. rewrite (seek_M 0 Hinstr) ?κ_norm /=. rewrite (seek_M 1 Hinstr) ?κ_norm /=. constructor; [done|by eexists]. - exists 2 => /=. rewrite (seek_M 0 Hinstr) ?κ_norm /=. rewrite (seek_M 4 Hinstr) ?κ_norm /=. rewrite (seek_M 5 Hinstr) ?κ_norm /=. constructor; [done|by eexists]. - exists 1 => /=. rewrite (seek_M 0 Hinstr) ?κ_norm /=. rewrite (seek_M 4 Hinstr) ?κ_norm /=. constructor; [done|by eexists]. - exists 3 => /=. rewrite (seek_M 0 Hinstr) ?κ_norm /=. rewrite (seek_M 1 Hinstr) ?κ_norm /=. rewrite (seek_M 2 Hinstr) ?κ_norm /=. rewrite (seek_M 3 Hinstr) ?κ_norm /=. constructor; [done |by eexists]. - exists 3 => /=. rewrite (seek_M 0 Hinstr) ?κ_norm /=. rewrite (seek_M 1 Hinstr) ?κ_norm /=. rewrite (seek_M 2 Hinstr) ?κ_norm /=. rewrite (seek_M 3 Hinstr) ?κ_norm /=. constructor; [done|by eexists]. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun