proposition: Lemma sync_dec_S p v i ts k : Vector.nth ts pos0 = enc (Vector.nth v pos0) -> encodes_counters v ts -> Vector.nth v i = S k -> i <> pos0 -> sync (p, vec_change v i k) (TM_facts.mk_mconfig (toState false p) (dec_bs i ts)).
proof: Proof. move=> H0vts /vec_Forall2_forall Hvts Hvi Hi. apply: sync_intro. - rewrite /dec_bs. apply /vec_Forall2_forall => j. have [<-|Hij] := pos_eq_dec i j. + rewrite /TM_facts.doAct_multi. rewrite !TM_facts.nth_map2'. rewrite -!vec_pos_nth_eq. rewrite !(vec_change_eq _ _ erefl). rewrite !vec_pos_nth_eq. move: (Vector.nth v i) (Vector.nth ts i) Hvi (Hvts i). move=> > -> [] m. by apply: (encodes_counter_intro _ (S m)). + rewrite /TM_facts.doAct_multi. rewrite !TM_facts.nth_map2'. rewrite -!vec_pos_nth_eq. rewrite !(vec_change_neq _ _ Hij). rewrite !vec_pos_nth_eq !TM_facts.nth_nop_action. by apply: Hvts. - rewrite /dec_bs. move: H0vts Hi. rewrite (Vector.eta v) (Vector.eta ts). have [->|[j ->]] := pos_S_inv i. + done. + by move=> /= ->. 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