[STATEMENT]
lemma fill_none [rule_format]:
  assumes A: "index_less index key"
  shows
   "(\<forall>x \<in> set xs. key x \<in> {mi..ma}) \<longrightarrow>
    ns \<noteq> [] \<longrightarrow>
    offs_pred ns ub xs index key mi ma \<longrightarrow>
    offs_none ns ub xs index key mi ma i \<longrightarrow>
      fill xs ns index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set xs. key x \<in> {mi..ma}) \<longrightarrow> ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None
[PROOF STEP]
proof (induction xs arbitrary: ns, simp add: offs_none_def offs_num_def offs_next_def,
 (rule impI)+, simp add: Let_def, (erule conjE)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
fix x xs and ns :: "nat list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
let ?i' = "index key x (length ns) mi ma"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
let ?ns' = "ns[?i' := Suc (ns ! ?i')]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
assume
    B: "offs_pred ns ub (x # xs) index key mi ma" and
    C: "offs_none ns ub (x # xs) index key mi ma i"
[PROOF STATE]
proof (state)
this:
offs_pred ns ub (x # xs) index key mi ma
offs_none ns ub (x # xs) index key mi ma i

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
assume
    D: "ns \<noteq> []" and "mi \<le> key x" and "key x \<le> ma"
[PROOF STATE]
proof (state)
this:
ns \<noteq> []
mi \<le> key x
key x \<le> ma

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ns \<noteq> []
mi \<le> key x
key x \<le> ma

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
ns \<noteq> []
mi \<le> key x
key x \<le> ma
[PROOF STEP]
have
    E: "?i' < length ns"
[PROOF STATE]
proof (prove)
using this:
ns \<noteq> []
mi \<le> key x
key x \<le> ma

goal (1 subgoal):
 1. index key x (length ns) mi ma < length ns
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
ns \<noteq> []
mi \<le> key x
key x \<le> ma
index_less index key

goal (1 subgoal):
 1. index key x (length ns) mi ma < length ns
[PROOF STEP]
by (simp add: index_less_def)
[PROOF STATE]
proof (state)
this:
index key x (length ns) mi ma < length ns

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
hence "offs_pred ?ns' ub xs index key mi ma"
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma < length ns

goal (1 subgoal):
 1. offs_pred (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma
[PROOF STEP]
by (rule_tac offs_pred_cons [OF B], simp)
[PROOF STATE]
proof (state)
this:
offs_pred (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_pred (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
assume "\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow>
    offs_none ns ub xs index key mi ma i \<longrightarrow>
    fill xs ns index key ub mi ma ! i = None"
[PROOF STATE]
proof (state)
this:
?ns \<noteq> [] \<longrightarrow> offs_pred ?ns ub xs index key mi ma \<longrightarrow> offs_none ?ns ub xs index key mi ma i \<longrightarrow> fill xs ?ns index key ub mi ma ! i = None

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ns \<noteq> []
mi \<le> key x
key x \<le> ma
offs_pred (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma
?ns \<noteq> [] \<longrightarrow> offs_pred ?ns ub xs index key mi ma \<longrightarrow> offs_none ?ns ub xs index key mi ma i \<longrightarrow> fill xs ?ns index key ub mi ma ! i = None
[PROOF STEP]
have
    F: "offs_none ?ns' ub xs index key mi ma i \<longrightarrow>
      fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
using this:
ns \<noteq> []
mi \<le> key x
key x \<le> ma
offs_pred (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma
?ns \<noteq> [] \<longrightarrow> offs_pred ?ns ub xs index key mi ma \<longrightarrow> offs_none ?ns ub xs index key mi ma i \<longrightarrow> fill xs ?ns index key ub mi ma ! i = None

goal (1 subgoal):
 1. offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. \<And>a xs ns. \<lbrakk>\<And>ns. ns \<noteq> [] \<longrightarrow> offs_pred ns ub xs index key mi ma \<longrightarrow> offs_none ns ub xs index key mi ma i \<longrightarrow> fill xs ns index key ub mi ma ! i = None; ns \<noteq> []; offs_pred ns ub (a # xs) index key mi ma; offs_none ns ub (a # xs) index key mi ma i; mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma\<rbrakk> \<Longrightarrow> (fill xs (ns[index key a (length ns) mi ma := Suc (ns ! index key a (length ns) mi ma)]) index key ub mi ma)[ns ! index key a (length ns) mi ma := Some a] ! i = None
[PROOF STEP]
show "(fill xs ?ns' index key ub mi ma)[ns ! ?i' := Some x] ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
proof (insert C, simp add: offs_none_def, erule disjE, erule_tac [2] disjE, simp_all del: subst_all
   add: offs_num_cons split: if_split_asm, erule conjE, rule case_split, drule mp,
   assumption, simp_all del: subst_all, (erule conjE)+, (erule_tac [2] conjE)+,
   erule_tac [3] conjE, erule_tac [5] conjE)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>j. \<lbrakk>index key x (length ns) mi ma = j; Suc (ns ! j + offs_num (length ns) xs index key mi ma j) \<le> i; j < length ns; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<And>j. \<lbrakk>index key x (length ns) mi ma \<noteq> j; ns ! j + offs_num (length ns) xs index key mi ma j \<le> i; j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 3. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 4. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 5. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>j. \<lbrakk>index key x (length ns) mi ma = j; Suc (ns ! j + offs_num (length ns) xs index key mi ma j) \<le> i; j < length ns; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<And>j. \<lbrakk>index key x (length ns) mi ma \<noteq> j; ns ! j + offs_num (length ns) xs index key mi ma j \<le> i; j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 3. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 4. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 5. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
assume
      G: "?i' = j" and
      H: "j < length ns" and
      I: "Suc (ns ! j + offs_num (length ns) xs index key mi ma j) \<le> i" and
      J: "i < offs_next ns ub (x # xs) index key mi ma j"
[PROOF STATE]
proof (state)
this:
index key x (length ns) mi ma = j
j < length ns
Suc (ns ! j + offs_num (length ns) xs index key mi ma j) \<le> i
i < offs_next ns ub (x # xs) index key mi ma j

goal (5 subgoals):
 1. \<And>j. \<lbrakk>index key x (length ns) mi ma = j; Suc (ns ! j + offs_num (length ns) xs index key mi ma j) \<le> i; j < length ns; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<And>j. \<lbrakk>index key x (length ns) mi ma \<noteq> j; ns ! j + offs_num (length ns) xs index key mi ma j \<le> i; j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 3. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 4. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 5. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
show "fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
proof (cases "0 < offs_num (length ns) xs index key mi ma j",
     case_tac [2] "offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}",
     simp_all only: not_not not_gr0)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and>
        ?ns' ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and>
        i < offs_next ?ns' ub xs index key mi ma j \<longrightarrow>
          fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by (simp add: offs_none_def, blast)
[PROOF STATE]
proof (state)
this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
assume "0 < offs_num (length ns) xs index key mi ma j"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma j

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma j

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "?ns' ! j + offs_num (length ns) xs index key mi ma j \<le> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i
[PROOF STEP]
using G and H and I
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = j
j < length ns
Suc (ns ! j + offs_num (length ns) xs index key mi ma j) \<le> i

goal (1 subgoal):
 1. ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "0 < offs_num (length ns) (x # xs) index key mi ma j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma j
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = j

goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma j
[PROOF STEP]
by (simp add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) (x # xs) index key mi ma j

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "offs_next ns ub (x # xs) index key mi ma j \<le>
        offs_next ?ns' ub xs index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma j

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
using G and H
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma j
index key x (length ns) mi ma = j
j < length ns

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
by (rule_tac offs_pred_next_cons [OF B], simp_all)
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "i < offs_next ?ns' ub xs index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
using J
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
i < offs_next ns ub (x # xs) index key mi ma j

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
0 < offs_num (length ns) xs index key mi ma j
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
have "fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
using this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
0 < offs_num (length ns) xs index key mi ma j
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
0 < offs_num (length ns) xs index key mi ma j
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
j < length ns

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 3. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
index key x (length ns) mi ma = j

goal (1 subgoal):
 1. fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
let ?j' = "Max (offs_set_prev ns (x # xs) index key mi ma j)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "?j' < length ns \<and> 0 < offs_num (length ns) xs index key mi ma ?j' \<and>
        ?ns' ! ?j' + offs_num (length ns) xs index key mi ma ?j' \<le> i \<and>
        i < offs_next ?ns' ub xs index key mi ma ?j' \<longrightarrow>
          fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by (simp add: offs_none_def, blast)
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
assume K: "offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}"
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "?j' \<in> offs_set_prev ns (x # xs) index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}

goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma j) \<in> offs_set_prev ns (x # xs) index key mi ma j
[PROOF STEP]
by (rule_tac Max_in, simp)
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma j) \<in> offs_set_prev ns (x # xs) index key mi ma j

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence L: "?j' < length ns \<and> ?j' < j \<and>
        0 < offs_num (length ns) xs index key mi ma ?j'"
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma j) \<in> offs_set_prev ns (x # xs) index key mi ma j

goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> Max (offs_set_prev ns (x # xs) index key mi ma j) < j \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma j) \<in> offs_set_prev ns (x # xs) index key mi ma j
index key x (length ns) mi ma = j

goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> Max (offs_set_prev ns (x # xs) index key mi ma j) < j \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))
[PROOF STEP]
by (auto, subst (asm) (2) offs_num_cons, simp)
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> Max (offs_set_prev ns (x # xs) index key mi ma j) < j \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> Max (offs_set_prev ns (x # xs) index key mi ma j) < j \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "ns ! ?j' + offs_num (length ns) (x # xs)
        index key mi ma ?j' \<le> ns ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j
[PROOF STEP]
using G and H and L
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = j
j < length ns
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> Max (offs_set_prev ns (x # xs) index key mi ma j) < j \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))

goal (1 subgoal):
 1. ns ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j
[PROOF STEP]
by (rule_tac offs_pred_asc [OF B], simp_all add:
         offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "?ns' ! ?j' + offs_num (length ns) xs index key mi ma ?j' \<le> ns ! j"
[PROOF STATE]
proof (prove)
using this:
ns ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j

goal (1 subgoal):
 1. ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j
[PROOF STEP]
using G and H and L
[PROOF STATE]
proof (prove)
using this:
ns ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j
index key x (length ns) mi ma = j
j < length ns
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> Max (offs_set_prev ns (x # xs) index key mi ma j) < j \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))

goal (1 subgoal):
 1. ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j
[PROOF STEP]
by (subst nth_list_update, simp_all add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "?ns' ! ?j' + offs_num (length ns) xs index key mi ma ?j' \<le> i"
[PROOF STATE]
proof (prove)
using this:
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j

goal (1 subgoal):
 1. ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> ns ! j
Suc (ns ! j + offs_num (length ns) xs index key mi ma j) \<le> i

goal (1 subgoal):
 1. ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
assume M: "offs_num (length ns) xs index key mi ma j = 0"
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma j = 0

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "offs_next (ns[j := Suc (ns ! j)]) ub xs index key mi ma ?j' =
       (if 0 < offs_num (length ns) xs index key mi ma j
        then Suc (ns ! j)
        else offs_next ns ub (x # xs) index key mi ma j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next (ns[j := Suc (ns ! j)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = (if 0 < offs_num (length ns) xs index key mi ma j then Suc (ns ! j) else offs_next ns ub (x # xs) index key mi ma j)
[PROOF STEP]
using G and K
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = j
offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}

goal (1 subgoal):
 1. offs_next (ns[j := Suc (ns ! j)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = (if 0 < offs_num (length ns) xs index key mi ma j then Suc (ns ! j) else offs_next ns ub (x # xs) index key mi ma j)
[PROOF STEP]
by (rule_tac offs_next_cons_neq, simp_all)
[PROOF STATE]
proof (state)
this:
offs_next (ns[j := Suc (ns ! j)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = (if 0 < offs_num (length ns) xs index key mi ma j then Suc (ns ! j) else offs_next ns ub (x # xs) index key mi ma j)

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "offs_next ?ns' ub xs index key mi ma ?j' =
        offs_next ns ub (x # xs) index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[j := Suc (ns ! j)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = (if 0 < offs_num (length ns) xs index key mi ma j then Suc (ns ! j) else offs_next ns ub (x # xs) index key mi ma j)

goal (1 subgoal):
 1. offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = offs_next ns ub (x # xs) index key mi ma j
[PROOF STEP]
using G and M
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[j := Suc (ns ! j)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = (if 0 < offs_num (length ns) xs index key mi ma j then Suc (ns ! j) else offs_next ns ub (x # xs) index key mi ma j)
index key x (length ns) mi ma = j
offs_num (length ns) xs index key mi ma j = 0

goal (1 subgoal):
 1. offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = offs_next ns ub (x # xs) index key mi ma j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = offs_next ns ub (x # xs) index key mi ma j

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "i < offs_next ?ns' ub xs index key mi ma ?j'"
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = offs_next ns ub (x # xs) index key mi ma j

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))
[PROOF STEP]
using J
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) = offs_next ns ub (x # xs) index key mi ma j
i < offs_next ns ub (x # xs) index key mi ma j

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> Max (offs_set_prev ns (x # xs) index key mi ma j) < j \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))
[PROOF STEP]
have "fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
Max (offs_set_prev ns (x # xs) index key mi ma j) < length ns \<and> Max (offs_set_prev ns (x # xs) index key mi ma j) < j \<and> 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))
ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! Max (offs_set_prev ns (x # xs) index key mi ma j) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j)) \<le> i
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma j))

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (2 subgoals):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
 2. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
index key x (length ns) mi ma = j

goal (1 subgoal):
 1. fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "offs_num (length ns) xs index key mi ma 0 = 0 \<and>
        i < offs_next ?ns' ub xs index key mi ma 0 \<longrightarrow>
          fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by (simp add: offs_none_def)
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
assume
        K: "offs_set_prev ns (x # xs) index key mi ma j = {}" and
        L: "offs_num (length ns) xs index key mi ma j = 0"
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma j = {}
offs_num (length ns) xs index key mi ma j = 0

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "offs_set_prev ns (x # xs) index key mi ma j =
        offs_set_prev ?ns' xs index key mi ma j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_set_prev ns (x # xs) index key mi ma j = offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = j

goal (1 subgoal):
 1. offs_set_prev ns (x # xs) index key mi ma j = offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j
[PROOF STEP]
by (rule_tac set_eqI, rule_tac iffI,
         simp_all add: offs_num_cons split: if_split_asm)
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma j = offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence M: "offs_set_prev ?ns' xs index key mi ma j = {}"
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma j = offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j

goal (1 subgoal):
 1. offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j = {}
[PROOF STEP]
using K
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma j = offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j
offs_set_prev ns (x # xs) index key mi ma j = {}

goal (1 subgoal):
 1. offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j = {}

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "offs_num (length ns) xs index key mi ma 0 = 0"
[PROOF STATE]
proof (prove)
using this:
offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j = {}

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0
[PROOF STEP]
using H and L
[PROOF STATE]
proof (prove)
using this:
offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j = {}
j < length ns
offs_num (length ns) xs index key mi ma j = 0

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0
[PROOF STEP]
by (cases j, simp_all)
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have N: "offs_next ?ns' ub xs index key mi ma 0 =
        offs_next ?ns' ub xs index key mi ma j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 = offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
using H and L and M
[PROOF STATE]
proof (prove)
using this:
j < length ns
offs_num (length ns) xs index key mi ma j = 0
offs_set_prev (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) xs index key mi ma j = {}

goal (1 subgoal):
 1. offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 = offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
by (rule_tac offs_next_zero, simp_all)
[PROOF STATE]
proof (state)
this:
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 = offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
have "offs_next ?ns' ub xs index key mi ma j =
        offs_next ns ub (x # xs) index key mi ma j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma j
[PROOF STEP]
using G and H and K
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = j
j < length ns
offs_set_prev ns (x # xs) index key mi ma j = {}

goal (1 subgoal):
 1. offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma j
[PROOF STEP]
by (subst offs_next_cons_eq, simp_all add:
         offs_num_cons)
[PROOF STATE]
proof (state)
this:
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma j

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "i < offs_next ?ns' ub xs index key mi ma 0"
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma j

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
using J and N
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma j
i < offs_next ns ub (x # xs) index key mi ma j
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 = offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
offs_num (length ns) xs index key mi ma 0 = 0
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
have "fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
offs_num (length ns) xs index key mi ma 0 = 0
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. \<lbrakk>offs_num (length ns) xs index key mi ma j = 0; offs_set_prev ns (x # xs) index key mi ma j = {}\<rbrakk> \<Longrightarrow> fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
index key x (length ns) mi ma = j

goal (1 subgoal):
 1. fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fill xs (ns[j := Suc (ns ! j)]) index key ub mi ma ! i = None

goal (4 subgoals):
 1. \<And>j. \<lbrakk>index key x (length ns) mi ma \<noteq> j; ns ! j + offs_num (length ns) xs index key mi ma j \<le> i; j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 3. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 4. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>j. \<lbrakk>index key x (length ns) mi ma \<noteq> j; ns ! j + offs_num (length ns) xs index key mi ma j \<le> i; j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 3. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 4. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>j. \<lbrakk>index key x (length ns) mi ma \<noteq> j; ns ! j + offs_num (length ns) xs index key mi ma j \<le> i; j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 3. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 4. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
assume
      G: "?i' \<noteq> j" and
      H: "j < length ns" and
      I: "ns ! j + offs_num (length ns) xs index key mi ma j \<le> i" and
      J: "i < offs_next ns ub (x # xs) index key mi ma j" and
      K: "0 < offs_num (length ns) xs index key mi ma j"
[PROOF STATE]
proof (state)
this:
index key x (length ns) mi ma \<noteq> j
j < length ns
ns ! j + offs_num (length ns) xs index key mi ma j \<le> i
i < offs_next ns ub (x # xs) index key mi ma j
0 < offs_num (length ns) xs index key mi ma j

goal (4 subgoals):
 1. \<And>j. \<lbrakk>index key x (length ns) mi ma \<noteq> j; ns ! j + offs_num (length ns) xs index key mi ma j \<le> i; j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 3. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 4. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
from G
[PROOF STATE]
proof (chain)
picking this:
index key x (length ns) mi ma \<noteq> j
[PROOF STEP]
have "ns ! ?i' \<noteq> i"
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma \<noteq> j

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
proof (rule_tac notI, cases "?i' < j", simp_all add: not_less le_less)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; index key x (length ns) mi ma < j\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "?i' < j"
[PROOF STATE]
proof (state)
this:
index key x (length ns) mi ma < j

goal (2 subgoals):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; index key x (length ns) mi ma < j\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "ns ! ?i' + offs_num (length ns) (x # xs) index key mi ma ?i' \<le> ns ! j"
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma < j

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma + offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma) \<le> ns ! j
[PROOF STEP]
using H and K
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma < j
j < length ns
0 < offs_num (length ns) xs index key mi ma j

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma + offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma) \<le> ns ! j
[PROOF STEP]
by (rule_tac offs_pred_asc [OF B], simp_all add:
         offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma + offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma) \<le> ns ! j

goal (2 subgoals):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; index key x (length ns) mi ma < j\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma + offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma) \<le> ns ! j

goal (2 subgoals):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; index key x (length ns) mi ma < j\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "ns ! ?i' = i"
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma = i

goal (2 subgoals):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; index key x (length ns) mi ma < j\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ns ! index key x (length ns) mi ma + offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma) \<le> ns ! j
ns ! index key x (length ns) mi ma = i
[PROOF STEP]
have "i < ns ! j"
[PROOF STATE]
proof (prove)
using this:
ns ! index key x (length ns) mi ma + offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma) \<le> ns ! j
ns ! index key x (length ns) mi ma = i

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

goal (2 subgoals):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; index key x (length ns) mi ma < j\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
i < ns ! j

goal (1 subgoal):
 1. False
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
i < ns ! j
ns ! j + offs_num (length ns) xs index key mi ma j \<le> i

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

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "j < ?i'"
[PROOF STATE]
proof (state)
this:
j < index key x (length ns) mi ma

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence L: "?i' \<in> offs_set_next ns (x # xs) index key mi ma j"
        (is "_ \<in> ?A")
[PROOF STATE]
proof (prove)
using this:
j < index key x (length ns) mi ma

goal (1 subgoal):
 1. index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma j
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
j < index key x (length ns) mi ma
index key x (length ns) mi ma < length ns

goal (1 subgoal):
 1. index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma j
[PROOF STEP]
by (simp add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma j

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "Min ?A \<le> ?i'"
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma j

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) \<le> index key x (length ns) mi ma
[PROOF STEP]
by (rule_tac Min_le, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<le> index key x (length ns) mi ma

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "Min ?A < ?i' \<or> Min ?A = ?i'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<le> index key x (length ns) mi ma

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<or> Min (offs_set_next ns (x # xs) index key mi ma j) = index key x (length ns) mi ma
[PROOF STEP]
by (simp add: le_less)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<or> Min (offs_set_next ns (x # xs) index key mi ma j) = index key x (length ns) mi ma

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "ns ! Min ?A \<le> ns ! ?i'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<or> Min (offs_set_next ns (x # xs) index key mi ma j) = index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
proof (rule disjE, simp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
assume "Min ?A < ?i'"
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
have "Min ?A \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma j

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j
[PROOF STEP]
by (rule_tac Min_in, simp, blast)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
hence "0 < offs_num (length ns) (x # xs) index key mi ma (Min ?A)"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j

goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j))

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j))
[PROOF STEP]
have "ns ! Min ?A + offs_num (length ns) (x # xs)
          index key mi ma (Min ?A) \<le> ns ! ?i'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j))

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j)) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j))
index key x (length ns) mi ma < length ns

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j)) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
by (rule_tac offs_pred_asc [OF B], simp_all add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j)) \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma j) + offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma j)) \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "offs_next ns ub (x # xs) index key mi ma j \<le> ns ! ?i'"
[PROOF STATE]
proof (prove)
using this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma j) \<le> ns ! index key x (length ns) mi ma
index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma j

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
by (simp only: offs_next_def split: if_split, blast)
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma j \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma j \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "ns ! ?i' = i"
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma = i

goal (1 subgoal):
 1. \<lbrakk>ns ! index key x (length ns) mi ma = i; j < index key x (length ns) mi ma\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_next ns ub (x # xs) index key mi ma j \<le> ns ! index key x (length ns) mi ma
ns ! index key x (length ns) mi ma = i
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma j \<le> ns ! index key x (length ns) mi ma
ns ! index key x (length ns) mi ma = i

goal (1 subgoal):
 1. False
[PROOF STEP]
using J
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma j \<le> ns ! index key x (length ns) mi ma
ns ! index key x (length ns) mi ma = i
i < offs_next ns ub (x # xs) index key mi ma j

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:
ns ! index key x (length ns) mi ma \<noteq> i

goal (4 subgoals):
 1. \<And>j. \<lbrakk>index key x (length ns) mi ma \<noteq> j; ns ! j + offs_num (length ns) xs index key mi ma j \<le> i; j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < offs_next ns ub (x # xs) index key mi ma j\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 3. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 4. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
thus "(fill xs ?ns' index key ub mi ma)[ns ! ?i' := Some x] ! i = None"
[PROOF STATE]
proof (prove)
using this:
ns ! index key x (length ns) mi ma \<noteq> i

goal (1 subgoal):
 1. (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
proof simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
have "j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and>
        ?ns' ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and>
        i < offs_next ?ns' ub xs index key mi ma j \<longrightarrow>
          fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by (simp add: offs_none_def, blast)
[PROOF STATE]
proof (state)
this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
have "offs_next ns ub (x # xs) index key mi ma j \<le>
        offs_next ?ns' ub xs index key mi ma j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
using E and K
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma < length ns
0 < offs_num (length ns) xs index key mi ma j

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
by (rule_tac offs_pred_next_cons [OF B], simp_all add:
         offs_num_cons)
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "i < offs_next ?ns' ub xs index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
using J
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
i < offs_next ns ub (x # xs) index key mi ma j

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
[PROOF STEP]
show "fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
using this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using G and H and I and K
[PROOF STATE]
proof (prove)
using this:
j < length ns \<and> 0 < offs_num (length ns) xs index key mi ma j \<and> ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! j + offs_num (length ns) xs index key mi ma j \<le> i \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma j
index key x (length ns) mi ma \<noteq> j
j < length ns
ns ! j + offs_num (length ns) xs index key mi ma j \<le> i
0 < offs_num (length ns) xs index key mi ma j

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None

goal (3 subgoals):
 1. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 3. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 3. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
assume
      G: "0 < ?i'" and
      H: "offs_num (length ns) xs index key mi ma 0 = 0" and
      I: "i < offs_next ns ub (x # xs) index key mi ma 0"
[PROOF STATE]
proof (state)
this:
0 < index key x (length ns) mi ma
offs_num (length ns) xs index key mi ma 0 = 0
i < offs_next ns ub (x # xs) index key mi ma 0

goal (3 subgoals):
 1. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 3. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
have "ns ! ?i' \<noteq> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma = i \<Longrightarrow> False
[PROOF STEP]
have "0 < offs_num (length ns) (x # xs) index key mi ma ?i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma)
[PROOF STEP]
by (simp add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma)

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma = i \<Longrightarrow> False
[PROOF STEP]
hence L: "?i' \<in> offs_set_next ns (x # xs) index key mi ma 0"
        (is "_ \<in> ?A")
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma)

goal (1 subgoal):
 1. index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma 0
[PROOF STEP]
using E and G
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma (index key x (length ns) mi ma)
index key x (length ns) mi ma < length ns
0 < index key x (length ns) mi ma

goal (1 subgoal):
 1. index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma 0

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

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> index key x (length ns) mi ma
[PROOF STEP]
by (rule_tac Min_le, simp)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma = i \<Longrightarrow> False
[PROOF STEP]
hence "Min ?A < ?i' \<or> Min ?A = ?i'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> index key x (length ns) mi ma

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<or> Min (offs_set_next ns (x # xs) index key mi ma 0) = index key x (length ns) mi ma
[PROOF STEP]
by (simp add: le_less)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<or> Min (offs_set_next ns (x # xs) index key mi ma 0) = index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma = i \<Longrightarrow> False
[PROOF STEP]
hence "ns ! Min ?A \<le> ns ! ?i'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<or> Min (offs_set_next ns (x # xs) index key mi ma 0) = index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
proof (rule disjE, simp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
assume "Min ?A < ?i'"
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
have "Min ?A \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) \<in> offs_set_next ns (x # xs) index key mi ma 0
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma 0

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) \<in> offs_set_next ns (x # xs) index key mi ma 0
[PROOF STEP]
by (rule_tac Min_in, simp, blast)
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma 0) \<in> offs_set_next ns (x # xs) index key mi ma 0

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
hence "0 < offs_num (length ns) (x # xs) index key mi ma (Min ?A)"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma 0) \<in> offs_set_next ns (x # xs) index key mi ma 0

goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0))

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0))
[PROOF STEP]
have "ns ! Min ?A + offs_num (length ns) (x # xs)
          index key mi ma (Min ?A) \<le> ns ! ?i'"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0))

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) + offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0)) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0))
index key x (length ns) mi ma < length ns

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) + offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0)) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
by (rule_tac offs_pred_asc [OF B], simp_all add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) + offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0)) \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma 0) < index key x (length ns) mi ma \<Longrightarrow> ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) + offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_next ns (x # xs) index key mi ma 0)) \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma = i \<Longrightarrow> False
[PROOF STEP]
hence "offs_next ns ub (x # xs) index key mi ma 0 \<le> ns ! ?i'"
[PROOF STATE]
proof (prove)
using this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
ns ! Min (offs_set_next ns (x # xs) index key mi ma 0) \<le> ns ! index key x (length ns) mi ma
index key x (length ns) mi ma \<in> offs_set_next ns (x # xs) index key mi ma 0

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
by (simp only: offs_next_def split: if_split, blast)
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma = i \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma = i \<Longrightarrow> False
[PROOF STEP]
assume "ns ! ?i' = i"
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma = i

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma = i \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_next ns ub (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
ns ! index key x (length ns) mi ma = i
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
ns ! index key x (length ns) mi ma = i

goal (1 subgoal):
 1. False
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
ns ! index key x (length ns) mi ma = i
i < offs_next ns ub (x # xs) index key mi ma 0

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:
ns ! index key x (length ns) mi ma \<noteq> i

goal (3 subgoals):
 1. \<lbrakk>0 < index key x (length ns) mi ma; offs_num (length ns) xs index key mi ma 0 = 0; i < offs_next ns ub (x # xs) index key mi ma 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
 2. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 3. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
thus "(fill xs ?ns' index key ub mi ma)[ns ! ?i' := Some x] ! i = None"
[PROOF STATE]
proof (prove)
using this:
ns ! index key x (length ns) mi ma \<noteq> i

goal (1 subgoal):
 1. (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
proof simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
have "offs_num (length ns) xs index key mi ma 0 = 0 \<and>
        i < offs_next ?ns' ub xs index key mi ma 0 \<longrightarrow>
          fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by (simp add: offs_none_def)
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
have "offs_next ns ub (x # xs) index key mi ma 0 \<le>
        offs_next ?ns' ub xs index key mi ma 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
using E and G and H
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma < length ns
0 < index key x (length ns) mi ma
offs_num (length ns) xs index key mi ma 0 = 0

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
by (rule_tac offs_pred_zero_cons [OF B],
         simp_all add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "i < offs_next ?ns' ub xs index key mi ma 0"
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
i < offs_next ns ub (x # xs) index key mi ma 0

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
show "fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
offs_num (length ns) xs index key mi ma 0 = 0

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None

goal (2 subgoals):
 1. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
assume
      G: "?i' = 0" and
      H: "i < ns ! 0"
[PROOF STATE]
proof (state)
this:
index key x (length ns) mi ma = 0
i < ns ! 0

goal (2 subgoals):
 1. \<lbrakk>index key x (length ns) mi ma = 0; i < ns ! 0\<rbrakk> \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
show "fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
proof (cases "0 < offs_num (length ns) xs index key mi ma 0", simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
have "0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ?ns' ! 0 \<longrightarrow>
        fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by (simp add: offs_none_def)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
assume "0 < offs_num (length ns) xs index key mi ma 0"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma 0

goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma 0

goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
have "i < ?ns' ! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0
[PROOF STEP]
using D and G and H
[PROOF STATE]
proof (prove)
using this:
ns \<noteq> []
index key x (length ns) mi ma = 0
i < ns ! 0

goal (1 subgoal):
 1. i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0

goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
 2. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
0 < offs_num (length ns) xs index key mi ma 0
i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
0 < offs_num (length ns) xs index key mi ma 0
i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0

goal (1 subgoal):
 1. fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
0 < offs_num (length ns) xs index key mi ma 0
i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0
index key x (length ns) mi ma = 0

goal (1 subgoal):
 1. fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
have "offs_num (length ns) xs index key mi ma 0 = 0 \<and>
        i < offs_next ?ns' ub xs index key mi ma 0 \<longrightarrow>
          fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by (simp add: offs_none_def)
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
assume "offs_num (length ns) xs index key mi ma 0 = 0"
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
have I: "offs_next ?ns' ub xs index key mi ma 0 =
        offs_next ns ub (x # xs) index key mi ma 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
using D and G
[PROOF STATE]
proof (prove)
using this:
ns \<noteq> []
index key x (length ns) mi ma = 0

goal (1 subgoal):
 1. offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
by (rule_tac offs_next_cons_eq, simp_all add:
         offs_num_cons)
[PROOF STATE]
proof (state)
this:
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
have "ns ! 0 < offs_next ns ub (x # xs) index key mi ma 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! 0 < offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
using D and G
[PROOF STATE]
proof (prove)
using this:
ns \<noteq> []
index key x (length ns) mi ma = 0

goal (1 subgoal):
 1. ns ! 0 < offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
by (rule_tac offs_pred_next [OF B], simp_all add:
         offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! 0 < offs_next ns ub (x # xs) index key mi ma 0

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
hence "i < offs_next ?ns' ub xs index key mi ma 0"
[PROOF STATE]
proof (prove)
using this:
ns ! 0 < offs_next ns ub (x # xs) index key mi ma 0

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
using H and I
[PROOF STATE]
proof (prove)
using this:
ns ! 0 < offs_next ns ub (x # xs) index key mi ma 0
i < ns ! 0
offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0

goal (1 subgoal):
 1. i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0 \<Longrightarrow> fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
offs_num (length ns) xs index key mi ma 0 = 0
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
offs_num (length ns) xs index key mi ma 0 = 0
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0

goal (1 subgoal):
 1. fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma 0 = 0 \<and> i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
offs_num (length ns) xs index key mi ma 0 = 0
i < offs_next (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma 0
index key x (length ns) mi ma = 0

goal (1 subgoal):
 1. fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fill xs (ns[0 := Suc (ns ! 0)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
assume
      G: "0 < ?i'" and
      H: "0 < offs_num (length ns) xs index key mi ma 0" and
      I: "i < ns ! 0"
[PROOF STATE]
proof (state)
this:
0 < index key x (length ns) mi ma
0 < offs_num (length ns) xs index key mi ma 0
i < ns ! 0

goal (1 subgoal):
 1. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
have "ns ! ?i' \<noteq> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
have "ns ! 0 + offs_num (length ns) (x # xs) index key mi ma 0 \<le> ns ! ?i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! 0 + offs_num (length ns) (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma 0

goal (1 subgoal):
 1. ns ! 0 + offs_num (length ns) (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
by (rule_tac offs_pred_asc [OF B G E], simp_all add:
         offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! 0 + offs_num (length ns) (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ns ! 0 + offs_num (length ns) (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
have "0 < offs_num (length ns) (x # xs) index key mi ma 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma 0
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma 0

goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma 0
[PROOF STEP]
by (simp add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) (x # xs) index key mi ma 0

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ns ! 0 + offs_num (length ns) (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns ! 0 + offs_num (length ns) (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma 0

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
ns ! 0 + offs_num (length ns) (x # xs) index key mi ma 0 \<le> ns ! index key x (length ns) mi ma
0 < offs_num (length ns) (x # xs) index key mi ma 0
i < ns ! 0

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma \<noteq> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma \<noteq> i

goal (1 subgoal):
 1. \<lbrakk>0 < index key x (length ns) mi ma; 0 < offs_num (length ns) xs index key mi ma 0; i < ns ! 0\<rbrakk> \<Longrightarrow> (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
thus "(fill xs ?ns' index key ub mi ma)[ns ! ?i' := Some x] ! i = None"
[PROOF STATE]
proof (prove)
using this:
ns ! index key x (length ns) mi ma \<noteq> i

goal (1 subgoal):
 1. (fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None
[PROOF STEP]
proof simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
have "0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ?ns' ! 0 \<longrightarrow>
        fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma i \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by (simp add: offs_none_def)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
have "i < ?ns' ! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0
[PROOF STEP]
using G and I
[PROOF STATE]
proof (prove)
using this:
0 < index key x (length ns) mi ma
i < ns ! 0

goal (1 subgoal):
 1. i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma \<noteq> i \<Longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0
[PROOF STEP]
show "fill xs ?ns' index key ub mi ma ! i = None"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma 0 \<and> i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0 \<longrightarrow> fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
i < ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)] ! 0
0 < offs_num (length ns) xs index key mi ma 0

goal (1 subgoal):
 1. fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma ! i = None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(fill xs (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) index key ub mi ma)[ns ! index key x (length ns) mi ma := Some x] ! i = None

goal:
No subgoals!
[PROOF STEP]
qed