Theory Abs_Induce_S_Verification

theory Abs_Induce_S_Verification
  imports "../abs-def/Abs_SAIS"
begin

section "Abstract Induce S Simple Properties"

lemma abs_induce_s_step_ex:
  "∃B' SA' i'. abs_induce_s_step a b = (B', SA', i')"
  by (meson prod_cases3)

lemma abs_induce_s_step_B_length:
  "abs_induce_s_step (B, SA, i) (α, T) = (B', SA', i') ⟹ length B' = length B"
  by (clarsimp split: prod.splits if_splits nat.splits SL_types.splits simp: Let_def)

lemma abs_induce_s_step_SA_length:
  "abs_induce_s_step (B, SA, i) (α, T) = (B', SA', i') ⟹ length SA' = length SA"
  by (clarsimp split: prod.splits if_splits nat.splits SL_types.splits simp: Let_def)

lemma abs_induce_s_step_Suc:
  "abs_induce_s_step (B, SA, Suc i) (α, T) = (B', SA', i') ⟹ i' = i"
  by (clarsimp split: prod.splits if_splits nat.splits SL_types.splits simp: Let_def)

lemma abs_induce_s_step_0:
  "abs_induce_s_step (B, SA, 0) (α, T) = (B, SA, 0)"
  by (clarsimp split: prod.splits if_splits nat.splits SL_types.splits simp: Let_def)

corollary abs_induce_s_step_0_alt:
  assumes "abs_induce_s_step (B, SA, i) (α, T) = (B', SA', i')"
  and     "i = 0"
shows "B = B' ∧ SA = SA' ∧ i' = 0"
  using assms(1) assms(2) by auto

lemma repeat_abs_induce_s_step_index:
  "∃B' SA'. repeat n abs_induce_s_step (B, SA, m) (α, T) = (B', SA', m - n) ∧
            length SA' = length SA ∧ length B' = length B"
proof(induct n arbitrary: m)
  case 0
  then show ?case by (clarsimp simp: repeat_0)
next
  case (Suc n)
  note IH = this

  from IH[of m]
  obtain B' SA' where
    "repeat n abs_induce_s_step (B, SA, m) (α, T) = (B', SA', m - n)"
    "length SA' = length SA"
    "length B' = length B"
    by blast
  with repeat_step[of n abs_induce_s_step "(B, SA, m)" "(α, T)"]
  have "repeat (Suc n) abs_induce_s_step (B, SA, m) (α, T) = abs_induce_s_step (B', SA', m - n) (α, T)"
    by simp
  moreover
  have "∃B'' SA''. abs_induce_s_step (B', SA', m - n) (α, T) = (B'', SA'', m - Suc n) ∧
                   length SA'' = length SA' ∧ length B'' = length B'"
  proof (cases "n < m")
    assume "n < m"
    hence "∃k. m - n = Suc k"
      by presburger
    then obtain k where
      "m - n = Suc k"
      by blast

    from abs_induce_s_step_ex[of "(B',SA', m - n)" "(α, T)"]
    obtain B'' SA'' i' where
      P: "abs_induce_s_step (B', SA', m - n) (α, T) = (B'', SA'', i')"
      by blast
    with `m - n = Suc k` abs_induce_s_step_Suc[of B' SA' k α T B'' SA'' i']
    have "i' = m - Suc n"
      by auto
    with `abs_induce_s_step (B', SA', m - n) (α, T) = (B'', SA'', i')`
          abs_induce_s_step_SA_length[OF P]
          abs_induce_s_step_B_length[OF P]
    show ?thesis
      by simp
  next
    assume "¬n < m"
    hence "m ≤ n"
      by simp
    hence "m - n = 0"
      by simp
    with abs_induce_s_step_0[of B' SA' α T]
    show ?thesis
      by simp
  qed
  ultimately show ?case
    by (simp add: `length SA' = length SA` `length B' = length B`)
qed

lemma abs_induce_s_base_index:
  "∃B' SA'. abs_induce_s_base α T B SA = (B', SA', 0)"
  unfolding abs_induce_s_base_def
  by (metis cancel_comm_monoid_add_class.diff_cancel repeat_abs_induce_s_step_index)

lemma abs_induce_s_length:
  "length (abs_induce_s α T B SA) = length SA"
  unfolding abs_induce_s_def abs_induce_s_base_def
  apply (rule repeat_maintain_inv; simp add: Let_def)
  apply (clarsimp split: prod.splits simp del: abs_induce_s_step.simps)
  apply (drule abs_induce_s_step_SA_length; simp)
  done

section "Preconditions"

definition l_types_init
  where
"l_types_init α T SA ≡
  (∀b ≤ α (Max (set T)).
    set (list_slice SA (bucket_start α T b) (l_bucket_end α T b)) = l_bucket α T b ∧
    distinct (list_slice SA (bucket_start α T b) (l_bucket_end α T b))
  )"

lemma l_types_initD:
  "⟦l_types_init α T SA; b ≤ α (Max (set T))⟧ ⟹
   set (list_slice SA (bucket_start α T b) (l_bucket_end α T b)) = l_bucket α T b"
  "⟦l_types_init α T SA; b ≤ α (Max (set T))⟧ ⟹
   distinct (list_slice SA (bucket_start α T b) (l_bucket_end α T b))"
  using l_types_init_def by blast+

lemma l_types_init_nth:
  assumes "length SA = length T"
  and     "l_types_init α T SA"
  and     "b ≤ α (Max (set T))"
  and     "bucket_start α T b ≤ i"
  and     "i < l_bucket_end α T b"
shows "SA ! i ∈ l_bucket α T b"
proof -
  have "l_bucket_end α T b ≤ length SA"
    by (metis assms(1) bucket_end_le_length dual_order.order_iff_strict l_bucket_end_le_bucket_end
              less_le_trans)
  with l_types_initD(1)[OF assms(2,3)] list_slice_nth_mem[OF assms(4,5)]
  show ?thesis
    by blast
qed

definition s_type_init
  where
"s_type_init T SA ≡ (∃n. length T = Suc n ∧ SA ! 0 = n)"

definition s_perm_pre
  where
"s_perm_pre α T B SA n ≡
  s_bucket_init α T B ∧
  s_type_init T SA ∧
  strict_mono α ∧
  α (Max (set T)) < length B ∧
  length SA = length T ∧
  l_types_init α T SA ∧
  valid_list T ∧
  α bot = 0 ∧
  Suc 0 < length T ∧
  length T ≤ n"

definition s_sorted_pre
  where
"s_sorted_pre α T SA ≡
  (∀b ≤ α (Max (set T)).
    ordlistns.sorted (map (suffix T) (list_slice SA (bucket_start α T b) (l_bucket_end α T b)))
  )"

lemma s_sorted_preD:
  "⟦s_sorted_pre α T SA; b ≤ α (Max (set T))⟧ ⟹
   ordlistns.sorted (map (suffix T) (list_slice SA (bucket_start α T b) (l_bucket_end α T b)))"
  using s_sorted_pre_def by blast

definition s_prefix_sorted_pre
  where
"s_prefix_sorted_pre α T SA ≡
  (∀b ≤ α (Max (set T)).
    ordlistns.sorted (map (lms_slice T) (list_slice SA (bucket_start α T b) (l_bucket_end α T b)))
  )"

lemma s_prefix_sorted_preD:
  "⟦s_prefix_sorted_pre α T SA; b ≤ α (Max (set T))⟧ ⟹
   ordlistns.sorted (map (lms_slice T) (list_slice SA (bucket_start α T b) (l_bucket_end α T b)))"
  using s_prefix_sorted_pre_def by blast

section "Invariants"

subsection "Definitions"

subsubsection "Distinctness"

definition s_distinct_inv
  where
"s_distinct_inv α T B SA ≡
  (∀b ≤ α (Max (set T)). distinct (list_slice SA (B ! b) (bucket_end α T b)))"

lemma s_distinct_invD:
  "⟦s_distinct_inv α T B SA; b ≤ α (Max (set T))⟧ ⟹
   distinct (list_slice SA (B ! b) (bucket_end α T b))"
  using s_distinct_inv_def by blast

subsubsection "S Bucket Ptr"

definition s_bucket_ptr_inv ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ bool"
  where
"s_bucket_ptr_inv α T B ≡
  (∀b ≤ α (Max (set T)).
    s_bucket_start α T b ≤ B ! b ∧
    B ! b ≤ bucket_end α T b ∧
    (b = 0 ⟶ B ! b = 0))"

lemma s_bucket_ptr_lower_bound:
  assumes "s_bucket_ptr_inv α T B"
  and     "b ≤ α (Max (set T))"
shows "s_bucket_start α T b ≤ B ! b"
  using assms(1) assms(2) s_bucket_ptr_inv_def by blast

lemma s_bucket_ptr_upper_bound:
  assumes "s_bucket_ptr_inv α T B"
  and     "b ≤ α (Max (set T))"
shows "B ! b ≤ bucket_end α T b"
  by (metis assms s_bucket_ptr_inv_def)

lemma s_bucket_ptr_0:
  assumes "s_bucket_ptr_inv α T B"
  and     "b = 0"
shows "B ! b = 0"
  using assms s_bucket_ptr_inv_def by auto

subsubsection "Locations"

definition s_locations_inv ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ bool"
  where
"s_locations_inv α T B SA ≡
  (∀b ≤ α (Max (set T)).
    (∀i. B ! b ≤ i ∧ i < bucket_end α T b ⟶ SA ! i ∈ s_bucket α T b))"

lemma s_locations_invD:
  "⟦s_locations_inv α T B SA; b ≤ α (Max (set T)); B ! b ≤ i; i < bucket_end α T b⟧ ⟹
   SA ! i ∈ s_bucket α T b"
  using s_locations_inv_def by blast

lemma s_locations_inv_in_list_slice:
  assumes "s_locations_inv α T B SA"
  and     "b ≤ α (Max (set T))"
  and     "x ∈ set (list_slice SA (B ! b) (bucket_end α T b))"
shows "x ∈ s_bucket α T b"
proof -
  from in_set_conv_nth[THEN iffD1, OF assms(3)]
  obtain i where
    "i < length (list_slice SA (B ! b) (bucket_end α T b))"
    "list_slice SA (B ! b) (bucket_end α T b) ! i = x"
    by blast
  with nth_list_slice
  have "SA ! (B ! b + i) = x"
    by fastforce
  moreover
  have "B ! b + i < bucket_end α T b"
    using ‹i < length (list_slice SA (B ! b) (bucket_end α T b))› by auto
  ultimately
  show ?thesis
    using assms(1,2) le_add1 s_locations_invD by blast
qed

lemma s_locations_inv_subset_s_bucket:
  assumes "s_locations_inv α T B SA"
  and     "b ≤ α (Max (set T))"
shows "set (list_slice SA (B ! b) (bucket_end α T b)) ⊆ s_bucket α T b"
  using assms s_locations_inv_in_list_slice by blast

subsubsection "Unchanged"

definition s_unchanged_inv ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ nat list ⇒ bool"
  where
"s_unchanged_inv α T B SA SA' ≡
  (∀b ≤ α (Max (set T)). (∀i. bucket_start α T b ≤ i ∧ i < B ! b ⟶  SA' ! i = SA ! i))"

lemma s_unchanged_invD:
  "⟦s_unchanged_inv α T B SA SA'; b ≤ α (Max (set T)); bucket_start α T b ≤ i; i < B ! b⟧ ⟹
   SA' ! i = SA ! i"
  using s_unchanged_inv_def by blast

subsubsection "Seen"

definition s_seen_inv ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ nat ⇒ bool"
  where
"s_seen_inv α T B SA n ≡
  ∀i < length SA. n ≤ i ⟶
    (suffix_type T (SA ! i) = S_type ⟶ in_s_current_bucket α T B (α (T ! (SA ! i))) i) ∧
    (suffix_type T (SA ! i) = L_type ⟶ in_l_bucket α T (α (T ! (SA ! i))) i) ∧
    SA ! i < length T"

lemma s_seen_invD:
  "⟦s_seen_inv α T B SA n; i < length SA; n ≤ i⟧ ⟹ SA ! i < length T"
  "⟦s_seen_inv α T B SA n; i < length SA; n ≤ i; suffix_type T (SA ! i) = L_type⟧ ⟹
   in_l_bucket α T (α (T ! (SA ! i))) i"
  "⟦s_seen_inv α T B SA n; i < length SA; n ≤ i; suffix_type T (SA ! i) = S_type⟧ ⟹
   in_s_current_bucket α T B (α (T ! (SA ! i))) i"
  unfolding s_seen_inv_def by blast+

subsubsection "Predecessor"

definition s_pred_inv ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ nat ⇒ bool"
  where
"s_pred_inv α T B SA n =
  (∀b i. in_s_current_bucket α T B b i ∧ b ≠ 0 ⟶
    (∃j < length SA. SA ! j = Suc (SA ! i) ∧ i < j ∧ n < j)
  )"

lemma s_pred_invD:
  "⟦s_pred_inv α T B SA k; in_s_current_bucket α T B b i; b ≠ 0⟧ ⟹
   ∃j < length SA. SA ! j = Suc (SA ! i) ∧ i < j ∧ k < j"
  using s_pred_inv_def by blast

subsubsection "Successor"

definition s_suc_inv ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ nat ⇒ bool"
  where
"s_suc_inv α T B SA n ≡
  ∀i < length SA. n < i ⟶
    (∀j. SA ! i = Suc j ∧ suffix_type T j = S_type ⟶
      (∃k. in_s_current_bucket α T B (α (T ! j)) k ∧ SA ! k = j ∧ k < i))"

lemma s_suc_invD:
  "⟦s_suc_inv α T B SA n; i < length SA; n < i; SA ! i = Suc j; suffix_type T j = S_type⟧ ⟹
   ∃k. in_s_current_bucket α T B (α (T ! j)) k ∧ SA ! k = j ∧ k < i"
  using s_suc_inv_def by blast

subsubsection "Combined Permutation Invariant"

definition s_perm_inv ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ nat list ⇒ nat ⇒ bool"
  where
"s_perm_inv α T B SA SA' n ≡
  s_distinct_inv α T B SA' ∧
  s_bucket_ptr_inv α T B ∧
  s_locations_inv α T B SA' ∧
  s_unchanged_inv α T B SA SA' ∧
  s_seen_inv α T B SA' n ∧
  s_pred_inv α T B SA' n ∧
  s_suc_inv α T B SA' n ∧
  strict_mono α ∧
  α (Max (set T)) < length B ∧
  length SA = length T ∧
  length SA' = length T ∧
  l_types_init α T SA ∧
  valid_list T ∧
  α bot = 0 ∧
  Suc 0 < length T"

lemma s_perm_inv_elims:
  "s_perm_inv α T B SA SA' n ⟹ s_distinct_inv α T B SA'"
  "s_perm_inv α T B SA SA' n ⟹ s_bucket_ptr_inv α T B"
  "s_perm_inv α T B SA SA' n ⟹ s_locations_inv α T B SA'"
  "s_perm_inv α T B SA SA' n ⟹ s_unchanged_inv α T B SA SA'"
  "s_perm_inv α T B SA SA' n ⟹ s_seen_inv α T B SA' n"
  "s_perm_inv α T B SA SA' n ⟹ s_pred_inv α T B SA' n"
  "s_perm_inv α T B SA SA' n ⟹ s_suc_inv α T B SA' n"
  "s_perm_inv α T B SA SA' n ⟹ strict_mono α"
  "s_perm_inv α T B SA SA' n ⟹ α (Max (set T)) < length B"
  "s_perm_inv α T B SA SA' n ⟹ length SA = length T"
  "s_perm_inv α T B SA SA' n ⟹ length SA' = length T"
  "s_perm_inv α T B SA SA' n ⟹ l_types_init α T SA"
  "s_perm_inv α T B SA SA' n ⟹ valid_list T"
  "s_perm_inv α T B SA SA' n ⟹ α bot = 0"
  "s_perm_inv α T B SA SA' n ⟹ Suc 0 < length T"
  by (simp_all add: s_perm_inv_def)

fun s_perm_inv_alt ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list × nat list × nat ⇒ bool"
  where
"s_perm_inv_alt α T SA (B, SA', n) = s_perm_inv α T B SA SA' n"

subsubsection "Sorted"

definition s_sorted_inv
  where
"s_sorted_inv α T B SA ≡
  (∀b ≤ α (Max (set T)).
    ordlistns.sorted (map (suffix T) (list_slice SA (B ! b) (bucket_end α T b)))
  )"

lemma s_sorted_invD:
  "⟦s_sorted_inv α T B SA; b ≤ α (Max (set T))⟧ ⟹
   ordlistns.sorted (map (suffix T) (list_slice SA (B ! b) (bucket_end α T b)))"
  using s_sorted_inv_def by blast

fun s_sorted_inv_alt ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list × nat list × nat ⇒ bool"
  where
"s_sorted_inv_alt α T SA (B, SA', n) =
  (s_perm_inv α T B SA SA' n ∧ s_sorted_pre α T SA ∧ s_sorted_inv α T B SA')"

definition s_prefix_sorted_inv
  where
"s_prefix_sorted_inv α T B SA ≡
  (∀b ≤ α (Max (set T)).
    ordlistns.sorted (map (lms_slice T) (list_slice SA (B ! b) (bucket_end α T b)))
  )"

lemma s_prefix_sorted_invD:
  "⟦s_prefix_sorted_inv α T B SA; b ≤ α (Max (set T))⟧ ⟹
   ordlistns.sorted (map (lms_slice T) (list_slice SA (B ! b) (bucket_end α T b)))"
  using s_prefix_sorted_inv_def by blast

fun s_prefix_sorted_inv_alt ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list × nat list × nat ⇒ bool"
  where
"s_prefix_sorted_inv_alt α T SA (B, SA', n) =
  (s_perm_inv α T B SA SA' n ∧ s_prefix_sorted_pre α T SA ∧ s_prefix_sorted_inv α T B SA')"

subsection "Helpers"

lemma s_current_bucket_pairwise_distinct:
  assumes "s_distinct_inv α T B SA"
  and     "s_locations_inv α T B SA"
  and     "b ≤ α (Max (set T))"
  and     "b' ≤ α (Max (set T))"
  and     "b ≠ b'"
shows "distinct (list_slice SA (B ! b) (bucket_end α T b) @ list_slice SA (B ! b') (bucket_end α T b'))"
proof (intro distinct_append[THEN iffD2] conjI disjointI')
  from s_distinct_invD[OF assms(1,3)]
  show "distinct (list_slice SA (B ! b) (bucket_end α T b))" .
next
  from s_distinct_invD[OF assms(1,4)]
  show "distinct (list_slice SA (B ! b') (bucket_end α T b'))" .
next
  fix x y
  assume A: "x ∈ set (list_slice SA (B ! b) (bucket_end α T b))"
            "y ∈ set (list_slice SA (B ! b') (bucket_end α T b'))"

  from s_locations_inv_in_list_slice[OF assms(2,3) A(1)]
  have "x ∈ s_bucket α T b" .
  moreover
  from s_locations_inv_in_list_slice[OF assms(2,4) A(2)]
  have "y ∈ s_bucket α T b'" .
  ultimately
  show "x ≠ y"
    using assms(5)
    by (metis (mono_tags, lifting) bucket_def s_bucket_def mem_Collect_eq)
qed

lemma s_unchanged_list_slice:
  assumes "s_unchanged_inv α T B SA0 SA"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "b ≤ α (Max (set T))"
  and     "bucket_start α T b ≤ i"
  and     "j ≤ B ! b"
shows "list_slice SA i j = list_slice SA0 i j"
proof (intro list_eq_iff_nth_eq[THEN iffD2] conjI allI impI)
  show "length (list_slice SA i j) = length (list_slice SA0 i j)"
    by (simp add: assms)
next
  fix k
  assume "k < length (list_slice SA i j)"
  hence "k < length (list_slice SA0 i j)"
    by (simp add: assms)

  from nth_list_slice[OF `k < length (list_slice SA i j)`]
  have "list_slice SA i j ! k = SA ! (i + k)" .
  moreover
  from nth_list_slice[OF `k < length (list_slice SA0 i j)`]
  have "list_slice SA0 i j ! k = SA0 ! (i + k)" .
  moreover
  {
    have "bucket_start α T b ≤ i + k"
      by (simp add: assms(5) trans_le_add1)
    moreover
    have "i + k < j"
      using ‹k < length (list_slice SA i j)› by auto
    hence "i + k < B ! b"
      using assms(6) order.strict_trans2 by blast
    ultimately
    have "SA ! (i + k) = SA0 ! (i + k)"
      using s_unchanged_invD[OF assms(1,4)]
      by blast
  }
  ultimately show "list_slice SA i j ! k = list_slice SA0 i j ! k"
    by simp
qed

lemma l_types_init_maintained:
  assumes "s_bucket_ptr_inv α T B"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
shows "l_types_init α T SA"
  unfolding l_types_init_def
proof(intro allI impI)
  fix b
  let ?xs = "list_slice SA (bucket_start α T b) (l_bucket_end α T b)"
  let ?ys = "list_slice SA0 (bucket_start α T b) (l_bucket_end α T b)"
  assume "b ≤ α (Max (set T))"
  with s_bucket_ptr_lower_bound[OF assms(1), of b]
  have "l_bucket_end α T b ≤ B ! b"
    by (simp add: s_bucket_start_eq_l_bucket_end)
  with s_unchanged_list_slice[OF assms(2-4) `b ≤ α (Max (set T))`,
        of "bucket_start α T b" "l_bucket_end α T b"]
  have "?xs = ?ys"
    by blast
  with assms(5)[simplified l_types_init_def, THEN spec, THEN mp, OF `b ≤ α (Max (set T))`]
  show "set ?xs = l_bucket α T b ∧ distinct ?xs"
    by simp
qed

lemma s_sorted_pre_maintained:
  assumes "s_bucket_ptr_inv α T B"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "s_sorted_pre α T SA0"
shows "s_sorted_pre α T SA"
  unfolding s_sorted_pre_def
proof(intro allI impI)
  fix b
  let ?xs = "list_slice SA (bucket_start α T b) (l_bucket_end α T b)"
  let ?ys = "list_slice SA0 (bucket_start α T b) (l_bucket_end α T b)"
  assume "b ≤ α (Max (set T))"
  with s_bucket_ptr_lower_bound[OF assms(1), of b]
  have "l_bucket_end α T b ≤ B ! b"
    by (simp add: s_bucket_start_eq_l_bucket_end)
  with s_unchanged_list_slice[OF assms(2-4) `b ≤ α (Max (set T))`,
        of "bucket_start α T b" "l_bucket_end α T b"]
  have "?xs = ?ys"
    by blast
  then show "ordlistns.sorted (map (suffix T) ?xs)"
    using ‹b ≤ α (Max (set T))› assms(5) s_sorted_pre_def by auto
qed

lemma s_prefix_sorted_pre_maintained:
  assumes "s_bucket_ptr_inv α T B"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "s_prefix_sorted_pre α T SA0"
shows "s_prefix_sorted_pre α T SA"
  unfolding s_prefix_sorted_pre_def
proof(intro allI impI)
  fix b
  let ?xs = "list_slice SA (bucket_start α T b) (l_bucket_end α T b)"
  let ?ys = "list_slice SA0 (bucket_start α T b) (l_bucket_end α T b)"
  assume "b ≤ α (Max (set T))"
  with s_bucket_ptr_lower_bound[OF assms(1), of b]
  have "l_bucket_end α T b ≤ B ! b"
    by (simp add: s_bucket_start_eq_l_bucket_end)
  with s_unchanged_list_slice[OF assms(2-4) `b ≤ α (Max (set T))`,
        of "bucket_start α T b" "l_bucket_end α T b"]
  have "?xs = ?ys"
    by blast
  then show "ordlistns.sorted (map (lms_slice T) ?xs)"
    using ‹b ≤ α (Max (set T))› assms(5) s_prefix_sorted_pre_def by auto
qed

lemma s_next_item_not_seen:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "strict_mono α"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
shows "j ∉ set (list_slice SA (B ! b) (bucket_end α T b))"
proof
  let ?xs = "list_slice SA (B ! b) (bucket_end α T b)"
  let ?b = "α (T ! (Suc j))"
  assume "j ∈ set ?xs"

  from s_seen_invD(1)[OF assms(5,14)] assms(13,15)
  have "Suc j < length T"
    by simp
  hence "?b ≤ α (Max (set T))"
    using assms(7)
    by (simp add: strict_mono_leD)

  have "bucket_end α T ?b ≤ length SA"
    by (simp add: assms(9) bucket_end_le_length)
  hence "l_bucket_end α T ?b ≤ length SA"
    by (metis dual_order.trans l_bucket_end_le_bucket_end)

  have "j < length T"
    by (simp add: assms(16) suffix_type_s_bound)

  from valid_list_length_ex[OF assms(11)]
  obtain n' where
    "length T = Suc n'"
    by blast
  with `Suc j < length T`
  have "j < n'"
    by linarith
  hence "T ! j ≠ bot"
    by (metis ‹length T = Suc n'› assms(11) diff_Suc_1 valid_list_def)
  hence "b ≠ 0"
    using assms(7,12,17) strict_mono_eq by fastforce

  with in_set_conv_nth[THEN iffD1, OF `j ∈ set ?xs`]
  obtain a where
    "a < length ?xs"
    "?xs ! a = j"
    by blast
  hence "SA ! (B ! b + a) = j"
    using nth_list_slice by fastforce

  from assms(9)
  have "bucket_end α T b ≤ length SA"
    by (simp add: bucket_end_le_length)
  with `a < length ?xs`
  have "B ! b + a < bucket_end α T b"
    by auto
  with assms(7,17) `j < length T`
  have "in_s_current_bucket α T B b (B ! b + a)"
    unfolding in_s_current_bucket_def
    by (simp add: strict_mono_less_eq)
  with s_pred_invD[OF assms(6) _ `b ≠ 0`, of "B ! b + a"] `SA ! (B ! b + a) = j`
  obtain m where
    "m < length SA"
    "SA ! m = Suc j"
    "B ! b + a < m"
    "i < m"
    by blast
  hence "i ≠ m"
    by blast

  have "suffix_type T (Suc j) = L_type ⟹ False"
  proof -
    assume "suffix_type T (Suc j) = L_type"
    with s_seen_invD(2)[OF assms(5) `m < length SA`] `i < m` `SA ! m = Suc j`
    have "in_l_bucket α T ?b m"
      by simp
    hence "bucket_start α T ?b ≤ m" "m < l_bucket_end α T ?b"
      using in_l_bucket_def by blast+
    moreover
    from `suffix_type T (Suc j) = L_type` assms(13,15)
         s_seen_invD(2)[OF assms(5) `Suc n < length SA`]
    have "in_l_bucket α T ?b i"
      by simp
    hence "bucket_start α T ?b ≤ i" "i < l_bucket_end α T ?b"
      using in_l_bucket_def by blast+
    ultimately
    show "False"
      using list_slice_nth_eq_iff_index_eq[
              OF l_types_initD(2)[OF l_types_init_maintained[OF assms(2,4,8-10)] `?b ≤ α _`]
                `l_bucket_end α T ?b ≤ length SA`,
              of i m]
            `i ≠ m` assms(13,15) `SA ! m = Suc j`
      by simp
  qed
  moreover
  have "suffix_type T (Suc j) = S_type ⟹ False"
  proof -
    assume "suffix_type T (Suc j) = S_type"
    with s_seen_invD(3)[OF assms(5) `m < length SA`] `i < m` `SA ! m = Suc j`
    have "in_s_current_bucket α T B ?b m"
      by simp
    hence "B ! ?b ≤ m" "m < bucket_end α T ?b"
      using in_s_current_bucket_def by blast+
    moreover
    from `suffix_type T (Suc j) = S_type` assms(13,15)
         s_seen_invD(3)[OF assms(5) `Suc n < length SA`]
    have "in_s_current_bucket α T B ?b i"
      by simp
    hence "B ! ?b ≤ i" "i < bucket_end α T ?b"
      using in_s_current_bucket_def by blast+
    ultimately
    show False
      using list_slice_nth_eq_iff_index_eq[
              OF s_distinct_invD[OF assms(1) `?b ≤ α _`] `bucket_end α T ?b ≤ length SA`,
              of i m]
            `i ≠ m` assms(13,15) `SA ! m = Suc j`
      by simp
  qed
  ultimately
  show False
    using SL_types.exhaust by blast
qed

lemma s_bucket_ptr_strict_lower_bound:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "strict_mono α"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
shows "s_bucket_start α T b < B ! b"
proof -
  have "j < length T"
    by (simp add: assms(16) suffix_type_s_bound)
  hence "b ≤ α (Max (set T))"
    by (simp add: assms(7,17) strict_mono_leD)

  let ?xs = "list_slice SA (B ! b) (bucket_end α T b)"

  have "bucket_end α T b ≤ length SA"
    by (simp add: assms(9) bucket_end_le_length)
  hence "length ?xs = bucket_end α T b - B ! b"
    by auto

  from s_next_item_not_seen[OF assms(1-17)]
  have "j ∉ set ?xs" .
  moreover
  have "j ∈ s_bucket α T b"
    by (simp add: assms(16,17) bucket_def s_bucket_def suffix_type_s_bound)
  ultimately
  have "set ?xs ⊂ s_bucket α T b"
    using s_locations_inv_subset_s_bucket[OF assms(3) `b ≤ _`]
    by blast
  hence "card (set ?xs) < s_bucket_size α T b"
    using psubset_card_mono[OF finite_s_bucket, simplified s_bucket_size_def[symmetric]]
    by blast
  moreover
  from s_distinct_invD[OF assms(1) `b ≤ _`]
  have "distinct ?xs" .
  ultimately
  have "length ?xs < s_bucket_size α T b"
    by (simp add: distinct_card)
  with `length ?xs = _`
  have "bucket_end α T b - B ! b < s_bucket_size α T b"
    by simp
  hence "bucket_end α T b < B ! b + s_bucket_size α T b"
    by linarith
  hence
    "s_bucket_start α T b + bucket_end α T b < B ! b + s_bucket_start α T b + s_bucket_size α T b"
    by simp
  then show "s_bucket_start α T b < B ! b"
    by (simp add: bucket_end_eq_s_start_pl_size)
qed

lemma outside_another_bucket:
  assumes "b ≠ b'"
  and     "bucket_start α T b ≤ i"
  and     "i < bucket_end α T b"
shows "¬(bucket_start α T b' ≤ i ∧ i < bucket_end α T b')"
  by (meson assms dual_order.antisym less_bucket_end_le_start not_le order.strict_trans1)

lemma s_B_val:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "strict_mono α"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "length T > Suc 0"
  and     "b ≤ α (Max (set T))"
  and     "i < B ! b"
shows "B ! b = s_bucket_start α T b"
proof (rule ccontr; drule neq_iff[THEN iffD1]; elim disjE)
  assume "B ! b < s_bucket_start α T b"
  with s_bucket_ptr_lower_bound[OF assms(2,13)]
  show False
    by linarith
next
  let ?k = "B ! b - Suc 0"
  assume "s_bucket_start α T b < B ! b"
  hence "s_bucket_start α T b ≤ ?k"
    by linarith
  hence "bucket_start α T b ≤ ?k"
    using bucket_start_le_s_bucket_start le_trans by blast

  have "?k < B ! b"
    using `s_bucket_start α T b < B ! b` by auto

  from assms(14)
  have "i ≤ ?k"
    by linarith

  from s_bucket_ptr_upper_bound[OF assms(2,13)]
  have "B ! b ≤ bucket_end α T b" .
  hence "?k < bucket_end α T b"
    using ‹s_bucket_start α T b < B ! b› by linarith

  have "bucket_end α T b ≤ length SA"
    by (simp add: assms(9) bucket_end_le_length)
  moreover
  have "bucket_end α T b = length SA ⟹ False"
  proof -
    assume "bucket_end α T b = length SA"
    with `s_bucket_start α T b < B ! b` `B ! b ≤ bucket_end α T b` assms(7,9,13)
    have "b = α (Max (set T))"
      using bucket_end_eq_length by fastforce
    hence "s_bucket α T b = {}"
      by (simp add: assms(7,11,12) s_bucket_Max)
    hence "s_bucket_size α T b = 0"
      by (simp add: s_bucket_size_def)
    hence "s_bucket_start α T b = bucket_end α T b"
      by (simp add: bucket_end_eq_s_start_pl_size)
    with `B ! b ≤ bucket_end α T b` `s_bucket_start α T b < B ! b`
    show False
      by simp
  qed
  moreover
  have "bucket_end α T b < length SA ⟹ False"
  proof -
    assume "bucket_end α T b < length SA"
    hence "B ! b < length SA"
      using `B ! b ≤ bucket_end α T b`
      by linarith
    hence "?k < length SA"
      using less_imp_diff_less by blast
    with s_seen_invD[OF assms(5) _  `i ≤ ?k`]
    have "SA ! ?k < length T"
      by blast

    let ?b = "α (T ! (SA ! ?k))"

    from `SA ! ?k < length T` assms(7)
    have "?b ≤ α (Max (set T))"
      using Max_greD strict_mono_leD by blast
    with s_bucket_ptr_lower_bound[OF assms(2)]
    have "s_bucket_start α T ?b ≤ B ! ?b"
      by blast
    hence "bucket_start α T ?b ≤ B ! ?b"
      using bucket_start_le_s_bucket_start le_trans by blast

    have "suffix_type T (SA ! ?k) = L_type ⟹ False"
    proof -
      assume "suffix_type T (SA ! ?k) = L_type"
      with s_seen_invD(2)[OF assms(5) `?k < length SA` `i ≤ ?k`]
      have "in_l_bucket α T ?b ?k"
        by blast
      hence "bucket_start α T ?b ≤ ?k" "?k < l_bucket_end α T ?b"
        using in_l_bucket_def by blast+
      hence "?k < bucket_end α T ?b"
        using l_bucket_end_le_bucket_end less_le_trans by blast

      from `?k < l_bucket_end _ _ _` `s_bucket_start _ _ _ ≤ ?k`
      have "b = ?b ⟹ False"
        by (simp add: s_bucket_start_eq_l_bucket_end)
      moreover
      from outside_another_bucket[OF _ `bucket_start _ _ b ≤ ?k` `?k < bucket_end _ _ b`]
           `bucket_start _ _ ?b ≤ ?k` `?k < bucket_end _ _ ?b`
      have "b ≠ ?b ⟹ False"
        by blast
      ultimately show False
        by blast
    qed
    moreover
    have "suffix_type T (SA ! ?k) = S_type ⟹ False"
    proof -
      assume "suffix_type T (SA ! ?k) = S_type"
      with s_seen_invD(3)[OF assms(5) `?k < length SA` `i ≤ ?k`]
      have "in_s_current_bucket α T B ?b ?k "
        by blast
      hence "B ! ?b ≤ ?k" "?k < bucket_end α T ?b"
        using in_s_current_bucket_def by blast+
      hence "bucket_start α T ?b ≤ ?k"
        using `bucket_start α T ?b ≤ B ! ?b` by linarith

      from `B ! ?b ≤ ?k` `?k < B ! b`
      have "b = ?b ⟹ False"
        by simp
      moreover
      from outside_another_bucket[OF _ `bucket_start _ _ b ≤ ?k` `?k < bucket_end _ _ b`]
           `bucket_start α T ?b ≤ ?k` `?k < bucket_end α T ?b`
      have "b ≠ ?b ⟹ False"
        by blast
      ultimately show False
        by blast
    qed
    ultimately show False
      using SL_types.exhaust by blast
  qed
  ultimately show False
    by linarith
qed

lemma s_bucket_eq_list_slice:
  assumes "s_distinct_inv α T B SA"
  and     "s_locations_inv α T B SA"
  and     "length SA = length T"
  and     "b ≤ α (Max (set T))"
  and     "B ! b = s_bucket_start α T b"
shows "set (list_slice SA (s_bucket_start α T b) (bucket_end α T b)) = s_bucket α T b"
      (is "set ?xs = s_bucket α T b")
  using card_subset_eq[
          OF finite_s_bucket s_locations_inv_subset_s_bucket[OF assms(2,4), simplified assms(5)]]
        distinct_card[OF s_distinct_invD[OF assms(1,4), simplified assms(5)]]
        bucket_end_eq_s_start_pl_size[of α T b]
        s_bucket_size_def[of α T b]
  by (metis assms(3) bucket_end_le_length diff_add_inverse length_list_slice min_def)

lemma bucket_eq_list_slice:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "b ≤ α (Max (set T))"
  and     "B ! b = s_bucket_start α T b"
shows "set (list_slice SA (bucket_start α T b) (bucket_end α T b)) = bucket α T b"
      (is "set ?xs = bucket α T b")
proof -
  let ?ys = "list_slice SA (bucket_start α T b) (l_bucket_end α T b)"
  and ?zs = "list_slice SA (s_bucket_start α T b) (bucket_end α T b)"

  have "?xs = ?ys @ ?zs"
    by (metis list_slice_append bucket_start_le_s_bucket_start l_bucket_end_le_bucket_end
          s_bucket_start_eq_l_bucket_end)
  hence "set ?xs = set ?ys ∪ set ?zs"
    by simp
  with l_types_initD(1)[OF l_types_init_maintained[OF assms(2,4-7)] assms(8)]
       s_bucket_eq_list_slice[OF assms(1,3,6,8,9)]
  have "set ?xs = l_bucket α T b ∪ s_bucket α T b"
    by simp
  then show ?thesis
    using l_un_s_bucket by blast
qed

lemma s_index_lower_bound:
  assumes "s_bucket_ptr_inv α T B"
  and     "s_seen_inv α T B SA n"
  and     "i < length SA"
  and     "n ≤ i"
shows "bucket_start α T (α (T ! (SA ! i))) ≤ i"
      (is "bucket_start α T ?b ≤ i")
proof -

  have "?b ≤ α (Max (set T))"
    by (meson SL_types.exhaust assms(2-) in_l_bucket_def in_s_current_bucketD(1) s_seen_invD(2,3))

  have "suffix_type T (SA ! i) = S_type ∨ suffix_type T (SA ! i) = L_type"
    using SL_types.exhaust by blast
  moreover
  have "suffix_type T (SA ! i) = S_type ⟹ ?thesis"
  proof -
    assume "suffix_type T (SA ! i) = S_type"
    with s_seen_invD(3)[OF assms(2-)] s_bucket_ptr_lower_bound[OF assms(1)]
    show ?thesis
      by (meson ‹?b ≤ α (Max (set T))› bucket_start_le_s_bucket_start dual_order.trans
            in_s_current_bucketD(2))
  qed
  moreover
  have "suffix_type T (SA ! i) = L_type ⟹ ?thesis"
  proof -
    assume "suffix_type T (SA ! i) = L_type"
    with s_seen_invD(2)[OF assms(2-)]
    show ?thesis
      using in_l_bucket_def by blast
  qed
  ultimately show ?thesis
    by blast
qed

lemma s_index_upper_bound:
  assumes "s_bucket_ptr_inv α T B"
  and     "s_seen_inv α T B SA n"
  and     "i < length SA"
  and     "n ≤ i"
shows "i < bucket_end α T (α (T ! (SA ! i)))"
      (is "i < bucket_end α T ?b")
proof -

  have "?b ≤ α (Max (set T))"
    by (meson SL_types.exhaust assms(2-) in_l_bucket_def in_s_current_bucketD(1) s_seen_invD(2,3))

  have "suffix_type T (SA ! i) = S_type ∨ suffix_type T (SA ! i) = L_type"
    using SL_types.exhaust by blast
  moreover
  have "suffix_type T (SA ! i) = S_type ⟹ ?thesis"
  proof -
    assume "suffix_type T (SA ! i) = S_type"
    with s_seen_invD(3)[OF assms(2-)] s_bucket_ptr_upper_bound[OF assms(1)]
    show ?thesis
      by (simp add: in_s_current_bucket_def)
  qed
  moreover
  have "suffix_type T (SA ! i) = L_type ⟹ ?thesis"
  proof -
    assume "suffix_type T (SA ! i) = L_type"
    with s_seen_invD(2)[OF assms(2-)]
    show ?thesis
      using in_l_bucket_def l_bucket_end_le_bucket_end less_le_trans by blast
  qed
  ultimately show ?thesis
    by blast
qed

subsection "Establishment and Maintenance Steps"

subsubsection "Distinctness"

lemma s_distinct_inv_established:
  assumes "s_bucket_init α T B"
  and     "valid_list T"
  and     "strict_mono α"
  and     "α bot = 0"
  shows "s_distinct_inv α T B SA"
  unfolding s_distinct_inv_def
proof (intro allI impI)
  fix b
  let ?goal = "distinct (list_slice SA (B ! b) (bucket_end α T b))"
  assume "b ≤ α (Max (set T))"

  have "b > 0 ⟹ ?goal"
  proof -
    assume "b > 0"
    with s_bucket_initD(1)[OF assms(1) `b ≤ _`]
    have "B ! b = bucket_end α T b"
      by blast
    then show ?goal
      using list_slice_n_n 
      by (metis distinct.simps(1))
  qed
  moreover
  have "b = 0 ⟹ ?goal"
  proof -
    assume "b = 0"
    with s_bucket_initD(2)[OF assms(1) `b ≤ _`]
    have "B ! b = 0" .
    moreover
    from `b = 0` assms(2-4)
    have "bucket_end α T b = Suc 0"
      by (simp add: valid_list_bucket_end_0)
    ultimately show ?thesis
      by (simp add: distinct_conv_nth)
  qed
  ultimately show ?goal
    by blast
qed

lemma s_distinct_inv_maintained_step:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_distinct_inv α T (B[b := k]) (SA[k := j])"
  unfolding s_distinct_inv_def
proof (intro allI impI)
  fix b'

  let ?goal = "distinct (list_slice (SA[k := j]) (B[b := k] ! b') (bucket_end α T b'))"

  assume "b' ≤ α (Max (set T))"

  from s_next_item_not_seen[OF assms(1-7,9-18)]
  have "j ∉ set (list_slice SA (B ! b) (bucket_end α T b))".

  from s_bucket_ptr_strict_lower_bound[OF assms(1-7,9-18)]
  have "s_bucket_start α T b < B ! b" .
  hence "s_bucket_start α T b ≤ k" "k < B ! b"
    using assms(19) by linarith+
  hence "bucket_start α T b ≤ k"
    using bucket_start_le_s_bucket_start le_trans by blast

  from assms(17)
  have "j < length T"
    by (simp add: suffix_type_s_bound)
  hence "b ≤ α (Max (set T))"
    by (simp add: assms(7,18) strict_mono_less_eq)
  with s_bucket_ptr_upper_bound[OF assms(2)] `k < B ! b`
  have "k < bucket_end α T b"
    using less_le_trans by auto
  hence "k < length SA"
    using assms(10) bucket_end_le_length less_le_trans by fastforce

  have "b = b' ⟹ ?goal"
  proof -
    assume "b = b'"
    hence "B[b := k] ! b' = k"
      using ‹b ≤ α (Max (set T))› assms(8) by auto
    from s_distinct_invD[OF assms(1) `b ≤ _`]
    have "distinct (list_slice SA (B ! b) (bucket_end α T b))" .
    moreover
    from ‹B[b := k] ! b' = k› ‹b = b'› ‹k < B ! b› ‹k < bucket_end α T b› ‹k < length SA› assms(19)
    have "list_slice (SA[k := j]) (B[b := k] ! b') (bucket_end α T b')
          = j # list_slice SA (B ! b) (bucket_end α T b)"
      by (metis Suc_pred diff_is_0_eq' dual_order.order_iff_strict gr0I length_list_update
            list_slice_Suc list_slice_update_unchanged_1 nth_list_update_eq)
    ultimately show ?thesis
      using `j ∉ set (list_slice SA (B ! b) (bucket_end α T b))`
      by simp
  qed
  moreover
  have "b ≠ b' ⟹ ?goal"
  proof -
    assume "b ≠ b'"
    hence "B[b := k] ! b' = B ! b'"
      by simp

    from outside_another_bucket[OF `b ≠ b'` `bucket_start _ _ _ ≤ k` `k < bucket_end _ _ _`]
    have "k < bucket_start α T b' ∨ bucket_end α T b' ≤ k"
      using leI by auto
    moreover
    have "k < bucket_start α T b' ⟹
          list_slice (SA[k := j]) (B[b := k] ! b') (bucket_end α T b')
            = list_slice SA (B ! b') (bucket_end α T b')"
    proof -
      assume "k < bucket_start α T b'"
      hence "k < B ! b'"
        by (meson ‹b' ≤ α (Max (set T))› assms(2) bucket_start_le_s_bucket_start less_le_trans
              s_bucket_ptr_inv_def)
      with list_slice_update_unchanged_1 `B[b := k] ! b' = B ! b'`
      show ?thesis
        by simp
    qed
    moreover
    from `B[b := k] ! b' = B ! b'`
    have "bucket_end α T b' ≤ k ⟹
          list_slice (SA[k := j]) (B[b := k] ! b') (bucket_end α T b')
            = list_slice SA (B ! b') (bucket_end α T b')"
      by (simp add: list_slice_update_unchanged_2)
    moreover
    from s_distinct_invD[OF assms(1) `b' ≤ _`]
    have "distinct (list_slice SA (B ! b') (bucket_end α T b'))" .
    ultimately show ?goal
      by auto
  qed
  ultimately
  show ?goal
    by blast
qed

corollary s_distinct_inv_maintained_perm_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_distinct_inv α T (B[b := k]) (SA[k := j])"
  using s_distinct_inv_maintained_step[OF s_perm_inv_elims(1-6,8-14)[OF assms(1)] assms(2-)]
  by blast

subsubsection "Bucket Pointer"

lemma s_bucket_ptr_inv_established:
  assumes "s_bucket_init α T B"
  and     "valid_list T"
  and     "strict_mono α"
  and     "α bot = 0"
  shows "s_bucket_ptr_inv α T B"
  unfolding s_bucket_ptr_inv_def
proof(intro allI impI)
  fix b
  let ?goal = "s_bucket_start α T b ≤ B ! b ∧ B ! b ≤ bucket_end α T b ∧ (b = 0 ⟶ B ! b = 0)"
  assume "b ≤ α (Max (set T))"

  have "b > 0 ⟹ ?goal"
  proof -
    assume "b > 0"
    with s_bucket_initD(1)[OF assms(1) `b ≤ _`]
    have "B ! b = bucket_end α T b" .
    then show ?thesis
      by (metis ‹0 < b› l_bucket_end_le_bucket_end less_numeral_extra(3) order_refl
            s_bucket_start_eq_l_bucket_end)
  qed
  moreover
  have "b = 0 ⟹ ?goal"
  proof -
    assume "b = 0"
    with s_bucket_initD(2)[OF assms(1) `b ≤ _`]
    have "B ! b = 0" .
    with `b = 0`
         valid_list_bucket_end_0[OF assms(2-)]
         valid_list_s_bucket_start_0[OF assms(2-)]
    show ?thesis
      by auto
  qed
  ultimately show "?goal"
    by auto
qed

lemma s_bucket_ptr_inv_maintained_step:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_bucket_ptr_inv α T (B[b := k])"
  unfolding s_bucket_ptr_inv_def
proof(intro allI impI)
  fix b'
  assume "b' ≤ α (Max (set T))"

  let ?goal = "s_bucket_start α T b' ≤ B[b := k] ! b' ∧  B[b := k] ! b' ≤ bucket_end α T b' ∧
               (b' = 0 ⟶ B[b := k] ! b' = 0)"

  from valid_list_length_ex[OF assms(12)]
  obtain m where
    "length T = Suc m"
    by blast
  moreover
  have "j < length T"
    by (simp add: assms(17) suffix_type_s_bound)
  moreover
  from s_seen_invD(1)[OF assms(5,15)] assms(14,16)
  have "Suc j < length T"
    by simp
  ultimately have "j < m"
    by linarith
  hence "b ≠ 0"
    by (metis  ‹length T = Suc m› assms(7,12,13,18) diff_Suc_1 strict_mono_eq valid_list_def)

  have "b ≠ b' ⟹ ?goal"
  proof -
    assume "b ≠ b'"
    hence "B[b := k] ! b' = B ! b'"
      by simp
    with s_bucket_ptr_lower_bound[OF assms(2) `b' ≤ α (Max (set T))`]
         s_bucket_ptr_upper_bound[OF assms(2) `b' ≤ α (Max (set T))`]
         s_bucket_ptr_0[OF assms(2)]
    show ?thesis
      by auto
  qed
  moreover
  have "b = b' ⟹ ?goal"
  proof -
    assume "b = b'"
    from s_bucket_ptr_strict_lower_bound[OF assms(1-7,9-13,14-18)]
    have "s_bucket_start α T b < B ! b".
    hence "s_bucket_start α T b ≤ k"
      using assms(19) by linarith
    moreover
    from ‹b = b'› ‹b' ≤ α (Max (set T))› assms(2,19)
    have "k ≤ bucket_end α T b"
      using le_diff_conv s_bucket_ptr_inv_def trans_le_add1 by blast
    moreover
    have "B[b := k] ! b' = k"
      using ‹b = b'› ‹b' ≤ α (Max (set T))› assms(8) by auto
    ultimately show ?thesis
      using ‹b = b'› ‹b ≠ 0› by auto
  qed
  ultimately show ?goal
    by linarith
qed

corollary s_bucket_ptr_inv_maintained_perm_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_bucket_ptr_inv α T (B[b := k])"
  using s_bucket_ptr_inv_maintained_step[OF s_perm_inv_elims(1-6,8-14)[OF assms(1)] assms(2-)]
  by blast

subsubsection "Locations"

lemma s_locations_inv_established:
  assumes "s_bucket_init α T B"
  and     "s_type_init T SA"
  and     "valid_list T"
  and     "strict_mono α"
  and     "α bot = 0"
  shows "s_locations_inv α T B SA"
  unfolding s_locations_inv_def
proof(safe)
  fix b i
  assume "b ≤ α (Max (set T))" "B ! b ≤ i" "i < bucket_end α T b"
  hence "b > 0 ⟹ SA ! i ∈ s_bucket α T b"
    by (metis assms(1) not_le s_bucket_init_def)
  moreover
  have "b = 0 ⟹ SA ! i ∈ s_bucket α T b"
  proof -
    assume "b = 0"
    have "0 ≤ i"
      by blast
    moreover
    have "bucket_end α T 0 = 1"
      using assms(3-5) valid_list_bucket_end_0 by blast
    with `i < bucket_end α T b` `b = 0`
    have "i < 1"
      by simp
    ultimately have "i = 0"
      by blast
    moreover
    from s_type_init_def[of T SA] assms(2)
    obtain n where
      "length T = Suc n"
      "SA ! 0 = n"
      by blast
    with suffix_type_last[of T n]
    have "suffix_type T n = S_type"
      by blast
    moreover
    have "T ! n = bot"
      by (metis ‹length T = Suc n› assms(3) diff_Suc_1 last_conv_nth less_numeral_extra(3)
            list.size(3) valid_list_def)
    hence "α (T ! n) = 0"
      by (simp add: assms(5))
    ultimately show ?thesis
      by (simp add: ‹SA ! 0 = n›‹b = 0› ‹length T = Suc n› bucket_def s_bucket_def)
  qed
  ultimately show "SA ! i ∈ s_bucket α T b"
    by linarith
qed

lemma s_locations_inv_maintained_step:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_locations_inv α T (B[b := k]) (SA[k := j])"
  unfolding s_locations_inv_def
proof(safe)
  fix b' i'
  assume "b' ≤ α (Max (set T))" "B[b := k] ! b' ≤ i'" "i' < bucket_end α T b'"

  from s_bucket_ptr_strict_lower_bound[OF assms(1-7,9-18)]
  have "s_bucket_start α T b < B ! b".
  hence "s_bucket_start α T b ≤ k"
    using assms(19) by linarith

  from `s_bucket_start α T b < B ! b`
  have "k < B ! b"
    using assms(19) by linarith

  have "j < length T"
    by (simp add: assms(17) suffix_type_s_bound)
  hence "b ≤ α (Max (set T))"
    by (simp add: assms(18) assms(7) strict_mono_less_eq)
  with s_bucket_ptr_upper_bound[OF assms(2)]
  have "B ! b ≤ bucket_end α T b"
    by blast

  have "b ≠ b' ⟹ SA[k := j] ! i' ∈ s_bucket α T b'"
  proof -
    assume "b ≠ b'"
    hence "B[b := k] ! b' = B ! b'"
      by simp
    with `B[b := k] ! b' ≤ i'`
    have "B ! b' ≤ i'"
      by simp
    with s_locations_invD[OF assms(3) `b' ≤ α (Max (set T))` _ `i' < bucket_end α T b'`]
    have "SA ! i' ∈ s_bucket α T b'"
      by linarith
    moreover
    from s_bucket_ptr_lower_bound[OF assms(2) `b' ≤ α (Max (set T))`] `B ! b' ≤ i'`
    have "bucket_start α T b' ≤ i'"
      by (meson bucket_start_le_s_bucket_start dual_order.trans)
    with outside_another_bucket[OF `b ≠ b'`[symmetric] _ `i' < _`]
         ‹B ! b ≤ bucket_end α T b› ‹k < B ! b› ‹s_bucket_start α T b ≤ k›
    have "k ≠ i'"
      using bucket_start_le_s_bucket_start le_trans less_le_trans by blast
    hence "SA[k := j] ! i' = SA ! i'"
      by simp
    ultimately show ?thesis
      by simp
  qed
  moreover
  have "b = b' ⟹ SA[k := j] ! i' ∈ s_bucket α T b'"
  proof -
    assume "b = b'"
    hence "k ≤ i'"
      using ‹B[b := k] ! b' ≤ i'› ‹b' ≤ α (Max (set T))› assms(8) by auto
    hence "k = i' ∨ k < i'"
      by linarith
    moreover
    have "k = i' ⟹ ?thesis"
    proof -
      assume "k = i'"
      hence "SA[k := j] ! i' = j"
        by (metis ‹i' < bucket_end α T b'› assms(10) bucket_end_le_length dual_order.strict_trans1
              nth_list_update)
      with assms(17,18) `b = b'` `j < length T`
      show ?thesis
        by (simp add: bucket_def s_bucket_def)
    qed
    moreover
    have "k < i' ⟹ ?thesis"
    proof -
      assume "k < i'"
      hence "B ! b ≤ i'"
        using assms(19) by linarith
      with s_locations_invD[OF assms(3) `b' ≤ _` _ `i' < bucket_end _ _ _`] `b = b'`
      have "SA ! i' ∈ s_bucket α T b'"
        by blast
      moreover
      have "SA[k := j] ! i' = SA ! i'"
        using ‹k < i'› by auto
      ultimately show ?thesis
        by simp
    qed
    ultimately show ?thesis
      by linarith
  qed
  ultimately show "SA[k := j] ! i' ∈ s_bucket α T b'"
    by blast
qed

corollary s_locations_inv_maintained_perm_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_locations_inv α T (B[b := k]) (SA[k := j])"
  using s_locations_inv_maintained_step[OF s_perm_inv_elims(1-6,8-14)[OF assms(1)] assms(2-)]
  by blast

subsubsection "Unchanged"

lemma s_unchanged_inv_established:
  shows "s_unchanged_inv α T B SA SA"
  by (simp add: s_unchanged_inv_def)

lemma s_unchanged_inv_maintained_step:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_unchanged_inv α T (B[b := k]) SA0 (SA[k := j])"
  unfolding s_unchanged_inv_def
proof(safe)
  fix b' i'
  assume "b' ≤ α (Max (set T))" "bucket_start α T b' ≤ i'" "i' < B[b := k] ! b'"

  from s_bucket_ptr_strict_lower_bound[OF assms(1-7,9-18)]
  have "s_bucket_start α T b < B ! b".
  hence "s_bucket_start α T b ≤ k"
    using assms(19) by linarith
  hence "bucket_start α T b ≤ k"
    using bucket_start_le_s_bucket_start le_trans by blast

  from `s_bucket_start α T b < B ! b`
  have "k < B ! b"
    using assms(19) by linarith

  have "j < length T"
    by (simp add: assms(17) suffix_type_s_bound)
  hence "b ≤ α (Max (set T))"
    by (simp add: assms(7,18) strict_mono_less_eq)
  with s_bucket_ptr_upper_bound[OF assms(2)]
  have "B ! b ≤ bucket_end α T b"
    by blast
  with `k < B ! b`
  have "k < bucket_end α T b"
    by linarith

  have "b = b' ⟹ SA[k := j] ! i' = SA0 ! i'"
  proof -
    assume "b = b'"
    hence "B[b := k] ! b' = k"
      using ‹b' ≤ α (Max (set T))› assms(8) by auto
    with `i' < B[b := k] ! b'`
    have "i' < k"
      by linarith
    hence "SA[k := j] ! i' = SA ! i'"
      by simp
    moreover
    from `i' < k` `k < B ! b` `b = b'`
    have "i' < B ! b'"
      by simp
    with s_unchanged_invD[OF assms(4) `b' ≤ _` `bucket_start _ _ _ ≤ i'`]
    have "SA ! i' = SA0 ! i'"
      by simp
    ultimately show ?thesis
      by simp
  qed
  moreover
  have "b ≠ b' ⟹ SA[k := j] ! i' = SA0 ! i'"
  proof -
    assume "b ≠ b'"
    with `i' < B[b := k] ! b'`
    have "i' < B ! b'"
      by simp
    with s_unchanged_invD[OF assms(4) `b' ≤ _` `bucket_start _ _ b' ≤ _`]
    have "SA ! i' = SA0 ! i'"
      by blast
    moreover
    from s_bucket_ptr_upper_bound[OF assms(2) `b' ≤ _`] `i' < B ! b'`
    have "i' < bucket_end α T b'"
      by linarith
    with outside_another_bucket[OF `b ≠ b'` `bucket_start _ _ _ ≤ k` `k < bucket_end _ _ _`]
         `bucket_start _ _ b' ≤ i'`
    have "k ≠ i'"
      by blast
    hence "SA[k := j] ! i' = SA ! i'"
      by simp
    ultimately show ?thesis
      by simp
  qed
  ultimately show "SA[k := j] ! i' = SA0 ! i'"
    by blast
qed

corollary s_unchanged_inv_maintained_perm_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_unchanged_inv α T (B[b := k]) SA0 (SA[k := j])"
  using s_unchanged_inv_maintained_step[OF s_perm_inv_elims(1-6,8-14)[OF assms(1)] assms(2-)]
  by blast

subsubsection "Seen"

lemma s_seen_inv_established:
  assumes "length SA = length T"
  and     "length T ≤ n"
shows "s_seen_inv α T B SA n"
  unfolding s_seen_inv_def
  using assms by auto

lemma s_seen_inv_maintained_step_c1:
  assumes "s_bucket_ptr_inv α T B"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "strict_mono α"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "Suc 0 < length T"
  and     "i = Suc n"
  and     "length SA ≤ Suc n"
  shows "s_seen_inv α T B SA n"
  unfolding s_seen_inv_def
proof (intro allI impI)
  fix j
  assume "j < length SA" "n ≤ j"
  hence "n < length SA"
    by simp
  with assms(10,11)
  have "length SA = Suc n"
    by linarith

  let ?b = "α (T ! (SA ! j))"
  let ?g1 = "(suffix_type T (SA ! j) = S_type ⟶ in_s_current_bucket α T B ?b j)"
  and ?g2 = "(suffix_type T (SA ! j) = L_type ⟶ in_l_bucket α T ?b j)"
  and ?g3 = "SA ! j < length T"

  from `n ≤ j`
  have "n = j ∨ Suc n ≤ j"
    using dual_order.antisym not_less_eq_eq by auto
  moreover
  have "n = j ⟹ ?g1 ∧ ?g2 ∧ ?g3"
  proof -
    let ?b_max = "α (Max (set T))"
    assume "n = j"
    hence "j < bucket_end α T ?b_max"
      using ‹j < length SA› assms(4,6) bucket_end_Max by fastforce
    hence "j < l_bucket_end α T ?b_max"
      using l_bucket_Max[OF assms(8,9,4)]
      by (simp add: bucket_end_def' bucket_size_def l_bucket_end_def l_bucket_size_def)
    moreover
    from ‹n = j› ‹j < length SA› ‹length SA = Suc n› assms(4,6,10)
    have "bucket_start α T ?b_max ≤ j"
      by (metis Suc_leI antisym bucket_end_eq_length bucket_end_le_length gr_implies_not0
                index_in_bucket_interval_gen length_0_conv)
    moreover
    have "?b_max ≤ α (Max (set T))"
      by simp
    ultimately have "SA ! j ∈ l_bucket α T ?b_max"
      using l_types_init_nth[OF assms(6) l_types_init_maintained[OF assms(1,2,5-7)] ]
      by blast
    hence "?b_max = α (T ! (SA ! j))"
      by (simp add: bucket_def l_bucket_def)
    moreover
    from `SA ! j ∈ l_bucket α T ?b_max`
    have ?g3
      by (simp add: bucket_def l_bucket_def)
    moreover
    from `SA ! j ∈ l_bucket α T ?b_max`
    have "suffix_type T (SA ! j) = L_type"
      by (simp add: bucket_def l_bucket_def)
    moreover
    have "in_l_bucket α T (α (T ! (SA ! j))) j"
      using ‹bucket_start _ _ _  ≤ j› ‹j < l_bucket_end _ _ _› calculation(1) in_l_bucket_def
      by fastforce
    hence "?g2"
      using calculation(3) by blast
    moreover
    from calculation(3)
    have "?g1"
      by simp
    ultimately show ?thesis
      by simp
  qed
  moreover
  have "Suc n ≤ j ⟹ ?g1 ∧ ?g2 ∧ ?g3"
  proof -
    assume "Suc n ≤ j"
    with s_seen_invD[OF assms(3) `j < length SA`] assms(10)
    show ?thesis
      by blast
  qed
  ultimately show "?g1 ∧ ?g2 ∧ ?g3"
    by blast
qed

corollary s_seen_inv_maintained_perm_step_c1:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "length SA ≤ Suc n"
  shows "s_seen_inv α T B SA n"
  using s_seen_inv_maintained_step_c1[OF s_perm_inv_elims(2,4,5,8,10-13,15)[OF assms(1)] assms(2-)]
  by blast

lemma s_seen_inv_maintained_step_c1_alt:
  assumes "s_bucket_ptr_inv α T B"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "strict_mono α"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "Suc 0 < length T"
  and     "i = Suc n"
  and     "length T ≤ SA ! Suc n"
  shows "s_seen_inv α T B SA n"
proof (cases "length SA ≤ Suc n")
  assume "length SA ≤ Suc n"
  then show ?thesis
    using assms(1-10) s_seen_inv_maintained_step_c1 by blast
next
  assume "¬ length SA ≤ Suc n"
  hence "Suc n < length SA"
    by simp
  show ?thesis
    unfolding s_seen_inv_def
  proof (intro allI impI)
    fix j
    assume "j < length SA" "n ≤ j"
    hence "n < length SA"
      by simp

    let ?b = "α (T ! (SA ! j))"
    let ?g1 = "(suffix_type T (SA ! j) = S_type ⟶ in_s_current_bucket α T B ?b j)"
    and ?g2 = "(suffix_type T (SA ! j) = L_type ⟶ in_l_bucket α T ?b j)"
    and ?g3 = "SA ! j < length T"
  
   from `n ≤ j`
    have "n = j ∨ Suc n ≤ j"
      using dual_order.antisym not_less_eq_eq by auto
    moreover
    have "n = j ⟹ ?g1 ∧ ?g2 ∧ ?g3"
      by (metis Suc_le_mono ‹Suc n < length SA› ‹n ≤ j› assms(3,10,11) linorder_not_le
                s_seen_invD(1))
    moreover
    have "Suc n ≤ j ⟹ ?g1 ∧ ?g2 ∧ ?g3"
    proof -
      assume "Suc n ≤ j"
      with s_seen_invD[OF assms(3) `j < length SA`] assms(10)
      show ?thesis
        by blast
    qed
    ultimately show "?g1 ∧ ?g2 ∧ ?g3"
      by blast
  qed
qed

corollary s_seen_inv_maintained_perm_step_c1_alt:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "length T ≤ SA ! Suc n"
  shows "s_seen_inv α T B SA n"
  using s_seen_inv_maintained_step_c1_alt[OF s_perm_inv_elims(2,4,5,8,10-13,15)[OF assms(1)] assms(2-)]
  by blast

lemma s_seen_inv_maintained_step_c2:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "s_suc_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "Suc 0 < length T"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = 0"
  shows "s_seen_inv α T B SA n"
 unfolding s_seen_inv_def
proof (intro allI impI)
  fix j
  assume "j < length SA" "n ≤ j"
  hence "n < length SA"
    by simp
  hence "n < length T"
    by (simp add: assms(11))


  let ?b = "α (T ! (SA ! j))"
  let ?g1 = "(suffix_type T (SA ! j) = S_type ⟶ in_s_current_bucket α T B ?b j)"
  and ?g2 = "(suffix_type T (SA ! j) = L_type ⟶ in_l_bucket α T ?b j)"
  and ?g3 = "SA ! j < length T"

 from `n ≤ j`
  have "n = j ∨ Suc n ≤ j"
    by linarith
  moreover
  have "n = j ⟹ ?g1 ∧ ?g2 ∧ ?g3"
  proof -
    assume "n = j"
    with index_in_bucket_interval_gen[OF `n < length T` assms(8)]
    obtain b where
      "b ≤ α (Max (set T))"
      "bucket_start α T b ≤ j"
      "j < bucket_end α T b"
      by blast

    have "j < l_bucket_end α T b ∨ s_bucket_start α T b ≤ j"
      by (metis not_le s_bucket_start_eq_l_bucket_end)
    moreover
    have "j < l_bucket_end α T b ⟹ ?thesis"
    proof -
      assume "j < l_bucket_end α T b"
      with l_types_init_nth[OF assms(11) l_types_init_maintained[OF assms(2,4,10-12)] `b ≤ _`
            `bucket_start _ _ _ ≤ j`]
      have "SA ! j ∈ l_bucket α T b" .
      hence "suffix_type T (SA ! j) = L_type" "SA ! j < length T"
        by (simp add: l_bucket_def bucket_def)+
      moreover
      have ?g1
        by(simp add: calculation(1) SL_types.exhaust)
      moreover
      from `SA ! j ∈ l_bucket α T b`
      have "b = α (T ! (SA ! j))"
        by (metis (mono_tags, lifting)  bucket_def l_bucket_def mem_Collect_eq)
      with `bucket_start α T b ≤ j` `j < l_bucket_end α T b` `b ≤ _`
      have "in_l_bucket α T (α (T ! (SA ! j))) j"
        using in_l_bucket_def by blast
      ultimately show ?thesis
        by blast
    qed
    moreover
    have "s_bucket_start α T b ≤ j ⟹ ?thesis"
    proof -
      assume "s_bucket_start α T b ≤ j"
      hence "s_bucket_start α T b < i"
        by (simp add: ‹n = j› assms(16))

      have "B ! b ≤ i"
      proof(rule ccontr)
        assume "¬B ! b ≤ i"
        hence "i < B ! b"
          by simp
        with s_B_val[OF assms(1-6,8,10-13,15) `b ≤ α _`]
        have "B ! b = s_bucket_start α T b" .
        with `s_bucket_start α T b < i` `i < B ! b`
        show False
          by linarith
      qed
      hence "B ! b < i ∨ B ! b = i"
        using dual_order.order_iff_strict by blast
      moreover
      have "B ! b < i ⟹ ?thesis"
      proof -
        assume "B ! b < i"
        hence "B ! b ≤ j"
          by (simp add: ‹n = j› assms(16))
        with s_locations_invD[OF assms(3) `b ≤ _` _ `j < bucket_end _ _ _`]
        have "SA ! j ∈ s_bucket α T b" .
        hence "SA ! j < length T" "suffix_type T (SA ! j) = S_type"
          by (simp add: s_bucket_def bucket_def)+
        moreover
        from calculation(2)
        have ?g2
          by simp
        moreover
        from `SA ! j ∈ s_bucket α T b`
        have "α (T ! (SA ! j)) = b"
          by (simp add: s_bucket_def bucket_def)
        with `B ! b ≤ j` `j < bucket_end α T b` `b ≤ _`
        have "in_s_current_bucket α T B (α (T ! (SA ! j))) j"
          by (simp add: in_s_current_bucket_def)
        ultimately show ?thesis
          by blast
      qed
      moreover
      have "B ! b = i ⟹ ?thesis"
      proof -
        assume "B ! b = i"
        hence "s_bucket_start α T b < B ! b"
          using ‹s_bucket_start α T b < i› by blast

        have "b ≠ 0"
          using ‹B ! b = i› assms(2,16) less_Suc_eq_0_disj s_bucket_ptr_0 by fastforce

        let ?xs = "list_slice SA (B ! b) (bucket_end α T b)"
        let ?B = "set ?xs"
        let ?A = "s_bucket α T b - ?B"

       from s_locations_inv_subset_s_bucket[OF assms(3) `b ≤ _`]
        have "?B ⊆ s_bucket α T b" .
        hence "?A ⊆ s_bucket α T b"
          by blast

        have "card (s_bucket α T b) = bucket_end α T b - s_bucket_start α T b"
          by (simp add: bucket_end_eq_s_start_pl_size s_bucket_size_def)

        from s_distinct_invD[OF assms(1) `b ≤ _`]
        have "card ?B = bucket_end α T b - B ! b"
          by (metis assms(11) bucket_end_le_length distinct_card length_list_slice min.absorb_iff1)
        hence "card ?B < card (s_bucket α T b)"
          using ‹card (s_bucket α T b) = bucket_end α T b - s_bucket_start α T b›
                ‹j < bucket_end α T b› ‹s_bucket_start α T b < B ! b› ‹s_bucket_start α T b ≤ j›
          by linarith
        with card_psubset[OF finite_s_bucket `?B ⊆ s_bucket α T b`]
        have "?B ⊂ s_bucket α T b" .
        hence "?A ≠ {}"
          by blast
        with subset_s_bucket_successor[OF assms(13,8,14) `b ≠ _` `?A ⊆ _`]
        obtain x where
          "x ∈ ?A"
          "Suc x ∈ ?B ∨ (∃b'. b < b' ∧ Suc x ∈ bucket α T b')"
          by blast
        hence "suffix_type T x = S_type" "α (T ! x) = b" "x < length T"
          by (simp add: s_bucket_def bucket_def)+

        from `x ∈ ?A`
        have "x ∉ ?B"
          by blast

        have "Suc x ∈ ?B ⟹ ?thesis"
        proof -
          assume "Suc x ∈ ?B"
          from nth_mem_list_slice[OF `Suc x ∈ ?B`]
          obtain i' where
            "i' < length SA"
            "B ! b ≤ i'"
            "i' < bucket_end α T b"
            "SA ! i' = Suc x"
            by blast

          have "i ≠ i'"
          proof (rule ccontr)
            assume "¬ i ≠ i'"
            hence "i = i'"
              by auto
            with assms(16,18) `SA ! i' = Suc x`
            show False
              by simp
          qed
          with `B ! b = i` `B ! b ≤ i'`
          have "i < i'"
            by simp
          with s_suc_invD[OF assms(7) `i' < length SA` _ `SA ! i' = Suc x` `suffix_type T x = _`,
                simplified `α (T ! x) = b`]
          obtain k where
            "in_s_current_bucket α T B b k"
            "SA ! k = x"
            "k < i'"
            by blast
          hence "x ∈ ?B"
            by (meson assms(11) in_s_current_bucket_list_slice)
          with `x ∉ ?B`
          have False
            by blast
          then show ?thesis
            by blast
        qed
        moreover
        have "∃b'. b < b' ∧ Suc x ∈ bucket α T b' ⟹ ?thesis"
        proof -
          assume "∃b'. b < b' ∧ Suc x ∈ bucket α T b'"
          then obtain b' where
            "b < b'"
            "Suc x ∈ bucket α T b'"
            by blast
          hence "bucket_end α T b ≤ bucket_start α T b'"
            by (simp add: less_bucket_end_le_start)
          with s_bucket_ptr_upper_bound[OF assms(2) `b ≤ _ `] `B ! b = i`
          have "i ≤ bucket_start α T b'"
            by linarith

          from ‹Suc x ∈ bucket α T b'›
          have "b' ≤ α (Max (set T))"
            by (metis (mono_tags, lifting) Max_greD assms(8) bucket_def mem_Collect_eq
                  strict_mono_less_eq)
          with `i ≤ bucket_start α T b'` s_bucket_ptr_lower_bound[OF assms(2), of b']
          have "i ≤ B ! b'"
            by (metis nat_le_iff_add s_bucket_start_def trans_le_add1)
          hence "i = B ! b' ∨ i < B ! b'"
            using antisym_conv1 by blast
          hence "B ! b' = s_bucket_start α T b'"
          proof
            assume "i = B ! b'"
            with `i ≤ bucket_start α T b'` s_bucket_ptr_lower_bound[OF assms(2) `b' ≤ _`]
            show ?thesis
              by (simp add: s_bucket_start_def)
          next
            assume "i < B ! b'"
            with s_B_val[OF assms(1-6,8,10-13,15) `b' ≤ _`]
            show ?thesis .
          qed

          from `Suc x ∈ bucket α T b'`
          have "Suc x ∈ l_bucket α T b' ∨ Suc x ∈ s_bucket α T b'"
            by (simp add: l_un_s_bucket)
          moreover
          have "Suc x ∈ l_bucket α T b' ⟹ ?thesis"
          proof -
            assume "Suc x ∈ l_bucket α T b'"
            with l_types_initD(1)[OF l_types_init_maintained[OF assms(2,4,10-12)] `b' ≤ _`]
            have "Suc x ∈ set (list_slice SA (bucket_start α T b') (l_bucket_end α T b'))"
              by simp
            with nth_mem_list_slice[of "Suc x" SA "bucket_start α T b'" "l_bucket_end α T b'"]
            obtain i' where
              "i' < length SA"
              "bucket_start α T b' ≤ i'"
              "i' < l_bucket_end α T b'"
              "SA ! i' = Suc x"
              by blast

            have "i ≠ i'"
            proof (rule ccontr)
              assume "¬ i ≠ i'"
              hence "i = i'"
                by auto
              with `SA ! i' = Suc x` assms(16,18)
              show False
                by simp
            qed
            hence "i < i'"
              using ‹bucket_start α T b' ≤ i'› ‹i ≤ bucket_start α T b'› by auto
            with s_suc_invD[OF assms(7) `i' < length _` _ `SA ! i' = _` `suffix_type T x = _`,
                  simplified `α (T ! x) = b`]
            obtain k where
              "in_s_current_bucket α T B b k"
              "SA ! k = x"
              "k < i'"
              by blast
            hence "x ∈ ?B"
              by (meson assms(11) in_s_current_bucket_list_slice)
            with `x ∉ ?B`
            have False
              by blast
            then show ?thesis
              by blast
          qed
          moreover
          have "Suc x ∈ s_bucket α T b' ⟹ ?thesis"
          proof -
            assume "Suc x ∈ s_bucket α T b'"

          let ?ys = "list_slice SA (s_bucket_start α T b') (bucket_end α T b')"

            from distinct_card[OF s_distinct_invD[OF assms(1) `b' ≤ _`],
                  simplified `B ! b' = s_bucket_start _ _ _`]
            have "card (set ?ys) = card (s_bucket α T b')"
              by (metis add_diff_cancel_left' assms(11) bucket_end_eq_s_start_pl_size
                    bucket_end_le_length length_list_slice min_def s_bucket_size_def)
            with card_subset_eq[
                  OF finite_s_bucket s_locations_inv_subset_s_bucket[OF assms(3) `b' ≤ _`],
                  simplified `B ! b' = s_bucket_start α T b'`]
            have "set ?ys = s_bucket α T b'"
              by blast
            with `Suc x ∈ s_bucket α T b'`
            have "Suc x ∈ set ?ys"
              by simp
            with nth_mem_list_slice[of "Suc x"]
            obtain i' where
              "i' < length SA"
              "s_bucket_start α T b' ≤ i'"
              "i' < bucket_end α T b'"
              "SA ! i' = Suc x"
              by blast

            from `SA ! i' = Suc x` assms(16,18)
            have "i ≠ i'"
              using nat.discI by blast
            hence "i < i'"
              using ‹B ! b' = s_bucket_start α T b'› ‹i ≤ B ! b'› ‹s_bucket_start α T b' ≤ i'›
              by linarith
            with s_suc_invD[OF assms(7) `i' < length _` _ `SA ! i' = _` `suffix_type T x = _`,
                  simplified `α (T ! x) = b`]
            obtain k where
              "in_s_current_bucket α T B b k"
              "SA ! k = x"
              "k < i'"
              by blast
            hence "x ∈ ?B"
              by (meson assms(11) in_s_current_bucket_list_slice)
            with `x ∉ ?B`
            have False
              by blast
            then show ?thesis
              by blast
          qed
          ultimately show ?thesis
            by blast
        qed
        ultimately show ?thesis
          using `Suc x ∈ ?B ∨ (∃b'. b < b' ∧ Suc x ∈ bucket α T b')` by blast
      qed
      ultimately show ?thesis
        by blast
    qed
    ultimately show ?thesis
      by blast
  qed
  moreover
  have "Suc n ≤ j ⟹ ?g1 ∧ ?g2 ∧ ?g3"
  proof -
    assume "Suc n ≤ j"
    with s_seen_invD[OF assms(5) `j < length SA`] assms(16)
    show ?thesis
      by blast
  qed
  ultimately show "?g1 ∧ ?g2 ∧ ?g3"
    by blast
qed

corollary s_seen_inv_maintained_perm_step_c2:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = 0"
shows "s_seen_inv α T B SA n"
  using s_seen_inv_maintained_step_c2[OF s_perm_inv_elims[OF assms(1)] assms(2-)]
  by blast

lemma s_seen_inv_maintained_step_c3:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "s_suc_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "Suc 0 < length T"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = L_type"
shows "s_seen_inv α T B SA n"
 unfolding s_seen_inv_def
proof (intro allI impI)
  fix k
  assume "k < length SA" "n ≤ k"
  hence "n < length SA"
    by simp
  hence "n < length T"
    by (simp add: assms(11))

  let ?b = "α (T ! (SA ! k))"
  let ?g1 = "(suffix_type T (SA ! k) = S_type ⟶ in_s_current_bucket α T B ?b k)"
  and ?g2 = "(suffix_type T (SA ! k) = L_type ⟶ in_l_bucket α T ?b k)"
  and ?g3 = "SA ! k < length T"

 from `n ≤ k`
  have "n = k ∨ Suc n ≤ k"
    by linarith
  moreover
  have "n = k ⟹ ?g1 ∧ ?g2 ∧ ?g3"
  proof -
    assume "n = k"
    with index_in_bucket_interval_gen[OF `n < length T` assms(8)]
    obtain b where
      "b ≤ α (Max (set T))"
      "bucket_start α T b ≤ k"
      "k < bucket_end α T b"
      by blast

    have "k < l_bucket_end α T b ∨ s_bucket_start α T b ≤ k"
      by (metis not_le s_bucket_start_eq_l_bucket_end)
    moreover
    have "k < l_bucket_end α T b ⟹ ?thesis"
    proof -
      assume "k < l_bucket_end α T b"
      with l_types_init_nth[OF assms(11) l_types_init_maintained[OF assms(2,4,10-12)]
            `b ≤ _` `bucket_start _ _ _ ≤ _`]
      have "SA ! k ∈ l_bucket α T b" .
      hence "SA ! k < length T" "suffix_type T (SA ! k) = L_type"
        by (simp add: l_bucket_def bucket_def)+
      moreover
      from calculation(2)
      have ?g1
        by simp
      moreover
      from `SA ! k ∈ l_bucket α T b`
      have "b = (α (T ! (SA ! k)))"
        by (simp add: l_bucket_def bucket_def)
      with `b ≤ _` `bucket_start _ _ _ ≤ _` `k < l_bucket_end _ _ _`
      have "in_l_bucket α T (α (T ! (SA ! k))) k"
        using in_l_bucket_def by blast
      ultimately show ?thesis
        by blast
    qed
    moreover
    have "s_bucket_start α T b ≤ k ⟹ ?thesis"
    proof -
      assume "s_bucket_start α T b ≤ k"
      hence "s_bucket_start α T b < i"
        by (simp add: ‹n = k› assms(16))

      have "B ! b ≤ i"
      proof(rule ccontr)
        assume "¬B ! b ≤ i"
        hence "i < B ! b"
          by simp
        with s_B_val[OF assms(1-6,8,10-13,15) `b ≤ α _`]
        have "B ! b = s_bucket_start α T b" .
        with `s_bucket_start α T b < i` `i < B ! b`
        show False
          by linarith
      qed
      hence "i = B ! b ∨ B ! b < i"
        by linarith
      moreover
      have "B ! b < i ⟹ ?thesis"
      proof -
        assume "B ! b < i"
        hence "B ! b ≤ k"
          by (simp add: ‹n = k› assms(16))
        with s_locations_invD[OF assms(3) `b ≤ _` _ `k < bucket_end _ _ _`]
        have "SA ! k ∈ s_bucket α T b" .
        hence "SA ! k < length T" "suffix_type T (SA ! k) = S_type"
          by (simp add: s_bucket_def bucket_def)+
        moreover
        from calculation(2)
        have ?g2
          by simp
        moreover
        from `SA ! k ∈ s_bucket α T b`
        have "α (T ! (SA ! k)) = b"
          by (simp add: s_bucket_def bucket_def)
        with `B ! b ≤ k` `k < bucket_end α T b` `b ≤ _`
        have "in_s_current_bucket α T B (α (T ! (SA ! k))) k"
          by (simp add: in_s_current_bucket_def)
        ultimately show ?thesis
          by blast
      qed
      moreover
      have "i = B ! b ⟹ ?thesis"
      proof -
        assume "i = B ! b"
        hence "k < B ! b"
          using ‹n = k› assms(16) by linarith

        have "s_bucket_start α T b < B ! b"
          using ‹i = B ! b› ‹s_bucket_start α T b < i› by blast

        have "b ≠ 0"
          by (metis ‹k < B ! b› assms(2) not_less_zero s_bucket_ptr_0)

        let ?xs = "list_slice SA (B ! b) (bucket_end α T b)"
        let ?B = "set ?xs"
        let ?A = "s_bucket α T b - ?B"

        from s_locations_inv_subset_s_bucket[OF assms(3) `b ≤ _`]
        have "?B ⊆ s_bucket α T b" .
        hence "?A ⊆ s_bucket α T b"
          by blast

        have "card (s_bucket α T b) = bucket_end α T b - s_bucket_start α T b"
          by (simp add: bucket_end_eq_s_start_pl_size s_bucket_size_def)

        from s_distinct_invD[OF assms(1) `b ≤ _`]
        have "card ?B = bucket_end α T b - B ! b"
          by (metis assms(11) bucket_end_le_length distinct_card length_list_slice min.absorb_iff1)
        hence "card ?B < card (s_bucket α T b)"
          using ‹card (s_bucket α T b) = bucket_end α T b - s_bucket_start α T b›
                ‹k < bucket_end α T b› ‹s_bucket_start α T b < B ! b› ‹s_bucket_start α T b ≤ k›
          by linarith
        with card_psubset[OF finite_s_bucket `?B ⊆ s_bucket α T b`]
        have "?B ⊂ s_bucket α T b" .
        hence "?A ≠ {}"
          by blast
        with subset_s_bucket_successor[OF assms(13,8,14) `b ≠ 0` `?A ⊆ s_bucket α T b`]
        obtain x where
          "x ∈ ?A"
          "Suc x ∈ s_bucket α T b - ?A ∨ (∃b'. b < b' ∧ Suc x ∈ bucket α T b')"
          by blast
        hence "Suc x ∈ ?B ∨ (∃b'. b < b' ∧ Suc x ∈ bucket α T b')"
          by blast

        from `x ∈ ?A` `?A ⊆ s_bucket α T b`
        have "suffix_type T x = S_type" "α (T ! x) = b"
          by (simp add: s_bucket_def bucket_def)+

        have "x ∉ ?B"
          using ‹x ∈ ?A› by blast

        from `Suc x ∈ ?B ∨ (∃b'. b < b' ∧ Suc x ∈ bucket α T b')`
        have False
        proof
          assume "Suc x ∈ ?B"
          from nth_mem_list_slice[OF `Suc x ∈ ?B`]
          obtain i' where
            "i' < length SA"
            "B ! b ≤ i'"
            "i' < bucket_end α T b"
            "SA ! i' = Suc x"
            by blast

          have "i ≠ i'"
          proof (rule ccontr)
            assume "¬ i ≠ i'"
            hence "i = i'"
              by auto
            hence "j = x"
              using ‹SA ! i' = Suc x› assms(16,18) by auto
            with assms(19) `suffix_type T x = _`
            show False
              by simp
          qed
          with `B ! b ≤ i'` `i = B ! b`
          have "i < i'"
            using nat_less_le by blast
          with s_suc_invD[OF assms(7) `i' < length SA ` _ `SA ! i' = _` `suffix_type T x = _`]
               `α (T ! x) = b`
          obtain k where
            "in_s_current_bucket α T B b k"
            "SA ! k = x"
            "k < i'"
            by blast
          hence "x ∈ ?B"
            by (meson assms(11) in_s_current_bucket_list_slice)
          with `x ∉ ?B`
          show False
            by blast
        next
          assume "∃b'. b < b' ∧ Suc x ∈ bucket α T b'"
          then obtain b' where
            "b < b'"
            "Suc x ∈ bucket α T b'"
            by blast
          hence "b' ≤ α (Max (set T))"
            by (metis (mono_tags, lifting) Max_greD assms(8) bucket_def mem_Collect_eq
                  strict_mono_less_eq)

          have "suffix_type T (Suc x) = S_type ∨ suffix_type T (Suc x) = L_type"
            by (simp add: suffix_type_def)
          hence "Suc x ∈ l_bucket α T b' ∨ Suc x ∈ s_bucket α T b'"
            using ‹Suc x ∈ bucket α T b'› l_bucket_def s_bucket_def by fastforce
          moreover
          have "Suc x ∈ l_bucket α T b' ⟹ False"
          proof -
            assume "Suc x ∈ l_bucket α T b'"
            with l_types_initD(1)[OF l_types_init_maintained[OF assms(2,4,10-12)] `b' ≤ _`]
            have "Suc x ∈ set (list_slice SA (bucket_start α T b') (l_bucket_end α T b'))"
              by blast
            with nth_mem_list_slice[of "Suc x"]
            obtain i' where
              "i' < length SA"
              "bucket_start α T b' ≤ i'"
              "i' < l_bucket_end α T b'"
              "SA ! i' = Suc x"
              by blast

            have "i ≠ i'"
            proof (rule ccontr)
              assume "¬ i ≠ i'"
              hence "i = i'"
                by auto
              hence "j = x"
                using ‹SA ! i' = Suc x› assms(16,18) by auto
              with assms(19) `suffix_type T x = _`
              show False
                by simp
            qed
            moreover
            from `b < b'`
            have "bucket_end α T b ≤ bucket_start α T b'"
              by (simp add: less_bucket_end_le_start)
            hence "B ! b ≤ i'"
              using s_bucket_ptr_upper_bound[OF assms(2) `b ≤ α (Max (set T))`]
                    `bucket_start α T b' ≤ i'`
              by linarith
            ultimately have "i < i'"
              using ‹i = B ! b› nat_less_le by blast
            with s_suc_invD[OF assms(7) `i' < length SA ` _ `SA ! i' = _` `suffix_type T x = _`]
                 `α (T ! x) = b`
            obtain k where
              "in_s_current_bucket α T B b k"
              "SA ! k = x"
              "k < i'"
              by blast
            hence "x ∈ ?B"
              by (meson assms(11) in_s_current_bucket_list_slice)
            with `x ∉ ?B`
            show False
              by blast
          qed
          moreover
          have "Suc x ∈ s_bucket α T b' ⟹ False"
          proof -
            assume "Suc x ∈ s_bucket α T b'"

            have "i ≤ bucket_end α T b"
              by (simp add: Suc_le_eq ‹k < bucket_end α T b› ‹n = k› assms(16))
            hence "i ≤ bucket_start α T b'"
              using ‹b < b'› less_bucket_end_le_start order.trans by blast
            hence "i ≤ B ! b'"
              using s_bucket_ptr_lower_bound[OF assms(2) `b' ≤ _`]
              by (metis l_bucket_end_def le_trans nat_le_iff_add s_bucket_start_eq_l_bucket_end)
            hence "i < B ! b' ∨ i = B ! b'"
              using nat_less_le by blast
            hence "B ! b' = s_bucket_start α T b'"
            proof
              assume "i < B ! b'"
              with s_B_val[OF assms(1-6,8,10-13,15) `b' ≤ _`]
              show "B ! b' = s_bucket_start α T b'"
                by blast
            next
              assume "i = B ! b'"
              with s_bucket_ptr_lower_bound[OF assms(2) `b' ≤ _`]
                   `i ≤ bucket_start α T b'`
              show "B ! b' = s_bucket_start α T b'"
                by (simp add: s_bucket_start_def)
            qed

            let ?ys = "list_slice SA (s_bucket_start α T b') (bucket_end α T b')"

            from distinct_card[OF s_distinct_invD[OF assms(1) `b' ≤ _`],
                  simplified `B ! b' = s_bucket_start _ _ _`]
            have "card (set ?ys) = card (s_bucket α T b')"
              by (metis add_diff_cancel_left' assms(11) bucket_end_eq_s_start_pl_size
                    bucket_end_le_length length_list_slice min_def s_bucket_size_def)
            with card_subset_eq[
                  OF finite_s_bucket s_locations_inv_subset_s_bucket[OF assms(3) `b' ≤ _`],
                  simplified `B ! b' = s_bucket_start α T b'`]
            have "set ?ys = s_bucket α T b'"
              by blast
            with `Suc x ∈ s_bucket α T b'`
            have "Suc x ∈ set ?ys"
              by simp
            with nth_mem_list_slice[of "Suc x"]
            obtain i' where
              "i' < length SA"
              "s_bucket_start α T b' ≤ i'"
              "i' < bucket_end α T b'"
              "SA ! i' = Suc x"
              by blast

            have "i ≠ i'"
            proof (rule ccontr)
              assume "¬ i ≠ i'"
              hence "i = i'"
                by auto
              hence "j = x"
                using ‹SA ! i' = Suc x› assms(16,18) by auto
              with assms(19) `suffix_type T x = _`
              show False
                by simp
            qed
            moreover
            have "i ≤ i'"
              using ‹B ! b' = s_bucket_start α T b'› ‹i ≤ B ! b'› ‹s_bucket_start α T b' ≤ i'›
              by linarith
            ultimately have "i < i'"
              using dual_order.order_iff_strict by blast
            with s_suc_invD[OF assms(7) `i' < length SA ` _ `SA ! i' = _` `suffix_type T x = _`]
                 `α (T ! x) = b`
            obtain k where
              "in_s_current_bucket α T B b k"
              "SA ! k = x"
              "k < i'"
              by blast
            hence "x ∈ ?B"
              by (meson assms(11) in_s_current_bucket_list_slice)
            with `x ∉ ?B`
            show False
              by blast
          qed
          ultimately show False
            by blast
        qed
        then show ?thesis
          by blast
      qed
      ultimately show ?thesis
        by blast
    qed
    ultimately show ?thesis
      by blast
  qed
  moreover
  have "Suc n ≤ k ⟹ ?g1 ∧ ?g2 ∧ ?g3"
  proof -
    assume "Suc n ≤ k"
    with s_seen_invD[OF assms(5) `k < length SA`] assms(16)
    show ?thesis
      by blast
  qed
  ultimately show "?g1 ∧ ?g2 ∧ ?g3"
    by blast
qed

corollary s_seen_inv_maintained_perm_step_c3:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = L_type"
shows "s_seen_inv α T B SA n"
  using s_seen_inv_maintained_step_c3[OF s_perm_inv_elims[OF assms(1)] assms(2-)]
  by blast

lemma s_seen_inv_maintained_step_c4:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "s_suc_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "Suc 0 < length T"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_seen_inv α T (B[b := k]) (SA[k := j]) n"
  unfolding s_seen_inv_def
proof(intro allI impI)
  fix i'
  assume "i' < length (SA[k := j])" "n ≤ i'"

  let ?g1 = "(suffix_type T (SA[k := j] ! i') = S_type ⟶
              in_s_current_bucket α T (B[b := k]) (α (T ! (SA[k := j] ! i'))) i')" and
      ?g2 = "(suffix_type T (SA[k := j] ! i') = L_type ⟶
              in_l_bucket α T (α (T ! (SA[k := j] ! i'))) i')" and
      ?g3 = "SA[k := j] ! i' < length T"

  from s_bucket_ptr_strict_lower_bound[OF assms(1-6,8,10-14,16-20)]
  have "s_bucket_start α T b < B ! b".
  hence "s_bucket_start α T b ≤ k"
    using assms(21) by linarith
  hence "bucket_start α T b ≤ k"
    using bucket_start_le_s_bucket_start le_trans by blast

  from `s_bucket_start α T b < B ! b`
  have "k < B ! b"
    using assms(21) by linarith

  have "j < length T"
    by (simp add: assms(19) suffix_type_s_bound)
  hence "b ≤ α (Max (set T))"
    by (simp add: assms(8,20) strict_mono_less_eq)
  with s_bucket_ptr_upper_bound[OF assms(2)]
  have "B ! b ≤ bucket_end α T b"
    by blast
  with `k < B ! b`
  have "k < bucket_end α T b"
    by linarith

  have "B ! b ≤ i"
  proof(rule ccontr)
    assume "¬B ! b ≤ i"
    hence "i < B ! b"
      by simp
    with s_B_val[OF assms(1-6,8,10-13,15) `b ≤ α _`]
    have "B ! b = s_bucket_start α T b" .
    with `s_bucket_start α T b < B ! b`
    show False
      by linarith
  qed
  hence "k < i"
    using ‹k < B ! b› less_le_trans by blast

  have "k = i' ⟹ n = i'"
    using ‹k < i› ‹n ≤ i'› assms(16) le_less_Suc_eq by blast

  have "k ≤ i'"
    using ‹k < i› ‹n ≤ i'› assms(16) by linarith

  have "i' < length T"
    using ‹i' < length (SA[k := j])› assms(11) by auto
  with index_in_bucket_interval_gen[OF _ assms(8), of i' T]
  obtain b' where
    "b' ≤ α (Max (set T))"
    "bucket_start α T b' ≤ i'"
    "i' < bucket_end α T b'"
    by blast
  hence "n < bucket_end α T b'"
    using ‹n ≤ i'› dual_order.strict_trans2 by blast
  hence "i ≤ bucket_end α T b'"
    using assms(16) by linarith

  have "b ≤ b'"
  proof (rule ccontr)
    assume "¬b ≤ b'"
    hence "b' < b"
      by linarith
    hence "bucket_end α T b' ≤ bucket_start α T b"
      by (simp add: less_bucket_end_le_start)
    with `i ≤ bucket_end α T b'` `bucket_start α T b ≤ k` `k < B ! b`
    have "i < B ! b"
      by linarith
    with `B ! b ≤ i`
    show False
      by linarith
  qed

  have "in_s_current_bucket α T (B[b := k]) b k"
    unfolding in_s_current_bucket_def
    using ‹b ≤ α (Max (set T))› ‹k < bucket_end α T b› assms(9) by auto

  have "b < b' ⟹ ?g1 ∧ ?g2 ∧ ?g3"
  proof -
    assume "b < b'"
    hence "bucket_end α T b ≤ bucket_start α T b'"
      by (simp add: less_bucket_end_le_start)
    with `k < bucket_end _ _ b` `bucket_start _ _ b' ≤ i'`
    have "k < i'"
      by linarith
    hence "SA[k := j] ! i' = SA ! i'"
      by simp

    from `b < b'`
    have "B[b := k] ! b' = B ! b'"
      by simp

    have "i' < l_bucket_end α T b' ∨ B ! b' ≤ i' ∨ (s_bucket_start α T b' ≤ i' ∧ i' < B ! b')"
      by (metis not_le s_bucket_start_eq_l_bucket_end)
    moreover
    have "B ! b' ≤ i' ⟹ ?thesis"
    proof -
      assume "B ! b' ≤ i'"
      with s_locations_invD[OF assms(3) `b' ≤ _` _ `i' < bucket_end _ _ _`]
      have "SA ! i' ∈ s_bucket α T b'" .
      hence "suffix_type T (SA ! i') = S_type" "α (T ! (SA ! i')) = b'" "SA ! i' < length T"
        by (simp add: s_bucket_def bucket_def)+
      moreover
      from `B[b := k] ! b' = B ! b'` `b' ≤ α _` `B ! b' ≤ i'` `i' < bucket_end α T b'`
      have "in_s_current_bucket α T (B[b := k]) b' i'"
        by (simp add: in_s_current_bucket_def)
      ultimately show ?thesis
        by (simp add: `SA[k := j] ! i' = SA ! i'`)
    qed
    moreover
    have "i' < l_bucket_end α T b' ⟹ ?thesis"
    proof -
      assume "i' < l_bucket_end α T b'"
      hence "in_l_bucket α T b' i'"
        by (simp add: `bucket_start α T b' ≤ i'` `b' ≤ α _` in_l_bucket_def)
      moreover
      from l_types_init_nth[OF assms(11) l_types_init_maintained[OF assms(2,4,10-12)]
            `b' ≤ α _` `bucket_start _ _ _ ≤ i'` `i' < l_bucket_end _ _ _`]
      have "SA ! i' ∈ l_bucket α T b'" .
      hence "SA ! i' < length T" "α (T ! (SA ! i')) = b'" "suffix_type T (SA ! i') = L_type"
        by (simp add: l_bucket_def bucket_def)+
      ultimately show ?thesis
        using `SA[k := j] ! i' = SA ! i'`
        by simp
    qed
    moreover
    have "⟦s_bucket_start α T b' ≤ i'; i' < B ! b'⟧ ⟹ ?thesis"
    proof -
      assume "s_bucket_start α T b' ≤ i'" "i' < B ! b'"
      have "B ! b' = i"
      proof (rule ccontr)
        assume "B ! b' ≠ i"
        hence "i < B ! b' ∨ B ! b' < i"
          by linarith
        moreover
        have "B ! b' < i ⟹ False"
          using `i' < B ! b'` ‹n ≤ i'› assms(16) by linarith
        moreover
        have "i < B ! b' ⟹ False"
        proof -
          assume "i < B ! b'"
          with s_B_val[OF assms(1-6,8,10-13,15) `b' ≤ α _`]
          have "B ! b' = s_bucket_start α T b'" .
          with `s_bucket_start α T b' ≤ i'` `i' < B ! b'`
          show False
            by linarith
        qed
        ultimately show False
          by linarith
      qed

      have "s_bucket_start α T b' < B ! b'"
        using ‹i' < B ! b'› ‹s_bucket_start α T b' ≤ i'› by linarith
      hence "s_bucket_start α T b' < bucket_end α T b'"
        using ‹B ! b' = i› ‹i ≤ bucket_end α T b'› order.strict_trans2 by blast
      hence "s_bucket α T b' ≠ {}"
        by (metis add.commute bucket_end_eq_s_start_pl_size distinct_card distinct_conv_nth
              empty_set less_irrefl_nat less_nat_zero_code list.size(3) plus_nat.add_0
              s_bucket_size_def)

      have "bucket_end α T b' ≤ length SA"
        by (simp add: assms(11) bucket_end_le_length)

      let ?xs = "list_slice SA (B ! b') (bucket_end α T b')"

      have "set ?xs ⊂ s_bucket α T b'"
      proof
        from s_locations_inv_subset_s_bucket[OF assms(3) `b' ≤ _`]
        show "set ?xs ⊆ s_bucket α T b'" .
      next
        from `s_bucket_start α T b' < B ! b'` `s_bucket_start α T b' < bucket_end α T b'`
        have "bucket_end α T b' - B ! b' < bucket_end α T b' - s_bucket_start α T b'"
          using diff_less_mono2 by blast
        hence "length ?xs < s_bucket_size α T b'"
          by (metis ‹bucket_end α T b' ≤ length SA› add_diff_cancel_left'
                bucket_end_eq_s_start_pl_size length_list_slice min_def)
        hence "card (set ?xs) ≠ card (s_bucket α T b')"
          by (metis card_length not_le s_bucket_size_def)
        then show "set ?xs ≠ s_bucket α T b'"
          by auto
      qed

      have P0: "∀i0 < length T. α (T ! i0) = b' ⟶ T ! i0 ≠ bot"
        using ‹b < b'› assms(8,20) strict_mono_less by fastforce
      hence P1: "∀i0 < length T. α (T ! i0) = b' ⟶ Suc i0 < length T"
        by (metis Suc_leI assms(13) diff_Suc_1 last_conv_nth le_imp_less_or_eq length_greater_0_conv
              valid_list_def)

      let ?S = "s_bucket α T b' - set ?xs"

      from `set ?xs ⊂ s_bucket α T b'`
      have "?S ≠ {}"
        by blast
      have "?S ⊆ s_bucket α T b'"
        by blast
      hence P2: "∀x ∈ ?S. α (T ! x) = b' ∧ suffix_type T x = S_type ∧ x < length T"
        by (simp add: bucket_def s_bucket_def)

      have P3: "∀x ∈ ?S. Suc x < length T ∧ α (T ! Suc x) ≥ b'"
      proof
        fix x
        assume "x ∈ ?S"
        with P2
        have "α (T ! x) = b'" "suffix_type T x = S_type" "x < length T"
          by blast+
        with P1
        have "Suc x < length T"
          by blast
        moreover
        from `suffix_type T x = S_type` `x < length T`
        have "T ! x ≤ T ! Suc x"
          using calculation nth_gr_imp_l_type by fastforce
        hence "α (T ! Suc x) ≥ b'"
          using ‹α (T ! x) = b'› assms(8) strict_mono_leD by blast
        ultimately show "Suc x < length T ∧ α (T ! Suc x) ≥ b'"
          by blast
      qed

      have "finite ?S"
        by (simp add: finite_s_bucket)

      have "∃x ∈ ?S. α (T ! Suc x) > b' ∨ Suc x ∈ set ?xs"
      proof (rule ccontr)
        assume "¬ (∃x ∈ ?S. b' < α (T ! Suc x) ∨ Suc x ∈ set ?xs)"
        hence "∀x ∈ ?S. α (T ! Suc x) ≤ b' ∧ Suc x ∉ set ?xs"
          using not_le_imp_less by blast
        with P3
        have P4: "∀x ∈ ?S. α (T ! Suc x) = b' ∧ Suc x ∉ set ?xs"
          using dual_order.antisym by blast
        hence P5: "∀x ∈ ?S. suffix_type T (Suc x) = S_type"
          by (metis P2 P3 assms(8) strict_mono_eq suffix_type_neq)
        hence P6: "∀x ∈ ?S. Suc x ∈ ?S"
          by (metis (mono_tags, lifting) Diff_iff P3 P4 bucket_def mem_Collect_eq s_bucket_def)
        with `?S ≠ {}` `finite ?S`
        show False
          using Suc_le_lessD infinite_growing by blast
      qed
      then obtain x where
        "x ∈ ?S"
        "α (T ! Suc x) > b' ∨ Suc x ∈ set ?xs"
        by blast
      with P3
      have "Suc x < length T"
        by blast

      from `x ∈ ?S`
      have "suffix_type T x = S_type" "α (T ! x) = b'" "x < length T"
        using P2 by blast+

      have P4: "∀b0 ≤ α (Max (set T)). b' < b0 ⟶ B ! b0 = s_bucket_start α T b0"
      proof(safe)
        fix b0
        assume "b0 ≤ α (Max (set T))" "b' < b0"
        hence "bucket_end α T b' ≤ bucket_start α T b0"
          by (simp add: less_bucket_end_le_start)
        with s_bucket_ptr_upper_bound[OF assms(2) `b' ≤ _ `]
             s_bucket_ptr_lower_bound[OF assms(2) `b0 ≤ _ `]
        have "B ! b' ≤ B ! b0"
          by (meson bucket_start_le_s_bucket_start le_trans)
        hence "B ! b' = B ! b0 ∨ B ! b' < B ! b0"
          by linarith
        moreover
        have "B ! b' = B ! b0 ⟹ B ! b0 = s_bucket_start α T b0"
          by (metis ‹B ! b' = i› ‹bucket_end α T b' ≤ bucket_start α T b0› le_trans
              ‹i ≤ bucket_end α T b'› ‹s_bucket_start α T b0 ≤ B ! b0›  dual_order.antisym
                bucket_start_le_s_bucket_start)
        moreover
        have "B ! b' < B ! b0 ⟹ i < B ! b0"
          by (simp add: ‹B ! b' = i›)
        with s_B_val[OF assms(1-6,8,10-13,15) `b0 ≤ _`]
        have "B ! b' < B ! b0 ⟹ B ! b0 = s_bucket_start α T b0"
          by blast
        ultimately show "B ! b0 = s_bucket_start α T b0"
          by blast
      qed

      from `α (T ! Suc x) > b' ∨ Suc x ∈ set ?xs`
      show ?thesis
      proof
        let ?b = "α (T ! Suc x)"
        let ?ys = "list_slice SA (bucket_start α T ?b) (l_bucket_end α T ?b)"
        and ?zs = "list_slice SA (s_bucket_start α T ?b) (bucket_end α T ?b)"

        assume "b' < ?b"
        with P4 `Suc x < length T`
        have "B ! ?b = s_bucket_start α T ?b"
          by (simp add: assms(8) strict_mono_less_eq)

        from `Suc x < length T`
        have "?b ≤ α (Max (set T))"
          by (simp add: assms(8) strict_mono_leD)

        have "bucket_end α T b' ≤ bucket_start α T ?b"
          using ‹b' < α (T ! Suc x)› less_bucket_end_le_start by blast
        hence "i ≤ bucket_start α T ?b"
          using ‹i ≤ bucket_end α T b'› order.trans by blast

        have "set ?zs = s_bucket α T ?b"
        proof (rule card_subset_eq[OF finite_s_bucket])
          show "set ?zs ⊆ s_bucket α T ?b"
            by (metis Max_greD ‹B ! ?b = s_bucket_start α T ?b› ‹Suc x < length T› assms(3,8)
                  s_locations_inv_subset_s_bucket strict_mono_leD)
        next
          from distinct_card[OF s_distinct_invD[OF assms(1) `?b ≤ _`]]
               `B ! ?b = s_bucket_start α T ?b`
          have "card (set ?zs) = length ?zs"
            by simp
          moreover
          have "length ?zs = bucket_end α T ?b - s_bucket_start α T ?b"
            by (metis assms(11) bucket_end_le_length length_list_slice min_def)
          moreover
          have "s_bucket_size α T ?b = bucket_end α T ?b - s_bucket_start α T ?b"
            by (simp add: bucket_end_eq_s_start_pl_size)
          hence "card (s_bucket α T ?b) = bucket_end α T ?b - s_bucket_start α T ?b"
            by (simp add: s_bucket_size_def)
          ultimately show "card (set ?zs) = card (s_bucket α T ?b)"
            by simp
        qed

        have "suffix_type T (Suc x) = L_type ⟹ ?thesis"
        proof -
          assume "suffix_type T (Suc x) = L_type"
          with l_types_initD(1)[OF l_types_init_maintained[OF assms(2,4,10-12)] `?b ≤ _`]
          have "Suc x ∈ set ?ys"
            by (simp add: ‹Suc x < length T› bucket_def l_bucket_def)

          from nth_mem_list_slice[OF `Suc x ∈ set ?ys`]
          obtain i0 where
            "i0 < length SA"
            "bucket_start α T ?b ≤ i0"
            "i0 < l_bucket_end α T ?b"
            "SA ! i0 = Suc x"
            by blast
          hence "i ≤ i0"
            using ‹i ≤ bucket_start α T ?b› dual_order.trans by blast
          hence "i = i0 ∨ i < i0"
            by linarith
          then show ?thesis
          proof
            assume "i = i0"
            hence "x = j"
              using ‹SA ! i0 = Suc x› assms(16,18) by auto
            then show ?thesis
              using ‹α (T ! x) = b'› ‹b < b'› assms(20) by blast
          next
            assume "i < i0"
            with s_suc_invD[OF assms(7) `i0 < length _` _ `SA ! i0 = _` `suffix_type T x = S_type`]
                 `α (T ! x) = b'`
            obtain i1 where
              "in_s_current_bucket α T B b' i1"
              "SA ! i1 = x"
              "i1 < i0"
              by auto
            with in_s_current_bucket_list_slice[OF assms(11)]
            have "x ∈ set ?xs"
              by blast
            then show ?thesis
              using ‹x ∈ ?S› by blast
          qed
        qed
        moreover
        have "suffix_type T (Suc x) = S_type ⟹ ?thesis"
        proof -
          assume "suffix_type T (Suc x) = S_type"
          with `set ?zs = s_bucket α T ?b` `Suc x < length T`
          have "Suc x ∈ set ?zs"
            by (simp add: s_bucket_def bucket_def)

          from nth_mem_list_slice[OF `Suc x ∈ set ?zs`]
          obtain i0 where
            "i0 < length SA"
            "s_bucket_start α T ?b ≤ i0"
            "i0 < bucket_end α T ?b"
            "SA ! i0 = Suc x"
            by blast
          hence "i ≤ i0"
            by (meson ‹i ≤ bucket_start α T ?b› bucket_start_le_s_bucket_start dual_order.trans)
          hence "i = i0 ∨ i < i0"
            by linarith
          then show ?thesis
          proof
            assume "i = i0"
            hence "x = j"
              using ‹SA ! i0 = Suc x› assms(16,18) by auto
            then show ?thesis
              using ‹α (T ! x) = b'› ‹b < b'› assms(20) by blast
          next
            assume "i < i0"
            with s_suc_invD[OF assms(7) `i0 < length _` _ `SA ! i0 = _` `suffix_type T x = S_type`]
                 `α (T ! x) = b'`
            obtain i1 where
              "in_s_current_bucket α T B b' i1"
              "SA ! i1 = x"
              "i1 < i0"
              by auto
            with in_s_current_bucket_list_slice[OF assms(11)]
            have "x ∈ set ?xs"
              by blast
            then show ?thesis
              using ‹x ∈ ?S› by blast
          qed
        qed
        ultimately show ?thesis
          using SL_types.exhaust by blast
      next
        assume "Suc x ∈ set ?xs"

        from nth_mem_list_slice[OF `Suc x ∈ set ?xs`]
        obtain i0 where
          "i0 < length SA"
          "B ! b' ≤ i0"
          "i0 < bucket_end α T b'"
          "SA ! i0 = Suc x"
          by blast
        with `B ! b' = i`
        have "i ≤ i0"
          by blast
        hence "i = i0 ∨ i < i0"
          by linarith
        then show ?thesis
        proof
          assume "i = i0"
          hence "x = j"
            using ‹SA ! i0 = Suc x› assms(16,18) by auto
          then show ?thesis
            using ‹α (T ! x) = b'› ‹b < b'›  assms(20) by blast
        next
          assume "i < i0"
          with s_suc_invD[OF assms(7) `i0 < length _` _ `SA ! i0 = _` `suffix_type T x = _`]
               `α (T ! x) = b'`
          obtain i1 where
            "in_s_current_bucket α T B b' i1"
            "SA ! i1 = x"
            "i1 < i0"
            by blast
          with in_s_current_bucket_list_slice[OF assms(11)]
          have "x ∈ set ?xs"
            by blast
          then show ?thesis
            using ‹x ∈ ?S› by blast
        qed
      qed
    qed
    ultimately show ?thesis
      by linarith
  qed
  moreover
  have "b = b' ⟹ ?g1 ∧ ?g2 ∧ ?g3"
  proof -
    assume "b = b'"
    have "k = i' ⟹ ?thesis"
    proof -
      assume "k = i'"
      hence "SA[k := j] ! i' = j"
        using ‹i' < length (SA[k := j])› by auto
      with `suffix_type T j = S_type` `j < length T` `in_s_current_bucket α T (B[b := k]) b k`
           assms(20) `k = i'`
      show ?thesis
        by simp
    qed
    moreover
    have "k < i' ⟹ ?thesis"
    proof -
      assume "k < i'"
      hence "B ! b ≤ i'"
        using assms(21) by linarith
      with s_locations_invD[OF assms(3) `b' ≤ α _` _ `i' < bucket_end _ _ _`] `b = b'`
      have "SA ! i' ∈ s_bucket α T b'"
        by blast
      hence "suffix_type T (SA ! i') = S_type" "α (T ! (SA ! i')) = b'"
        by (simp add: s_bucket_def bucket_def)+
      moreover
      have "SA[k := j] ! i' = SA ! i'"
        using `k < i'` by simp
      moreover
      have "in_s_current_bucket α T (B[b := k]) b' i'"
        by (metis (no_types, lifting) ‹b = b'› ‹b' ≤ α (Max (set T))› ‹i' < bucket_end α T b'›
              ‹k ≤ i'› assms(9) dual_order.strict_trans2 in_s_current_bucket_def nth_list_update_eq)
      ultimately show ?thesis
        by (simp add: suffix_type_s_bound)
    qed
    ultimately show ?thesis
      using `k ≤ i'` dual_order.order_iff_strict by blast
  qed
  ultimately show "?g1 ∧ ?g2 ∧ ?g3"
    using ‹b ≤ b'› dual_order.order_iff_strict by blast
qed

corollary s_seen_inv_maintained_perm_step_c4:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_seen_inv α T (B[b := k]) (SA[k := j]) n"
  using s_seen_inv_maintained_step_c4[OF s_perm_inv_elims[OF assms(1)] assms(2-)]
  by blast

lemmas s_seen_inv_maintained_perm_step =
  s_seen_inv_maintained_perm_step_c1
  s_seen_inv_maintained_perm_step_c2
  s_seen_inv_maintained_perm_step_c3
  s_seen_inv_maintained_perm_step_c4

subsubsection "Predecessor"

lemma s_pred_inv_established:
  assumes "s_bucket_init α T B"
shows "s_pred_inv α T B SA n"
  unfolding s_pred_inv_def
proof (safe)
  fix b i
  assume A: "in_s_current_bucket α T B b i" "0 < b"

  let ?goal = "∃j<length SA. SA ! j = Suc (SA ! i) ∧ i < j ∧ n < j"

  have "b = 0 ∨ 0 < b"
    by blast
  moreover
  from A(2)
  have "b = 0 ⟹ ?goal"
    by blast
  moreover
  have "0 < b ⟹ ?goal"
  proof -
    assume "0 < b"
    with s_bucket_initD(1)[OF assms(1) in_s_current_bucketD(1)[OF A(1)]]
    have "B ! b = bucket_end α T b" .
    with in_s_current_bucketD(2,3)[OF A(1)]
    show ?goal
      by linarith
  qed
  ultimately show ?goal
    by blast
qed

lemma s_pred_inv_maintained_step_alt:
  assumes "s_pred_inv α T B SA i"
  and     "i = Suc n"
shows "s_pred_inv α T B SA n"
  unfolding s_pred_inv_def
proof (intro allI impI; elim conjE)
  fix b i'
  assume "in_s_current_bucket α T B b i'" "b ≠ 0"
  with s_pred_invD[OF assms(1), of b i'] assms(2)
  show  "∃j<length SA. SA ! j = Suc (SA ! i') ∧ i' < j ∧ n < j"
    using Suc_lessD by blast
qed

corollary s_pred_inv_maintained_perm_step_alt:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
shows "s_pred_inv α T B SA n"
  using s_pred_inv_maintained_step_alt[OF s_perm_inv_elims(6), OF assms]
  by blast

lemma s_pred_inv_maintained_step:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "s_suc_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "Suc 0 < length T"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_pred_inv α T (B[b := k]) (SA[k := j]) n"
  unfolding s_pred_inv_def
proof(safe)
  fix b' i'
  assume "in_s_current_bucket α T (B[b := k]) b' i'" "0 < b'"
  hence "b' ≠ 0"
    by linarith

  let ?goal = "∃j'<length (SA[k := j]). SA[k := j] ! j' = Suc (SA[k := j] ! i') ∧ i' < j' ∧ n < j'"

  from s_bucket_ptr_strict_lower_bound[OF assms(1-6,8,10-14,16-20)]
  have "s_bucket_start α T b < B ! b".
  hence "s_bucket_start α T b ≤ k"
    using assms(21) by linarith
  hence "bucket_start α T b ≤ k"
    using bucket_start_le_s_bucket_start le_trans by blast

  from `s_bucket_start α T b < B ! b`
  have "k < B ! b"
    using assms(21) by linarith

  have "j < length T"
    by (simp add: assms(19) suffix_type_s_bound)
  hence "b ≤ α (Max (set T))"
    by (simp add: assms(8,20) strict_mono_less_eq)
  with s_bucket_ptr_upper_bound[OF assms(2)]
  have "B ! b ≤ bucket_end α T b"
    by blast
  with `k < B ! b`
  have "k < bucket_end α T b"
    by linarith

  have "B ! b ≤ i"
  proof(rule ccontr)
    assume "¬B ! b ≤ i"
    hence "i < B ! b"
      by simp
    with s_B_val[OF assms(1-6,8,10-13,15) `b ≤ α (Max (set T))`] `s_bucket_start α T b < B ! b`
    show False
      by simp
  qed
  with `k < B ! b`
  have "k < i"
    by linarith

  have "b ≠ b' ⟹ ?goal"
  proof -
    assume "b ≠ b'"
    hence "B[b := k] ! b' = B ! b'"
      by simp
    with `in_s_current_bucket α T (B[b := k]) b' i'`
    have "in_s_current_bucket α T B b' i'"
      by (simp add: in_s_current_bucket_def)
    with s_pred_invD[OF assms(6) _ `b' ≠ 0`]
    obtain j' where
      "j' < length SA"
      "SA ! j' = Suc (SA ! i')"
      "i' < j'"
      "i < j'"
      by blast
    moreover
    from `in_s_current_bucket α T B b' i'`
    have "B ! b' ≤ i'" "i' < bucket_end α T b'"
      by (simp_all add: in_s_current_bucket_def)
    with s_bucket_ptr_lower_bound[OF assms(2)]
         in_s_current_bucketD(1)[OF `in_s_current_bucket _ _ B _ _`]
    have "bucket_start α T b' ≤ i'"
      by (meson bucket_start_le_s_bucket_start le_trans)
    with outside_another_bucket[OF `b ≠ b'` `bucket_start _ _ _ ≤ k` `k < bucket_end _ _ _`]
         `i' < bucket_end α T b'`
    have "k ≠ i'"
      by blast
    hence "SA[k := j] ! i' = SA ! i'"
      by simp
    moreover
    from `i < j'` assms(16)
    have "n < j'"
      using Suc_lessD by blast
    moreover
    have "SA[k := j] ! j' = SA ! j'"
      using ‹k < i› calculation(4) by auto
    ultimately show ?thesis
      by auto
  qed
  moreover
  have "b = b' ⟹ ?goal"
  proof -
    assume "b = b'"
    hence "B[b := k] ! b' = k"
      using ‹b ≤ α (Max (set T))› assms(9) by auto

    have "k = i' ⟹ ?goal"
    proof -
      assume "k = i'"
      hence "SA[k := j] ! i' = j"
        using ‹k < i› assms(16,17) by auto
      moreover
      have "SA[k := j] ! i = SA ! i"
        using ‹k < i› by auto
      ultimately show ?goal
        using assms(16-18) `k = i'` `k < i`
        by auto
    qed
    moreover
    have "k ≠ i' ⟹ ?goal"
    proof -
      assume "k ≠ i'"
      with `in_s_current_bucket α T (B[b := k]) b' i'` `B[b := k] ! b' = k`
      have "k < i'"
        by (simp add: in_s_current_bucket_def)
      hence "B ! b' ≤ i'"
        using assms(21) `b = b'` `k < B ! b` by simp
      hence "in_s_current_bucket α T B b' i'"
        using ‹in_s_current_bucket α T (B[b := k]) b' i'› in_s_current_bucket_def by blast
      with s_pred_invD[OF assms(6) _ `b' ≠ 0`]
      obtain j' where
        "j' < length SA"
        "SA ! j' = Suc (SA ! i')"
        "i' < j'"
        "i < j'"
        by blast
      moreover
      have "SA[k := j] ! i' = SA ! i'"
        using `k ≠ i'` by simp
      moreover
      have "SA[k := j] ! j' = SA ! j'"
        using `k < i'` `i' < j'`
        by auto
      ultimately show ?goal
        using assms(16) by auto
    qed
    ultimately show ?goal
      by blast
  qed
  ultimately show ?goal
    by blast
qed

corollary s_pred_inv_maintained_perm_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_pred_inv α T (B[b := k]) (SA[k := j]) n"
  using s_pred_inv_maintained_step[OF s_perm_inv_elims[OF assms(1)] assms(2-)]
  by blast

subsubsection "Successor"

lemma s_suc_inv_established:
  assumes "length SA = length T"
  and     "length T ≤ n"
shows "s_suc_inv α T B SA n"
  unfolding s_suc_inv_def
  using assms(1) assms(2) by linarith

lemma s_suc_inv_maintained_step_c1:
  assumes "length SA ≤ Suc n"
shows "s_suc_inv α T B SA n"
  unfolding s_suc_inv_def
proof (intro allI impI; elim conjE)
  fix i' j
  assume "i' < length SA" "n < i'" "SA ! i' = Suc j" "suffix_type T j = S_type"
  with assms
  have False
    using less_trans_Suc not_less by blast
  then show "∃k. in_s_current_bucket α T B (α (T ! j)) k ∧ SA ! k = j ∧ k < i'"
    by blast
qed

corollary s_suc_inv_maintained_perm_step_c1:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "length SA ≤ Suc n"
shows "s_suc_inv α T B SA n"
  by (simp add: assms(3) s_suc_inv_maintained_step_c1)

lemma s_suc_inv_maintained_step_c1_alt:
  assumes "s_suc_inv α T B SA i"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "valid_list T"
  and     "α bot = 0"
  and     "i = Suc n"
  and     "length T ≤ SA ! Suc n"
  shows "s_suc_inv α T B SA n"
proof (cases "length SA ≤ Suc n")
  case True
  then show ?thesis
    by (simp add: s_suc_inv_maintained_step_c1)
next
  case False
  hence "Suc n < length SA"
    by simp
  show ?thesis
    unfolding s_suc_inv_def
  proof (intro allI impI; elim conjE)
    fix i' j
    let ?goal = "∃k. in_s_current_bucket α T B (α (T ! j)) k ∧ SA ! k = j ∧ k < i'"
    assume "i' < length SA" "n < i'" "SA ! i' = Suc j" "suffix_type T j = S_type"
    hence "i' = Suc n ∨ Suc n < i'"
      using Suc_lessI by blast
    moreover
    from s_suc_invD[OF assms(1) ‹i' < length SA› _ ‹SA ! i' = Suc j› ‹suffix_type T j = S_type›]
    have "Suc n < i' ⟹ ?goal"
      using ‹i = Suc n› by blast
    moreover
    have "i' = Suc n ⟹ ?goal"
    proof -
      assume "i' = Suc n"
      have "j < length T ∨ length T ≤ j"
        using linorder_not_le by blast
      moreover
      have "length T ≤ j ⟹ ?goal"
        by (meson ‹suffix_type T j = S_type› linorder_not_le suffix_type_s_bound)
      moreover
      have "j < length T ⟹ ?goal"
      proof -
        assume "j < length T"
        hence "length T = Suc j"
          using ‹SA ! i' = Suc j› ‹i' = Suc n› ‹length T ≤ SA ! Suc n› by force
        hence "T ! j = bot"
          by (metis ‹valid_list T› diff_Suc_1 last_conv_nth length_greater_0_conv valid_list_def)
        hence "α (T ! j) = 0"
          using ‹α bot = 0› by presburger
        hence "in_s_current_bucket α T B (α (T ! j)) 0"
          unfolding in_s_current_bucket_def
          using One_nat_def assms(2,4,6,7) lessI s_bucket_ptr_0 valid_list_bucket_end_0
          by fastforce
        moreover
        {
          have "0 < bucket_end α T 0"
            using ‹α (T ! j) = 0› calculation in_s_current_bucket_def by fastforce
          with s_bucket_ptr_0[OF assms(2), of 0, simplified]
               s_locations_invD[OF assms(3), of 0 0, simplified]
          have "SA ! 0 ∈ s_bucket α T 0"
            by simp
          moreover
          have "s_bucket α T 0 = {j}"
            by (simp add: ‹length T = Suc j› assms(4) assms(6) assms(7) s_bucket_0)
          ultimately have "SA ! 0 = j"
            by blast
        }
        ultimately show ?goal
          using ‹i' = Suc n› by blast
      qed
      ultimately show ?goal
        by blast
    qed
    ultimately show ?goal
      by blast
  qed
qed

corollary s_suc_inv_maintained_perm_step_c1_alt:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "length T ≤ SA ! Suc n"
shows "s_suc_inv α T B SA n"
  using assms s_perm_inv_def s_suc_inv_maintained_step_c1_alt by blast

lemma s_suc_inv_maintained_step_c2:
  assumes "s_suc_inv α T B SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = 0"
shows "s_suc_inv α T B SA n"
  unfolding s_suc_inv_def
proof (intro allI impI; elim conjE)
  fix i' j
  assume "i' < length SA" "n < i'" "SA ! i' = Suc j" "suffix_type T j = S_type"

  let ?goal = "∃k. in_s_current_bucket α T B (α (T ! j)) k ∧ SA ! k = j ∧ k < i'"

  from `n < i'` `i = Suc n`
  have "i = i' ∨ i < i'"
    by linarith
  moreover
  from assms(2,4) `SA ! i' = Suc j`
  have "i = i' ⟹ ?goal"
    by simp
  moreover
  from s_suc_invD[OF assms(1) `i' < _` _ `SA ! i' = _` `suffix_type T j = _`] assms(2)
  have "i < i' ⟹ ?goal"
    by blast
  ultimately show ?goal
    by blast
qed

corollary s_suc_inv_maintained_perm_step_c2:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = 0"
shows "s_suc_inv α T B SA n"
  using assms s_perm_inv_elims(7) s_suc_inv_maintained_step_c2 by blast

lemma s_suc_inv_maintained_step_c3:
  assumes "s_suc_inv α T B SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = L_type"
shows "s_suc_inv α T B SA n"
  unfolding s_suc_inv_def
proof (intro allI impI; elim conjE)
  fix i' j'
  assume "i' < length SA" "n < i'" "SA ! i' = Suc j'" "suffix_type T j' = S_type"

  let ?goal = "∃k. in_s_current_bucket α T B (α (T ! j')) k ∧ SA ! k = j' ∧ k < i'"

  from `n < i'` assms(2)
  have "i = i' ∨ i < i'"
    using Suc_lessI by blast
  moreover
  from assms(2,4,5) `SA ! i' = _` `suffix_type T j' = _`
  have "i = i' ⟹ ?goal"
    by simp
  moreover
  from s_suc_invD[OF assms(1) `i' < _` _ `SA ! i' = _` `suffix_type T j' = _`]
  have "i < i' ⟹ ?goal"
    by blast
  ultimately show ?goal
    by blast
qed

corollary s_suc_inv_maintained_perm_step_c3:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = L_type"
shows "s_suc_inv α T B SA n"
  using assms s_perm_inv_elims(7) s_suc_inv_maintained_step_c3 by blast

lemma s_suc_inv_maintained_step_c4:
  assumes "s_distinct_inv α T B SA"
  and     "s_bucket_ptr_inv α T B"
  and     "s_locations_inv α T B SA"
  and     "s_unchanged_inv α T B SA0 SA"
  and     "s_seen_inv α T B SA i"
  and     "s_pred_inv α T B SA i"
  and     "s_suc_inv α T B SA i"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA0 = length T"
  and     "length SA = length T"
  and     "l_types_init α T SA0"
  and     "valid_list T"
  and     "α bot = 0"
  and     "Suc 0 < length T"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_suc_inv α T (B[b := k]) (SA[k := j]) n"
  unfolding s_suc_inv_def
proof(safe)
  fix i' j'
  assume "i' < length (SA[k := j])" "n < i'" "SA[k := j] ! i' = Suc j'" "suffix_type T j' = S_type"
  hence "i' < length SA"
    by simp

  let ?b = "α (T ! j')"
  and ?B = "B[b := k]"
  and ?SA = "SA[k := j]"

  let ?goal = "∃k'. in_s_current_bucket α T ?B ?b k' ∧ ?SA ! k' = j' ∧ k' < i'"

  from `suffix_type T j' = _`
  have "j' < length T"
    by (simp add: suffix_type_s_bound)
  hence "?b ≤ α (Max (set T))"
    using `strict_mono _`
    by (simp add: strict_mono_less_eq)

  from s_bucket_ptr_strict_lower_bound[OF assms(1-6,8,10-14,16-20)]
  have "s_bucket_start α T b < B ! b".
  hence "s_bucket_start α T b ≤ k"
    using assms(21) by linarith
  hence "bucket_start α T b ≤ k"
    using bucket_start_le_s_bucket_start le_trans by blast

  from `s_bucket_start α T b < B ! b`
  have "k < B ! b"
    using assms(21) by linarith

  have "j < length T"
    by (simp add: assms(19) suffix_type_s_bound)
  hence "b ≤ α (Max (set T))"
    by (simp add: assms(8,20) strict_mono_less_eq)
  with s_bucket_ptr_upper_bound[OF assms(2)]
  have "B ! b ≤ bucket_end α T b"
    by blast
  with `k < B ! b`
  have "k < bucket_end α T b"
    by linarith

  have "B ! b ≤ i"
  proof(rule ccontr)
    assume "¬B ! b ≤ i"
    hence "i < B ! b"
      by simp
    with s_B_val[OF assms(1-6,8,10-13,15) `b ≤ α (Max (set T))`] `s_bucket_start α T b < B ! b`
    show False
      by simp
  qed
  with `k < B ! b`
  have "k < i"
    by linarith
  hence "k ≤ n"
    by (simp add: assms(16))
  with `n < i'`
  have "k < i'"
    using dual_order.strict_trans2 by blast
  hence "SA[k := j] ! i' = SA ! i'"
    by simp
  with `SA[k := j] ! i' = Suc j'`
  have "SA ! i' = Suc j'"
    by simp

  have "i ≤ i'"
    by (simp add: Suc_leI ‹n < i'› assms(16))
  hence "i = i' ∨ i < i'"
    by (simp add: nat_less_le)
  moreover
  have "i = i' ⟹ ?goal"
  proof -
    assume "i = i'"
    hence "j = j'"
      using ‹SA ! i' = Suc j'› assms(16,18) by auto
    hence "SA[k := j] ! k = j'"
      using ‹k ≤ n› assms(17) by auto
    moreover
    have "?b = b"
      using ‹j = j'› assms(20) by blast
    hence "in_s_current_bucket α T ?B ?b k = in_s_current_bucket α T ?B b k"
      by simp
    moreover
    from `α (T ! j') ≤ α (Max (set T))`
         `?b = b`[symmetric]
    have "in_s_current_bucket α T ?B b k"
      unfolding in_s_current_bucket_def
      using ‹k < bucket_end α T b› assms(9) by auto
    ultimately show ?goal
      using `k < i'` by blast
  qed
  moreover
  have "i < i' ⟹ ?goal"
  proof -
    assume "i < i'"
    with s_suc_invD[OF assms(7) `i' < length SA` _ `SA ! i' = Suc j'` `suffix_type T j' = _`]
    obtain k' where
      "in_s_current_bucket α T B ?b k'"
      "SA ! k' = j'"
      "k' < i'"
      by blast
    moreover
    from in_s_current_bucketD[OF `in_s_current_bucket α T B ?b k'`]
    have "in_s_current_bucket α T ?B ?b k'"
      unfolding in_s_current_bucket_def
    proof (safe)
      show "?B ! ?b ≤ k'"
        by (metis ‹B ! ?b ≤ k'› ‹k < B ! b› dual_order.trans list_update_beyond nat_le_linear
              not_less nth_list_update_eq nth_list_update_neq)
    qed
    moreover
    from in_s_current_bucketD(2)[OF `in_s_current_bucket α T B ?b k'`]
    have "B ! ?b ≤ k'" .
    hence "s_bucket_start α T ?b ≤ k'"
      by (meson ‹?b ≤ α (Max (set T))› assms(2) le_less_trans not_le s_bucket_ptr_inv_def)
    hence "bucket_start α T ?b ≤ k'"
      using bucket_start_le_s_bucket_start dual_order.trans by blast

    have "b = ?b ∨ b ≠ ?b"
      by blast
    hence "k ≠ k'"
    proof
      assume "b = ?b"
      with `B ! ?b ≤ k'` `k < B ! b`
      show ?thesis
        by simp
    next
      assume "b ≠ ?b"
      with outside_another_bucket[OF _  `bucket_start _ _ _ ≤ k` `k < bucket_end _ _ _`]
           `bucket_start α T ?b ≤ k'` in_s_current_bucketD(3)[OF `in_s_current_bucket α T B ?b k'`]
      show ?thesis
        by blast
    qed
    hence "SA[k := j] ! k' = SA ! k'"
      by simp
    ultimately show ?goal
      by blast
  qed
  ultimately show ?goal
    by blast
qed

corollary s_suc_inv_maintained_perm_step_c4:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_suc_inv α T (B[b := k]) (SA[k := j]) n"
  using s_suc_inv_maintained_step_c4[OF s_perm_inv_elims[OF assms(1)] assms(2-)]
  by blast

lemmas s_suc_inv_maintained_perm_step =
  s_suc_inv_maintained_step_c1
  s_suc_inv_maintained_perm_step_c2
  s_suc_inv_maintained_perm_step_c3
  s_suc_inv_maintained_perm_step_c4

subsubsection "Combined Permutation Invariant"

lemma s_perm_inv_established:
  assumes "s_bucket_init α T B"
  and     "s_type_init T SA"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA = length T"
  and     "l_types_init α T SA"
  and     "valid_list T"
  and     "α bot = 0"
  and     "Suc 0 < length T"
  and     "length T ≤ n"
shows "s_perm_inv α T B SA SA n"
  unfolding s_perm_inv_def
  by (simp add: assms s_distinct_inv_established s_bucket_ptr_inv_established
                s_locations_inv_established s_unchanged_inv_established s_seen_inv_established
                s_pred_inv_established s_suc_inv_established)

lemma s_perm_inv_maintained_step_c1:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "length SA ≤ Suc n"
shows "s_perm_inv α T B SA0 SA n"
  unfolding s_perm_inv_def
  by (clarsimp simp: s_perm_inv_elims[OF assms(1)]
                     s_seen_inv_maintained_perm_step_c1[OF assms]
                     s_pred_inv_maintained_perm_step_alt[OF assms(1,2)]
                     s_suc_inv_maintained_step_c1[OF assms(3)])

lemma s_perm_inv_maintained_step_c1_alt:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "length T ≤ SA ! Suc n"
shows "s_perm_inv α T B SA0 SA n"
proof (cases "length T ≤ Suc n")
  case True
  then show ?thesis
    by (metis assms(1) assms(2) s_perm_inv_elims(11) s_perm_inv_maintained_step_c1)
next
  case False
  hence "Suc n < length T"
    by simp
  then show ?thesis
    unfolding s_perm_inv_def
    by (metis assms s_perm_inv_def s_pred_inv_maintained_step_alt
              s_seen_inv_maintained_perm_step_c1_alt s_suc_inv_maintained_perm_step_c1_alt)
qed

lemma s_perm_inv_maintained_step_c2:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = 0"
shows "s_perm_inv α T B SA0 SA n"
  unfolding s_perm_inv_def
  by (clarsimp simp: s_perm_inv_elims[OF assms(1)]
                     s_seen_inv_maintained_perm_step_c2[OF assms]
                     s_pred_inv_maintained_perm_step_alt[OF assms(1,2)]
                     s_suc_inv_maintained_perm_step_c2[OF assms])

lemma s_perm_inv_maintained_step_c3:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = L_type"
shows "s_perm_inv α T B SA0 SA n"
  unfolding s_perm_inv_def
  by (clarsimp simp: s_perm_inv_elims[OF assms(1)]
                     s_seen_inv_maintained_perm_step_c3[OF assms]
                     s_pred_inv_maintained_perm_step_alt[OF assms(1,2)]
                     s_suc_inv_maintained_perm_step_c3[OF assms])

lemma s_perm_inv_maintained_step_c4:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_perm_inv α T (B[b := k]) SA0 (SA[k := j]) n"
  unfolding s_perm_inv_def
  by (clarsimp simp: s_perm_inv_elims[OF assms(1)]
                     s_distinct_inv_maintained_perm_step[OF assms]
                     s_bucket_ptr_inv_maintained_perm_step[OF assms]
                     s_locations_inv_maintained_perm_step[OF assms]
                     s_unchanged_inv_maintained_perm_step[OF assms]
                     s_seen_inv_maintained_perm_step_c4[OF assms]
                     s_pred_inv_maintained_perm_step[OF assms]
                     s_suc_inv_maintained_perm_step_c4[OF assms])

theorem abs_induce_s_perm_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "abs_induce_s_step (B, SA, i) (α, T) = (B', SA', i')"
shows "s_perm_inv α T B' SA0 SA' i'"
proof (cases i)
  case 0
  then show ?thesis
    using assms by force
next
  case (Suc n)
  assume "i = Suc n"
  have "T ≠ []"
    using s_perm_inv_elims(15)[OF assms(1)] by fastforce
  show ?thesis
  proof (cases "Suc n < length SA ∧ SA ! Suc n < length T")
    assume "Suc n < length SA ∧ SA ! Suc n < length T"
    hence "Suc n < length SA" "SA ! Suc n < length T"
      by blast+
    show ?thesis
    proof (cases "SA ! Suc n")
      case 0
      then show ?thesis
        using s_perm_inv_maintained_step_c2[OF assms(1) ‹i = Suc n› ‹Suc n < length SA› "0"] assms
        by (clarsimp simp: ‹i = Suc n› ‹Suc n < length SA› "0" ‹T ≠ []›)
    next
      case (Suc j)
      assume "SA ! Suc n = Suc j"
      hence "Suc j < length T"
        using ‹SA ! Suc n < length T› by auto
      show ?thesis
      proof (cases "suffix_type T j")
        case S_type
        then show ?thesis
          using assms ‹i = Suc n› ‹Suc n < length SA› ‹SA ! Suc n = Suc j›
                s_perm_inv_maintained_step_c4[OF assms(1), of n j "α (T ! j)" "B ! α (T ! j) - Suc 0"]
          by (clarsimp simp: Let_def ‹Suc j < length T›)
      next
        case L_type
        then show ?thesis
          using assms ‹i = Suc n› ‹Suc n < length SA› ‹SA ! Suc n = Suc j›
                s_perm_inv_maintained_step_c3[OF assms(1)]
          by (clarsimp simp: Let_def ‹Suc j < length T›)
      qed
    qed
  next
    assume "¬(Suc n < length SA ∧ SA ! Suc n < length T)" 
    hence "¬ Suc n < length SA ∨ ¬ SA ! Suc n < length T"
      by blast
    then show ?thesis
    proof
      assume "¬ Suc n < length SA"
      then show ?thesis
        using assms ‹i = Suc n› s_perm_inv_maintained_step_c1[OF assms(1)] by force
    next
      assume "¬ SA ! Suc n < length T"
      hence "length T ≤ SA ! Suc n"
        by simp
      then show ?thesis
        using assms ‹i = Suc n› s_perm_inv_maintained_step_c1_alt[OF assms(1)] by simp
    qed
  qed
qed

corollary abs_induce_s_perm_step_alt:
 "⋀a. s_perm_inv_alt α T SA0 a ⟹ s_perm_inv_alt α T SA0 (abs_induce_s_step a (α, T))"
  by (metis abs_induce_s_perm_step s_perm_inv_alt.elims(2) s_perm_inv_alt.elims(3))

theorem abs_induce_s_perm_alt_maintained:
  assumes "s_perm_inv_alt α T SA0 (B, SA, length T)"
  shows "s_perm_inv_alt α T SA0 (abs_induce_s_base α T B SA)"
  unfolding abs_induce_s_base_def
  using repeat_maintain_inv[of "s_perm_inv_alt α T SA0" abs_induce_s_step "(α, T)", OF _ assms(1)]
        abs_induce_s_perm_step_alt
  by blast

corollary abs_induce_s_perm_maintained:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B SA0 SA (length T)"
shows "s_perm_inv α T B' SA0 SA' n"
  using assms abs_induce_s_perm_alt_maintained by force


lemma s_perm_inv_0_B_val:
  assumes "s_perm_inv α T B SA SA' 0"
  and     "b ≤ α (Max (set T))"
shows "B ! b = s_bucket_start α T b"
proof -
  from s_bucket_ptr_lower_bound[OF s_perm_inv_elims(2)[OF assms(1)] assms(2)]
  have "s_bucket_start α T b ≤ B ! b" .

  have "s_bucket_start α T b ≥ 0"
    by blast
  hence "s_bucket_start α T b = 0 ∨ 0 < s_bucket_start α T b"
    by blast
  with `s_bucket_start α T b ≤ B ! b`
  have "B ! b = s_bucket_start α T b ∨ 0 < B ! b"
    by linarith
  then show ?thesis
  proof
    assume "B ! b = s_bucket_start α T b"
    then show ?thesis .
  next
    assume "0 < B ! b"
    with s_B_val[OF s_perm_inv_elims(1-6,8,10-13,15)[OF assms(1)] assms(2)]
    show ?thesis .
  qed
qed

lemma s_perm_inv_0_list_slice_bucket:
  assumes "s_perm_inv α T B SA SA' 0"
  and     "b ≤ α (Max (set T))"
shows "set (list_slice SA' (bucket_start α T b) (bucket_end α T b)) = bucket α T b"
  by (meson assms bucket_eq_list_slice s_perm_inv_0_B_val s_perm_inv_elims(1-4,10-12))

lemma s_perm_inv_0_distinct_list_slice:
  assumes "s_perm_inv α T B SA SA' 0"
  and     "b ≤ α (Max (set T))"
shows "distinct (list_slice SA' (bucket_start α T b) (bucket_end α T b))"
      (is "distinct ?xs")
proof -
  let ?ys = "list_slice SA' (bucket_start α T b) (l_bucket_end α T b)"
  and ?zs = "list_slice SA' (s_bucket_start α T b) (bucket_end α T b)"

  have "?xs = ?ys @ ?zs"
    by (metis list_slice_append bucket_start_le_s_bucket_start l_bucket_end_le_bucket_end
          s_bucket_start_eq_l_bucket_end)

  from l_types_initD(1)[OF l_types_init_maintained[OF s_perm_inv_elims(2,4,10-12)[OF assms(1)]]
        assms(2)]
  have "set ?ys = l_bucket α T b" .
  moreover
  from s_bucket_eq_list_slice[OF s_perm_inv_elims(1,3,11)[OF assms(1)] assms(2)
        s_perm_inv_0_B_val[OF assms]]
  have "set ?zs = s_bucket α T b" .
  ultimately have "set ?ys ∩ set ?zs = {}"
    using disjoint_l_s_bucket by blast
  with s_distinct_invD[OF s_perm_inv_elims(1), OF assms, simplified s_perm_inv_0_B_val[OF assms]]
       l_types_initD(2)[OF l_types_init_maintained[OF s_perm_inv_elims(2,4,10-12)[OF assms(1)]]
         assms(2)]
       `?xs = ?ys @ ?zs`
  show ?thesis
    by auto
qed

lemma abs_induce_s_base_distinct:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B' SA SA' n"
shows "distinct SA'"
proof(intro distinct_conv_nth[THEN iffD2] allI impI)
  fix i j
  assume "i < length SA'" "j < length SA'" "i ≠ j"
  hence "i < length T" "j < length T"
    using assms(2) s_perm_inv_elims(11) by fastforce+

  from abs_induce_s_base_index[of α T B SA] assms(1)
  have "n = 0"
    by simp

  from index_in_bucket_interval_gen[OF `i < length T` s_perm_inv_elims(8)[OF assms(2)]]
  obtain b0 where
    "b0 ≤ α (Max (set T))"
    "bucket_start α T b0 ≤ i"
    "i < bucket_end α T b0"
    by blast

  have "bucket_end α T b0 ≤ length SA'"
    using assms(2) bucket_end_le_length s_perm_inv_elims(11) by fastforce

  let ?xs = "list_slice SA' (bucket_start α T b0) (bucket_end α T b0)"

  from index_in_bucket_interval_gen[OF `j < length T` s_perm_inv_elims(8)[OF assms(2)]]
  obtain b1 where
    "b1 ≤ α (Max (set T))"
    "bucket_start α T b1 ≤ j"
    "j < bucket_end α T b1"
    by blast

  have "bucket_end α T b1 ≤ length SA'"
    using assms(2) bucket_end_le_length s_perm_inv_elims(11) by fastforce

  have "b0 ≠ b1 ⟹ SA' ! i ≠ SA' ! j"
  proof -
    assume "b0 ≠ b1"
    hence "bucket α T b0 ∩ bucket α T b1 = {}"
      by (metis (mono_tags, lifting) Int_emptyI bucket_def mem_Collect_eq)
    moreover
    from s_perm_inv_0_list_slice_bucket[OF assms(2)[simplified `n = 0`] `b0 ≤ _`]
         list_slice_nth_mem[OF `bucket_start α T b0 ≤ i` `i < bucket_end α T b0`
           `bucket_end α T b0 ≤ _`]
    have "SA' ! i ∈ bucket α T b0"
      by blast
    moreover
    from s_perm_inv_0_list_slice_bucket[OF assms(2)[simplified `n = 0`] `b1 ≤ _`]
         list_slice_nth_mem[OF `bucket_start α T b1 ≤ j` `j < bucket_end α T b1`
           `bucket_end α T b1 ≤ _`]
    have "SA' ! j ∈ bucket α T b1"
      by blast
    ultimately show ?thesis
      by auto
  qed
  moreover
  have "b0 = b1 ⟹ SA' ! i ≠ SA' ! j"
  proof -
    assume "b0 = b1"
    with `bucket_start α T b1 ≤ j` `j < bucket_end α T b1`
    have "bucket_start α T b0 ≤ j" "j < bucket_end α T b0"
      by simp_all
    with list_slice_nth_eq_iff_index_eq[
          OF s_perm_inv_0_distinct_list_slice[OF assms(2)[simplified`n = 0`] `b0 ≤ _`]
            `bucket_end _ _ b0 ≤ _` `bucket_start α T b0 ≤ i` `i < bucket_end α T b0`, of j]
         `i ≠ j`
    show ?thesis
      by blast
  qed
  ultimately show "SA' ! i ≠ SA' ! j"
    by blast
qed

lemma abs_induce_s_base_subset_upt:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B' SA SA' n"
shows "set SA' ⊆ {0..<length T}"
proof
  fix x
  assume "x ∈ set SA'"
  from in_set_conv_nth[THEN iffD1, OF `x ∈ set SA'`]
  obtain i where
    "i < length SA'"
    "SA' ! i = x"
    by blast
  hence "i < length T"
    using assms(2) s_perm_inv_elims(11) by fastforce
  with index_in_bucket_interval_gen[OF _ s_perm_inv_elims(8)[OF assms(2)]]
  obtain b where
    "b ≤ α (Max (set T))"
    "bucket_start α T b ≤ i"
    "i < bucket_end α T b"
    by blast

  from abs_induce_s_base_index[of α T B SA] assms(1)
  have "n = 0"
    by simp

  have "bucket_end α T b ≤ length SA'"
    using assms(2) bucket_end_le_length s_perm_inv_elims(11) by fastforce
  with s_perm_inv_0_list_slice_bucket[OF assms(2)[simplified `n = 0`] `b ≤ _`]
       `SA' ! i = x` `bucket_start α T b ≤ i` `i < bucket_end α T b`
  have "x ∈ bucket α T b"
    using list_slice_nth_mem by blast
  hence "x < length T"
    using bucket_def by blast
  then show "x ∈ {0..< length T}"
    by simp
qed

corollary abs_induce_s_base_eq_upt:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B' SA SA' n"
shows "set SA' = {0..<length T}"
  by (rule card_subset_eq[OF finite_atLeastLessThan abs_induce_s_base_subset_upt[OF assms]];
      clarsimp simp: distinct_card[OF abs_induce_s_base_distinct[OF assms]]
                     s_perm_inv_elims(11)[OF assms(2)])

theorem abs_induce_s_base_perm:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B' SA SA' n"
shows "SA' <~~> [0..< length T]"
  by (rule perm_distinct_set_of_upt_iff[THEN iffD2];
      clarsimp simp: abs_induce_s_base_distinct[OF assms] abs_induce_s_base_eq_upt[OF assms])

subsubsection "Sorted"

lemma s_sorted_established:
  assumes "s_bucket_init α T B"
  and     "strict_mono α"
  and     "valid_list T"
  and     "α bot = 0"
  and     "b ≤ α (Max (set T))"
shows "sorted_wrt R (list_slice SA (B ! b) (bucket_end α T b))"
      (is "sorted_wrt R ?xs")
proof -
  have "b = 0 ∨ 0 < b"
    by blast
  moreover
  have "0 < b ⟹ ?thesis"
  proof -
    assume "0 < b"
    hence "B ! b = bucket_end α T b"
      by (simp add: ‹b ≤ α (Max (set T))› assms(1) s_bucket_initD)
    then show ?thesis 
      by simp
  qed
  moreover
  have "b = 0 ⟹ ?thesis"
  proof -
    assume "b = 0"
    hence "bucket_end α T b = Suc 0"
      by (simp add: assms(2-4) valid_list_bucket_end_0)
    moreover
    from `b = 0`
    have "B ! b = 0"
      using assms(1) s_bucket_initD(2) by auto
    ultimately show ?thesis
      by (simp add: sorted_wrt01)
  qed
  ultimately show ?thesis
    by blast
qed

lemma s_sorted_inv_established:
  assumes "s_bucket_init α T B"
  and     "strict_mono α"
  and     "valid_list T"
  and     "α bot = 0"
shows "s_sorted_inv α T B SA"
  unfolding s_sorted_inv_def
  using assms ordlistns.sorted_map s_sorted_established by blast

lemma s_prefix_sorted_inv_established:
  assumes "s_bucket_init α T B"
  and     "strict_mono α"
  and     "valid_list T"
  and     "α bot = 0"
shows "s_prefix_sorted_inv α T B SA"
  unfolding s_prefix_sorted_inv_def
  using assms ordlistns.sorted_map s_sorted_established by blast

lemma s_sorted_maintained_unchanged_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
  and     "b' ≤ α (Max (set T))"
  and     "sorted_wrt R (list_slice SA (B ! b') (bucket_end α T b'))"
  and     "b ≠ b'"
shows "sorted_wrt R (list_slice (SA[k := j]) ((B[b := k]) ! b') (bucket_end α T b'))"
proof -
  let ?xs = "list_slice (SA[k := j]) (B[b := k] ! b') (bucket_end α T b')"

  have "bucket_end α T b ≤ length T"
    using bucket_end_le_length by blast
  moreover
  have "B ! b ≤ bucket_end α T b"
    using assms(1,5,6) s_bucket_ptr_upper_bound s_perm_inv_elims(2,8) strict_mono_less_eq
          suffix_type_s_bound by fastforce
  ultimately have "k < length T"
    using assms(1,7) s_perm_inv_elims(15) by fastforce
  hence "k < length SA"
    by (metis assms(1) s_perm_inv_def)

  from s_bucket_ptr_strict_lower_bound[OF s_perm_inv_elims(1-6,8,10-14)[OF assms(1)] assms(2-6)]
  have "s_bucket_start α T b < B ! b" .
  hence "k < B ! b"
    using assms(7) diff_less gr_implies_not_zero by blast

  have "s_bucket_start α T b ≤ k"
    using assms s_bucket_ptr_strict_lower_bound s_perm_inv_def by fastforce
  hence "bucket_start α T b ≤ k"
    using bucket_start_le_s_bucket_start le_trans by blast

  from `b ≠ b'`
  have "B[b := k] ! b' = B ! b'"
    by simp

  have "k < B ! b' ∨ bucket_end α T b' ≤ k"
  proof -
    from `b ≠ b'`
    have "b < b' ∨ b' < b"
      using nat_neq_iff by blast
    moreover
    have "b < b' ⟹ k < B ! b'"
    proof -
      assume "b < b'"
      hence "bucket_end α T b ≤ bucket_start α T b'"
        by (simp add: less_bucket_end_le_start)
      hence "k < bucket_start α T b'"
        using ‹B ! b ≤ bucket_end α T b› ‹k < B ! b› by linarith
      with s_bucket_ptr_lower_bound[OF s_perm_inv_elims(2)[OF assms(1)] `b' ≤ _`]
      show ?thesis
        by (meson bucket_start_le_s_bucket_start order.strict_trans2)
    qed
    moreover
    have "b' < b ⟹ bucket_end α T b' ≤ k"
    proof -
      assume "b' < b"
      hence "bucket_end α T b' ≤ bucket_start α T b"
        by (simp add: less_bucket_end_le_start)
      then show ?thesis
        using ‹bucket_start α T b ≤ k› by linarith
    qed
    ultimately show ?thesis
      by blast
  qed
  with list_slice_update_unchanged_1
       list_slice_update_unchanged_2
  have "?xs = list_slice SA (B ! b') (bucket_end α T b')"
    using ‹B[b := k] ! b' = B ! b'› by auto
  then show ?thesis
    using assms(9) by auto
qed

lemma s_sorted_inv_maintained_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "s_sorted_pre α T SA0"
  and     "s_sorted_inv α T B SA"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_sorted_inv α T (B[b := k]) (SA[k := j])"
  unfolding s_sorted_inv_def
proof (safe)
  fix b'
  assume "b' ≤ α (Max (set T))"
  let ?xs = "list_slice (SA[k := j]) (B[b := k] ! b') (bucket_end α T b')"

  have "bucket_end α T b ≤ length T"
    using bucket_end_le_length by blast

  moreover
  have "B ! b ≤ bucket_end α T b"
    using assms(1,7,8) s_bucket_ptr_upper_bound suffix_type_s_bound
          s_perm_inv_elims(2,8) strict_mono_less_eq
    by fastforce

  ultimately have "k < length T"
    using assms(1,9) s_perm_inv_elims(15) by fastforce
  hence "k < length SA"
    by (metis assms(1) s_perm_inv_def)

  from s_bucket_ptr_strict_lower_bound
          [OF s_perm_inv_elims(1-6,8,10-14)
          [OF assms(1)] assms(4-8)]
  have "s_bucket_start α T b < B ! b" .
  hence "k < B ! b"
    using assms(9) diff_less gr_implies_not_zero by blast

  have "s_bucket_start α T b ≤ k"
    using assms s_bucket_ptr_strict_lower_bound s_perm_inv_def 
    by fastforce
  hence "bucket_start α T b ≤ k"
    using bucket_start_le_s_bucket_start le_trans 
    by blast
  hence "b ≤ α (Max (set T))"
    by (metis ‹k < length SA› assms(1) bucket_end_Max dual_order.trans
              less_bucket_end_le_start s_perm_inv_elims(8,11) leD leI)

  have "b = b' ∨ b ≠ b'"
    by blast
  moreover
  have "b = b' ⟹ ordlistns.sorted (map (suffix T) ?xs)"
  proof -
    assume "b = b'"
    hence "B[b := k] ! b' = k"
      by (meson ‹b' ≤ α (Max (set T))› assms(1) le_less_trans nth_list_update_eq
            s_perm_inv_elims(9))

    have "SA[k := j] ! k = j"
      by (simp add: ‹k < length SA›)

    from list_slice_update_unchanged_1
         `k < B ! b` 
         `SA[k := j] ! k = j` 
         `B[b := k] ! b' = k` 
         `B ! b ≤ bucket_end α T b`
         `b = b'` `k < length SA`
    have "?xs = j # list_slice SA (B ! b) (bucket_end α T b)"
      by (metis Suc_pred  assms(9) length_list_update not_le  
                less_nat_zero_code list_slice_Suc less_le_trans)
    moreover
    have "ordlistns.sorted 
            (map (suffix T) (j # list_slice SA (B ! b) (bucket_end α T b)))"
    proof -
      let ?ys = "list_slice SA (B ! b) (bucket_end α T b)"

      have A: "map (suffix T) (j # ?ys) = (suffix T j) # map (suffix T) ?ys"
        by simp

      from s_sorted_invD[OF assms(3) `b ≤ _`]
      have B: "ordlistns.sorted (map (suffix T) ?ys)" .

      have "?ys = [] ∨ ?ys ≠ []"
        by blast
      hence "map (suffix T) ?ys = [] ∨ map (suffix T) ?ys ≠ []"
        by simp
      moreover
      have "map (suffix T) ?ys = [] ⟹ ?thesis"
        using ordlistns.sorted_cons_nil by fastforce
      moreover
      have "map (suffix T) ?ys ≠ [] ⟹
             ordlistns.sorted ((suffix T j) # map (suffix T) ?ys)"
      proof (rule ordlistns.sorted_consI[OF _ B])
        assume "map (suffix T) (list_slice SA (B ! b) (bucket_end α T b)) ≠ []"
        then 
        show "map (suffix T) (list_slice SA (B ! b) (bucket_end α T b)) ≠ []"
          by simp
      next
        assume "map (suffix T) ?ys ≠ []"
        hence "map (suffix T) ?ys ! 0 = suffix T (?ys ! 0)"
          by (metis length_greater_0_conv list.simps(8) nth_map)
        moreover
        have "list_less_eq_ns (suffix T j) (suffix T (?ys ! 0))"
        proof -
          have "?ys ! 0 ∈ s_bucket α T b"
            by (metis assms(1) length_greater_0_conv s_perm_inv_elims(3)
                      length_map nth_mem s_locations_inv_in_list_slice
                      ‹b = b'› 
                      ‹b' ≤ α (Max (set T))›
                      ‹map (suffix T) ?ys ≠ []› )
          hence "α (T ! (?ys ! 0)) = b" "suffix_type T (?ys ! 0) = S_type"
            by (simp add: s_bucket_def bucket_def)+
          hence "T ! j = T ! (?ys ! 0)"
            using assms(1,8) s_perm_inv_elims(8) strict_mono_eq by fastforce

          have "?ys ! 0 = SA ! (B ! b)"
            using ‹map (suffix T) ?ys ≠ []› nth_list_slice by fastforce

          have "b ≠ 0"
            by (metis ‹s_bucket_start α T b < B ! b› assms(1)
                      gr_implies_not_zero s_bucket_ptr_0 s_perm_inv_elims(2))

          have "in_s_current_bucket α T B b (B ! b)"
            using ‹b = b'› ‹b' ≤ α (Max (set T))› ‹map (suffix T) ?ys ≠ []›  
            by (metis ‹B ! b ≤ bucket_end α T b› in_s_current_bucket_def
                      le_eq_less_or_eq list.map_disc_iff list_slice_n_n)
            with s_pred_invD
                  [OF s_perm_inv_elims(6)[OF assms(1)] _ `b ≠ 0`, 
                   of "B ! b"]
          obtain i' where i'_assms:
            "i' < length SA"
            "SA ! i' = Suc (SA ! (B ! b))"
            "B ! b < i'"
            "i < i'"
            by blast

          let ?b0 = "α (T ! (Suc j))"
          and ?b1 = "α (T ! (Suc (SA ! (B ! b))))"

          have i_less: "i < length SA"
            by (simp add: assms(4-5))

          have "?b0 ≤ α (Max (set T))"
            by (metis Max_greD Suc_leI assms(1,4-6) strict_mono_leD
                      s_perm_inv_elims(5,8) s_seen_invD(1) lessI)

          have "?b1 ≤ α (Max (set T))"
            by (metis Max_greD i'_assms(1,2,4) assms(1)
                  less_imp_le_nat s_perm_inv_elims(5,8) 
                  s_seen_invD(1) strict_mono_leD)

          have S0: "suffix T j = T ! j # suffix T (Suc j)"
            using assms(7) suffix_cons_Suc suffix_type_s_bound 
            by blast

          have S1: "suffix T (?ys ! 0) = 
                      T ! (?ys ! 0) # suffix T (Suc (SA ! (B ! b)))"
            using ‹?ys ! 0 = SA ! (B ! b)› 
                  ‹suffix_type T (?ys ! 0) = S_type› suffix_cons_Suc
                  suffix_type_s_bound by auto

          have "?b0 ≤ ?b1"
          proof(rule ccontr)
            assume "¬?b0 ≤ ?b1"
            hence "?b1 < ?b0"
              by simp
            hence "bucket_end α T ?b1 ≤ bucket_start α T ?b0"
              by (simp add: less_bucket_end_le_start)
            with s_index_upper_bound[OF s_perm_inv_elims(2,5)[OF assms(1)] i'_assms(1)]
                 s_index_lower_bound[OF s_perm_inv_elims(2,5)[OF assms(1)] i_less,
                                     simplified]
                 order.strict_implies_order[OF i'_assms(4)]
            show False
              using i'_assms(2) assms(4,6) by auto
          qed
          hence "?b0 = ?b1 ∨ ?b0 < ?b1"
            by linarith
          moreover
          have "?b0 < ?b1 ⟹ 
                list_less_eq_ns 
                  (suffix T (Suc j)) 
                  (suffix T (Suc (SA ! (B ! b))))"
          proof -
            assume "?b0 < ?b1"
            hence "T ! (Suc j) < T ! (Suc (SA ! (B ! b)))"
              using assms(1) s_perm_inv_elims(8) strict_mono_less by blast
            then show ?thesis
              by (metis i'_assms(1,2,4) assms(1,4-6) s_perm_inv_def
                        leD  s_seen_invD(1) list_less_eq_ns_linear
                        suffix_cons_Suc list_less_eq_ns_cons)
          qed
          moreover
          have "?b0 = ?b1 ⟹ 
                  list_less_eq_ns 
                    (suffix T (Suc j)) 
                    (suffix T (Suc (SA ! (B ! b))))"
          proof -
            assume "?b0 = ?b1"
            with s_index_upper_bound
                   [OF s_perm_inv_elims(2,5)[OF assms(1)]
                 `i' < _`] i'_assms(4)
            have "i' < bucket_end α T ?b0"
              by (simp add: ‹SA ! i' = Suc (SA ! (B ! b))›)

            have "suffix_type T (SA ! i) = S_type ∨ 
                  suffix_type T (SA ! i) = L_type"
              using SL_types.exhaust by blast
            moreover
            have "suffix_type T (SA ! i) = S_type ⟹ ?thesis"
            proof -
              assume "suffix_type T (SA ! i) = S_type"
              with s_seen_invD(3)
                    [OF s_perm_inv_elims(5)[OF assms(1)] i_less, 
                     simplified]
              have "in_s_current_bucket α T B ?b0 i"
                by (simp add: assms(4) assms(6))
              hence "B ! ?b0 ≤ i"
                using in_s_current_bucket_def by blast
              hence "∃m. B ! ?b0 + m = i"
                using less_eqE by blast
              then obtain m0 where m0_assm:
                "B ! ?b0 + m0 = i"
                by blast

              from `B ! ?b0 ≤ i` i'_assms(4) 
              have "∃m. B ! ?b0 + m = i'"
                by presburger
              then obtain m1 where m1_assm:
                "B ! ?b0 + m1 = i'"
                by blast
              hence "B ! ?b0 + m0 ≤ B ! ?b0 + m1"
                by (simp add: m0_assm i'_assms(4) dual_order.order_iff_strict)
              hence "m0 ≤ m1"
                using add_le_imp_le_left by blast

              have "(list_slice SA (B ! ?b0) (bucket_end α T ?b0)) ! m0 = 
                    Suc j"
                using m0_assm i_less
                      ‹in_s_current_bucket α T B ?b0 i› assms(4,6) 
                      in_s_current_bucketD(3) 
                by (metis ‹B ! α (T ! Suc j) ≤ i› diff_add_inverse list_slice_nth)
              moreover
              have "(list_slice  SA (B ! ?b0) (bucket_end α T ?b0)) ! m1 = 
                    Suc (SA ! (B ! b))"
                using m1_assm i'_assms
                       ‹i' < bucket_end α T ?b0›
                by (metis diff_add_inverse le_add1 list_slice_nth)
              moreover
              have "length (list_slice SA (B ! ?b0) (bucket_end α T ?b0)) = 
                    (bucket_end α T ?b0) - B ! ?b0"
                by (metis assms(1) bucket_end_le_length length_list_slice min_def s_perm_inv_def)
              with `B ! ?b0 + m1 = i'` 
                    `i' < bucket_end α T ?b0`
              have "m1 < length (list_slice SA (B ! ?b0) (bucket_end α T ?b0))"
                by linarith
              ultimately
              show ?thesis
                using ordlistns.sorted_nth_mono
                        [OF s_sorted_invD[OF assms(3) `?b0 ≤ α (Max _)`]
                            `m0 ≤ m1`]
                      ‹m0 ≤ m1› 
                by auto
            qed
            moreover
            have "suffix_type T (SA ! i) = L_type ⟹ ?thesis"
            proof -
              assume "suffix_type T (SA ! i) = L_type"
              with s_seen_invD(2)
                    [OF s_perm_inv_elims(5)[OF assms(1)] i_less, 
                     simplified]
              have "in_l_bucket α T ?b0 i"
                by (simp add: assms(4) assms(6))
              hence "bucket_start α T ?b0 ≤ i"
                by (simp add: in_l_bucket_def)
              hence "∃m. bucket_start α T ?b0 + m = i"
                using less_eqE by blast
              then obtain m0 where start_plus_m0_eq:
                "bucket_start α T ?b0 + m0 = i"
                by blast

              have "suffix_type T (SA ! i') = L_type ∨ 
                    suffix_type T (SA ! i') = S_type"
                using SL_types.exhaust by blast
              moreover
              have "suffix_type T (SA ! i') = S_type ⟹ ?thesis"
              proof -
                assume "suffix_type T (SA ! i') = S_type"

                have "SA ! i < length T"
                  by (meson ‹i < length SA› assms(1) order_refl s_perm_inv_elims(5) s_seen_invD(1))

                have "SA ! i' < length T"
                  by (simp add: ‹suffix_type T (SA ! i') = S_type› suffix_type_s_bound)

                from `?b0 = ?b1`
                have "T ! (Suc j) = T ! Suc (SA ! (B ! b))"
                  using assms(1) s_perm_inv_def strict_mono_eq by blast
                hence "hd (suffix T (SA ! i')) = hd (suffix T (SA ! i))"
                  by (metis assms(4,6) list.sel(1) suffix_cons_Suc
                        ‹SA ! i < length T› ‹SA ! i' < length T› 
                        ‹SA ! i' = Suc (SA ! (B ! b))›)
                with l_less_than_s_type
                      [OF s_perm_inv_elims(13)[OF assms(1)] 
                          `SA ! i' < length T`
                          `SA ! i < length T` _ 
                          `suffix_type T (SA ! i') = _`
                          `suffix_type T (SA ! i) = _`]
                have "list_less_ns (suffix T (SA ! i)) (suffix T (SA ! i'))".
                then show ?thesis
                  by (simp add: ‹SA ! i' = Suc (SA ! (B ! b))› assms(4,6))
              qed
              moreover
              have "suffix_type T (SA ! i') = L_type ⟹ ?thesis"
              proof -
                assume "suffix_type T (SA ! i') = L_type"
                with s_seen_invD(2)
                      [OF s_perm_inv_elims(5)[OF assms(1)] 
                          `i' < length SA`,
                       simplified 
                         `?b0 = ?b1`[symmetric]
                         `SA ! i' = Suc (SA ! (B ! b))`]
                         `SA ! i' = Suc (SA ! (B ! b))`
                have "in_l_bucket α T ?b0 i'"
                  by (simp add: ‹i < i'› dual_order.order_iff_strict)
                hence i'_le_end: "i' < l_bucket_end α T ?b0"
                  by (simp add: in_l_bucket_def)
                hence "∃m. bucket_start α T ?b0 + m = i'"
                  by (metis ‹in_l_bucket α T ?b0 i'› in_l_bucket_def less_eqE)
                then obtain m1 where start_plus_m1_eq:
                  "bucket_start α T ?b0 + m1 = i'"
                  by blast

                let ?zs = 
                    "list_slice SA 
                      (bucket_start α T ?b0) 
                      (l_bucket_end α T ?b0)"

                have "?zs ! m0 = Suc j" 
                  by (metis ‹bucket_start α T (α (T ! Suc j)) ≤ i› 
                            assms(4,6)  i'_assms(4) i'_le_end 
                            diff_add_inverse dual_order.order_iff_strict
                            i_less list_slice_nth order.strict_trans1 
                            start_plus_m0_eq)
                moreover
                have "?zs ! m1 = Suc (SA ! (B ! b))"
                  using list_slice_nth dual_order.order_iff_strict i'_assms(4)
                        le_trans [OF ‹bucket_start α T (α (T ! Suc j)) ≤ i›]
                        ‹SA ! i' = Suc (SA ! (B ! b))› 
                        ‹bucket_start α T ?b0 + m1 = i'›
                        ‹i' < l_bucket_end α T ?b0› 
                        ‹i' < length SA› 
                  by (metis diff_add_inverse)             
                moreover
                have "m0 ≤ m1"
                  using start_plus_m0_eq start_plus_m1_eq i'_assms(4)
                  by linarith
                moreover
                have "length ?zs = l_bucket_end α T ?b0 - bucket_start α T ?b0"
                  by (metis ‹?b0 ≤ α (Max (set T))› assms(1)
                            add_diff_cancel_left' distinct_card
                            l_bucket_end_def l_bucket_size_def 
                            l_types_init_def s_perm_inv_def
                            l_types_init_maintained)
                hence "m1 < length ?zs"
                  using start_plus_m1_eq i'_le_end by linarith
                moreover
                from s_sorted_pre_maintained
                      [OF s_perm_inv_elims(2,4,10,11)[OF assms(1)] 
                          assms(2)]
                have "s_sorted_pre α T SA" .
                ultimately show ?thesis
                  using ordlistns.sorted_nth_mono
                        [OF s_sorted_preD
                            [of α T SA,
                             OF _ `?b0 ≤ α (Max _)`], 
                        of m0 m1]
                  by (simp add: ‹m1 < length ?zs› le_less_trans
                                ‹s_sorted_pre α T SA›)
              qed
              ultimately show ?thesis
                by blast
            qed
            ultimately show ?thesis
              by blast
          qed
          ultimately 
          have "list_less_eq_ns 
                  (suffix T (Suc j)) 
                  (suffix T (Suc (SA ! (B ! b))))"
            by blast
          with S0 S1 `T ! j = T ! (?ys ! 0)`
          show ?thesis
            by (simp add: list_less_eq_ns_cons)
        qed
        ultimately 
        show "list_less_eq_ns (suffix T j) (map (suffix T) ?ys ! 0)"
          by simp
      qed
      ultimately show ?thesis
        using A by fastforce
    qed
    ultimately show ?thesis
      by simp
  qed
  moreover
  have "b ≠ b' ⟹ ordlistns.sorted (map (suffix T) ?xs)"
  proof -
    assume "b ≠ b'"
    with s_sorted_maintained_unchanged_step[OF assms(1,4-) `b' ≤ _`]
         s_sorted_invD[OF assms(3) `b' ≤ _`]
    show ?thesis
      using ordlistns.sorted_map by blast
  qed
  ultimately show "ordlistns.sorted (map (suffix T) ?xs)"
    by blast
qed

lemma s_prefix_sorted_inv_maintained_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "s_prefix_sorted_pre α T SA0"
  and     "s_prefix_sorted_inv α T B SA"
  and     "i = Suc n"
  and     "Suc n < length SA"
  and     "SA ! Suc n = Suc j"
  and     "suffix_type T j = S_type"
  and     "b = α (T ! j)"
  and     "k = B ! b - Suc 0"
shows "s_prefix_sorted_inv α T (B[b := k]) (SA[k := j])"
  unfolding s_prefix_sorted_inv_def
proof (safe)
  fix b'
  assume "b' ≤ α (Max (set T))"
  let ?xs = "list_slice (SA[k := j]) (B[b := k] ! b') (bucket_end α T b')"

  have "bucket_end α T b ≤ length T"
    using bucket_end_le_length by blast
  moreover
  have "B ! b ≤ bucket_end α T b"
    using assms(1,7,8) s_bucket_ptr_upper_bound s_perm_inv_elims(2,8) strict_mono_less_eq
          suffix_type_s_bound by fastforce

  ultimately have "k < length T"
    using assms(1,9) s_perm_inv_elims(15) by fastforce
  hence "k < length SA"
    by (metis assms(1) s_perm_inv_def)

  from s_bucket_ptr_strict_lower_bound
        [OF s_perm_inv_elims(1-6,8,10-14)[OF assms(1)] assms(4-8)]
  have "s_bucket_start α T b < B ! b" .
  hence "k < B ! b"
    using assms(9) diff_less gr_implies_not_zero by blast

  have "s_bucket_start α T b ≤ k"
    using assms s_bucket_ptr_strict_lower_bound s_perm_inv_def by fastforce
  hence "bucket_start α T b ≤ k"
    using bucket_start_le_s_bucket_start le_trans by blast
  hence "b ≤ α (Max (set T))"
    by (metis ‹k < length SA› assms(1) bucket_end_Max dual_order.trans 
              leD leI  s_perm_inv_elims(8,11) less_bucket_end_le_start)

  have "b = b' ∨ b ≠ b'"
    by blast
  moreover
  have "b = b' ⟹ ordlistns.sorted (map (lms_slice T) ?xs)"
  proof -
    assume "b = b'"
    hence "B[b := k] ! b' = k"
      by (meson ‹b' ≤ α (Max (set T))› assms(1) le_less_trans 
                nth_list_update_eq s_perm_inv_elims(9))

    have "SA[k := j] ! k = j"
      by (simp add: ‹k < length SA›)

    from list_slice_update_unchanged_1[OF `k < B ! b`]
         `k < B ! b` `SA[k := j] ! k = j` `B[b := k] ! b' = k` 
         `B ! b ≤ bucket_end α T b`
         `b = b'` `k < length SA`
    have "?xs = j # list_slice SA (B ! b) (bucket_end α T b)"
      by (metis Suc_pred assms(9) length_list_update not_le
                less_nat_zero_code list_slice_Suc less_le_trans)
    moreover
    have "ordlistns.sorted 
              (map (lms_slice T)
                   (j # list_slice SA (B ! b) 
                   (bucket_end α T b)))"
    proof -
      let ?ys = "list_slice SA (B ! b) (bucket_end α T b)"

      have A: "map (lms_slice T) (j # ?ys) = (lms_slice T j) # map (lms_slice T) ?ys"
        by simp

      from s_prefix_sorted_invD[OF assms(3) `b ≤ _`]
      have B: "ordlistns.sorted (map (lms_slice T) ?ys)" .

      have "?ys = [] ∨ ?ys ≠ []"
        by blast
      hence "map (lms_slice T) ?ys = [] ∨ map (lms_slice T) ?ys ≠ []"
        by simp
      moreover
      have "map (lms_slice T) ?ys = [] ⟹ ?thesis"
        using ordlistns.sorted_cons_nil by fastforce
      moreover
      have "map (lms_slice T) ?ys ≠ [] ⟹
            ordlistns.sorted ((lms_slice T j) # map (lms_slice T) ?ys)"
      proof (rule ordlistns.sorted_consI[OF _ B])
        assume "map (lms_slice T) ?ys ≠ []"
        hence "map (lms_slice T) ?ys ! 0 = lms_slice T (?ys ! 0)"
          by (metis length_greater_0_conv list.simps(8) nth_map)
        moreover
        have "list_less_eq_ns (lms_slice T j) (lms_slice T (?ys ! 0))"
        proof -
          have "?ys ! 0 ∈ s_bucket α T b"
            by (metis ‹b = b'› ‹b' ≤ α (Max (set T))› ‹map (lms_slice T) ?ys ≠ []› assms(1)
                      length_greater_0_conv length_map nth_mem s_locations_inv_in_list_slice
                      s_perm_inv_elims(3))
          hence "α (T ! (?ys ! 0)) = b" "suffix_type T (?ys ! 0) = S_type"
            by (simp add: s_bucket_def bucket_def)+
          hence "T ! j = T ! (?ys ! 0)"
            using assms(1,8) s_perm_inv_elims(8) strict_mono_eq by fastforce

          have "?ys ! 0 = SA ! (B ! b)"
            using ‹map (lms_slice T) ?ys ≠ []› nth_list_slice by fastforce

          have "b ≠ 0"
            by (metis ‹s_bucket_start α T b < B ! b› assms(1)
                  gr_implies_not_zero s_bucket_ptr_0 s_perm_inv_elims(2))

          have "in_s_current_bucket α T B b (B ! b)"
            using ‹b = b'› ‹b' ≤ α (Max (set T))› 
                  ‹map (lms_slice T) ?ys ≠ []›
                  in_s_current_bucket_def 
            by (metis ‹B ! b ≤ bucket_end α T b› 
                      dual_order.order_iff_strict list.map_disc_iff 
                      list_slice_n_n)
            with s_pred_invD
                    [OF s_perm_inv_elims(6)[OF assms(1)] _ `b ≠ 0`, 
                     of "B ! b"]
          obtain i' where
            "i' < length SA"
            "SA ! i' = Suc (SA ! (B ! b))"
            "B ! b < i'"
            "i < i'"
            by blast

          let ?b0 = "α (T ! (Suc j))"
          and ?b1 = "α (T ! (Suc (SA ! (B ! b))))"

          have "i < length SA"
            by (simp add: assms(4-5))

          have "?b0 ≤ α (Max (set T))"
            by (metis Max_greD Suc_leI assms(1,4-6) lessI s_perm_inv_elims(5,8) s_seen_invD(1)
                  strict_mono_leD)

          have "?b1 ≤ α (Max (set T))"
            by (metis Max_greD ‹SA ! i' = Suc (SA ! (B ! b))› ‹i < i'› ‹i' < length SA› assms(1)
                  less_imp_le_nat s_perm_inv_elims(5) s_perm_inv_elims(8) s_seen_invD(1)
                  strict_mono_leD)

          have S0: "lms_slice T j = T ! j # lms_slice T (Suc j)"
            using assms(7) lms_slice_cons suffix_type_s_bound by blast

          have S1:
            "lms_slice T (?ys ! 0) = T ! (?ys ! 0) # lms_slice T (Suc (SA ! (B ! b)))"
            using ‹?ys ! 0 = SA ! (B ! b)› ‹suffix_type T (?ys ! 0) = S_type› lms_slice_cons
                  suffix_type_s_bound by auto

          have "?b0 ≤ ?b1"
          proof(rule ccontr)
            assume "¬?b0 ≤ ?b1"
            hence "?b1 < ?b0"
              by simp
            hence "bucket_end α T ?b1 ≤ bucket_start α T ?b0"
              by (simp add: less_bucket_end_le_start)
            with s_index_upper_bound[OF s_perm_inv_elims(2,5)[OF assms(1)] `i' < length SA`]
                 s_index_lower_bound[OF s_perm_inv_elims(2,5)[OF assms(1)] `i < length SA`,
                   simplified]
                 order.strict_implies_order[OF `i < i'`]
            show False
              using ‹SA ! i' = Suc (SA ! (B ! b))› assms(4,6) by auto
          qed
          hence "?b0 = ?b1 ∨ ?b0 < ?b1"
            by linarith
          moreover
          have
            "?b0 < ?b1 ⟹
             list_less_eq_ns (lms_slice T (Suc j)) (lms_slice T (Suc (SA ! (B ! b))))"
          proof -
            assume "?b0 < ?b1"
            hence "T ! (Suc j) < T ! (Suc (SA ! (B ! b)))"
              using assms(1) s_perm_inv_elims(8) strict_mono_less by blast
            moreover
            have "Suc j < length T"
              using ‹i < length SA› assms(1,4,6) s_perm_inv_elims(5) s_seen_invD(1) by fastforce
            hence "∃as. lms_slice T (Suc j) = T ! (Suc j) # as"
              by (metis dual_order.strict_trans abs_find_next_lms_lower_bound_1 lessI list_slice_Suc
                        lms_slice_def)
            then obtain as where
              "lms_slice T (Suc j) = T ! (Suc j) # as"
              by blast
            moreover
            have "Suc (SA ! (B ! b)) < length T"
              using ‹SA ! i' = Suc (SA ! (B ! b))› ‹i < i'› ‹i' < length SA› assms(1)
                    s_perm_inv_elims(5) s_seen_invD(1) by fastforce
            hence "∃bs. lms_slice T (Suc (SA ! (B ! b))) = T ! (Suc (SA ! (B ! b))) # bs"
              by (metis abs_find_next_lms_lower_bound_1 less_Suc_eq 
                        list_slice_Suc lms_slice_def)
            then obtain bs where
              "lms_slice T (Suc (SA ! (B ! b))) = T ! (Suc (SA ! (B ! b))) # bs"
              by blast
            ultimately show ?thesis
              using list_less_eq_ns_cons by fastforce
          qed
          moreover
          have
            "?b0 = ?b1 ⟹
             list_less_eq_ns (lms_slice T (Suc j)) (lms_slice T (Suc (SA ! (B ! b))))"
          proof -
            assume "?b0 = ?b1"
            with s_index_upper_bound[OF s_perm_inv_elims(2,5)[OF assms(1)] `i' < _`] `i < i'`
            have "i' < bucket_end α T ?b0"
              by (simp add: ‹SA ! i' = Suc (SA ! (B ! b))›)

            have "suffix_type T (SA ! i) = S_type ∨ suffix_type T (SA ! i) = L_type"
              using SL_types.exhaust by blast
            moreover
            have "suffix_type T (SA ! i) = S_type ⟹ ?thesis"
            proof -
              assume "suffix_type T (SA ! i) = S_type"
              with s_seen_invD(3)[OF s_perm_inv_elims(5)[OF assms(1)] `i < length SA`, simplified]
              have "in_s_current_bucket α T B ?b0 i"
                by (simp add: assms(4) assms(6))
              hence "B ! ?b0 ≤ i"
                using in_s_current_bucket_def by blast
              hence "∃m. B ! ?b0 + m = i"
                using less_eqE by blast
              then obtain m0 where
                "B ! ?b0 + m0 = i"
                by blast

              from `B ! ?b0 ≤ i` `i < i'`
              have "∃m. B ! ?b0 + m = i'"
                by presburger
              then obtain m1 where
                "B ! ?b0 + m1 = i'"
                by blast
              hence "B ! ?b0 + m0 ≤ B ! ?b0 + m1"
                by (simp add: ‹B ! α (T ! Suc j) + m0 = i› 
                    ‹i < i'› dual_order.order_iff_strict)
              hence "m0 ≤ m1"
                using add_le_imp_le_left by blast

              have "(list_slice SA (B ! ?b0) (bucket_end α T ?b0)) ! m0 = Suc j"
                using ‹B ! α (T ! Suc j) + m0 = i› ‹i < length SA›
                      ‹in_s_current_bucket α T B ?b0 i› assms(4,6) 
                      in_s_current_bucketD(3)
                by (metis ‹B ! α (T ! Suc j) ≤ i› diff_add_inverse list_slice_nth)
              moreover
              have "(list_slice SA (B ! ?b0) (bucket_end α T ?b0)) ! m1 = Suc (SA ! (B ! b))"
                using ‹B ! ?b0 + m1 = i'› ‹SA ! i' = Suc (SA ! (B ! b))› ‹i' < bucket_end α T ?b0›
                      ‹i' < length SA› 
                by (metis diff_add_inverse le_add1 list_slice_nth)
              moreover
              have "length (list_slice SA (B ! ?b0) (bucket_end α T ?b0))
                    = (bucket_end α T ?b0) - B ! ?b0"
                by (metis assms(1) bucket_end_le_length length_list_slice min_def s_perm_inv_def)
              with `B ! ?b0 + m1 = i'` `i' < bucket_end α T ?b0`
              have "m1 < length (list_slice SA (B ! ?b0) (bucket_end α T ?b0))"
                by linarith
              ultimately
              show ?thesis
                using ordlistns.sorted_nth_mono[OF
                        s_prefix_sorted_invD[OF assms(3) `?b0 ≤ α (Max _)`] `m0 ≤ m1`]
                      ‹m0 ≤ m1› by auto
            qed
            moreover
            have "suffix_type T (SA ! i) = L_type ⟹ ?thesis"
            proof -
              assume "suffix_type T (SA ! i) = L_type"
              with s_seen_invD(2)[OF s_perm_inv_elims(5)[OF assms(1)] `i < length SA`, simplified]
              have "in_l_bucket α T ?b0 i"
                by (simp add: assms(4) assms(6))
              hence "bucket_start α T ?b0 ≤ i"
                by (simp add: in_l_bucket_def)
              hence "∃m. bucket_start α T ?b0 + m = i"
                using less_eqE by blast
              then obtain m0 where
                "bucket_start α T ?b0 + m0 = i"
                by blast

              have "suffix_type T (SA ! i') = L_type ∨ suffix_type T (SA ! i') = S_type"
                using SL_types.exhaust by blast
              moreover
              have "suffix_type T (SA ! i') = S_type ⟹ ?thesis"
              proof -
                assume "suffix_type T (SA ! i') = S_type"

                have "SA ! i < length T"
                  by (meson ‹i < length SA› assms(1) order_refl s_perm_inv_elims(5) s_seen_invD(1))

                have "SA ! i' < length T"
                  by (simp add: ‹suffix_type T (SA ! i') = S_type› suffix_type_s_bound)

                from `?b0 = ?b1`
                have "T ! (Suc j) = T ! Suc (SA ! (B ! b))"
                  using assms(1) s_perm_inv_def strict_mono_eq by blast
                hence "hd (suffix T (SA ! i')) = hd (suffix T (SA ! i))"
                  by (metis ‹SA ! i < length T› ‹SA ! i' < length T› ‹SA ! i' = Suc (SA ! (B ! b))›
                            assms(4) assms(6) list.sel(1) suffix_cons_Suc)
                hence "list_less_ns (lms_slice T (SA ! i)) (lms_slice T (SA ! i'))"
                  using ‹SA ! i < length T› ‹SA ! i' < length T› ‹SA ! i' = Suc (SA ! (B ! b))›
                        ‹T ! Suc j = T ! Suc (SA ! (B ! b))› ‹suffix_type T (SA ! i') = S_type›
                        ‹suffix_type T (SA ! i) = L_type› assms(1,4,6) s_perm_inv_elims(13)
                        lms_slice_l_less_than_s_type by fastforce
                then show ?thesis
                  by (simp add: ‹SA ! i' = Suc (SA ! (B ! b))› assms(4,6))
              qed
              moreover
              have "suffix_type T (SA ! i') = L_type ⟹ ?thesis"
              proof -
                assume "suffix_type T (SA ! i') = L_type"
                with s_seen_invD(2)[OF s_perm_inv_elims(5)[OF assms(1)] `i' < length SA`,
                      simplified `?b0 = ?b1`[symmetric] `SA ! i' = Suc (SA ! (B ! b))`]
                     `SA ! i' = Suc (SA ! (B ! b))`
                have "in_l_bucket α T ?b0 i'"
                  by (simp add: ‹i < i'› dual_order.order_iff_strict)
                hence "i' < l_bucket_end α T ?b0"
                  by (simp add: in_l_bucket_def)
                hence "∃m. bucket_start α T ?b0 + m = i'"
                  by (metis ‹in_l_bucket α T ?b0 i'› in_l_bucket_def less_eqE)
                then obtain m1 where
                  "bucket_start α T ?b0 + m1 = i'"
                  by blast

                let ?zs = "list_slice SA (bucket_start α T ?b0) (l_bucket_end α T ?b0)"

                have "?zs ! m0 = Suc j"
                  using ‹bucket_start α T ?b0 + m0 = i› ‹i < i'› ‹i < length SA›
                        ‹i' < l_bucket_end α T ?b0› assms(4,6)
                  by (metis ‹bucket_start α T (α (T ! Suc j)) ≤ i› 
                            diff_add_inverse dual_order.order_iff_strict 
                            list_slice_nth order.strict_trans1)
                moreover
                have "?zs ! m1 = Suc (SA ! (B ! b))"
                  using ‹SA ! i' = Suc (SA ! (B ! b))› ‹bucket_start α T ?b0 + m1 = i'›
                        ‹i' < l_bucket_end α T ?b0› ‹i' < length SA› 
                  by (metis ‹in_l_bucket α T (α (T ! Suc j)) i'› 
                            diff_add_inverse in_l_bucket_def list_slice_nth)
                moreover
                have "m0 ≤ m1"
                  using ‹bucket_start α T ?b0 + m0 = i› ‹bucket_start α T ?b0 + m1 = i'› ‹i < i'›
                  by linarith
                moreover
                have "length ?zs = l_bucket_end α T ?b0 - bucket_start α T ?b0"
                  by (metis ‹?b0 ≤ α (Max (set T))› add_diff_cancel_left' assms(1) distinct_card
                        l_bucket_end_def l_bucket_size_def l_types_init_def l_types_init_maintained
                        s_perm_inv_def)
                hence "m1 < length ?zs"
                  using ‹bucket_start α T ?b0 + m1 = i'› ‹i' < l_bucket_end α T ?b0› by linarith
                moreover
                from s_prefix_sorted_pre_maintained[OF s_perm_inv_elims(2,4,10,11)[OF assms(1)]
                      assms(2)]
                have "s_prefix_sorted_pre α T SA" .
                ultimately show ?thesis
                  using ordlistns.sorted_nth_mono[OF s_prefix_sorted_preD[of α T SA,
                          OF _ `?b0 ≤ α (Max _)`], of m0 m1]
                  by (simp add: ‹m1 < length ?zs› ‹s_prefix_sorted_pre α T SA› le_less_trans)
              qed
              ultimately show ?thesis
                by blast
            qed
            ultimately show ?thesis
              by blast
          qed
          ultimately have
            "list_less_eq_ns (lms_slice T (Suc j)) (lms_slice T (Suc (SA ! (B ! b))))"
            by blast
          with S0 S1 `T ! j = T ! (?ys ! 0)`
          show ?thesis
            by (simp add: list_less_eq_ns_cons)
        qed
        ultimately show "list_less_eq_ns (lms_slice T j) (map (lms_slice T) ?ys ! 0)"
          by simp
      qed 
      ultimately show ?thesis
        using A by fastforce
    qed
    ultimately show ?thesis
      by simp
  qed
  moreover
  have "b ≠ b' ⟹ ordlistns.sorted (map (lms_slice T) ?xs)"
  proof -
    assume "b ≠ b'"
    with s_sorted_maintained_unchanged_step[OF assms(1,4-) `b' ≤ _`]
         s_prefix_sorted_invD[OF assms(3) `b' ≤ _`]
    show ?thesis
      using ordlistns.sorted_map by blast
  qed
  ultimately show "ordlistns.sorted (map (lms_slice T) ?xs)"
    by blast
qed

theorem abs_induce_s_sorted_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "s_sorted_pre α T SA0"
  and     "s_sorted_inv α T B SA"
  and     "abs_induce_s_step (B, SA, i) (α, T) = (B', SA', i')"
shows " s_sorted_inv α T B' SA'"
proof (rule abs_induce_s_step.elims[OF assms(4)];
       clarsimp simp: assms(3,4) Let_def not_less
                split: if_splits SL_types.splits nat.splits[where ?nat = i] nat.splits)
  assume "B = B'" "SA' = SA"
  with assms(3)
  show "s_sorted_inv α T B' SA"
    by simp
next
  assume "B = B'" "SA' = SA"
  with assms(3)
  show "s_sorted_inv α T B' SA"
    by simp
next
  assume "B = B'" "SA' = SA"
  with assms(3)
  show "s_sorted_inv α T B' SA"
    by simp
next
  assume "B = B'" "SA' = SA"
  with assms(3)
  show "s_sorted_inv α T B' SA"
    by simp
next
  fix j

  let ?b = "α (T ! j)"
  let ?k = "B ! ?b - Suc 0"

  assume A: "i = Suc i'" "Suc i' < length SA" "SA ! Suc i' = Suc j" "suffix_type T j = S_type"
            "B' = B[?b := ?k]" "SA' = SA[?k := j]"

  from s_sorted_inv_maintained_step[OF assms(1-3) A(1-4), of ?b ?k, simplified]
  show "s_sorted_inv α T (B[?b := ?k]) (SA[?k := j])" .
qed

corollary abs_induce_s_sorted_step_alt:
 "⋀a. s_sorted_inv_alt α T SA0 a ⟹ s_sorted_inv_alt α T SA0 (abs_induce_s_step a (α, T))"
proof -
  fix a
  assume "s_sorted_inv_alt α T SA0 a"

  have "∃B SA i. a = (B, SA, i)"
    by (meson prod_cases3)
  then obtain B SA i where
    "a = (B, SA, i)"
    by blast
  with `s_sorted_inv_alt α T SA0 a`
  have P: "s_perm_inv α T B SA0 SA i" "s_sorted_pre α T SA0" "s_sorted_inv α T B SA"
    by simp_all

  from abs_induce_s_step_ex[of "(B, SA, i)" "(α, T)"]
  obtain B' SA' i' where
    Q: "abs_induce_s_step (B, SA, i) (α, T) = (B', SA', i')"
    by blast

  from abs_induce_s_sorted_step[OF P Q] abs_induce_s_perm_step[OF P(1) Q] `s_sorted_pre _ _ _`
  show "s_sorted_inv_alt α T SA0 (abs_induce_s_step a (α, T))"
    using Q ‹a = (B, SA, i)› by auto
qed

theorem abs_induce_s_sorted_alt_maintained:
  assumes "s_sorted_inv_alt α T SA0 (B, SA, length T)"
  shows "s_sorted_inv_alt α T SA0 (abs_induce_s_base α T B SA)"
  unfolding abs_induce_s_base_def
  using repeat_maintain_inv
          [of "s_sorted_inv_alt α T SA0" abs_induce_s_step "(α, T)", OF _ assms(1)]
              abs_induce_s_sorted_step_alt
  by blast

corollary abs_induce_s_sorted_maintained:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B SA0 SA (length T)"
  and     "s_sorted_pre α T SA0"
  and     "s_sorted_inv α T B SA"
shows "s_sorted_inv α T B' SA'"
  using assms abs_induce_s_sorted_alt_maintained by force

theorem abs_induce_s_prefix_sorted_step:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "s_prefix_sorted_pre α T SA0"
  and     "s_prefix_sorted_inv α T B SA"
  and     "abs_induce_s_step (B, SA, i) (α, T) = (B', SA', i')"
shows "s_prefix_sorted_inv α T B' SA'"
proof (rule abs_induce_s_step.elims[OF assms(4)];
       clarsimp simp: assms(3,4) Let_def not_less
                split: if_splits SL_types.splits nat.splits[where ?nat = i] nat.splits)
  assume "B = B'"
  with assms(3)
  show "s_prefix_sorted_inv α T B' SA"
    by simp
next
  assume "B = B'"
  with assms(3)
  show "s_prefix_sorted_inv α T B' SA"
    by simp
next
  assume "B = B'"
  with assms(3)
  show "s_prefix_sorted_inv α T B' SA"
    by simp
next
  assume "B = B'"
  with assms(3)
  show "s_prefix_sorted_inv α T B' SA"
    by simp
next
  fix j

  let ?b = "α (T ! j)"
  let ?k = "B ! ?b - Suc 0"

  assume A: "i = Suc i'" "Suc i' < length SA" "SA ! Suc i' = Suc j" "suffix_type T j = S_type"
            "B' = B[?b := ?k]" "SA' = SA[?k := j]"

  from s_prefix_sorted_inv_maintained_step[OF assms(1-3) A(1-4), of ?b ?k, simplified]
  show "s_prefix_sorted_inv α T (B[?b := ?k]) (SA[?k := j])" .
qed

corollary abs_induce_s_prefix_sorted_step_alt:
 "⋀a. s_prefix_sorted_inv_alt α T SA0 a ⟹
      s_prefix_sorted_inv_alt α T SA0 (abs_induce_s_step a (α, T))"
proof -
  fix a
  assume "s_prefix_sorted_inv_alt α T SA0 a"

  have "∃B SA i. a = (B, SA, i)"
    by (meson prod_cases3)
  then obtain B SA i where
    "a = (B, SA, i)"
    by blast
  with `s_prefix_sorted_inv_alt α T SA0 a`
  have P: "s_perm_inv α T B SA0 SA i" "s_prefix_sorted_pre α T SA0" "s_prefix_sorted_inv α T B SA"
    by simp_all

  from abs_induce_s_step_ex[of "(B, SA, i)" "(α, T)"]
  obtain B' SA' i' where
    Q: "abs_induce_s_step (B, SA, i) (α, T) = (B', SA', i')"
    by blast

  from abs_induce_s_prefix_sorted_step[OF P Q] abs_induce_s_perm_step[OF P(1) Q] `s_prefix_sorted_pre _ _ _`
  show "s_prefix_sorted_inv_alt α T SA0 (abs_induce_s_step a (α, T))"
    using Q ‹a = (B, SA, i)› by auto
qed

theorem abs_induce_s_prefix_sorted_alt_maintained:
  assumes "s_prefix_sorted_inv_alt α T SA0 (B, SA, length T)"
  shows "s_prefix_sorted_inv_alt α T SA0 (abs_induce_s_base α T B SA)"
  unfolding abs_induce_s_base_def
  using repeat_maintain_inv[of "s_prefix_sorted_inv_alt α T SA0" abs_induce_s_step "(α, T)",
          OF _ assms(1)]
        abs_induce_s_prefix_sorted_step_alt
  by blast

corollary abs_induce_s_prefix_sorted_maintained:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B SA0 SA (length T)"
  and     "s_prefix_sorted_pre α T SA0"
  and     "s_prefix_sorted_inv α T B SA"
shows "s_prefix_sorted_inv α T B' SA'"
  using assms abs_induce_s_prefix_sorted_alt_maintained by force

theorem s_sorted_bucket:
  assumes "s_perm_inv α T B SA0 SA 0"
  and     "s_sorted_pre α T SA0"
  and     "s_sorted_inv α T B SA"
  and     "b ≤ α (Max (set T))"
shows "ordlistns.sorted (map (suffix T) (list_slice SA (bucket_start α T b) (bucket_end α T b)))"
      (is "ordlistns.sorted (map (suffix T) ?xs)")
proof -
  let ?ys = "list_slice SA (bucket_start α T b) (l_bucket_end α T b)"
  and ?zs = "list_slice SA (s_bucket_start α T b) (bucket_end α T b)"

  from s_perm_inv_0_B_val[OF assms(1,4)]
  have "B ! b = s_bucket_start α T b" .

  from s_sorted_pre_maintained[OF s_perm_inv_elims(2,4,10,11)[OF assms(1)] assms(2)]
  have "s_sorted_pre α T SA" .

  have "?xs = ?ys @ ?zs"
    by (metis bucket_start_le_s_bucket_start l_bucket_end_le_bucket_end list_slice_append
          s_bucket_start_eq_l_bucket_end)
  hence "map (suffix T) ?xs = map (suffix T) ?ys @ map (suffix T) ?zs"
    by simp
  moreover
  from s_sorted_preD[OF `s_sorted_pre _ _ SA` `b ≤ _`]
  have "ordlistns.sorted (map (suffix T) ?ys)" .
  moreover
  from s_sorted_invD[OF assms(3,4), simplified `_ = s_bucket_start α _ _`]
  have "ordlistns.sorted (map (suffix T) ?zs)" .
  moreover
  have "∀y ∈ set (map (suffix T) ?ys). ∀z ∈ set (map (suffix T) ?zs). list_less_eq_ns y z"
  proof(safe)
    fix y z
    assume "y ∈ set (map (suffix T) ?ys)" "z ∈ set (map (suffix T) ?zs)"
    with in_set_mapD[of y "suffix T" ?ys]
         in_set_mapD[of z "suffix T" ?zs]
    obtain i j where
      "y = suffix T i" "i ∈ set ?ys" 
      "z = suffix T j" "j ∈ set ?zs"
      by blast

    from l_types_initD(1)[OF l_types_init_maintained[OF s_perm_inv_elims(2,4,10-12)[OF assms(1)]]
          `b ≤ _`]
         `i ∈ set ?ys`
    have "i ∈ l_bucket α T b"
      by blast
    hence "suffix_type T i = L_type" "α (T ! i) = b" "i < length T"
      by (simp add: l_bucket_def bucket_def)+
    moreover
    from s_bucket_eq_list_slice[OF s_perm_inv_elims(1,3,11)[OF assms(1)] `b ≤ _`
          `B ! b = s_bucket_start α _ _`]
         `j ∈ set ?zs`
    have "j ∈ s_bucket α T b"
      by blast
    hence "suffix_type T j = S_type" "α (T ! j) = b" "j < length T"
      by (simp add: s_bucket_def bucket_def)+
    moreover
    have "T ! i = T ! j"
      using calculation(2,5) s_perm_inv_elims(8)[OF assms(1)] strict_mono_eq by fastforce
    ultimately have "list_less_eq_ns (suffix T i) (suffix T j)"
      using l_less_than_s_type_suffix[of j T i] by simp
    then show "list_less_eq_ns y z"
      using ‹y = suffix T i› ‹z = suffix T j› by blast
  qed
  ultimately show ?thesis
    by (simp add: ordlistns.sorted_append)
qed

theorem abs_induce_s_base_sorted:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B SA0 SA (length T)"
  and     "s_sorted_pre α T SA0"
  and     "s_sorted_inv α T B SA"
shows "ordlistns.sorted (map (suffix T) SA')"
proof (intro sorted_wrt_mapI)
  fix i j
  assume "i < j" "j < length SA'"
  hence "i < length T" "j < length T"
    by (metis (no_types, lifting) abs_induce_s_perm_maintained 
              assms(1,2) order.strict_trans s_perm_inv_elims(11))+

  let ?goal = "list_less_eq_ns (suffix T (SA' ! i)) (suffix T (SA' ! j))"

  from index_in_bucket_interval_gen[OF `i < length _` s_perm_inv_elims(8)[OF assms(2)]]
  obtain b0 where
    "b0 ≤ α (Max (set T))"
    "bucket_start α T b0 ≤ i"
    "i < bucket_end α T b0"
    by blast

  from index_in_bucket_interval_gen[OF `j < length T` s_perm_inv_elims(8)[OF assms(2)]]
  obtain b1 where
    "b1 ≤ α (Max (set T))"
    "bucket_start α T b1 ≤ j"
    "j < bucket_end α T b1"
    by blast

  from abs_induce_s_perm_maintained[OF assms(1,2)]
  have "s_perm_inv α T B' SA0 SA' n" .
  moreover
  have "n = 0"
    by (metis Pair_inject assms(1) abs_induce_s_base_index)
  ultimately have "s_perm_inv α T B' SA0 SA' 0"
    by simp

  let ?xs = "list_slice SA' (bucket_start α T b0) (bucket_end α T b0)"
  and ?ys = "list_slice SA' (bucket_start α T b1) (bucket_end α T b1)"

  have "b0 ≤ b1"
  proof (rule ccontr)
    assume "¬ b0 ≤ b1"
    hence "b1 < b0"
      by (simp add: not_le)
    hence "bucket_end α T b1 ≤ bucket_start α T b0"
      by (simp add: less_bucket_end_le_start)
    with `j < bucket_end α T b1` `bucket_start α T b0 ≤ i` `i < j`
    show False
      by linarith
  qed
  hence "b0 = b1 ∨ b0 < b1"
    by (simp add: nat_less_le)
  moreover
  have "b0 < b1 ⟹ ?goal"
  proof -
    assume "b0 < b1"
    moreover
    from s_perm_inv_0_list_slice_bucket[OF `s_perm_inv _ _ _ _ _ 0` `b0 ≤ α _`]
    have "set ?xs = bucket α T b0" .
    hence "SA' ! i ∈ bucket α T b0"
      by (metis ‹bucket_start α T b0 ≤ i› ‹i < bucket_end α T b0› ‹s_perm_inv α T B' SA0 SA' 0›
            bucket_end_le_length list_slice_nth_mem s_perm_inv_elims(11))
    hence "α (T ! (SA' ! i)) = b0" "SA' ! i < length T"
      by (simp add: bucket_def)+
    moreover
    from s_perm_inv_0_list_slice_bucket[OF `s_perm_inv _ _ _ _ _ 0` `b1 ≤ α _`]
    have "set ?ys = bucket α T b1" .
    hence "SA' ! j ∈ bucket α T b1"
      by (metis ‹bucket_start α T b1 ≤ j› ‹j < bucket_end α T b1› ‹s_perm_inv α T B' SA0 SA' 0›
            bucket_end_le_length list_slice_nth_mem s_perm_inv_elims(11))
    hence "α (T ! (SA' ! j)) = b1" "SA' ! j < length T"
      by (simp add: bucket_def)+
    ultimately have "T ! (SA' ! i) < T ! (SA' ! j)"
      using assms(2) s_perm_inv_elims(8) strict_mono_less by blast
    then show ?thesis
      by (metis ‹SA' ! i < length T› ‹SA' ! j < length T› less_imp_le list_less_eq_ns_cons neq_iff
            suffix_cons_Suc)
  qed
  moreover
  have "b0 = b1 ⟹ ?goal"
  proof -
    assume "b0 = b1"
    with `j < bucket_end α T b1`
    have "j < bucket_end α T b0"
      by simp

    have "∃i'. i = bucket_start α T b0 + i'"
      using ‹bucket_start α T b0 ≤ i› nat_le_iff_add by blast
    then obtain i' where
      "i = bucket_start α T b0 + i'"
      by blast

    have "∃j'. j = bucket_start α T b0 + j'"
      by (simp add: ‹b0 = b1› ‹bucket_start α T b1 ≤ j› le_Suc_ex)
    then obtain j' where
      "j = bucket_start α T b0 + j'"
      by blast
    with `i < j` `i = bucket_start α T b0 + i'`
    have "i' ≤ j'"
      by linarith

    have "j' < length ?xs"
      by (metis ‹b0 = b1› ‹j < bucket_end α T b1› ‹j = bucket_start α T b0 + j'›
                ‹s_perm_inv α T B' SA0 SA' n› add.commute bucket_end_le_length length_list_slice
                less_diff_conv min_def s_perm_inv_elims(11))
    with ordlistns.sorted_nth_mono[OF s_sorted_bucket[OF `s_perm_inv _ _ _ _ _ 0` assms(3)
          abs_induce_s_sorted_maintained[OF assms] `b0 ≤ α _`] `i' ≤ j'`]
    have "list_less_eq_ns (suffix T (?xs ! i')) (suffix T (?xs ! j'))"
      using ‹i' ≤ j'› nth_map by auto
    moreover
    have "SA' ! i = ?xs ! i'"
      using ‹i < bucket_end α T b0› ‹i < length T› ‹i = bucket_start α T b0 + i'›
            ‹s_perm_inv α T B' SA0 SA' n› s_perm_inv_elims(11) 
      by (metis ‹bucket_start α T b0 ≤ i› diff_add_inverse list_slice_nth)
     moreover
    have "SA' ! j = ?xs ! j'"
      using ‹j < bucket_end α T b0› ‹j < length SA'› 
            ‹j = bucket_start α T b0 + j'› 
      by (simp add: nth_list_slice)
    ultimately show ?goal
      by simp
  qed
  ultimately show ?goal
    by blast
qed

theorem s_prefix_sorted_bucket:
  assumes "s_perm_inv α T B SA0 SA 0"
  and     "s_prefix_sorted_pre α T SA0"
  and     "s_prefix_sorted_inv α T B SA"
  and     "b ≤ α (Max (set T))"
shows "ordlistns.sorted (map (lms_slice T) (list_slice SA (bucket_start α T b) (bucket_end α T b)))"
      (is "ordlistns.sorted (map (lms_slice T) ?xs)")
proof -
  let ?ys = "list_slice SA (bucket_start α T b) (l_bucket_end α T b)"
  and ?zs = "list_slice SA (s_bucket_start α T b) (bucket_end α T b)"

  from s_perm_inv_0_B_val[OF assms(1,4)]
  have "B ! b = s_bucket_start α T b" .

  from s_prefix_sorted_pre_maintained[OF s_perm_inv_elims(2,4,10,11)[OF assms(1)] assms(2)]
  have "s_prefix_sorted_pre α T SA" .

  have "?xs = ?ys @ ?zs"
    by (metis bucket_start_le_s_bucket_start l_bucket_end_le_bucket_end list_slice_append
          s_bucket_start_eq_l_bucket_end)
  hence "map (lms_slice T) ?xs = map (lms_slice T) ?ys @ map (lms_slice T) ?zs"
    by simp
  moreover
  from s_prefix_sorted_preD[OF `s_prefix_sorted_pre _ _ SA` `b ≤ _`]
  have "ordlistns.sorted (map (lms_slice T) ?ys)" .
  moreover
  from s_prefix_sorted_invD[OF assms(3,4), simplified `_ = s_bucket_start α _ _`]
  have "ordlistns.sorted (map (lms_slice T) ?zs)" .
  moreover
  have "∀y ∈ set (map (lms_slice T) ?ys). ∀z ∈ set (map (lms_slice T) ?zs).
          list_less_eq_ns y z"
  proof safe
    fix y z
    assume "y ∈ set (map (lms_slice T) ?ys)"
           "z ∈ set (map (lms_slice T) ?zs)"
    with in_set_mapD[of y "lms_slice T" ?ys]
         in_set_mapD[of z "lms_slice T" ?zs]
    obtain i j where
      "y = lms_slice T i" 
      "i ∈ set ?ys"
      "z = lms_slice T j"
      "j ∈ set ?zs"
      by blast

    from l_types_initD(1)[OF l_types_init_maintained[OF s_perm_inv_elims(2,4,10-12)[OF assms(1)]]
          `b ≤ _`]
         `i ∈ set ?ys`
    have "i ∈ l_bucket α T b"
      by blast
    hence "suffix_type T i = L_type" "α (T ! i) = b" "i < length T"
      by (simp add: l_bucket_def bucket_def)+
    moreover
    from s_bucket_eq_list_slice[OF s_perm_inv_elims(1,3,11)[OF assms(1)] `b ≤ _`
          `B ! b = s_bucket_start α _ _`]
         `j ∈ set ?zs`
    have "j ∈ s_bucket α T b"
      by blast
    hence "suffix_type T j = S_type" "α (T ! j) = b" "j < length T"
      by (simp add: s_bucket_def bucket_def)+
    moreover
    have "T ! i = T ! j"
      using assms(1) calculation(2,5) s_perm_inv_elims(8) strict_mono_eq by fastforce
    ultimately have "list_less_eq_ns (lms_slice T i) (lms_slice T j)"
      using lms_slice_l_less_than_s_type[of i T j] by simp
    then show "list_less_eq_ns y z"
      by (simp add: ‹y = lms_slice T i› ‹z = lms_slice T j›)
  qed
  ultimately show ?thesis
    by (simp add: ordlistns.sorted_append)
qed

theorem abs_induce_s_base_prefix_sorted:
  assumes "abs_induce_s_base α T B SA = (B', SA', n)"
  and     "s_perm_inv α T B SA0 SA (length T)"
  and     "s_prefix_sorted_pre α T SA0"
  and     "s_prefix_sorted_inv α T B SA"
shows "ordlistns.sorted (map (lms_slice T) SA')"
proof (intro sorted_wrt_mapI)
  fix i j
  assume "i < j" "j < length SA'"
  hence "i < length T" "j < length T"
    by (metis (no_types, lifting) abs_induce_s_perm_maintained 
              assms(1,2) order.strict_trans s_perm_inv_elims(11))+

  let ?goal = "list_less_eq_ns (lms_slice T (SA' ! i)) (lms_slice T (SA' ! j))"

  from index_in_bucket_interval_gen[OF `i < length _` s_perm_inv_elims(8)[OF assms(2)]]
  obtain b0 where
    "b0 ≤ α (Max (set T))"
    "bucket_start α T b0 ≤ i"
    "i < bucket_end α T b0"
    by blast

  from index_in_bucket_interval_gen[OF `j < length T` s_perm_inv_elims(8)[OF assms(2)]]
  obtain b1 where
    "b1 ≤ α (Max (set T))"
    "bucket_start α T b1 ≤ j"
    "j < bucket_end α T b1"
    by blast

  from abs_induce_s_perm_maintained[OF assms(1,2)]
  have "s_perm_inv α T B' SA0 SA' n" .
  moreover
  have "n = 0"
    by (metis Pair_inject assms(1) abs_induce_s_base_index)
  ultimately have "s_perm_inv α T B' SA0 SA' 0"
    by simp

  let ?xs = "list_slice SA' (bucket_start α T b0) (bucket_end α T b0)"
  and ?ys = "list_slice SA' (bucket_start α T b1) (bucket_end α T b1)"

  have "b0 ≤ b1"
  proof (rule ccontr)
    assume "¬b0 ≤ b1"
    hence "b1 < b0"
      by (simp add: not_le)
    hence "bucket_end α T b1 ≤ bucket_start α T b0"
      by (simp add: less_bucket_end_le_start)
    with `j < bucket_end α T b1` `bucket_start α T b0 ≤ i` `i < j`
    show False
      by linarith
  qed
  hence "b0 = b1 ∨ b0 < b1"
    by (simp add: nat_less_le)
  moreover
  have "b0 < b1 ⟹ ?goal"
  proof -
    assume "b0 < b1"
    moreover
    from s_perm_inv_0_list_slice_bucket[OF `s_perm_inv _ _ _ _ _ 0` `b0 ≤ α _`]
    have "set ?xs = bucket α T b0" .
    hence "SA' ! i ∈ bucket α T b0"
      by (metis ‹bucket_start α T b0 ≤ i› ‹i < bucket_end α T b0› ‹s_perm_inv α T B' SA0 SA' 0›
            bucket_end_le_length list_slice_nth_mem s_perm_inv_elims(11))
    hence "α (T ! (SA' ! i)) = b0" "SA' ! i < length T"
      by (simp add: bucket_def)+
    moreover
    from s_perm_inv_0_list_slice_bucket[OF `s_perm_inv _ _ _ _ _ 0` `b1 ≤ α _`]
    have "set ?ys = bucket α T b1" .
    hence "SA' ! j ∈ bucket α T b1"
      by (metis ‹bucket_start α T b1 ≤ j› ‹j < bucket_end α T b1› ‹s_perm_inv α T B' SA0 SA' 0›
            bucket_end_le_length list_slice_nth_mem s_perm_inv_elims(11))
    hence "α (T ! (SA' ! j)) = b1" "SA' ! j < length T"
      by (simp add: bucket_def)+
    ultimately have "T ! (SA' ! i) < T ! (SA' ! j)"
      using assms(2) s_perm_inv_elims(8) strict_mono_less by blast
    then show ?thesis
      by (metis ‹SA' ! i < length T› ‹SA' ! j < length T› abs_find_next_lms_lower_bound_1 
            less_SucI less_imp_le list_less_eq_ns_cons list_slice_Suc neq_iff lms_slice_def)
  qed
  moreover
  have "b0 = b1 ⟹ ?goal"
  proof -
    assume "b0 = b1"
    with `j < bucket_end α T b1`
    have "j < bucket_end α T b0"
      by simp

    have "∃i'. i = bucket_start α T b0 + i'"
      using ‹bucket_start α T b0 ≤ i› nat_le_iff_add by blast
    then obtain i' where
      "i = bucket_start α T b0 + i'"
      by blast

    have "∃j'. j = bucket_start α T b0 + j'"
      by (simp add: ‹b0 = b1› ‹bucket_start α T b1 ≤ j› le_Suc_ex)
    then obtain j' where
      "j = bucket_start α T b0 + j'"
      by blast
    with `i < j` `i = bucket_start α T b0 + i'`
    have "i' ≤ j'"
      by linarith

    have "j' < length ?xs"
      by (metis ‹b0 = b1› 
            ‹j < bucket_end α T b1› 
            ‹j = bucket_start α T b0 + j'›
            ‹s_perm_inv α T B' SA0 SA' n› 
            add.commute bucket_end_le_length length_list_slice
            less_diff_conv min_def s_perm_inv_elims(11))
    with ordlistns.sorted_nth_mono
           [OF s_prefix_sorted_bucket
                 [OF `s_perm_inv _ _ _ _ _ 0` assms(3)
                     abs_induce_s_prefix_sorted_maintained
                        [OF assms] `b0 ≤ α _`] `i' ≤ j'`]
    have "list_less_eq_ns (lms_slice T (?xs ! i')) (lms_slice T (?xs ! j'))"
      using ‹i' ≤ j'› nth_map by auto
    moreover
    have "SA' ! i = ?xs ! i'"
      using ‹i < bucket_end α T b0› 
            ‹i < length T› 
            ‹i = bucket_start α T b0 + i'›
            ‹s_perm_inv α T B' SA0 SA' n›  
            ‹j' < length (list_slice SA' 
                     (bucket_start α T b0) 
                     (bucket_end α T b0))› 
      by (metis ‹i' ≤ j'› nth_list_slice order.strict_trans1)
    moreover
    have "SA' ! j = ?xs ! j'"
      using ‹j < bucket_end α T b0› ‹j < length SA'› 
            ‹j = bucket_start α T b0 + j'› 
      by (simp add: nth_list_slice)
    ultimately show ?goal
      by simp
  qed
  ultimately show ?goal
    by blast
qed

section "Induce S Correctness Theorems"

theorem abs_induce_s_perm:
  assumes "s_perm_pre α T B SA (length T)"
  shows "abs_induce_s α T B SA <~~> [0..< length T]"
proof -
  from s_perm_inv_established assms[simplified s_perm_pre_def]
  have "s_perm_inv α T B SA SA (length T)"
    by blast
  moreover
  from abs_induce_s_base_index[of α T B SA]
  obtain B' SA' where
    "abs_induce_s_base α T B SA = (B', SA', 0)"
    by blast
  ultimately have "s_perm_inv α T B' SA SA' 0"
    using abs_induce_s_perm_maintained[of α T B SA B' SA' 0 SA]
    by blast
  hence "SA' <~~> [0..< length T]"
    using abs_induce_s_base_perm[OF `abs_induce_s_base α T B SA = (B', SA', 0)`]
    by blast
  with `abs_induce_s_base α T B SA = (B', SA', 0)`
  show ?thesis
    by (simp add: abs_induce_s_def)
qed


 ―‹ Used in SAIS algorithm as part of inducing the suffix ordering based on LMS ›
theorem abs_induce_s_sorted:
  assumes "s_perm_pre α T B SA (length T)"
  and     "s_sorted_pre α T SA"
shows "ordlistns.sorted (map (suffix T) (abs_induce_s α T B SA))"
proof -
  from s_perm_inv_established assms(1)[simplified s_perm_pre_def]
  have "s_perm_inv α T B SA SA (length T)"
    by blast
  moreover
  from abs_induce_s_base_index[of α T B SA]
  obtain B' SA' where
    "abs_induce_s_base α T B SA = (B', SA', 0)"
    by blast
  moreover
  from s_sorted_inv_established assms(1)[simplified s_perm_pre_def]
  have "s_sorted_inv α T B SA"
    by blast
  ultimately have "ordlistns.sorted (map (suffix T) SA')"
    using abs_induce_s_base_sorted[OF _ _ assms(2), of B SA B' SA' 0]
    by blast
  then show ?thesis
    by (simp add: ‹abs_induce_s_base α T B SA = (B', SA', 0)› abs_induce_s_def)
qed

 ―‹ Used in SAIS algorithm as part of inducing the prefix ordering based on LMS ›
theorem abs_induce_s_prefix_sorted:
  assumes "s_perm_pre α T B SA (length T)"
  and     "s_prefix_sorted_pre α T SA"
shows "ordlistns.sorted (map (lms_slice T) (abs_induce_s α T B SA))"
proof -

  from s_perm_inv_established assms(1)[simplified s_perm_pre_def]
  have "s_perm_inv α T B SA SA (length T)"
    by blast
  moreover
  from abs_induce_s_base_index[of α T B SA]
  obtain B' SA' where
    "abs_induce_s_base α T B SA = (B', SA', 0)"
    by blast
  moreover
  from s_prefix_sorted_inv_established assms(1)[simplified s_perm_pre_def]
  have "s_prefix_sorted_inv α T B SA"
    by blast
  ultimately have "ordlistns.sorted (map (lms_slice T) SA')"
    using abs_induce_s_base_prefix_sorted[OF _ _ assms(2), of B SA B' SA' 0]
    by blast
  then show ?thesis
    by (simp add: ‹abs_induce_s_base α T B SA = (B', SA', 0)› abs_induce_s_def)
qed

end