(* From Undecidability Require Import Combinators.Combinators Multi Basic.Mono TMTac. *)
Require Export Undecidability.TM.Code.CodeTM Undecidability.TM.Code.ChangeAlphabet.
Require Export Undecidability.TM.Compound.TMTac Undecidability.TM.Compound.MoveToSymbol.
Require Export Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi.
(* the above imports sidestep the import of ProgrammingTools below to avoid the dependency on Hoare *)
(*From Undecidability.TM Require Import ProgrammingTools.*)
From Undecidability Require Import ArithPrelim.
From Undecidability Require Import TM.Compound.Shift.
From Undecidability Require Import TM.Util.VectorPrelim.

From Undecidability Require Import EncodeTapes TM.Util.VectorPrelim.
Require Import FunInd.

Local Set Printing Coercions.

(* Avoid using Vector.to_list, because it doesn't cbn good. Use vector_to_list instead. *)
Local Arguments Vector.to_list {A n} (!v).

Local Arguments plus : simpl never.
Local Arguments mult : simpl never.

Lemma removelast_cons (X : Type) (xs : list X) (x : X) :
  xs <> nil ->
  removelast (x :: xs) = x :: removelast xs.
Proof.
  destruct xs as [ | x' xs']; cbn.
  - congruence.
  - intros _. auto.
Qed.

(* TODO: ~> somewhere else *)
Lemma vector_to_list_inj (X : Type) (n : nat) (xs ys : Vector.t X n) :
  vector_to_list xs = vector_to_list ys -> xs = ys.
Proof.
  revert ys. induction xs as [ | x n xs IH]; intros; cbn in *.
  - destruct_vector. reflexivity.
  - destruct_vector. cbn in *. inv H. f_equal. auto.
Qed.

Section Fin.

  Global Coercion fin_to_nat (n : nat) (i : Fin.t n) : nat := proj1_sig (Fin.to_nat i).
  Global Set Printing Coercions.

  Lemma fin_to_nat_lt (n : nat) (i : Fin.t n) : fin_to_nat i < n.
  Proof. unfold fin_to_nat. destruct (Fin.to_nat i). cbn. auto. Qed.

  Lemma fin_to_nat_O (n : nat) :
    fin_to_nat (@Fin.F1 n) = 0.
  Proof. reflexivity. Qed.

  Lemma fin_to_nat_S (n : nat) (i : Fin.t n) :
    fin_to_nat (Fin.FS i) = S (fin_to_nat i).
  Proof.
    unfold fin_to_nat. destruct i as [ | n i].
    - cbn. reflexivity.
    - cbn in *. destruct (Fin.to_nat i) as [k ?]. cbn in *. reflexivity.
  Qed.

  Lemma fin_is_0 (n : nat) (i : Fin.t (S n)) :
    fin_to_nat i = 0 -> i = Fin0.
  Proof.
    intros H. pose proof fin_destruct_S i as [ (i'&->) | ->]; cbn in *; auto.
    rewrite fin_to_nat_S in H. lia.
  Qed.

  Lemma fin_is_1 (n : nat) (i : Fin.t (S (S n))) :
    fin_to_nat i = 1 -> i = Fin1.
  Proof.
    intros H. pose proof fin_destruct_S i as [ (i'&->) | ->]; cbn in *; auto.
    rewrite fin_to_nat_S in H. inv H. now apply fin_is_0 in H1 as ->.
  Qed.

  Lemma fin_is_2 (n : nat) (i : Fin.t (S (S (S n)))) :
    fin_to_nat i = 1 -> i = Fin1.
  Proof.
    intros H. pose proof fin_destruct_S i as [ (i'&->) | ->]; cbn in *; auto.
    rewrite fin_to_nat_S in H. inv H. now apply fin_is_0 in H1 as ->.
  Qed.

  Fixpoint finMax (n : nat) {struct n} : n <> 0 -> Fin.t n.
  Proof.
    destruct n as [ | n'].
    - abstract congruence.
    - decide (n' = 0) as [ H | H]. (* destruct makes troubles here *)
      + intros _. apply Fin.F1.
      + intros _. apply Fin.FS. apply (finMax n'). auto.
  Defined. (* because definition *)

  Definition finMax' (n : nat) : Fin.t (S n).
  Proof.
    apply finMax. apply Nat.neq_succ_0.
  Defined. (* because definition *)

  Lemma finMax_ext (n : nat) (H1 H2 : n <> 0) : finMax H1 = finMax H2.
  Proof.
    induction n as [ | n' IH].
    - congruence.
    - cbn. decide (n' = 0) as [H | H]; f_equal.
  Qed.

  Lemma finMax_val (n : nat) (H : n <> 0) : fin_to_nat (finMax H) = n - 1.
  Proof.
    unfold fin_to_nat. induction n as [ | n' IH ].
    - congruence.
    - cbn. decide (n' = 0) as [ -> | H']; cbn.
      + reflexivity.
      + replace (n' - 0) with n' by lia.
        specialize IH with (H := H').
        destruct (Fin.to_nat (finMax H')) as [k ?]; cbn in *. lia.
  Qed.

  (* Arguments finMax (n) H : clear implicits. *)

  (* Compute finMax (ltac:(congruence) : 1 <> 0). *)
  (* Compute finMax (ltac:(congruence) : 10 <> 0). *)
  (* Compute finMax' 99. *)

  Definition finMin (n : nat) : n <> 0 -> Fin.t n.
  Proof.
    refine (match n as n' return n' <> 0 -> Fin.t n' with
            | 0 => fun H => False_rec _ _
            | S n' => fun _ => Fin.F1
            end); auto.
  Defined. (* because definition *)

  Lemma finMin_O (n : nat) (H : S n <> 0) : finMin H = Fin.F1.
  Proof. cbn. reflexivity. Qed.

  Lemma finMin_ext (n : nat) (H1 H2 : n <> 0) : finMin H1 = finMin H2.
  Proof.
    destruct n.
    - congruence.
    - auto.
  Qed.

  Lemma finMin_val (n : nat) (H : n <> 0) : fin_to_nat (finMin H) = 0.
  Proof.
    unfold fin_to_nat. destruct n as [ | n'].
    - congruence.
    - cbn. reflexivity.
  Qed.

  Lemma finSucc_help (i : Fin.t 1) : i = Fin0.
  Proof. now destruct_fin i. Qed.

  Lemma finSucc_help' (n : nat) (i1 i2 : Fin.t n) :
    Fin.FS i1 <> Fin.FS i2 -> i1 <> i2.
  Proof. now intros H1 ->. Qed.

  Fixpoint finSucc (n : nat) (i : Fin.t n) {struct n} : forall (H : n <> 0), i <> finMax H -> Fin.t n.
  Proof.
    destruct n as [ | n'].
    - intros. abstract congruence.
    - cbn. decide (n' = 0) as [ HDec | HDec]; cbn.
      + intros _ Hi. exfalso. apply Hi. subst. apply finSucc_help.
      + intros _.
        revert n' i HDec. refine (@Fin.caseS (fun n' i => forall (HDec : n' <> 0), i <> Fin.FS (finMax HDec) -> Fin.t (S n')) _ _).
        * intros. apply Fin.FS. apply finMin. apply HDec.
        * intros. apply Fin.FS. eapply finSucc. eapply finSucc_help'. apply H.
  Defined. (* because definition *)

  Definition finSucc' (n : nat) (i : Fin.t (S n)) (H : i <> finMax' n) : Fin.t (S n).
  Proof. unshelve eapply finSucc with (i := i). apply Nat.neq_succ_0. apply H. Defined. (* because definition *)

  (* Compute @finSucc 5 Fin0 _ _. *)
  (* Compute finSucc' (_ : Fin4 <> finMax' 10). *)

  Fixpoint finSucc_opt (n : nat) (i : Fin.t n) {struct i} : option (Fin.t n).
  Proof.
    destruct i.
    - destruct n.
      + apply None.
      + apply Some. apply Fin.FS. apply Fin.F1.
    - destruct n.
      + destruct_fin i.
      + destruct (finSucc_opt _ i) as [ rec | ].
        * apply Some. apply Fin.FS. apply rec.
        * apply None.
  Defined. (* because definition *)

  (* Compute eq_refl : @finSucc_opt 1 Fin0 = None. *)
  (* Compute eq_refl : @finSucc_opt 2 Fin0 = Some Fin1. *)
  (* Compute eq_refl : @finSucc_opt 2 Fin1 = None. *)
  (* Compute eq_refl : @finSucc_opt 3 Fin1 = Some Fin2. *)
  (* Compute eq_refl : @finSucc_opt 3 Fin0 = Some Fin1. *)
  (* Compute eq_refl : @finSucc_opt 8 Fin7 = None. *)
  (* Compute eq_refl : @finSucc_opt 9 Fin7 = Some Fin8. *)

  Lemma finSucc_opt_Some (n : nat) (i : Fin.t n) :
    S (fin_to_nat i) < n ->
    exists i', finSucc_opt i = Some i'.
  Proof.
    induction i; intros; cbn in *.
    - destruct n. lia. eauto.
    - destruct n; cbn. lia.
      rewrite !fin_to_nat_S in *.
      spec_assert IHi as (i'&IH) by lia. rewrite IH. eauto.
  Qed.

  Lemma finSucc_opt_Some' (n : nat) (i i' : Fin.t n) :
    finSucc_opt i = Some i' ->
    fin_to_nat i' = S (fin_to_nat i).
  Proof.
    revert i'. induction i; cbn; intros.
    - destruct n; inv H. cbn. reflexivity.
    - destruct n; cbn in *. destruct_fin i.
      destruct (finSucc_opt i) as [ i'' | ] eqn:E; inv H.
      rewrite fin_to_nat_S. rewrite IHi; auto.
      now rewrite fin_to_nat_S.
  Qed.

  Lemma finSucc_opt_None (n : nat) (i : Fin.t n) :
    S (fin_to_nat i) = n ->
    finSucc_opt i = None.
  Proof.
    induction i; intros; cbn in *.
    - inv H. reflexivity.
    - rewrite fin_to_nat_S in *. inv H. spec_assert IHi by assumption.
      destruct n; cbn. lia. rewrite IHi. reflexivity.
  Qed.

  Lemma finSucc_opt_None' (n : nat) (i : Fin.t n) :
    finSucc_opt i = None ->
    S (fin_to_nat i) = n.
  Proof.
    induction i; cbn; intros.
    - destruct n; now inv H.
    - destruct n. destruct_fin i.
      destruct (finSucc_opt i) as [ i' | ]; inv H.
      now rewrite fin_to_nat_S, IHi.
  Qed.

  Definition finMin_opt (n : nat) : option (Fin.t n).
  Proof.
    destruct n.
    - apply None.
    - apply Some. apply Fin.F1.
  Defined. (* because definition *)

  Lemma finMin_opt_None (n : nat) :
    finMin_opt n = None -> n = 0.
  Proof. destruct n; cbn; congruence. Qed.

  Lemma finMin_opt_Some (n : nat) i :
    finMin_opt n = Some i -> exists n', n = S n'.
  Proof. destruct n; cbn; intros H; inv H; eauto. Qed.

  Lemma finMin_opt_Some_val (n : nat) i :
    finMin_opt n = Some i -> fin_to_nat i = 0.
  Proof. destruct n; cbn; intros H; inv H; auto. Qed.

  Lemma finSucc_correct (n : nat) (i : Fin.t n) (H1 : n <> 0) (H2 : i <> finMax H1) :
    fin_to_nat (finSucc H2) = S (fin_to_nat i).
  Proof.
     revert i H1 H2. induction n as [ | n' IH]; intros; cbn in *.
    - congruence.
    - decide (n' = 0) as [-> | HDec]; cbn.
      + exfalso. apply H2. apply finSucc_help.
      + pose proof fin_destruct_S i as [ (i'&->) | -> ]; cbn -[Fin.to_nat]; swap 1 2.
        * change (S (proj1_sig (Fin.to_nat Fin0))) with 1.
          rewrite fin_to_nat_S. f_equal. rewrite finMin_val. reflexivity.
        * rewrite !fin_to_nat_S. f_equal. now rewrite IH.
  Qed.

End Fin.

Fixpoint map_vect_list (X Y : Type) (f : X -> Y -> X) (n : nat) (vs : Vector.t Y n) (ls : list X) {struct ls} : list X :=
  match ls with
  | nil => nil
  | x :: ls' =>
    match vs with
    | [| |] => ls
    | y ::: vs' =>
      f x y :: map_vect_list f vs' ls'
    end
  end.

Lemma map_vect_list_length (X Y : Type) (f : X -> Y -> X) (n : nat) (vs : Vector.t Y n) (ls : list X) :
  length (map_vect_list f vs ls) = length ls.
Proof.
  revert n vs. induction ls as [ | x ls IH]; cbn; intros.
  - reflexivity.
  - destruct vs as [ | y n vs]; cbn; f_equal; auto.
Qed.

Lemma map_vect_list_app (X Y : Type) (f : X -> Y -> X) (n : nat) (vs : Vector.t Y n) (ls : list X)
      (x : X) (i : Fin.t n) :
  fin_to_nat i = length ls ->
  map_vect_list f vs (ls ++ [x]) =
  map_vect_list f vs ls ++ [f x vs[@i]].
Proof.
  revert n vs i. induction ls as [ | x' ls IH]; cbn; intros.
  - destruct vs. destruct_fin i.
    enough (i = Fin.F1) as -> by auto.
    pose proof fin_destruct_S i as [ (i'&->) | ]; cbn in *; auto.
    rewrite fin_to_nat_S in *. lia.
  - destruct vs as [ | v n vs]; cbn in *.
    + destruct_fin i.
    + f_equal.
      pose proof fin_destruct_S i as [ (i'&->) | -> ]; cbn in *.
      * rewrite fin_to_nat_S in *. apply IH. lia.
      * lia.
Qed.

Lemma map_vect_list_eq (X Y : Type) (n1 : nat) (f : X -> Y -> X) (vs : Vector.t Y n1) (xs : Vector.t X n1) :
  map_vect_list f vs (vector_to_list xs) = vector_to_list (Vector.map2 f xs vs).
Proof.
  revert xs. induction vs as [ | v n1 vs IH]; intros; cbn in *.
  - destruct_vector. cbn. reflexivity.
  - pose proof destruct_vector_cons xs as (x'&xs'&->). cbn.
    f_equal. auto.
Qed.

Lemma destruct_tapes1 (sig : Type) (t : tapes sig 1) :
  exists t', t = [| t' |].
Proof. destruct_tapes. eauto. Qed.

Section BookKeepingForRead.

  Variable sig : Type.

  Set Default Proof Using "Type".

  Fixpoint knowsFirstSymbols {n' : nat} (readSymbols : Vector.t (option sig) n') (tps : list (tape sig)) {struct readSymbols} : Prop :=
    match readSymbols, tps with
    | Vector.nil _, nil => True /\ True /\ True
    | Vector.nil _, _::_ => True /\ True (* to much tapes *)
    | x ::: readSymbols, nil => True (* list of tapes is too big, must not happen *)
    | x ::: readSymbols', tp :: tps' =>
      current tp = x /\ knowsFirstSymbols readSymbols' tps'
    end.

  Lemma knowsFirstSymbols_nil {n : nat} (readSymbols : Vector.t (option sig) n) :
    knowsFirstSymbols readSymbols nil.
  Proof.
    destruct n.
    - destruct_vector. cbn. tauto.
    - destruct_vector. cbn. tauto.
  Qed.

  Definition insertKnownSymbol {n : nat} (readSymbols : Vector.t (option sig) n) (i : Fin.t n) (s : option sig) : Vector.t (option sig) n :=
    Vector.replace readSymbols i s.

  Fixpoint insertKnownSymbols {n : nat} (readSymbols : Vector.t (option sig) n) (i : Fin.t n) (newSymbols : list (option sig)) :
    Vector.t (option sig) n :=
    match newSymbols with
    | nil => readSymbols
    | s :: newSymbols' =>
      match finSucc_opt i with
      | Some i' => insertKnownSymbols (insertKnownSymbol readSymbols i s) i' newSymbols'
      | None => insertKnownSymbol readSymbols i s
      end
    end.

  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.
    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.

  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.
    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.

  (*
  H : knowsFirstSymbols
        (insertKnownSymbols (current tp ::: Vector.const None n) Fin0
           (map (current (sig:=sig)) (tp :: vector_to_list T))) ( ++ tp :: vector_to_list T)
  ============================
  insertKnownSymbols (current tp ::: Vector.const None n) Fin0 (vector_to_list (current_chars T)) =
  current_chars (tp ::: T)
*)

  Lemma knowsFirstSymbols_all n (tps : list (tape sig)) (symbols : Vector.t (option sig) n) :
    length tps = n ->
    knowsFirstSymbols symbols tps ->
    vector_to_list symbols = map (@current _) tps.
  Proof.
    revert tps. induction symbols; cbn; intros.
    - destruct tps; cbn in *; auto.
    - destruct tps; cbn in *; inv H. destruct H0 as [ <- ?]. f_equal. auto.
  Qed.

  Lemma knowsFirstSymbols_all' n (T : tapes sig n) (symbols : Vector.t (option sig) n) :
    knowsFirstSymbols symbols (vector_to_list T) ->
    symbols = current_chars T.
  Proof.
    induction T as [ | tp n T IH]; intros; cbn in *.
    - destruct_vector. reflexivity.
    - destruct_vector. unfold current_chars. cbn in *. destruct H as [ <- H]. f_equal. auto.
  Qed.

  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.
    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_to_list_length.
    - 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.
        destruct_tapes. cbn. auto.
  Qed.


  (*
  E_val : fin_to_nat min = 0
  E2_val : fin_to_nat minSucc = 1
  minSucc : Fin.t (S n')
  ============================
  insertKnownSymbols (insertKnownSymbol (Vector.const None (S n')) min (current (Vector.hd T))) minSucc
    (map (current (sig:=eqType_X (type sig))) (vector_to_list (Vector.tl T))) = 
  current_chars T
  *)

End BookKeepingForRead.

Section ToSingleTape.

  Variable (sig F : finType).
  Variable n : nat.
  (* Hypothesis (nNeq0 : n <> 0). (* This really makes no sense for 0 tapes. *) *)
  Notation nMax := (finMax' n).
  Local Arguments finMax' : simpl never.

  Notation sigSim := (FinType(EqType(boundary + sigList (sigTape sig)))).

  Implicit Types (T : tapes sig n).

  Definition contains_tapes (t : tape sigSim) T :=
    t = midtape nil (inl START) (map inr (encode_tapes T) ++ [inl STOP]).
  Notation "t ≃ T" := (contains_tapes t T) (at level 70, no associativity).

  Hypothesis pM : pTM sig F n.

  (* Go to the current symbol of the selected tape *)
  Section GoToCurrent.

    Definition atStart (t : tape sigSim) (tps : list (tape sig)) : Prop :=
      t = midtape nil (inl START) (map inr (encode_list _ tps) ++ [inl STOP]).

    Definition atCons (t : tape sigSim) (tps1 tps2 : list (tape sig)) (tp : tape sig) : Prop :=
      t = midtape (map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
                  (inr (sigList_cons))
                  (map inr (map sigList_X (encode_tape tp)) ++ map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atNil (t : tape sigSim) (tps : list (tape sig)) : Prop :=
      t = midtape (map inr (rev (removelast (encode_list _ tps))) ++ [inl START]) (inr (sigList_nil)) [inl STOP].

    Definition atCons_current_niltape (t : tape sigSim) (tps1 tps2 : list (tape sig)) : Prop :=
      t = midtape
            (inr (sigList_cons) :: map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
            (inr (sigList_X NilBlank))
            (map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atCons_current_leftof (t : tape sigSim) (tps1 tps2 : list (tape sig)) (r : sig) (rs : list sig) :=
      t = midtape
            (inr (sigList_cons) :: map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
            (inr (sigList_X (LeftBlank true)))
            (inr (sigList_X (UnmarkedSymbol r)) ::
                 map (fun s => inr (sigList_X (UnmarkedSymbol s))) rs ++ inr (sigList_X (RightBlank false)) ::
                 map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atCons_current_midtape (t : tape sigSim) (tps1 tps2 : list (tape sig)) (ls : list sig) (m : sig) (rs : list sig) :=
      t = midtape
            (map (fun s => inr (sigList_X (UnmarkedSymbol s))) ls ++ (* ls is reversed twice *)
                 inr (sigList_X (LeftBlank false)) :: inr (sigList_cons) :: map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
            (inr (sigList_X (MarkedSymbol m)))
            (map (fun s => inr (sigList_X (UnmarkedSymbol s))) rs ++ inr (sigList_X (RightBlank false)) ::
                 map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atCons_current_rightof (t : tape sigSim) (tps1 tps2 : list (tape sig)) (l :sig) (ls : list sig) :=
      t = midtape
            (inr (sigList_X (UnmarkedSymbol l)) ::
                 map (fun s => inr (sigList_X (UnmarkedSymbol s))) ls ++ (* ls is reversed twice *)
                 inr (sigList_X (LeftBlank false)) :: inr (sigList_cons) :: map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
            (inr (sigList_X (RightBlank true)))
            (map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atCons_current (t : tape sigSim) (tps1 tps2 : list (tape sig)) (tp : tape sig) :=
      match tp with
      | niltape _ => atCons_current_niltape t tps1 tps2
      | leftof r rs => atCons_current_leftof t tps1 tps2 r rs
      | midtape ls m rs => atCons_current_midtape t tps1 tps2 ls m rs
      | rightof l ls => atCons_current_rightof t tps1 tps2 l ls
      end.

    Definition tape_dir (t : tape sig) : option move :=
      match t with
      | niltape _ => None
      | leftof _ _ => Some Lmove
      | midtape _ _ _ => Some Nmove
      | rightof _ _ => Some Rmove
      end.

    Definition isMarked' (s : sigSim) : bool :=
      match s with
      | inr (sigList_X s) => isMarked s
      | _ => false
      end.

    Definition IsCons_Rel : pRel sigSim bool 1 :=
      fun tin '(yout, tout) =>
        (forall tps1 tps2 tp,
            atCons tin[@Fin0] tps1 tps2 tp ->
            atCons tout[@Fin0] tps1 tps2 tp /\
            yout = true) /\
        (forall tps,
            atNil tin[@Fin0] tps ->
            atNil tout[@Fin0] tps /\
            yout = false).

    Definition IsCons : pTM sigSim bool 1 :=
      Switch ReadChar
             (fun (s : option sigSim) =>
                match s with
                | Some (inr (sigList_cons)) => Return Nop true
                | Some (inr (sigList_nil)) => Return Nop false
                | _ => Return Nop default
                end).

    Definition IsCons_steps := 2.

    Lemma IsCons_Sem : IsCons ⊨c(IsCons_steps) IsCons_Rel.
    Proof.
      unfold IsCons_steps. eapply RealiseIn_monotone.
      { unfold IsCons. TM_Correct. }
      { Unshelve. 4-5: reflexivity. all: reflexivity. }
      {
        intros tin (yout, tout) H. split.
        { (* cons case *) intros tps1 tps2 tp HCons. unfold atCons in *. TMSimp. auto. }
        { (* nil case *) intros tps HNil. unfold atNil in *. TMSimp. auto. }
      }
    Qed.

    Definition GoToCurrent_Rel : pRel sigSim (option move) 1 :=
      fun tin '(yout, tout) =>
        forall (tps1 tps2 : list (tape sig)) (tp : tape sig),
          atCons tin[@Fin0] tps1 tps2 tp ->
          atCons_current tout[@Fin0] tps1 tps2 tp /\
          yout = tape_dir tp.

    Definition GoToCurrent : pTM sigSim (option move) 1 :=
      MoveToSymbol isMarked' id;;
      Switch ReadChar
      (fun (c : option sigSim) =>
         match c with
         | Some (inr (sigList_X (RightBlank true))) => Return Nop (Some Rmove)
         | Some (inr (sigList_X (LeftBlank true))) => Return Nop (Some Lmove)
         | Some (inr (sigList_X (MarkedSymbol _))) => Return Nop (Some Nmove)
         | Some (inr (sigList_X NilBlank)) => Return Nop (None)
         | _ => Return Nop None
         end).

    Lemma GoToCurrent_Realise : GoToCurrent ⊨ GoToCurrent_Rel.
    Proof.
      eapply Realise_monotone.
      { unfold GoToCurrent. TM_Correct. }
      {
        intros tin (yout, tout) H. intros tps1 tps2 tp HCons. unfold atCons in *. TMSimp.
        rename H1 into H.
        destruct tp as [ | r rs | l ls | ls m rs]; cbn in *; TMSimp.
        - (* tp = niltape *)
          do 2 ( rewrite MoveToSymbol_Fun_equation in *; cbn in * ). TMSimp.
          split; eauto. hnf. reflexivity.
        - (* tp = leftof r rs *)
          do 2 ( rewrite MoveToSymbol_Fun_equation in *; cbn in * ). TMSimp.
          split; auto. hnf. cbn. f_equal. rewrite !List.map_map, !map_app, <- !app_assoc, !List.map_map. cbn. reflexivity.
        - (* tp = rightof l ls *)
          replace (inr (sigList_X (LeftBlank false)) ::
                       map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l; RightBlank true])) ++
                       map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with
              ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l])))
                 ++ inr (sigList_X (RightBlank true)) :: (map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]))
            in H by (now simpl_list; cbn; rewrite <- !app_assoc).
          rewrite MoveToSymbol_correct_midtape in H; cbn; auto.
          + cbn in *. TMSimp. split; auto. hnf. f_equal.
            rewrite !map_id, !List.map_map. cbv [id].
            rewrite !map_app; cbn. rewrite !List.map_map. rewrite rev_app_distr. cbn. rewrite !map_rev, rev_involutive, <- app_assoc. reflexivity.
          + rewrite !map_app, !List.map_map. cbn. intros ? [<- | [(?&<-&?)%in_map_iff | [<- | ?]] % in_app_iff ]; cbn; auto.
        - (* tp = midtape ls m rs *)
          replace (inr (sigList_X (LeftBlank false)) ::
                       map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ MarkedSymbol m :: map UnmarkedSymbol rs ++ [RightBlank false])) ++ map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with
              ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls))))
                 ++ inr (sigList_X (MarkedSymbol m)) ::
                 (map inr (map sigList_X (map UnmarkedSymbol rs ++ [RightBlank false])) ++
                      map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP])) in H.
          rewrite MoveToSymbol_correct_midtape in H; cbn; auto.
          + cbn in *. TMSimp. split; auto. hnf.
            rewrite !map_id, !List.map_map. cbv [id].
            rewrite !map_app; cbn. rewrite !List.map_map, <- !app_assoc. rewrite map_rev, rev_involutive. f_equal.
          + rewrite !List.map_map. intros ? [ <- | (?&<-&?) % in_map_iff]; cbn; auto.
          + simpl_list. cbn. f_equal. f_equal. f_equal. rewrite !map_app, <- !app_assoc. cbn. f_equal.
      }
    Qed.

    Definition GoToCurrent_steps' (tp : tape sig) :=
      match tp with
       | niltape _ => 8
       | leftof r rs => 8
       | rightof l ls => 16 + 4 * length ls
       | midtape ls m rs => 16 + 4 * length ls
       end.

    Definition GoToCurrent_steps (tp : tape sig) :=
       GoToCurrent_steps' tp + 3.

    Definition GoToCurrent_T : tRel sigSim 1 :=
      fun tin k => exists tps1 tps2 tp, atCons tin[@Fin0] tps1 tps2 tp /\ GoToCurrent_steps tp <= k.

    Lemma GoToCurrent_Terminates : projT1 GoToCurrent ↓ GoToCurrent_T.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold GoToCurrent. TM_Correct. }
      { intros tin k (tps1&tps2&tp&HCons&Hk). unfold GoToCurrent_steps in Hk.
        exists (GoToCurrent_steps' tp), 2. cbn.
        repeat split. 2: lia.
        {
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp.
          - (* tp = niltape *) do 2 ( rewrite MoveToSymbol_steps_equation; cbn in * ). reflexivity.
          - (* tp = leftof r rs *) do 2 ( rewrite MoveToSymbol_steps_equation; cbn in * ). reflexivity.
          - (* tp = rightof l ls *)
            replace (inr (sigList_X (LeftBlank false)) ::
                         map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l; RightBlank true])) ++
                         map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with
                ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l])))
                   ++ inr (sigList_X (RightBlank true)) :: (map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]))
              by (now simpl_list; cbn; rewrite <- !app_assoc).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. rewrite Nat.mul_succ_r. cbn. lia.
          - (* tp = midtape ls m rs *)
            replace (inr (sigList_X (LeftBlank false)) ::
                         map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ MarkedSymbol m :: map UnmarkedSymbol rs ++ [RightBlank false])) ++ map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with
                ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls))))
                   ++ inr (sigList_X (MarkedSymbol m)) ::
                   (map inr (map sigList_X (map UnmarkedSymbol rs ++ [RightBlank false])) ++
                        map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP])).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            + simpl_list. cbn. lia.
            + simpl_list. cbn. f_equal. f_equal. f_equal. rewrite !map_app, <- !app_assoc. cbn. f_equal.
        }
        { intros ? [] ?. exists 1, 0. repeat split. lia. lia. intros ? ? (->&->). destruct *; reflexivity. }
      }
    Qed.

  End GoToCurrent.

  Section GoToNext.

    Definition GoToNext_Rel : pRel sigSim bool 1 :=
      fun tin '(yout, tout) =>
        forall tps1 tps2 tp,
          atCons_current tin[@Fin0] tps1 tps2 tp ->
          match yout, tps2 with
          | true, tp' :: tps2' =>
            atCons tout[@Fin0] (tps1 ++ [tp]) tps2' tp'
          | false, nil =>
            atNil tout[@Fin0] (tps1 ++ [tp])
          | _, _ => False
          end.

    Definition isNilCons : sigSim -> bool :=
      fun s => match s with
            | inr sigList_nil => true
            | inr sigList_cons => true
            | _ => false
            end.

    Definition GoToNext : pTM sigSim bool 1 :=
      MoveToSymbol isNilCons id;; IsCons.

    Lemma GoToNext_Realise : GoToNext ⊨ GoToNext_Rel.
    Proof.
      eapply Realise_monotone.
      { unfold GoToNext. TM_Correct. eapply RealiseIn_Realise. apply IsCons_Sem. }
      {
        intros tin (yout, tout) H. intros tps1 tps2 tp HCons. unfold atCons_current in *. TMSimp.
        TMSimp. rename H1 into H.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp; rename H into HNil, H0 into HCons.
        { (* niltape *)
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - specialize (HNil (tps1 ++ [niltape _])). spec_assert HNil as [HNil ->]; auto.
            do 2 (rewrite MoveToSymbol_Fun_equation; cbn). hnf.
            cbv [id]. hnf. f_equal. rewrite encode_list_app. rewrite removelast_app by apply encode_list_neq_nil.
            cbn. rewrite rev_app_distr. cbn. f_equal.
          - specialize (HCons (tps1 ++ [niltape _]) tps2' tp'). spec_assert HCons as [HCons ->]; auto.
            do 2 (rewrite MoveToSymbol_Fun_equation; cbn).
            cbv [id]. hnf. f_equal.
            + rewrite encode_list_app; cbn. rewrite removelast_app by congruence.
              cbn. rewrite rev_app_distr. cbn. f_equal.
            + rewrite !List.map_map. rewrite !map_app, <- !app_assoc. now rewrite !List.map_map. }
        { (* leftof r rs *)
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - specialize (HNil (tps1 ++ [leftof r rs])). spec_assert HNil as [HNil ->]; auto.
            rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))).
            rewrite MoveToSymbol_correct_midtape; cbn in *; auto.
            + rewrite !map_id; cbv [id]. hnf. f_equal.
              simpl_list. cbn. rewrite encode_list_app. cbn.
              rewrite !map_app. cbn. rewrite !removelast_app by congruence. rewrite !removelast_cons by congruence.
              rewrite removelast_cons.
              2: { intros H. symmetry in H. now apply app_cons_not_nil in H. }
              rewrite removelast_app by congruence. cbn. rewrite app_nil_r.
              rewrite rev_app_distr. cbn. rewrite <- !app_assoc.
              rewrite !rev_app_distr, <- !app_assoc. cbn. rewrite !map_rev.
              rewrite map_app, <- !app_assoc. cbn. rewrite !map_rev, !List.map_map. f_equal.
            + intros ? [ <- | [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff ]; cbn; auto.
          - specialize (HCons (tps1 ++ [leftof r rs]) tps2' tp'). spec_assert HCons as [HCons ->]; auto.
            rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))).
            rewrite MoveToSymbol_correct_midtape; cbn in *; auto.
            + rewrite !map_id; cbv [id]. hnf. f_equal.
              * simpl_list. cbn. rewrite encode_list_app. cbn.
                rewrite !map_app. cbn. rewrite !removelast_app by congruence. rewrite !removelast_cons by congruence.
                rewrite removelast_cons.
                2: { intros H. symmetry in H. now apply app_cons_not_nil in H. }
                rewrite removelast_app by congruence. cbn. rewrite app_nil_r.
                rewrite rev_app_distr. cbn. rewrite <- !app_assoc.
                rewrite !rev_app_distr, <- !app_assoc. cbn. rewrite !map_rev.
                rewrite map_app, <- !app_assoc. cbn. rewrite !map_rev, !List.map_map. f_equal.
              * now simpl_list.
            + intros ? [ <- | [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff ]; cbn; auto.
        }
        { (* rightof l ls *)
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - specialize (HNil (tps1 ++ [rightof l ls])). spec_assert HNil as [HNil ->]; auto.
            do 2 (rewrite MoveToSymbol_Fun_equation; cbn).
            cbv [id]. hnf. f_equal.
            rewrite encode_list_app. cbn. rewrite removelast_app by congruence.
            rewrite !removelast_cons. 3: congruence.
            2: { intros H; symmetry in H; now apply app_cons_not_nil in H. }
            rewrite map_app, !List.map_map, <- !app_assoc. cbn.
            rewrite removelast_app by congruence. cbn.
            rewrite rev_app_distr; cbn. rewrite <- !app_assoc. cbn. rewrite !map_app, <- !app_assoc.
            rewrite !rev_app_distr. cbn. rewrite !map_rev, rev_involutive. rewrite !List.map_map. reflexivity.
          - specialize (HCons (tps1 ++ [rightof l ls]) tps2' tp'). spec_assert HCons as [HCons ->]; auto.
            do 2 (rewrite MoveToSymbol_Fun_equation; cbn).
            cbv [id]. hnf. f_equal.
            + rewrite encode_list_app. cbn. rewrite removelast_app by congruence.
              rewrite !removelast_cons. 3: congruence.
              2: { intros H; symmetry in H; now apply app_cons_not_nil in H. }
              rewrite map_app, !List.map_map, <- !app_assoc. cbn.
              rewrite removelast_app by congruence. cbn.
              rewrite rev_app_distr; cbn. rewrite <- !app_assoc. cbn. rewrite !map_app, <- !app_assoc.
              rewrite !rev_app_distr. cbn. rewrite !map_rev, rev_involutive. rewrite !List.map_map. reflexivity.
            + now simpl_list.
        }
        { (* midtape ls m rs *)
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - specialize (HNil (tps1 ++ [midtape ls m rs])). spec_assert HNil as [HNil ->]; auto.
            rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite MoveToSymbol_correct_midtape; cbn; auto.
            + cbn in *. TMSimp. rewrite map_id; cbv [id]. hnf. f_equal.
              rewrite encode_list_app. cbn. rewrite !map_app.
              rewrite removelast_app by congruence.
              rewrite !removelast_cons. 3: congruence.
              2: { intros H; symmetry in H; now apply app_cons_not_nil in H. }
              rewrite removelast_app by congruence. cbn. rewrite !map_rev.
              simpl_list. cbn. rewrite <- !app_assoc. cbn. rewrite !map_app. cbn. rewrite !map_rev.
              repeat first [ progress cbn | rewrite rev_app_distr | rewrite map_app | rewrite <- app_assoc | rewrite rev_involutive | rewrite map_map ].
              f_equal.
            + intros ? [ (?&<-&?) % in_map_iff | [<- | ] ] % in_app_iff; cbn; auto.
          - specialize (HCons (tps1 ++ [midtape ls m rs]) tps2' tp'). spec_assert HCons as [HCons ->]; auto.
            rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite MoveToSymbol_correct_midtape; cbn; auto.
            + cbn in *. TMSimp. rewrite map_id; cbv [id]. hnf. f_equal.
              rewrite encode_list_app. cbn. rewrite !map_app.
              * rewrite removelast_app by congruence.
                rewrite !removelast_cons. 3: congruence.
                2: { intros H; symmetry in H; now apply app_cons_not_nil in H. }
                rewrite removelast_app by congruence. cbn. rewrite !map_rev.
                simpl_list. cbn. rewrite <- !app_assoc. cbn. rewrite !map_app. cbn. rewrite !map_rev.
                repeat first [ progress cbn | rewrite rev_app_distr | rewrite map_app | rewrite <- app_assoc | rewrite rev_involutive | rewrite map_map ].
                f_equal.
              * now simpl_list.
            + intros ? [ (?&<-&?) % in_map_iff | [<- | ] ] % in_app_iff; cbn; auto.
        }
      }
    Qed.

    Definition GoToNext_steps' (t : tape sig) :=
      match t with
      | niltape _ => 8
      | leftof r rs => 16 + 4 * length rs
      | rightof r rs => 8
      | midtape ls m rs => 16 + 4 * length rs
      end.

    Definition GoToNext_steps (tp : tape sig) :=
        GoToNext_steps' tp + 3.

    Definition GoToNext_T : tRel sigSim 1 :=
      fun tin k => exists tps1 tps2 tp, atCons_current tin[@Fin0] tps1 tps2 tp /\ GoToNext_steps tp <= k.

    Lemma GoToNext_Terminates : projT1 GoToNext ↓ GoToNext_T.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold GoToNext. TM_Correct. eapply RealiseIn_TerminatesIn. apply IsCons_Sem. }
      { intros tin k (tps1&tps2&tp&HCons&Hk). hnf in HCons. unfold GoToNext_steps in Hk.
        exists (GoToNext_steps' tp), 2. repeat split. 2: lia. 2: intros _ _ _; reflexivity.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp.
        { (* tp = niltape *)
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity.
          - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity.
        }
        { (* tp = leftof r rs *)
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. lia.
          - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. lia.
        }
        { (* rightof l ls *)
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity.
          - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity.
        }
        { (* midtape ls m rs *)
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. lia.
          - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. lia.
        }
      }
    Qed.

  End GoToNext.

  (* Read the current symbols *)
  Section ReadCurrentSymbols.

    Local Arguments insertKnownSymbol : simpl never.
    (* Local Arguments insertKnownSymbols : simpl never. *)

    Definition ReadCurrent : pTM sigSim (option sig) 1 :=
      Switch ReadChar
             (fun (s : option sigSim) =>
                match s with
                | Some (inr (sigList_X (MarkedSymbol s))) => Return Nop (Some s)
                | _ => Return Nop None
                end).

    Definition ReadCurrent_Rel : pRel sigSim (option sig) 1 :=
      fun tin '(yout, tout) =>
        forall tps1 tps2 tp,
          atCons_current tin[@Fin0] tps1 tps2 tp ->
          atCons_current tout[@Fin0] tps1 tps2 tp /\
          yout = current tp.

    Definition ReadCurrent_steps := 2.

    Lemma ReadCurrent_Sem : ReadCurrent ⊨c(ReadCurrent_steps) ReadCurrent_Rel.
    Proof.
      unfold ReadCurrent_steps. eapply RealiseIn_monotone.
      { unfold ReadCurrent. TM_Correct. }
      { Unshelve. 4,5: reflexivity. all: reflexivity. }
      { intros tin (yout, tout) H. intros tps1 tps2 tp HCons.
        unfold atCons_current in *. TMSimp.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp.
        all: (split; hnf; auto).
      }
    Qed.

    Definition ReadCurrentSymbols_Step_Rel (st : Vector.t (option sig) n * Fin.t n) :
      pRel sigSim (Vector.t (option sig) n * Fin.t n + Vector.t (option sig) n) 1 :=
      fun tin '(yout, tout) =>
        (forall tps1 tps2 tp ,
            (length tps1 =? fin_to_nat (snd st)) = true ->
            (length tps1 + (1 + length tps2) =? n) = true ->
            atCons tin[@Fin0] tps1 tps2 tp ->
            knowsFirstSymbols (fst st) tps1 ->
            match tps2 with
            | nil =>
              atNil tout[@Fin0] (tps1 ++ [tp]) /\
              yout = inr (insertKnownSymbol (fst st) (snd st) (current tp))
            | tp' :: tps2' =>
              atCons tout[@Fin0] (tps1 ++ [tp]) tps2' tp' /\
              match finSucc_opt (snd st) with
              | Some i' =>
                yout = inl (insertKnownSymbol (fst st) (snd st) (current tp), i')
              | None => False
              end
            end) /\
        (forall tps,
            atNil tin[@Fin0] tps ->
            atNil tout[@Fin0] tps /\
            yout = inr (fst st)).

    Definition ReadCurrentSymbols_Step : forall (st : Vector.t (option sig) n * Fin.t n),
        pTM sigSim (Vector.t (option sig) n * Fin.t n + Vector.t (option sig) n) 1 :=
      fun '(readSymbols, i) =>
        If IsCons
           (GoToCurrent;;
            Switch (ReadCurrent)
                   (fun (c : option sig) =>
                      Return (GoToNext)
                             (match finSucc_opt i with
                              | None =>
                                inr (insertKnownSymbol readSymbols i c)
                              | Some i' =>
                                inl (insertKnownSymbol readSymbols i c, i')
                              end)))
           (Return Nop (inr readSymbols)).

    Lemma ReadCurrentSymbols_Step_Realise : forall st, ReadCurrentSymbols_Step st ⊨ ReadCurrentSymbols_Step_Rel st.
    Proof.
      intros (readSymbols,i). eapply Realise_monotone.
      { unfold ReadCurrentSymbols_Step. TM_Correct_step; [ | TM_Correct_step | TM_Correct].
        - eapply RealiseIn_Realise. apply IsCons_Sem.
        - apply GoToCurrent_Realise.
        - apply Switch_Realise.
          + eapply RealiseIn_Realise. apply ReadCurrent_Sem.
          + intros c. apply Return_Realise. apply GoToNext_Realise. }
      {
        intros tin (yout, tout). TMSimp. split.
        {
          intros tps1 tps2 tp HL1 HL2 HCons HKnown.
          destruct H; TMSimp.
          { (* cons case *)
            rename H into HIsCons_cons, H0 into HGotoCurrent, H1 into IsCons_nil, H2 into HReadCurrent, H4 into HGoToNext.
            specialize HIsCons_cons with (1 := HCons) as (HIsCons_cons&_).
            specialize HGotoCurrent with (1 := HIsCons_cons) as (HGotoCurrent&->).
            specialize HReadCurrent with (1 := HGotoCurrent) as (HReadCurrent&->).
            specialize HGoToNext with (1 := HReadCurrent).
            destruct ymid1, tps2 as [ | tp' tps2']; auto.
            { (* tps = tp' :: tps' *) split; auto.
              destruct (finSucc_opt i) as [i'| ] eqn:Ei.
              - reflexivity.
              - exfalso. apply finSucc_opt_None' in Ei. apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2. cbn in *. lia.
            }
            { (* tps = nil *) split; auto.
              enough (finSucc_opt i = None) as -> by reflexivity.
              apply finSucc_opt_None.
              apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2. cbn in *. lia.
            }
          }
          { (* wrong nil case *) specialize H with (1 := HCons) as (_&H); congruence. }
        }
        { (* nil case *)
          intros tps HNil.
          destruct H; TMSimp.
          { (* wrong cons case *) specialize H1 with (1 := HNil) as (_&H1); congruence. }
          { now specialize H2 with (1 := HNil) as (H0&_). }
        }
      }
    Qed.

    Definition ReadCurrentSymbols_Step_steps_cons tp :=
      3 + IsCons_steps + GoToCurrent_steps tp + ReadCurrent_steps + GoToNext_steps tp.

    Definition ReadCurrentSymbols_Step_steps_nil := 1 + IsCons_steps.

    Definition ReadCurrentSymbols_Step_T : tRel sigSim 1 :=
      fun tin k =>
        (exists tps1 tps2 tp, atCons tin[@Fin0] tps1 tps2 tp /\ ReadCurrentSymbols_Step_steps_cons tp <= k) \/
        (exists tps, atNil tin[@Fin0] tps /\ ReadCurrentSymbols_Step_steps_nil <= k).

    Lemma ReadCurrentSymbols_Step_Terminates st : projT1 (ReadCurrentSymbols_Step st) ↓ ReadCurrentSymbols_Step_T.
    Proof.
      destruct st as [readSymbols i]. eapply TerminatesIn_monotone.
      { unfold ReadCurrentSymbols_Step. TM_Correct_step.
        { eapply RealiseIn_Realise. apply IsCons_Sem. }
        { eapply RealiseIn_TerminatesIn. apply IsCons_Sem. }
        { TM_Correct_step. apply GoToCurrent_Realise. apply GoToCurrent_Terminates.
          apply Switch_TerminatesIn.
          - eapply RealiseIn_Realise. apply ReadCurrent_Sem.
          - eapply RealiseIn_TerminatesIn. apply ReadCurrent_Sem.
          - intros st. apply Return_Terminates. apply GoToNext_Terminates. }
        { TM_Correct. }
      }
      {
        intros tin k. intros [ (tps1&tps2&tp&HCons&Hk) | (tps&HNil&Hk) ].
        { (* cons case *) unfold ReadCurrentSymbols_Step_steps_cons in Hk.
          exists (IsCons_steps), (2 + GoToCurrent_steps tp + ReadCurrent_steps + GoToNext_steps tp). repeat split; try lia.
          intros tmid ymid (HIsCons_cons&HIsCons_nil). specialize HIsCons_cons with (1 := HCons) as (HIsCons&->).
          exists (GoToCurrent_steps tp), (1 + ReadCurrent_steps + GoToNext_steps tp). repeat split; try lia. hnf; eauto.
          intros tmid0 ymid0 HGoToCurrent. cbn in HGoToCurrent. specialize HGoToCurrent with (1 := HIsCons) as (HGoToCurrent&->).
          exists (ReadCurrent_steps), (GoToNext_steps tp). repeat split; try lia.
          intros tmid1 ymid1 HReadCurrent. cbn in HReadCurrent. specialize HReadCurrent with (1 := HGoToCurrent) as (HReadCurrent&->). hnf. eauto.
        }
        { (* nil case *) unfold ReadCurrentSymbols_Step_steps_nil in Hk.
          exists (IsCons_steps), 0. repeat split; try lia.
          intros tmid ymid (HIsCons_cons&HIsCons_nil). specialize HIsCons_nil with (1 := HNil) as (HIsNil&->). reflexivity.
        }
      }
    Qed.

    Definition ReadCurrentSymbols_Loop := StateWhile ReadCurrentSymbols_Step.

    Definition ReadCurrentSymbols_Loop_Rel (st : Vector.t (option sig) n * Fin.t n) :
      pRel sigSim (Vector.t (option sig) n) 1 :=
      fun tin '(yout, tout) =>
        (forall tps1 tp tps2,
            (length tps1 =? fin_to_nat (snd st)) = true ->
            (length tps1 + (1 + length tps2) =? n) = true ->
            atCons tin[@Fin0] tps1 tps2 tp ->
            knowsFirstSymbols (fst st) tps1 ->
            atNil tout[@Fin0] (tps1 ++ tp :: tps2) /\
            yout = insertKnownSymbols (fst st) (snd st) (current tp :: map (@current _) tps2)) /\
        (forall tps,
            (length tps =? n) = true ->
            atNil tin[@Fin0] tps ->
            knowsFirstSymbols (fst st) tps ->
            atNil tout[@Fin0] tps /\
            yout = (fst st)).

    Lemma ReadCurrentSymbols_Loop_Realise st : ReadCurrentSymbols_Loop st ⊨ ReadCurrentSymbols_Loop_Rel st.
    Proof.
      eapply Realise_monotone.
      { unfold ReadCurrentSymbols_Loop. TM_Correct. apply ReadCurrentSymbols_Step_Realise. }
      { revert st. apply StateWhileInduction; intros; rename l into st.
        {
          destruct st as [ readSymbols i]; cbn in *.
          destruct HLastStep as [HLastStepCons HLastStepNil].
          cbn. split; [intros tps1 tp tps2 HL1 HL2 HCons HRead | intros tps HL HNil HRead]; TMSimp.
          {
            specialize HLastStepCons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead).
            destruct tps2 as [ | tp' tps2']; cbn in *.
            - destruct HLastStepCons as [HLastStepCons HLastStepCons']; inv HLastStepCons'.
              split; auto.
              (*
              apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2. *)
              destruct (finSucc_opt i) as [i'| ]; auto.
            - destruct HLastStepCons as [ HLastStepCons HLastStepCons'].
              destruct (finSucc_opt i) as [i' | ]; auto. congruence.
          }
          { specialize HLastStepNil with (1 := HNil). destruct HLastStepNil as [H1 H2]. inv H2. split; auto. }
        }
        {
          destruct st as [ readSymbols i]; cbn in *.
          destruct HStar as [HStar_cons HStar_nil]. destruct HLastStep as [HLastStep_cons HLastStep_nil]. cbn in *.
          cbn. split; [intros tps1 tp tps2 HL1 HL2 HCons HRead | intros tps HL HNil HRead].
          {
            specialize HStar_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead).
            destruct tps2 as [ | tp' tps2']; cbn in *.
            - destruct HStar_cons as [HStar1 HStar2]. inv HStar2.
            - destruct HStar_cons as [HStar1 HStar2].
              destruct (finSucc_opt i) as [i' | ] eqn:E; auto. inv HStar2.
              specialize HLastStep_cons with (3 := HStar1).
              apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2.
              spec_assert HLastStep_cons.
              { simpl_list; cbn. apply Nat.eqb_eq. apply finSucc_opt_Some' in E. lia. }
              spec_assert HLastStep_cons.
              { simpl_list; cbn. apply Nat.eqb_eq. apply finSucc_opt_Some' in E. lia. }
              spec_assert HLastStep_cons as [HLastStep_cons ->].
              { cbn. apply insertKnownSymbol_correct; auto. }
              cbn in *. rewrite <- app_assoc in HLastStep_cons. split; auto.
          }
          { specialize HStar_nil with (1 := HNil) as [HStar1 HStar2]; inv HStar2. }
        }
      }
    Qed.

    Definition ReadCurrentSymbols_Loop_steps_nil := ReadCurrentSymbols_Step_steps_nil.

    Fixpoint ReadCurrentSymbols_Loop_steps_cons tps2 tp :=
      match tps2 with
      | nil => ReadCurrentSymbols_Step_steps_cons tp
      | tp' :: tps2' => 1 + ReadCurrentSymbols_Step_steps_cons tp + ReadCurrentSymbols_Loop_steps_cons tps2' tp'
      end.

    Definition ReadCurrentSymbols_Loop_T (st : Vector.t (option sig) n * Fin.t n) : tRel sigSim 1 :=
      fun tin k =>
        (exists tps1 tps2 tp,
            (length tps1 =? fin_to_nat (snd st)) = true /\
            (length tps1 + (1 + length tps2) =? n) = true /\
            knowsFirstSymbols (fst st) tps1 /\
            atCons tin[@Fin0] tps1 tps2 tp /\ ReadCurrentSymbols_Loop_steps_cons tps2 tp <= k) \/
        (exists tps, atNil tin[@Fin0] tps /\ ReadCurrentSymbols_Loop_steps_nil <= k).

    Lemma ReadCurrentSymbols_Loop_Terminates st : projT1 (ReadCurrentSymbols_Loop st) ↓ ReadCurrentSymbols_Loop_T st.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold ReadCurrentSymbols_Loop. TM_Correct.
        - apply ReadCurrentSymbols_Step_Realise.
        - apply ReadCurrentSymbols_Step_Terminates. }
      {
        revert st. apply StateWhileCoInduction. intros (readSymbols&i). intros. unfold ReadCurrentSymbols_Loop_T in *. unfold ReadCurrentSymbols_Step_T in *.
        destruct HT as [ (tps1&tps2&tp&HL1&HL2&HRead&HCons&Hk) | (tps&HNil&Hk)].
        { (* cons case *)
           eexists. repeat split. left. eauto.
           intros ymid tmid (HStep_cons&HStep_nil). clear HStep_nil. cbn in *. destruct ymid as [ (readSymbols'&i') | result ].
           - (* continue case *)
             specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead).
             destruct tps2 as [ | tp' tps2']; cbn in *.
             + TMSimp. congruence.
             + destruct HStep_cons as (HStep_cons1&HStep_cons2). destruct (finSucc_opt i) as [ i'' | ] eqn:Ei; inv HStep_cons2; rename i'' into i'.
               eexists. split. 2: apply Hk. left. exists (tps1 ++ [tp]), (tps2'), tp'. repeat split.
               * simpl_list. cbn. apply finSucc_opt_Some' in Ei. apply Nat.eqb_eq. apply Nat.eqb_eq in HL1. lia.
               * simpl_list. cbn. apply finSucc_opt_Some' in Ei. apply Nat.eqb_eq. apply Nat.eqb_eq in HL2. lia.
               * apply insertKnownSymbol_correct. now apply Nat.eqb_eq. assumption.
               * assumption.
               * reflexivity.
           - (* break case *)
             specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead).
             destruct tps2 as [ | tp' tps2']; cbn in *.
             + lia.
             + lia.
        }
        { (* nil case *)
          eexists. repeat split. right. eauto.
          intros ymid tmid (HStep_cons&HStep_nil). clear HStep_cons. cbn in *. destruct ymid as [ (readSymbols'&i') | result ].
          - (* continue case *) specialize HStep_nil with (1 := HNil) as (?&?). congruence.
          - (* break case *) reflexivity.
        }
      }
    Qed.

    Definition ReadCurrentSymbols :=
      match (finMin_opt n) with
      | None => Return (Move Rmove) (Vector.const None n) (* Nothing to do, just move from the start to the nil symbol *)
      | Some min =>
        Move Rmove;; ReadCurrentSymbols_Loop (Vector.const None n, min)
      end.

    Definition ReadCurrentSymbols_Rel : pRel sigSim (Vector.t (option sig) n) 1 :=
      fun tin '(yout, tout) =>
        forall T,
          tin[@Fin0] ≃ T ->
          atNil tout[@Fin0] (vector_to_list T) /\
          yout = current_chars T.

    Lemma ReadCurrentSymbols_Realise : ReadCurrentSymbols ⊨ ReadCurrentSymbols_Rel.
    Proof.
      clear pM F. unfold ReadCurrentSymbols.
      destruct (finMin_opt n) as [min| ] eqn:E; swap 1 2.
      {
        eapply Realise_monotone.
        { TM_Correct. }
        { intros tin (yout, tout) H. intros T HEncT. unfold contains_tapes in *. TMSimp.
          clear_except E. apply finMin_opt_None in E as ->. destruct_tapes. cbn.
          split; cbn; auto. hnf. reflexivity.
        }
      }
      {
        eapply Realise_monotone.
        { TM_Correct. apply ReadCurrentSymbols_Loop_Realise. }
        { intros tin (yout, tout) H. intros T HEncT. unfold contains_tapes in *. TMSimp.
          rename H0 into HLoop_cons, H1 into HLoop_nil. clear HLoop_nil.
          pose proof finMin_opt_Some E as (n'&E'). pose (T' := Vector.cast T E').
          pose proof finMin_opt_Some_val E as E_val.
          specialize (HLoop_cons nil (Vector.hd T') (vector_to_list (Vector.tl T'))). cbn in *.
          rewrite E_val in HLoop_cons. subst. specialize HLoop_cons with (1 := eq_refl). spec_assert HLoop_cons.
          { rewrite vector_to_list_length. apply Nat.eqb_eq. reflexivity. } spec_assert HLoop_cons.
          { hnf. cbn. clear_all. destruct_tapes. cbn. f_equal. simpl_list. now rewrite vector_cast_refl. }
          spec_assert HLoop_cons as [HLoop_cons1 ->] by (cbn; tauto).
          rewrite vector_to_list_eta in HLoop_cons1. subst T'. rewrite vector_cast_refl in *. split; auto.
          destruct (finSucc_opt min) as [minSucc | ] eqn:E2.
          - pose proof finSucc_opt_Some' E2 as E2_val. rewrite E_val in E2_val.
            now apply insertKnownSymbols_correct_cons.
          - apply finSucc_opt_None' in E2.
            apply Nat.succ_inj in E2. assert (n' = 0) as -> by lia. cbn.
            compute [insertKnownSymbol]. destruct_fin min. cbn.
            destruct_tapes. cbn. unfold current_chars. cbn. reflexivity.
        }
      }
    Qed.

    Definition ReadCurrentSymbols_steps (n : nat) (T : tapes sig n) :=
      match T with
      | [| |] => ReadCurrentSymbols_Loop_steps_nil
      | tp ::: T' => 2 + ReadCurrentSymbols_Loop_steps_cons (vector_to_list T') tp
      end.

    Definition ReadCurrentSymbols_T : tRel sigSim 1 :=
      fun tin k => exists T, tin[@Fin0] ≃ T /\ ReadCurrentSymbols_steps T <= k.

    Lemma ReadCurrentSymbols_Terminates : projT1 ReadCurrentSymbols ↓ ReadCurrentSymbols_T.
    Proof.
      unfold ReadCurrentSymbols.
      destruct (finMin_opt n) as [min| ] eqn:E.
      { eapply TerminatesIn_monotone.
        { TM_Correct. eapply ReadCurrentSymbols_Loop_Terminates. }
        {
          intros tin k (T&HEncT&Hk).
          pose proof finMin_opt_Some E as (n'&E'). pose proof finMin_opt_Some_val E as E_val.
          pose (T' := Vector.cast T E').
          exists 1, (ReadCurrentSymbols_Loop_steps_cons (vector_to_list (Vector.tl T')) (Vector.hd T')). repeat split; try lia.
          { rewrite <- Hk. clear_all. subst n T'. rewrite !vector_cast_refl. destruct_tapes. cbn. reflexivity. }
          {
            intros tmid [] HMove. cbn in HMove. hnf. left. exists (nil), (vector_to_list (Vector.tl T')), (Vector.hd T'). cbn. rewrite E_val. cbn. repeat split; auto.
            - rewrite vector_to_list_length. apply Nat.eqb_eq. lia.
            - apply knowsFirstSymbols_nil.
            - rewrite HMove. hnf in HEncT. cbn in *. rewrite HEncT. clear_all. subst n T'. cbn. rewrite !vector_cast_refl.
              destruct_tapes. cbn. hnf. f_equal. now rewrite !map_app, !List.map_map, <- !app_assoc.
          }
        }
      }
      { eapply TerminatesIn_monotone.
        { TM_Correct. }
        {
          intros tin k (T&HEnc&Hk). rewrite <- Hk. apply finMin_opt_None in E. clear_except E. subst. destruct_tapes. cbn. unfold ReadCurrentSymbols_Loop_steps_nil, ReadCurrentSymbols_Step_steps_nil. lia.
        }
      }
    Qed.

  End ReadCurrentSymbols.

  (* Move from the nil symbol back to the start symbol *)
  Section MoveToStart.

    Definition MoveToStart_Rel : pRel sigSim unit 1 :=
      ignoreParam
        (fun tin tout =>
           forall tps, atNil tin[@Fin0] tps ->
                  atStart tout[@Fin0] tps).

    Definition isStart : sigSim -> bool :=
      fun s => match s with
            | inl START => true
            | _ => false
            end.

    Definition MoveToStart : pTM sigSim unit 1 :=
      MoveToSymbol_L isStart id.

    Lemma MoveToStart_Realise : MoveToStart ⊨ MoveToStart_Rel.
    Proof.
      eapply Realise_monotone.
      { unfold MoveToStart. TM_Correct. }
      {
        intros tin (yout, tout) H. intros tps HNil. unfold atNil, atStart in *. TMSimp. clear_all.
        rewrite MoveToSymbol_L_correct_midtape; cbn; auto.
        - rewrite !map_id; cbv [id]. rewrite map_rev, rev_involutive.
          f_equal.
          change [inr (@sigList_nil (sigTape sig)); inl STOP]
            with (List.map inr [ @sigList_nil (sigTape sig)] ++ [inl STOP]).
          rewrite app_assoc, <- map_app. f_equal. f_equal.
          apply encode_list_remove.
        - intros ? (?&<-&?) % in_map_iff. cbn. reflexivity.
      }
    Qed.

    (*
    Definition tape_size (tp : tape sig) : nat :=
      match tp with
      | niltape _ => 1
      | rightof l ls => 3 + length ls
      | leftof r rs => 3 + length rs
      | midtape ls m rs => 3 + length ls + length rs
      end.

    Fixpoint tapes_size (tps : list (tape sig)) : nat :=
      match tps with
      | nil => 1
      | tp :: tps' => 1 + tape_size tp + tapes_size tps'
      end.

    Lemma tape_size_length (tp : tape sig) :
      tape_size tp = length (encode_tape tp).
    Proof. destruct tp eqn:E; cbn; simpl_list; cbn; auto. all: try lia. simpl_list. cbn. lia. Qed.

    Lemma tapes_size_length (tps : list (tape sig)) :
      tapes_size tps = length (encode_list _ tps).
    Proof.
      induction tps as  | tp tsp.
      - cbn. reflexivity.
      - cbn.  simpl_list. rewrite <- IHtsp. cbn. rewrite <- tape_size_length. lia.
    Qed.
    *)

    Definition MoveToStart_steps (tps : list (tape sig)) :=
      8 + 4 * length (encode_list _ tps).

    Definition MoveToStart_T : tRel sigSim 1 :=
      fun tin k => exists tps, atNil tin[@Fin0] tps /\ MoveToStart_steps tps <= k.

    (* TODO: somewhere *)
    Lemma removelast_length (X : Type) (xs : list X) :
      length (removelast xs) = length xs - 1.
    Proof.
      induction xs as [ | x xs IH].
      - cbn. reflexivity.
      - cbn. destruct xs as [ | x' xs]; cbn in *.
        + reflexivity.
        + f_equal. rewrite IH. lia.
    Qed.

    Lemma MoveToStart_Terminates : projT1 MoveToStart ↓ MoveToStart_T.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold MoveToStart. TM_Correct. }
      {
        intros tin k (tps&HNil&Hk). hnf in HNil. TMSimp. rewrite MoveToSymbol_L_steps_midtape; cbn; auto. simpl_list. cbn.
        rewrite <- Hk. rewrite removelast_length. unfold MoveToStart_steps. lia.
      }
    Qed.

    Lemma atStart_contains (t : tape sigSim) (tps : list (tape sig)) (T : tapes sig n) :
      length tps = n ->
      atStart t tps ->
      vector_to_list T = tps ->
      t ≃ T.
    Proof.
      clear pM F.
      intros HL HStart HToList. unfold contains_tapes, atStart in *. subst.
      f_equal. f_equal. f_equal. unfold encode_tapes. f_equal. auto.
    Qed.

  End MoveToStart.

  Section DoActions.

    Variable (acts : Vector.t (option sig * move) n).

    (* Abuse UNKNOWN as a special marker, to return to the place where we inserted the symbol with shifting *)
    Definition isReturnMarker (s : sigSim) : bool :=
      match s with
      | inl UNKNOWN => true
      | _ => false
      end.

    (* The more complicated part is writing, because we may have to alocate more memory by shifting *)

    Definition DoWrite_Rel (d : option move) (s : sig) : pRel sigSim unit 1 :=
      ignoreParam
        (fun tin tout =>
           forall tps1 tps2 tp,
             tape_dir tp = d ->
             atCons_current tin[@Fin0] tps1 tps2 tp ->
             atCons_current tout[@Fin0] tps1 tps2 (tape_write tp (Some s))).

    Definition DoWrite (d : option move) (s : sig) : pTM sigSim unit 1 :=
      match d with
      | Some Lmove => (* leftof ~> shift left and change boundary symbol to LeftBlank false *)
        Shift_L (fun _ => false) (inl UNKNOWN);;
        MoveToSymbol isReturnMarker id;;
        WriteMove (inr (sigList_X (MarkedSymbol s))) Lmove;;
        WriteMove (inr (sigList_X (LeftBlank false))) Rmove
      | Some Rmove => (* rightof ~> shift right and change boundary symbol to RightBlank false *)
        Shift (fun _ => false) (inl UNKNOWN);;
        MoveToSymbol_L isReturnMarker id;;
        WriteMove (inr (sigList_X (MarkedSymbol s))) Rmove;;
        WriteMove (inr (sigList_X (RightBlank false))) Lmove
      | Some Nmove => (* midtape ~> just write the symbol *)
        Write (inr (sigList_X (MarkedSymbol s)))
      | None => (* midtape ~> we need to shift left and right and insert RightBlank false and LeftBlank false *)
        Shift (fun _ => false) (inl UNKNOWN);;
        MoveToSymbol_L isReturnMarker id;;
        Shift_L (fun _ => false) (inr (sigList_X (MarkedSymbol s)));;
        MoveToSymbol isReturnMarker id;;
        WriteMove (inr (sigList_X (LeftBlank false))) Rmove;;
        Move Rmove;;
        WriteMove (inr (sigList_X (RightBlank false))) Lmove
      end.

    Lemma DoWrite_Realise (d : option move) (s : sig) : DoWrite d s ⊨ DoWrite_Rel d s.
    Proof.
      unfold DoWrite. destruct d as [ [ | | ] | ].
      { (* Some Lmove (leftof) *) eapply Realise_monotone. TM_Correct.
        intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. unfold atCons_current in *. TMSimp.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. simpl_tape.
        unfold atCons_current_leftof in HCons. TMSimp.
        rewrite app_comm_cons. rewrite Shift_L_fun_correct_midtape; auto.
        rewrite app_comm_cons'. rewrite MoveToSymbol_correct_midtape; cbn; auto.
        - hnf. cbn. f_equal. f_equal. rewrite map_id, rev_app_distr; cbn; cbv [id].
          rewrite rev_app_distr. cbn. rewrite rev_involutive. reflexivity.
        - rewrite map_rev, rev_involutive.
          intros ? [ [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff | [ <- | ] ] % in_app_iff; cbn; auto.
      }
      { (* Some Rmove (rightof) *) eapply Realise_monotone. TM_Correct.
        intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. unfold atCons_current in *. TMSimp.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. simpl_tape.
        unfold atCons_current_rightof in HCons. TMSimp.
        rewrite Shift_fun_correct_midtape; auto.
        rewrite app_comm_cons'. rewrite MoveToSymbol_L_correct_midtape; cbn; auto.
        - hnf. cbn. f_equal. f_equal. rewrite map_id, rev_app_distr; cbn. now rewrite rev_involutive.
        - intros ? [ (?&<-&?) % in_rev % in_map_iff | [ <- | ] ] % in_app_iff; cbn; auto.
      }
      { (* Some Nmove (midtape) *) eapply Realise_monotone. TM_Correct.
        intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. unfold atCons_current in *. TMSimp.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
        unfold atCons_current_midtape in HCons. TMSimp.
        hnf. cbn. reflexivity.
      }
      { (* None (niltape) *) eapply Realise_monotone. TM_Correct.
        intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. unfold atCons_current in *. TMSimp.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
        unfold atCons_current_niltape in HCons. TMSimp.
        simpl_tape. rewrite Shift_fun_correct_midtape; auto. cbn.
        rewrite app_comm_cons'. rewrite MoveToSymbol_L_correct_midtape; cbn; auto.
        + rewrite app_comm_cons. rewrite Shift_L_fun_correct_midtape; auto; cbn.
          rewrite map_rev, rev_involutive, !map_id. rewrite MoveToSymbol_correct_midtape; cbn; auto.
          * simpl_tape. rewrite !map_id. cbv [id]. cbn. rewrite !rev_app_distr. cbn.
            hnf. cbn. rewrite <- !map_rev. rewrite !rev_involutive. reflexivity.
          * intros ? [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff; cbn; auto.
        + intros ? [ (?&<-&?) % in_rev % in_map_iff | [ <- | ] ] % in_app_iff; cbn; auto.
      }
    Qed.

    Definition DoWrite_steps (d : option move) (tps1 tps2 : list (tape sig)) :=
      match d with
      | Some Lmove => 37 + 8 * length (encode_list _ tps1)
      | Some Rmove => 37 + 8 * length (encode_list _ tps2)
      | Some Nmove => 1
      | None => 73 + 8 * length (encode_list _ tps1) + 8 * length (encode_list _ tps2)
      end.

    Definition DoWrite_T (d : option move) : tRel sigSim 1 :=
      fun tin k => exists tps1 tps2 tp, tape_dir tp = d /\ atCons_current tin[@Fin0] tps1 tps2 tp /\ DoWrite_steps d tps1 tps2 <= k.

    Lemma DoWrite_Terminates (d : option move) (s : sig) : projT1 (DoWrite d s) ↓ DoWrite_T d.
    Proof.
      unfold DoWrite. destruct d as [ [ | | ] | ].
      { (* d = Some Lmove (leftof) *) eapply TerminatesIn_monotone. TM_Correct.
        intros tin k (tps1&tps2&tp&HDir&HCons&Hk). cbn in *.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir.
        unfold atCons_current_leftof in HCons. TMSimp.
        exists (16 + 4 * length (encode_list _ tps1)), (20 + 4 * length (encode_list _ tps1)). repeat split.
        { rewrite Shift_steps_local. simpl_list; cbn. rewrite removelast_length. lia. }
        { lia. }
        intros tmid [] ->. exists (16 + 4 * length (encode_list _ tps1)), 3. repeat split.
        { rewrite app_comm_cons. rewrite Shift_L_fun_correct_midtape; auto. rewrite app_comm_cons'. rewrite MoveToSymbol_steps_midtape; cbn; auto.
          simpl_list. rewrite removelast_length. cbn. lia. }
        { lia. }
        intros ? [] ?. exists 1, 1. repeat split. reflexivity. reflexivity. intros _ _ _. reflexivity.
      }
      { (* d = Some Rmove (rightof) *) eapply TerminatesIn_monotone. TM_Correct.
        intros tin k (tps1&tps2&tp&HDir&HCons&Hk). cbn in *.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir.
        unfold atCons_current_rightof in HCons. TMSimp.
        exists (16 + 4 * length (encode_list _ tps2)), (20 + 4 * length (encode_list _ tps2)). repeat split.
        { rewrite Shift_steps_local. simpl_list; cbn. lia. }
        { lia. }
        intros tmid [] ->. exists (16 + 4 * length (encode_list _ tps2)), 3. repeat split.
        { rewrite app_comm_cons. rewrite Shift_fun_correct_midtape; auto. rewrite app_comm_cons'. rewrite MoveToSymbol_L_steps_midtape; cbn; auto.
          simpl_list. cbn. lia. }
        { lia. }
        intros ? [] ?. exists 1, 1. repeat split. reflexivity. reflexivity. intros _ _ _. reflexivity.
      }
      { (* d = Somme Nmove (midtape) *) eapply TerminatesIn_monotone. TM_Correct.
        intros tin k (tps1&tps2&tp&HDir&HCons&Hk). cbn in *. assumption.
      }
      { (* d = None (niltapp) *) eapply TerminatesIn_monotone. TM_Correct.
        intros tin k (tps1&tps2&tp&HDir&HCons&Hk). cbn in *.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir.
        unfold atCons_current_niltape in HCons. TMSimp.
        rewrite Shift_fun_correct_midtape; auto. cbn.
        exists (16 + 4 * length (encode_list _ tps2)), (56 + 8 * length (encode_list _ tps1) + 4 * length (encode_list _ tps2)). repeat split; try lia.
        { rewrite Shift_steps_local. simpl_list. cbn. lia. }
        intros tmid [] ->. exists (16 + 4 * length (encode_list _ tps2)), (39 + 8 * length (encode_list _ tps1)). repeat split; try lia.
        { rewrite app_comm_cons. rewrite app_comm_cons'. rewrite MoveToSymbol_L_steps_midtape; cbn; auto. simpl_list. cbn. lia. }
        intros tmid0 [] ->.
        rewrite app_comm_cons. rewrite app_comm_cons'. rewrite MoveToSymbol_L_correct_midtape; cbn; auto.
        2: { intros ? [ (?&<-&?) % in_rev % in_map_iff | [ <- | ] ] % in_app_iff; cbn; auto. }
        exists (16 + 4 * length (encode_list _ tps1)), (22 + 4 * length (encode_list _ tps1)). repeat split; try lia.
        { rewrite Shift_steps_local. simpl_list. cbn. rewrite removelast_length. lia. }
        intros tmid1 [] ->. exists (16 + 4 * length (encode_list _ tps1)), (5). repeat split; try lia.
        { rewrite app_comm_cons. rewrite Shift_L_fun_correct_midtape; auto. rewrite MoveToSymbol_steps_midtape; cbn; auto.
          simpl_list. rewrite removelast_length. cbn. lia. }
        (* constant time *)
        intros ? [] ?. exists 1, 3. repeat split. reflexivity. reflexivity. intros ? ? ?. exists 1, 1. repeat split. reflexivity. reflexivity. intros _ _ _. reflexivity.
      }
    Qed.

    Definition DoMove_Rel (d : option move) (m : move) : pRel sigSim unit 1 :=
      ignoreParam
        (fun tin tout =>
           forall tps1 tps2 tp,
             tape_dir tp = d ->
             atCons_current tin[@Fin0] tps1 tps2 tp ->
             atCons_current tout[@Fin0] tps1 tps2 (tape_move tp m)).

    Definition toggle_marked (s : sigTape sig) : sigTape sig :=
      match s with
      | UnmarkedSymbol s => MarkedSymbol s
      | MarkedSymbol s => UnmarkedSymbol s
      | LeftBlank b => LeftBlank (negb b)
      | RightBlank b => RightBlank (negb b)
      | NilBlank => NilBlank
      end.

    Definition ToggleMarked_Rel : pRel sigSim unit 1 :=
      ignoreParam (fun tin tout => forall ls m rs,
                       tin[@Fin0] = midtape ls (inr (sigList_X m)) rs ->
                       tout[@Fin0] = midtape ls (inr (sigList_X (toggle_marked m))) rs).

    Definition ToggleMarked : pTM sigSim unit 1 :=
      Switch ReadChar
             (fun (s : option sigSim) =>
                match s with
                | Some (inr (sigList_X m)) => Write (inr (sigList_X (toggle_marked m)))
                | _ => Nop
                end).

    Lemma ToggleMarked_Sem : ToggleMarked ⊨c(3) ToggleMarked_Rel.
    Proof.
      eapply RealiseIn_monotone.
      { unfold ToggleMarked. TM_Correct. }
      { Unshelve. 4, 11: reflexivity. all: lia. }
      { intros tin ([], tout) H. intros ls m rs Hmidtape. TMCrush; TMSolve 1. }
    Qed.

    (* this should take constant time *)
    Definition DoMove (d : option move) (m : move) : pTM sigSim unit 1 :=
      match d with
      | Some Lmove => match m with
                 | Nmove => Nop
                 | Lmove => Nop
                 | Rmove => ToggleMarked;; Move Rmove;; ToggleMarked
                 end
      | Some Rmove => match m with
                 | Nmove => Nop
                 | Rmove => Nop
                 | Lmove => ToggleMarked;; Move Lmove;; ToggleMarked
                 end
      | Some Nmove => match m with
                 | Nmove => Nop
                 | Rmove => ToggleMarked;; Move Rmove;; ToggleMarked
                 | Lmove => ToggleMarked;; Move Lmove;; ToggleMarked
                 end
      | None => Nop
      end.


    Definition DoMove_steps := 9.

    Lemma DoMove_Sem (d : option move) (m : move) : DoMove d m ⊨c(DoMove_steps) DoMove_Rel d m.
    Proof.
      unfold DoMove_steps. unfold DoMove. destruct d as [ [ | | ] | ].
      { (* leftof *)
        destruct m; cbn.
        { eapply RealiseIn_monotone. TM_Correct. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_leftof in *. TMSimp. f_equal. }
        { eapply RealiseIn_monotone. TM_Correct; apply ToggleMarked_Sem. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_leftof, atCons_current_midtape in *. TMSimp.
          specialize H with (1 := eq_refl); TMSimp; specialize H1 with (1 := eq_refl); TMSimp. f_equal. }
        { eapply RealiseIn_monotone. TM_Correct. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_leftof in *. TMSimp. f_equal. }
      }
      { (* rightof *)
        destruct m; cbn.
        { eapply RealiseIn_monotone. TM_Correct; apply ToggleMarked_Sem. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_rightof, atCons_current_midtape in *. TMSimp.
          specialize H with (1 := eq_refl); TMSimp; specialize H1 with (1 := eq_refl); TMSimp. f_equal. }
        { eapply RealiseIn_monotone. TM_Correct. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_rightof in *. TMSimp. f_equal. }
        { eapply RealiseIn_monotone. TM_Correct. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_rightof in *. TMSimp. f_equal. }
      }
      { (* midtape *)
        destruct m; cbn.
        { (* Lmove *)
          eapply RealiseIn_monotone. TM_Correct; apply ToggleMarked_Sem. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_midtape, atCons_current_midtape in *. TMSimp.
          specialize H with (1 := eq_refl); TMSimp.
          destruct ls as [ | l' ls']; cbn in *.
          { specialize H1 with (1 := eq_refl). TMSimp. hnf. f_equal. }
          { specialize H1 with (1 := eq_refl). TMSimp. hnf. f_equal. }
        }
        { (* Rmove *)
          eapply RealiseIn_monotone. TM_Correct; apply ToggleMarked_Sem. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_midtape in *. TMSimp.
          specialize H with (1 := eq_refl); TMSimp.
          destruct rs as [ | r' rs']; cbn in *.
          { specialize H1 with (1 := eq_refl). TMSimp. hnf. f_equal. }
          { specialize H1 with (1 := eq_refl). TMSimp. hnf. f_equal. }
        }
        { (* Nmove *)
          eapply RealiseIn_monotone. TM_Correct; apply ToggleMarked_Sem. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp.
          unfold atCons_current_midtape in *. TMSimp. f_equal. }
      }
      { (* niltape *)
        eapply RealiseIn_monotone. TM_Correct; apply ToggleMarked_Sem. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons.
        destruct tp as [ | r rs | l ls | ls m' rs ]; cbn in *; inv HDir; TMSimp.
        now simpl_tape in *.
      }
    Qed.

    Arguments DoMove : simpl never.

    (* First write, then move *)
    Definition DoAction_Rel (d : option move) (a : option sig * move) : pRel sigSim unit 1 :=
      ignoreParam
        (fun tin tout =>
           forall (tps1 tps2 : list (tape sig)) (tp : tape sig),
             tape_dir tp = d ->
             atCons_current tin[@Fin0] tps1 tps2 tp ->
             atCons_current tout[@Fin0] tps1 tps2 (doAct tp a)).

    Definition DoAction (d : option move) (a : option sig * move) : pTM sigSim unit 1 :=
      match (fst a) with
      | Some s => DoWrite d s;; DoMove (Some Nmove) (snd a) (* after wrting, we have a midtape *)
      | None => DoMove d (snd a)
      end.

    Lemma DoAction_Realise (d : option move) (a : option sig * move) : DoAction d a ⊨ DoAction_Rel d a.
    Proof.
      unfold DoAction. destruct a as [[ w | ] m]; cbn.
      { (* Write w and move m *)
        eapply Realise_monotone. TM_Correct. apply DoWrite_Realise. eapply RealiseIn_Realise. apply DoMove_Sem.
        intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. TMSimp.
        rename H into HWrite, H0 into HMove.
        specialize HWrite with (1 := eq_refl) (2 := HCons).
        specialize (HMove tps1 tps2 (midtape (left tp) w (right tp))). cbn in *. auto.
      }
      { (* Just move m *)
        eapply Realise_monotone. eapply RealiseIn_Realise. apply DoMove_Sem.
        intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. TMSimp.
        specialize H with (1 := eq_refl) (2 := HCons). auto.
      }
    Qed.

    Definition DoAction_steps (d : option move) (a : option sig * move) (tps1 tps2 : list (tape sig)) :=
      match (fst a) with
      | Some s => 1 + DoWrite_steps d tps1 tps2 + DoMove_steps
      | None => DoMove_steps
      end.

    Definition DoAction_T (d : option move) (a : option sig * move) : tRel sigSim 1 :=
      fun tin k => exists tps1 tps2 tp, tape_dir tp = d /\ atCons_current tin[@Fin0] tps1 tps2 tp /\ DoAction_steps d a tps1 tps2 <= k.

    Lemma DoAction_Terminates (d : option move) (a : option sig * move) : projT1 (DoAction d a) ↓ DoAction_T d a.
    Proof.
      unfold DoAction. destruct a as [ [ w | ] m]; cbn in *.
      { (* Write and Move *) eapply TerminatesIn_monotone.
        { TM_Correct.
          - apply DoWrite_Realise.
          - apply DoWrite_Terminates.
          - eapply RealiseIn_TerminatesIn. apply DoMove_Sem. }
        { intros tin k. intros (tps1&tps2&tp&HDir&HCons&Hk). cbn in *. exists (DoWrite_steps d tps1 tps2), DoMove_steps. repeat split; try lia.
          { hnf. do 3 eexists. repeat split; eauto. }
        }
      }
      { (* Only Move *) eapply TerminatesIn_monotone.
        { eapply RealiseIn_TerminatesIn. apply DoMove_Sem. }
        { intros tin k. intros (tps1&tps2&tp&HDir&HCons&Hk). cbn in *. assumption. }
      }
    Qed.

    Definition DoActions_Step_Rel (i : Fin.t n) : pRel sigSim (Fin.t n + unit) 1 :=
      fun tin '(yout, tout) =>
        (forall tps1 tps2 tp,
            (length tps1 =? fin_to_nat i) = true ->
            (length tps1 + (1 + length tps2) =? n) = true ->
            atCons tin[@Fin0] tps1 tps2 tp ->
            match tps2 with
            | tp' :: tps2' =>
              atCons tout[@Fin0] (tps1 ++ [doAct tp acts[@i]]) tps2' tp' /\
              match finSucc_opt i with
              | Some i' => yout = inl i'
              | None => False
              end
            | nil =>
              atNil tout[@Fin0] (tps1 ++ [doAct tp acts[@i]]) /\
              yout = inr tt
            end) /\
        (forall tps,
            atNil tin[@Fin0] tps ->
            atNil tout[@Fin0] tps /\
            yout = inr tt).

    Definition opt_to_sum_unit (X : Type) (x : option X) : X + unit :=
      match x with
      | Some x => inl x
      | None => inr tt
      end.

    Definition DoActions_Step (i : Fin.t n) : pTM sigSim (Fin.t n + unit) 1 :=
      If IsCons
         (Switch GoToCurrent
                 (fun (d : option move) =>
                    Return (DoAction d (acts[@i]);; GoToNext) (opt_to_sum_unit (finSucc_opt i))))
         (Return Nop (inr tt)).

    Lemma DoActions_Step_Realise (i : Fin.t n) : DoActions_Step i ⊨ DoActions_Step_Rel i.
    Proof.
      eapply Realise_monotone.
      { apply If_Realise.
        { eapply RealiseIn_Realise. apply IsCons_Sem. }
        { apply Switch_Realise.
          - apply GoToCurrent_Realise.
          - intros d. TM_Correct.
            + apply DoAction_Realise.
            + apply GoToNext_Realise. }
        { TM_Correct. }
      }
      {
        intros tin (yout, tout) H; split.
        { (* cons case *)
          intros tps1 tps2 tp HL1 HL2 HCons. TMSimp.
          destruct H; TMSimp; swap 1 2.
          { specialize H with (1 := HCons) as (_&?). congruence. }
          rename H into HIsCons, H0 into HGoToCurrent, H3 into HDoAct, H4 into HDoActs_Step.
          specialize HIsCons with (1 := HCons) as (HIsCons&_).
          specialize HGoToCurrent with (1 := HIsCons) as (HGoToCurrent1&->).
          apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2.
          specialize HDoAct with (1 := eq_refl) (2 := HGoToCurrent1).
          specialize HDoActs_Step with (1 := HDoAct).
          destruct tps2 as [ | tp' tps2']; (destruct ymid0; auto).
          - split; auto. cbn in *.
            unshelve epose proof @finSucc_opt_None n i _ as ->. lia. reflexivity.
          - split; auto. cbn in *.
            unshelve epose proof @finSucc_opt_Some n i _ as (i'&->). lia. reflexivity.
        }
        { (* nil case *)
          intros tps HNil.
          destruct H; TMSimp.
          { specialize H1 with (1 := HNil) as (_&?). congruence. }
          now specialize H2 with (1 := HNil) as (HIsNil&_).
        }
      }
    Qed.

    Definition DoActions_Step_steps_cons i tps1 tps2 tp :=
      3 + IsCons_steps + GoToCurrent_steps tp + DoAction_steps (tape_dir tp) (acts[@i]) tps1 tps2 + GoToNext_steps (doAct tp acts[@i]).

    Definition DoActions_Step_steps_nil := 1 + IsCons_steps.

    Definition DoActions_Step_T (i : Fin.t n) : tRel sigSim 1 :=
      fun tin k =>
        (exists tps1 tps2 tp,
            (length tps1 =? fin_to_nat i) = true /\
            (length tps1 + (1 + length tps2) =? n) = true /\
            atCons tin[@Fin0] tps1 tps2 tp /\
            DoActions_Step_steps_cons i tps1 tps2 tp <= k) \/
        (exists tps, atNil tin[@Fin0] tps /\ DoActions_Step_steps_nil <= k).

    Lemma DoActions_Step_Terminates (i : Fin.t n) : projT1 (DoActions_Step i) ↓ DoActions_Step_T i.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold DoActions_Step. TM_Correct_step.
        { eapply RealiseIn_Realise. apply IsCons_Sem. }
        { eapply RealiseIn_TerminatesIn. apply IsCons_Sem. }
        { apply Switch_TerminatesIn. apply GoToCurrent_Realise. apply GoToCurrent_Terminates. intros i'.
          TM_Correct. apply DoAction_Realise. apply DoAction_Terminates. apply GoToNext_Terminates. }
        { TM_Correct. }
      }
      {
        intros tin k [ (tps1&tps2&tp&HL1&HL2&HCons&Hk) | (tps&HNil&Hk) ].
        { (* cons case *) unfold DoActions_Step_steps_cons in Hk.
          exists (IsCons_steps), (2 + GoToCurrent_steps tp + DoAction_steps (tape_dir tp) (acts[@i]) tps1 tps2 + GoToNext_steps (doAct tp acts[@i])). repeat split; try lia.
          intros tmid ymid (HIsCons_cons&_). specialize HIsCons_cons with (1 := HCons) as (HIsCons&->).
          exists (GoToCurrent_steps tp), (1 + DoAction_steps (tape_dir tp) (acts[@i]) tps1 tps2 + GoToNext_steps (doAct tp acts[@i])). repeat split; try lia.
          { hnf. eauto. }
          intros tmid0 ymid0 HGoToCurrent. cbn in HGoToCurrent. specialize HGoToCurrent with (1 := HIsCons) as (HGoToCurrent&->).
          exists (DoAction_steps (tape_dir tp) (acts[@i]) tps1 tps2), (GoToNext_steps (doAct tp acts[@i])). repeat split; try lia.
          { hnf. eauto 6. }
          intros tmid1 ymid1 HDoAction. cbn in HDoAction. specialize HDoAction with (1 := eq_refl) (2 := HGoToCurrent).
          { hnf. eauto. }
        }
        { (* nil case *) unfold DoActions_Step_steps_nil in Hk.
          exists IsCons_steps, 0. repeat split; try lia.
          intros tmid ymid (_&HIsCons_nil). specialize HIsCons_nil with (1 := HNil) as (HIsNil&->). reflexivity.
        }
      }
    Qed.

    Definition DoActions_Loop : Fin.t n -> pTM sigSim unit 1 := StateWhile DoActions_Step.

    Definition DoActions_Loop_Rel (i : Fin.t n) : pRel sigSim unit 1 :=
      fun tin '(yout, tout) =>
        (forall tps1 tps2 tp,
            (length tps1 =? fin_to_nat i) = true ->
            (length tps1 + (1 + length tps2) =? n) = true ->
            atCons tin[@Fin0] (map_vect_list (@doAct sig) acts tps1) tps2 tp ->
            atNil tout[@Fin0] (map_vect_list (@doAct sig) acts (tps1 ++ tp :: tps2))
        ) /\
        (forall tps,
            atNil tin[@Fin0] tps ->
            atNil tout[@Fin0] tps).

    Lemma DoActions_Loop_Realise (i : Fin.t n) : DoActions_Loop i ⊨ DoActions_Loop_Rel i.
    Proof.
      eapply Realise_monotone.
      { unfold DoActions_Loop. TM_Correct.
        - apply DoActions_Step_Realise. }
      {
        revert i; apply StateWhileInduction; intros; rename l into i.
        { (* cons case *)
          split.
          {
            intros tps1 tps2 tp HL1 HL2 HCons. TMSimp. rename H into HCaseCons, H0 into HCaseNil.
            specialize HCaseCons with (3 := HCons).
            do 2 spec_assert HCaseCons by now rewrite map_vect_list_length.
            destruct tps2 as [ | tp' tps']; destruct HCaseCons as [HCaseCons1 HCaseCons2].
            - apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2; cbn in *.
              assert (S (fin_to_nat i) = n) by lia. clear HCaseCons2.
              replace (map_vect_list (doAct (sig:=eqType_X (type sig))) acts (tps1 ++ [tp])) with
                  (map_vect_list (doAct (sig:=eqType_X (type sig))) acts tps1 ++ [doAct tp acts[@i]]); auto.
              symmetry. apply map_vect_list_app. lia.
            - apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2; cbn in *.
              assert (S (fin_to_nat i) < n) by lia.
              apply finSucc_opt_Some in H as (i'&H). rewrite H in HCaseCons2. inv HCaseCons2.
          }
          { intros tps HNil. TMSimp. now specialize H0 with (1 := HNil). }
        }
        { (* nil case *)
          split.
          {
            intros tps1 tps2 tp HL1 HL2 HCons. TMSimp.
            rename H1 into HCaseCons1, H2 into HCaseNil1, H into HCaseCons2, H0 into HCaseNil2.
            specialize HCaseCons1 with (3 := HCons).
            do 2 spec_assert HCaseCons1 by now rewrite map_vect_list_length.
            destruct tps2 as [ | tp' tps2'].
            - destruct HCaseCons1 as [ _ ? ]. inv H.
            - destruct HCaseCons1 as [ HCaseCons1 ? ]. destruct (finSucc_opt i) as [ i' | ] eqn:E; auto. inv H.
              apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2; cbn in *.
              rewrite <- map_vect_list_app in HCaseCons1 by lia.
              specialize HCaseCons2 with (3 := HCaseCons1).
              spec_assert HCaseCons2.
              { apply Nat.eqb_eq. rewrite app_length. cbn.
                enough (fin_to_nat i' = S (fin_to_nat i)) by lia.
                now apply finSucc_opt_Some'. }
              spec_assert HCaseCons2.
              { apply Nat.eqb_eq. rewrite app_length. cbn. lia. }
              rewrite <- app_assoc in HCaseCons2. cbn in *. auto.
          }
          { intros tps HNil. TMSimp. now specialize H2 with (1 := HNil). }
        }
      }
    Qed.

    Definition DoActions_Loop_steps_nil := DoActions_Step_steps_nil.

    Fixpoint DoActions_Loop_steps_cons (i : Fin.t n) tps1 tps2 tp :=
      match tps2 with
      | nil => DoActions_Step_steps_cons i tps1 [] tp
      | tp' :: tps2' =>
        match finSucc_opt i with
        | None => 0 (* can't happen *)
        | Some i' =>
          1 + DoActions_Step_steps_cons i tps1 tps2 tp + DoActions_Loop_steps_cons i' (tps1 ++ [doAct tp acts[@i]]) tps2' tp'
        end
      end.

    Definition DoActions_Loop_T (i : Fin.t n) : tRel sigSim 1 :=
      fun tin k =>
        (exists tps1 tps2 tp,
            (length tps1 =? fin_to_nat i) = true /\
            (length tps1 + (1 + length tps2) =? n) = true /\
            atCons tin[@Fin0] tps1 tps2 tp /\
            DoActions_Loop_steps_cons i tps1 tps2 tp <= k) \/
        (exists tps, atNil tin[@Fin0] tps /\ DoActions_Loop_steps_nil <= k).

    Lemma DoActions_Loop_Terminates (i : Fin.t n) : projT1 (DoActions_Loop i) ↓ DoActions_Loop_T i.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold DoActions_Loop. TM_Correct.
        - apply DoActions_Step_Realise.
        - apply DoActions_Step_Terminates. }
      {
        revert i. apply StateWhileCoInduction; intros i; intros. destruct HT as [ (tps1&tps2&tp&HL1&HL2&HCons&Hk) | (tps&HNil&Hk) ].
        { (* cons case *)
          exists (DoActions_Step_steps_cons i tps1 tps2 tp). repeat split.
          { hnf. left. eauto 7. }
          intros ymid mmid (HStep_cons&HStep_nil). destruct ymid as [ i' | [] ].
          { (* continue case *) specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons).
            destruct tps2 as [ | tp' tps2']; cbn in *.
            - destruct HStep_cons as (?&?); congruence.
            - destruct HStep_cons as [HStep_cons HStep_cons']. destruct (finSucc_opt i) as [ iSucc | ] eqn:Ei; auto. inv HStep_cons'. rename iSucc into i'.
              eexists. split; eauto.
              { hnf. left. exists (tps1 ++ [doAct tp acts[@i]]), tps2', tp'. simpl_list. cbn. apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2.
                apply finSucc_opt_Some' in Ei. repeat split; auto; apply Nat.eqb_eq; lia. }
          }
          { (* false break case *) specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons).
            destruct tps2 as [ | tp' tps2']; cbn in *.
            - destruct HStep_cons as (HStep_cons&_). auto.
            - destruct HStep_cons as (?&?). destruct (finSucc_opt i); auto; congruence.
          }
        }
        { (* nil case *) exists (DoActions_Step_steps_nil). repeat split.
          { hnf. right. eauto. }
          intros ymid tmid (HStep_cons&HStep_nil). destruct ymid as [ i' | ]; cbn in *.
          - specialize HStep_nil with (1 := HNil) as (HStep_nil&HStep_nil'); inv HStep_nil'.
          - specialize HStep_nil with (1 := HNil) as (HStep_nil&HStep_nil'); inv HStep_nil'. auto.
        }
      }
    Qed.


    Definition DoActions_Rel : pRel sigSim unit 1 :=
      ignoreParam
        (fun tin tout =>
           forall (tps : list (tape sig)),
             (length tps =? n) = true ->
             atStart tin[@Fin0] tps ->
             atNil tout[@Fin0] (map_vect_list (@doAct _) acts tps)).

    Definition DoActions : pTM sigSim unit 1 :=
      match finMin_opt n with
      | None => Move Rmove (* Nothing to do, just move from the start to the nil symbol *)
      | Some i =>
        Move Rmove;; (* Move from start to first cons *)
        DoActions_Loop i
      end.

    Lemma DoActions_Realise : DoActions ⊨ DoActions_Rel.
    Proof.
      clear pM F.
      unfold DoActions.
      destruct (finMin_opt n) as [ i | ] eqn:E; swap 1 2.
      {
        eapply Realise_monotone.
        { TM_Correct. }
        {
          intros tin ([], tout) H. intros tps HL HStart. cbn in *. intros. TMSimp.
          unfold atStart in HStart. TMSimp.
          apply finMin_opt_None in E as ->.
          destruct tps; cbn in *; inv HL.
          hnf. cbn. reflexivity.
        }
      }
      {
        eapply Realise_monotone.
        { TM_Correct. apply DoActions_Loop_Realise. }
        {
          intros tin ([], tout) H. intros tps HL HStart. TMSimp.
          rename H0 into HLoop_Nil, H1 into HLoop_Cons. clear HLoop_Cons.
          pose proof finMin_opt_Some E as (n'&E').
          apply finMin_opt_Some_val in E. subst.
          destruct tps as [ | tp tps]; cbn in *. inv HL.
          specialize (HLoop_Nil nil tps tp).
          spec_assert HLoop_Nil by now rewrite E. spec_assert HLoop_Nil by auto. spec_assert HLoop_Nil.
          { cbn. unfold atStart in HStart. TMSimp. hnf. f_equal. now rewrite map_app, <- app_assoc. }
          destruct_vector. cbn. auto.
        }
      }
    Qed.

    Definition DoActions_steps (tps : list (tape sig)) : nat :=
      match finMin_opt n with
      | None => 1
      | Some i =>
        match tps with
        | nil => 0 (* can't happen *)
        | tp :: tps => 2 + DoActions_Loop_steps_cons i [] tps tp
        end
      end.

    Definition DoActions_T : tRel sigSim 1 :=
      fun tin k => exists tps, (length tps =? n) = true /\ atStart tin[@Fin0] tps /\ DoActions_steps tps <= k.

    Lemma DoActions_Terminates : projT1 DoActions ↓ DoActions_T.
    Proof.
      clear pM F.
      unfold DoActions. unfold DoActions_T, DoActions_steps. destruct (finMin_opt n) as [ i | ] eqn:Ei.
      { eapply TerminatesIn_monotone.
        { TM_Correct. apply DoActions_Loop_Terminates. }
        { intros tin k. intros (tps&HL&HStart&Hk). hnf in HStart. TMSimp.
          destruct tps as [ | tp tps]; cbn in *.
          { exfalso. clear acts Hk. destruct n; cbn in *; congruence. }
          exists 1, (DoActions_Loop_steps_cons i [] tps tp). repeat split; try lia.
          intros tmid () H. hnf. left. TMSimp. exists nil, tps, tp. cbn. rewrite (finMin_opt_Some_val Ei). repeat split; auto.
          hnf. now simpl_list.
        }
      }
      { eapply TerminatesIn_monotone. TM_Correct. now intros tin k (?&?&?&H). }
    Qed.

  End DoActions.

  Section Step.

    Variable (q : state (projT1 pM)).

    Definition Step_Rel : pRel sigSim (state (projT1 pM) + F) 1 :=
      fun tin '(yout, tout) =>
        forall (T : tapes sig n),
          tin[@Fin0] ≃ T ->
          if halt q
          then tout[@Fin0] ≃ T /\ yout = inr (projT2 pM q)
          else
            let c := {| cstate := q; ctapes := T |} in
            let (q', T') := step c in
            tout[@Fin0] ≃ T' /\ yout = inl q'.

    Definition Step : pTM sigSim (state (projT1 pM) + F) 1 :=
      if halt q
      then Return Nop (inr (projT2 pM q))
      else
        Switch ReadCurre