Theory Abs_Bucket_Insert_Verification

theory Abs_Bucket_Insert_Verification
  imports 
    "../abs-def/Abs_SAIS"
    "../../util/List_Util"
    "../../util/List_Slice"
   

begin

section ‹Bucket Insert with Ghost State›

fun bucket_insert_abs' ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   nat list ⇒
   nat list ⇒
   nat list ⇒
   nat list ⇒
   nat list × nat list × nat list"
where
  "bucket_insert_abs' α T B SA gs [] = (SA, B, gs)" |
  "bucket_insert_abs' α T B SA gs (x # xs) =
    (let b = α (T ! x);
         k = B ! b - Suc 0;
         SA' = SA[k := x];
         B' = B[b := k];
         gs' = gs @ [x]
     in bucket_insert_abs' α T B' SA' gs' xs)"

section ‹Simple Properties›

lemma abs_bucket_insert_length:
  "length (abs_bucket_insert α T B SA xs) = length SA"
  by (induct xs arbitrary: B SA; simp add: Let_def)

lemma abs_bucket_insert_equiv:
  "abs_bucket_insert α T B SA xs = fst (bucket_insert_abs' α T B SA gs xs)"
  by (induct xs arbitrary: B SA gs; simp add: Let_def)

section ‹Invariants›

subsection ‹Defintions and Simple Helper Lemmas›

subsubsection ‹Distinctness›

definition lms_distinct_inv :: 
  "('a :: {linorder, order_bot}) list ⇒ nat list ⇒ nat list ⇒ bool"
where
  "lms_distinct_inv T SA LMS = 
     distinct ((filter (λx. x < length T) SA) @ LMS)"

lemma lms_inv_distinct_inv_helper:
  assumes "lms_distinct_inv T SA LMS"
  shows   "distinct (filter (λx. x < length T) SA) ∧ 
           distinct LMS ∧
           set (filter (λx. x < length T) SA) ∩ set LMS = {}"
  using assms distinct_append lms_distinct_inv_def by blast

subsubsection ‹LMS Bucket Ptr›

definition cur_lms_types ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat ⇒ nat set"
where
  "cur_lms_types α T SA b = 
      {i|i. i ∈ set SA ∧ 
      i ∈ lms_bucket α T b }"

lemma cur_lms_subset_SA:
  "cur_lms_types α T SA b ⊆ set SA"
  using cur_lms_types_def by blast

lemma cur_lms_subset_lms_bucket:
  "cur_lms_types α T SA b ⊆ lms_bucket α T b"
  using cur_lms_types_def by blast

definition num_lms_types ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat ⇒ nat"
where
  "num_lms_types α T SA b = 
    card (cur_lms_types α T SA b)"

lemma num_lms_types_upper_bound:
  "num_lms_types α T SA b ≤ lms_bucket_size α T b"
  by (metis not_le cur_lms_subset_lms_bucket num_lms_types_def
            finite_lms_bucket lms_bucket_size_def card_mono)

definition lms_bucket_ptr_inv ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 
   'a list ⇒ nat list ⇒ nat list ⇒ bool"
where
  "lms_bucket_ptr_inv α T B SA ≡
     (∀b ≤ α (Max (set T)). 
        B ! b + num_lms_types α T SA b = bucket_end α T b)"

lemma lms_bucket_ptr_invD:
  assumes "lms_bucket_ptr_inv α T B SA"
  and     "b ≤ α (Max (set T))"
  shows "B ! b + num_lms_types α T SA b = bucket_end α T b"
  using assms lms_bucket_ptr_inv_def by blast

lemma lms_bucket_ptr_lower_bound:
  assumes "lms_bucket_ptr_inv α T B SA"
  and     "b ≤ α (Max (set T))"
  shows "lms_bucket_start α T b ≤ B ! b"
proof -
  from lms_bucket_ptr_invD[OF assms]
  have "B ! b + num_lms_types α T SA b = bucket_end α T b" .
  then show ?thesis
    by (metis add.commute add_le_cancel_left lms_bucket_pl_size_eq_end num_lms_types_upper_bound)
qed

lemma lms_bucket_ptr_upper_bound:
  assumes "lms_bucket_ptr_inv α T B SA"
  and     "b ≤ α (Max (set T))"
  shows   "B ! b ≤ bucket_end α T b"
  by (metis assms le_iff_add lms_bucket_ptr_inv_def)

subsubsection ‹Unknowns›

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

lemma lms_unknowns_invD:
  assumes "lms_unknowns_inv α T B SA"
  and     "b ≤ α (Max (set T))"
  and     "lms_bucket_start α T b ≤ i"
  and     "i < B ! b"
  shows "SA ! i = length T"
  using assms lms_unknowns_inv_def by blast

subsubsection ‹Locations›

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

lemma lms_locations_invD:
  assumes "lms_locations_inv α T B SA"
  and     "b ≤ α (Max (set T))"
  and     "B ! b ≤ i" 
  and     "i < bucket_end α T b" 
  shows "SA ! i ∈ lms_bucket α T b"
  using assms lms_locations_inv_def by blast

subsubsection ‹Unchanged›

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

lemma lms_unchanged_invD:
  assumes "lms_unchanged_inv α T B SA SA'"
  and     " b ≤ α (Max (set T))" 
  and     "bucket_start α T b ≤ i"
  and     "i < B ! b"
  shows "SA' ! i = SA ! i"
  using assms lms_unchanged_inv_def by blast

subsubsection ‹Inserted›

definition lms_inserted_inv :: 
  "nat list ⇒ nat list ⇒ nat list ⇒ nat list ⇒ bool"
where
  "lms_inserted_inv LMS SA LMSa LMSb ≡ 
      LMS = LMSa @ LMSb ∧ 
      set LMSa ⊆ set SA"

lemma lms_inserted_invD:
   "⋀LMS SA LMSa LMSb. lms_inserted_inv LMS SA LMSa LMSb ⟹ LMS = LMSa @ LMSb"
   "⋀LMS SA LMSa LMSb. lms_inserted_inv LMS SA LMSa LMSb ⟹ set LMSa ⊆ set SA"
  unfolding lms_inserted_inv_def by blast+

subsubsection ‹Sorted›

definition lms_sorted_inv :: "('a :: {linorder, order_bot}) list ⇒ nat list ⇒ nat list ⇒ bool"
where
"lms_sorted_inv T LMS SA ≡
  (∀j < length SA.
    ∀i < j.
      SA ! i ∈ set LMS ∧ SA ! j ∈ set LMS ⟶
        (T ! (SA ! i) ≠ T ! (SA ! j) ⟶ T ! (SA ! i) < T ! (SA ! j)) ∧
        (T ! (SA ! i) = T ! (SA ! j) ⟶
          (∃j' < length LMS. ∃i' < j'. LMS ! i' = SA ! j ∧ LMS ! j' = SA ! i))
  )"

lemma lms_sorted_invD:
  "⟦lms_sorted_inv T LMS SA; j < length SA; i < j; SA ! i ∈ set LMS; SA ! j ∈ set LMS⟧ ⟹
   (T ! (SA ! i) ≠ T ! (SA ! j) ⟶ T ! (SA ! i) < T ! (SA ! j)) ∧
   (T ! (SA ! i) = T ! (SA ! j) ⟶
    (∃j' < length LMS. ∃i' < j'. LMS ! i' = SA ! j ∧ LMS ! j' = SA ! i))"
  using lms_sorted_inv_def by blast

lemma lms_sorted_invD1:
  "⟦lms_sorted_inv T LMS SA; j < length SA; i < j; 
  SA ! i ∈ set LMS; SA ! j ∈ set LMS;
    T ! (SA ! i) ≠ T ! (SA ! j)⟧ ⟹
   T ! (SA ! i) < T ! (SA ! j)"
  using lms_sorted_inv_def by blast

lemma lms_sorted_invD2:
  "⟦lms_sorted_inv T LMS SA; j < length SA; i < j; SA ! i ∈ set LMS; SA ! j ∈ set LMS;
    T ! (SA ! i) = T ! (SA ! j)⟧ ⟹
   ∃j' < length LMS. ∃i' < j'. LMS ! i' = SA ! j ∧ LMS ! j' = SA ! i"
  using lms_sorted_inv_def by blast

subsection ‹Combined Invariant›

definition lms_inv ::
  "('a :: {linorder, order_bot} ⇒ nat) ⇒
   'a list ⇒
    nat list ⇒
    nat list ⇒
    nat list ⇒
    nat list ⇒
    nat list ⇒
    nat list ⇒
    bool"
where
"lms_inv α T B LMS LMSa LMSb SA0 SA ≡
  lms_distinct_inv T SA LMSb ∧
  lms_bucket_ptr_inv α T B SA ∧
  lms_unknowns_inv α T B SA ∧
  lms_locations_inv α T B SA ∧
  lms_unchanged_inv α T B SA0 SA ∧
  lms_inserted_inv LMS SA LMSa LMSb ∧
  lms_sorted_inv T LMS SA ∧
  strict_mono α ∧
  α (Max (set T)) < length B ∧
  set LMS ⊆ {i. abs_is_lms T i} ∧
  length SA0 = length T ∧
  length SA = length T ∧
  (∀i < length T. SA0 ! i = length T)"

lemma lms_invD:
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ lms_distinct_inv T SA LMSb"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ lms_bucket_ptr_inv α T B SA"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ lms_unknowns_inv α T B SA"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ lms_locations_inv α T B SA"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ lms_unchanged_inv α T B SA0 SA"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ lms_inserted_inv LMS SA LMSa LMSb"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ lms_sorted_inv T LMS SA"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ strict_mono α"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ α (Max (set T)) < length B"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ set LMS ⊆ {i. abs_is_lms T i}"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ length SA0 = length T"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ length SA = length T"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ ∀i < length T. SA0 ! i = length T"
  unfolding lms_inv_def by blast+

lemma lms_inv_lms_helper:
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ ∀x ∈ set LMS. abs_is_lms T x"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ ∀x ∈ set LMSa. abs_is_lms T x"
  "lms_inv α T B LMS LMSa LMSb SA0 SA ⟹ ∀x ∈ set LMSb. abs_is_lms T x"
  using lms_invD(10) lms_inserted_invD(1)[OF lms_invD(6)] by fastforce+

subsection ‹Helpers›

lemma lms_distinct_bucket_ptr_lower_bound:
  assumes "b = α (T ! x)"
  and     "lms_distinct_inv T SA (x # LMS)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "strict_mono α"
  and     "∀i ∈ set (x # LMS). abs_is_lms T i"
shows "lms_bucket_start α T b < B ! b"
proof (rule ccontr)
  assume "¬ lms_bucket_start α T b < B ! b"
  hence "B ! b ≤ lms_bucket_start α T b"
    by simp
  moreover
  from lms_bucket_ptr_invD[OF assms(3), of b] assms(1,4,5)
  have "B ! b + num_lms_types α T SA b = bucket_end α T b"
    by (simp add: abs_is_lms_imp_less_length strict_mono_leD)
  ultimately
  have "lms_bucket_start α T b + num_lms_types α T SA b ≥ bucket_end α T b"
    by linarith
  with lms_bucket_pl_size_eq_end
  have "num_lms_types α T SA b ≥ lms_bucket_size α T b"
    by (metis add_le_cancel_left)
  with card_seteq[OF finite_lms_bucket cur_lms_subset_lms_bucket]
  have "cur_lms_types α T SA b = lms_bucket α T b"
    by (simp add: lms_bucket_size_def num_lms_types_def)
  with cur_lms_subset_SA
  have "lms_bucket α T b ⊆ set SA"
    by blast
  moreover
  from assms(1,5)
  have "x ∈ lms_bucket α T b"
    by (simp add: bucket_def abs_is_lms_imp_less_length lms_bucket_def)
  ultimately
  have "x ∈ set SA"
    by blast
  moreover
  from assms(2,5)
  have "x ∉ set SA"
    by (simp add: abs_is_lms_imp_less_length lms_distinct_inv_def)
  ultimately
  show False
    by blast
qed

lemma lms_next_insert_at_unknown:
  assumes "b = α (T ! x)"
  and     "k = (B ! b) - Suc 0"
  and     "lms_distinct_inv T SA (x # LMS)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "lms_unknowns_inv α T B SA"
  and     "strict_mono α"
  and     "length SA = length T"
  and     "∀i ∈ set (x # LMS). abs_is_lms T i"
shows "k < length SA ∧ SA ! k = length T"
proof -

  from lms_distinct_bucket_ptr_lower_bound[OF assms(1,3-4,6,8)]
  have "lms_bucket_start α T b < B ! b"
    by assumption
   with assms(2)
  have "lms_bucket_start α T b ≤ k" "k < B ! b"
    by linarith+
  with lms_unknowns_invD[OF assms(5), of b k] assms(1,6,8)
  have "SA ! k = length T"
    by (simp add: abs_is_lms_imp_less_length strict_mono_less_eq)
  moreover
  from `k < B ! b` lms_bucket_ptr_invD[OF assms(4), of b] assms(1,6,8)
  have "k < bucket_end α T b"
    by (simp add: assms(7) abs_is_lms_imp_less_length strict_mono_less_eq)
  with assms(7)
  have  "k < length SA"
    by (metis bucket_end_le_length dual_order.strict_trans1)
  ultimately
  show ?thesis
    by blast
qed

lemma lms_distinct_slice:
  assumes "lms_distinct_inv T SA LMS"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "lms_locations_inv α T B SA"
  and     "length SA = length T"
  and     "b ≤ α (Max (set T ))"
shows "distinct (list_slice SA (B ! b) (bucket_end α T b))"
proof -
  from assms(4)
  have "bucket_end α T b ≤ length SA"
    by (simp add: bucket_end_le_length)

  from lms_bucket_ptr_upper_bound[OF assms(2,5)]
  have "B ! b ≤ bucket_end α T b" .

  from lms_locations_invD[OF assms(3,5)]
  have "∀i. B ! b ≤ i ∧ i < bucket_end α T b ⟶ SA ! i ∈ lms_bucket α T b"
    by blast
  hence "∀i. B ! b ≤ i ∧ i < bucket_end α T b ⟶ SA ! i < length T"
    by (simp add: abs_is_lms_imp_less_length lms_bucket_def)

  have "∀x ∈ set (list_slice SA (B ! b) (bucket_end α T b)). x < length T"
  proof
    fix x
    assume A: "x ∈ set (list_slice SA (B ! b) (bucket_end α T b))"
    from in_set_conv_nth[THEN iffD1, OF A]
    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 "(list_slice SA (B ! b) (bucket_end α T b)) ! i = SA ! (B ! b + i)"
      by blast
    moreover
    from `i < length (list_slice SA (B ! b) (bucket_end α T b))`
    have "B ! b + i < bucket_end α T b"
      by (simp add: ‹bucket_end α T b ≤ length SA› 
                    length_list_slice)
    with `∀i. B ! b ≤ i ∧ i < bucket_end α T b ⟶ SA ! i < length T`
    have "SA ! (B ! b + i) < length T"
      by simp
    ultimately
    show "x < length T"
      using `(list_slice SA (B ! b) (bucket_end α T b)) ! i = x` by simp
  qed

  from lms_inv_distinct_inv_helper[OF assms(1)]
  have "distinct (filter (λx. x < length T) SA)" "distinct LMS"
       "set (filter (λx. x < length T) SA) ∩ set LMS = {}"
    by blast+

  have "SA = list_slice SA 0 (length SA)"
    by (simp add: list_slice_0_length)
  hence "SA = list_slice SA 0 (B ! b) @ list_slice SA (B ! b) (length SA)"
    using append_take_drop_id 
    by (simp add: list_slice.simps)
  moreover
  from list_slice_append[OF `B ! b ≤ bucket_end α T b` `bucket_end α T b ≤ length SA`, of SA]
  have "list_slice SA (B ! b) (length SA)
          = list_slice SA (B ! b) (bucket_end α T b) @ list_slice SA (bucket_end α T b) (length SA)"
    by assumption
  ultimately
  have "SA = list_slice SA 0 (B ! b) @ list_slice SA (B ! b) (bucket_end α T b) @
             list_slice SA (bucket_end α T b) (length SA)"
    by metis
  with `distinct (filter (λx. x < length T) SA)`
  have "distinct (filter (λx. x < length T) (list_slice SA (B ! b) (bucket_end α T b)))"
    by (metis distinct_append filter_append)
  with `∀x ∈ set (list_slice SA (B ! b) (bucket_end α T b)). x < length T`
  show "distinct (list_slice SA (B ! b) (bucket_end α T b))"
    by simp
qed

lemma lms_slice_subset_lms_bucket:
  assumes "lms_locations_inv α T B SA"
  and     "length SA = length T"
  and     "b ≤ α (Max (set T ))"
shows "set (list_slice SA (B ! b) (bucket_end α T b)) ⊆ lms_bucket α T b"
proof
  fix x
  assume A: "x ∈ set (list_slice SA (B ! b) (bucket_end α T b))"
  from in_set_conv_nth[THEN iffD1, OF A]
  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 "(list_slice SA (B ! b) (bucket_end α T b)) ! i = SA ! (B ! b + i)"
    by blast
  moreover
  from `i < length (list_slice SA (B ! b) (bucket_end α T b))`
  have "B ! b + i < bucket_end α T b"
    by (simp add: assms(2) bucket_end_le_length length_list_slice)
  moreover
  have "B ! b ≤ B ! b + i"
    by simp
  ultimately
  show "x ∈ lms_bucket α T b"
    using ‹list_slice SA (B ! b) (bucket_end α T b) ! i = x› assms(1,3) lms_locations_invD
    by fastforce
qed

lemma lms_val_location:
  assumes "lms_locations_inv α T B SA"
  and     "lms_unchanged_inv α T B SA0 SA"
  and     "strict_mono α"
  and     "length SA = length T"
  and     "∀i < length T. SA0 ! i = length T"
  and     "i < length SA"
  and     "SA ! i < length T"
shows "∃b ≤ α (Max (set T)). B ! b ≤ i ∧ i < bucket_end α T b"
proof -
  from assms
  have "i < length T"
    by simp
  with index_in_bucket_interval_gen[OF _ assms(3)]
  obtain b where
    "b ≤ α (Max (set T))"
    "bucket_start α T b ≤ i"
    "i < bucket_end α T b"
    by blast
  moreover
  have "B ! b ≤ i"
  proof (rule ccontr)
    assume "¬B ! b ≤ i"
    hence "i < B ! b"
      by simp
    with lms_unchanged_invD[OF assms(2) `b ≤ α (Max (set T))` `bucket_start α T b ≤ i`]
    have "SA ! i = SA0 ! i"
      by blast
    with assms(5) `i < length T`
    have "SA ! i = length T"
      by auto
    with assms(7)
    show False
      by auto
  qed
  ultimately
  show ?thesis
    by auto
qed

lemma lms_val_imp_abs_is_lms:
  assumes "lms_locations_inv α T B SA"
  and     "lms_unchanged_inv α T B SA0 SA"
  and     "strict_mono α"
  and     "length SA = length T"
  and     "∀i < length T. SA0 ! i = length T"
  and     "i < length SA"
  and     "SA ! i < length T"
shows "abs_is_lms T (SA ! i)"
proof -
  from lms_val_location[OF assms(1-7)]
  obtain b where
    "b ≤ α (Max (set T))"
    "B ! b ≤ i"
    "i < bucket_end α T b"
    by blast
  with lms_locations_invD[OF assms(1)]
  have "SA ! i ∈ lms_bucket α T b"
    by blast
  then show "abs_is_lms T (SA ! i)"
    using lms_bucket_def by blast
qed

lemma lms_lms_prefix_sorted:
  assumes "lms_bucket_ptr_inv α T B SA"
  and     "lms_locations_inv α T B SA"
  and     "lms_unchanged_inv α T B SA0 SA"
  and     "strict_mono α"
  and     "length SA = length T"
  and     "∀i < length T. SA0 ! i = length T"
  and     "set LMS = {i. abs_is_lms T i}"
shows "ordlistns.sorted (map (lms_prefix T) (filter (λx. x < length T) SA))"
proof (intro sorted_wrt_mapI)
  fix i j
  let ?fs = "filter (λx. x < length T) SA"
  let ?goal = "list_less_eq_ns (lms_prefix T (?fs ! i)) (lms_prefix T (?fs ! j))"
  assume "i < j" "j < length ?fs"

  from filter_nth_relative_2[OF `j < length ?fs` `i < j`]
  obtain i' j' where
    "j' < length SA"
    "i' < j'"
    "?fs ! j = SA ! j'"
    "?fs ! i = SA ! i'"
    by blast
  hence "i' < length SA"
    by linarith

  have "SA ! i' < length T"
    by (metis ‹?fs ! i = SA ! i'› ‹i < j› ‹j < length ?fs› filter_set member_filter
              nth_mem order.strict_trans)
  with lms_val_location[OF assms(2-6) `i' < length SA`]
  obtain b where
    "b ≤ α (Max (set T))"
    "B ! b ≤ i'"
    "i' < bucket_end α T b"
    by blast
  with lms_locations_invD[OF assms(2)]
  have "SA ! i' ∈ lms_bucket α T b"
    by blast
  hence "α (T ! (SA ! i')) = b" "abs_is_lms T (SA ! i')"
    by (simp add: bucket_def lms_bucket_def)+

  from lms_lms_prefix[OF `abs_is_lms T (SA ! i')`] `?fs ! i = SA ! i'`
  have S1: "lms_prefix T (?fs ! i) = [T ! (SA ! i')]"
    by simp

  have "SA ! j' < length T"
    using ‹?fs ! j = SA ! j'› ‹j < length ?fs› nth_mem by fastforce
  with lms_val_location[OF assms(2-6) `j' < length SA`]
  obtain b' where
    "b' ≤ α (Max (set T))"
    "B ! b' ≤ j'"
    "j' < bucket_end α T b'"
    by blast
  with lms_locations_invD[OF assms(2)]
  have "SA ! j' ∈ lms_bucket α T b'"
    by blast
  hence "α (T ! (SA ! j')) = b'" "abs_is_lms T (SA ! j')"
    by (simp add: bucket_def lms_bucket_def)+

  from lms_lms_prefix[OF `abs_is_lms T (SA ! j')`] `?fs ! j = SA ! j'`
  have S2: "lms_prefix T (?fs ! j) = [T ! (SA ! j')]"
    by simp

  have "b ≤ b'"
  proof (rule ccontr)
    assume "¬b ≤ b'"
    hence "b' < b"
      by simp
    hence "bucket_end α T b' ≤ bucket_start α T b"
      by (simp add: less_bucket_end_le_start)
    hence "bucket_end α T b' ≤ lms_bucket_start α T b"
      by (metis l_bucket_end_def l_bucket_end_le_lms_bucket_start le_add1 le_trans)
    with lms_bucket_ptr_lower_bound[OF assms(1) `b ≤ α (Max (set T))`]
    have "bucket_end α T b' ≤ B ! b"
      by linarith
    with `j' < bucket_end α T b'` `B ! b ≤ i'` `i' < j'`
    show False
      by linarith
  qed
  moreover
  have "b < b' ⟹ ?goal"
  proof -
    assume "b < b'"
    with `α (T ! (SA ! i')) = b` `α (T ! (SA ! j')) = b'` assms(4)
    have "T ! (SA ! i') < T ! (SA ! j')"
      using strict_mono_less by blast
    with S1 S2
    show ?goal
      by (simp add: list_less_eq_ns_cons)
  qed
  moreover
  have "b = b' ⟹ ?goal"
  proof -
    assume "b = b'"
    with `α (T ! (SA ! i')) = b` `α (T ! (SA ! j')) = b'` assms(4)
    have "T ! (SA ! i') = T ! (SA ! j')"
      by (meson strict_mono_eq)
    with S1 S2
    show ?goal
      by simp
  qed
  ultimately
  show ?goal
    using less_le by blast
qed

lemma lms_suffix_sorted:
  assumes "lms_bucket_ptr_inv α T B SA"
  and     "lms_locations_inv α T B SA"
  and     "lms_unchanged_inv α T B SA0 SA"
  and     "lms_sorted_inv T LMS SA"
  and     "strict_mono α"
  and     "length SA = length T"
  and     "∀i < length T. SA0 ! i = length T"
  and     "set LMS = {i. abs_is_lms T i}"
  and     "ordlistns.sorted (map (suffix T) (rev LMS))"
shows "ordlistns.sorted (map (suffix T) (filter (λx. x < length T) SA))"
proof (intro sorted_wrt_mapI)
  fix i j
  let ?fs = "filter (λx. x < length T) SA"
  let ?goal = "list_less_eq_ns (suffix T (?fs ! i)) (suffix T (?fs ! j))"
  assume "i < j" "j < length ?fs"

  from filter_nth_relative_2[OF `j < length ?fs` `i < j`]
  obtain i' j' where
    "j' < length SA"
    "i' < j'"
    "?fs ! j = SA ! j'"
    "?fs ! i = SA ! i'"
    by blast
  hence "i' < length SA"
    by linarith

  have "SA ! i' < length T"
    by (metis ‹?fs ! i = SA ! i'› ‹i < j› ‹j < length ?fs› filter_set member_filter
              nth_mem order.strict_trans)
  with lms_val_location[OF assms(2,3,5-7) `i' < length SA`]
  obtain b where
    "b ≤ α (Max (set T))"
    "B ! b ≤ i'"
    "i' < bucket_end α T b"
    by blast
  with lms_locations_invD[OF assms(2)]
  have "SA ! i' ∈ lms_bucket α T b"
    by blast
  hence "α (T ! (SA ! i')) = b" "abs_is_lms T (SA ! i')"
    by (simp add: bucket_def lms_bucket_def)+
  hence "SA ! i' ∈ set LMS"
    using assms(8)
    by blast

  have "SA ! j' < length T"
    using ‹?fs ! j = SA ! j'› ‹j < length ?fs› nth_mem by fastforce
  with lms_val_location[OF assms(2,3,5-7) `j' < length SA`]
  obtain b' where
    "b' ≤ α (Max (set T))"
    "B ! b' ≤ j'"
    "j' < bucket_end α T b'"
    by blast
  with lms_locations_invD[OF assms(2)]
  have "SA ! j' ∈ lms_bucket α T b'"
    by blast
  hence "α (T ! (SA ! j')) = b'" "abs_is_lms T (SA ! j')"
    by (simp add: bucket_def lms_bucket_def)+
  hence "SA ! j' ∈ set LMS"
    using assms(8)
    by blast

  have "b ≤ b'"
  proof (rule ccontr)
    assume "¬b ≤ b'"
    hence "b' < b"
      by simp
    hence "bucket_end α T b' ≤ bucket_start α T b"
      by (simp add: less_bucket_end_le_start)
    hence "bucket_end α T b' ≤ lms_bucket_start α T b"
      by (metis l_bucket_end_def l_bucket_end_le_lms_bucket_start le_add1 le_trans)
    with lms_bucket_ptr_lower_bound[OF assms(1) `b ≤ α (Max (set T))`]
    have "bucket_end α T b' ≤ B ! b"
      by linarith
    with `j' < bucket_end α T b'` `B ! b ≤ i'` `i' < j'`
    show False
      by linarith
  qed
  moreover
  have "b < b' ⟹ ?goal"
  proof -
    assume "b < b'"
    with `α (T ! (SA ! i')) = b` `α (T ! (SA ! j')) = b'` assms(5)
    have "T ! (SA ! i') < T ! (SA ! j')"
      using strict_mono_less by blast
    with `?fs ! i = SA ! i'` `?fs ! j = SA ! j'` `SA ! i' < length T` `SA ! j' < length T`
    show ?goal
      by (metis list_less_ns_cons_diff ordlistns.less_imp_le suffix_cons_ex)
  qed
  moreover
  have "b = b' ⟹ ?goal"
  proof -
    assume "b = b'"
    with `α (T ! (SA ! i')) = b` `α (T ! (SA ! j')) = b'` assms(5)
    have "T ! (SA ! i') = T ! (SA ! j')"
      by (meson strict_mono_eq)
    with lms_sorted_invD2[OF assms(4) `j' < length SA` `i' < j'` `SA ! i' ∈ set LMS`
                             `SA ! j' ∈ set LMS`]
    obtain m n where
      "n < length LMS"
      "m < n"
      "LMS ! m = SA ! j'"
      "LMS ! n = SA ! i'"
      by blast
    hence "rev LMS ! (length LMS - Suc m) = SA ! j'" "rev LMS ! (length LMS - Suc n) = SA ! i'"
      by (metis length_rev order.strict_trans rev_nth rev_rev_ident)+
    moreover
    from  `m < n` `n < length LMS`
    have "length LMS - Suc n ≤ length LMS - Suc m"
      by linarith
    moreover
    have "length LMS - Suc m < length (rev LMS)"
      using ‹n < length LMS› by auto
    ultimately
    have "list_less_eq_ns (suffix T (SA ! i')) (suffix T (SA ! j'))"
      using ordlistns.sorted_nth_mono[OF assms(9)]
      by fastforce
    with `?fs ! i = SA ! i'` `?fs ! j = SA ! j'`
    show ?goal
      by simp
  qed
  ultimately
  show ?goal
    using less_le by blast
qed

lemma next_index_outside:
  assumes "b = α (T ! x)"
  and     "k = B ! b - Suc 0"
  and     "lms_distinct_inv T SA (x # LMS)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "strict_mono α"
  and     "∀a ∈ set (x # LMS). abs_is_lms T a"
  and     "b' ≤ α (Max (set T))"
  and     "b ≠ b'"
shows "k < bucket_start α T b' ∨ bucket_end α T b' ≤ k"
proof -

  from lms_distinct_bucket_ptr_lower_bound[OF assms(1,3-6)]
  have "lms_bucket_start α T b < B ! b" .
  hence "k < B ! b"
    using assms(2) by linarith

  from `lms_bucket_start α T b < B ! b`
  have "lms_bucket_start α T b ≤ k"
    using assms(2) by linarith

  have "x < length T"
    by (simp add: assms(6) abs_is_lms_imp_less_length)
  hence "b ≤ α (Max (set T))"
    by (simp add: assms(1,5) strict_mono_leD)

  from assms(8)
  have "b < b' ∨ b' < b"
    by linarith
  moreover
  have "b < b' ⟹ k < bucket_start α T b'"
  proof -
    assume "b < b'"
    hence "bucket_end α T b ≤ bucket_start α T b'"
      by (simp add: less_bucket_end_le_start)
    with lms_bucket_ptr_upper_bound[OF assms(4) `b ≤ α (Max (set T))`]
    have "B ! b ≤ bucket_start α T b'"
      by linarith
    with `k < B ! b`
    show ?thesis
      by linarith
  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)
    hence "bucket_end α T b' ≤ lms_bucket_start α T b"
      by (metis l_bucket_end_def l_bucket_end_le_lms_bucket_start le_add1 le_trans)
    with `lms_bucket_start α T b ≤ k`
    show ?thesis
      using le_trans by blast
  qed
  ultimately show ?thesis
    by blast
qed

subsection ‹Establishment and Maintenance Steps›

subsubsection ‹Distinctness›

lemma lms_distinct_inv_established:
  assumes "distinct LMS"
  and     "∀i < length SA. SA ! i = length T"
shows "lms_distinct_inv T SA LMS"
proof -
  from assms(2)
  have "filter (λx. x < length T) SA = []"
    by (metis filter_False in_set_conv_nth nat_neq_iff)
  then show ?thesis
  unfolding lms_distinct_inv_def
  using distinct_append assms(1)
  by simp
qed

lemma lms_distinct_inv_maintained_step:
  assumes "lms_distinct_inv T SA (x # LMS)"
shows "lms_distinct_inv T (SA[k := x]) LMS"
  unfolding lms_distinct_inv_def
proof(intro distinct_conv_nth[THEN iffD2] allI impI)
  let ?xs = "filter (λx. x < length T) SA" and
      ?ys = "filter (λx. x < length T) (SA[k := x])"
  fix i j
  assume "i ≠ j" "i < length (filter (λx. x < length T) (SA[k := x]) @ LMS)"
         "j < length (filter (λx. x < length T) (SA[k := x]) @ LMS)"
  hence "i < length ?ys + length LMS"  "j < length ?ys + length LMS"
    by simp_all

  let ?goal = "(?ys @ LMS) ! i ≠ (?ys @ LMS) ! j"

  from assms(1) distinct_append
  have "distinct LMS" "distinct ?xs" "x ∉ set ?xs" "x ∉ set LMS" "set ?xs ∩ set LMS = {}"
    by (simp add: lms_distinct_inv_def)+

  from `distinct LMS` `i < length ?ys + length LMS` `j < length ?ys + length LMS` `i ≠ j`
  have R1: "⟦length ?ys ≤ i; length ?ys ≤ j⟧ ⟹ ?goal"
    by (metis le_Suc_ex nat_add_left_cancel_less nth_append_length_plus nth_eq_iff_index_eq)

  have "set ?ys ⊆ {x} ∪ set ?xs"
    by (meson filter_nth_update_subset)

  have R2:
    "⋀i j. ⟦i < length ?ys; length ?ys ≤ j; j < length ?ys + length LMS⟧ ⟹
            (?ys @ LMS) ! i ≠ (?ys @ LMS) ! j"
  proof -
    fix i j
    assume "i < length ?ys" "length ?ys ≤ j" "j < length ?ys + length LMS"
    hence "?ys ! i ∈ {x} ∪ set ?xs"
      using `set ?ys ⊆ {x} ∪ set ?xs` nth_mem by blast
    hence "(?ys @ LMS) ! i ∈ {x} ∪ set ?xs"
      by (simp add: ‹i < length ?ys› nth_append)
    moreover
    from `length ?ys ≤ j` `j < length ?ys + length LMS`
    have "(?ys @ LMS) ! j ∈ set LMS"
      by (metis add.commute in_set_conv_nth leD less_diff_conv2 nth_append)
    moreover
    from `set ?xs ∩ set LMS = {}` `x ∉ set LMS`
    have "({x} ∪ set ?xs) ∩ set LMS = {}"
      by blast
    ultimately
    show "(?ys @ LMS) ! i ≠ (?ys @ LMS) ! j"
      by (metis disjoint_iff_not_equal)
  qed

  have R3: "⟦i < length ?ys; j < length ?ys⟧ ⟹ ?goal"
  proof -
    assume "i < length ?ys" "j < length ?ys"
    with filter_nth_relative_neq_2[OF _ _ `i ≠ j`]
    obtain i' j' where
      "i' < length (SA[k := x])"
      "j' < length (SA[k := x])"
      "(SA[k := x]) ! i' = ?ys ! i"
      "(SA[k := x]) ! j' = ?ys ! j"
      "i' ≠ j'"
      by blast

    have "?ys ! i < length T"
      using ‹i < length ?ys› nth_mem by fastforce
    hence "(SA[k := x]) ! i' < length T"
      using `(SA[k := x]) ! i' = ?ys ! i` by simp

    have "?ys ! j < length T"
      using ‹j < length ?ys› nth_mem by fastforce
    hence "(SA[k := x]) ! j' < length T"
      using `(SA[k := x]) ! j' = ?ys ! j` by simp

    have R4:
      "⋀i j. ⟦i ≠ k; j = k; i < length (SA[k := x]); j < length (SA[k := x]);
              (SA[k := x]) ! i < length T⟧ ⟹
              (SA[k := x]) ! i ≠ (SA[k := x]) ! j"
    proof -
      fix i j
      assume "i ≠ k" "j = k" "i < length (SA[k := x])" "j < length (SA[k := x])"
             "(SA[k := x]) ! i < length T"

      from `j = k` `j < length (SA[k := x])`
      have "(SA[k := x]) ! j = x"
        by simp
      moreover
      from `i ≠ k` `i < length (SA[k := x])`
      have "(SA[k := x]) ! i = SA ! i"
        by simp
      with `(SA[k := x]) ! i < length T`
      have "SA ! i < length T"
        by simp
      with filter_nth_1[of i SA "λx. x < length T"] `i < length (SA[k := x])`
      obtain i' where
        "i' < length ?xs"
        "?xs ! i' = SA ! i"
        by auto
      with `(SA[k := x]) ! i = SA ! i`
      have "(SA[k := x]) ! i ∈ set ?xs"
        using nth_mem by fastforce
      ultimately
      show "(SA[k := x]) ! i ≠ (SA[k := x]) ! j"
        using `x ∉ set ?xs` by auto
    qed

    have "⟦i' ≠ k; j' ≠ k⟧ ⟹ (SA[k := x]) ! i' ≠ (SA[k := x]) ! j'"
    proof -
      assume "i' ≠ k" "j' ≠ k"
      with `(SA[k := x]) ! i' = ?ys ! i` `(SA[k := x]) ! j' = ?ys ! j`
      have "?ys ! i = SA ! i'" "?ys ! j = SA ! j'"
        by auto
      with `?ys ! i < length T` `?ys ! j < length T` `i' < length (SA[k := x])`
           `j' < length (SA[k := x])`
           filter_nth_relative_neq_1[of i' SA "λx. x < length T" j', OF _ _ _ _ `i' ≠ j'`]
      obtain i'' j'' where
        "i'' < length ?xs"
        "j'' < length ?xs"
        "?xs ! i'' = SA ! i'"
        "?xs ! j'' = SA ! j'"
        "i'' ≠ j''"
        by auto
      with `distinct ?xs`
      have "SA ! i' ≠ SA ! j'"
        by (metis distinct_Ex1 in_set_conv_nth)
      then show ?thesis
        using ‹SA[k := x] ! i' = ?ys ! i› ‹?ys ! i = SA ! i'› ‹j' ≠ k› by auto
    qed
    moreover
    from `i' ≠ j'`
    have "⟦i' = k; j' = k⟧ ⟹ False"
      by blast
    ultimately
    have "(SA[k := x]) ! i' ≠ (SA[k := x]) ! j'"
      using R4[of i' j', OF _ _ `i' < length (SA[k := x])` `j' < length (SA[k := x])`
                `(SA[k := x]) ! i' < length T`]
            R4[of j' i', OF _ _ `j' < length (SA[k := x])` `i' < length (SA[k := x])`
                `(SA[k := x]) ! j' < length T`]
      by metis
    with `(SA[k := x]) ! i' = ?ys ! i` `i < length ?ys`
         `(SA[k := x]) ! j' = ?ys ! j` `j < length ?ys`
    show ?goal
      by (simp add: nth_append)
  qed

  from R1 R2[of i j, OF _ _ `j < length ?ys + length LMS`]
       R2[of j i, OF _ _ `i < length ?ys + length LMS`] R3
  show ?goal
    by presburger
qed

lemma lms_distinct_inv_maintained:
  assumes "lms_distinct_inv T SA LMS"
  shows "lms_distinct_inv T (abs_bucket_insert α T B SA LMS) []"
  using assms
proof (induct rule: abs_bucket_insert.induct[of _ α T B SA LMS])
  case (1 α T uu SA)
  then show ?case
    by simp
next
  case (2 α T B SA x xs)
  note IH = this
  let ?b = "α (T ! x)"
  let ?k = "B ! ?b - Suc 0"
  from IH(1)[OF  _ _ _ _ lms_distinct_inv_maintained_step[OF IH(2), of ?k], of ?b ?k "B[?b := ?k]"]
  show ?case
    by (metis (full_types) One_nat_def abs_bucket_insert.simps(2))
qed

lemma abs_bucket_insert_lms_distinct_inv:
  assumes "distinct LMS"
  and     "∀i < length SA. SA ! i = length T"
shows "lms_distinct_inv T (abs_bucket_insert α T B SA LMS) []"
  using assms lms_distinct_inv_maintained lms_distinct_inv_established
  by blast

subsubsection ‹Bucket Ptr›

lemma lms_bucket_ptr_inv_established:
  assumes "lms_bucket_init α T B"
  and     "∀i < length SA. SA ! i = length T"
shows "lms_bucket_ptr_inv α T B SA"
  unfolding lms_bucket_ptr_inv_def
proof (intro allI impI)
  fix b
  assume "b ≤ α (Max (set T))"
  with lms_bucket_initD[OF assms(1)]
  have "B ! b = bucket_end α T b"
    by simp
  moreover
  from assms(2)
  have "∀i ∈ set SA. ¬abs_is_lms T i"
    by (metis in_set_conv_nth abs_is_lms_imp_less_length less_not_refl2)
  hence "cur_lms_types α T SA b = {}"
    by (simp add: cur_lms_types_def lms_bucket_def)
  hence "num_lms_types α T SA b = 0"
    by (simp add: num_lms_types_def)
  ultimately
  show "B ! b + num_lms_types α T SA b = bucket_end α T b"
    by simp
qed

lemma lms_bucket_ptr_inv_maintained_step:
  assumes "b = α (T ! x)"
  and     "k = B ! b - Suc 0"
  and     "lms_distinct_inv T SA (x # LMS)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "lms_unknowns_inv α T B SA"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA = length T"
  and     "∀a ∈ set (x # LMS). abs_is_lms T a"
shows "lms_bucket_ptr_inv α T (B[b := k]) (SA[k := x])"
  unfolding lms_bucket_ptr_inv_def
proof (intro allI impI)
  fix b'
  assume "b' ≤ α (Max (set T))"

  let ?goal = "B[b := k] ! b' + num_lms_types α T (SA[k := x]) b' = bucket_end α T b'"

  from assms(1,9)
  have "x ∈ lms_bucket α T b"
    by (simp add: bucket_def abs_is_lms_imp_less_length lms_bucket_def)

  from lms_next_insert_at_unknown[OF assms(1-6,8,9)]
  have "k < length SA" "SA ! k = length T"
    by blast+

  have "b' ≠ b ⟹ ?goal"
  proof -
    assume "b' ≠ b"
    with `x ∈ lms_bucket α T b`
    have "x ∉ lms_bucket α T b'"
      by (simp add: bucket_def lms_bucket_def)
    with cur_lms_subset_lms_bucket
    have "x ∉ cur_lms_types α T SA b'"
      by blast

    have "cur_lms_types α T (SA[k := x]) b' = cur_lms_types α T SA b'"
      unfolding cur_lms_types_def
    proof (intro equalityI subsetI)
      fix y
      assume "y ∈ {i |i. i ∈ set (SA[k := x]) ∧ i ∈ lms_bucket α T b'}"
      hence "y ∈ set (SA[k := x])" "y ∈ lms_bucket α T b'"
        by simp_all
      with `x ∉ lms_bucket α T b'`
      have "y ∈ set SA"
        by (metis in_set_conv_nth length_list_update nth_list_update_eq nth_list_update_neq)
      then show "y ∈ {i |i. i ∈ set SA ∧ i ∈ lms_bucket α T b'}"
        by (simp add: ‹y ∈ lms_bucket α T b'›)
    next
      fix y
      assume "y ∈ {i |i. i ∈ set SA ∧ i ∈ lms_bucket α T b'}"
      hence "y ∈ set SA" "y ∈ lms_bucket α T b'"
        by simp_all
      with `x ∉ lms_bucket α T b'` `SA ! k = length T`
      have "y ∈ set (SA[k := x])"
        using in_set_list_update abs_is_lms_imp_less_length lms_bucket_def by fastforce
      then show "y ∈ {i |i. i ∈ set (SA[k := x]) ∧ i ∈ lms_bucket α T b'}"
        using ‹y ∈ lms_bucket α T b'› by blast
    qed
    hence "num_lms_types α T (SA[k := x]) b' = num_lms_types α T SA b'"
      by (simp add: num_lms_types_def)
    with lms_bucket_ptr_invD[OF assms(4) `b' ≤ α (Max (set T))`] `b' ≠ b`
    show ?thesis
      by simp
  qed
  moreover
  have "b' = b ⟹ ?goal"
  proof -
    assume "b' = b"
    with `b' ≤ α (Max (set T))`
    have "b ≤ α (Max (set T))"
      by simp

    from assms(3,9)
    have "x ∉ set SA"
      by (simp add: abs_is_lms_imp_less_length lms_distinct_inv_def)

    from `k < length SA`
    have "x ∈ set (SA[k := x])"
      by (simp add: set_update_memI)

    have "b < length B"
      using ‹b ≤ α (Max (set T))› assms(7) dual_order.strict_trans2 by blast
    hence "B[b := k] ! b = k"
      by simp

    have "finite (cur_lms_types α T SA b)"
      by (meson List.finite_set cur_lms_subset_SA finite_subset)
    moreover
    from `x ∉ set SA`
    have "cur_lms_types α T SA b - {x} = cur_lms_types α T SA b"
      using cur_lms_subset_SA by fastforce
    moreover
    have "insert x (cur_lms_types α T SA b) = cur_lms_types α T (SA[k := x]) b"
      unfolding cur_lms_types_def
    proof (intro equalityI subsetI)
      fix y
      assume "y ∈ insert x {i |i. i ∈ set SA ∧ i ∈ lms_bucket α T b}"
      hence "y = x ∨ y ∈ set SA ∧ y ∈ lms_bucket α T b"
        by blast
      with ‹SA ! k = length T› ‹x ∈ lms_bucket α T b› ‹x ∈ set (SA[k := x])›
      have "y ∈ set (SA[k := x]) ∧ y ∈ lms_bucket α T b"
        by (metis (no_types, lifting) in_set_list_update abs_is_lms_imp_less_length less_irrefl_nat
                                      lms_bucket_def mem_Collect_eq)
      then show "y ∈ {i |i. i ∈ set (SA[k := x]) ∧ i ∈ lms_bucket α T b}"
        by blast
    next
      fix y
      assume "y ∈ {i |i. i ∈ set (SA[k := x]) ∧ i ∈ lms_bucket α T b}"
      hence "y ∈ set (SA[k := x])" "y ∈ lms_bucket α T b"
        by simp_all
      moreover
      have "y ∈ set SA ⟹ y ∈ insert x {i |i. i ∈ set SA ∧ i ∈ lms_bucket α T b}"
        using calculation(2) by blast
      moreover
      from ‹k < length SA ∧ SA ! k = length T›
      have "y ∉ set SA ⟹ y ∈ insert x {i |i. i ∈ set SA ∧ i ∈ lms_bucket α T b}"
        by (metis (no_types, lifting) calculation(1) in_set_conv_nth insert_iff length_list_update
                                      nth_list_update)
      ultimately show "y ∈ insert x {i |i. i ∈ set SA ∧ i ∈ lms_bucket α T b}"
        by blast
    qed
    ultimately
    have "num_lms_types α T (SA[k := x]) b = Suc (num_lms_types α T SA b)"
      by (metis num_lms_types_def card.insert_remove)
    with `b' = b` `B[b := k] ! b = k` assms(2)
    have "B[b := k] ! b' + num_lms_types α T (SA[k := x]) b'
            = B ! b - Suc 0 + Suc (num_lms_types α T SA b)"
      by simp
    hence "B[b := k] ! b' + num_lms_types α T (SA[k := x]) b' = B ! b + num_lms_types α T SA b"
      using add_Suc_shift assms less_nat_zero_code lms_distinct_bucket_ptr_lower_bound
            neq0_conv
      by fastforce
    with `b' = b`
    have "B[b := k] ! b' + num_lms_types α T (SA[k := x]) b' = B ! b' + num_lms_types α T SA b'"
      by simp
    with lms_bucket_ptr_invD[OF assms(4) `b' ≤ α (Max (set T))`]
    show ?thesis
      by simp
  qed
  ultimately
  show ?goal
    by blast
qed

subsubsection ‹Unknowns›

lemma lms_unknowns_inv_established:
  assumes "lms_bucket_init α T B"
  and     "∀i < length SA. SA ! i = length T"
  and     "length SA = length T"
shows "lms_unknowns_inv α T B SA"
  unfolding lms_unknowns_inv_def
proof (intro allI impI; elim conjE)
  fix b i
  assume "b ≤ α (Max (set T))" "lms_bucket_start α T b ≤ i" "i < B ! b"
  with lms_bucket_initD[OF assms(1)]
  have "B ! b = bucket_end α T b"
    by simp
  with `i < B ! b`
  have "i < length T"
    by (simp add: bucket_end_le_length less_le_trans)
  with assms(3)
  have "i < length SA"
    by simp
  with assms(2)
  show "SA ! i = length T"
    by simp
qed

lemma lms_unknowns_inv_maintained_step:
  assumes "b = α (T ! x)"
  and     "k = B ! b - Suc 0"
  and     "lms_distinct_inv T SA (x # LMS)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "lms_unknowns_inv α T B SA"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "∀a ∈ set (x # LMS). abs_is_lms T a"
shows "lms_unknowns_inv α T (B[b := k]) (SA[k := x])"
  unfolding lms_unknowns_inv_def
proof (intro allI impI; elim conjE)
  fix b' i
  assume "b' ≤ α (Max (set T))" "lms_bucket_start α T b' ≤ i" "i < B[b := k] ! b'"

  let ?goal = "SA[k := x] ! i = length T"

  have "b' ≠ b ⟹ ?goal"
  proof -
    assume "b' ≠ b"
    with `i < B[b := k] ! b'`
    have "i < B ! b'"
      by simp
    with lms_unknowns_invD[OF assms(5) `b' ≤ α (Max (set T))` `lms_bucket_start α T b' ≤ i`]
    have "SA ! i = length T"
      by simp

    from `b' ≠ b`
    have "b' < b ∨ b < b'"
      by auto
    then show ?thesis
    proof
      assume "b' < b"
      from lms_distinct_bucket_ptr_lower_bound[OF assms(1,3,4,6,8)]
      have "lms_bucket_start α T b < B ! b" .
      hence "bucket_start α T b < B ! b"
        by (metis dual_order.strict_trans2 l_bucket_end_def l_bucket_end_le_lms_bucket_start le_add1)
      moreover
      from lms_bucket_ptr_upper_bound[OF assms(4) `b' ≤ α (Max (set T))`]
      have "B ! b' ≤ bucket_end α T b'" .
      ultimately
      have "B ! b' < B ! b"
        by (meson ‹b' < b› dual_order.strict_trans2 less_bucket_end_le_start)
      hence "i ≠ k"
        using assms(2,3) `i < B ! b'`
        by linarith
      with `SA ! i = length T`
      show ?thesis
        by auto
    next
      assume "b < b'"
      from `lms_bucket_start α T b' ≤ i`
      have "bucket_start α T b' ≤ i"
        by (metis l_bucket_end_def l_bucket_end_le_lms_bucket_start le_add1 le_trans)
      moreover
      from lms_bucket_ptr_upper_bound[OF assms(4), of b] assms(7)
      have "B ! b ≤ bucket_end α T b"
        using ‹b < b'› ‹b' ≤ α (Max (set T))› by linarith
      hence "k < bucket_end α T b"
        using assms lms_distinct_bucket_ptr_lower_bound by fastforce
      ultimately
      have "i ≠ k"
        by (meson ‹b < b'› leD le_trans less_bucket_end_le_start)
      with `SA ! i = length T`
      show ?thesis
        by auto
    qed
  qed
  moreover
  have "b' = b ⟹ ?goal"
  proof -
    assume "b' = b"
    with `b' ≤ α (Max (set T))` `lms_bucket_start α T b' ≤ i` `i < B[b := k] ! b'`
    have "b ≤ α (Max (set T))" "lms_bucket_start α T b ≤ i" "i < B[b := k] ! b"
      by simp_all
    hence "i < B ! b - Suc 0"
      using assms by auto
    with lms_unknowns_invD[OF assms(5) `b ≤ α (Max (set T))` `lms_bucket_start α T b ≤ i`]
    have "SA ! i = length T"
      by linarith
    with `i < B ! b - Suc 0` assms(2)
    show ?thesis
      by simp
  qed
  ultimately
  show ?goal
    by blast
qed

subsubsection ‹Locations›

lemma lms_locations_inv_established:
  assumes "lms_bucket_init α T B"
shows "lms_locations_inv α T B SA"
  unfolding lms_locations_inv_def
proof (intro allI impI; elim conjE)
  fix b i
  assume "b ≤ α (Max (set T))" "B ! b ≤ i" "i < bucket_end α T b"
  with lms_bucket_initD[OF assms(1), of b]
  have False
    by linarith
  then show "SA ! i ∈ lms_bucket α T b"
    by blast
qed

lemma lms_locations_inv_maintained_step:
  assumes "b = α (T ! x)"
  and     "k = (B ! b) - Suc 0"
  and     "lms_distinct_inv T SA (x # LMS)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "lms_locations_inv α T B SA"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA = length T"
  and     "∀a ∈ set (x # LMS). abs_is_lms T a"
shows "lms_locations_inv α T (B[b := k]) (SA[k := x])"
  unfolding lms_locations_inv_def
proof (intro allI impI; elim conjE)
  fix b' i
  assume "b' ≤ α (Max (set T))" "B[b := k] ! b' ≤ i" "i < bucket_end α T b'"

  let ?goal = "SA[k := x] ! i ∈ lms_bucket α T b'"

  have "lms_bucket_start α T b < B ! b"
    using assms lms_distinct_bucket_ptr_lower_bound by blast

  have "b' ≠ b ⟹ ?goal"
  proof -
    assume "b' ≠ b"
    with `B[b := k] ! b' ≤ i`
    have "B ! b' ≤ i"
      by simp

    from `b' ≠ b`
    have "b' < b ∨ b < b'"
      by auto
    then show ?thesis
    proof
      assume "b' < b"
      from `lms_bucket_start α T b < B ! b`
      have "bucket_start α T b < B ! b"
        by (metis dual_order.strict_trans2 l_bucket_end_def l_bucket_end_le_lms_bucket_start
                  le_add1)
      with `i < bucket_end α T b'` `b' < b`
      have "i ≠ k"
        using assms(2,3)
        by (metis Suc_lessI Suc_pred dual_order.strict_trans1 less_bucket_end_le_start
                  less_nat_zero_code not_less_iff_gr_or_eq)
      hence "SA[k := x] ! i = SA ! i"
        by auto
      with lms_locations_invD[OF assms(5) `b' ≤ α (Max (set T))` `B ! b' ≤ i`
                                 `i < bucket_end α T b'`]
      show ?thesis
        by simp
    next
      assume "b < b'"
      from lms_bucket_ptr_lower_bound[OF assms(4) `b' ≤ α (Max (set T))`]
      have "lms_bucket_start α T b' ≤ B ! b'" .
      hence "bucket_start α T b' ≤ B ! b'"
        by (metis l_bucket_end_def l_bucket_end_le_lms_bucket_start le_add1 le_trans)
      hence "bucket_start α T b' ≤ i"
        using `B ! b' ≤ i` le_trans by blast
      moreover
      from lms_bucket_ptr_upper_bound[OF assms(4), of b] assms(7)
      have "B ! b ≤ bucket_end α T b"
        using ‹b < b'› ‹b' ≤ α (Max (set T))› by linarith
      with `lms_bucket_start α T b < B ! b`
      have "k < bucket_end α T b"
        using assms(2) by linarith
      ultimately
      have "i ≠ k"
        by (meson ‹b < b'› leD le_less_trans less_bucket_end_le_start)
      hence "SA[k := x] ! i = SA ! i"
        by simp
      with lms_locations_invD[OF assms(5)`b' ≤ α (Max (set T))` `B ! b' ≤ i`
                                 `i < bucket_end α T b'`]
      show ?thesis
        by simp
    qed
  qed
  moreover
  have "b' = b ⟹ ?goal"
  proof -
    assume "b' = b"
    with `b' ≤ α (Max (set T))` `B[b := k] ! b' ≤ i` `i < bucket_end α T b'`
    have "b ≤ α (Max (set T))" "B[b := k] ! b ≤ i" "i < bucket_end α T b"
      by simp_all
    hence "k ≤ i"
      by (simp add: assms(7) order.strict_trans1)
    hence "k = i ∨ B ! b ≤ i"
      using assms(2) by linarith
    then show ?thesis
    proof
      assume "k = i"
      hence "SA[k := x] ! i = x"
        using ‹i < bucket_end α T b› assms(8) bucket_end_le_length order.strict_trans2 by fastforce
      moreover
      from assms(1,9)
      have "x ∈ lms_bucket α T b"
        by (simp add: bucket_def abs_is_lms_imp_less_length lms_bucket_def)
      ultimately
      show ?thesis
        using `b' = b` by simp
    next
      assume "B ! b ≤ i"
      with lms_locations_invD[OF assms(5) `b ≤ α (Max (set T))` _ `i < bucket_end α T b`]
      have "SA ! i ∈ lms_bucket α T b"
        by blast
      moreover
      from `B ! b ≤ i` assms(2) `lms_bucket_start α T b < B ! b`
      have "SA[k := x] ! i = SA ! i"
        by auto
      ultimately
      show ?thesis
        using `b' = b` by simp
    qed
  qed
  ultimately
  show ?goal
    by blast
qed
subsubsection ‹Unchanged›

lemma lms_unchanged_inv_established:
  "lms_unchanged_inv α T B SA SA"
  unfolding lms_unchanged_inv_def
  by blast

lemma lms_unchanged_inv_maintained_step:
  assumes "b = α (T ! x)"
  and     "k = (B ! b) - Suc 0"
  and     "lms_distinct_inv T SA (x # LMS)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "lms_unchanged_inv α T B SA0 SA"
  and     "strict_mono α"
  and     "α (Max (set T)) < length B"
  and     "length SA = length T"
  and     "∀a ∈ set (x # LMS). abs_is_lms T a"
shows "lms_unchanged_inv α T (B[b := k]) SA0 (SA[k := x])"
  unfolding lms_unchanged_inv_def
proof (intro allI impI; elim conjE)
  fix b' i
  assume "b' ≤ α (Max (set T))" "bucket_start α T b' ≤ i" "i < B[b := k] ! b'"

  let ?goal = "SA[k := x] ! i = SA0 ! i"

  have "lms_bucket_start α T b < B ! b"
    using assms lms_distinct_bucket_ptr_lower_bound by blast

  have "b' ≠ b ⟹ ?goal"
  proof -
    assume "b' ≠ b"
    with `i < B[b := k] ! b'`
    have "i < B ! b'"
      by simp

    from `b' ≠ b`
    have "b' < b ∨ b < b'"
      by linarith
    then show ?thesis
    proof
      assume "b' < b"
      from `lms_bucket_start α T b < B ! b`
      have "bucket_start α T b < B ! b"
        by (simp add: lms_bucket_start_def)
      with assms(2)
      have "bucket_start α T b ≤ k"
        by linarith
      moreover
      from lms_bucket_ptr_upper_bound[OF assms(4) `b' ≤ α (Max (set T))`]
      have "B ! b' ≤ bucket_end α T b'" .
      with `i < B ! b'`
      have "i < bucket_end α T b'"
        using less_le_trans by blast
      ultimately
      have "i ≠ k"
        using `b' < b`
        by (meson dual_order.strict_trans2 less_bucket_end_le_start order.strict_implies_not_eq)
      hence "SA[k := x] ! i = SA ! i"
        by simp
      with lms_unchanged_invD[OF assms(5) `b' ≤ α (Max (set T))` `bucket_start α T b' ≤ i`
                                 `i < B ! b'`]
      show ?thesis
        by simp
    next
      assume "b < b'"
      from `lms_bucket_start α T b < B ! b` assms(2)
      have "k < B ! b"
        by linarith
      with lms_bucket_ptr_upper_bound[OF assms(4), of b] `b' ≤ α (Max (set T))` `b < b'` assms(7)
      have "k < bucket_end α T b"
        by linarith
      with `bucket_start α T b' ≤ i` `b < b'`
      have "i ≠ k"
        by (meson dual_order.strict_trans1 leD less_bucket_end_le_start)
      hence "SA[k := x] ! i = SA ! i"
        by simp
      with lms_unchanged_invD[OF assms(5) `b' ≤ α (Max (set T))` `bucket_start α T b' ≤ i`
                                 `i < B ! b'`]
      show ?thesis
        by simp
    qed
  qed
  moreover
  have "b' = b ⟹ ?goal"
  proof -
    assume "b' = b"
    with `b' ≤ α (Max (set T))` `bucket_start α T b' ≤ i` `i < B[b := k] ! b'`
    have "b ≤ α (Max (set T))" "bucket_start α T b ≤ i" "i < B[b := k] ! b"
      by simp_all
    hence "i < k"
      using assms(7) by auto
    hence "i < B ! b"
      using assms(2) by linarith
    with lms_unchanged_invD[OF assms(5) `b ≤ α (Max (set T))` `bucket_start α T b ≤ i`]
    have "SA ! i = SA0 ! i"
      by simp
    with `i < k`
    show ?thesis
      by auto
  qed
  ultimately
  show ?goal
    by blast
qed


subsubsection ‹Inserted›

lemma lms_inserted_inv_established:
  shows "lms_inserted_inv LMS SA [] LMS"
  unfolding lms_inserted_inv_def
  by simp

lemma lms_inserted_inv_maintained_step:
  assumes "b = α (T ! x)"
  and     "k = (B ! b) - Suc 0"
  and     "lms_distinct_inv T SA (x # LMSb)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "lms_unknowns_inv α T B SA"
  and     "lms_inserted_inv LMS SA LMSa (x # LMSb)"
  and     "strict_mono α"
  and     "length SA = length T"
  and     "∀a ∈ set LMS. abs_is_lms T a"
shows "lms_inserted_inv LMS (SA[k := x]) (LMSa @ [x]) LMSb"
proof -

  from lms_inserted_invD(1)[OF assms(6)] assms(9)
  have "∀a ∈ set (x # LMSb). abs_is_lms T a"
    by auto
  with lms_next_insert_at_unknown[OF assms(1-5,7,8)]
  have "k < length SA" "SA ! k = length T"
    by blast+

  from lms_inserted_invD(1)[OF assms(6)] assms(9)
  have "∀a ∈ set LMSa. abs_is_lms T a"
    by auto
  hence "∀a ∈ set LMSa. a < length T"
    using abs_is_lms_imp_less_length by blast

  have "set LMSa ⊆ set (SA[k := x])"
  proof (intro subsetI)
    fix y
    assume "y ∈ set LMSa"
    with `∀a ∈ set LMSa. a < length T`
    have "y < length T"
      by blast
    with `SA ! k = length T`
    have "SA ! k ≠ y"
      by simp
    moreover
    from lms_inserted_invD(2)[OF assms(6)] `y ∈ set LMSa`
    have "y ∈ set SA"
      by blast
    ultimately
    show "y ∈ set (SA[k := x])"
      using in_set_list_update by fast
  qed
  moreover
  from `k < length SA`
  have "x ∈ set (SA[k := x])"
    by (simp add: set_update_memI)
  ultimately
  have "set (LMSa @ [x]) ⊆ set (SA[k := x])"
    by simp
  with lms_inserted_invD(1)[OF assms(6)]
  show ?thesis
    by (simp add: lms_inserted_inv_def)
qed

subsubsection ‹Sorted›

lemma lms_sorted_inv_established:
  assumes "∀i < length SA. SA ! i = length T"
  and     "∀a ∈ set LMS. abs_is_lms T a"
shows "lms_sorted_inv T LMS SA"
  unfolding lms_sorted_inv_def
proof (intro allI impI; elim conjE)
  fix i j
  assume A: "j < length SA" "i < j"  "SA ! i ∈ set LMS" "SA ! j ∈ set LMS"
  from A(1) assms(1)
  have "SA ! j = length T"
    by blast
  moreover
  from A(4) assms(2)
  have "SA ! j < length T"
    using abs_is_lms_imp_less_length by blast
  ultimately
  have False
    by auto
  then show
    "(T ! (SA ! i) ≠ T ! (SA ! j) ⟶ T ! (SA ! i) < T ! (SA ! j)) ∧
     (T ! (SA ! i) = T ! (SA ! j) ⟶
      (∃j'<length LMS. ∃i'<j'. LMS ! i' = SA ! j ∧ LMS ! j' = SA ! i))"
    by blast
qed

lemma lms_sorted_inv_maintained_step:
  assumes "b = α (T ! x)"
  and     "k = (B ! b) - Suc 0"
  and     "lms_distinct_inv T SA (x # LMSb)"
  and     "lms_bucket_ptr_inv α T B SA"
  and     "lms_unknowns_inv α T B SA"
  and     "lms_locations_inv α T B SA"
  and     "lms_unchanged_inv α T B SA0 SA"
  and     "lms_inserted_inv LMS SA LMSa (x # LMSb)"
  and     "lms_sorted_inv T LMS SA"
  and     "strict_mono α"
  and     "length SA = length T"
  and     "∀i < length T. SA0 ! i = length T"
  and     "∀a ∈ set LMS. abs_is_lms T a"
shows "lms_sorted_inv T LMS (SA[k := x])"
  unfolding lms_sorted_inv_def
proof (intro allI impI; elim conjE)
  fix i j
  assume A: "j < length (SA[k := x])" "i < j" "SA[k := x] ! i ∈ set LMS"
            "SA[k := x] ! j ∈ set LMS"
  let ?goal1 = "T ! (SA[k := x] ! i) ≠ T ! (SA[k := x] ! j) ⟶
                  T ! (SA[k := x] ! i) < T ! (SA[k := x] ! j)"
  and ?goal2 = "T ! (SA[k := x] ! i) = T ! (SA[k := x] ! j) ⟶
                  (∃j'<length LMS. ∃i'<j'.
                    LMS ! i' = SA[k := x] ! j ∧ LMS! j' = SA[k := x] ! i)"

  let ?goal = "?goal1 ∧ ?goal2"

  from assms(13) lms_inserted_invD[OF assms(8)]
  have "∀a∈set (x # LMSb). abs_is_lms T a"
    by auto
  with lms_next_insert_at_unknown[OF assms(1-5,10,11)]
  have "k < length SA" "SA ! k = length T"
    by blast+

  from lms_distinct_bucket_ptr_lower_bound[OF assms(1,3,4,10) `∀a∈set (x # LMSb). abs_is_lms T a`]
  have "lms_bucket_start α T b < B ! b" .

  from assms(1,10) `∀a∈set (x # LMSb). abs_is_lms T a`
  have "b ≤ α (Max (set T))"
    by (simp add: abs_is_lms_imp_less_length strict_mono_less_eq)

  have "⟦k ≠ i; k ≠ j⟧ ⟹ ?goal"
  proof -
    assume "k ≠ i" "k ≠ j"
    with A
    have "j < length SA" "SA ! i ∈ set LMS" "SA ! j ∈ set LMS"
      by simp_all
    with lms_sorted_invD[OF assms(9) _ `i < j`] `k ≠ i` `k ≠ j`
    show ?goal
      by simp
  qed
  moreover
  have "⟦k = i; k ≠ j⟧ ⟹ ?goal"
  proof -
    assume "k = i" "k ≠ j"
    with A(1,4)
    have "j < length SA" "SA ! j ∈ set LMS" "SA[k := x] ! j = SA ! j"
      by simp_all

    from `k = i` assms(2)
    have "i = B ! b - Suc 0"
      by simp

    from `SA ! j ∈ set LMS` assms(13)
    have "SA ! j < length T"
      using abs_is_lms_imp_less_length by blast

    from index_in_bucket_interval_gen[of j T, OF _ assms(10)] assms(11) `j < length SA`
    obtain b' where
      "b' ≤ α (Max (set T))"
      "bucket_start α T b' ≤ j"
      "j < bucket_end α T b'"
      by auto

    have "B ! b' ≤ j"
    proof (rule ccontr)
      assume "¬ B ! b' ≤ j"
      hence "j < B ! b'"
        by simp
      with lms_unchanged_invD[OF assms(7) `b' ≤ α (Max (set T))` `bucket_start α T b' ≤ j`]
           assms(11,12) `j < length SA`
      have "SA ! j = length T"
        by auto
      with `SA ! j < length T`
      show False
        by auto
    qed
    with lms_locations_invD[OF assms(6) `b' ≤ α (Max (set T))` _ `j < bucket_end α T b'`]
    have "SA ! j ∈ lms_bucket α T b'"
      by blast
    hence "α (T ! (SA ! j)) = b'"
      by (simp add: bucket_def lms_bucket_def)

    from `lms_bucket_start α T b < B ! b` `i = B ! b - Suc 0`
    have "lms_bucket_start α T b ≤ i"
      by linarith
    hence "bucket_start α T b ≤ i"
      by (metis l_bucket_end_def l_bucket_end_le_lms_bucket_start le_add1 le_trans)

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

    from assms(3)[simplified lms_distinct_inv_def distinct_append] `SA ! j < length T`
         `j < length SA`
    have "SA ! j ∉ set (x # LMSb)"
      by (metis IntI empty_iff filter_set member_filter nth_mem)
    with lms_inserted_invD[OF assms(8)] `SA ! j ∈ set LMS`
    have "SA ! j ∈ set LMSa"
      by auto
    hence "∃j' < length LMSa. LMSa ! j' = SA ! j"
      by (simp add: in_set_conv_nth)
    then obtain j' where
      "j' < length LMSa"
      "LMSa ! j' = SA ! j"
      by blast
    with lms_inserted_invD(1)[OF assms(8)] `SA[k := x] ! j = SA ! j`
    have "LMS ! j' = SA[k := x] ! j"
      by (simp add: nth_append)

    from `α (T ! (SA ! j)) = b'` `SA[k := x] ! j = SA ! j`
    have "α (T ! (SA[k := x] ! j)) = b'"
      by simp

    from lms_inserted_invD(1)[OF assms(8)]
    have "length LMSa < length LMS"
      by simp

    from assms(3)[simplified lms_distinct_inv_def distinct_append] lms_inserted_invD[OF assms(8)]
    have "x ∉ set LMSa"
      using ‹∀a∈set (x # LMSb). abs_is_lms T a› abs_is_lms_imp_less_length by fastforce
    with lms_inserted_invD(1)[OF assms(8)]
    have "LMS ! length LMSa = x"
      by simp
    hence "LMS ! length LMSa = SA[k := x] ! i"
      using ‹k < length SA› ‹k = i› by auto

    from `k = i` assms(1) `k < length SA`
    have "α (T ! (SA[k := x] ! i)) = b"
      by auto

    have "b = b' ⟹ ?goal2"
    proof
      from `LMS ! j' = SA[k := x] ! j` `LMS ! length LMSa = SA[k := x] ! i` `j' < length LMSa`
           `length LMSa < length LMS`
      show "∃j'<length LMS. ∃i'<j'. LMS ! i' = SA[k := x] ! j ∧ LMS ! j' = SA[k := x] ! i"
        by blast
    qed
    moreover
    from `α (T ! (SA[k := x] ! j)) = b'` `α (T ! (SA[k := x] ! i)) = b` assms(10)
    have "b = b' ⟹ T ! (SA[k := x] ! i) = T ! (SA[k := x] ! j)"
      using strict_mono_eq by auto
    moreover
    have "b < b' ⟹ ?goal1"
    proof
      assume "b < b'"
      with `α (T ! (SA[k := x] ! i)) = b` `α (T ! (SA[k := x] ! j)) = b'` assms(10)
      show "T ! (SA[k := x] ! i) < T ! (SA[k := x] ! j)"
        using strict_mono_less by blast
    qed
    moreover
    from `α (T ! (SA[k := x] ! j)) = b'` `α (T ! (SA[k := x] ! i)) = b` assms(10)
    have "b < b' ⟹ T ! (SA[k := x] ! i) ≠ T ! (SA[k := x] ! j)"
      by auto
    moreover
    from `b ≤ b'`
    have "b = b' ∨ b < b'"
      by linarith
    ultimately
    show ?goal
      by blast
  qed
  moreover
  have "⟦k ≠ i; k = j⟧ ⟹ ?goal"
  proof -
    assume "k ≠ i" "k = j"
    with `SA[k := x] ! i ∈ set LMS`
    have "SA[k := x] ! i = SA ! i" "SA ! i ∈ set LMS"
      by simp_all

    from `k = j` assms(2)
    have "j = B ! b - Suc 0"
      by simp

    from `j < length (SA[k := x])` `i < j` assms(11)
    have "i < length T"
      by simp
    with index_in_bucket_interval_gen[of i T, OF _ assms(10)]
    obtain b' where
      "b' ≤ α (Max (set T))"
      "bucket_start α T b' ≤ i"
      "i < bucket_end α T b'"
      by auto

    from `SA ! i ∈ set LMS` assms(13)
    have "SA ! i < length T"
      using abs_is_lms_imp_less_length by blast

    have "B ! b' ≤ i"
    proof (rule ccontr)
      assume "¬B ! b' ≤ i"
      hence "i < B ! b'"
        by (simp add: not_le)
      with lms_unchanged_invD[OF assms(7) `b' ≤ α (Max (set T))` `bucket_start α T b' ≤ i`]
           assms(12) `i < length T`
      have "SA ! i = length T"
        by simp
      with `SA ! i < length T`
      show False
        by linarith
    qed
    with lms_locations_invD[OF assms(6) `b' ≤ α (Max (set T))` _ `i < bucket_end α T b'`]
    have "SA ! i ∈ lms_bucket α T b'"
      by blast
    hence "α (T ! (SA ! i)) = b'"
      by (simp add: bucket_def lms_bucket_def)
    with `SA[k := x] ! i = SA ! i`
    have "α (T ! (SA[k := x] ! i)) = b'"
      by simp

    from `i < j` `j = B ! b - Suc 0` `lms_bucket_start α T b < B ! b`
    have "i < B ! b"
      using diff_le_self dual_order.strict_trans1 by blast

    have "i < bucket_start α T b"
    proof (rule ccontr)
      assume "¬i < bucket_start α T b"
      hence "bucket_start α T b ≤ i"
        by (simp add: not_le)
      with lms_unchanged_invD[OF assms(7) `b ≤ α (Max (set T))` _ `i < B ! b`]
           assms(12) `i < length T`
      have "SA ! i = length T"
        by auto
      with `SA ! i < length T`
      show False
        by linarith
    qed
    with `bucket_start α T b' ≤ i`
    have "bucket_start α T b' < bucket_start α T b"
      by linarith
    hence "b' < b"
      by (meson bucket_start_le leD leI)

    from assms(1) `k = j` `k < length SA`
    have "α (T ! (SA[k := x] ! j)) = b"
      by simp
    with `α (T ! (SA[k := x] ! i)) = b'` `b' < b` assms(10)
    have "T ! (SA[k := x] ! i) < T ! (SA[k := x] ! j)"
      using strict_mono_less by blast
    then show ?goal
      by auto
  qed
  moreover
  from `i < j`
  have "⟦k = i; k = j⟧ ⟹ ?goal"
    by blast
  ultimately
  show ?goal
    by blast
qed

subsection ‹Combined Establishment and Maintenance›

lemma lms_inv_established:
  assumes "∀i < length SA. SA ! i = length T"
  and     "∀x ∈ set LMS. abs_is_lms T x"
  and     "distinct LMS"
  and     "lms_bucket_init α T B"
  and     "length SA = length T"
  and     "strict_mono α"
shows "lms_inv α T B LMS [] LMS SA SA"
  unfolding lms_inv_def
  using lms_distinct_inv_established[OF assms(3,1)]
        lms_bucket_ptr_inv_established[OF assms(4,1)]
        lms_unknowns_inv_established[OF assms(4,1,5)]
        lms_locations_inv_established[OF assms(4)]
        lms_unchanged_inv_established
        lms_inserted_inv_established
        lms_sorted_inv_established[OF assms(1,2)]
        lms_bucket_init_length[OF assms(4)]
        assms
  by auto

lemma lms_inv_maintained_step:
  assumes "lms_inv α T B LMS LMSa (x # LMSb) SA0 SA"
  and     "b = α (T ! x)"
  and     "k = (B ! b) - Suc 0"
shows "lms_inv α T (B[b := k]) LMS (LMSa @ [x]) LMSb SA0 (SA[k := x])"
  unfolding lms_inv_def
  using lms_distinct_inv_maintained_step[OF lms_invD(1)[OF assms(1)]]
        lms_bucket_ptr_inv_maintained_step[OF assms(2-3)
                                              lms_invD(1-3,8,9,12)[OF assms(1)]
                                              lms_inv_lms_helper(3)[OF assms(1)]]
        lms_unknowns_inv_maintained_step[OF assms(2-3)
                                            lms_invD(1-3,8,9)[OF assms(1)]
                                            lms_inv_lms_helper(3)[OF assms(1)]]
        lms_locations_inv_maintained_step[OF assms(2-3)
                                             lms_invD(1-2,4,8,9,12)[OF assms(1)]
                                             lms_inv_lms_helper(3)[OF assms(1)]]
        lms_unchanged_inv_maintained_step[OF assms(2-3)
                                             lms_invD(1-2,5,8,9,12)[OF assms(1)]
                                             lms_inv_lms_helper(3)[OF assms(1)]]
        lms_inserted_inv_maintained_step[OF assms(2-3)
                                           lms_invD(1-3,6,8,12)[OF assms(1)]
                                           lms_inv_lms_helper(1)[OF assms(1)]]
        lms_sorted_inv_maintained_step[OF assms(2-3)
                                         lms_invD(1-8,12,13)[OF assms(1)]
                                         lms_inv_lms_helper(1)[OF assms(1)]]
  by (metis assms(1) length_list_update lms_inv_def)

lemma lms_inv_maintained:
  assumes " bucket_insert_abs' α T B SA gs xs = (SA', B', gs')"
  and     "lms_inv α T B LMS gs xs SA0 SA"
shows "lms_inv α T B' LMS gs' [] SA0 SA'"
  using assms
proof (induct arbitrary: SA' B' gs' LMS SA0
              rule: bucket_insert_abs'.induct[of _ α T B SA gs xs])
  case (1 α T B SA gs)
  note BC = this
  from BC(1)[simplified]
  have "B' = B" "SA' = SA" "gs' = gs"
    by auto
  with BC(2)
  show ?case
    by simp
next
  case (2 α T B SA gs x xs)
  note IH = this
  let ?b = "α (T ! x)"
  let ?k = "B ! ?b - Suc 0"
  from lms_inv_maintained_step[OF IH(3), of ?b ?k]
  have R1: "lms_inv α T (B[?b := ?k]) LMS (gs @ [x]) xs SA0 (SA[?k := x])"
    by simp

  from IH(2)[simplified, simplified Let_def]
  have R2: " bucket_insert_abs' α T (B[?b := ?k]) (SA[?k := x]) (gs @ [x]) xs = (SA', B', gs')" .

  from IH(1)[of ?b ?k "SA[?k := x]" "B[?b := ?k]" "gs @ [x]" SA' B' gs' LMS SA0,
             simplified,
             OF R2 R1]
  show ?case .
qed

lemma lms_inv_holds:
  assumes "∀i < length SA. SA ! i = length T"
  and     "∀x ∈ set LMS. abs_is_lms T x"
  and     "distinct LMS"
  and     "lms_bucket_init α T B"
  and     "length SA = length T"
  and     "strict_mono α"
  and     "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs')"
shows "lms_inv α T B' LMS gs' [] SA SA'"
  using lms_inv_maintained[OF assms(7) lms_inv_established[OF assms(1-6)]] .

section ‹Exhaustiveness›

definition lms_type_exhaustive :: "('a :: {linorder, order_bot}) list ⇒ nat list ⇒ bool"
where
"lms_type_exhaustive T SA = (∀i < length T. abs_is_lms T i ⟶ i ∈ set SA)"

lemma lms_type_exhaustiveD:
  "⟦lms_type_exhaustive T SA; i < length T; abs_is_lms T i⟧ ⟹ i ∈ set SA"
  using lms_type_exhaustive_def by blast

lemma lms_all_inserted_imp_exhaustive:
  assumes "lms_inserted_inv LMS SA LMS []"
  and     "set LMS = {i. abs_is_lms T i}"
shows "lms_type_exhaustive T SA"
  unfolding lms_type_exhaustive_def
proof (intro allI impI)
  fix i
  assume "i < length T" "abs_is_lms T i"
  with assms(2)
  have "i ∈ set LMS"
    by blast
  with lms_inserted_invD(2)[OF assms(1)]
  show "i ∈ set SA"
    by blast
qed

lemma lms_type_exhaustive_imp_lms_bucket_subset:
  assumes "lms_type_exhaustive T SA"
  and     "b ≤ α (Max (set T))"
shows "lms_bucket α T b ⊆ set SA"
proof (intro subsetI)
  fix x
  assume "x ∈ lms_bucket α T b"
  hence "x < length T"
    by (simp add: abs_is_lms_imp_less_length lms_bucket_def)

  from `x ∈ lms_bucket α T b`
  have "abs_is_lms T x"
    by (simp add: lms_bucket_def)

  from lms_type_exhaustiveD[OF assms(1) `x < length T` `abs_is_lms T x`]
  show "x ∈ set SA" .
qed


lemma lms_B_val:
  assumes "∀i < length SA. SA ! i = length T"
  and     "distinct LMS"
  and     "lms_bucket_init α T B"
  and     "length SA = length T"
  and     "strict_mono α"
  and     "set LMS = {i. abs_is_lms T i}"
  and     "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs')"
  and     "b ≤ α (Max (set T))"
shows "B' ! b = lms_bucket_start α T b"
proof -
  from assms(6)
  have "∀x ∈ set LMS. abs_is_lms T x"
    by blast
  with lms_inv_holds[OF assms(1) _ assms(2-5,7)]
  have "lms_inv α T B' LMS gs' [] SA SA'" .
  hence "lms_inserted_inv LMS SA' gs' []"
    using lms_inv_def by blast
  hence "gs' = LMS"
    by (simp add: lms_inserted_inv_def)
  with `lms_inserted_inv LMS SA' gs' []` lms_all_inserted_imp_exhaustive[OF _ assms(6), of SA']
  have "lms_type_exhaustive T SA'"
    by simp
  with lms_type_exhaustive_imp_lms_bucket_subset assms(8)
  have "lms_bucket α T b ⊆ set SA'"
    by blast
  with cur_lms_subset_lms_bucket
  have "cur_lms_types α T SA' b = lms_bucket α T b"
    by (simp add: cur_lms_types_def equalityI subset_eq)
  hence "num_lms_types α T SA' b = card (lms_bucket α T b)"
    by (simp add: num_lms_types_def)
  moreover
  from `lms_inv α T B' LMS gs' [] SA SA'`
  have "lms_bucket_ptr_inv α T B' SA'"
    using lms_inv_def by blast
  with lms_bucket_ptr_invD assms(8)
  have "B' ! b + num_lms_types α T SA' b = bucket_end α T b"
    by blast
  ultimately
  have "B' ! b + card (lms_bucket α T b) = bucket_end α T b"
    by simp
  then show "B' ! b = lms_bucket_start α T b"
    by (metis add_implies_diff lms_bucket_pl_size_eq_end lms_bucket_size_def)
qed

section ‹Postconditions›

definition lms_vals_post ::  "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list  ⇒ bool"
where
"lms_vals_post α T SA =
  (∀b ≤ α (Max (set T)).
    lms_bucket α T b = set (list_slice SA (lms_bucket_start α T b) (bucket_end α T b))
  )"

lemma lms_vals_postD:
  "⟦lms_vals_post α T SA; b ≤ α (Max (set T))⟧ ⟹
   lms_bucket α T b = set (list_slice SA (lms_bucket_start α T b) (bucket_end α T b))"
  using lms_vals_post_def by blast

definition 
  lms_pre :: "('a :: {linorder, order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ nat list ⇒ bool"
where
  "lms_pre α T B SA LMS ≡
    (∀i < length SA. SA ! i = length T) ∧
    length SA = length T ∧
    lms_bucket_init α T B ∧
    strict_mono α ∧
    distinct LMS ∧
    set LMS = {i. abs_is_lms T i}"

lemma lms_pre_elims:
  "lms_pre α T B SA LMS ⟹ ∀i < length SA. SA ! i = length T"
  "lms_pre α T B SA LMS ⟹ length SA  = length T"
  "lms_pre α T B SA LMS ⟹ lms_bucket_init α T B"
  "lms_pre α T B SA LMS ⟹ strict_mono α"
  "lms_pre α T B SA LMS ⟹ distinct LMS"
  "lms_pre α T B SA LMS ⟹ set LMS = {i. abs_is_lms T i}"
  using lms_pre_def by blast+

lemma lms_vals_post_holds:
  assumes "∀i < length SA. SA ! i = length T"
  and     "distinct LMS"
  and     "lms_bucket_init α T B"
  and     "length SA = length T"
  and     "strict_mono α"
  and     "set LMS = {i. abs_is_lms T i}"
  and     "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs')"
shows "lms_vals_post α T SA'"
  unfolding lms_vals_post_def
proof(intro allI impI)
  fix b
  assume "b ≤ α (Max (set T))"

  from assms(6)
  have "∀x ∈ set LMS. abs_is_lms T x"
    by blast
  with lms_inv_holds[OF assms(1) _ assms(2-5,7)]
  have R0:"lms_inv α T B' LMS gs' [] SA SA'" .

  from lms_B_val[OF assms(1-7) `b ≤ α (Max (set T))`]
  have R1: "B' ! b = lms_bucket_start α T b" .

  have "bucket_end α T b ≤ length SA'"
    by (metis R0 bucket_end_le_length lms_inv_def)

  have "finite (lms_bucket α T b)"
    by (simp add: finite_lms_bucket)
  moreover
  from lms_slice_subset_lms_bucket[OF lms_invD(4,12)[OF R0] `b ≤ α (Max (set T))`]
  have "set (list_slice SA' (B' ! b) (bucket_end α T b)) ⊆ lms_bucket α T b" .
  with R1
  have "set (list_slice SA' (lms_bucket_start α T b) (bucket_end α T b)) ⊆ lms_bucket α T b"
    by simp
  moreover
  from lms_distinct_slice[OF lms_invD(1,2,4,12)[OF R0] `b ≤ α (Max (set T))`]
  have "distinct (list_slice SA' (B' ! b) (bucket_end α T b))" .
  with R1
  have "distinct (list_slice SA' (lms_bucket_start α T b) (bucket_end α T b))"
    by simp
  with distinct_card
  have "card (set (list_slice SA' (lms_bucket_start α T b) (bucket_end α T b)))
        = length (list_slice SA' (lms_bucket_start α T b) (bucket_end α T b))"
    by blast
  with `bucket_end α T b ≤ length SA'`
  have "card (set (list_slice SA' (lms_bucket_start α T b) (bucket_end α T b)))
        = lms_bucket_size α T b"
    by (metis add_diff_cancel_left' length_list_slice lms_bucket_pl_size_eq_end min.absorb_iff1)
  hence "card (set (list_slice SA' (lms_bucket_start α T b) (bucket_end α T b)))
         = card (lms_bucket α T b)"
    by (simp add: lms_bucket_size_def)
  ultimately
  show "lms_bucket α T b = set (list_slice SA' (lms_bucket_start α T b) (bucket_end α T b))"
    using card_subset_eq by blast
qed

corollary abs_bucket_insert_vals:
  assumes "lms_pre α T B SA LMS"
  shows "lms_vals_post α T (abs_bucket_insert α T B SA LMS)"
proof -
  have "∃SA' B' gs. bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by (meson prod_cases3)
  then obtain SA' B' gs where
    A: "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by blast
  hence "abs_bucket_insert α T B SA LMS = SA'"
    by (metis abs_bucket_insert_equiv fst_conv)
  with lms_vals_post_holds[OF lms_pre_elims(1,5,3,2,4,6)[OF assms] A]
  show ?thesis
    by simp
qed

definition lms_unknowns_post
where
  "lms_unknowns_post α T SA =
  (∀b ≤ α (Max (set T)).
    (∀i. bucket_start α T b ≤ i ∧ i < lms_bucket_start α T b ⟶ SA ! i = length T)
  )"

lemma lms_unknowns_postD:
  "⟦lms_unknowns_post α T SA; b ≤ α (Max (set T)); bucket_start α T b ≤ i;
    i < lms_bucket_start α T b⟧ ⟹
   SA ! i = length T"
  using lms_unknowns_post_def by blast

lemma lms_unknowns_post_holds:
  assumes "∀i < length SA. SA ! i = length T"
  and     "distinct LMS"
  and     "lms_bucket_init α T B"
  and     "length SA = length T"
  and     "strict_mono α"
  and     "set LMS = {i. abs_is_lms T i}"
  and     "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs')"
shows "lms_unknowns_post α T SA'"
  unfolding lms_unknowns_post_def
proof(intro allI impI; elim conjE)
  fix b i
  assume "b ≤ α (Max (set T))" "bucket_start α T b ≤ i" "i < lms_bucket_start α T b"

  from assms(6)
  have "∀x ∈ set LMS. abs_is_lms T x"
    by blast
  with lms_inv_holds[OF assms(1) _ assms(2-5,7)]
  have R0:"lms_inv α T B' LMS gs' [] SA SA'" .

  from `i < lms_bucket_start α T b`
  have "i < length SA"
    by (metis assms(4) bucket_end_le_length dual_order.strict_trans1 lms_bucket_start_le_bucket_end)
  moreover
  from lms_B_val[OF assms(1-7) `b ≤ α (Max (set T))`]
  have "B' ! b = lms_bucket_start α T b" .
  with `i < lms_bucket_start α T b`
  have "i < B' ! b"
    by simp
  with lms_unchanged_invD[OF lms_invD(5)[OF R0] `b ≤ α (Max (set T))` `bucket_start α T b ≤ i`]
  have "SA' ! i = SA ! i"
    by blast
  ultimately
  show "SA' ! i = length T"
    using assms(1) by auto
qed

corollary abs_bucket_insert_unknowns:
  assumes "lms_pre α T B SA LMS"
  shows "lms_unknowns_post α T (abs_bucket_insert α T B SA LMS)"
proof -
  have "∃SA' B' gs. bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by (meson prod_cases3)
  then obtain SA' B' gs where
    A: "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by blast
  hence "abs_bucket_insert α T B SA LMS = SA'"
    by (metis abs_bucket_insert_equiv fst_conv)
  with lms_unknowns_post_holds[OF lms_pre_elims(1,5,3,2,4,6)[OF assms] A]
  show ?thesis
    by simp
qed

corollary abs_bucket_insert_values:
  assumes "lms_pre α T B SA LMS"
  shows "∀b ≤ α (Max (set T)).
           (∀i. bucket_start α T b ≤ i ∧ i < lms_bucket_start α T b ⟶ (abs_bucket_insert α T B SA LMS) ! i = length T) ∧
           lms_bucket α T b = set (list_slice (abs_bucket_insert α T B SA LMS) (lms_bucket_start α T b) (bucket_end α T b))"
  by (meson assms abs_bucket_insert_unknowns abs_bucket_insert_vals lms_unknowns_postD lms_vals_postD)

lemma lms_lms_prefix_sorted_holds:
  assumes "∀i < length SA. SA ! i = length T"
  and     "distinct LMS"
  and     "lms_bucket_init α T B"
  and     "length SA = length T"
  and     "strict_mono α"
  and     "set LMS = {i. abs_is_lms T i}"
  and     "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs')"
shows "ordlistns.sorted (map (lms_prefix T) (filter (λx. x < length T) SA'))"
proof -
  from assms(6)
  have "∀x ∈ set LMS. abs_is_lms T x"
    by blast
  with lms_inv_holds[OF assms(1) _ assms(2-5,7)]
  have R0:"lms_inv α T B' LMS gs' [] SA SA'" .

  from lms_lms_prefix_sorted[OF lms_invD(2,4,5,8,12,13)[OF R0] assms(6)]
  show ?thesis .
qed

lemma lms_suffix_sorted_holds:
  assumes "∀i < length SA. SA ! i = length T"
  and     "distinct LMS"
  and     "lms_bucket_init α T B"
  and     "length SA = length T"
  and     "strict_mono α"
  and     "set LMS = {i. abs_is_lms T i}"
  and     "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs')"
  and     "ordlistns.sorted (map (suffix T) (rev LMS))"
shows "ordlistns.sorted (map (suffix T) (filter (λx. x < length T) SA'))"
proof -
  from assms(6)
  have "∀x ∈ set LMS. abs_is_lms T x"
    by blast
  with lms_inv_holds[OF assms(1) _ assms(2-5,7)]
  have R0:"lms_inv α T B' LMS gs' [] SA SA'" .

  from lms_suffix_sorted[OF lms_invD(2,4,5,7,8,12,13)[OF R0] assms(6) assms(8)]
  show ?thesis .
qed

lemma lms_bot_is_first:
  assumes "∀i < length SA. SA ! i = length T"
  and     "distinct LMS"
  and     "lms_bucket_init α T B"
  and     "length SA = length T"
  and     "strict_mono α"
  and     "set LMS = {i. abs_is_lms T i}"
  and     "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs')"
  and     "valid_list T"
  and     "length T = Suc (Suc n)"
  and     "α bot = 0"
shows "SA' ! 0 = Suc n"
proof -
  have "abs_is_lms T (Suc n)"
    by (simp add: assms(8,9) abs_is_lms_last)
  moreover
  have "α (T ! (Suc n)) = 0"
    by (metis assms(8-10) diff_Suc_1 last_conv_nth length_greater_0_conv valid_list_def)
  ultimately
  have "Suc n ∈ lms_bucket α T 0"
    by (simp add: assms(5,8-10) bucket_0 lms_bucket_def)

  have "lms_bucket_size α T 0 = Suc 0" "l_bucket_size α T 0 = 0" "pure_s_bucket_size α T 0 = 0"
    using assms(5,8-10) bucket_0_size2 by blast+
  hence "lms_bucket α T 0 = {Suc n}"
    by (metis One_nat_def add.commute assms(5,8-10) atLeastLessThan_singleton bucket_0
              lms_bucket_size_def lms_bucket_subset_bucket plus_1_eq_Suc subset_card_intvl_is_intvl)

  from assms(6)
  have "∀x ∈ set LMS. abs_is_lms T x"
    by blast
  with lms_inv_holds[OF assms(1) _ assms(2-5,7)]
  have R0:"lms_inv α T B' LMS gs' [] SA SA'" .


  from ‹l_bucket_size α T 0 = 0› ‹pure_s_bucket_size α T 0 = 0›
  have "lms_bucket_start α T 0 = 0"
    by (simp add: bucket_start_0 lms_bucket_start_def)
  moreover
  from lms_B_val[OF assms(1-7), of 0]
  have "B' ! 0 = lms_bucket_start α T 0"
    by simp
  moreover
  have "0 < bucket_end α T 0 "
    by (simp add: assms(5,8,10) valid_list_bucket_end_0)
  ultimately
  show ?thesis
    using lms_locations_invD[OF lms_invD(4)[OF R0], of 0 0] `lms_bucket α T 0 = {Suc n}`
    by auto
qed

corollary abs_bucket_insert_bot_first:
  assumes "lms_pre α T B SA LMS"
  and     "valid_list T"
  and     "length T = Suc (Suc n)"
  and     "α bot = 0"
shows "(abs_bucket_insert α T B SA LMS) ! 0 = Suc n"
proof -
  have "∃SA' B' gs. bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by (meson prod_cases3)
  then obtain SA' B' gs where
    A: "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by blast
  hence "abs_bucket_insert α T B SA LMS = SA'"
    by (metis abs_bucket_insert_equiv fst_conv)
  with lms_bot_is_first[OF lms_pre_elims(1,5,3,2,4,6)[OF assms(1)] A assms(2-)]
  show ?thesis
    by simp
qed

 ―‹ Used in SAIS algorithm as part of inducing the prefix ordering based on LMS ›
theorem lms_prefix_sorted_bucket:
  assumes "lms_pre α T B SA LMS"
  and     "b ≤ α (Max (set T))"
shows "ordlistns.sorted (map (lms_prefix T)
        (list_slice (abs_bucket_insert α T B SA LMS) (lms_bucket_start α T b) (bucket_end α T b)))"
      (is "ordlistns.sorted (map ?f ?SA)")
proof -
  have "∃SA' B' gs. bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by (meson prod_cases3)
  then obtain SA' B' gs where
    A: "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by blast
  hence "abs_bucket_insert α T B SA LMS = SA'"
    by (metis abs_bucket_insert_equiv fst_conv)

  from lms_vals_postD[OF abs_bucket_insert_vals[OF assms(1)] assms(2)]
  have P: "∀x ∈ set ?SA . x < length T"
    using abs_is_lms_imp_less_length lms_bucket_def by blast

  from lms_lms_prefix_sorted_holds[OF lms_pre_elims(1,5,3,2,4,6)[OF assms(1)] A]
  have "ordlistns.sorted (map (lms_prefix T) (filter (λx. x < length T) SA'))" .
  hence "ordlistns.sorted (map (lms_prefix T) (filter (λx. x < length T) ?SA))"
    using ‹abs_bucket_insert α T B SA LMS = SA'› ordlistns.sorted_map_filter_list_slice 
    by blast
  then show ?thesis
    by (simp add: P)
qed

 ―‹ Used in SAIS algorithm as part of inducing the suffix ordering based on LMS ›
theorem lms_suffix_sorted_bucket:
  assumes "lms_pre α T B SA LMS"
  and     "ordlistns.sorted (map (suffix T) (rev LMS))"
  and     "b ≤ α (Max (set T))"
shows "ordlistns.sorted (map (suffix T)
        (list_slice (abs_bucket_insert α T B SA LMS) (lms_bucket_start α T b) (bucket_end α T b)))"
      (is "ordlistns.sorted (map ?f ?SA)")
proof -
  have "∃SA' B' gs. bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by (meson prod_cases3)
  then obtain SA' B' gs where
    A: "bucket_insert_abs' α T B SA [] LMS = (SA', B', gs)"
    by blast
  hence "abs_bucket_insert α T B SA LMS = SA'"
    by (metis abs_bucket_insert_equiv fst_conv)

  from lms_vals_postD[OF abs_bucket_insert_vals[OF assms(1)] assms(3)]
  have P: "∀x ∈ set ?SA . x < length T"
    using abs_is_lms_imp_less_length lms_bucket_def by blast

  from lms_suffix_sorted_holds[OF lms_pre_elims(1,5,3,2,4,6)[OF assms(1)] A assms(2)]
  have "ordlistns.sorted (map (suffix T) (filter (λx. x < length T) SA'))" .
  hence "ordlistns.sorted (map (suffix T) (filter (λx. x < length T) ?SA))"
    using ‹abs_bucket_insert α T B SA LMS = SA'› ordlistns.sorted_map_filter_list_slice by blast
  then show ?thesis
    by (simp add: P)
qed

end