Theory Wrap_Defs

theory Wrap_Defs
  imports Wrap_Base "Multitape_TM_Substrate.Multitape_Origin_Float"
begin

section ‹Faithful (k-tape) encoding wrap: plant-‹le› variant (HU 12.4)›

text ‹Reaching faithful ‹k› tapes for the super-linear speed-up
  \<^cite>‹‹Theorem 12.3› in "Hopcroft1979:introduction"› by
  ∗‹rewinding› the reused input tape costs a ‹~2n› setup that the
  super-linear growth hypothesis absorbs.  Theorem 12.4's
  tight ‹(1+ε)n› bound cannot absorb it, so this variant avoids the
  rewind of the input tape entirely: it plants a fresh ‹le› at the input
  head's final position, ∗‹floating› the origin (the spent raw input to
  its left becomes unreachable, penned off by clause 1).

  Only the reset phase differs from the transpose wrap.  The storage
  tape (physical @{text 1}, carrying M's tape 0 = the encoded input) is
  still rewound to its ‹le› --- but that is only ‹⌈n/c⌉› cells (the
  encoded length), the ‹ε⋅n› term --- via the generic single-tape
  rewind @{const wrap_rewind_loop_delta_gen}.  The input tape (physical
  @{text 0}, becoming M's tape 1) is ∗‹not› rewound: the rewind-done
  step plants ‹le› on it and hands over to @{text W_Disp}.  Everything
  else --- the six transpose encoder families, the transposed run, the
  dispatch --- is reused verbatim.

  The planted ‹le› makes the wrap ∗‹not› @{const le_unique} (it writes
  ‹le› where it did not read ‹le›); it remains @{const valid_mttm}, since
  clause 1 constrains only transitions that ∗‹read› ‹le›.  The engine
  is then run from a floated-origin init config, bridged back to the
  proper @{const init_config_mttm} by the origin-float lemmas of
  @{theory Multitape_TM_Substrate.Multitape_Origin_Float}.›

subsection ‹The plant-‹le› reset done step›

text ‹Rewind-done for the plant variant: fires when the storage tape
  (index @{text "Suc 0"}) reads ‹le› (its cell 0, reached by the generic
  rewind loop), and in the same transition writes ‹le› on the input tape
  (index @{text 0}) at its current head --- the plant --- handing over to
  @{text W_Disp}.  No head moves.  This is the sole wrap-B-specific reset
  family; the loop is the generic @{const wrap_rewind_loop_delta_gen}.›

definition wrap_plant_done_delta ::
  "('q, 'b) mttm ⇒ 'a set
   ⇒ (('q, 'a, 'b) wrap_state
       × (nat ⇒ ('a, 'b) wrap_alphabet)
       × ('q, 'a, 'b) wrap_state
       × (nat ⇒ ('a, 'b) wrap_alphabet)
       × (nat ⇒ dir)) set"
where
  "wrap_plant_done_delta M Σu =
     { (W_Reset, sym, W_Disp,
        (λt. if t = 0 then Enc (le_tm M) else sym t),
        λ_. dir.N)
       | sym.
           sym (Suc 0) = Enc (le_tm M)
           ∧ (∀i≥k_tm M. sym i = Enc (bl_tm M))
           ∧ sym ∈ UNIV → Raw ` Σu ∪ Enc ` Γ_tm M }"

subsection ‹The plant-‹le› combinator›

text ‹The plant wrap's transition relation: the six transpose encoder
  families at @{term "K = k_tm M"}, the transposed run and dispatch, and
  --- for the reset --- the generic single-tape storage rewind (loop)
  plus the plant-done step.›

definition wrap_delta ::
  "('q, 'b) mttm ⇒ ('a list ⇒ 'b) ⇒ nat ⇒ 'a set
   ⇒ (('q, 'a, 'b) wrap_state
       × (nat ⇒ ('a, 'b) wrap_alphabet)
       × ('q, 'a, 'b) wrap_state
       × (nat ⇒ ('a, 'b) wrap_alphabet)
       × (nat ⇒ dir)) set"
where
  "wrap_delta M pack c Σu =
     wrap_init_delta_gen (k_tm M) M
     ∪ wrap_buf_extend_delta_gen (k_tm M) M c Σu
     ∪ wrap_buf_close_delta_gen (k_tm M) M pack c Σu
     ∪ wrap_buf_empty_end_delta_gen (k_tm M) M Σu
     ∪ wrap_buf_nonempty_end_delta_gen (k_tm M) M pack c Σu
     ∪ wrap_rewind_loop_delta_gen W_Reset (Suc 0) (k_tm M) M Σu
     ∪ wrap_plant_done_delta M Σu
     ∪ wrap_disp_delta_gen (k_tm M) M Σu
     ∪ wrap_run_delta M Σu"

text ‹The faithful ‹k›-tape plant-‹le› encoding wrap: transition relation
  @{const wrap_delta} at tape count @{term "k_tm M"}, reusing the wrap
  state set (no new state --- the plant folds into the reset-done step).
  Well-formed only when @{term "k_tm M ≥ 2"}, as for the transpose wrap.›

fun encoding_wrap ::
  "('q, 'b) mttm ⇒ ('a list ⇒ 'b) ⇒ nat ⇒ 'a set
   ⇒ (('q, 'a, 'b) wrap_state, ('a, 'b) wrap_alphabet) mttm"
where
  "encoding_wrap M pack c Σu =
     MTTM
       (wrap_state_set M c Σu)
       (Raw ` Σu)
       (Raw ` Σu ∪ Enc ` Γ_tm M)
       (Enc (bl_tm M))
       (Enc (le_tm M))
       (wrap_delta M pack c Σu)
       W_Init
       (W_Run (t_tm M))
       W_Rej
       (k_tm M)"


subsection ‹Well-formedness of the plant-‹le› wrap›

text ‹Phase-family case split for @{const wrap_delta}: a transition
  belongs to exactly one of the nine builders --- the six
  boundary-parameterised encoder families at @{term "k_tm M"}, the generic
  single-tape storage rewind loop, the plant-‹le› rewind-done step, and the
  transposed run.›

lemma wrap_delta_cases:
  assumes "(q, a, q', a', d) ∈ wrap_delta M pack c Σu"
  obtains
    (init) "(q, a, q', a', d) ∈ wrap_init_delta_gen (k_tm M) M"
  | (ext) "(q, a, q', a', d) ∈ wrap_buf_extend_delta_gen (k_tm M) M c Σu"
  | (close) "(q, a, q', a', d) ∈ wrap_buf_close_delta_gen (k_tm M) M pack c Σu"
  | (eend) "(q, a, q', a', d) ∈ wrap_buf_empty_end_delta_gen (k_tm M) M Σu"
  | (nend) "(q, a, q', a', d) ∈ wrap_buf_nonempty_end_delta_gen (k_tm M) M pack c Σu"
  | (rloop) "(q, a, q', a', d)
               ∈ wrap_rewind_loop_delta_gen W_Reset (Suc 0) (k_tm M) M Σu"
  | (rdone) "(q, a, q', a', d) ∈ wrap_plant_done_delta M Σu"
  | (disp) "(q, a, q', a', d) ∈ wrap_disp_delta_gen (k_tm M) M Σu"
  | (run) "(q, a, q', a', d) ∈ wrap_run_delta M Σu"
  using assms unfolding wrap_delta_def by blast

text ‹Obligation 1 --- well-formedness of the faithful @{text k}-tape
  plant-‹le› wrap at tape count @{term "k_tm M"}.  Hypotheses:
  @{term "2 ≤ k_tm M"}, @{term "valid_mttm M"}, and
  @{term "le_tm M ≠ bl_tm M"} (the storage rewind passes @{text bl}
  through unchanged, and the plant writes @{text le}, so the
  no-spurious-LE obligations need them distinct).  It does ∗‹not› require
  @{const le_unique} of the input, and --- crucially --- the resulting wrap
  is itself ∗‹not› @{const le_unique}: the plant-done step writes @{text le}
  on physical tape @{text 0} without reading it there.  That is legal for
  @{const valid_mttm}, whose clause 1 (obligation 14 below) constrains only
  transitions that ∗‹read› @{text le}; the dropped clause 2 was exactly the
  no-planting rule.›

lemma wrap_wf:
  assumes valM: "valid_mttm M"
      and le_ne_bl: "le_tm M ≠ bl_tm M"
      and finSu: "finite Σu"
      and c_pos: "0 < c"
      and k2: "2 ≤ k_tm M"
  shows "valid_mttm (encoding_wrap M pack c Σu)"
proof -
  have eq:
    "encoding_wrap M pack c Σu =
       MTTM (wrap_state_set M c Σu)
            (Raw ` Σu)
            (Raw ` Σu ∪ Enc ` Γ_tm M)
            (Enc (bl_tm M))
            (Enc (le_tm M))
            (wrap_delta M pack c Σu)
            W_Init
            (W_Run (t_tm M))
            W_Rej
            (k_tm M)"
    by simp
  show ?thesis
    unfolding eq valid_mttm.simps
  proof (intro conjI)
    ― ‹(1) finite Q'›
    show "finite (wrap_state_set M c Σu)"
      by (rule finite_wrap_state_set[OF valM finSu])
    ― ‹(2) finite ‹Γ›'›
    show "finite (Raw ` Σu ∪ Enc ` Γ_tm M)"
      using finSu valid_mttm_finite_Gamma[OF valM] by simp
    ― ‹(3) ‹Σ›' ‹⊆› ‹Γ›'›
    show "Raw ` Σu ⊆ Raw ` Σu ∪ Enc ` Γ_tm M"
      by blast
    ― ‹(4) start in Q'›
    show "W_Init ∈ wrap_state_set M c Σu"
      unfolding wrap_state_set_def by simp
    ― ‹(5) accept in Q'›
    show "W_Run (t_tm M) ∈ wrap_state_set M c Σu"
      using valid_mttm_t_in_Q[OF valM]
      unfolding wrap_state_set_def by simp
    ― ‹(6) reject in Q'›
    show "W_Rej ∈ wrap_state_set M c Σu"
      unfolding wrap_state_set_def by simp
    ― ‹(7a) bl in ‹Γ›'›
    show "Enc (bl_tm M) ∈ Raw ` Σu ∪ Enc ` Γ_tm M"
      using valid_mttm_blank_in_Gamma[OF valM] by blast
    ― ‹(7b) bl not in ‹Σ›'›
    show "Enc (bl_tm M) ∉ Raw ` Σu"
      by auto
    ― ‹(8a) le in ‹Γ›'›
    show "Enc (le_tm M) ∈ Raw ` Σu ∪ Enc ` Γ_tm M"
      using valid_mttm_LE_in_Gamma[OF valM] by blast
    ― ‹(8b) le not in ‹Σ›'›
    show "Enc (le_tm M) ∉ Raw ` Σu"
      by auto
    ― ‹(11) accept ‹≠› reject›
    show "W_Run (t_tm M) ≠ W_Rej"
      by simp
    ― ‹(12) ‹0 < k›: the plant wrap keeps M's tape count.›
    show "0 < k_tm M"
      using valid_mttm_k_pos[OF valM] by simp
    ― ‹(13) ‹δ›-shape: source / dest / read / write range typing.  The
       plant writes @{text "Enc le"} on tape @{text 0}, which is in range by
       @{thm valid_mttm_LE_in_Gamma}.›
    show "wrap_delta M pack c Σu
            ⊆ (wrap_state_set M c Σu - {W_Run (t_tm M), W_Rej})
              × (UNIV → Raw ` Σu ∪ Enc ` Γ_tm M)
              × wrap_state_set M c Σu
              × (UNIV → Raw ` Σu ∪ Enc ` Γ_tm M)
              × (UNIV → UNIV)"
      unfolding wrap_delta_def
                wrap_init_delta_gen_def wrap_buf_extend_delta_gen_def
                wrap_buf_close_delta_gen_def wrap_buf_empty_end_delta_gen_def
                wrap_buf_nonempty_end_delta_gen_def
                wrap_rewind_loop_delta_gen_def
                wrap_plant_done_delta_def
                wrap_disp_delta_gen_def wrap_run_delta_def
                wrap_state_set_def
      using c_pos valid_mttm_t_in_Q[OF valM] valid_mttm_s_in_Q[OF valM]
            valid_mttm_LE_in_Gamma[OF valM] valid_mttm_blank_in_Gamma[OF valM]
            valid_mttm_delta_set[OF valM]
            valid_mttm_Sigma_sub_Gamma[OF valM]
      by (fastforce split: nat.split if_splits)
    ― ‹(14) ‹δ›LE-preservation: read LE ‹⟹› write LE and dir ‹∈› {N, R}.
       The plant-done step writes LE on tape @{text 0} regardless of what it
       read there --- legal, since this obligation only fires when the read
       cell already ∗‹is› LE, and then the plant writes LE anyway.  The
       rewind loop only moves the storage head (@{text "Suc 0"}), whose
       read cannot be LE (its guard), so no LE-read cell moves.›
    show "∀q a q' a' d k.
            (q, a, q', a', d) ∈ wrap_delta M pack c Σu ⟶
            a k = Enc (le_tm M) ⟶
            a' k = Enc (le_tm M) ∧ d k ∈ {dir.N, dir.R}"
    proof (intro allI impI)
      fix q a q' a' d k
      assume in_δ: "(q, a, q', a', d) ∈ wrap_delta M pack c Σu"
         and LE: "a k = Enc (le_tm M)"
      from in_δ show "a' k = Enc (le_tm M) ∧ d k ∈ {dir.N, dir.R}"
      proof (cases rule: wrap_delta_cases)
        case init
        thus ?thesis using LE unfolding wrap_init_delta_gen_def
          by (auto split: nat.splits if_splits)
      next
        case ext
        thus ?thesis using LE unfolding wrap_buf_extend_delta_gen_def
          by (auto split: nat.splits)
      next
        case close
        thus ?thesis using LE unfolding wrap_buf_close_delta_gen_def
          by (fastforce split: nat.splits if_splits)
      next
        case eend
        thus ?thesis using LE unfolding wrap_buf_empty_end_delta_gen_def
          by (auto split: nat.splits)
      next
        case nend
        thus ?thesis using LE unfolding wrap_buf_nonempty_end_delta_gen_def
          by (fastforce split: nat.splits if_splits)
      next
        case rloop
        ― ‹Storage rewind: write = read, so LE is preserved; the only moving
           head is @{text "Suc 0"}, whose guard forbids reading LE, so a
           LE-read cell (necessarily @{text "k ≠ Suc 0"}) stays stationary.›
        thus ?thesis using LE unfolding wrap_rewind_loop_delta_gen_def
          by (auto split: if_splits)
      next
        case rdone
        ― ‹Plant-done: read = write on every tape except @{text 0}, where the
           plant writes LE; either way the write at a LE-read cell is LE, and
           no head moves.›
        thus ?thesis using LE unfolding wrap_plant_done_delta_def
          by (auto split: if_splits)
      next
        case disp
        thus ?thesis using LE unfolding wrap_disp_delta_gen_def
          by (auto split: nat.splits)
      next
        case run
        then obtain qq σ q'' σ' dd sym where
            aeq: "a = sym"
            and a'eq: "a' = (λp. Enc (σ' (wrap_tau p)))"
            and deq: "d = (λp. dd (wrap_tau p))"
            and trM: "(qq, σ, q'', σ', dd) ∈ delta_tm M"
            and symc: "∀p. sym p = Enc (σ (wrap_tau p))"
          unfolding wrap_run_delta_def by auto
        have "sym k = Enc (le_tm M)" using LE aeq by simp
        moreover have "sym k = Enc (σ (wrap_tau k))" using symc by simp
        ultimately have "σ (wrap_tau k) = le_tm M" by simp
        from valid_mttm_deltaLE[OF valM trM this]
        have "σ' (wrap_tau k) = le_tm M ∧ dd (wrap_tau k) ∈ {dir.N, dir.R}" .
        with a'eq deq show ?thesis by simp
      qed
    qed
    ― ‹(15) ‹δ›-support: beyond the tape count each transition reads and
       writes blank and is stationary.  Since ‹2 ≤ k_tm M ≤ j› we have
       ‹2 ≤ j›: the storage head @{text "Suc 0"} and the plant tape @{text 0}
       are both ‹< j›, so both reset families are blank-stationary there, and
       the run inherits @{thm valid_mttm_delta_support}.›
    show "∀q a q' a' d.
            (q, a, q', a', d) ∈ wrap_delta M pack c Σu ⟶
            (∀j ≥ k_tm M.
               a j = Enc (bl_tm M) ∧ a' j = Enc (bl_tm M) ∧ d j = dir.N)"
    proof (intro allI impI)
      fix q a q' a' d j
      assume in_δ: "(q, a, q', a', d) ∈ wrap_delta M pack c Σu"
         and jge: "k_tm M ≤ j"
      from k2 jge have j2: "2 ≤ j" by simp
      from in_δ
      show "a j = Enc (bl_tm M) ∧ a' j = Enc (bl_tm M) ∧ d j = dir.N"
      proof (cases rule: wrap_delta_cases)
        case init
        thus ?thesis using jge j2 unfolding wrap_init_delta_gen_def
          by (auto split: nat.splits if_splits)
      next
        case ext
        thus ?thesis using jge j2 unfolding wrap_buf_extend_delta_gen_def
          by (auto split: nat.splits)
      next
        case close
        thus ?thesis using jge j2 unfolding wrap_buf_close_delta_gen_def
          by (auto split: nat.splits if_splits)
      next
        case eend
        thus ?thesis using jge j2 unfolding wrap_buf_empty_end_delta_gen_def
          by (auto split: nat.splits)
      next
        case nend
        thus ?thesis using jge j2 unfolding wrap_buf_nonempty_end_delta_gen_def
          by (auto split: nat.splits if_splits)
      next
        case rloop
        thus ?thesis using jge j2 unfolding wrap_rewind_loop_delta_gen_def
          by (auto split: if_splits)
      next
        case rdone
        thus ?thesis using jge j2 unfolding wrap_plant_done_delta_def
          by (auto split: if_splits)
      next
        case disp
        thus ?thesis using jge j2 unfolding wrap_disp_delta_gen_def
          by (auto split: nat.splits)
      next
        case run
        then obtain qq σ q'' σ' dd sym where
            aeq: "a = sym"
            and a'eq: "a' = (λp. Enc (σ' (wrap_tau p)))"
            and deq: "d = (λp. dd (wrap_tau p))"
            and trM: "(qq, σ, q'', σ', dd) ∈ delta_tm M"
            and symc: "∀p. sym p = Enc (σ (wrap_tau p))"
          unfolding wrap_run_delta_def by auto
        have tauj: "wrap_tau j = j" using j2 by (rule wrap_tau_ge2_id)
        from valid_mttm_delta_support[OF valM trM jge]
        have supp: "σ j = bl_tm M ∧ σ' j = bl_tm M ∧ dd j = dir.N" .
        have "a j = Enc (bl_tm M)" using aeq symc tauj supp by simp
        moreover have "a' j = Enc (bl_tm M)" using a'eq tauj supp by simp
        moreover have "d j = dir.N" using deq tauj supp by simp
        ultimately show ?thesis by simp
      qed
    qed
  qed
qed


subsection ‹Determinism of the plant-‹le› wrap›

text ‹Obligation 4 --- determinism preservation, conditional on
  @{term "det_mttm M"}.  The encoder families and
  dispatch are functional per read pattern, and the transposed run inherits
  M-determinism through @{const wrap_tau}.  Only the @{text W_Reset} case
  differs: instead of the two combined-reset families it disambiguates the
  generic storage rewind loop from the plant-done step by their
  @{text le}-guards on the storage tape (index @{text "Suc 0"}) --- the loop
  reads a non-@{text le} there, the plant-done reads @{text le} --- each
  functional in the read.›

lemma wrap_det:
  assumes valM: "valid_mttm M"
      and detM: "det_mttm M"
      and finSu: "finite Σu"
      and c_pos: "0 < c"
  shows "det_mttm (encoding_wrap M pack c Σu)"
  unfolding det_mttm_def
proof (intro allI impI)
  fix q a p1 b1 d1 p2 b2 d2
  assume t1: "(q, a, p1, b1, d1) ∈ delta_tm (encoding_wrap M pack c Σu)"
     and t2: "(q, a, p2, b2, d2) ∈ delta_tm (encoding_wrap M pack c Σu)"
  hence t1w: "(q, a, p1, b1, d1) ∈ wrap_delta M pack c Σu"
    and t2w: "(q, a, p2, b2, d2) ∈ wrap_delta M pack c Σu"
    by simp_all
  show "(p1, b1, d1) = (p2, b2, d2)"
  proof (cases q)
    case W_Init
    with t1w t2w show ?thesis
      unfolding wrap_delta_def
                wrap_init_delta_gen_def wrap_buf_extend_delta_gen_def
                wrap_buf_close_delta_gen_def wrap_buf_empty_end_delta_gen_def
                wrap_buf_nonempty_end_delta_gen_def
                wrap_rewind_loop_delta_gen_def
                wrap_plant_done_delta_def
                wrap_disp_delta_gen_def wrap_run_delta_def
      by auto
  next
    case (W_Buf ws)
    with t1w t2w show ?thesis
      unfolding wrap_delta_def
                wrap_init_delta_gen_def wrap_buf_extend_delta_gen_def
                wrap_buf_close_delta_gen_def wrap_buf_empty_end_delta_gen_def
                wrap_buf_nonempty_end_delta_gen_def
                wrap_rewind_loop_delta_gen_def
                wrap_plant_done_delta_def
                wrap_disp_delta_gen_def wrap_run_delta_def
      by auto
  next
    case W_Reset
    ― ‹Both storage-rewind families read @{text "sym (Suc 0)"}; the loop
       fires when it is not @{text le} (looping in @{text W_Reset}, no head
       moves but @{text "Suc 0"} left), the plant-done when it is @{text le}
       (to @{text W_Disp}, planting @{text le} on tape @{text 0}).  Their
       guards are complementary, so at most one fires per read.›
    with t1w t2w show ?thesis
      unfolding wrap_delta_def
                wrap_init_delta_gen_def wrap_buf_extend_delta_gen_def
                wrap_buf_close_delta_gen_def wrap_buf_empty_end_delta_gen_def
                wrap_buf_nonempty_end_delta_gen_def
                wrap_rewind_loop_delta_gen_def
                wrap_plant_done_delta_def
                wrap_disp_delta_gen_def wrap_run_delta_def
      by (auto split: if_splits)
  next
    case W_Disp
    with t1w t2w show ?thesis
      unfolding wrap_delta_def
                wrap_init_delta_gen_def wrap_buf_extend_delta_gen_def
                wrap_buf_close_delta_gen_def wrap_buf_empty_end_delta_gen_def
                wrap_buf_nonempty_end_delta_gen_def
                wrap_rewind_loop_delta_gen_def
                wrap_plant_done_delta_def
                wrap_disp_delta_gen_def wrap_run_delta_def
      by auto
  next
    case (W_Run qM)
    ― ‹Only ‹wrap_run_delta› has a ‹W_Run› source.  Extract the M-side
       ‹δ›-tuples linked to each wrap-tuple, then use M-determinism.›
    from t1w W_Run obtain sig1 q1' sig1' dd1 where
      m1: "(qM, sig1, q1', sig1', dd1) ∈ delta_tm M"
      and sym1: "∀p. a p = Enc (sig1 (wrap_tau p))"
      and p1_eq: "p1 = W_Run q1'"
      and b1_eq: "b1 = (λp. Enc (sig1' (wrap_tau p)))"
      and d1_eq: "d1 = (λp. dd1 (wrap_tau p))"
      unfolding wrap_delta_def
                wrap_init_delta_gen_def wrap_buf_extend_delta_gen_def
                wrap_buf_close_delta_gen_def wrap_buf_empty_end_delta_gen_def
                wrap_buf_nonempty_end_delta_gen_def
                wrap_rewind_loop_delta_gen_def
                wrap_plant_done_delta_def
                wrap_disp_delta_gen_def wrap_run_delta_def
      by auto
    from t2w W_Run obtain sig2 q2' sig2' dd2 where
      m2: "(qM, sig2, q2', sig2', dd2) ∈ delta_tm M"
      and sym2: "∀p. a p = Enc (sig2 (wrap_tau p))"
      and p2_eq: "p2 = W_Run q2'"
      and b2_eq: "b2 = (λp. Enc (sig2' (wrap_tau p)))"
      and d2_eq: "d2 = (λp. dd2 (wrap_tau p))"
      unfolding wrap_delta_def
                wrap_init_delta_gen_def wrap_buf_extend_delta_gen_def
                wrap_buf_close_delta_gen_def wrap_buf_empty_end_delta_gen_def
                wrap_buf_nonempty_end_delta_gen_def
                wrap_rewind_loop_delta_gen_def
                wrap_plant_done_delta_def
                wrap_disp_delta_gen_def wrap_run_delta_def
      by auto
    have sigma_eq: "sig1 = sig2"
    proof (rule ext)
      fix x
      have e1: "a (wrap_tau x) = Enc (sig1 (wrap_tau (wrap_tau x)))"
        using sym1 by blast
      have e2: "a (wrap_tau x) = Enc (sig2 (wrap_tau (wrap_tau x)))"
        using sym2 by blast
      from e1 e2 have "sig1 (wrap_tau (wrap_tau x)) = sig2 (wrap_tau (wrap_tau x))"
        by simp
      thus "sig1 x = sig2 x" by (simp add: wrap_tau_invol)
    qed
    have M_det: "(q1', sig1', dd1) = (q2', sig2', dd2)"
      using m1 m2 sigma_eq detM[unfolded det_mttm_def] by blast
    hence q'_eq: "q1' = q2'" and sig'_eq: "sig1' = sig2'" and dd_eq: "dd1 = dd2"
      by simp_all
    show ?thesis
      using p1_eq p2_eq b1_eq b2_eq d1_eq d2_eq q'_eq sig'_eq dd_eq
      by metis
  next
    case W_Rej
    with t1w show ?thesis
      unfolding wrap_delta_def
                wrap_init_delta_gen_def wrap_buf_extend_delta_gen_def
                wrap_buf_close_delta_gen_def wrap_buf_empty_end_delta_gen_def
                wrap_buf_nonempty_end_delta_gen_def
                wrap_rewind_loop_delta_gen_def
                wrap_plant_done_delta_def
                wrap_disp_delta_gen_def wrap_run_delta_def
      by auto
  qed
qed

end