proposition: Lemma insertKnownSymbols_correct_cons n (T : tapes sig (S n)) (min minSucc : Fin.t (S n)) : fin_to_nat min = 0 -> fin_to_nat minSucc = 1 -> insertKnownSymbols (insertKnownSymbol (Vector.const None (S n)) min (current (Vector.hd T))) minSucc (map (@current _) (vector_to_list (Vector.tl T))) = current_chars T.
proof: Proof. intros HMin_val HMinSucc_val. unshelve epose proof @insertKnownSymbols_correct (S n) (Vector.const None (S n)) min nil (vector_to_list T) _ _ _. - cbn. auto. - cbn. apply Vector.length_to_list. - cbn. tauto. - cbn in *. apply knowsFirstSymbols_all' in H. rewrite <- H. assert (min = Fin.F1) as -> by now apply fin_is_0. cbn. destruct n as [ | n']. + destruct_fin minSucc; auto. lia. + assert (minSucc = Fin.FS Fin.F1) as -> by now apply fin_is_1. cbn. rewrite (Vector.eta T), (Vector.eta (Vector.tl T)) in *. auto. Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)