[STATEMENT]
lemma offs_next_cons_neq:
  assumes
    A: "index key x (length ns) mi ma = i" and
    B: "offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}" and
    C: "Max (offs_set_prev ns (x # xs) index key mi ma i) = j"
  shows "offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j =
    (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[i := Suc (ns ! i)]) ub xs index key mi ma j = (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 STEP]
proof (simp, rule conjI, rule_tac [!] impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma i \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)
 2. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
let ?A = "offs_set_next ns (x # xs) index key mi ma j"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma i \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)
 2. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
assume "0 < offs_num (length ns) xs index key mi ma i"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma i

goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma i \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)
 2. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
index key x (length ns) mi ma = i
0 < offs_num (length ns) xs index key mi ma i
[PROOF STEP]
have "offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = ?A"
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i
0 < offs_num (length ns) xs index key mi ma i

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

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

goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma i \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)
 2. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
have "0 < offs_num (length ns) (x # xs) index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma i
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i

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

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

goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i
[PROOF STEP]
using B and C
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma i
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}
Max (offs_set_prev ns (x # xs) index key mi ma i) = j

goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i
[PROOF STEP]
by (subst offs_next_prev, simp)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i

goal (2 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma i \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)
 2. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma j
0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i
[PROOF STEP]
show "offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j =
    Suc (ns ! i)"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma j
0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma j
0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)
[PROOF STEP]
by (simp only: offs_next_def, simp, subst nth_list_update_eq, blast,
     simp)
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
let ?A = "offs_set_prev ns (x # xs) index key mi ma i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
assume "offs_num (length ns) xs index key mi ma i = 0"
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma i = 0

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
index key x (length ns) mi ma = i
offs_num (length ns) xs index key mi ma i = 0
[PROOF STEP]
have "offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j =
    offs_set_next ns (x # xs) index key mi ma i"
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i
offs_num (length ns) xs index key mi ma i = 0

goal (1 subgoal):
 1. offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i
[PROOF STEP]
proof (rule_tac set_eqI, rule_tac iffI, simp_all add: offs_num_cons split:
   if_split_asm, rule_tac conjI, rule_tac notI, simp, rule_tac impI,
   (erule_tac [!] conjE)+, rule_tac ccontr, simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
have "i < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ns
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. i < length ns
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i < length ns

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

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
assume "i \<noteq> k" and "\<not> i < k"
[PROOF STATE]
proof (state)
this:
i \<noteq> k
\<not> i < k

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
hence "k < i"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> k
\<not> i < k

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

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < i

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
assume "0 < offs_num (length ns) xs index key mi ma k"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma k

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i < length ns
k < i
0 < offs_num (length ns) xs index key mi ma k
[PROOF STEP]
have "k \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
i < length ns
k < i
0 < offs_num (length ns) xs index key mi ma k

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

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
hence "k \<le> Max ?A"
[PROOF STATE]
proof (prove)
using this:
k \<in> offs_set_prev ns (x # xs) index key mi ma i

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

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
assume "j < k"
[PROOF STATE]
proof (state)
this:
j < k

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<noteq> xa; xa < length ns; j < xa; 0 < offs_num (length ns) xs index key mi ma xa; \<not> i < xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)
j < k
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
k \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)
j < k

goal (1 subgoal):
 1. False
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
k \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)
j < k
Max (offs_set_prev ns (x # xs) index key mi ma i) = j

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
have "Max ?A \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_prev ns (x # xs) index key mi ma i
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
hence "j < i"
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_prev ns (x # xs) index key mi ma i

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

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < i

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < length ns; i < xa; 0 < offs_num (length ns) xs index key mi ma xa; index key x (length ns) mi ma = i; offs_num (length ns) xs index key mi ma i = 0\<rbrakk> \<Longrightarrow> j < xa
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < i
i < k
[PROOF STEP]
show "j < k"
[PROOF STATE]
proof (prove)
using this:
j < i
i < k

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

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

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma i = 0 \<Longrightarrow> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
with B
[PROOF STATE]
proof (chain)
picking this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}
offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i
[PROOF STEP]
show "offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j =
    offs_next ns ub (x # xs) index key mi ma i"
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}
offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
proof (simp only: offs_next_def split: if_split, (rule_tac conjI, rule_tac [!] impI,
   simp)+, subst nth_list_update, blast, simp (no_asm_simp))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_next ns (x # xs) index key mi ma i \<noteq> {}; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_next ns (x # xs) index key mi ma i \<noteq> {}; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> i \<noteq> Min (offs_set_next ns (x # xs) index key mi ma i)
[PROOF STEP]
assume "offs_set_next ns (x # xs) index key mi ma i \<noteq> {}"
[PROOF STATE]
proof (state)
this:
offs_set_next ns (x # xs) index key mi ma i \<noteq> {}

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

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

goal (1 subgoal):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_next ns (x # xs) index key mi ma i \<noteq> {}; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_next ns (x # xs) index key mi ma i \<noteq> {}; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i; offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}; offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j = offs_set_next ns (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> i \<noteq> Min (offs_set_next ns (x # xs) index key mi ma i)
[PROOF STEP]
thus "i \<noteq> Min (offs_set_next ns (x # xs) index key mi ma i)"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma i) \<in> offs_set_next ns (x # xs) index key mi ma i

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_pred_ub_aux [rule_format]:
  assumes A: "offs_pred ns ub xs index key mi ma"
  shows "i < length ns \<Longrightarrow>
    \<forall>j < length ns. i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow>
      ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ns \<Longrightarrow> \<forall>j<length ns. i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
proof (erule strict_inc_induct, rule_tac [!] allI, (rule_tac [!] impI)+,
 drule le_less_Suc_eq, simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
assume B: "length ns = Suc i"
[PROOF STATE]
proof (state)
this:
length ns = Suc i

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
hence "offs_num (Suc i) xs index key mi ma i \<le>
    offs_next ns ub xs index key mi ma i - ns ! i"
[PROOF STATE]
proof (prove)
using this:
length ns = Suc i

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

goal (1 subgoal):
 1. offs_num (Suc i) xs index key mi ma i \<le> offs_next ns ub xs index key mi ma i - ns ! i
[PROOF STEP]
by (simp add: offs_pred_def)
[PROOF STATE]
proof (state)
this:
offs_num (Suc i) xs index key mi ma i \<le> offs_next ns ub xs index key mi ma i - ns ! i

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (Suc i) xs index key mi ma i \<le> offs_next ns ub xs index key mi ma i - ns ! i

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
have "offs_next ns ub xs index key mi ma i = ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub xs index key mi ma i = ub
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
length ns = Suc i

goal (1 subgoal):
 1. offs_next ns ub xs index key mi ma i = ub
[PROOF STEP]
by (simp add: offs_next_def)
[PROOF STATE]
proof (state)
this:
offs_next ns ub xs index key mi ma i = ub

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (Suc i) xs index key mi ma i \<le> offs_next ns ub xs index key mi ma i - ns ! i
offs_next ns ub xs index key mi ma i = ub
[PROOF STEP]
have "offs_num (Suc i) xs index key mi ma i \<le> ub - ns ! i"
[PROOF STATE]
proof (prove)
using this:
offs_num (Suc i) xs index key mi ma i \<le> offs_next ns ub xs index key mi ma i - ns ! i
offs_next ns ub xs index key mi ma i = ub

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

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (Suc i) xs index key mi ma i \<le> ub - ns ! i

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
assume "0 < offs_num (Suc i) xs index key mi ma i"
[PROOF STATE]
proof (state)
this:
0 < offs_num (Suc i) xs index key mi ma i

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>length ns = Suc i; j = i; 0 < offs_num (Suc i) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub
 2. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (Suc i) xs index key mi ma i \<le> ub - ns ! i
0 < offs_num (Suc i) xs index key mi ma i
[PROOF STEP]
show "ns ! i + offs_num (Suc i) xs index key mi ma i \<le> ub"
[PROOF STATE]
proof (prove)
using this:
offs_num (Suc i) xs index key mi ma i \<le> ub - ns ! i
0 < offs_num (Suc i) xs index key mi ma i

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
assume "j < length ns"
[PROOF STATE]
proof (state)
this:
j < length ns

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
hence "offs_num (length ns) xs index key mi ma j \<le>
    offs_next ns ub xs index key mi ma j - ns ! j"
[PROOF STATE]
proof (prove)
using this:
j < length ns

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
j < length ns
offs_pred ns ub xs index key mi ma

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j
[PROOF STEP]
by (simp add: offs_pred_def)
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
assume
    B: "\<forall>k < length ns. Suc i \<le> k \<longrightarrow>
      0 < offs_num (length ns) xs index key mi ma k \<longrightarrow>
      ns ! k + offs_num (length ns) xs index key mi ma k \<le> ub" and
    C: "i \<le> j"
[PROOF STATE]
proof (state)
this:
\<forall>k<length ns. Suc i \<le> k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! k + offs_num (length ns) xs index key mi ma k \<le> ub
i \<le> j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
have "offs_next ns ub xs index key mi ma j \<le> ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub xs index key mi ma j \<le> ub
[PROOF STEP]
proof (simp only: offs_next_def split: if_split, rule conjI, simp, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ub
[PROOF STEP]
let ?A = "offs_set_next ns xs index key mi ma j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ub
[PROOF STEP]
assume "?A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
offs_set_next ns xs index key mi ma j \<noteq> {}

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

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

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

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns xs index key mi ma j) + offs_num (length ns) xs index key mi ma (Min (offs_set_next ns xs index key mi ma j)) \<le> ub
[PROOF STEP]
using B and C
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns xs index key mi ma j) \<in> offs_set_next ns xs index key mi ma j
\<forall>k<length ns. Suc i \<le> k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! k + offs_num (length ns) xs index key mi ma k \<le> ub
i \<le> j

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs_next ns ub xs index key mi ma j \<le> ub

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j
offs_next ns ub xs index key mi ma j \<le> ub
[PROOF STEP]
have "offs_num (length ns) xs index key mi ma j \<le> ub - ns ! j"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j
offs_next ns ub xs index key mi ma j \<le> ub

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma j \<le> ub - ns ! j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
assume "0 < offs_num (length ns) xs index key mi ma j"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<forall>j<length ns. Suc i \<le> j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub; j < length ns; i \<le> j; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma j \<le> ub - ns ! j
0 < offs_num (length ns) xs index key mi ma j
[PROOF STEP]
show "ns ! j + offs_num (length ns) xs index key mi ma j \<le> ub"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma j \<le> ub - ns ! j
0 < offs_num (length ns) xs index key mi ma j

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_pred_ub:
 "\<lbrakk>offs_pred ns ub xs index key mi ma; i < length ns;
   0 < offs_num (length ns) xs index key mi ma i\<rbrakk> \<Longrightarrow>
     ns ! i + offs_num (length ns) xs index key mi ma i \<le> ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>offs_pred ns ub xs index key mi ma; i < length ns; 0 < offs_num (length ns) xs index key mi ma i\<rbrakk> \<Longrightarrow> ns ! i + offs_num (length ns) xs index key mi ma i \<le> ub
[PROOF STEP]
by (drule offs_pred_ub_aux, assumption+, simp)


[STATEMENT]
lemma offs_pred_asc_aux [rule_format]:
  assumes A: "offs_pred ns ub xs index key mi ma"
  shows "i < length ns \<Longrightarrow>
    \<forall>j k. k < length ns \<longrightarrow> i \<le> j \<longrightarrow> j < k \<longrightarrow>
      0 < offs_num (length ns) xs index key mi ma j \<longrightarrow>
      0 < offs_num (length ns) xs index key mi ma k \<longrightarrow>
      ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ns \<Longrightarrow> \<forall>j k. k < length ns \<longrightarrow> i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
proof (erule strict_inc_induct, simp, (rule allI)+, (rule impI)+, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
fix i j k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
assume
    B: "k < length ns" and
    C: "j < k"
[PROOF STATE]
proof (state)
this:
k < length ns
j < k

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
hence "j < length ns"
[PROOF STATE]
proof (prove)
using this:
k < length ns
j < k

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

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
hence "offs_num (length ns) xs index key mi ma j \<le>
    offs_next ns ub xs index key mi ma j - ns ! j"
[PROOF STATE]
proof (prove)
using this:
j < length ns

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
j < length ns
offs_pred ns ub xs index key mi ma

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j
[PROOF STEP]
by (simp add: offs_pred_def)
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
assume
    D: "\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow>
      0 < offs_num (length ns) xs index key mi ma j \<longrightarrow>
      0 < offs_num (length ns) xs index key mi ma k \<longrightarrow>
      ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k" and
    E: "i \<le> j" and
    F: "0 < offs_num (length ns) xs index key mi ma k"
[PROOF STATE]
proof (state)
this:
\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
i \<le> j
0 < offs_num (length ns) xs index key mi ma k

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
have "offs_next ns ub xs index key mi ma j \<le> ns ! k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub xs index key mi ma j \<le> ns ! k
[PROOF STEP]
proof (simp only: offs_next_def split: if_split, rule conjI, rule_tac [!] impI,
   rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x>j. x < length ns \<longrightarrow> offs_num (length ns) xs index key mi ma x = 0; \<not> ub \<le> ns ! k\<rbrakk> \<Longrightarrow> False
 2. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
assume "\<forall>n > j. n < length ns \<longrightarrow>
      offs_num (length ns) xs index key mi ma n = 0"
[PROOF STATE]
proof (state)
this:
\<forall>n>j. n < length ns \<longrightarrow> offs_num (length ns) xs index key mi ma n = 0

goal (2 subgoals):
 1. \<lbrakk>\<forall>x>j. x < length ns \<longrightarrow> offs_num (length ns) xs index key mi ma x = 0; \<not> ub \<le> ns ! k\<rbrakk> \<Longrightarrow> False
 2. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
hence "offs_num (length ns) xs index key mi ma k = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>n>j. n < length ns \<longrightarrow> offs_num (length ns) xs index key mi ma n = 0

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma k = 0
[PROOF STEP]
using B and C
[PROOF STATE]
proof (prove)
using this:
\<forall>n>j. n < length ns \<longrightarrow> offs_num (length ns) xs index key mi ma n = 0
k < length ns
j < k

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

goal (2 subgoals):
 1. \<lbrakk>\<forall>x>j. x < length ns \<longrightarrow> offs_num (length ns) xs index key mi ma x = 0; \<not> ub \<le> ns ! k\<rbrakk> \<Longrightarrow> False
 2. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma k = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma k = 0
0 < offs_num (length ns) xs index key mi ma k

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
let ?A = "offs_set_next ns xs index key mi ma j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
have G: "k \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> offs_set_next ns xs index key mi ma j
[PROOF STEP]
using B and C and F
[PROOF STATE]
proof (prove)
using this:
k < length ns
j < k
0 < offs_num (length ns) xs index key mi ma k

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

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

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
hence "Min ?A < k \<or> Min ?A = k"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns xs index key mi ma j) \<le> k

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns xs index key mi ma j) < k \<or> Min (offs_set_next ns xs index key mi ma j) = k

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns xs index key mi ma j) < k \<or> Min (offs_set_next ns xs index key mi ma j) = k

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
have "Suc i \<le> Min ?A \<longrightarrow> Min ?A < k \<longrightarrow>
        0 < offs_num (length ns) xs index key mi ma (Min ?A) \<longrightarrow>
        ns ! Min ?A + offs_num (length ns) xs index key mi ma (Min ?A) \<le> ns ! k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc i \<le> Min (offs_set_next ns xs index key mi ma j) \<longrightarrow> Min (offs_set_next ns xs index key mi ma j) < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_next ns xs index key mi ma j)) \<longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) + offs_num (length ns) xs index key mi ma (Min (offs_set_next ns xs index key mi ma j)) \<le> ns ! k
[PROOF STEP]
using B and D and F
[PROOF STATE]
proof (prove)
using this:
k < length ns
\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
0 < offs_num (length ns) xs index key mi ma k

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Suc i \<le> Min (offs_set_next ns xs index key mi ma j) \<longrightarrow> Min (offs_set_next ns xs index key mi ma j) < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_next ns xs index key mi ma j)) \<longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) + offs_num (length ns) xs index key mi ma (Min (offs_set_next ns xs index key mi ma j)) \<le> ns ! k

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
assume "Min ?A < k"
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns xs index key mi ma j) < k

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

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

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

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

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

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns xs index key mi ma j) < k \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) < ns ! k

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns xs index key mi ma j) < k \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) < ns ! k

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
assume "Min ?A = k"
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns xs index key mi ma j) = k

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
hence "ns ! Min ?A = ns ! k"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns xs index key mi ma j) = k

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns xs index key mi ma j) = ns ! k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns ! Min (offs_set_next ns xs index key mi ma j) = ns ! k

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns xs index key mi ma j) = k \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) = ns ! k

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma j \<noteq> {} \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next ns xs index key mi ma j) < k \<or> Min (offs_set_next ns xs index key mi ma j) = k
Min (offs_set_next ns xs index key mi ma j) < k \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) < ns ! k
Min (offs_set_next ns xs index key mi ma j) = k \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) = ns ! k
[PROOF STEP]
show "ns ! Min ?A \<le> ns ! k"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns xs index key mi ma j) < k \<or> Min (offs_set_next ns xs index key mi ma j) = k
Min (offs_set_next ns xs index key mi ma j) < k \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) < ns ! k
Min (offs_set_next ns xs index key mi ma j) = k \<Longrightarrow> ns ! Min (offs_set_next ns xs index key mi ma j) = ns ! k

goal (1 subgoal):
 1. ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k
[PROOF STEP]
by (simp add: le_less, blast)
[PROOF STATE]
proof (state)
this:
ns ! Min (offs_set_next ns xs index key mi ma j) \<le> ns ! k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs_next ns ub xs index key mi ma j \<le> ns ! k

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j
offs_next ns ub xs index key mi ma j \<le> ns ! k
[PROOF STEP]
have "offs_num (length ns) xs index key mi ma j \<le> ns ! k - ns ! j"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub xs index key mi ma j - ns ! j
offs_next ns ub xs index key mi ma j \<le> ns ! k

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

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma j \<le> ns ! k - ns ! j

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
assume "0 < offs_num (length ns) xs index key mi ma j"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma j

goal (1 subgoal):
 1. \<And>i j k. \<lbrakk>\<forall>j k. k < length ns \<longrightarrow> Suc i \<le> j \<longrightarrow> j < k \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<longrightarrow> 0 < offs_num (length ns) xs index key mi ma k \<longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k; k < length ns; i \<le> j; j < k; 0 < offs_num (length ns) xs index key mi ma j; 0 < offs_num (length ns) xs index key mi ma k\<rbrakk> \<Longrightarrow> ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma j \<le> ns ! k - ns ! j
0 < offs_num (length ns) xs index key mi ma j
[PROOF STEP]
show "ns ! j + offs_num (length ns) xs index key mi ma j \<le> ns ! k"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma j \<le> ns ! k - ns ! j
0 < offs_num (length ns) xs index key mi ma j

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_pred_asc:
 "\<lbrakk>offs_pred ns ub xs index key mi ma; i < j; j < length ns;
   0 < offs_num (length ns) xs index key mi ma i;
   0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow>
     ns ! i + offs_num (length ns) xs index key mi ma i \<le> ns ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>offs_pred ns ub xs index key mi ma; i < j; j < length ns; 0 < offs_num (length ns) xs index key mi ma i; 0 < offs_num (length ns) xs index key mi ma j\<rbrakk> \<Longrightarrow> ns ! i + offs_num (length ns) xs index key mi ma i \<le> ns ! j
[PROOF STEP]
by (drule offs_pred_asc_aux, erule less_trans, assumption+, rule order_refl)


[STATEMENT]
lemma offs_pred_next:
  assumes
    A: "offs_pred ns ub xs index key mi ma" and
    B: "i < length ns" and
    C: "0 < offs_num (length ns) xs index key mi ma i"
  shows "ns ! i < offs_next ns ub xs index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! i < offs_next ns ub xs index key mi ma i
[PROOF STEP]
proof (simp only: offs_next_def split: if_split, rule conjI, rule_tac [!] impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. offs_set_next ns xs index key mi ma i = {} \<Longrightarrow> ns ! i < ub
 2. offs_set_next ns xs index key mi ma i \<noteq> {} \<Longrightarrow> ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)
[PROOF STEP]
have "ns ! i + offs_num (length ns) xs index key mi ma i \<le> ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! i + offs_num (length ns) xs index key mi ma i \<le> ub
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
offs_pred ns ub xs index key mi ma
i < length ns
0 < offs_num (length ns) xs index key mi ma i

goal (1 subgoal):
 1. ns ! i + offs_num (length ns) xs index key mi ma i \<le> ub
[PROOF STEP]
by (rule offs_pred_ub)
[PROOF STATE]
proof (state)
this:
ns ! i + offs_num (length ns) xs index key mi ma i \<le> ub

goal (2 subgoals):
 1. offs_set_next ns xs index key mi ma i = {} \<Longrightarrow> ns ! i < ub
 2. offs_set_next ns xs index key mi ma i \<noteq> {} \<Longrightarrow> ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)
[PROOF STEP]
thus "ns ! i < ub"
[PROOF STATE]
proof (prove)
using this:
ns ! i + offs_num (length ns) xs index key mi ma i \<le> ub

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

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma i \<noteq> {} \<Longrightarrow> ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma i \<noteq> {} \<Longrightarrow> ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)
[PROOF STEP]
assume "offs_set_next ns xs index key mi ma i \<noteq> {}"
[PROOF STATE]
proof (state)
this:
offs_set_next ns xs index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma i \<noteq> {} \<Longrightarrow> ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)
[PROOF STEP]
hence "Min (offs_set_next ns xs index key mi ma i)
    \<in> offs_set_next ns xs index key mi ma i"
[PROOF STATE]
proof (prove)
using this:
offs_set_next ns xs index key mi ma i \<noteq> {}

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma i \<noteq> {} \<Longrightarrow> ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)
[PROOF STEP]
hence "ns ! i + offs_num (length ns) xs index key mi ma i \<le>
    ns ! Min (offs_set_next ns xs index key mi ma i)"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns xs index key mi ma i) \<in> offs_set_next ns xs index key mi ma i

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

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

goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma i \<noteq> {} \<Longrightarrow> ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)
[PROOF STEP]
thus "ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)"
[PROOF STATE]
proof (prove)
using this:
ns ! i + offs_num (length ns) xs index key mi ma i \<le> ns ! Min (offs_set_next ns xs index key mi ma i)

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

goal (1 subgoal):
 1. ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns ! i < ns ! Min (offs_set_next ns xs index key mi ma i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_pred_next_cons_less:
  assumes
    A: "offs_pred ns ub (x # xs) index key mi ma" and
    B: "index key x (length ns) mi ma = i" and
    C: "offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}" and
    D: "Max (offs_set_prev ns (x # xs) index key mi ma i) = j"
  shows "offs_next ns ub (x # xs) index key mi ma j <
    offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j"
  (is "?M < ?N")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
have E: "0 < offs_num (length ns) (x # xs) index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma i
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i

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

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
hence "0 < offs_num (length ns) (x # xs) index key mi ma j \<and>
    offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and>
    Min (offs_set_next ns (x # xs) index key mi ma j) = i"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma i

goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i
[PROOF STEP]
using C and D
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma i
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}
Max (offs_set_prev ns (x # xs) index key mi ma i) = j

goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i
[PROOF STEP]
by (subst offs_next_prev, simp)
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
hence F: "?M = ns ! i"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma j \<and> offs_set_next ns (x # xs) index key mi ma j \<noteq> {} \<and> Min (offs_set_next ns (x # xs) index key mi ma j) = i

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

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
have "?N = (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[i := Suc (ns ! i)]) ub xs index key mi ma j = (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 STEP]
using B and C and D
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}
Max (offs_set_prev ns (x # xs) index key mi ma i) = j

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = (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 STEP]
by (rule offs_next_cons_neq)
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = (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)

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = (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)

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
proof (split if_split_asm)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma i; offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
 2. \<lbrakk>\<not> 0 < offs_num (length ns) xs index key mi ma i; offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
assume "?N = Suc (ns ! i)"
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = Suc (ns ! i)

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<not> 0 < offs_num (length ns) xs index key mi ma i; offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> 0 < offs_num (length ns) xs index key mi ma i; offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
assume "?N = offs_next ns ub (x # xs) index key mi ma i"
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma i

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

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

goal (1 subgoal):
 1. ns ! i < offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
by (rule_tac offs_pred_next [OF A _ E], blast)
[PROOF STATE]
proof (state)
this:
ns ! i < offs_next ns ub (x # xs) index key mi ma i

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_pred_next_cons:
  assumes
    A: "offs_pred ns ub (x # xs) index key mi ma" and
    B: "index key x (length ns) mi ma = i" and
    C: "i < length ns" and
    D: "0 < offs_num (length ns) (x # xs) index key mi ma j"
  shows "offs_next ns ub (x # xs) index key mi ma j \<le>
    offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j"
  (is "?M \<le> ?N")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
let ?P = "offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and>
    Max (offs_set_prev ns (x # xs) index key mi ma i) = j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
have "?P \<or> \<not> ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<or> \<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<or> \<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j)

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<or> \<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j)

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<or> \<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j)

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
assume ?P
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
hence "?M < ?N"
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j

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

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
by (rule_tac offs_pred_next_cons_less [OF A], simp_all)
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma j < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j

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

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

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
assume "\<not> ?P"
[PROOF STATE]
proof (state)
this:
\<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j)

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
hence "?N = ?M"
[PROOF STATE]
proof (prove)
using this:
\<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j)

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma j
[PROOF STEP]
by (rule_tac offs_next_cons_eq [OF B C D], blast)
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = offs_next ns ub (x # xs) index key mi ma j

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

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

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j) \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<or> \<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j)
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
\<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j) \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<or> \<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j)
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j
\<not> (offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<and> Max (offs_set_prev ns (x # xs) index key mi ma i) = j) \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j

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

goal:
No subgoals!
[PROOF STEP]
qed