proposition: Lemma simulation i v i' v' st : (1, M) // (i, v) ->> (i', v') -> sync (i, v) st -> exists st', sync (i', v') st' /\ clos_refl_trans _ step2 st st'.
proof: Proof. Proof using M_mon. move=> /sss_compute_iff H1 H2. by apply: (Sim.clos_refl_trans_transport fstep H2 H1). Qed.
imports: Undecidability.TM(TM) Undecidability.MinskyMachines(MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL(CompoundFinTypes) Undecidability.Shared.Libs.PSL.EqDec List Lia PeanoNat Compare_dec Relations ssreflect ssrbool ssrfun