[STATEMENT]
lemma fill_index_none [rule_format]:
  assumes
    A: "index_less index key" and
    B: "key x \<in> {mi..ma}" and
    C: "ns \<noteq> []" and
    D: "offs_pred ns ub (x # xs) index key mi ma"
  shows "\<forall>x \<in> set xs. key x \<in> {mi..ma} \<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) = None"
  (is "_ \<Longrightarrow> fill _ ?ns' _ _ _ _ _ ! (_ ! ?i) = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. key x \<in> {mi..ma} \<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) = None
[PROOF STEP]
using A and B and C and D
[PROOF STATE]
proof (prove)
using this:
index_less index key
key x \<in> {mi..ma}
ns \<noteq> []
offs_pred ns ub (x # xs) index key mi ma

goal (1 subgoal):
 1. \<forall>x\<in>set xs. key x \<in> {mi..ma} \<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) = None
[PROOF STEP]
proof (rule_tac fill_none, simp_all, rule_tac offs_pred_cons,
 simp_all, simp add: index_less_def, cases "0 < ?i",
 cases "offs_set_prev ns (x # xs) index key mi ma ?i = {}",
 case_tac [3] "0 < offs_num (length ns) xs index key mi ma 0")
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 4. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
assume
    E: "0 < ?i" and
    F: "offs_set_prev ns (x # xs) index key mi ma ?i = {}"
[PROOF STATE]
proof (state)
this:
0 < index key x (length ns) mi ma
offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}

goal (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 4. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have G: "?i < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index key x (length ns) mi ma < length ns
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
index_less index key
key x \<in> {mi..ma}
ns \<noteq> []

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 (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 4. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence "offs_num (length ns) (x # xs) index key mi ma 0 = 0"
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma < length ns

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

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

goal (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 4. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence "offs_num (length ns) xs index key mi ma 0 = 0"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) (x # xs) index key mi ma 0 = 0

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

goal (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 4. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0

goal (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 4. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have "offs_next ?ns' ub xs index key mi ma 0 =
   (if 0 < offs_num (length ns) xs index key mi ma ?i
    then Suc (ns ! ?i)
    else offs_next ns ub (x # xs) index key mi ma ?i)"
[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 = (if 0 < offs_num (length ns) xs index key mi ma (index key x (length ns) mi ma) then Suc (ns ! index key x (length ns) mi ma) else offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma))
[PROOF STEP]
using E and F and G
[PROOF STATE]
proof (prove)
using this:
0 < index key x (length ns) mi ma
offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}
index key x (length ns) mi ma < length ns

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 = (if 0 < offs_num (length ns) xs index key mi ma (index key x (length ns) mi ma) then Suc (ns ! index key x (length ns) mi ma) else offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma))
[PROOF STEP]
by (rule_tac offs_next_zero_cons_neq, 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 = (if 0 < offs_num (length ns) xs index key mi ma (index key x (length ns) mi ma) then Suc (ns ! index key x (length ns) mi ma) else offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma))

goal (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 4. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence "ns ! ?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 0 = (if 0 < offs_num (length ns) xs index key mi ma (index key x (length ns) mi ma) then Suc (ns ! index key x (length ns) mi ma) else offs_next ns ub (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 < 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 split: if_split_asm, rule_tac offs_pred_next [OF D G], simp add:
     offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma < 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 (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) = {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 4. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma 0 = 0
ns ! index key x (length ns) mi ma < 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 "offs_none ?ns' ub xs index key mi ma (ns ! ?i)"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma 0 = 0
ns ! index key x (length ns) mi ma < 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_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (ns ! index key x (length ns) mi ma)
[PROOF STEP]
by (simp add: offs_none_def)
[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 (ns ! index key x (length ns) mi ma)

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
assume
    E: "0 < ?i" and
    F: "offs_set_prev ns (x # xs) index key mi ma ?i \<noteq> {}"
      (is "?A \<noteq> _")
[PROOF STATE]
proof (state)
this:
0 < index key x (length ns) mi ma
offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have G: "?i < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index key x (length ns) mi ma < length ns
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
index_less index key
key x \<in> {mi..ma}
ns \<noteq> []

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 (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have H: "Max ?A \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) \<in> offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}

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

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence I: "Max ?A < ?i"
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) \<in> offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)

goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < index key x (length ns) mi ma
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < index key x (length ns) mi ma

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have "Max ?A < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < length ns
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) \<in> offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)

goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < length ns
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < length ns

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < length ns

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have "0 < offs_num (length ns) (x # xs) index key mi ma (Max ?A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) \<in> offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)

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

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence "0 < offs_num (length ns) xs index key mi ma (Max ?A)"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))

goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < index key x (length ns) mi ma

goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))
[PROOF STEP]
by (subst (asm) offs_num_cons, split if_split_asm, simp_all)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have "ns ! Max ?A + offs_num (length ns) (x # xs)
    index key mi ma (Max ?A) \<le> ns ! ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) + offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
using G and H
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma < length ns
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) \<in> offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)

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

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence "?ns' ! Max ?A + offs_num (length ns) xs
    index key mi ma (Max ?A) \<le> ns ! ?i"
[PROOF STATE]
proof (prove)
using this:
ns ! Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) + offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma

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 (index key x (length ns) mi ma)) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
ns ! Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) + offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < index key x (length ns) mi ma

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 (index key x (length ns) mi ma)) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma
[PROOF STEP]
by (simp 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 (index key x (length ns) mi ma)) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[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 (index key x (length ns) mi ma)) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have "offs_next ?ns' ub xs index key mi ma (Max ?A) =
   (if 0 < offs_num (length ns) xs index key mi ma ?i
    then Suc (ns ! ?i)
    else offs_next ns ub (x # xs) index key mi ma ?i)"
[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 (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) = (if 0 < offs_num (length ns) xs index key mi ma (index key x (length ns) mi ma) then Suc (ns ! index key x (length ns) mi ma) else offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma))
[PROOF STEP]
using F and I
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < index key x (length ns) mi ma

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 (index key x (length ns) mi ma))) = (if 0 < offs_num (length ns) xs index key mi ma (index key x (length ns) mi ma) then Suc (ns ! index key x (length ns) mi ma) else offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma))
[PROOF STEP]
by (rule_tac offs_next_cons_neq, 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 (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) = (if 0 < offs_num (length ns) xs index key mi ma (index key x (length ns) mi ma) then Suc (ns ! index key x (length ns) mi ma) else offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma))

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence "ns ! ?i < offs_next ?ns' ub xs index key mi ma (Max ?A)"
[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 (index key x (length ns) mi ma))) = (if 0 < offs_num (length ns) xs index key mi ma (index key x (length ns) mi ma) then Suc (ns ! index key x (length ns) mi ma) else offs_next ns ub (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 < 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 (index key x (length ns) mi ma)))
[PROOF STEP]
by (simp split: if_split_asm, rule_tac offs_pred_next [OF D G], simp add:
     offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma < 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 (index key x (length ns) mi ma)))

goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 3. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < length ns
0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))
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 (index key x (length ns) mi ma)) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma
ns ! index key x (length ns) mi ma < 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 (index key x (length ns) mi ma)))
[PROOF STEP]
show "offs_none ?ns' ub xs index key mi ma (ns ! ?i)"
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)) < length ns
0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma)))
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 (index key x (length ns) mi ma)) + offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma (index key x (length ns) mi ma))) \<le> ns ! index key x (length ns) mi ma
ns ! index key x (length ns) mi ma < 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 (index key x (length ns) mi ma)))

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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
by (simp add: offs_none_def, blast)
[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 (ns ! index key x (length ns) mi ma)

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
assume "0 < offs_num (length ns) xs index key mi ma 0" and "\<not> 0 < ?i"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma 0
\<not> 0 < index key x (length ns) mi ma

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma 0
\<not> 0 < index key x (length ns) mi ma

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have "?i < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index key x (length ns) mi ma < length ns
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
index_less index key
key x \<in> {mi..ma}
ns \<noteq> []

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 (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
 2. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < offs_num (length ns) xs index key mi ma 0
\<not> 0 < index key x (length ns) mi ma
index key x (length ns) mi ma < length ns
[PROOF STEP]
show "offs_none ?ns' ub xs index key mi ma (ns ! ?i)"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma 0
\<not> 0 < index key x (length ns) mi ma
index key x (length ns) mi ma < length ns

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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
by (simp add: offs_none_def)
[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 (ns ! index key x (length ns) mi ma)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
assume
    E: "\<not> 0 < ?i" and
    F: "\<not> 0 < offs_num (length ns) xs index key mi ma 0"
[PROOF STATE]
proof (state)
this:
\<not> 0 < index key x (length ns) mi ma
\<not> 0 < offs_num (length ns) xs index key mi ma 0

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have G: "?i < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index key x (length ns) mi ma < length ns
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
index_less index key
key x \<in> {mi..ma}
ns \<noteq> []

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. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have "offs_num (length ns) xs index key mi ma 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma 0 = 0
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < offs_num (length ns) xs index key mi ma 0

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma 0 = 0

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
have "offs_next ?ns' ub xs index key mi ma ?i =
    offs_next ns ub (x # xs) index key mi ma ?i"
[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 (index key x (length ns) mi ma) = offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma)
[PROOF STEP]
using E and G
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < index key x (length ns) mi ma
index key x (length ns) mi ma < length ns

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 (index key x (length ns) mi ma) = offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma)
[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 (index key x (length ns) mi ma) = offs_next ns ub (x # xs) index key mi ma (index key x (length ns) mi ma)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence "ns ! ?i < offs_next ?ns' ub xs index key mi ma ?i"
[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 (index key x (length ns) mi ma) = offs_next ns ub (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 < 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 (index key x (length ns) mi ma)
[PROOF STEP]
by (simp, rule_tac offs_pred_next [OF D G], simp add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
ns ! index key x (length ns) mi ma < 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 (index key x (length ns) mi ma)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
hence "ns ! ?i < offs_next ?ns' ub xs index key mi ma 0"
[PROOF STATE]
proof (prove)
using this:
ns ! index key x (length ns) mi ma < 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 (index key x (length ns) mi ma)

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma < 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
[PROOF STATE]
proof (prove)
using this:
ns ! index key x (length ns) mi ma < 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 (index key x (length ns) mi ma)
\<not> 0 < index key x (length ns) mi ma

goal (1 subgoal):
 1. ns ! index key x (length ns) mi ma < 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:
ns ! index key x (length ns) mi ma < 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>\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; mi \<le> key x \<and> key x \<le> ma; index_less index key; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < index key x (length ns) mi ma; index_less index key; key x \<in> {mi..ma}; ns \<noteq> []; offs_pred ns ub (x # xs) index key mi ma; \<not> 0 < offs_num (length ns) xs index key mi ma 0\<rbrakk> \<Longrightarrow> 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 (ns ! index key x (length ns) mi ma)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma 0 = 0
ns ! index key x (length ns) mi ma < 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 "offs_none ?ns' ub xs index key mi ma (ns ! ?i)"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma 0 = 0
ns ! index key x (length ns) mi ma < 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_none (ns[index key x (length ns) mi ma := Suc (ns ! index key x (length ns) mi ma)]) ub xs index key mi ma (ns ! index key x (length ns) mi ma)
[PROOF STEP]
by (simp add: offs_none_def)
[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 (ns ! index key x (length ns) mi ma)

goal:
No subgoals!
[PROOF STEP]
qed