Require Import Undecidability.TM.SBTM.

Require Import Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Shared.Libs.PSL.EqDec.

Require Import List Arith Lia Bool.

From Undecidability.Shared.Libs.DLW
  Require Import utils list_bool pos vec subcode sss.

From Undecidability.StackMachines.BSM
  Require Import bsm_defs.

Import ListNotations.
Import VectorNotations2.
Local Open Scope vector.

Set Default Proof Using "Type".

Tactic Notation "rew" "length" := autorewrite with length_db.

Local Notation "e #> x" := (vec_pos e x).
Local Notation "e [ v / x ]" := (vec_change e x v).

Local Notation "P // s -[ k ]-> t" := (sss_steps (@bsm_sss _) P k s t).
Local Notation "P // r -+> s" := (sss_progress(@bsm_sss _) P r s).
Local Notation "P // s ->> t" := (sss_compute (@bsm_sss _) P s t).

Definition enc_tape (t : tape) : Vector.t (list bool) 4 :=
    [| left t ; match curr t with Some c => [c] | None => [] end ; right t ; [] |]%vector.

Ltac solve_sc :=
  repeat match goal with
          | [ |- (?i, _) <sc (?i, _)] => eexists [], _; split; [reflexivity | cbn; try lia]
          | [ |- (?o + ?i, ?c1) <sc (?i, ?c2) ] => exists (firstn o c2); eexists; split; [ reflexivity | cbn; lia]
          | [ |- (?l, ?c1) <sc (?i, ?c2) ] =>
            let x := fresh "x" in
            let H := fresh "H" in
            evar (x : nat);
            assert (l = x + i); [ ring_simplify; subst x; reflexivity | rewrite H; subst x ]
          end.

Hint Extern 0 => solve_sc : core.

Notation CURR := (Fin1 : Fin.t 4).
Notation LEFT := (Fin0 : Fin.t 4).
Notation RIGHT := (Fin2 : Fin.t 4).
Notation ZERO := (Fin3 : Fin.t 4).
Notation CURR_ := 1.
Notation LEFT_ := 0.
Notation RIGHT_ := 2.
Notation ZERO_ := 3.

Notation JMP i := (POP ZERO i i).

Section fixi.

    Variable i : nat.

    Notation END := (23 + i).

    Definition MOVE_L :=
        [
         POP CURR (8 + i) (5 + i) ;
         POP LEFT (14 + i) (12 + i) ;
         PUSH CURR true ;
         PUSH RIGHT true;
         JMP END ;
         POP LEFT (17 + i) END ;
         PUSH CURR true ;
         JMP END ;
         POP LEFT (21 + i) (19 + i) ;
         PUSH CURR true ;
         PUSH RIGHT false ;
         JMP END ;
         PUSH RIGHT true ;
         JMP END ;
         PUSH CURR false ;
         PUSH RIGHT true ;
         JMP END ;
         PUSH CURR false ;
         JMP END ;
         PUSH RIGHT false ;
         JMP END ;
         PUSH CURR false ;
         PUSH RIGHT false
        ].

    Fact MOVE_L_length : length MOVE_L = 23.
    Proof. reflexivity. Qed.

    Fact MOVE_L_spec t : (i,MOVE_L) // (i, enc_tape t) ->> (END, enc_tape (mv Lmove t)).
    Proof.
      unfold MOVE_L.
      destruct t as [[ [ | l ls] [ [] | ] ] rs].
      - bsm sss POP 1 with CURR (8 + i) (5 + i) [].
        bsm sss POP empty with LEFT (14 + i) (12 + i).
        bsm sss PUSH with RIGHT true.
        bsm sss POP empty with ZERO END END.
        bsm sss stop.
      - bsm sss POP 0 with CURR (8 + i) (5 + i) [].
        bsm sss POP empty with LEFT (21 + i) (19 + i).
        bsm sss PUSH with RIGHT false.
        bsm sss POP empty with ZERO END END.
        bsm sss stop.
      - bsm sss POP empty with CURR (8 + i) (5 + i).
        bsm sss POP empty with LEFT (17 + i) END.
        bsm sss stop.
      - bsm sss POP 1 with CURR (8 + i) (5 + i) [].
        destruct l.
        + bsm sss POP 1 with LEFT (14 + i) (12 + i) ls.
          bsm sss PUSH with CURR true.
          bsm sss PUSH with RIGHT true.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
        + bsm sss POP 0 with LEFT (14 + i) (12 + i) ls.
          bsm sss PUSH with CURR false.
          bsm sss PUSH with RIGHT true.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
      - bsm sss POP 0 with CURR (8 + i) (5 + i) [].
        destruct l.
        + bsm sss POP 1 with LEFT (21 + i) (19 + i) ls.
          bsm sss PUSH with CURR true.
          bsm sss PUSH with RIGHT false.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
        + bsm sss POP 0 with LEFT (21 + i) (19 + i) ls.
          bsm sss PUSH with CURR false.
          bsm sss PUSH with RIGHT false.
          bsm sss stop.
      - bsm sss POP empty with CURR (8 + i) (5 + i).
        destruct l.
        + bsm sss POP 1 with LEFT (17 + i) END ls.
          bsm sss PUSH with CURR true.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
        + bsm sss POP 0 with LEFT (17 + i) END ls.
          bsm sss PUSH with CURR false.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
    Qed.

    Definition MOVE_R :=
        [
         POP CURR (8 + i) (5 + i) ;
         POP RIGHT (14 + i) (12 + i) ;
         PUSH CURR true ;
         PUSH LEFT true;
         JMP END ;
         POP RIGHT (17 + i) END ;
         PUSH CURR true ;
         JMP END ;
         POP RIGHT (21 + i) (19 + i) ;
         PUSH CURR true ;
         PUSH LEFT false ;
         JMP END ;
         PUSH LEFT true ;
         JMP END ;
         PUSH CURR false ;
         PUSH LEFT true ;
         JMP END ;
         PUSH CURR false ;
         JMP END ;
         PUSH LEFT false ;
         JMP END ;
         PUSH CURR false ;
         PUSH LEFT false
        ].

    Fact MOVE_R_length : length MOVE_R = 23.
    Proof. reflexivity. Qed.

    Fact MOVE_R_spec t : (i,MOVE_R) // (i, enc_tape t) ->> (END, enc_tape (mv Rmove t)).
    Proof.
      unfold MOVE_R.
      destruct t as [[ls c] rs]; destruct rs as [ | r rs], c as [ [] | ].
      - bsm sss POP 1 with CURR (8 + i) (5 + i) [].
        bsm sss POP empty with RIGHT (14 + i) (12 + i).
        bsm sss PUSH with LEFT true.
        bsm sss POP empty with ZERO END END.
        bsm sss stop.
      - bsm sss POP 0 with CURR (8 + i) (5 + i) [].
        bsm sss POP empty with RIGHT (21 + i) (19 + i).
        bsm sss PUSH with LEFT false.
        bsm sss POP empty with ZERO END END.
        bsm sss stop.
      - bsm sss POP empty with CURR (8 + i) (5 + i).
        bsm sss POP empty with RIGHT (17 + i) END.
        bsm sss stop.
      - bsm sss POP 1 with CURR (8 + i) (5 + i) [].
        destruct r.
        + bsm sss POP 1 with RIGHT (14 + i) (12 + i) rs.
          bsm sss PUSH with CURR true.
          bsm sss PUSH with LEFT true.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
        + bsm sss POP 0 with RIGHT (14 + i) (12 + i) rs.
          bsm sss PUSH with CURR false.
          bsm sss PUSH with LEFT true.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
      - bsm sss POP 0 with CURR (8 + i) (5 + i) [].
        destruct r.
        + bsm sss POP 1 with RIGHT (21 + i) (19 + i) rs.
          bsm sss PUSH with CURR true.
          bsm sss PUSH with LEFT false.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
        + bsm sss POP 0 with RIGHT (21 + i) (19 + i) rs.
          bsm sss PUSH with CURR false.
          bsm sss PUSH with LEFT false.
          bsm sss stop.
      - bsm sss POP empty with CURR (8 + i) (5 + i).
        destruct r.
        + bsm sss POP 1 with RIGHT (17 + i) END rs.
          bsm sss PUSH with CURR true.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
        + bsm sss POP 0 with RIGHT (17 + i) END rs.
          bsm sss PUSH with CURR false.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
    Qed.

End fixi.

Section fixM.

    Variable M : SBTM.

    Notation δ := (trans M).

    Notation "! p" := (proj1_sig (Fin.to_nat p)) (at level 1).

    Notation c := 76.

    Local Notation "'if!' x 'is' p 'then' a 'else' b" := (match x with p => a | _ => b end) (at level 0, p pattern).

    Notation END := ((2 + num_states M) * c).

    Definition PROG (i : Fin.t (S (num_states M))) :=
      let off := c * !i in
      [
          POP CURR (26 + off) (51 + off) ;
          PUSH CURR (if! δ (i, Some true) is Some (_, Some false, _) then false else true)
      ] ++
          match δ (i, Some true) with Some (_, _, Rmove) => MOVE_R (2 + off) | Some (_, _, Lmove) => MOVE_L (2 + off) | _ => repeat (JMP (25 + off)) 23 end ++
      [ JMP (match δ (i, Some true) with None => END | Some (q', _, _) => (c * ! q') end) ;
          PUSH CURR (if! δ (i, Some false) is Some (_, Some true, _) then true else false) ]
         ++
          match δ (i, Some false) with Some (_, _, Rmove) => MOVE_R (27 + off) | Some (_, _, Lmove) => MOVE_L (27 + off) | _ => repeat (JMP (50 + off)) 23 end ++
      [ JMP (match δ (i, Some false) with None => END | Some (q', _, _) => (c * ! q') end) ;
          match δ (i, None) with None => JMP END | Some (_, Some w, _) => PUSH CURR w | Some _ => JMP (52 + off) end ] ++
          match δ (i, None) with Some (_, _, Rmove) => MOVE_R (52 + off) | Some (_, _, Lmove) => MOVE_L (52 + off) | _ => repeat (JMP (75 + off)) 23 end ++
      [ JMP (match δ (i, None) with None => END | Some (q', _, _) => (c * ! q') end )
      ]
      .

    Fact PROG_length i : length (PROG i) = c.
    Proof. unfold PROG. rewrite app_length.
           destruct (δ (i, Some false)) as [ [[? []] []] | ] eqn:E1;
           destruct (δ (i, Some true)) as [ [[? []] []] | ] eqn:E2;
           destruct (δ (i, None)) as [ [[? []] []] | ] eqn:E3.
           all:reflexivity.
    Qed.

    Lemma subcode1 i : let off := c * !i in (26 + off, [PUSH CURR (if! δ (i, Some false) is Some (_, Some true, _) then true else false) ]
    ++
     match δ (i, Some false) with Some (_, _, Rmove) => MOVE_R (27 + off) | Some (_, _, Lmove) => MOVE_L (27 + off) | _ => repeat (JMP (50 + off)) 23 end ++
 [ JMP (match δ (i, Some false) with None => END | Some (q', _, _) => (c * ! q') end) ;
     match δ (i, None) with None => JMP END | Some (_, Some w, _) => PUSH CURR w | Some _ => JMP (52 + off) end ] ++
     match δ (i, None) with Some (_, _, Rmove) => MOVE_R (52 + off) | Some (_, _, Lmove) => MOVE_L (52 + off) | _ => repeat (JMP (75 + off)) 23 end ++
 [ JMP (match δ (i, None) with None => END | Some (q', _, _) => (c * ! q') end )
 ]) <sc (off, PROG i).
    Proof.
      intros ?.
      match goal with
      | [ |- (?o + ?i, ?c1) <sc (?i, ?c2) ] => exists (firstn o c2); exists []; split
      end.
      rewrite app_nil_r. 2:rewrite firstn_length, PROG_length. 2:lia.
      enough (firstn 26 (PROG i) = [ POP CURR (26 + off) (51 + off) ;
       PUSH CURR (if! δ (i, Some true) is Some (_, Some false, _) then false else true)
   ] ++
       match δ (i, Some true) with Some (_, _, Rmove) => MOVE_R (2 + off) | Some (_, _, Lmove) => MOVE_L (2 + off) | _ => repeat (JMP (25 + off)) 23 end ++
   [ JMP (match δ (i, Some true) with None => END | Some (q', _, _) => (c * ! q') end)]); subst off. rewrite H.
      unfold PROG. now rewrite <- !app_assoc.
      unfold PROG. destruct (δ (i, Some One)) as [ [ [] [] ] | ]; reflexivity.
    Qed.

    Lemma subcode2 i : let off := c * !i in (51 + off, [
     match δ (i, None) with None => JMP END | Some (_, Some w, _) => PUSH CURR w | Some _ => JMP (52 + off) end ] ++
     match δ (i, None) with Some (_, _, Rmove) => MOVE_R (52 + off) | Some (_, _, Lmove) => MOVE_L (52 + off) | _ => repeat (JMP (75 + off)) 23 end ++
 [ JMP (match δ (i, None) with None => END | Some (q', _, _) => (c * ! q') end )
 ]) <sc (off, PROG i).
    Proof.
      intros ?.
      match goal with
      | [ |- (?o + ?i, ?c1) <sc (?i, ?c2) ] => exists (firstn o c2); exists []; split
      end.
      rewrite app_nil_r. 2:rewrite firstn_length, PROG_length. 2:lia.
      enough (firstn 51 (PROG i) = [ POP CURR (26 + off) (51 + off) ;
       PUSH CURR (if! δ (i, Some true) is Some (_, Some false, _) then false else true)
   ] ++
       match δ (i, Some true) with Some (_, _, Rmove) => MOVE_R (2 + off) | Some (_, _, Lmove) => MOVE_L (2 + off) | _ => repeat (JMP (25 + off)) 23 end ++
   [ JMP (match δ (i, Some true) with None => END | Some (q', _, _) => (c * ! q') end) ;
       PUSH CURR (if! δ (i, Some false) is Some (_, Some true, _) then true else false) ]
      ++
       match δ (i, Some false) with Some (_, _, Rmove) => MOVE_R (27 + off) | Some (_, _, Lmove) => MOVE_L (27 + off) | _ => repeat (JMP (50 + off)) 23 end ++
   [ JMP (match δ (i, Some false) with None => END | Some (q', _, _) => (c * ! q') end)]); subst off. rewrite H.
      unfold PROG. now rewrite <- !app_assoc.
      unfold PROG. destruct (δ (i, Some One)) as [ [ [] [] ] | ]; destruct (δ (i, Some false)) as [ [ [] [] ] | ]; reflexivity.
    Qed.

    Lemma case_Some_false o {X} (c1 c2 : X) : (if! o is Some false then c1 else c2 = c1 /\ o = Some false)
                            \/ (if! o is Some false then c1 else c2 = c2 /\ o <> Some false).
    Proof using M.
      destruct o as [ [] | ]; firstorder congruence.
    Qed.

    Lemma case_Some_true o {X} (c1 c2 : X) : (if! o is Some true then c1 else c2 = c1 /\ o = Some true)
                            \/ (if! o is Some true then c1 else c2 = c2 /\ o <> Some true).
    Proof using M.
      destruct o as [ [] | ]; firstorder congruence.
    Qed.

    Lemma case_None (o : option bool) {X} (c2 : X) c1 : (if! o is Some w then c1 w else c2 = c2 /\ o = None)
                            \/ (exists w, (if! o is Some w then c1 w else c2) = c1 w /\ o = Some w).
    Proof.
      destruct o as [ [] | ]. right. eauto. right. eauto. eauto.
    Qed.

    Fact PROG_spec (i : Fin.t (S (num_states M))) t :
      (c * !i, PROG i) // (c * !i, enc_tape t) -+> match δ (i, curr t)
                                                   with None => (END, enc_tape t) |
                                                        Some (q', w, m) => (c * !q' , enc_tape (mv m (wr w t)))
                                                   end.
    Proof.
      set (off := c * !i).
      destruct t as [[ls [ [] | ]] rs] eqn:Eq_tape.
      - cbn [curr].
        eapply sss_progress_compute_trans. exists 1. split. lia. econstructor. 2:econstructor.
        eapply subcode_sss_step with (P := (off, [POP CURR (26 + off) (51 + off)])). auto.
        eapply in_sss_step with (l := []). cbn; lia.
        econstructor 3. reflexivity.
        unfold PROG.
        destruct (δ (i, Some true)) as [ [[q' w] m] | ] eqn:Eq_nxt.
        + edestruct (@case_Some_false w) as [ [H H0] | [H H0]].
          * rewrite H.
            bsm sss PUSH with CURR false.
            destruct m eqn:Eq_mv.
            -- eapply subcode_sss_compute_trans with (P := (2+off, MOVE_L (2 + off))). eauto.
               cbn - [plus mult].
               eapply (MOVE_L_spec (2 + off) (ls, Some Zero, rs)).
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. rewrite H0. reflexivity.
            -- eapply subcode_sss_compute_trans with (P := (2+off, MOVE_R (2 + off))). eauto.
               cbn - [plus mult].
               eapply (MOVE_R_spec (2 + off) (ls, Some Zero, rs)).
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. rewrite H0. reflexivity.
            -- bsm sss POP empty with ZERO (25 + off) (25 + off).
               bsm sss POP empty with ZERO (c * !q') (c * !q').
               bsm sss stop. subst; reflexivity.
          * rewrite H. bsm sss PUSH with CURR true.
            destruct m eqn:Eq_mv.
            -- eapply subcode_sss_compute_trans with (P := (2+off, MOVE_L (2 + off))). eauto.
               cbn - [plus mult].
               eapply (MOVE_L_spec (2 + off) (ls, Some One, rs)).
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. destruct w as [ [] | ]; try reflexivity. congruence.
            -- eapply subcode_sss_compute_trans with (P := (2+off, MOVE_R (2 + off))). eauto.
               cbn - [plus mult].
               eapply (MOVE_R_spec (2 + off) (ls, Some One, rs)).
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. destruct w as [ [] | ]; try reflexivity. congruence.
            -- bsm sss POP empty with ZERO (25 + off) (25 + off).
               bsm sss POP empty with ZERO (c * !q') (c * !q').
               bsm sss stop. destruct w as [ [] | ]; try reflexivity. congruence.
        + bsm sss PUSH with CURR true.
          bsm sss POP empty with ZERO (25 + off) (25 + off).
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
      - cbn [curr].
        eapply sss_progress_compute_trans. exists 1. split. lia. econstructor. 2:econstructor.
        eapply subcode_sss_step with (P := (off, [POP CURR (26 + off) (51 + off)])). auto.
        eapply in_sss_step with (l := []). cbn; lia.
        econstructor 2. reflexivity.
        unfold PROG.
        eapply subcode_sss_compute_trans; try eapply subcode1. 2:{ bsm sss stop. }
        destruct (δ (i, Some false)) as [ [[q' w] m] | ] eqn:Eq_nxt.
        + edestruct (@case_Some_true w) as [ [] | []].
          * rewrite H. change (76 * !i) with off.
            bsm sss PUSH with CURR true.
            destruct m eqn:Eq_mv.
            -- eapply subcode_sss_compute_trans with (P := (27+off, MOVE_L (27 + off))). eauto.
               eapply (MOVE_L_spec (27 + off) (ls, Some One, rs)).
               replace (23 + (27 + off)) with (24 + (26 + off)) by lia.
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. rewrite H0. reflexivity.
            -- eapply subcode_sss_compute_trans with (P := (27 +off, MOVE_R (27 + off))). eauto.
               eapply (MOVE_R_spec (27 + off) (ls, Some One, rs)).
               replace (23 + (27 + off)) with (24 + (26 + off)) by lia.
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. rewrite H0. reflexivity.
            -- bsm sss POP empty with ZERO (50 + off) (50 + off).
               replace (50 + off) with (24 + (26 + off)) by lia.
               bsm sss POP empty with ZERO (c * !q') (c * !q').
               bsm sss stop. subst; reflexivity.
          * rewrite H. change (76 * !i) with off.
            bsm sss PUSH with CURR false.
            destruct m eqn:Eq_mv.
            -- eapply subcode_sss_compute_trans with (P := (27+off, MOVE_L (27 + off))). replace (27 + off) with (1 + (26 + off)) at 1 by lia. eauto.
               eapply (MOVE_L_spec (27 + off) (ls, Some false, rs)).
               replace (23 + (27 + off)) with (24 + (26 + off)) by lia.
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. destruct w as [ [] | ]; try reflexivity. congruence.
            -- eapply subcode_sss_compute_trans with (P := (27 +off, MOVE_R (27 + off))).
               replace (27 + off) with (1 + (26 + off)) at 1 by lia. eauto.
               eapply (MOVE_R_spec (27 + off) (ls, Some false, rs)).
               replace (23 + (27 + off)) with (24 + (26 + off)) by lia.
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. destruct w as [ [] | ]; try reflexivity. congruence.
            -- bsm sss POP empty with ZERO (50 + off) (50 + off).
               replace (50 + off) with (24 + (26 + off)) by lia.
               bsm sss POP empty with ZERO (c * !q') (c * !q').
               bsm sss stop. destruct w as [ [] | ]; try reflexivity. congruence.
        + change (76 * !i) with off.
          bsm sss PUSH with CURR false.
          bsm sss POP empty with ZERO (50 + off) (50 + off).
          replace (50 + off) with (24 + (26 + off)) by lia.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
      - cbn [curr].
        eapply sss_progress_compute_trans. exists 1. split. lia. econstructor. 2:econstructor.
        eapply subcode_sss_step with (P := (off, [POP CURR (26 + off) (51 + off)])). auto.
        eapply in_sss_step with (l := []). cbn; lia.
        econstructor 1. reflexivity.
        unfold PROG.
        eapply subcode_sss_compute_trans; try eapply subcode2. 2:{ bsm sss stop. }
        destruct (δ (i, None)) as [ [[q' w] m] | ] eqn:Eq_nxt.
        + edestruct (@case_None w) as [ [] | []].
          * rewrite H. change (76 * !i) with off.
            bsm sss POP empty with ZERO (52 + off) (52 + off).
            destruct m eqn:Eq_mv.
            -- eapply subcode_sss_compute_trans with (P := (52+off, MOVE_L (52 + off))). eauto.
               eapply (MOVE_L_spec (52 + off) (ls, None, rs)).
               replace (23 + (52 + off)) with (24 + (51 + off)) by lia.
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. rewrite H0. reflexivity.
            -- eapply subcode_sss_compute_trans with (P := (52 +off, MOVE_R (52 + off))). eauto.
               eapply (MOVE_R_spec (52 + off) (ls, None, rs)).
               replace (23 + (52 + off)) with (24 + (51 + off)) by lia.
               bsm sss POP empty with ZERO (c * ! q') (c * ! q').
               bsm sss stop. rewrite H0. reflexivity.
            -- replace (52 + off) with (1 + (51 + off)) by lia.
               bsm sss POP empty with ZERO (75 + off) (75 + off).
               replace (75 + off) with (24 + (51 + off)) by lia.
               bsm sss POP empty with ZERO (c * !q') (c * !q').
               bsm sss stop. subst; reflexivity.
          * destruct w eqn:Eq_w.
            -- change (76 * !i) with off.
               bsm sss PUSH with CURR b.
               destruct m eqn:Eq_mv.
               ++ eapply subcode_sss_compute_trans with (P := (52+off, MOVE_L (52 + off))). replace (52 + off) with (1 + (51 + off)) at 1 by lia. eauto.
                  eapply (MOVE_L_spec (52 + off) (ls, Some b, rs)).
                  replace (23 + (52 + off)) with (24 + (51 + off)) by lia.
                  bsm sss POP empty with ZERO (c * ! q') (c * ! q').
                  bsm sss stop.
               ++ eapply subcode_sss_compute_trans with (P := (52 +off, MOVE_R (52 + off))).
                  replace (52 + off) with (1 + (51 + off)) at 1 by lia. eauto.
                  eapply (MOVE_R_spec (52 + off) (ls, Some b, rs)).
                  replace (23 + (52 + off)) with (24 + (51 + off)) by lia.
                  bsm sss POP empty with ZERO (c * ! q') (c * ! q').
                  bsm sss stop.
               ++ bsm sss POP empty with ZERO (75 + off) (75 + off).
                  replace (75 + off) with (24 + (51 + off)) by lia.
                  bsm sss POP empty with ZERO (c * !q') (c * !q').
                  bsm sss stop.
            -- change (76 * !i) with off.
               bsm sss POP empty with ZERO (52 + off) (52 + off).
               destruct m eqn:Eq_mv.
               ++ eapply subcode_sss_compute_trans with (P := (52+off, MOVE_L (52 + off))). replace (52 + off) with (1 + (51 + off)) at 1 by lia. eauto.
                  eapply (MOVE_L_spec (52 + off) (ls, None, rs)).
                  replace (23 + (52 + off)) with (24 + (51 + off)
                                                 ) by lia.
                  bsm sss POP empty with ZERO (c * ! q') (c * ! q').
                  bsm sss stop.
               ++ eapply subcode_sss_compute_trans with (P := (52 +off, MOVE_R (52 + off))).
                  replace (52 + off) with (1 + (51 + off)) at 1 by lia. eauto.
                  eapply (MOVE_R_spec (52 + off) (ls, None, rs)).
                  replace (23 + (52 + off)) with (24 + (51 + off)) by lia.
                  bsm sss POP empty with ZERO (c * ! q') (c * ! q').
                  bsm sss stop.
               ++ replace (52 + off) with (1 + (51 + off)) by lia.
                  bsm sss POP empty with ZERO (75 + off) (75 + off).
                  replace (75 + off) with (24 + (51 + off)) by lia.
                  bsm sss POP empty with ZERO (c * !q') (c * !q').
                  bsm sss stop.
        + change (76 * !i) with off.
          bsm sss POP empty with ZERO END END.
          bsm sss stop.
    Qed.

    Fixpoint sim (n : nat) (H : n <= S (num_states M)) : list (bsm_instr 4).
    Proof.
      destruct n.
      - exact [].
      - refine (sim n _ ++ _). abstract lia.
        assert (Hn : n < S (num_states M)) by abstract lia.
        refine (PROG (Fin.of_nat_lt Hn)).
    Defined.

    Definition SIM : list (bsm_instr 4). refine (@sim (S (num_states M)) _). Proof using M. abstract lia. Defined.

    Lemma sim_length (n : nat) (H : n <= S (num_states M)) :
       @length (bsm_instr 4) (@sim n H) = c * n.
    Proof.
      induction n.
      - unfold sim. cbn. lia.
      - unfold sim. fold sim. rewrite app_length. rewrite PROG_length. rewrite IHn. lia.
    Qed.

    Lemma SIM_length : length SIM = c * (S (num_states M)).
    Proof.
      unfold SIM. rewrite sim_length. lia.
    Qed.
    Arguments sim _ _ : clear implicits.

    Lemma of_nat_lt_0 n (H : 0 < S n) : Fin.of_nat_lt H = @Fin.F1 n.
    Proof.
      unfold Fin.of_nat_lt. reflexivity.
    Qed.

    Arguments Fin.of_nat_lt _ {_} _.

    Lemma PROG_sim_sc q n (H : n <= S (num_states M)) : ! q < n -> (76 * ! q, PROG q) <sc (0, sim n H).
    Proof.
      revert q.
      induction n as [n IH] using lt_wf_ind; intros q.
      destruct n.
      - intros. lia.
      - intros H0. eapply le_lt_or_eq in H0 as [H0 | H0].
        + unfold sim. fold sim. eapply subcode_app_end. eapply IH. lia. lia.
        + inversion H0. subst. clear H0. unfold sim. fold sim. revert H IH.
          eapply (Fin.caseS' q).
          * intros H IH. cbn [Fin.to_nat proj1_sig sim]. rewrite of_nat_lt_0.
            cbn - [PROG]. eexists [], []. split. rewrite app_nil_r. reflexivity. reflexivity.
          * clear q. intros q H IH.
            erewrite Fin.of_nat_ext.
            rewrite Fin.of_nat_to_nat_inv.
            eapply subcode_right. rewrite sim_length.
            pose proof (Fin.R_sanity 1 q). clear IH.
            cbn - [mult] in *. destruct (Fin.to_nat q). cbn - [mult] in *. inversion H0. reflexivity.
    Qed.

    Lemma PROG_sc q : (76 * ! q, PROG q) <sc (0, SIM).
    Proof.
      eapply PROG_sim_sc. destruct (Fin.to_nat q). cbn. lia.
    Qed.

    Theorem SIM_computes q t q' t' :
       eval M q t q' t' -> (0,SIM) // (c * !q, enc_tape t) ->> (END, enc_tape t').
    Proof.
      induction 1.
      - eapply subcode_sss_compute_trans with (P := (76 * !q, PROG q)). eapply PROG_sc.
        eapply sss_progress_compute. eapply PROG_spec.
        rewrite H.
        bsm sss stop.
      - eapply subcode_sss_compute_trans with (P := (76 * !q, PROG q)). eapply PROG_sc.
        eapply sss_progress_compute. eapply PROG_spec.
        rewrite H. eapply IHeval.
    Qed.

    Theorem SIM_term q t i out :
       i >= length SIM ->
       (0,SIM) // (c * !q, enc_tape t) ->> (i, out) -> exists q' t', i = END /\ out = enc_tape t' /\ eval M q t q' t'.
    Proof.
      intros Hout [k H]. revert q t H.
      induction k as [k IH] using lt_wf_ind; intros q t H.
      edestruct PROG_spec as [k' H'].
      eapply subcode_sss_subcode_inv in H. 4: eapply PROG_sc. 4: eapply H'. 2:{ apply bsm_sss_fun. }
      - destruct H as (k'' & -> & HH).
        destruct (δ (q, curr t)) as [ [[q' w] m] | ] eqn:Eq_nxt.
        + eapply IH in HH.
          * destruct HH as (q'' & t'' & -> & -> & HH). exists q'', t''; repeat split.
            econstructor. eassumption. eassumption.
          * destruct H'. lia.
        + eapply sss_steps_stop in HH as [= <- <-].
          exists q, t. repeat split. econstructor. eauto.
          unfold out_code. right. unfold fst, code_end, snd, fst, plus. rewrite SIM_length. lia.
      - unfold out_code. right. unfold fst, code_end, snd, fst. rewrite PROG_length.
        transitivity (length SIM). rewrite SIM_length. destruct (Fin.to_nat q). cbn. lia. lia.
    Qed.

    Theorem SIM_correct t :
      HaltSBTM (M, t) <-> BSM_HALTING (existT _ 4 (existT _ 0 (existT _ SIM (enc_tape t)))).
    Proof.
      split.
      - intros (q' & t' & H). eapply SIM_computes in H.
        unfold BSM_HALTING. eexists. split. rewrite mult_comm in H. eapply H.
        unfold out_code. right. unfold fst, code_end, snd, fst. rewrite SIM_length. lia.
      - intros ([i out] & H1 & H2). eapply (@SIM_term pos0) in H1 as (q' & t' & -> & -> & H).
        exists q', t'. eassumption. destruct H2. cbn in H. lia.
        unfold code_end, fst, snd in H. lia.
    Qed.

End fixM.

Require Import Undecidability.Synthetic.Definitions.

Theorem SBTM_to_BSM :
  HaltSBTM BSM_HALTING.
Proof.
  unshelve eexists.
  - intros [M t]. exists 4. exists 0. exists (SIM M). exact (enc_tape t).
  - intros [M t]. eapply SIM_correct.
Qed.