Coq Proof Comparison: Original vs AI-Generated (Opus 4.6)

Lemma AES_Closed_NonHalt tm S st:
  InAES st S ->
  AES_isClosed tm S ->
  ~Halts _ tm st.

Proof.
  intros.
  eapply CPS_correct.
  1: apply H.
  unfold isClosed.
  unfold AES_isClosed in H0.
  intros st0 H1.
  specialize (H0 st0 H1).
  destruct H0 as [st1 [H0a H0b]].
  exists 0.
  exists st1.
  split. 2: assumption.
  cbn.
  ector.
  - ector.
  - assumption.
Qed.

Lemma AES_Closed_NonHalt tm S st:
  InAES st S ->
  AES_isClosed tm S ->
  ~Halts _ tm st.

Proof.
  intros Hp HAD.
  enough (forall n, exists st', Steps _ tm n st st' /\ InAES st' S) as Hinf.
  { apply NonHalt_iff. intros n. destruct (Hinf n) as [st' [H _]]. eauto. }
  induction n as [|n' IH].
  - exists st. split; [constructor|exact Hp].
  - destruct IH as [st' [Hst' Hp']].
    destruct (HAD st' Hp') as [st1 [Hyz Hp1]].
    exists st1. split; [|exact Hp1].
    eapply steps_S; eauto.
Qed.

Lemma AES_isClosed'_correct tm S:
  AES_isClosed' tm S ->
  AES_isClosed tm S.

Proof.
  destruct S.
  unfold AES_isClosed',AES_isClosed,AES_CloseAt.
  intros H st0 H0.
  unfold InAES in H0.
  destruct st0 as [s t].
  destruct H0 as [[mw [H0a H0b]] [H0c H0d]].
  specialize (H mw H0a).
  destruct mw.
  destruct l0 as [|hl l1]. 1: contradiction.
  destruct r0 as [|hr r1]. 1: contradiction.
  destruct (tm s0 m0) as [[s1 d o]|] eqn:E.
  2: contradiction.
  unfold MidWord_matches in H0b.
  destruct H0b as [H1a [H1b [H1c H1d]]].
  subst.
  cbn.
  rewrite E.
  eexists.
  split.
  1: reflexivity.
  unfold InAES.

  destruct d.
  {
    destruct H as [Ha Hb].
    pose proof (H0c 2) as H2.
    cbn in H2.
    assert (H3:1<2) by lia.
    specialize (H2 H3).
    destruct H2 as [ls [H2a H2b]].
    subst.
    specialize (Hb (t (-1-(Z.of_nat len_l))%Z)).
    split.
    - exists
     {|
       l := l1 ++ t (-1 - Z.of_nat len_l)%Z :: nil;
       r := o :: pop_back hr r1;
       m := hl;
       s := s1
     |}.
      assert (H':(l1 ++ t (-1 - Z.of_nat len_l)%Z :: nil)=(tape_seg t (-2) Dneg len_l)). {
        pose proof (tape_seg_pop _ _ _ Dneg _ H1c) as H4.
        cbn in H4.
        rewrite <-H4 in H2a.
        assert (H5:(Z.neg (Pos.of_succ_nat len_l))=(-1 - Z.of_nat len_l)%Z) by lia.
        rewrite <-H5.
        apply H4.
      }
      split.
      + apply Hb.
        rewrite H'; assumption.
      + unfold MidWord_matches.
        repeat split; auto.
        * cbn.
          eapply tape_seg_hd. apply H1c.
        * rewrite H'.
          apply (tape_seg_mov_upd _ Dneg _ _).
        * apply (tape_seg_mov_upd_2 _ _ _ Dpos _ _ H1d).
    - split.
      + apply xset_matches_mov_upd_1; assumption.
      + rewrite H1d in Ha.
        eapply (xset_matches_mov_upd_2 _ _ Dpos _ _); eassumption.
  }
  {
    destruct H as [Ha Hb].
    pose proof (H0d 2) as H2.
    cbn in H2.
    assert (H3:1<2) by lia.
    specialize (H2 H3).
    destruct H2 as [ls [H2a H2b]].
    subst.
    specialize (Hb (t (1+(Z.of_nat len_r))%Z)).
    split.
    - exists
       {|
         l := o :: pop_back hl l1;
         r := r1 ++ t (1 + Z.of_nat len_r)%Z :: nil;
         m := hr;
         s := s1
       |}.
      assert (H':(r1 ++ t (1 + Z.of_nat len_r)%Z :: nil)=(tape_seg t (2) Dpos len_r)). {
        pose proof (tape_seg_pop _ _ _ Dpos _ H1d) as H4.
        cbn in H4.
        rewrite <-H4 in H2a.
        assert (H5:(Z.pos (Pos.of_succ_nat len_r))=(1 + Z.of_nat len_r)%Z) by lia.
        rewrite <-H5.
        apply H4.
      }
      split.
      + apply Hb.
        rewrite H'; assumption.
      + unfold MidWord_matches.
        repeat split; auto.
        * cbn.
          eapply tape_seg_hd. apply H1d.
        * apply (tape_seg_mov_upd_2 _ _ _ Dneg _ _ H1c).
        * rewrite H'.
          apply (tape_seg_mov_upd _ Dpos _ _).
    - split.
      + rewrite H1c in Ha.
        eapply (xset_matches_mov_upd_2 _ _ Dneg _ _); eassumption.
      + apply xset_matches_mov_upd_1; assumption.
  }
Qed.

Lemma AES_isClosed'_correct tm S:
  AES_isClosed' tm S ->
  AES_isClosed tm S.

Proof.
  destruct S as [ls rs ms].
  intro Hadtw'. unfold AES_isClosed. intros [s t] [[mw [Hmsmw Hwue]] [Hwl Hwr]].
  destruct mw as [l0 r0 m0 s0].
  unfold MidWord_matches in Hwue. destruct Hwue as [Hseq [Hmeq [Hleq Hreq]]].
  subst s0 m0 l0 r0.
  set (l0 := tape_seg t (-1)%Z Dneg len_l) in *.
  set (r0 := tape_seg t 1%Z Dpos len_r) in *.
  assert (Hib: AES_CloseAt tm {| lset := ls; rset := rs; mset := ms |}
    {| l := l0; r := r0; m := t 0%Z; s := s |}).
  { apply Hadtw'. exact Hmsmw. }
  simpl in Hib.
  destruct l0 as [|hl l1] eqn:El0; [destruct Hib|].
  destruct r0 as [|hr r1] eqn:Er0; [destruct Hib|].
  destruct (tm s (t 0%Z)) as [tr|] eqn:Etm; [|destruct Hib].
  destruct tr as [s1 d o].
  unfold step. rewrite Etm.
  eexists; split; [reflexivity|].
  destruct d.
  - destruct Hib as [Hrs0 Hib].
    unfold InAES. split; [|split].
    + destruct (Hwl 2 ltac:(lia)) as [lsn [Hlsn Hlsneq]].
      pose proof (tape_seg_pop hl l1 t Dneg len_l ltac:(symmetry; exact El0)) as HF6s_l.
      set (xn := t (Dir_to_Z Dneg * Z.of_nat (S len_l))%Z).
      assert (Hls_xn: ls (l1 ++ xn :: nil)).
      { assert (Heq: lsn = l1 ++ xn :: nil).
        { rewrite Hlsneq. symmetry.
          replace (Z.of_nat 2 * Dir_to_Z Dneg)%Z with (Dir_to_Z Dneg * 2)%Z by lia.
          exact HF6s_l. }
        rewrite <- Heq. exact Hlsn. }
      specialize (Hib xn Hls_xn).
      exists {| l := l1 ++ xn :: nil; r := o :: pop_back hr r1; m := hl; s := s1 |}.
      split; [exact Hib|].
      unfold MidWord_matches. repeat split.
      * unfold mov, upd, Dir_to_Z. simpl.
        apply (tape_seg_hd hl l1 t (-1)%Z Dneg len_l). symmetry. exact El0.
      * change ((-1)%Z) with (Dir_to_Z Dneg).
        transitivity (tape_seg t (Dir_to_Z Dneg * 2) Dneg len_l).
        { exact HF6s_l. }
        { exact (tape_seg_mov_upd t Dneg o len_l). }
      * change Dneg with (Dir_rev Dpos). change (1%Z) with (Dir_to_Z Dpos).
        exact (tape_seg_mov_upd_2 hr r1 t Dpos o len_r ltac:(symmetry; exact Er0)).
    + apply (xset_matches_mov_upd_1 t ls Dneg o len_l). exact Hwl.
    + apply (xset_matches_mov_upd_2 t rs Dpos o len_r). exact Hwr.
      assert (Er0': tape_seg t (Dir_to_Z Dpos) Dpos len_r = hr :: r1) by exact Er0.
      rewrite Er0'. exact Hrs0.
  - destruct Hib as [Hls0 Hib].
    unfold InAES. split; [|split].
    + destruct (Hwr 2 ltac:(lia)) as [rsn [Hrsn Hrsneq]].
      pose proof (tape_seg_pop hr r1 t Dpos len_r ltac:(symmetry; exact Er0)) as HF6s_r.
      set (xn := t (Dir_to_Z Dpos * Z.of_nat (S len_r))%Z).
      assert (Hrs_xn: rs (r1 ++ xn :: nil)).
      { assert (Heq: rsn = r1 ++ xn :: nil).
        { rewrite Hrsneq. symmetry.
          replace (Z.of_nat 2 * Dir_to_Z Dpos)%Z with (Dir_to_Z Dpos * 2)%Z by lia.
          exact HF6s_r. }
        rewrite <- Heq. exact Hrsn. }
      specialize (Hib xn Hrs_xn).
      exists {| l := o :: pop_back hl l1; r := r1 ++ xn :: nil; m := hr; s := s1 |}.
      split; [exact Hib|].
      unfold MidWord_matches. repeat split.
      * unfold mov, upd, Dir_to_Z. simpl.
        apply (tape_seg_hd hr r1 t 1%Z Dpos len_r). symmetry. exact Er0.
      * change Dpos with (Dir_rev Dneg). change ((-1)%Z) with (Dir_to_Z Dneg).
        exact (tape_seg_mov_upd_2 hl l1 t Dneg o len_l ltac:(symmetry; exact El0)).
      * change (1%Z) with (Dir_to_Z Dpos).
        transitivity (tape_seg t (Dir_to_Z Dpos * 2) Dpos len_r).
        { exact HF6s_r. }
        { exact (tape_seg_mov_upd t Dpos o len_r). }
    + apply (xset_matches_mov_upd_2 t ls Dneg o len_l). exact Hwl.
      assert (El0': tape_seg t (Dir_to_Z Dneg) Dneg len_l = hl :: l1) by exact El0.
      rewrite El0'. exact Hls0.
    + apply (xset_matches_mov_upd_1 t rs Dpos o len_r). exact Hwr.
Qed.

Lemma BB4_lower_bound:
  exists tm,
  HaltsAt _ tm (N.to_nat BB) (InitES Σ Σ0).

Proof.
  exists BB4_champion.
  apply halt_time_verifier_spec.
  vm_compute.
  reflexivity.
Qed.

Lemma BB4_lower_bound:
  exists tm,
  HaltsAt _ tm (N.to_nat BB) (InitES Σ Σ0).

Proof.
  exists BB4_champion. unfold BB. simpl N.to_nat.
  apply halt_time_verifier_spec. native_compute. reflexivity.
Qed.

Lemma BB4_upperbound:
  forall tm n0, HaltsAt Σ tm n0 (InitES Σ Σ0) -> n0 <= N.to_nat BB.

Proof.
  intros tm n0.
  apply allTM_HTUB.
  trivial.
Qed.

Lemma BB4_upperbound:
  forall tm n0, HaltsAt Σ tm n0 (InitES Σ Σ0) -> n0 <= N.to_nat BB.

Proof.
  intros tm n0 Hhalt. apply (allTM_HTUB tm n0). exact I. exact Hhalt.
Qed.

Lemma BB4_value:
  (forall tm n0, HaltsAt Σ tm n0 (InitES Σ Σ0) -> n0 <= N.to_nat BB) /\
  (exists tm, HaltsAt Σ tm (N.to_nat BB) (InitES Σ Σ0)).

Proof.
  split.
  - intros tm n0.
    apply allTM_HTUB.
    trivial.
  - apply BB4_lower_bound.
Qed.

Lemma BB4_value:
  (forall tm n0, HaltsAt Σ tm n0 (InitES Σ Σ0) -> n0 <= N.to_nat BB) /\
  (exists tm, HaltsAt Σ tm (N.to_nat BB) (InitES Σ Σ0)).

Proof.
  split.
  - exact BB4_upperbound.
  - exact BB4_lower_bound.
Qed.

Lemma CPS_correct tm S st:
  InT st S ->
  isClosed tm S ->
  ~Halts _ tm st.

Proof.
  intros.
  unfold Halts.
  intro H1.
  destruct H1 as [n H1].
  destruct (Closed_NonHalt _ _ _ H H0 (1+n)) as [m [H2 [st0 [H3 H4]]]].
  assert (H5:n<m) by lia.
  apply (Steps_NonHalt _ H5 H3 H1).
Qed.

Lemma CPS_correct tm S st:
  InT st S ->
  isClosed tm S ->
  ~Halts _ tm st.

Proof.
  intros Hin Hinv. rewrite <- NonHalt_iff. unfold NonHalt. intros n.
  pose proof (Closed_NonHalt tm S st Hin Hinv n) as [m [Hle [st0 [Hsteps _]]]].
  destruct (@Steps_le _ _ n m _ _ Hle Hsteps) as [stm Hstm].
  exists stm. exact Hstm.
Qed.

Lemma Closed_NonHalt tm S st:
  InT st S ->
  isClosed tm S ->
  forall n:nat,
  exists m:nat,
  n<=m /\
  exists st0,
  Steps Σ tm m st st0 /\
  InT st0 S.

Proof.
  intros H H0 n.
  induction n.
  - exists 0.
    split.
    1: lia.
    exists st.
    split.
    2: assumption.
    ctor.
  - destruct IHn as [m [H1 [st0 [H2 H3]]]].
    destruct (H0 _ H3) as [n0 [st1 [H4 H5]]].
    pose proof (Steps_trans _ H2 H4) as H6.
    exists (1+n0+m).
    split.
    1: lia.
    exists st1.
    tauto.
Qed.

Lemma Closed_NonHalt tm S st:
  InT st S ->
  isClosed tm S ->
  forall n:nat,
  exists m:nat,
  n<=m /\
  exists st0,
  Steps Σ tm m st st0 /\
  InT st0 S.

Proof.
  intros Hin Hinv n. induction n as [|n' IH].
  - exists 0. split. lia. exists st. split. constructor. exact Hin.
  - destruct IH as [m [Hle [st0 [Hsteps Hin0]]]].
    unfold isClosed in Hinv. specialize (Hinv st0 Hin0).
    destruct Hinv as [k [st1 [Hstep1 Hin1]]].
    exists ((1+k)+m). split. lia. exists st1. split.
    apply Steps_trans with st0; auto. exact Hin1.
Qed.

Lemma CountHaltTrans_0_NonHalt {tm st}:
  CountHaltTrans tm = 0 ->
  ~Halts Σ tm st.

Proof.
  intro H.
  assert (forall s i, tm s i <> None). {
    intros.
    unfold CountHaltTrans in H.
    cbn in H.
    repeat rewrite Nat.eq_add_0 in H.
    repeat rewrite isHaltTrans_0 in H.
    repeat destruct_and.
    destruct s,i; assumption.
  }
  intro H1.
  unfold Halts,HaltsAt in H1.
  destruct H1 as [n [st' [H1 H2]]].
  destruct st'. cbn in H2.
  destruct (tm s (σ 0%Z)) eqn:E; cg.
  destruct t. cg.
Qed.

Lemma CountHaltTrans_0_NonHalt {tm st}:
  CountHaltTrans tm = 0 ->
  ~Halts Σ tm st.

Proof.
  intros Hcnt. rewrite <- NonHalt_iff. unfold NonHalt. intros n.
  induction n as [|n' IH].
  - exists st. constructor.
  - destruct IH as [st' Hst']. destruct st' as [s' t'].
    assert (H: tm s' (t' Z0) <> None).
    { assert (Haux: forall s0 i0, isHaltTrans (tm s0 i0) = 0).
      { intros s0 i0. unfold CountHaltTrans, St_list, Σ_list in Hcnt. simpl in Hcnt. destruct s0, i0; lia. }
      specialize (Haux s' (t' Z0)). rewrite <- isHaltTrans_0. exact Haux. }
    destruct (tm s' (t' Z0)) as [tr|] eqn:E.
    + destruct tr as [s'' d o]. eexists. eapply steps_S; eauto. simpl. rewrite E. reflexivity.
    + exfalso. apply H. reflexivity.
Qed.

Lemma CountHaltTrans_upd {tm s i} tr:
  tm s i = None ->
  S (CountHaltTrans (TM_upd Σ Σ_eqb tm s i (Some tr))) =
  (CountHaltTrans tm).

Proof.
  unfold CountHaltTrans.
  cbn.
  unfold TM_upd.
  intro H.
  destruct s,i; cbn; rewrite H; cbn; lia.
Qed.

Lemma CountHaltTrans_upd {tm s i} tr:
  tm s i = None ->
  S (CountHaltTrans (TM_upd Σ Σ_eqb tm s i (Some tr))) =
  (CountHaltTrans tm).

Proof.
  intros Hnone.
  unfold CountHaltTrans, TM_upd, St_list, Σ_list, list_nat_sum.
  simpl.
  destruct s, i;
  simpl;
  repeat (match goal with
  | |- context [St_eqb ?x ?y] => destruct (St_eqb x y) eqn:?
  | |- context [Σ_eqb ?x ?y] => destruct (Σ_eqb x y) eqn:?
  end; simpl; try lia);
  try (rewrite Hnone; simpl; lia);
  try (pose proof (St_eqb_spec _ _ ) as HH; rewrite Heqb in HH; congruence);
  try (pose proof (Σ_eqb_spec _ _) as HH; rewrite Heqb0 in HH; congruence).
Qed.

Lemma Dir_enc_inj: is_inj Dir_enc.

Proof.
  intros x1 x2 H.
  destruct x1,x2; cbn in H; cg.
Qed.

Lemma Dir_enc_inj: is_inj Dir_enc.

Proof.
  intros a b H. destruct a, b; simpl in H; congruence.
Qed.

Lemma Dir_eqb_spec d1 d2:
  if Dir_eqb d1 d2 then d1=d2 else d1<>d2.

Proof.
  destruct d1,d2; cbn; cg.
Qed.

Lemma Dir_eqb_spec d1 d2:
  if Dir_eqb d1 d2 then d1=d2 else d1<>d2.

Proof.
destruct d1, d2; simpl; congruence.
Qed.

Lemma Dir_list_spec:
  forall s, In s Dir_list.

Proof.
  intro s.
  destruct s; cbn; tauto.
Qed.

Lemma Dir_list_spec:
  forall s, In s Dir_list.

Proof.
destruct s; simpl; auto.
Qed.

Lemma ExecState_rev_rev:
  forall st,
    ExecState_rev (ExecState_rev st) = st.

Proof.
  intros.
  destruct st as [s t].
  cbn.
  f_equal.
  apply Tape_rev_rev.
Qed.

Lemma ExecState_rev_rev:
  forall st,
    ExecState_rev (ExecState_rev st) = st.

Proof.
  intro st. destruct st as [s t]. simpl. rewrite Tape_rev_rev. reflexivity.
Qed.

Lemma ExecState_swap_swap:
  forall st,
    ExecState_swap (ExecState_swap st) = st.

Proof.
  intros.
  destruct st as [s t].
  unfold ExecState_swap.
  f_equal.
  apply St_swap_swap.
Qed.

Lemma ExecState_swap_swap:
  forall st,
    ExecState_swap (ExecState_swap st) = st.

Proof.
  intro st. destruct st as [s t]. simpl. rewrite St_swap_swap. reflexivity.
Qed.

Lemma F_HaltsFromInit:
  HaltsFromInit Σ (F Σ0') tm ->
  HaltsFromInit Σ' Σ0' tm'.

Proof.
  unfold HaltsFromInit,Halts,HaltsAt.
  rewrite F_InitES.
  intro H.
  destruct H as [n [st' [H H0]]].
  exists n.
  destruct (F_Steps _ _ _ H) as [st [H1 H2]].
  exists st.
  split; auto.
  destruct st,st'.
  cbn in H2.
  invst H2.
  apply F_step_halt,H0.
Qed.

Lemma F_HaltsFromInit:
  HaltsFromInit Σ (F Σ0') tm ->
  HaltsFromInit Σ' Σ0' tm'.

Proof.
  unfold HaltsFromInit, Halts, HaltsAt.
  intros [n [st' [Hsteps Hhalt]]].
  rewrite F_InitES in Hsteps.
  destruct (F_Steps n _ _ Hsteps) as [st1' [Hst1' Heq]].
  exists n, st1'. split; [exact Hst1'|].
  subst st'. apply F_step_halt. exact Hhalt.
Qed.

Lemma F_InitES:
  InitES Σ (F Σ0') = 
  F_ES (InitES Σ' Σ0').

Proof.
  reflexivity.
Qed.

Lemma F_InitES:
  InitES Σ (F Σ0') = 
  F_ES (InitES Σ' Σ0').

Proof.
  unfold InitES, F_ES. reflexivity.
Qed.

Lemma F_NonHaltsFromInit:
  ~HaltsFromInit Σ' Σ0' tm' ->
  ~HaltsFromInit Σ (F Σ0') tm.

Proof.
  pose proof F_HaltsFromInit.
  tauto.
Qed.

Lemma F_NonHaltsFromInit:
  ~HaltsFromInit Σ' Σ0' tm' ->
  ~HaltsFromInit Σ (F Σ0') tm.

Proof.
  intros H1 H2. apply H1. apply F_HaltsFromInit. exact H2.
Qed.

Lemma F_Steps n st0 st1:
  Steps Σ tm n (F_ES st0) st1->
  exists st1',
  Steps Σ' tm' n st0 st1' /\
  F_ES st1' = st1.

Proof.
gd st1.
induction n; intros st1 H.
- invst H.
  exists st0.
  split. 2:reflexivity.
  ctor.
- invst H.
  destruct (IHn _ H1) as [st1' [H4 H5]].
  subst.
  destruct (F_step _ _ H3) as [st2 [H5 H6]].
  exists st2.
  split. 2: assumption.
  ector; eauto.
Qed.

Lemma F_Steps n st0 st1:
  Steps Σ tm n (F_ES st0) st1->
  exists st1',
  Steps Σ' tm' n st0 st1' /\
  F_ES st1' = st1.

Proof.
  revert st0 st1. induction n; intros st0 st1 Hsteps.
  - inversion Hsteps; subst. exists st0. split; [constructor|reflexivity].
  - inversion Hsteps; subst.
    match goal with
    | [ H : Steps _ _ n _ _, H2 : step _ _ _ = Some _ |- _ ] =>
      destruct (IHn _ _ H) as [st2' [Hst2' Heq2]];
      subst;
      destruct (F_step st2' st1 H2) as [st1' [Hyz' Heq1]];
      exists st1'; split; [|exact Heq1];
      eapply steps_S; eauto
    end.
Qed.

Lemma F_step st0 st1:
  step Σ tm (F_ES st0) = Some st1->
  exists st1',
  step Σ' tm' st0 = Some st1' /\
  F_ES st1' = st1.

Proof.
  destruct st0 as [s t].
  cbn.
  intro H.
  pose proof (HF s (t 0%Z)) as H0.
  destruct (tm s (F (t 0%Z))) as [[s1 d1 o1]|] eqn:E. 2: cg.
  destruct (tm' s (t 0%Z)) as [[s1' d1' o1']|] eqn:E'. 2: cg.
  invst H0; clear H0.
  eexists.
  split.
  1: reflexivity.
  cbn.
  invst H.
  f_equal.
  unfold mov,upd.
  fext.
  destruct ((x + Dir_to_Z d1' =? 0)%Z); reflexivity.
Qed.

Lemma F_step st0 st1:
  step Σ tm (F_ES st0) = Some st1->
  exists st1',
  step Σ' tm' st0 = Some st1' /\
  F_ES st1' = st1.

Proof.
  destruct st0 as [s0 t0].
  unfold F_ES, step. simpl.
  pose proof (HF s0 (t0 0%Z)) as HF0.
  destruct (tm' s0 (t0 0%Z)) as [[s' d o']|] eqn:Etm'.
  - rewrite HF0. intro H. inversion H. subst.
    exists (s', mov Σ' (upd Σ' t0 o') d). split.
    + reflexivity.
    + unfold F_ES, mov, upd. f_equal.
      extensionality x. destruct d; simpl;
      destruct (Z.eqb _ _) eqn:Ez; reflexivity.
  - rewrite HF0. intro H. discriminate.
Qed.

Lemma F_step_halt st0:
  step Σ tm (F_ES st0) = None->
  step Σ' tm' st0 = None.

Proof.
  unfold step.
  destruct st0 as [s t]. cbn.
  specialize (HF s (t Z0)).
  destruct (tm' s (t 0%Z)); cbn; cg.
  destruct t0. rewrite HF. cg.
Qed.

Lemma F_step_halt st0:
  step Σ tm (F_ES st0) = None->
  step Σ' tm' st0 = None.

Proof.
  destruct st0 as [s0 t0].
  unfold F_ES, step. simpl.
  pose proof (HF s0 (t0 0%Z)) as HF0.
  destruct (tm' s0 (t0 0%Z)) as [[s' d o']|] eqn:Etm'.
  - rewrite HF0. intro H. discriminate.
  - rewrite HF0. intro. reflexivity.
Qed.

Lemma HaltDecider_cons_spec(f g:HaltDecider):
  HaltDecider_WF f ->
  HaltDecider_WF g ->
  HaltDecider_WF (HaltDecider_cons f g).

Proof.
  intros Hf Hg tm.
  specialize (Hf tm).
  specialize (Hg tm).
  unfold HaltDecider_cons.
  destruct (f tm); auto 1.
Qed.

Lemma HaltDecider_cons_spec(f g:HaltDecider):
  HaltDecider_WF f ->
  HaltDecider_WF g ->
  HaltDecider_WF (HaltDecider_cons f g).

Proof.
  intros Hf Hg tm. unfold HaltDecider_cons.
  specialize (Hf tm). specialize (Hg tm).
  destruct (f tm); auto.
Qed.

Lemma HaltTimeUpperBound_LE_Halt st tm n s t:
  HaltsAt tm n st ->
  Steps tm n st (s,t) ->
  n<=BB ->
  (forall tr, HaltTimeUpperBound st (LE (TM_upd tm s (t Z0) (Some tr)))) ->
  HaltTimeUpperBound st (LE tm).

Proof.
  intros.
  unfold HaltTimeUpperBound.
  intros.
  destruct (tm0 s (t Z0)) as [tr|] eqn:E.
  - specialize (H2 tr).
    eapply H2.
    2: apply H4.
    eapply LE_HaltsAtES_2; eassumption.
  - pose proof (LE_HaltsAtES_1 H3 H H0 E).
    rewrite (HaltsAt_unique H4 H5).
    assumption.
Qed.

Lemma HaltTimeUpperBound_LE_Halt st tm n s t:
  HaltsAt tm n st ->
  Steps tm n st (s,t) ->
  n<=BB ->
  (forall tr, HaltTimeUpperBound st (LE (TM_upd tm s (t Z0) (Some tr)))) ->
  HaltTimeUpperBound st (LE tm).

Proof.
  intros Hhalt Hsteps HnBB Hforall.
  intros tm' n0 Hle Hhalt'.
  destruct (Hhalt) as [st' [Hsteps' Hhalt'']].
  assert (st' = (s,t)) by (eapply Steps_unique; eassumption). subst.
  destruct (tm' s (t Z0)) eqn:Etm'.
  - apply (Hforall t0 tm' n0).
    + eapply LE_HaltsAtES_2; eauto.
    + exact Hhalt'.
  - assert (Hhalt0: HaltsAt tm' n st).
    { eapply LE_HaltsAtES_1; eauto. }
    assert (n = n0) by (eapply HaltsAt_unique; eauto).
    lia.
Qed.

Lemma HaltTimeUpperBound_LE_HaltAtES_MergeUnusedState tm n s t (P:St->Prop) BB:
  HaltsAt _ tm n (InitES Σ Σ0) ->
  Steps _ tm n (InitES Σ Σ0) (s,t) ->
  n<=BB ->
  ((exists s0, P s0 /\ UnusedState tm s0) \/
   (forall s0, ~UnusedState tm s0)) ->
  (forall s0, ~UnusedState tm s0 -> P s0) ->
  (forall tr,
    P (nxt _ tr) ->
    HaltTimeUpperBound _ BB (InitES Σ Σ0) (LE _ (TM_upd Σ Σ_eqb tm s (t Z0) (Some tr)))) ->
  HaltTimeUpperBound _ BB (InitES Σ Σ0) (LE _ tm).

Proof.
  intros.
  destruct H2 as [H2|H2].
  - eapply HaltTimeUpperBound_LE_Halt; eauto 1.
    1: apply Σ_eqb_spec.
    intro.
    destruct (UnusedState_dec tm (nxt _ tr)) as [H5|H5].
    + destruct H2 as [s0 [H2a H2b]].
      destruct tr as [s1 d1 o1].
      cbn in H5.
      eapply HaltTimeUpperBound_LE_HaltsAtES_UnusedState.
      * apply H.
      * apply H0.
      * apply H2b.
      * apply H5.
      * apply H4,H2a.
    + apply H4,H3,H5.
  - eapply HaltTimeUpperBound_LE_Halt; eauto 1.
    1: apply Σ_eqb_spec.
    intro. apply H4,H3,H2.
Qed.

Lemma HaltTimeUpperBound_LE_HaltAtES_MergeUnusedState tm n s t (P:St->Prop) BB:
  HaltsAt _ tm n (InitES Σ Σ0) ->
  Steps _ tm n (InitES Σ Σ0) (s,t) ->
  n<=BB ->
  ((exists s0, P s0 /\ UnusedState tm s0) \/
   (forall s0, ~UnusedState tm s0)) ->
  (forall s0, ~UnusedState tm s0 -> P s0) ->
  (forall tr,
    P (nxt _ tr) ->
    HaltTimeUpperBound _ BB (InitES Σ Σ0) (LE _ (TM_upd Σ Σ_eqb tm s (t Z0) (Some tr)))) ->
  HaltTimeUpperBound _ BB (InitES Σ Σ0) (LE _ tm).

Proof.
  intros Hhalt Hsteps Hle Hdisj Hndead Hext.
  apply (HaltTimeUpperBound_LE_Halt Σ BB Σ_eqb Σ_eqb_spec (InitES Σ Σ0) tm n s t); auto.
  intros tr.
  destruct (UnusedState_dec tm (nxt _ tr)) as [Hdead|Hndead2].
  - destruct Hdisj as [[s0 [Hs0P Hs0D]]|Hallnd].
    + destruct tr as [s_tr d_tr o_tr]. simpl in *.
      apply (HaltTimeUpperBound_LE_HaltsAtES_UnusedState Hhalt Hsteps s0 s_tr d_tr o_tr Hs0D Hdead).
      apply Hext. simpl. exact Hs0P.
    + exfalso. apply (Hallnd (nxt _ tr)). exact Hdead.
  - apply Hext. apply Hndead. exact Hndead2.
Qed.

Lemma HaltTimeUpperBound_LE_HaltAtES_UnusedState_ptr {tm n s t s1 BB}:
  HaltsAt _ tm n (InitES Σ Σ0) ->
  Steps _ tm n (InitES Σ Σ0) (s,t) ->
  n<=BB ->
  UnusedState_ptr tm s1 ->
  (forall tr,
    St_le s1 (nxt _ tr) ->
    HaltTimeUpperBound _ BB (InitES Σ Σ0) (LE _ (TM_upd Σ Σ_eqb tm s (t Z0) (Some tr)))) ->
  HaltTimeUpperBound _ BB (InitES Σ Σ0) (LE _ tm).

Proof.
  intros.
  destruct H2 as [H2|H2].
  - eapply HaltTimeUpperBound_LE_HaltAtES_MergeUnusedState with (P:=St_le s1); eauto 1.
    + left.
      exists s1.
      rewrite H2.
      split; unfold St_le; lia.
    + intros. rewrite H2 in H4.
      unfold St_le. unfold St_le in H4. lia.
  - destruct H2 as [H2a H2b].
    eapply HaltTimeUpperBound_LE_HaltAtES_MergeUnusedState with (P:=St_le s1); eauto 1.
    tauto.
Qed.

Lemma HaltTimeUpperBound_LE_HaltAtES_UnusedState_ptr {tm n s t s1 BB}:
  HaltsAt _ tm n (InitES Σ Σ0) ->
  Steps _ tm n (InitES Σ Σ0) (s,t) ->
  n<=BB ->
  UnusedState_ptr tm s1 ->
  (forall tr,
    St_le s1 (nxt _ tr) ->
    HaltTimeUpperBound _ BB (InitES Σ Σ0) (LE _ (TM_upd Σ Σ_eqb tm s (t Z0) (Some tr)))) ->
  HaltTimeUpperBound _ BB (InitES Σ Σ0) (LE _ tm).

Proof.
  intros Hhalt Hsteps Hle Hlsn Hext.
  apply (HaltTimeUpperBound_LE_HaltAtES_MergeUnusedState tm n s t (fun s0 => St_le s1 s0) BB); auto.
  - destruct Hlsn as [Hiff|[Hallnd Hmax]].
    + destruct (UnusedState_dec tm s1) as [Hdead|Hndead].
      * left. exists s1. split. unfold St_le. lia. exact Hdead.
      * exfalso. apply Hndead. apply (proj2 (Hiff s1)). unfold St_le. lia.
    + right. exact Hallnd.
  - intros s0 Hndead. destruct Hlsn as [Hiff|[_ Hmax]].
    + destruct (UnusedState_dec tm s0) as [Hdead|_].
      * exfalso. apply Hndead. exact Hdead.
      * unfold St_le. destruct (Hiff s0) as [_ Hback].
        assert (Hn: ~St_le s0 s1). { intro Hc. apply Hndead. apply Hback. exact Hc. }
        unfold St_le in Hn. lia.
    + apply Hmax.
Qed.

Lemma HaltTimeUpperBound_LE_HaltsAtES_UnusedState{tm n s t bb}:
  HaltsAt _ tm n (InitES Σ Σ0) ->
  Steps _ tm n (InitES Σ Σ0) (s,t) ->
  forall s1 s2 d o,
    UnusedState tm s1 ->
    UnusedState tm s2 ->
    HaltTimeUpperBound _ bb (InitES Σ Σ0) (LE Σ (TM_upd Σ Σ_eqb tm s (t Z0) (Some {| nxt:=s1; dir:=d; out:=o |}))) ->
    HaltTimeUpperBound _ bb (InitES Σ Σ0) (LE Σ (TM_upd Σ Σ_eqb tm s (t Z0) (Some {| nxt:=s2; dir:=d; out:=o |}))).

Proof.
  intros.
  St_eq_dec s1 s2; rename H4 into n0.
  1: subst; auto 1.
  pose proof (Steps_UnusedState H0) as H'0.
  assert (U1:s1<>s) by (intro X; subst; contradiction).
  assert (U2:s2<>s) by (intro X; subst; contradiction).
  destruct H1 as [H1a [H1b H1c]].
  destruct H2 as [H2a [H2b H2c]].
  assert (H':TM_swap Σ s1 s2
        (TM_upd Σ Σ_eqb tm s (t 0%Z) (Some {| nxt := s1; dir := d; out := o |})) =
        (TM_upd Σ Σ_eqb tm s (t 0%Z) (Some {| nxt := s2; dir := d; out := o |}))). {
    fext. fext.
    unfold TM_upd,TM_swap,option_Trans_swap. cbn.
    unfold St_swap. cbn.
    St_eq_dec s1 x.
    {
      subst.
      St_eq_dec s2 s; cg. cbn.
      rewrite H1b,H2b.
      St_eq_dec x s; cg. cbn. cg.
    }
    St_eq_dec s2 x.
    {
      subst.
      St_eq_dec s1 s; cg. cbn.
      rewrite H1b,H2b.
      St_eq_dec x s; cg. cbn. cg.
    }
    St_eq_dec x s.
    {
      subst. cbn.
      (Σ_eq_dec x0 (t Z0)).
      - subst. f_equal.
        cbn. f_equal. unfold St_swap.
        St_eq_dec s1 s1; cg.
      - specialize (H1a s x0).
        specialize (H2a s x0).
        destruct (tm s x0) as [[s' d1 o1]|]; cg. f_equal.
        cbn in H1a,H2a.
        erewrite <-Trans_swap_id; eauto 1.
    }
    cbn.
    specialize (H1a x x0).
    specialize (H2a x x0).
    destruct (tm x x0) as [[s' d1 o1]|]; cg. f_equal.
    cbn in H1a,H2a.
    erewrite <-Trans_swap_id; eauto 1.
  }
  rewrite <-H'.
  apply HaltTimeUpperBound_LE_swap_InitES; assumption.
Qed.

Lemma HaltTimeUpperBound_LE_HaltsAtES_UnusedState{tm n s t bb}:
  HaltsAt _ tm n (InitES Σ Σ0) ->
  Steps _ tm n (InitES Σ Σ0) (s,t) ->
  forall s1 s2 d o,
    UnusedState tm s1 ->
    UnusedState tm s2 ->
    HaltTimeUpperBound _ bb (InitES Σ Σ0) (LE Σ (TM_upd Σ Σ_eqb tm s (t Z0) (Some {| nxt:=s1; dir:=d; out:=o |}))) ->
    HaltTimeUpperBound _ bb (InitES Σ Σ0) (LE Σ (TM_upd Σ Σ_eqb tm s (t Z0) (Some {| nxt:=s2; dir:=d; out:=o |}))).

Proof.
  intros Hhalt Hsteps sa sb d o Hdead_a Hdead_b Hbb.
  pose proof (St_eqb_spec sa sb) as Eab_spec.
  destruct (St_eqb sa sb) eqn:Eab.
  - subst. exact Hbb.
  - set (tm' := TM_upd Σ Σ_eqb tm s (t Z0) (Some {| nxt := sa; dir := d; out := o |})).
    set (tm'' := TM_upd Σ Σ_eqb tm s (t Z0) (Some {| nxt := sb; dir := d; out := o |})).
    destruct Hdead_a as [Hnxt_a [Hfrom_a Hneq0_a]].
    destruct Hdead_b as [Hnxt_b [Hfrom_b Hneq0_b]].
    pose proof (Steps_UnusedState Hsteps) as Hnd_s.
    assert (Hneq_sa_s: sa <> s). {
      intro Heq. subst. apply Hnd_s. split; [|split]; assumption.
    }
    assert (Hneq_sb_s: sb <> s). {
      intro Heq. subst. apply Hnd_s. split; [|split]; assumption.
    }
    assert (Hlav_sa_s: St_eqb sa s = false). {
      pose proof (St_eqb_spec sa s). destruct (St_eqb sa s); [exfalso; apply Hneq_sa_s; assumption|reflexivity].
    }
    assert (Hlav_sb_s: St_eqb sb s = false). {
      pose proof (St_eqb_spec sb s). destruct (St_eqb sb s); [exfalso; apply Hneq_sb_s; assumption|reflexivity].
    }
    assert (HLE: LE Σ (TM_swap Σ sa sb tm') tm'').
    { intros s0 i0. unfold TM_swap, option_Trans_swap, Trans_swap, St_swap, tm', tm'', TM_upd.
      pose proof (St_eqb_spec sa s0) as Ha0. destruct (St_eqb sa s0) eqn:Eas0.
      - subst s0. rewrite Hlav_sb_s.
        destruct (andb (St_eqb sb s) (Σ_eqb i0 (t Z0))); simpl.
        + right. rewrite (Hfrom_b i0). reflexivity.
        + right. rewrite (Hfrom_b i0). reflexivity.
      - pose proof (St_eqb_spec sb s0) as Hb0. destruct (St_eqb sb s0) eqn:Ebs0.
        + subst s0. rewrite Hlav_sa_s.
          destruct (andb (St_eqb sa s) (Σ_eqb i0 (t Z0))); simpl.
          * right. rewrite (Hfrom_a i0). reflexivity.
          * right. rewrite (Hfrom_a i0). reflexivity.
        + destruct (andb (St_eqb s0 s) (Σ_eqb i0 (t Z0))) eqn:Econd.
          * simpl.
            pose proof (St_eqb_spec sa sa) as Haa. destruct (St_eqb sa sa) eqn:Eaa.
            -- left. reflexivity.
            -- exfalso. apply Haa. reflexivity.
          * destruct (tm s0 i0) as [[s' d0 o0]|] eqn:Etm.
            -- simpl. left. f_equal.
               specialize (Hnxt_a s0 i0). rewrite Etm in Hnxt_a. simpl in Hnxt_a.
               specialize (Hnxt_b s0 i0). rewrite Etm in Hnxt_b. simpl in Hnxt_b.
               pose proof (St_eqb_spec sa s') as Has'. destruct (St_eqb sa s').
               ++ exfalso. apply Hnxt_a. symmetry. exact Has'.
               ++ pose proof (St_eqb_spec sb s') as Hbs'. destruct (St_eqb sb s').
                  ** exfalso. apply Hnxt_b. symmetry. exact Hbs'.
                  ** reflexivity.
            -- simpl. left. reflexivity.
    }
    assert (Hbb2: HaltTimeUpperBound Σ bb (InitES Σ Σ0) (LE Σ (TM_swap Σ sa sb tm'))).
    { apply (@HaltTimeUpperBound_LE_swap_InitES Σ Σ0 bb sa sb Eab_spec Hneq0_a Hneq0_b). exact Hbb. }
    intros tmx n0 HLEx Hhaltx.
    apply (Hbb2 tmx n0).
    + intros s0 i0. destruct (HLE s0 i0) as [Heq|Hnone].
      * destruct (HLEx s0 i0) as [Heq2|Hnone2].
        -- left. rewrite <- Heq2. exact Heq.
        -- right. rewrite <- Hnone2. exact Heq.
      * right. exact Hnone.
    + exact Hhaltx.
Qed.

Lemma HaltTimeUpperBound_LE_NonHalt {st tm}:
  ~Halts tm st ->
  HaltTimeUpperBound st (LE tm).

Proof.
  unfold HaltTimeUpperBound.
  intros.
  pose proof (LE_NonHalts H0 H) as H2.
  assert False by (apply H2; eexists; apply H1).
  contradiction.
Qed.

Lemma HaltTimeUpperBound_LE_NonHalt {st tm}:
  ~Halts tm st ->
  HaltTimeUpperBound st (LE tm).

Proof.
  intros Hnhalt tm' n0 Hle Hhalt.
  exfalso. apply (LE_NonHalts Hle Hnhalt).
  exists n0. exact Hhalt.
Qed.

Lemma HaltTimeUpperBound_LE_rev tm st:
  HaltTimeUpperBound st (LE tm) -> HaltTimeUpperBound (ExecState_rev st) (LE (TM_rev tm)).

Proof.
  unfold HaltTimeUpperBound.
  intros.
  rewrite LE_rev,TM_rev_rev in H0.
  eapply H.
  1: apply H0.
  rewrite <-ExecState_rev_rev.
  rewrite <-HaltsAt_rev.
  apply H1.
Qed.

Lemma HaltTimeUpperBound_LE_rev tm st:
  HaltTimeUpperBound st (LE tm) -> HaltTimeUpperBound (ExecState_rev st) (LE (TM_rev tm)).

Proof.
  unfold HaltTimeUpperBound. intros Hbb tm0 n0 HLE Hhalt.
  apply (Hbb (TM_rev tm0) n0).
  - apply LE_rev. rewrite TM_rev_rev. exact HLE.
  - apply HaltsAt_rev in Hhalt. rewrite ExecState_rev_rev in Hhalt. exact Hhalt.
Qed.

Lemma HaltTimeUpperBound_LE_rev_InitES tm:
  HaltTimeUpperBound InitES (LE tm) -> HaltTimeUpperBound InitES (LE (TM_rev tm)).

Proof.
  intro.
  rewrite <-InitES_rev.
  apply HaltTimeUpperBound_LE_rev,H.
Qed.

Lemma HaltTimeUpperBound_LE_rev_InitES tm:
  HaltTimeUpperBound InitES (LE tm) -> HaltTimeUpperBound InitES (LE (TM_rev tm)).

Proof.
  rewrite <- InitES_rev at 2. apply HaltTimeUpperBound_LE_rev.
Qed.

Lemma HaltTimeUpperBound_LE_swap tm st:
  HaltTimeUpperBound st (LE tm) -> HaltTimeUpperBound (ExecState_swap st) (LE (TM_swap tm)).

Proof.
  unfold HaltTimeUpperBound.
  intros.
  rewrite LE_swap,TM_swap_swap in H0.
  eapply H.
  1: apply H0.
  rewrite <-ExecState_swap_swap.
  rewrite <-HaltsAt_swap.
  apply H1.
Qed.

Lemma HaltTimeUpperBound_LE_swap tm st:
  HaltTimeUpperBound st (LE tm) -> HaltTimeUpperBound (ExecState_swap st) (LE (TM_swap tm)).

Proof.
  unfold HaltTimeUpperBound. intros Hbb tm0 n0 HLE Hhalt.
  apply (Hbb (TM_swap tm0) n0).
  - apply LE_swap. rewrite TM_swap_swap. exact HLE.
  - apply HaltsAt_swap in Hhalt. rewrite ExecState_swap_swap in Hhalt. exact Hhalt.
Qed.

Lemma HaltTimeUpperBound_LE_swap_InitES tm:
  HaltTimeUpperBound InitES (LE tm) -> HaltTimeUpperBound InitES (LE (TM_swap tm)).

Proof.
  intro.
  rewrite <-InitES_swap.
  apply HaltTimeUpperBound_LE_swap,H.
Qed.

Lemma HaltTimeUpperBound_LE_swap_InitES tm:
  HaltTimeUpperBound InitES (LE tm) -> HaltTimeUpperBound InitES (LE (TM_swap tm)).

Proof.
  rewrite <- InitES_swap at 2. apply HaltTimeUpperBound_LE_swap.
Qed.

Lemma HaltsAtES_Trans {tm n st s t}:
  HaltsAt Σ tm n st ->
  Steps Σ tm n st (s, t) ->
  tm s (t Z0) = None.

Proof.
  intros.
  destruct H as [[s0 t0] [Ha Hb]].
  pose proof (Steps_unique _ Ha H0) as H.
  invst H.
  unfold step in Hb.
  destruct (tm s (t Z0)); cg.
  destruct t0; cg.
Qed.

Lemma HaltsAtES_Trans {tm n st s t}:
  HaltsAt Σ tm n st ->
  Steps Σ tm n st (s, t) ->
  tm s (t Z0) = None.

Proof.
  intros [st' [Hsteps Hhalt]] Hsteps2.
  pose proof (@Steps_unique _ _ _ _ _ _ Hsteps2 Hsteps) as Heq. subst st'.
  simpl in Hhalt.
  destruct (tm s (t Z0)) eqn:E.
  - destruct t0 as [s' d o]. discriminate.
  - reflexivity.
Qed.

Lemma HaltsAt_rev tm n st:
  HaltsAt tm n st <->
  HaltsAt (TM_rev tm) n (ExecState_rev st).

Proof.
  split.
  - apply HaltsAt_rev_0.
  - pose proof (HaltsAt_rev_0 (TM_rev tm) n (ExecState_rev st)) as H.
    rewrite TM_rev_rev,ExecState_rev_rev in H.
    apply H.
Qed.

Lemma HaltsAt_rev tm n st:
  HaltsAt tm n st <->
  HaltsAt (TM_rev tm) n (ExecState_rev st).

Proof.
  split.
  - apply HaltsAt_rev_0.
  - intro H. rewrite <- (ExecState_rev_rev st). rewrite <- (TM_rev_rev tm).
    apply HaltsAt_rev_0. exact H.
Qed.

Lemma HaltsAt_rev_0 tm n st:
  HaltsAt tm n st ->
  HaltsAt (TM_rev tm) n (ExecState_rev st).

Proof.
  unfold HaltsAt.
  intros.
  destruct H as [st' [H H0]].
  eexists.
  split.
  - rewrite Steps_rev.
    rewrite <-ExecState_rev_rev in H.
    rewrite ExecState_rev_rev.
    apply H.
  - rewrite step_halt_rev,ExecState_rev_rev.
    apply H0.
Qed.

Lemma HaltsAt_rev_0 tm n st:
  HaltsAt tm n st ->
  HaltsAt (TM_rev tm) n (ExecState_rev st).

Proof.
  intro H. destruct H as [st' [Hsteps Hhalt]].
  exists (ExecState_rev st'). split.
  - apply Steps_rev. rewrite ExecState_rev_rev. rewrite ExecState_rev_rev. exact Hsteps.
  - apply step_halt_rev. rewrite ExecState_rev_rev. exact Hhalt.
Qed.

Lemma HaltsAt_swap tm n st:
  HaltsAt tm n st <->
  HaltsAt (TM_swap tm) n (ExecState_swap st).

Proof.
  split.
  - apply HaltsAt_swap_0.
  - pose proof (HaltsAt_swap_0 (TM_swap tm) n (ExecState_swap st)) as H.
    rewrite TM_swap_swap,ExecState_swap_swap in H.
    apply H.
Qed.

Lemma HaltsAt_swap tm n st:
  HaltsAt tm n st <->
  HaltsAt (TM_swap tm) n (ExecState_swap st).

Proof.
  split.
  - apply HaltsAt_swap_0.
  - intro H. rewrite <- (ExecState_swap_swap st). rewrite <- (TM_swap_swap tm).
    apply HaltsAt_swap_0. exact H.
Qed.

Lemma HaltsAt_swap_0 tm n st:
  HaltsAt tm n st ->
  HaltsAt (TM_swap tm) n (ExecState_swap st).

Proof.
  unfold HaltsAt.
  intros.
  destruct H as [st' [H H0]].
  eexists.
  split.
  - rewrite Steps_swap.
    rewrite <-ExecState_swap_swap in H.
    rewrite ExecState_swap_swap.
    apply H.
  - rewrite step_halt_swap,ExecState_swap_swap.
    apply H0.
Qed.

Lemma HaltsAt_swap_0 tm n st:
  HaltsAt tm n st ->
  HaltsAt (TM_swap tm) n (ExecState_swap st).

Proof.
  intro H. destruct H as [st' [Hsteps Hhalt]].
  exists (ExecState_swap st'). split.
  - apply Steps_swap. rewrite ExecState_swap_swap. rewrite ExecState_swap_swap. exact Hsteps.
  - apply step_halt_swap. rewrite ExecState_swap_swap. exact Hhalt.
Qed.

Lemma HaltsAt_unique {tm n1 n2 st}:
  HaltsAt tm n1 st ->
  HaltsAt tm n2 st ->
  n1=n2.

Proof.
  intros.
  pose proof H as H''.
  pose proof H0 as H0''.
  unfold HaltsAt in H,H0.
  pose proof H as H'.
  pose proof H0 as H0'.
  destruct H as [st0 [Ha Hb]].
  destruct H0 as [st1 [H0a H0b]].
  assert (n1=n2\/n1<n2\/n2<n1) by lia.
  destruct H as [H|[H|H]]; cg.
  - destruct (Steps_NonHalt H H0a H'').
  - destruct (Steps_NonHalt H Ha H0'').
Qed.

Lemma HaltsAt_unique {tm n1 n2 st}:
  HaltsAt tm n1 st ->
  HaltsAt tm n2 st ->
  n1=n2.

Proof.
  intros [st1 [H1 Hhalt1]] [st2 [H2 Hhalt2]].
  destruct (Nat.lt_trichotomy n1 n2) as [Hlt|[Heq|Hgt]].
  - exfalso. eapply (Steps_NonHalt Hlt H2). exists st1. auto.
  - exact Heq.
  - exfalso. eapply (Steps_NonHalt Hgt H1). exists st2. auto.
Qed.

Lemma In_RepWL_ES_InitES:
  In_RepWL_ES (InitES Σ Σ0) RepWL_InitES.

Proof.
  unfold RepWL_InitES.
  replace (InitES Σ Σ0) with (St0,make_tape'' half_tape_all0 nil half_tape_all0 Dpos).
  1: repeat ctor.
  unfold InitES.
  f_equal.
  fext.
  destruct x; cbn.
  2,3: rewrite app_halftape_nil; unfold half_tape_cdr,half_tape_all0.
  all: reflexivity.
Qed.

Lemma In_RepWL_ES_InitES:
  In_RepWL_ES (InitES Σ Σ0) RepWL_InitES.

Proof.
  replace (InitES Σ Σ0) with (St0, make_tape'' half_tape_all0 nil half_tape_all0 Dpos).
  2:{ unfold InitES, make_tape'', make_tape', make_tape, app_halftape, half_tape_all0, half_tape_cdr.
      f_equal. extensionality z. destruct z; simpl; try reflexivity.
      all: destruct (Nat.pred (Pos.to_nat p)); reflexivity. }
  apply (In_RepWL_ES_intro half_tape_all0 half_tape_all0 nil nil St0 Dpos); apply RepWL_match_O.
Qed.

Lemma InitES_InAES_cond (S:AbstractES):
  let (ls,rs,ms):=S in
  ls (repeat Σ0 len_l) ->
  rs (repeat Σ0 len_r) ->
  ms {| l:=repeat Σ0 len_l; r:=repeat Σ0 len_r; m:=Σ0; s:=St0 |} ->
  InAES (InitES Σ Σ0) S.

Proof.
  destruct S as [ls rs ms].
  intros.
  cbn.
  repeat split.
  - eexists.
    split.
    1: apply H1.
    cbn.
    repeat split; cg; apply tape_seg__repeat_Σ0.
  - unfold xset_matches. intros.
    eexists.
    split.
    1: apply H.
    apply tape_seg__repeat_Σ0.
  - unfold xset_matches. intros.
    eexists.
    split.
    1: apply H0.
    apply tape_seg__repeat_Σ0.
Qed.

Lemma InitES_InAES_cond (S:AbstractES):
  let (ls,rs,ms):=S in
  ls (repeat Σ0 len_l) ->
  rs (repeat Σ0 len_r) ->
  ms {| l:=repeat Σ0 len_l; r:=repeat Σ0 len_r; m:=Σ0; s:=St0 |} ->
  InAES (InitES Σ Σ0) S.

Proof.
  destruct S as [ls rs ms].
  intros Hls Hrs Hms.
  unfold InAES, InitES.
  split; [|split].
  - exists {| l:=repeat Σ0 len_l; r:=repeat Σ0 len_r; m:=Σ0; s:=St0 |}.
    split; [exact Hms|].
    unfold MidWord_matches. simpl. repeat split.
    + rewrite (tape_seg__repeat_Σ0 (-1)%Z Dneg). reflexivity.
    + rewrite (tape_seg__repeat_Σ0 1%Z Dpos). reflexivity.
  - unfold xset_matches. intros n Hn.
    exists (repeat Σ0 len_l). split; [exact Hls|].
    rewrite (tape_seg__repeat_Σ0 (Z.of_nat n * (-1))%Z Dneg). reflexivity.
  - unfold xset_matches. intros n Hn.
    exists (repeat Σ0 len_r). split; [exact Hrs|].
    rewrite (tape_seg__repeat_Σ0 (Z.of_nat n * 1)%Z Dpos). reflexivity.
Qed.

Lemma InitES_rev:
  ExecState_rev InitES = InitES.

Proof.
  reflexivity.
Qed.

Lemma InitES_rev:
  ExecState_rev InitES = InitES.

Proof.
  unfold ExecState_rev, InitES, Tape_rev. reflexivity.
Qed.

Lemma InitES_swap:
  ExecState_swap InitES = InitES.

Proof.
  unfold InitES. cbn.
  f_equal.
  unfold St_swap.
  St_eq_dec s1 St0; try cg.
  St_eq_dec s2 St0; try cg.
Qed.

Lemma InitES_swap:
  ExecState_swap InitES = InitES.

Proof.
  unfold ExecState_swap, InitES, St_swap.
  pose proof (St_eqb_spec s1 St0) as H1.
  destruct (St_eqb s1 St0).
  - exfalso. apply Hneq01. assumption.
  - pose proof (St_eqb_spec s2 St0) as H2.
    destruct (St_eqb s2 St0).
    + exfalso. apply Hneq02. assumption.
    + reflexivity.
Qed.

Lemma LE_HaltsAtES_1 {tm tm0 n st s t}:
  LE tm tm0 ->
  HaltsAt tm n st ->
  Steps tm n st (s,t) ->
  tm0 s (t 0%Z) = None ->
  HaltsAt tm0 n st.

Proof.
  intros.
  unfold HaltsAt.
  epose proof (LE_Steps H H1).
  exists (s,t).
  split. 1: assumption.
  cbn. rewrite H2. reflexivity.
Qed.

Lemma LE_HaltsAtES_1 {tm tm0 n st s t}:
  LE tm tm0 ->
  HaltsAt tm n st ->
  Steps tm n st (s,t) ->
  tm0 s (t 0%Z) = None ->
  HaltsAt tm0 n st.

Proof.
  intros Hle [st' [Hsteps Hhalt]] Hsteps' Htm0.
  assert (st' = (s,t)) by (eapply Steps_unique; eassumption). subst.
  exists (s,t). split.
  - eapply LE_Steps; eauto.
  - simpl. rewrite Htm0. reflexivity.
Qed.

Lemma LE_HaltsAtES_2 {tm tm0 n st s t tr}:
  LE tm tm0 ->
  HaltsAt tm n st ->
  Steps tm n st (s,t) ->
  tm0 s (t 0%Z) = Some tr ->
  LE (TM_upd tm s (t 0%Z) (Some tr)) tm0.

Proof.
  unfold LE.
  intros.
  unfold TM_upd.
  St_eq_dec s0 s.
  - Σ_eq_dec i (t Z0); cbn.
    + left; cg.
    + apply H.
  - apply H.
Qed.

Lemma LE_HaltsAtES_2 {tm tm0 n st s t tr}:
  LE tm tm0 ->
  HaltsAt tm n st ->
  Steps tm n st (s,t) ->
  tm0 s (t 0%Z) = Some tr ->
  LE (TM_upd tm s (t 0%Z) (Some tr)) tm0.

Proof.
  intros Hle Hhalt Hsteps Htm0.
  intros s0 i0.
  unfold TM_upd.
  pose proof (St_eqb_spec s0 s) as Hs.
  destruct (St_eqb s0 s) eqn:Es.
  - subst. simpl.
    pose proof (Σ_eqb_spec i0 (t 0%Z)) as Hi.
    destruct (Σ_eqb i0 (t 0%Z)).
    + subst. left. symmetry. exact Htm0.
    + destruct (Hle s i0) as [Heq|Hnone]; auto.
  - simpl. destruct (Hle s0 i0) as [Heq|Hnone]; auto.
Qed.

Lemma LE_NonHalts {tm tm' st}:
  LE tm tm' ->
  ~Halts tm st ->
  ~Halts tm' st.

Proof.
  repeat rewrite <-NonHalt_iff.
  unfold NonHalt.
  intros.
  destruct (H0 n) as [st' H1].
  exists st'.
  eapply LE_Steps; eassumption.
Qed.

Lemma LE_NonHalts {tm tm' st}:
  LE tm tm' ->
  ~Halts tm st ->
  ~Halts tm' st.

Proof.
  intros Hle Hnhalt.
  apply NonHalt_iff. apply NonHalt_iff in Hnhalt.
  intros n. destruct (Hnhalt n) as [stn Hstn].
  exists stn. eapply LE_Steps; eauto.
Qed.

Lemma LE_Steps {tm tm' n st st0}:
  LE tm tm' ->
  Steps tm n st st0 ->
  Steps tm' n st st0.

Proof.
  intros.
  induction H0.
  - ctor.
  - ector.
    1: apply IHSteps,H.
    eapply LE_step; eassumption.
Qed.

Lemma LE_Steps {tm tm' n st st0}:
  LE tm tm' ->
  Steps tm n st st0 ->
  Steps tm' n st st0.

Proof.
  intros Hle Hsteps. induction Hsteps.
  - constructor.
  - eapply steps_S; [exact (IHHsteps Hle) | eapply LE_step; eauto].
Qed.

Lemma LE_rev tm tm':
  LE tm tm' <-> LE (TM_rev tm) (TM_rev tm').

Proof.
  split.
  - apply LE_rev_0.
  - pose proof (LE_rev_0 (TM_rev tm) (TM_rev tm')) as H.
    repeat rewrite TM_rev_rev in H.
    apply H.
Qed.

Lemma LE_rev tm tm':
  LE tm tm' <-> LE (TM_rev tm) (TM_rev tm').

Proof.
  split.
  - apply LE_rev_0.
  - intro H. rewrite <- (TM_rev_rev tm). rewrite <- (TM_rev_rev tm'). apply LE_rev_0. exact H.
Qed.

Lemma LE_rev_0 tm tm':
  LE tm tm' -> LE (TM_rev tm) (TM_rev tm').

Proof.
  unfold LE.
  intros.
  unfold TM_rev.
  pose proof (H s i) as H0.
  destruct H0 as [H0|H0]; rewrite H0; tauto.
Qed.

Lemma LE_rev_0 tm tm':
  LE tm tm' -> LE (TM_rev tm) (TM_rev tm').

Proof.
  intro HLE. unfold LE, TM_rev in *. intros s i.
  destruct (HLE s i) as [Heq|Hnone].
  - left. rewrite Heq. reflexivity.
  - right. rewrite Hnone. reflexivity.
Qed.

Lemma LE_step tm tm' st st0:
  LE tm tm' ->
  step tm st = Some st0 ->
  step tm' st = Some st0.

Proof.
  unfold LE,step.
  destruct st as [s t].
  intros.
  specialize (H s (t Z0)).
  destruct (tm s (t Z0)) as [[s' d o]|]; cg.
  destruct H; cg.
  rewrite <-H. cg.
Qed.

Lemma LE_step tm tm' st st0:
  LE tm tm' ->
  step tm st = Some st0 ->
  step tm' st = Some st0.

Proof.
  intros Hle Hstep.
  destruct st as [s t]. simpl in *.
  destruct (Hle s (t 0%Z)) as [Heq | Hnone].
  - rewrite <- Heq. exact Hstep.
  - rewrite Hnone in Hstep. discriminate.
Qed.

Lemma LE_swap tm tm':
  LE tm tm' <-> LE (TM_swap tm) (TM_swap tm').

Proof.
  split.
  - apply LE_swap_0.
  - pose proof (LE_swap_0 (TM_swap tm) (TM_swap tm')) as H.
    repeat rewrite TM_swap_swap in H.
    apply H.
Qed.

Lemma LE_swap tm tm':
  LE tm tm' <-> LE (TM_swap tm) (TM_swap tm').

Proof.
  split.
  - apply LE_swap_0.
  - intro H. rewrite <- (TM_swap_swap tm). rewrite <- (TM_swap_swap tm'). apply LE_swap_0. exact H.
Qed.

Lemma LE_swap_0 tm tm':
  LE tm tm' -> LE (TM_swap tm) (TM_swap tm').

Proof.
  unfold LE.
  intros.
  unfold TM_swap.
  specialize (H (St_swap s) i).
  destruct H as [H|H]; rewrite H; tauto.
Qed.

Lemma LE_swap_0 tm tm':
  LE tm tm' -> LE (TM_swap tm) (TM_swap tm').

Proof.
  intro HLE. unfold LE, TM_swap in *. intros s i.
  destruct (HLE (St_swap s) i) as [Heq|Hnone].
  - left. rewrite Heq. reflexivity.
  - right. rewrite Hnone. reflexivity.
Qed.

Lemma ListES_Steps_spec tm n es:
  match ListES_Steps tm n es with
  | Some es0 => Steps _ tm n (ListES_toES es) (ListES_toES es0)
  | None => True
  end.

Proof.
  gd es.
  induction n.
  1: intro; cbn; ctor.
  intro.
  cbn.
  destruct (tm (s es) (m es)) as [tr|] eqn:E.
  2: trivial.
  destruct es as [l0 r0 m0 s0].
  cbn in E.
  epose proof (ListES_step'_spec tm l0 r0 m0 s0) as H.
  rewrite E in H.
  specialize (IHn (ListES_step' tr {| l := l0; r := r0; m := m0; s := s0 |})).
  destruct (ListES_Steps tm n (ListES_step' tr {| l := l0; r := r0; m := m0; s := s0 |})).
  2: trivial.
  replace (S n) with (n+1) by lia.
  eapply Steps_trans.
  2: apply IHn.
  ector; eauto 1.
  ctor.
Qed.

Lemma ListES_Steps_spec tm n es:
  match ListES_Steps tm n es with
  | Some es0 => Steps _ tm n (ListES_toES es) (ListES_toES es0)
  | None => True
  end.

Proof.
  revert es. induction n as [|n' IH]; intros es.
  - simpl. constructor.
  - destruct es as [l0 r0 m0 s0].
    change (match (match tm s0 m0 with | Some tr => ListES_Steps tm n' (ListES_step' tr (Build_ListES l0 r0 m0 s0)) | None => None end)
      with | Some es0 => Steps _ tm (S n') (ListES_toES (Build_ListES l0 r0 m0 s0)) (ListES_toES es0) | None => True end).
    destruct (tm s0 m0) as [tr|] eqn:Etm; [|exact I].
    specialize (IH (ListES_step' tr (Build_ListES l0 r0 m0 s0))).
    destruct (ListES_Steps tm n' (ListES_step' tr (Build_ListES l0 r0 m0 s0))) as [es0|]; [|exact I].
    pose proof (ListES_step'_spec tm l0 r0 m0 s0) as Hspec.
    rewrite Etm in Hspec.
    assert (Hstep1: Steps Σ tm 1
      (ListES_toES (Build_ListES l0 r0 m0 s0))
      (ListES_toES (ListES_step' tr (Build_ListES l0 r0 m0 s0)))).
    { econstructor. econstructor. exact Hspec. }
    replace (S n') with (n' + 1) by lia.
    eapply Steps_trans; eauto.
Qed.

Lemma ListES_step'_spec tm l0 r0 m0 s0:
  step Σ tm (ListES_toES (Build_ListES l0 r0 m0 s0)) =
  match tm s0 m0 with
  | Some tr => Some (ListES_toES (ListES_step' tr (Build_ListES l0 r0 m0 s0)))
  | None => None
  end.

Proof.
  erewrite (ListES_step_spec).
  cbn.
  destruct (tm s0 m0) as [[s1 d o]|]; reflexivity.
Qed.

Lemma ListES_step'_spec tm l0 r0 m0 s0:
  step Σ tm (ListES_toES (Build_ListES l0 r0 m0 s0)) =
  match tm s0 m0 with
  | Some tr => Some (ListES_toES (ListES_step' tr (Build_ListES l0 r0 m0 s0)))
  | None => None
  end.

Proof.
  unfold step, ListES_toES, ListES_step'.
  destruct (tm s0 m0) as [[s1 d o]|]; [|reflexivity].
  destruct d; [destruct l0 as [|m1 l1]|destruct r0 as [|m1 r1]];
  f_equal; f_equal; extensionality z; unfold mov, upd, Dir_to_Z;
  destruct z as [|p|p]; try reflexivity.
  1: {
    destruct p as [p|p|]; [
      replace (Z.pos p~1 + Z.neg 1)%Z with (Z.pos p~0)%Z by lia;
      change ((Z.pos p~0 =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?Pos2Nat.inj_xO, ?Pos2Nat.inj_xI;
        pose proof (Pos2Nat.is_pos p); lia
    |
      replace (Z.pos p~0 + Z.neg 1)%Z with (Z.pos (Pos.pred_double p))%Z
        by (rewrite Pos.pred_double_spec; lia);
      change ((Z.pos (Pos.pred_double p) =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?pos_to_nat_pred_double, ?Pos2Nat.inj_xO;
        pose proof (Pos2Nat.is_pos p); lia
    |
      simpl; reflexivity ].
  }
  1: {
    replace (Z.neg p + Z.neg 1)%Z with (Z.neg (p + 1))%Z by lia.
    change ((Z.neg (p+1) =? 0)%Z) with false.
    rewrite Pos2Nat.inj_add. change (Pos.to_nat 1) with 1. rewrite Nat.add_1_r.
    change (nth (S (Pos.to_nat p)) (m0 :: @nil Σ) Σ0)
      with (nth (Pos.to_nat p) (@nil Σ) Σ0).
    rewrite nth_Sigma0_nil. reflexivity.
  }
  1: {
    destruct p as [p|p|]; [
      replace (Z.pos p~1 + Z.neg 1)%Z with (Z.pos p~0)%Z by lia;
      change ((Z.pos p~0 =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?Pos2Nat.inj_xO, ?Pos2Nat.inj_xI;
        pose proof (Pos2Nat.is_pos p); lia
    |
      replace (Z.pos p~0 + Z.neg 1)%Z with (Z.pos (Pos.pred_double p))%Z
        by (rewrite Pos.pred_double_spec; lia);
      change ((Z.pos (Pos.pred_double p) =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?pos_to_nat_pred_double, ?Pos2Nat.inj_xO;
        pose proof (Pos2Nat.is_pos p); lia
    |
      simpl; reflexivity ].
  }
  1: {
    replace (Z.neg p + Z.neg 1)%Z with (Z.neg (p + 1))%Z by lia.
    change ((Z.neg (p+1) =? 0)%Z) with false.
    rewrite Pos2Nat.inj_add. change (Pos.to_nat 1) with 1. rewrite Nat.add_1_r.
    simpl. reflexivity.
  }
  1: {
    replace (Z.pos p + Z.pos 1)%Z with (Z.pos (p + 1))%Z by lia.
    change ((Z.pos (p+1) =? 0)%Z) with false.
    rewrite Pos2Nat.inj_add. change (Pos.to_nat 1) with 1. rewrite Nat.add_1_r.
    change (nth (S (Pos.to_nat p)) (m0 :: @nil Σ) Σ0)
      with (nth (Pos.to_nat p) (@nil Σ) Σ0).
    rewrite nth_Sigma0_nil. reflexivity.
  }
  1: {
    destruct p as [p|p|]; [
      replace (Z.neg p~1 + Z.pos 1)%Z with (Z.neg p~0)%Z by lia;
      change ((Z.neg p~0 =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?Pos2Nat.inj_xO, ?Pos2Nat.inj_xI;
        pose proof (Pos2Nat.is_pos p); lia
    |
      replace (Z.neg p~0 + Z.pos 1)%Z with (Z.neg (Pos.pred_double p))%Z
        by (rewrite Pos.pred_double_spec; lia);
      change ((Z.neg (Pos.pred_double p) =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?pos_to_nat_pred_double, ?Pos2Nat.inj_xO;
        pose proof (Pos2Nat.is_pos p); lia
    |
      simpl; reflexivity ].
  }
  1: {
    replace (Z.pos p + Z.pos 1)%Z with (Z.pos (p + 1))%Z by lia.
    change ((Z.pos (p+1) =? 0)%Z) with false.
    rewrite Pos2Nat.inj_add. change (Pos.to_nat 1) with 1. rewrite Nat.add_1_r.
    simpl. reflexivity.
  }
  1: {
    destruct p as [p|p|]; [
      replace (Z.neg p~1 + Z.pos 1)%Z with (Z.neg p~0)%Z by lia;
      change ((Z.neg p~0 =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?Pos2Nat.inj_xO, ?Pos2Nat.inj_xI;
        pose proof (Pos2Nat.is_pos p); lia
    |
      replace (Z.neg p~0 + Z.pos 1)%Z with (Z.neg (Pos.pred_double p))%Z
        by (rewrite Pos.pred_double_spec; lia);
      change ((Z.neg (Pos.pred_double p) =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?pos_to_nat_pred_double, ?Pos2Nat.inj_xO;
        pose proof (Pos2Nat.is_pos p); lia
    |
      simpl; reflexivity ].
  }
Qed.

Lemma ListES_step_spec tm x:
  step Σ tm (ListES_toES x) =
  match ListES_step tm x with
  | None => None
  | Some x1 => Some (ListES_toES x1)
  end.

Proof.
  destruct x as [l0 r0 m0 s0].
  cbn.
  destruct (tm s0 m0) as [[s' d o]|].
  2: reflexivity.
  unfold mov,upd.
  destruct d; cbn.
  + destruct l0; cbn.
    * f_equal. f_equal. fext.
      assert (H:(x<0\/x=0\/x=1\/x>1)%Z) by lia.
      destruct H as [H|[H|[H|H]]].
      -- destruct x; try lia.
         destruct ((Z.neg p + -1)%Z) eqn:E; cbn; try lia.
         destruct (Pos.to_nat p0) eqn:E0. 1: lia.
         destruct n,(Pos.to_nat p); auto 1.
         ++ destruct n; reflexivity.
         ++ destruct n0; reflexivity.
      -- subst. reflexivity.
      -- subst. reflexivity.
      -- destruct x; try lia.
         destruct ((Z.pos p + -1)%Z) eqn:E; cbn; try lia.
         destruct (Pos.to_nat p0) eqn:E0. 1: lia.
         assert (Pos.to_nat p = S (S n)) by lia. rewrite H0. reflexivity.
    * f_equal. f_equal. fext.
      assert (H:(x<0\/x=0\/x=1\/x>1)%Z) by lia.
      destruct H as [H|[H|[H|H]]].
      -- destruct x; try lia.
         destruct ((Z.neg p + -1)%Z) eqn:E; cbn; try lia.
         destruct (Pos.to_nat p0) eqn:E0. 1: lia.
         assert (n=Pos.to_nat p) by lia. rewrite H0. reflexivity.
      -- subst. reflexivity.
      -- subst. reflexivity.
      -- destruct x; try lia.
         destruct ((Z.pos p + -1)%Z) eqn:E; cbn; try lia.
         destruct (Pos.to_nat p0) eqn:E0. 1: lia.
         assert (Pos.to_nat p = S (S n)) by lia. rewrite H0. reflexivity.
  + destruct r0; cbn.
    * f_equal. f_equal. fext.
      assert (H:(x>0\/x=0\/x=-1\/x<(-1))%Z) by lia.
      destruct H as [H|[H|[H|H]]].
      -- destruct x; try lia.
         destruct ((Z.neg p + -1)%Z) eqn:E; cbn; try lia.
         destruct (Pos.to_nat p0) eqn:E0. 1: lia.
         destruct (Pos.to_nat (p + 1)) eqn:E1; try lia.
         destruct n0,(Pos.to_nat p); auto 1.
         ++ destruct n0; reflexivity.
         ++ destruct n1; reflexivity.
      -- subst. reflexivity.
      -- subst. reflexivity.
      -- destruct x; try lia.
         destruct ((Z.neg p + 1)%Z) eqn:E; cbn; try lia.
         destruct (Pos.to_nat p0) eqn:E0. 1: lia.
         assert (Pos.to_nat p = S (S n)) by lia. rewrite H0. reflexivity.
    * f_equal. f_equal. fext.
      assert (H:(x>0\/x=0\/x=-1\/x<(-1))%Z) by lia.
      destruct H as [H|[H|[H|H]]].
      -- destruct x; try lia.
         destruct ((Z.pos p + 1)%Z) eqn:E; cbn; try lia.
         destruct (Pos.to_nat p) eqn:E0. 1: lia.
         assert (Pos.to_nat p0 = S (S n)) by lia. rewrite H0. reflexivity.
      -- subst. reflexivity.
      -- subst. reflexivity.
      -- destruct x; try lia.
         destruct ((Z.neg p + 1)%Z) eqn:E; cbn; try lia.
         destruct (Pos.to_nat p) eqn:E0. 1: lia.
         assert (n=Pos.to_nat p0) by lia. rewrite <-H0.
         destruct n. 1: lia. reflexivity.
Qed.

Lemma ListES_step_spec tm x:
  step Σ tm (ListES_toES x) =
  match ListES_step tm x with
  | None => None
  | Some x1 => Some (ListES_toES x1)
  end.

Proof.
  destruct x as [l0 r0 m0 s0].
  unfold step, ListES_toES, ListES_step.
  destruct (tm s0 m0) as [[s1 d o]|]; [|reflexivity].
  destruct d; [destruct l0 as [|m1 l1]|destruct r0 as [|m1 r1]];
  f_equal; f_equal; extensionality z; unfold mov, upd, Dir_to_Z;
  destruct z as [|p|p]; try reflexivity.
  1: {
    destruct p as [p|p|]; [
      replace (Z.pos p~1 + Z.neg 1)%Z with (Z.pos p~0)%Z by lia;
      change ((Z.pos p~0 =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?Pos2Nat.inj_xO, ?Pos2Nat.inj_xI;
        pose proof (Pos2Nat.is_pos p); lia
    |
      replace (Z.pos p~0 + Z.neg 1)%Z with (Z.pos (Pos.pred_double p))%Z
        by (rewrite Pos.pred_double_spec; lia);
      change ((Z.pos (Pos.pred_double p) =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?pos_to_nat_pred_double, ?Pos2Nat.inj_xO;
        pose proof (Pos2Nat.is_pos p); lia
    |
      simpl; reflexivity ].
  }
  1: {
    replace (Z.neg p + Z.neg 1)%Z with (Z.neg (p + 1))%Z by lia.
    change ((Z.neg (p+1) =? 0)%Z) with false.
    rewrite Pos2Nat.inj_add. change (Pos.to_nat 1) with 1. rewrite Nat.add_1_r.
    change (nth (S (Pos.to_nat p)) (m0 :: @nil Σ) Σ0)
      with (nth (Pos.to_nat p) (@nil Σ) Σ0).
    rewrite nth_Sigma0_nil. reflexivity.
  }
  1: {
    destruct p as [p|p|]; [
      replace (Z.pos p~1 + Z.neg 1)%Z with (Z.pos p~0)%Z by lia;
      change ((Z.pos p~0 =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?Pos2Nat.inj_xO, ?Pos2Nat.inj_xI;
        pose proof (Pos2Nat.is_pos p); lia
    |
      replace (Z.pos p~0 + Z.neg 1)%Z with (Z.pos (Pos.pred_double p))%Z
        by (rewrite Pos.pred_double_spec; lia);
      change ((Z.pos (Pos.pred_double p) =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?pos_to_nat_pred_double, ?Pos2Nat.inj_xO;
        pose proof (Pos2Nat.is_pos p); lia
    |
      simpl; reflexivity ].
  }
  1: {
    replace (Z.neg p + Z.neg 1)%Z with (Z.neg (p + 1))%Z by lia.
    change ((Z.neg (p+1) =? 0)%Z) with false.
    rewrite Pos2Nat.inj_add. change (Pos.to_nat 1) with 1. rewrite Nat.add_1_r.
    simpl. reflexivity.
  }
  1: {
    replace (Z.pos p + Z.pos 1)%Z with (Z.pos (p + 1))%Z by lia.
    change ((Z.pos (p+1) =? 0)%Z) with false.
    rewrite Pos2Nat.inj_add. change (Pos.to_nat 1) with 1. rewrite Nat.add_1_r.
    change (nth (S (Pos.to_nat p)) (m0 :: @nil Σ) Σ0)
      with (nth (Pos.to_nat p) (@nil Σ) Σ0).
    rewrite nth_Sigma0_nil. reflexivity.
  }
  1: {
    destruct p as [p|p|]; [
      replace (Z.neg p~1 + Z.pos 1)%Z with (Z.neg p~0)%Z by lia;
      change ((Z.neg p~0 =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?Pos2Nat.inj_xO, ?Pos2Nat.inj_xI;
        pose proof (Pos2Nat.is_pos p); lia
    |
      replace (Z.neg p~0 + Z.pos 1)%Z with (Z.neg (Pos.pred_double p))%Z
        by (rewrite Pos.pred_double_spec; lia);
      change ((Z.neg (Pos.pred_double p) =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?pos_to_nat_pred_double, ?Pos2Nat.inj_xO;
        pose proof (Pos2Nat.is_pos p); lia
    |
      simpl; reflexivity ].
  }
  1: {
    replace (Z.pos p + Z.pos 1)%Z with (Z.pos (p + 1))%Z by lia.
    change ((Z.pos (p+1) =? 0)%Z) with false.
    rewrite Pos2Nat.inj_add. change (Pos.to_nat 1) with 1. rewrite Nat.add_1_r.
    simpl. reflexivity.
  }
  1: {
    destruct p as [p|p|]; [
      replace (Z.neg p~1 + Z.pos 1)%Z with (Z.neg p~0)%Z by lia;
      change ((Z.neg p~0 =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?Pos2Nat.inj_xO, ?Pos2Nat.inj_xI;
        pose proof (Pos2Nat.is_pos p); lia
    |
      replace (Z.neg p~0 + Z.pos 1)%Z with (Z.neg (Pos.pred_double p))%Z
        by (rewrite Pos.pred_double_spec; lia);
      change ((Z.neg (Pos.pred_double p) =? 0)%Z) with false;
      apply nth_shift_eq; rewrite ?pos_to_nat_pred_double, ?Pos2Nat.inj_xO;
        pose proof (Pos2Nat.is_pos p); lia
    |
      simpl; reflexivity ].
  }
Qed.

Lemma ListES_toES_O:
  (ListES_toES {| l := nil; r := nil; m := Σ0; s := St0 |}) = InitES Σ Σ0.

Proof.
  unfold InitES.
  cbn.
  f_equal.
  fext.
  destruct x.
  1: reflexivity.
  - destruct (Pos.to_nat p).
    1: reflexivity.
    destruct n; reflexivity.
  - destruct (Pos.to_nat p).
    1: reflexivity.
    destruct n; reflexivity.
Qed.

Lemma ListES_toES_O:
  (ListES_toES {| l := nil; r := nil; m := Σ0; s := St0 |}) = InitES Σ Σ0.

Proof.
  unfold ListES_toES, InitES. f_equal.
  extensionality x. destruct x as [|p0|p0]; try reflexivity.
  - destruct (Pos.to_nat p0) eqn:E; [lia|].
    simpl. destruct n; reflexivity.
  - destruct (Pos.to_nat p0) eqn:E; [lia|].
    simpl. destruct n; reflexivity.
Qed.

Lemma MidWord_enc_inj: is_inj MidWord_enc.

Proof.
  intros x1 x2 H.
  destruct x1 as [l1 r1 m1 s1].
  destruct x2 as [l2 r2 m2 s2].
  unfold MidWord_enc in H.
  pose proof (enc_list_inj _ _ H). clear H.
  invst H0.
  rewrite (St_enc_inj _ _ H1).
  rewrite (Σ_enc_inj _ _ H2).
  rewrite (listΣ_enc_inj _ _ H3).
  rewrite (listΣ_enc_inj _ _ H4).
  reflexivity.
Qed.

Lemma MidWord_enc_inj: is_inj MidWord_enc.

Proof.
  unfold is_inj, MidWord_enc. intros [la ra ma sa] [lb rb mb sb].
  intro H. apply enc_list_inj in H. simpl in H.
  injection H as Hs Hm Hl Hr.
  apply St_enc_inj in Hs. apply Σ_enc_inj in Hm.
  apply listΣ_enc_inj in Hl. apply listΣ_enc_inj in Hr.
  subst. reflexivity.
Qed.

Lemma MoveDist_Steps {tm n st st0 d}:
  MoveDist tm n st st0 d ->
  Steps Σ tm n st st0.

Proof.
  intros.
  induction H.
  1: ctor.
  ector; eauto 1.
Qed.

Lemma MoveDist_Steps {tm n st st0 d}:
  MoveDist tm n st st0 d ->
  Steps Σ tm n st st0.

Proof.
  induction 1.
  - constructor.
  - eapply steps_S; eauto.
Qed.

Lemma MoveDist_minus {tm n1 n2 st st0 st1 d d1}:
  MoveDist tm (n1+n2) st st0 d ->
  MoveDist tm n2 st st1 d1 ->
  MoveDist tm n1 st1 st0 (d-d1).

Proof.
  intros.
  destruct (MoveDist_split H) as [st3 [d3 [H1 H2]]].
  destruct (MoveDist_unique H1 H0). cg.
Qed.

Lemma MoveDist_minus {tm n1 n2 st st0 st1 d d1}:
  MoveDist tm (n1+n2) st st0 d ->
  MoveDist tm n2 st st1 d1 ->
  MoveDist tm n1 st1 st0 (d-d1).

Proof.
  intros H1 H2.
  apply MoveDist_split in H1. destruct H1 as [st1' [d1' [Hmd1 Hmd2]]].
  pose proof (MoveDist_unique H2 Hmd1) as [Heq Hd]. subst. exact Hmd2.
Qed.

Lemma MoveDist_split {tm n1 n2 st st0 d}:
  MoveDist tm (n1+n2) st st0 d ->
  exists st1 d1,
  MoveDist tm n2 st st1 d1 /\
  MoveDist tm n1 st1 st0 (d-d1).

Proof.
gd d. gd st0.
induction n1; intros.
- cbn in H.
  exists st0. exists d.
  split; auto 1.
  replace (d-d)%Z with 0%Z by lia.
  ctor.
- cbn in H.
  invst H.
  specialize (IHn1 _ _ H1).
  destruct IHn1 as [st1 [d1 [IHn1a IHn1b]]].
  exists st1. exists d1.
  split; auto 1.
  ector; eauto 1.
  rewrite <-H5. lia.
Qed.

Lemma MoveDist_split {tm n1 n2 st st0 d}:
  MoveDist tm (n1+n2) st st0 d ->
  exists st1 d1,
  MoveDist tm n2 st st1 d1 /\
  MoveDist tm n1 st1 st0 (d-d1).

Proof.
  revert st0 d. induction n1; intros st0 d H.
  - simpl in H. exists st0, d. split; [exact H|].
    replace (d - d)%Z with Z0 by lia. constructor.
  - change (S n1 + n2) with (S (n1 + n2)) in H.
    inversion_clear H.
    destruct (IHn1 _ _ H0) as [st1 [d1 [Hmd1 Hmd2]]].
    exists st1, d1. split; [exact Hmd1|].
    eapply MoveDist_S; eauto. lia.
Qed.

Lemma MoveDist_unique {tm n st0 st1 d st1' d'}:
  MoveDist tm n st0 st1 d ->
  MoveDist tm n st0 st1' d' ->
  (st1=st1' /\ d=d').

Proof.
  gd d'. gd st1'.
  gd d. gd st1.
  induction n.
  - intros.
    invst H. invst H0. tauto.
  - intros.
    invst H. invst H0.
    specialize (IHn _ _ _ _ H2 H5).
    destruct IHn as [IHn0 IHn1].
    invst IHn0.
    rewrite H8 in H4.
    invst H4.
    rewrite H7 in H3.
    invst H3.
    repeat split.
    rewrite <-H10 in H6.
    lia.
Qed.

Lemma MoveDist_unique {tm n st0 st1 d st1' d'}:
  MoveDist tm n st0 st1 d ->
  MoveDist tm n st0 st1' d' ->
  (st1=st1' /\ d=d').

Proof.
  intros H1. revert st1' d'.
  induction H1 as [|tm' n' st0' s1 t1 st2 d0 d1 tr H1' IH Hyzc Htm Hdist];
    intros st1' d' H2.
  - inversion H2; subst. split; reflexivity.
  - inversion H2; subst.
    destruct (IH _ _ H0) as [Heq Hdeq].
    inversion Heq; subst.
    rewrite Hyzc in H1. inversion H1; subst.
    rewrite Htm in H3. inversion H3; subst.
    split; [reflexivity | lia].
Qed.

Lemma NGramCPS_LRU_decider_0_spec len_l len_r m tm:
  NGramCPS_LRU_decider_0 len_l len_r m tm = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  intro H.
  unfold NGramCPS_LRU_decider_0 in H.
  eapply TM_history_LRU_NonHaltsFromInit.
  eapply NGramCPS_decider_spec.
  3: apply H.
  - apply Σ_history_enc_inj.
  - apply listT_enc_inj,Σ_history_enc_inj.
Qed.

Lemma NGramCPS_LRU_decider_0_spec len_l len_r m tm:
  NGramCPS_LRU_decider_0 len_l len_r m tm = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  intro H. unfold NGramCPS_LRU_decider_0 in H.
  apply TM_history_LRU_NonHaltsFromInit.
  exact (NGramCPS_decider_spec Σ_history len_l len_r Σ_history_enc Σ_history_enc_inj
    (listT_enc Σ_history_enc) (listT_enc_inj Σ_history_enc Σ_history_enc_inj)
    Σ_history_0 m (TM_history_LRU tm) H).
Qed.

Lemma NGramCPS_LRU_decider_spec len_l len_r m BB:
  HaltDecider_WF BB (NGramCPS_LRU_decider len_l len_r m).

Proof.
  intros tm.
  unfold NGramCPS_LRU_decider.
  pose proof (NGramCPS_LRU_decider_0_spec len_l len_r m tm).
  destruct (NGramCPS_LRU_decider_0 len_l len_r m tm); tauto.
Qed.

Lemma NGramCPS_LRU_decider_spec len_l len_r m BB:
  HaltDecider_WF BB (NGramCPS_LRU_decider len_l len_r m).

Proof.
  unfold HaltDecider_WF, NGramCPS_LRU_decider. intro tm.
  destruct (NGramCPS_LRU_decider_0 len_l len_r m tm) eqn:E; [|trivial].
  apply NGramCPS_LRU_decider_0_spec in E. exact E.
Qed.

Lemma NGramCPS_decider_0_spec m n tm S:
  AES_impl_WF S ->
  NGramCPS_decider_0 m n tm S = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  gd S. gd n.
  induction m; intros.
  1: cbn in H0; cg.
  cbn in H0.
  destruct (update_AES tm (fst (mset' S)) S true n) as [[S' flag] n0_] eqn:E.
  epose proof (update_AES_Closed _ _ _ _ H) as H1.
  rewrite E in H1.
  destruct H1 as [H1a H1b].
  pose proof (check_InitES_InAES_spec S' H1a).
  destruct flag.
  - specialize (H1b eq_refl).
    destruct H1b as [H1b H1c].
    specialize (H1 H0).
    subst.
    apply (AES_Closed_NonHalt _ _ _ H1 H1b).
  - eapply IHm.
    + apply H1a.
    + apply H0.
Qed.

Lemma NGramCPS_decider_0_spec m n tm S:
  AES_impl_WF S ->
  NGramCPS_decider_0 m n tm S = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  revert n S. induction m as [|m' IH]; intros n S HSI Hgp.
  - simpl in Hgp. discriminate.
  - simpl in Hgp.
    pose proof (update_AES_Closed tm S true n HSI) as Hhp.
    destruct (update_AES tm (fst (mset' S)) S true n) as [[S' flag'] n0] eqn:Es.
    destruct Hhp as [HSI' Hhp2].
    destruct flag'.
    + destruct (Hhp2 eq_refl) as [Hadtw Heq]. subst S'.
      assert (Hp9: InAES (InitES Σ Σ0) (AES_impl_to_AES S)).
      { apply check_InitES_InAES_spec; assumption. }
      unfold HaltsFromInit. apply (AES_Closed_NonHalt tm (AES_impl_to_AES S)). exact Hp9. exact Hadtw.
    + apply (IH n0 S' HSI' Hgp).
Qed.

Lemma NGramCPS_decider_impl1_0_spec len_h len_l len_r m tm:
  NGramCPS_decider_impl1_0 len_h len_l len_r m tm = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  intro H.
  unfold NGramCPS_decider_impl1_0 in H.
  eapply TM_history_NonHaltsFromInit.
  eapply NGramCPS_decider_spec.
  3: apply H.
  - apply Σ_history_enc_inj.
  - apply listT_enc_inj,Σ_history_enc_inj.
Qed.

Lemma NGramCPS_decider_impl1_0_spec len_h len_l len_r m tm:
  NGramCPS_decider_impl1_0 len_h len_l len_r m tm = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  intro H. unfold NGramCPS_decider_impl1_0 in H.
  apply TM_history_NonHaltsFromInit with (n:=len_h).
  exact (NGramCPS_decider_spec Σ_history len_l len_r Σ_history_enc Σ_history_enc_inj
    (listT_enc Σ_history_enc) (listT_enc_inj Σ_history_enc Σ_history_enc_inj)
    Σ_history_0 m (TM_history len_h tm) H).
Qed.

Lemma NGramCPS_decider_impl1_spec len_h len_l len_r m BB:
  HaltDecider_WF BB (NGramCPS_decider_impl1 len_h len_l len_r m).

Proof.
  intros tm.
  unfold NGramCPS_decider_impl1.
  pose proof (NGramCPS_decider_impl1_0_spec len_h len_l len_r m tm).
  destruct (NGramCPS_decider_impl1_0 len_h len_l len_r m tm); tauto.
Qed.

Lemma NGramCPS_decider_impl1_spec len_h len_l len_r m BB:
  HaltDecider_WF BB (NGramCPS_decider_impl1 len_h len_l len_r m).

Proof.
  unfold HaltDecider_WF, NGramCPS_decider_impl1. intro tm.
  destruct (NGramCPS_decider_impl1_0 len_h len_l len_r m tm) eqn:E; [|trivial].
  apply NGramCPS_decider_impl1_0_spec in E. exact E.
Qed.

Lemma NGramCPS_decider_impl2_0_spec len_l len_r m tm:
  NGramCPS_decider_impl2_0 len_l len_r m tm = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  intro H.
  unfold NGramCPS_decider_impl2_0 in H.
  eapply NGramCPS_decider_spec; eauto 1.
  - apply Σ_enc_inj.
  - apply listΣ_inj.
Qed.

Lemma NGramCPS_decider_impl2_0_spec len_l len_r m tm:
  NGramCPS_decider_impl2_0 len_l len_r m tm = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  intro H. unfold NGramCPS_decider_impl2_0 in H.
  exact (NGramCPS_decider_spec Σ len_l len_r Σ_enc Σ_enc_inj
    listΣ_enc listΣ_inj Σ0 m tm H).
Qed.

Lemma NGramCPS_decider_impl2_spec len_l len_r m BB:
  HaltDecider_WF BB (NGramCPS_decider_impl2 len_l len_r m).

Proof.
  intros tm.
  unfold NGramCPS_decider_impl2.
  pose proof (NGramCPS_decider_impl2_0_spec len_l len_r m tm).
  destruct (NGramCPS_decider_impl2_0 len_l len_r m tm); tauto.
Qed.

Lemma NGramCPS_decider_impl2_spec len_l len_r m BB:
  HaltDecider_WF BB (NGramCPS_decider_impl2 len_l len_r m).

Proof.
  unfold HaltDecider_WF, NGramCPS_decider_impl2. intro tm.
  destruct (NGramCPS_decider_impl2_0 len_l len_r m tm) eqn:E; [|trivial].
  apply NGramCPS_decider_impl2_0_spec in E. exact E.
Qed.

Lemma NGramCPS_decider_spec m tm:
  NGramCPS_decider m tm = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  unfold NGramCPS_decider.
  destruct len_l as [|nl];
  destruct len_r as [|nr];
  cg.
  apply NGramCPS_decider_0_spec.
  split.
  {
    destruct ((xset_ins (PositiveMap.empty (list Σ * PositiveMap.tree unit)) (repeat Σ0 (S nl)))) as [ls' flag] eqn:E.
    apply (xset_ins_spec _ _ _ _ _ xset_WF_empty E).
  }
  split.
  {
    destruct ((xset_ins (PositiveMap.empty (list Σ * PositiveMap.tree unit)) (repeat Σ0 (S nr)))) as [rs' flag] eqn:E.
    apply (xset_ins_spec _ _ _ _ _ xset_WF_empty E).
  }
  {
    destruct ((mset_ins0 (nil, PositiveMap.empty unit)
          {| l := repeat Σ0 (S nl); r := repeat Σ0 (S nr); m := Σ0; s := St0 |})) as [ms' flag] eqn:E.
    apply (mset_ins0_spec _ _ _ _ (empty_set_WF _) E).
  }
Qed.

Lemma NGramCPS_decider_spec m tm:
  NGramCPS_decider m tm = true ->
  ~HaltsFromInit Σ Σ0 tm.

Proof.
  unfold NGramCPS_decider. intro H.
  destruct len_l as [|nl]; [discriminate|].
  destruct len_r as [|nr]; [discriminate|].
  assert (wKw3H_init: forall xs n, xset_WF xs -> xset_WF (fst (xset_ins xs (repeat Σ0 (Datatypes.S n))))).
  { intros xs n0 Hwk.
    destruct (xset_ins xs (repeat Σ0 (Datatypes.S n0))) as [xs' fl] eqn:Eng.
    simpl. exact (proj1 (xset_ins_spec xs Σ0 (repeat Σ0 n0) xs' fl Hwk Eng)). }
  assert (gHKhe_init: forall ms mw, mset_WF ms -> mset_WF (fst (mset_ins0 ms mw))).
  { intros ms mw Hms.
    destruct (mset_ins0 ms mw) as [ms' fl] eqn:Ems.
    simpl. exact (proj1 (mset_ins0_spec ms mw ms' fl Hms Ems)). }
  eapply NGramCPS_decider_0_spec; [|exact H].
  split; [|split].
  - apply wKw3H_init. exact xset_WF_empty.
  - apply wKw3H_init. exact xset_WF_empty.
  - apply gHKhe_init. exact (empty_set_WF MidWord_enc).
Qed.

Lemma NonHalt_iff {tm st}:
  NonHalt tm st <-> ~Halts tm st.

Proof.
  split; intro.
  - intro H0.
    destruct H0 as [n H0].
    specialize (H (S n)).
    destruct H as [st' H].
    eapply Steps_NonHalt.
    2,3: eassumption.
    lia.
  - intro n.
    induction n.
    + eexists. ector.
    + destruct IHn as [st' IHn].
      unfold Halts,HaltsAt in H.
      destruct (step tm st') as [st''|] eqn:E.
      * exists st''. ector; eassumption.
      * assert False by (apply H; eexists; eexists; split; eassumption).
        contradiction.
Qed.

Lemma NonHalt_iff {tm st}:
  NonHalt tm st <-> ~Halts tm st.

Proof.
  unfold NonHalt, Halts, HaltsAt. split.
  - intros Hinf [n [st' [Hsteps Hhalt]]].
    destruct (Hinf (S n)) as [st1 Hst1].
    assert (Hex: exists stm, Steps tm n st stm /\ step tm stm = Some st1).
    { inversion Hst1; subst; eauto. }
    destruct Hex as [stm [Hstm Hstep]].
    replace st' with stm in * by (eapply Steps_unique; eassumption).
    congruence.
  - intros Hnhalt n.
    induction n.
    + exists st. constructor.
    + destruct IHn as [stn Hstn].
      destruct (step tm stn) eqn:E.
      * exists e. eapply steps_S; eauto.
      * exfalso. apply Hnhalt. exists n. exists stn. auto.
Qed.

Lemma RepWL_ES_decider_spec n BB:
  HaltDecider_WF BB (RepWL_ES_decider n).

Proof.
  eapply T_decider_spec.
  - apply RepWL_ES_enc_inj.
  - apply In_RepWL_ES_InitES.
  - apply RepWL_step_spec.
Qed.

Lemma RepWL_ES_decider_spec n BB:
  HaltDecider_WF BB (RepWL_ES_decider n).

Proof.
  unfold RepWL_ES_decider.
  apply (T_decider_spec _ RepWL_ES_enc RepWL_ES_enc_inj In_RepWL_ES RepWL_InitES In_RepWL_ES_InitES RepWL_step RepWL_step_spec).
Qed.

Lemma RepWL_ES_enc_inj: is_inj RepWL_ES_enc.

Proof.
  intros x1 x2 H.
  destruct x1,x2.
  epose proof (enc_list_inj _ _ H).
  invst H0.
  f_equal.
  - eapply list_enc_inj; eauto 1.
    apply RepeatWord_enc_inj.
  - eapply list_enc_inj; eauto 1.
    apply RepeatWord_enc_inj.
  - apply St_enc_inj; auto 1.
  - apply Dir_enc_inj; auto 1.
Qed.

Lemma RepWL_ES_enc_inj: is_inj RepWL_ES_enc.

Proof.
  intros [l1 r1 s1 sgn1] [l2 r2 s2 sgn2] H.
  unfold RepWL_ES_enc in H.
  apply enc_list_inj in H. injection H as H1 H2 H3 H4.
  apply Dir_enc_inj in H1.
  apply St_enc_inj in H2.
  apply (list_enc_inj RepeatWord_enc RepeatWord_enc_inj) in H3.
  apply (list_enc_inj RepeatWord_enc RepeatWord_enc_inj) in H4.
  subst. reflexivity.
Qed.

Lemma RepWL_step00_spec tm x w0 r0:
  match RepWL_step00 tm x w0 r0 with
  | None => True
  | Some x1 =>
  let (l0,_,s0,sgn0):=x in
    forall st0, In_RepWL_ES st0 {| l:=l0; r:=push' r0 w0; s:=s0; sgn:=sgn0 |} ->
    exists n st1, (Steps Σ tm (1+n) st0 st1 /\ In_RepWL_ES st1 x1)
  end.

Proof.
unfold RepWL_step00.
destruct x as [l0 r0' s0 sgn0].
pose proof (WordUpdate_spec tm s0 w0 sgn0).
destruct (WordUpdate tm s0 w0 sgn0) as [[[s1 w1] d1]|].
2: trivial.
destruct d1 eqn:Ed1.
- intros.
  destruct st0 as [s0' t0'].
  invst H0.
  destruct sgn0.
  + specialize (H l1 (halftape_skipn (length w0) r1)).
    destruct H as [n H]. cbn. cbn in H.
    exists n.
    exists (s1, make_tape'' (app_halftape w1 (halftape_skipn (length w0) r1)) nil 
        (l1) Dpos).
    split.
    * unfold make_tape'' in H.
      destruct w0;
      cbn in H.
      ++ apply H.
      ++ replace (make_tape' (half_tape_cdr r1) nil (r1 0) nil l1) with
        (make_tape' (halftape_skipn (S (length w0)) r1) w0 σ nil l1).
        apply H.
        unfold make_tape'.
        invst H8.
        invst H3.
        rewrite <-app_halftape_assoc.
        cbn.
        f_equal.
        rewrite app_halftape_nil.
        apply app_halftape_skipn_cdr.
    * ector; eauto 1.
      invst H8. invst H3. invst H7.
      rewrite app_nil_r.
      apply push_spec.
      rewrite app_halftape_skipn.
      apply H6.
  + specialize (H l1 (halftape_skipn (length w0) r1)).
    destruct H as [n H]. cbn. cbn in H.
    exists n.
    exists (s1, make_tape'' (app_halftape w1 (halftape_skipn (length w0) r1)) nil 
        (l1) Dneg).
    split.
    * unfold make_tape'' in H.
      destruct w0;
      cbn in H.
      ++ rewrite halftape_skipn_0 in H.
        rewrite halftape_skipn_0.
        unfold make_tape''.
        apply H.
      ++ replace (make_tape' l1 nil (r1 0) nil (half_tape_cdr r1)) with
        (make_tape' l1 nil σ w0 (halftape_skipn (S (length w0)) r1)).
        apply H.
        unfold make_tape'.
        invst H8.
        invst H3.
        rewrite <-app_halftape_assoc.
        cbn.
        f_equal.
        rewrite app_halftape_nil.
        apply app_halftape_skipn_cdr.
    * ector; eauto 1.
      invst H8. invst H3. invst H7.
      rewrite app_nil_r.
      apply push_spec.
      rewrite app_halftape_skipn.
      apply H6.
- intros.
  destruct st0 as [s0' t0'].
  invst H0.
  destruct sgn0.
  + specialize (H l1 (halftape_skipn (length w0) r1)).
    destruct H as [n H]. cbn. cbn in H.
    exists n.
    exists (s1, make_tape'' (app_halftape w1 l1) nil (halftape_skipn (length w0) r1)
        Dneg).
    split.
    * unfold make_tape'' in H.
      destruct w0;
      cbn in H.
      ++ rewrite halftape_skipn_0 in H.
        rewrite halftape_skipn_0.
        unfold make_tape''.
        apply H.
      ++ replace (make_tape' (half_tape_cdr r1) nil (r1 0) nil l1) with (make_tape' (halftape_skipn (S (length w0)) r1) w0 σ nil l1).
        apply H.
        unfold make_tape'.
        repeat rewrite app_halftape_nil.
        invst H8. invst H3.
        rewrite <-app_halftape_assoc.
        cbn.
        f_equal.
        apply app_halftape_skipn_cdr.
    * invst H8. invst H3. invst H7.
      ector; eauto 1.
      -- apply push_spec,H4.
      -- rewrite app_nil_r,app_halftape_skipn.
         apply H6.
  + specialize (H l1 (halftape_skipn (length w0) r1)).
    destruct H as [n H]. cbn. cbn in H.
    exists n.
    exists (s1, make_tape'' (app_halftape w1 l1) nil (halftape_skipn (length w0) r1)
        Dpos).
    split.
    * unfold make_tape'' in H.
      destruct w0;
      cbn in H.
      ++ rewrite halftape_skipn_0 in H.
        rewrite halftape_skipn_0.
        unfold make_tape''.
        apply H.
      ++ replace (make_tape' l1 nil (r1 0) nil (half_tape_cdr r1)) with 
          (make_tape' l1 nil σ w0 (halftape_skipn (S (length w0)) r1)).
        apply H.
        unfold make_tape'.
        repeat rewrite app_halftape_nil.
        invst H8. invst H3.
        rewrite <-app_halftape_assoc.
        cbn.
        f_equal.
        apply app_halftape_skipn_cdr.
    * invst H8. invst H3. invst H7.
      ector; eauto 1.
      -- apply push_spec,H4.
      -- rewrite app_nil_r,app_halftape_skipn.
         apply H6.
Qed.

Lemma RepWL_step00_spec tm x w0 r0:
  match RepWL_step00 tm x w0 r0 with
  | None => True
  | Some x1 =>
  let (l0,_,s0,sgn0):=x in
    forall st0, In_RepWL_ES st0 {| l:=l0; r:=push' r0 w0; s:=s0; sgn:=sgn0 |} ->
    exists n st1, (Steps Σ tm (1+n) st0 st1 /\ In_RepWL_ES st1 x1)
  end.

Proof.
  destruct x as [l0 r_ign s0 sgn0].
  destruct w0 as [|m0 w2].
  { simpl. exact I. }
  pose proof (WordUpdate_spec tm s0 (m0::w2) sgn0) as Hstep.
  unfold RepWL_step00.
  destruct (WordUpdate tm s0 (m0::w2) sgn0) as [[[s1 w1] is_back]|] eqn:ED.
  2:{ exact I. }
  destruct is_back.
  - intros st0 HinR.
    inversion HinR as [l1 r1 ? ? ? ? Hml Hmr Hst_eq Hes_eq].
    clear HinR. subst.
    inversion Hmr as [|h_rw t_rw fh ft Hrw_fh Hrw_ft Heq_r Heq_ft]. subst.
    clear Hmr.
    inversion Hrw_fh; subst; try (exfalso; congruence).
    match goal with H : RepW_match _ _ |- _ => inversion H; subst; try (exfalso; congruence); clear H end.
    specialize (Hstep l1 ft).
    destruct Hstep as [n Hsteps].
    rewrite app_nil_r.
    rewrite tape_eq.
    exists n, (s1, make_tape'' (app_halftape w1 ft) nil l1 (Dir_rev sgn0)).
    split; [exact Hsteps|].
    apply In_RepWL_ES_intro.
    -- apply push_spec. exact Hrw_ft.
    -- exact Hml.
  - intros st0 HinR.
    inversion HinR as [l1 r1 ? ? ? ? Hml Hmr Hst_eq Hes_eq].
    clear HinR. subst.
    inversion Hmr as [|h_rw t_rw fh ft Hrw_fh Hrw_ft Heq_r Heq_ft]. subst.
    clear Hmr.
    inversion Hrw_fh; subst; try (exfalso; congruence).
    match goal with H : RepW_match _ _ |- _ => inversion H; subst; try (exfalso; congruence); clear H end.
    specialize (Hstep l1 ft).
    destruct Hstep as [n Hsteps].
    rewrite app_nil_r.
    rewrite tape_eq.
    exists n, (s1, make_tape'' (app_halftape w1 l1) nil ft sgn0).
    split; [exact Hsteps|].
    apply In_RepWL_ES_intro.
    -- apply push_spec. exact Hml.
    -- exact Hrw_ft.
Qed.

Lemma RepWL_step0_spec tm x w0 r0:
  match RepWL_step0 tm x w0 r0 with
  | None => True
  | Some x1 =>
  let (l0,_,s0,sgn0):=x in
    forall st0, (exists r1, In r1 r0 /\ In_RepWL_ES st0 {| l:=l0; r:=push' r1 w0; s:=s0; sgn:=sgn0 |}) ->
    exists n st1 x2, (Steps Σ tm (1+n) st0 st1 /\ In_RepWL_ES st1 x2 /\ In x2 x1)
  end.

Proof.
  induction r0.
  - cbn.
    destruct x as [l0 r0' s0 sgn0].
    intros.
    destruct H as [n1 [Ha Hb]].
    contradiction.
  - cbn.
    pose proof (RepWL_step00_spec tm x w0 a) as H.
    destruct (RepWL_step00 tm x w0 a).
    2: trivial.
    destruct (RepWL_step0 tm x w0 r0).
    2: trivial.
    destruct x as [l1 r0' s0 sgn0].
    intros.
    destruct H0 as [r2 [H0a H0b]].
    destruct H0a as [H0a|H0a].
    + subst a. specialize (H st0 H0b).
      destruct H as [n [st1 [Ha Hb]]].
      exists n. exists st1. eexists.
      repeat split; eauto 1.
      left. reflexivity.
    + specialize (IHr0 st0).
      eassert (H1:_). {
        apply IHr0.
        eexists.
        split; eauto 1.
      }
      destruct H1 as [n [st1 [x2 [H1a [H1b H1c]]]]].
      exists n. exists st1. exists x2.
      repeat split; auto 1. right. auto 1.
Qed.

Lemma RepWL_step0_spec tm x w0 r0:
  match RepWL_step0 tm x w0 r0 with
  | None => True
  | Some x1 =>
  let (l0,_,s0,sgn0):=x in
    forall st0, (exists r1, In r1 r0 /\ In_RepWL_ES st0 {| l:=l0; r:=push' r1 w0; s:=s0; sgn:=sgn0 |}) ->
    exists n st1 x2, (Steps Σ tm (1+n) st0 st1 /\ In_RepWL_ES st1 x2 /\ In x2 x1)
  end.

Proof.
  destruct x as [l0 r_ignored s0 sgn0].
  induction r0 as [|r1h r0t IH].
  - simpl. intros st0 [r1 [Hin _]]. destruct Hin.
  - simpl RepWL_step0.
    pose proof (RepWL_step00_spec tm (Build_RepeatWordList_ES l0 r_ignored s0 sgn0) w0 r1h) as HV.
    simpl RepWL_step00 in HV.
    destruct (WordUpdate tm s0 w0 sgn0) as [[[s1 w1] is_back]|]; [|trivial].
    destruct is_back.
    + specialize (IH). simpl in IH.
      destruct (RepWL_step0 tm (Build_RepeatWordList_ES l0 r_ignored s0 sgn0) w0 r0t) as [ret|]; [|trivial].
      intros st0 [r1 [Hin HinR]].
      destruct Hin as [Heq|Hin0].
      * subst r1. specialize (HV st0 HinR).
        destruct HV as [n [st1 [Hsteps HinR1]]].
        exists n, st1, {| l := push r1h w1; r := l0; s := s1; sgn := Dir_rev sgn0 |}.
        repeat split; [exact Hsteps|exact HinR1|left; reflexivity].
      * specialize (IH st0).
        assert (Hex: exists r1, In r1 r0t /\ In_RepWL_ES st0 {| l := l0; r := push' r1 w0; s := s0; sgn := sgn0 |}).
        { exists r1. split; [exact Hin0|exact HinR]. }
        specialize (IH Hex).
        destruct IH as [n [st1 [x2 [Hsteps [HinR1 Hinx2]]]]].
        exists n, st1, x2. repeat split; [exact Hsteps|exact HinR1|right; exact Hinx2].
    + specialize (IH). simpl in IH.
      destruct (RepWL_step0 tm (Build_RepeatWordList_ES l0 r_ignored s0 sgn0) w0 r0t) as [ret|]; [|trivial].
      intros st0 [r1 [Hin HinR]].
      destruct Hin as [Heq|Hin0].
      * subst r1. specialize (HV st0 HinR).
        destruct HV as [n [st1 [Hsteps HinR1]]].
        exists n, st1, {| l := push l0 w1; r := r1h; s := s1; sgn := sgn0 |}.
        repeat split; [exact Hsteps|exact HinR1|left; reflexivity].
      * specialize (IH st0).
        assert (Hex: exists r1, In r1 r0t /\ In_RepWL_ES st0 {| l := l0; r := push' r1 w0; s := s0; sgn := sgn0 |}).
        { exists r1. split; [exact Hin0|exact HinR]. }
        specialize (IH Hex).
        destruct IH as [n [st1 [x2 [Hsteps [HinR1 Hinx2]]]]].
        exists n, st1, x2. repeat split; [exact Hsteps|exact HinR1|right; exact Hinx2].
Qed.

Lemma RepWL_step_spec tm x:
  match RepWL_step tm x with
  | None => True
  | Some ls =>
    forall st0, In_RepWL_ES st0 x ->
    exists n st1 x1, (Steps Σ tm (1+n) st0 st1 /\ In_RepWL_ES st1 x1 /\ In x1 ls)
  end.

Proof.
  unfold RepWL_step.
  destruct x as [l0 r0 s0 sgn0].
  pose proof (pop_spec r0) as H0.
  destruct (pop r0) as [[w0 ls]|] eqn:E.
  2: trivial.
  pose proof (RepWL_step0_spec tm {| l := l0; r := r0; s := s0; sgn := sgn0 |} w0 ls) as H.
  destruct (RepWL_step0 tm {| l := l0; r := r0; s := s0; sgn := sgn0 |} w0 ls).
  2: trivial.
  intros.
  specialize (H st0).
  apply H.
  invst H1.

  specialize (H0 _ H8).
  destruct H0 as [wl0 [f1 [H0a [H0b H0c]]]].
  exists wl0.
  repeat split; auto 1.
  rewrite H0c.
  ector; eauto 1.
  rewrite <-app_nil_r.
  ctor. ctor.
Qed.

Lemma RepWL_step_spec tm x:
  match RepWL_step tm x with
  | None => True
  | Some ls =>
    forall st0, In_RepWL_ES st0 x ->
    exists n st1 x1, (Steps Σ tm (1+n) st0 st1 /\ In_RepWL_ES st1 x1 /\ In x1 ls)
  end.

Proof.
  destruct x as [l0 r0 s0 sgn0].
  unfold RepWL_step.
  pose proof (pop_spec r0) as Hb.
  destruct (pop r0) as [[w0 ls0]|] eqn:Excj; [|exact I].
  pose proof (RepWL_step0_spec tm (Build_RepeatWordList_ES l0 r0 s0 sgn0) w0 ls0) as Hckj.
  simpl in Hckj.
  destruct (RepWL_step0 tm (Build_RepeatWordList_ES l0 r0 s0 sgn0) w0 ls0) as [ret|] eqn:Ej; [|exact I].
  intros st0 HinR.
  apply Hckj.
  inversion HinR as [l1 r1 l0' r0' s0' sgn0' Hl Hr Hst Hx]. subst.
  specialize (Hb r1 Hr).
  destruct Hb as [wl0 [f1 [Hinwl0 [Hmatch Heq]]]].
  exists wl0. split; [exact Hinwl0|].
  subst r1.
  unfold push'.
  assert (Hrmatch: RepWL_match ({| w := w0; min_cnt := 1; is_const := true |} :: wl0) (app_halftape w0 f1)).
  { replace (app_halftape w0 f1) with (app_halftape (w0 ++ nil) f1)
      by (rewrite app_nil_r; reflexivity).
    apply RepWL_match_S; [|exact Hmatch].
    apply RepW_match_S0. apply RepW_match_O.
  }
  exact (In_RepWL_ES_intro l1 (app_halftape w0 f1) l0
    ({| w := w0; min_cnt := 1; is_const := true |} :: wl0) s0 sgn0
    Hl Hrmatch).
Qed.

Lemma RepeatWord_enc_inj: is_inj RepeatWord_enc.

Proof.
  intros x1 x2 H.
  destruct x1,x2.
  epose proof (enc_list_inj _ _ H).
  invst H0.
  f_equal.
  - apply listΣ_inj; auto 1.
  - lia.
  - apply bool_enc_inj; auto 1.
Qed.

Lemma RepeatWord_enc_inj: is_inj RepeatWord_enc.

Proof.
  intros [w1 mc1 isc1] [w2 mc2 isc2] H.
  unfold RepeatWord_enc in H.
  apply enc_list_inj in H. injection H as H1 H2 H3.
  apply listΣ_inj in H1.
  apply SuccNat2Pos.inj in H2.
  apply bool_enc_inj in H3.
  subst. reflexivity.
Qed.

Lemma SearchQueue_bfs_spec q x0 f:
  SearchQueue_WF q x0 ->
  HaltDecider_WF f ->
  SearchQueue_WF (SearchQueue_bfs q f) x0.

Proof.
  intros.
  unfold SearchQueue_bfs.
  apply SearchQueue_reset_spec.
  apply SearchQueue_upds_bfs_spec; auto 1.
Qed.

Lemma SearchQueue_bfs_spec q x0 f:
  SearchQueue_WF q x0 ->
  HaltDecider_WF f ->
  SearchQueue_WF (SearchQueue_bfs q f) x0.

Proof.
  intros Hq Hf. unfold SearchQueue_bfs. apply SearchQueue_reset_spec. apply SearchQueue_upds_bfs_spec; auto.
Qed.

Lemma SearchQueue_reset_spec {q x0}:
  SearchQueue_WF q x0 ->
  SearchQueue_WF (SearchQueue_reset q) x0.

Proof.
  unfold SearchQueue_WF,SearchQueue_reset.
  destruct q as [q1 q2].
  intro.
  split.
  - intros. apply H.
    rewrite app_nil_r in H0. apply H0.
  - intros. apply H.
    intros. apply H0. rewrite app_nil_r. apply H1.
Qed.

Lemma SearchQueue_reset_spec {q x0}:
  SearchQueue_WF q x0 ->
  SearchQueue_WF (SearchQueue_reset q) x0.

Proof.
  destruct q as [q1 q2]. unfold SearchQueue_WF, SearchQueue_reset.
  intros [Hwf Himp]. split.
  - intros x Hx. rewrite app_nil_r in Hx. apply Hwf. apply in_or_app.
    apply in_app_or in Hx. destruct Hx; auto.
  - intros Hall. apply Himp. intros x Hx. apply Hall.
    rewrite app_nil_r. apply in_or_app. apply in_app_or in Hx. destruct Hx; auto.
Qed.

Lemma SearchQueue_upd_bfs_spec {q x0 f}:
  SearchQueue_WF q x0 ->
  HaltDecider_WF f ->
  SearchQueue_WF (SearchQueue_upd_bfs q f) x0.

Proof.
  intros.
  pose proof (SearchQueue_upd_spec H H0).
  unfold SearchQueue_WF.
  unfold SearchQueue_upd_bfs.
  unfold SearchQueue_WF in H1.
  unfold SearchQueue_upd in H1.
  destruct q as [q1 q2].
  destruct q1 as [|h t].
  1: apply H1.
  destruct (f (TNF_tm h)); auto 1.
  assert (
    forall x, In x ((TNF_Node_expand h s i ++ t) ++ q2) <-> In x (t ++ TNF_Node_expand h s i ++ q2)
  ). {
  intros.
  repeat rewrite in_app_iff.
  tauto.
  }
  split.
  - intro. rewrite <-H2.
    apply H1.
  - intro. apply H1.
    intros.
    apply H3; auto 1.
    rewrite <-H2.
    apply H4.
Qed.

Lemma SearchQueue_upd_bfs_spec {q x0 f}:
  SearchQueue_WF q x0 ->
  HaltDecider_WF f ->
  SearchQueue_WF (SearchQueue_upd_bfs q f) x0.

Proof.
  intros Hq Hf.
  destruct q as [q1 q2]. destruct q1 as [|h t].
  - simpl. exact Hq.
  - simpl. unfold SearchQueue_WF in Hq. destruct Hq as [Hwf Himp].
    specialize (Hf (TNF_tm h)) as Hfh.
    assert (Hwf_h: TNF_Node_WF h).
    { apply Hwf. apply in_or_app. left. left. reflexivity. }
    assert (Hwf_t: forall x, In x t -> TNF_Node_WF x).
    { intros x Hx. apply Hwf. apply in_or_app. left. right. exact Hx. }
    assert (Hwf_q2: forall x, In x q2 -> TNF_Node_WF x).
    { intros x Hx. apply Hwf. apply in_or_app. right. exact Hx. }
    destruct (f (TNF_tm h)) eqn:Ef; unfold SearchQueue_WF.
    + (* Result_Halt s i *)
      destruct Hfh as [n [t0 [Hhalt [Hsteps [Heqi Hle]]]]].
      subst i.
      pose proof (TNF_Node_expand_spec Hhalt Hsteps Hle Hwf_h) as [Hwf_children Hchildren].
      split.
      * intros x Hx. apply in_app_or in Hx. destruct Hx as [Hx|Hx].
        -- apply Hwf_t. exact Hx.
        -- apply in_app_or in Hx. destruct Hx as [Hx|Hx].
           ++ apply Hwf_children. exact Hx.
           ++ apply Hwf_q2. exact Hx.
      * intros Hall. apply Himp. intros x Hx. simpl in Hx.
        destruct Hx as [Heq|Hx].
        -- subst x. apply Hchildren. intros x' Hx'. apply Hall.
           apply in_or_app. right. apply in_or_app. left. exact Hx'.
        -- apply in_app_or in Hx. destruct Hx as [Hx|Hx].
           ++ apply Hall. apply in_or_app. left. exact Hx.
           ++ apply Hall. apply in_or_app. right. apply in_or_app. right. exact Hx.
    + (* Result_NonHalt *)
      split.
      * intros x Hx. apply in_app_or in Hx. destruct Hx as [Hx|Hx].
        -- apply Hwf_t. exact Hx.
        -- apply Hwf_q2. exact Hx.
      * intros Hall. apply Himp. intros x Hx. simpl in Hx.
        destruct Hx as [Heq|Hx].
        -- subst x. apply TNF_Node_NonHalt. exact Hfh.
        -- apply in_app_or in Hx. destruct Hx as [Hx|Hx].
           ++ apply Hall. apply in_or_app. left. exact Hx.
           ++ apply Hall. apply in_or_app. right. exact Hx.
    + (* Result_Unknown *)
      split.
      * intros x Hx. apply in_app_or in Hx. destruct Hx as [Hx|Hx].
        -- apply Hwf_t. exact Hx.
        -- simpl in Hx. destruct Hx as [Heq|Hx].
           ++ subst x. exact Hwf_h.
           ++ apply Hwf_q2. exact Hx.
      * intros Hall. apply Himp. intros x Hx. simpl in Hx.
        destruct Hx as [Heq|Hx].
        -- subst x. apply Hall. apply in_or_app. right. left. reflexivity.
        -- apply in_app_or in Hx. destruct Hx as [Hx|Hx].
           ++ apply Hall. apply in_or_app. left. exact Hx.
           ++ apply Hall. apply in_or_app. right. right. exact Hx.
Qed.