proposition: Lemma syncE s s' : sync s s' -> let avw := Vector.splitat _ (snd s) in let i := fst s in let a := Vector.hd (fst avw) in let v := Vector.tl (fst avw) in let w := snd avw in s = (i, Vector.append (a ## v) w) /\ s' = (shift_addr i, Vector.append (0 ## v) (Vector.append w (a ## vec_nil))).
proof: Proof. case => /= >. by rewrite Vector.splitat_append. 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