proposition: Lemma to_MM2_ZERO_HALTING : MM2_ZERO_HALTING mm.
proof: Proof. Proof using HN. rewrite /MM2_ZERO_HALTING -/c0. have [s [H1s H2s]] := init_encodes. move Ht: (repeat so (1+N)) (c0) H2s H1s => t c Hst. have {}Ht : Forall (fun x => fst so = x) (map fst t). { subst t. elim: (N); by constructor. } move: Hst Ht c. move=> /rt_rt1n. elim. - move=> {}s Hs [? [? ?]] /= [?] [?] [{}t] [?] [H]. subst s. move: Hs. rewrite ?map_app ?Forall_app H. by move=> [_] [/Forall_cons_iff] []. - move=> > /simulate_srs_step H _ IH /IH {}IH c /H []. + by move=> /IH. + have [[y Hcy]|?] := mm2_exists_step_dec mm c. * move=> /(_ y Hcy) /IH [c'0 [? ?]]. exists c'0. split; [|done]. by apply: rt_trans; [apply: rt_step|]; eassumption. * move=> _. exists c. by split; [apply: rt_refl|]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun