proposition: Lemma insertKnownSymbol_correct (n : nat) (readSymbols : Vector.t (option sig) n) (i : Fin.t n) tps tp : length tps = fin_to_nat i -> knowsFirstSymbols readSymbols tps -> knowsFirstSymbols (insertKnownSymbol readSymbols i (current tp)) (tps ++ [tp]).
proof: Proof. revert i tps tp. induction readSymbols as [ | x n readSymbols IH]; intros; cbn in *. - destruct_fin i. - pose proof fin_destruct_S i as [ ( i0 & -> ) | -> ]; cbn in *. + rewrite fin_to_nat_S in *. destruct tps; cbn in *; inv H. destruct H0 as [H0 H0']. split; auto. + destruct tps; cbn in *; inv H. split; auto. apply knowsFirstSymbols_nil. 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)