[STATEMENT]
lemma offs_enum_next_cons [rule_format]:
  assumes
    A: "index_less index key" and
    B: "\<forall>x \<in> set xs. key x \<in> {mi..ma}"
  shows "(if i < index key x n mi ma then (\<le>) else (<))
    (offs_next (offs (enum xs index key n mi ma) k)
      (length xs + k) xs index key mi ma i)
    (offs_next (offs ((enum xs index key n mi ma) [index key x n mi ma :=
      Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)
      (Suc (length xs + k)) (x # xs) index key mi ma i)"
  (is "(if i < ?i' then _ else _)
    (offs_next (offs ?ns _) _ _ _ _ _ _ _)
    (offs_next (offs ?ns' _) _ _ _ _ _ _ _)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < index key x n mi ma then (\<le>) else (<)) (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) (offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i)
[PROOF STEP]
proof (simp_all only: offs_next_def not_less split: if_split, (rule conjI, rule impI)+,
 simp, simp, (rule_tac [!] impI, (rule_tac [!] conjI)?)+, rule_tac [2-3] FalseE,
 rule_tac [4] conjI, rule_tac [4-5] impI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
assume
    C: "offs_set_next (offs ?ns k) xs index key mi ma i = {}"
      (is "?A = _") and
    D: "offs_set_next (offs ?ns' k) (x # xs) index key mi ma i \<noteq> {}"
      (is "?A' \<noteq> _") and
    E: "i < ?i'"
[PROOF STATE]
proof (state)
this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}
i < index key x n mi ma

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
from C
[PROOF STATE]
proof (chain)
picking this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}
[PROOF STEP]
have F: "\<forall>j \<noteq> ?i'. j \<notin> ?A'"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}

goal (1 subgoal):
 1. \<forall>j. j \<noteq> index key x n mi ma \<longrightarrow> j \<notin> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
by (rule_tac allI, rule_tac impI, rule_tac notI, simp add: enum_length
     offs_length offs_num_cons split: if_split_asm, (erule_tac conjE)+, simp)
[PROOF STATE]
proof (state)
this:
\<forall>j. j \<noteq> index key x n mi ma \<longrightarrow> j \<notin> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
from D
[PROOF STATE]
proof (chain)
picking this:
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}
[PROOF STEP]
have "Min ?A' \<in> ?A'"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
by (rule_tac Min_in, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence G: "Min ?A' < n"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have H: "Min ?A' = ?i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma
[PROOF STEP]
proof (rule Min_eqI, simp, rule eq_refl, erule contrapos_pp, insert F, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>j. j \<noteq> index key x n mi ma \<longrightarrow> j \<notin> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<Longrightarrow> index key x n mi ma \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
have "\<exists>j. j \<in> ?A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. \<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. \<forall>j. j \<noteq> index key x n mi ma \<longrightarrow> j \<notin> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<Longrightarrow> index key x n mi ma \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
obtain j where "j \<in> ?A'"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. (\<And>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. \<forall>j. j \<noteq> index key x n mi ma \<longrightarrow> j \<notin> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<Longrightarrow> index key x n mi ma \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. \<forall>j. j \<noteq> index key x n mi ma \<longrightarrow> j \<notin> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<Longrightarrow> index key x n mi ma \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
have "j = ?i'"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. j = index key x n mi ma
[PROOF STEP]
by (erule_tac contrapos_pp, insert F, simp)
[PROOF STATE]
proof (state)
this:
j = index key x n mi ma

goal (1 subgoal):
 1. \<forall>j. j \<noteq> index key x n mi ma \<longrightarrow> j \<notin> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<Longrightarrow> index key x n mi ma \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
j = index key x n mi ma
[PROOF STEP]
show "?i' \<in> ?A'"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
j = index key x n mi ma

goal (1 subgoal):
 1. index key x n mi ma \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index key x n mi ma \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
with G
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma
[PROOF STEP]
have "offs ?ns' k ! Min ?A' = offs ?ns k ! Min ?A'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma

goal (1 subgoal):
 1. offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by (subst offs_update, simp_all add: enum_length)
[PROOF STATE]
proof (state)
this:
offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
from A and B and G and H
[PROOF STATE]
proof (chain)
picking this:
index_less index key
\<forall>x\<in>set xs. key x \<in> {mi..ma}
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma
[PROOF STEP]
have
   "\<dots> = offs_next (offs ?ns k) (length xs + k) xs index key mi ma (Min ?A')"
[PROOF STATE]
proof (prove)
using this:
index_less index key
\<forall>x\<in>set xs. key x \<in> {mi..ma}
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
[PROOF STEP]
proof (rule_tac offs_enum_zero, simp_all, rule_tac ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (index key x n mi ma); index_less index key; index key x n mi ma < n; Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "?i' < n" and "0 < offs_num n xs index key mi ma ?i'"
[PROOF STATE]
proof (state)
this:
index key x n mi ma < n
0 < offs_num n xs index key mi ma (index key x n mi ma)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (index key x n mi ma); index_less index key; index key x n mi ma < n; Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "?i' \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma < n
0 < offs_num n xs index key mi ma (index key x n mi ma)

goal (1 subgoal):
 1. index key x n mi ma \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma < n
0 < offs_num n xs index key mi ma (index key x n mi ma)
i < index key x n mi ma

goal (1 subgoal):
 1. index key x n mi ma \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
index key x n mi ma \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; 0 < offs_num n xs index key mi ma (index key x n mi ma); index_less index key; index key x n mi ma < n; Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. False
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "\<dots> = length xs + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = length xs + k
[PROOF STEP]
proof (simp only: offs_next_def split: if_split, rule conjI, simp, rule impI,
   rule FalseE, simp, erule exE, (erule conjE)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "j < length (offs ?ns k)"
[PROOF STATE]
proof (state)
this:
j < length (offs (enum xs index key n mi ma) k)

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length (offs (enum xs index key n mi ma) k)

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "Min ?A' < j"
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < j

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "i < j"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < j

goal (1 subgoal):
 1. i < j
[PROOF STEP]
using E and H
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < j
i < index key x n mi ma
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = index key x n mi ma

goal (1 subgoal):
 1. i < j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < j

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < j

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "0 < offs_num (length (offs ?ns k)) xs index key mi ma j"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < length (offs (enum xs index key n mi ma) k)
i < j
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
have "j \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
j < length (offs (enum xs index key n mi ma) k)
i < j
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j

goal (1 subgoal):
 1. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < xa; xa < length (offs (enum xs index key n mi ma) k); 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. False
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = length xs + k

goal (5 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 5. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = length xs + k
[PROOF STEP]
show "length xs + k \<le> offs ?ns' k ! Min ?A'"
[PROOF STATE]
proof (prove)
using this:
offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = length xs + k

goal (1 subgoal):
 1. length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length xs + k \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
assume
    C: "offs_set_next (offs ?ns k) xs index key mi ma i = {}"
      (is "?A = _") and
    D: "offs_set_next (offs ?ns' k) (x # xs) index key mi ma i \<noteq> {}"
      (is "?A' \<noteq> _") and
    E: "?i' \<le> i"
[PROOF STATE]
proof (state)
this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}
index key x n mi ma \<le> i

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "\<exists>j. j \<in> ?A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. \<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
obtain j where F: "j \<in> ?A'"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. (\<And>j. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "j < length (offs ?ns k)"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. j < length (offs (enum xs index key n mi ma) k)
[PROOF STEP]
by (simp add: offs_length)
[PROOF STATE]
proof (state)
this:
j < length (offs (enum xs index key n mi ma) k)

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length (offs (enum xs index key n mi ma) k)

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "i < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. i < j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < j

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < j

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
i < j
[PROOF STEP]
have
   "0 < offs_num (length (offs ?ns k)) xs index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
using E and F
[PROOF STATE]
proof (prove)
using this:
i < j
index key x n mi ma \<le> i
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. 0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
by (simp add: offs_length enum_length offs_num_cons)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < length (offs (enum xs index key n mi ma) k)
i < j
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j
[PROOF STEP]
have "j \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
j < length (offs (enum xs index key n mi ma) k)
i < j
0 < offs_num (length (offs (enum xs index key n mi ma) k)) xs index key mi ma j

goal (1 subgoal):
 1. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (4 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 4. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. False
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
assume
    C: "offs_set_next (offs ?ns k) xs index key mi ma i \<noteq> {}"
      (is "?A \<noteq> _") and
    D: "offs_set_next (offs ?ns' k) (x # xs) index key mi ma i = {}"
      (is "?A' = _")
[PROOF STATE]
proof (state)
this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "\<exists>j. j \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. \<exists>j. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
obtain j where E: "j \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. (\<And>j. j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "j < length (offs ?ns' k)"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. j < length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)
[PROOF STEP]
by (simp add: offs_length)
[PROOF STATE]
proof (state)
this:
j < length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "i < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. i < j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < j

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < j

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "0 < offs_num (length (offs ?ns' k)) (x # xs) index key mi ma j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)) (x # xs) index key mi ma j
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. 0 < offs_num (length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)) (x # xs) index key mi ma j
[PROOF STEP]
by (simp add: offs_length enum_length offs_num_cons)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)) (x # xs) index key mi ma j

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)
i < j
0 < offs_num (length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)) (x # xs) index key mi ma j
[PROOF STEP]
have "j \<in> ?A'"
[PROOF STATE]
proof (prove)
using this:
j < length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)
i < j
0 < offs_num (length (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k)) (x # xs) index key mi ma j

goal (1 subgoal):
 1. j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (3 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 3. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. False
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
assume "offs_set_next (offs ?ns k) xs index key mi ma i \<noteq> {}"
    (is "?A \<noteq> _")
[PROOF STATE]
proof (state)
this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "Min ?A \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by (rule_tac Min_in, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence C: "Min ?A < n"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
assume "offs_set_next (offs ?ns' k) (x # xs) index key mi ma i \<noteq> {}"
    (is "?A' \<noteq> _")
[PROOF STATE]
proof (state)
this:
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence D: "Min ?A' \<in> ?A'"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
by (rule_tac Min_in, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence E: "Min ?A' < n"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "offs ?ns k ! Min ?A \<le> offs ?ns k ! Min ?A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
proof (cases "offs_num n xs index key mi ma (Min ?A') = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = 0

goal (2 subgoals):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "offs ?ns k ! Min ?A' =
      offs_next (offs ?ns k) (length xs + k) xs index key mi ma (Min ?A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
[PROOF STEP]
using A and B and E and True
[PROOF STATE]
proof (prove)
using this:
index_less index key
\<forall>x\<in>set xs. key x \<in> {mi..ma}
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n
offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = 0

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
[PROOF STEP]
by (rule_tac offs_enum_zero, simp_all)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (2 subgoals):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) = offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (2 subgoals):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
from A and B and C
[PROOF STATE]
proof (chain)
picking this:
index_less index key
\<forall>x\<in>set xs. key x \<in> {mi..ma}
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n
[PROOF STEP]
have "\<dots> \<ge> offs ?ns k ! Min ?A"
[PROOF STATE]
proof (prove)
using this:
index_less index key
\<forall>x\<in>set xs. key x \<in> {mi..ma}
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
[PROOF STEP]
proof (simp only: offs_next_def split: if_split, rule_tac conjI, rule_tac [!] impI,
     rule_tac offs_enum_ub, simp, simp, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
assume "offs_set_next (offs ?ns k) xs index key mi ma (Min ?A') \<noteq> {}"
        (is "?B \<noteq> _")
[PROOF STATE]
proof (state)
this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
hence "Min ?B \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> {}

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
[PROOF STEP]
by (rule_tac Min_in, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (1 subgoal):
 1. \<lbrakk>index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
hence "Min ?B \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. \<lbrakk>index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. \<lbrakk>index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
have "Min ?A \<le> Min ?B"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
by (rule_tac Min_le, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))

goal (1 subgoal):
 1. \<lbrakk>index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < n; offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> {}\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
show "offs ?ns k ! Min ?A \<le> offs ?ns k ! Min ?B"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))
[PROOF STEP]
by (rule_tac offs_mono, simp_all add: offs_length)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (2 subgoals):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) = 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0

goal (1 subgoal):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "Min ?A' \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "Min ?A \<le> Min ?A'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by (rule_tac Min_le, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)) \<noteq> 0 \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by (rule offs_mono, simp_all add: enum_length E)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "\<dots> \<le> offs ?ns' k ! Min ?A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by (subst offs_update, simp_all add: enum_length)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (2 subgoals):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; i < index key x n mi ma\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
 2. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
show "offs ?ns k ! Min ?A \<le> offs ?ns' k ! Min ?A'"
[PROOF STATE]
proof (prove)
using this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
let ?A = "offs_set_next (offs ?ns k) xs index key mi ma i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
assume "offs_set_next (offs ?ns' k) (x # xs) index key mi ma i \<noteq> {}"
    (is "?A' \<noteq> _")
[PROOF STATE]
proof (state)
this:
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence C: "Min ?A' \<in> ?A'"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i
[PROOF STEP]
by (rule_tac Min_in, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence D: "Min ?A' < n"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < n

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
assume "?i' \<le> i"
[PROOF STATE]
proof (state)
this:
index key x n mi ma \<le> i

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence E: "?i' < Min ?A'"
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma \<le> i

goal (1 subgoal):
 1. index key x n mi ma < Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma \<le> i
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. index key x n mi ma < Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index key x n mi ma < Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "0 < offs_num n xs index key mi ma (Min ?A')"
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma < Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. 0 < offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma < Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. 0 < offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
[PROOF STEP]
by (simp add: offs_length enum_length offs_num_cons)
[PROOF STATE]
proof (state)
this:
0 < offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "Min ?A' \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
0 < offs_num n xs index key mi ma (Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i))
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i
[PROOF STEP]
by (simp add: offs_length enum_length)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "Min ?A \<le> Min ?A'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) \<in> offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by (rule_tac Min_le, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
hence "offs ?ns k ! Min ?A \<le> offs ?ns k ! Min ?A'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by (rule offs_mono, simp_all add: enum_length D)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) \<le> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
have "\<dots> < offs ?ns' k ! Min ?A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma < Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
by (subst offs_update, simp_all add: enum_length D)
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. \<lbrakk>offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i \<noteq> {}; offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i \<noteq> {}; index key x n mi ma \<le> i\<rbrakk> \<Longrightarrow> offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
show "offs ?ns k ! Min ?A < offs ?ns' k ! Min ?A'"
[PROOF STATE]
proof (prove)
using this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offs (enum xs index key n mi ma) k ! Min (offs_set_next (offs (enum xs index key n mi ma) k) xs index key mi ma i) < offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! Min (offs_set_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (x # xs) index key mi ma i)

goal:
No subgoals!
[PROOF STEP]
qed