proposition: Lemma fstep s t s' : step1 s t -> sync s s' -> exists t', clos_trans _ step2 s' t' /\ sync t t'.
proof: Proof. move=> + /syncE /= [Hs ?]. subst s'. rewrite Hs. move: (fst s) => i. move: (Vector.hd (snd s)) => a. move: (Vector.splitat _ (Vector.tl (snd s))) => [v w] /=. move: t => [i' a'v'w']. rewrite (Vector.eta a'v'w') (vec_append_splitat (VectorDef.tl a'v'w')) Vector.splitat_append. move=> /simulation_sss_step ?. eexists. by split; [apply: t_step; eassumption|apply: sync_intro]. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect