proposition: Lemma syncE i v p bs : sync (i, v) (TM_facts.mk_mconfig p bs) -> encodes_counters v bs /\ Vector.nth bs pos0 = enc (Vector.nth v pos0) /\ p = toState false i.
proof: Proof. intros H. now inversion H. 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