proposition: Lemma insertKnownSymbols_correct (n : nat) (readSymbols : Vector.t (option sig) n) (i : Fin.t n) tps1 tps2 : length tps1 = fin_to_nat i -> length tps1 + length tps2 = n -> knowsFirstSymbols readSymbols tps1 -> knowsFirstSymbols (insertKnownSymbols readSymbols i (map (@current _) tps2)) (tps1 ++ tps2).
proof: Proof. revert n i tps1 readSymbols. induction tps2 as [ | tp' tps2 IH]; cbn; intros. - now rewrite app_nil_r. - subst. destruct (finSucc_opt i) as [ i' | ] eqn:E. + pose proof finSucc_opt_Some' E as E'. rewrite app_comm_cons'. apply IH; simpl_list; cbn. lia. lia. apply insertKnownSymbol_correct; auto. + apply finSucc_opt_None' in E. assert (| tps2 | = 0) by lia. destruct tps2; cbn in *; inv H0. apply insertKnownSymbol_correct; 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)