[STATEMENT]
lemma offs_next_prev:
 "(0 < offs_num (length ns) xs index key mi ma i \<and>
    offs_set_next ns xs index key mi ma i \<noteq> {} \<and>
    Min (offs_set_next ns xs index key mi ma i) = j) =
  (0 < offs_num (length ns) xs index key mi ma j \<and>
    offs_set_prev ns xs index key mi ma j \<noteq> {} \<and>
    Max (offs_set_prev ns xs index key mi ma j) = i)"
  (is "?P = ?Q")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j) = (0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i)
[PROOF STEP]
proof (rule iffI, (erule_tac [!] conjE)+)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma i; offs_set_next ns xs index key mi ma i \<noteq> {}; Min (offs_set_next ns xs index key mi ma i) = j\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i
 2. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
let ?A = "offs_set_next ns xs index key mi ma i"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma i; offs_set_next ns xs index key mi ma i \<noteq> {}; Min (offs_set_next ns xs index key mi ma i) = j\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i
 2. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
let ?B = "offs_set_prev ns xs index key mi ma j"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma i; offs_set_next ns xs index key mi ma i \<noteq> {}; Min (offs_set_next ns xs index key mi ma i) = j\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i
 2. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
assume
    A: "0 < offs_num (length ns) xs index key mi ma i" and
    B: "?A \<noteq> {}" and
    C: "Min ?A = j"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma i
offs_set_next ns xs index key mi ma i \<noteq> {}
Min (offs_set_next ns xs index key mi ma i) = j

goal (2 subgoals):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma i; offs_set_next ns xs index key mi ma i \<noteq> {}; Min (offs_set_next ns xs index key mi ma i) = j\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i
 2. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[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 i) \<in> offs_set_next ns xs index key mi ma i
[PROOF STEP]
using B
[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 (2 subgoals):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma i; offs_set_next ns xs index key mi ma i \<noteq> {}; Min (offs_set_next ns xs index key mi ma i) = j\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i
 2. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
hence D: "j \<in> ?A"
[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. j \<in> 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
Min (offs_set_next ns xs index key mi ma i) = j

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

goal (2 subgoals):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma i; offs_set_next ns xs index key mi ma i \<noteq> {}; Min (offs_set_next ns xs index key mi ma i) = j\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i
 2. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
hence E: "i \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next ns xs index key mi ma i

goal (1 subgoal):
 1. i \<in> offs_set_prev ns xs index key mi ma j
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
j \<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. i \<in> offs_set_prev ns xs index key mi ma j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<in> offs_set_prev ns xs index key mi ma j

goal (2 subgoals):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma i; offs_set_next ns xs index key mi ma i \<noteq> {}; Min (offs_set_next ns xs index key mi ma i) = j\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i
 2. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
show ?Q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i
[PROOF STEP]
proof (rule conjI, rule_tac [2] conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma j
 2. offs_set_prev ns xs index key mi ma j \<noteq> {}
 3. Max (offs_set_prev ns xs index key mi ma j) = i
[PROOF STEP]
show "0 < offs_num (length ns) xs index key mi ma j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma j
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next ns xs index key mi ma i

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

goal (2 subgoals):
 1. offs_set_prev ns xs index key mi ma j \<noteq> {}
 2. Max (offs_set_prev ns xs index key mi ma j) = i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. offs_set_prev ns xs index key mi ma j \<noteq> {}
 2. Max (offs_set_prev ns xs index key mi ma j) = i
[PROOF STEP]
show "?B \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_set_prev ns xs index key mi ma j \<noteq> {}
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
i \<in> offs_set_prev ns xs index key mi ma j

goal (1 subgoal):
 1. offs_set_prev ns xs index key mi ma j \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
offs_set_prev ns xs index key mi ma j \<noteq> {}

goal (1 subgoal):
 1. Max (offs_set_prev ns xs index key mi ma j) = i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Max (offs_set_prev ns xs index key mi ma j) = i
[PROOF STEP]
from E
[PROOF STATE]
proof (chain)
picking this:
i \<in> offs_set_prev ns xs index key mi ma j
[PROOF STEP]
show "Max ?B = i"
[PROOF STATE]
proof (prove)
using this:
i \<in> offs_set_prev ns xs index key mi ma j

goal (1 subgoal):
 1. Max (offs_set_prev ns xs index key mi ma j) = i
[PROOF STEP]
proof (subst Max_eq_iff, simp, blast, simp, rule_tac allI, rule_tac impI,
     (erule_tac conjE)+, rule_tac ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>j < length ns; a < j; 0 < offs_num (length ns) xs index key mi ma a; 0 < offs_num (length ns) xs index key mi ma i; \<not> a \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>j < length ns; a < j; 0 < offs_num (length ns) xs index key mi ma a; 0 < offs_num (length ns) xs index key mi ma i; \<not> a \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume F: "k < j" and "j < length ns"
[PROOF STATE]
proof (state)
this:
k < j
j < length ns

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

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

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

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

goal (1 subgoal):
 1. \<And>a. \<lbrakk>j < length ns; a < j; 0 < offs_num (length ns) xs index key mi ma a; 0 < offs_num (length ns) xs index key mi ma i; \<not> a \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < length ns
\<not> k \<le> i
0 < offs_num (length ns) xs index key mi ma k
[PROOF STEP]
have "k \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
k < length ns
\<not> k \<le> i
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 i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k \<in> offs_set_next ns xs index key mi ma i

goal (1 subgoal):
 1. \<And>a. \<lbrakk>j < length ns; a < j; 0 < offs_num (length ns) xs index key mi ma a; 0 < offs_num (length ns) xs index key mi ma i; \<not> a \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "Min ?A \<le> k"
[PROOF STATE]
proof (prove)
using this:
k \<in> offs_set_next ns xs index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next ns xs index key mi ma i) \<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 i) \<le> k

goal (1 subgoal):
 1. \<And>a. \<lbrakk>j < length ns; a < j; 0 < offs_num (length ns) xs index key mi ma a; 0 < offs_num (length ns) xs index key mi ma i; \<not> a \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns xs index key mi ma i) \<le> k

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma j \<and> offs_set_prev ns xs index key mi ma j \<noteq> {} \<and> Max (offs_set_prev ns xs index key mi ma j) = i

goal (1 subgoal):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
let ?A = "offs_set_prev ns xs index key mi ma j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
let ?B = "offs_set_next ns xs index key mi ma i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
assume
    A: "0 < offs_num (length ns) xs index key mi ma j" and
    B: "?A \<noteq> {}" and
    C: "Max ?A = i"
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma j
offs_set_prev ns xs index key mi ma j \<noteq> {}
Max (offs_set_prev ns xs index key mi ma j) = i

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

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

goal (1 subgoal):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
hence D: "i \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns xs index key mi ma j) \<in> offs_set_prev ns xs index key mi ma j

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

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

goal (1 subgoal):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
hence E: "j \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
i \<in> offs_set_prev ns xs index key mi ma j

goal (1 subgoal):
 1. j \<in> offs_set_next ns xs index key mi ma i
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
i \<in> offs_set_prev ns xs index key mi ma j
0 < offs_num (length ns) xs index key mi ma j

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

goal (1 subgoal):
 1. \<lbrakk>0 < offs_num (length ns) xs index key mi ma j; offs_set_prev ns xs index key mi ma j \<noteq> {}; Max (offs_set_prev ns xs index key mi ma j) = i\<rbrakk> \<Longrightarrow> 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
proof (rule conjI, rule_tac [2] conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 < offs_num (length ns) xs index key mi ma i
 2. offs_set_next ns xs index key mi ma i \<noteq> {}
 3. Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
show "0 < offs_num (length ns) xs index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
i \<in> offs_set_prev ns xs index key mi ma j

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

goal (2 subgoals):
 1. offs_set_next ns xs index key mi ma i \<noteq> {}
 2. Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. offs_set_next ns xs index key mi ma i \<noteq> {}
 2. Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
show "?B \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma i \<noteq> {}
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
j \<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> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
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) = j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
from E
[PROOF STATE]
proof (chain)
picking this:
j \<in> offs_set_next ns xs index key mi ma i
[PROOF STEP]
show "Min ?B = j"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_next ns xs index key mi ma i

goal (1 subgoal):
 1. Min (offs_set_next ns xs index key mi ma i) = j
[PROOF STEP]
proof (subst Min_eq_iff, simp, blast, simp, rule_tac allI, rule_tac impI,
     (erule_tac conjE)+, rule_tac ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < x; 0 < offs_num (length ns) xs index key mi ma x; \<not> j \<le> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>j < length ns; 0 < offs_num (length ns) xs index key mi ma j; i < x; 0 < offs_num (length ns) xs index key mi ma x; \<not> j \<le> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume
       "j < length ns" and
       "\<not> j \<le> k" and
       "0 < offs_num (length ns) xs index key mi ma k"
[PROOF STATE]
proof (state)
this:
j < length ns
\<not> j \<le> k
0 < offs_num (length ns) xs index key mi ma k

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) xs index key mi ma i \<and> offs_set_next ns xs index key mi ma i \<noteq> {} \<and> Min (offs_set_next ns xs index key mi ma i) = j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_next_cons_eq:
  assumes
    A: "index key x (length ns) mi ma = i" and
    B: "i < length ns" and
    C: "0 < offs_num (length ns) (x # xs) index key mi ma j"
  shows
   "offs_set_prev ns (x # xs) index key mi ma i = {} \<or>
      Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j \<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 j"
  (is "?P \<or> ?Q \<Longrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_set_prev ns (x # xs) index key mi ma i = {} \<or> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j \<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 j
[PROOF STEP]
proof (simp only: disj_imp, cases "j < i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
let ?A = "offs_set_prev ns (x # xs) index key mi ma i"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
let ?B = "offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
let ?C = "offs_set_next ns (x # xs) index key mi ma j"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j < i

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence D: "j \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
j < i

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

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence "j \<le> Max ?A"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_prev ns (x # xs) index key mi ma i

goal (1 subgoal):
 1. j \<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:
j \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
assume "\<not> ?P \<longrightarrow> ?Q"
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence ?Q
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j

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

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)
Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j
[PROOF STEP]
have E: "j < Max ?A"
[PROOF STATE]
proof (prove)
using this:
j \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)
Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
have F: "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 D
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_prev ns (x # xs) index key mi ma i

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, blast)
[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 (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
have G: "Max ?A \<in> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j
[PROOF STEP]
proof (simp, rule conjI, rule_tac [2] conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Max (offs_set_prev ns (x # xs) index key mi ma i) < length ns
 2. j < Max (offs_set_prev ns (x # xs) index key mi ma i)
 3. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
show "Max ?A < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma i) < length ns
[PROOF STEP]
using F
[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. Max (offs_set_prev ns (x # xs) index key mi ma i) < length ns
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma i) < length ns

goal (2 subgoals):
 1. j < Max (offs_set_prev ns (x # xs) index key mi ma i)
 2. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j < Max (offs_set_prev ns (x # xs) index key mi ma i)
 2. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
show "j < Max ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < Max (offs_set_prev ns (x # xs) index key mi ma i)
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
j < Max (offs_set_prev ns (x # xs) index key mi ma i)

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

goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
have "0 < offs_num (length ns) (x # xs) index key mi ma (Max ?A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
using F
[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. 0 < offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))

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

goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
have "Max ?A < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
using F
[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. Max (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma i) < i

goal (1 subgoal):
 1. 0 < offs_num (length ns) xs index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
Max (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
show "0 < offs_num (length ns) xs index key mi ma (Max ?A)"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) (x # xs) index key mi ma (Max (offs_set_prev ns (x # xs) index key mi ma i))
Max (offs_set_prev ns (x # xs) index key mi ma i) < i

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

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

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence H: "offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j =
    ns[i := Suc (ns ! i)] ! Min ?B"
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
have "Min ?B \<le> Max ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
have "Max ?A < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
using F
[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. Max (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Max (offs_set_prev ns (x # xs) index key mi ma i) < i

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)
Max (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
have I: "Min ?B < i"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<le> Max (offs_set_prev ns (x # xs) index key mi ma i)
Max (offs_set_prev ns (x # xs) index key mi ma i) < i

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence J: "offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j =
    ns ! Min ?B"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) 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 = ns ! Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j)
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) < i
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = ns[i := Suc (ns ! i)] ! Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j)

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
have "Min ?B \<in> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j
[PROOF STEP]
using G
[PROOF STATE]
proof (prove)
using this:
Max (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j

goal (1 subgoal):
 1. Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next (ns[i := Suc (ns ! i)]) 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[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence K: "Min ?B \<in> ?C"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j

goal (1 subgoal):
 1. Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j
[PROOF STEP]
using A and I
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j
index key x (length ns) mi ma = i
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) < i

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence L: "Min ?C \<le> Min ?B"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
have "Min ?C \<in> ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j
[PROOF STEP]
using K
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
have "Min ?C < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_next ns (x # xs) index key mi ma j) < i
[PROOF STEP]
using L and I
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<le> Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j)
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) < i

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j
Min (offs_set_next ns (x # xs) index key mi ma j) < i
[PROOF STEP]
have "Min ?C \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j
Min (offs_set_next ns (x # xs) index key mi ma j) < i

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

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence "Min ?B \<le> Min ?C"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next ns (x # xs) index key mi ma j) \<in> offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j

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

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence "Min ?B = Min ?C"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<le> Min (offs_set_next ns (x # xs) index key mi ma j)

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

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) = Min (offs_set_next ns (x # xs) index key mi ma j)

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
have "offs_next ns ub (x # xs) index key mi ma j = ns ! Min ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma j = ns ! Min (offs_set_next ns (x # xs) index key mi ma j)
[PROOF STEP]
using K
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) \<in> offs_set_next ns (x # xs) index key mi ma j

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

goal (2 subgoals):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; j < i\<rbrakk> \<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 j
 2. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) = Min (offs_set_next ns (x # xs) index key mi ma j)
offs_next ns ub (x # xs) index key mi ma j = ns ! Min (offs_set_next ns (x # xs) index key mi ma j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) = Min (offs_set_next ns (x # xs) index key mi ma j)
offs_next ns ub (x # xs) index key mi ma j = ns ! Min (offs_set_next ns (x # xs) index key mi ma 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]
using J
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j) = Min (offs_set_next ns (x # xs) index key mi ma j)
offs_next ns ub (x # xs) index key mi ma j = ns ! Min (offs_set_next ns (x # xs) index key mi ma j)
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j = ns ! Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma 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 simp
[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. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
let ?A = "offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
let ?B = "offs_set_next ns (x # xs) index key mi ma j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> j < i

goal (1 subgoal):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
hence "?A = ?B"
[PROOF STATE]
proof (prove)
using this:
\<not> j < 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]
using A
[PROOF STATE]
proof (prove)
using this:
\<not> j < i
index key x (length ns) 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, simp add: offs_num_cons)
[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 (1 subgoal):
 1. \<lbrakk>offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<longrightarrow> Max (offs_set_prev ns (x # xs) index key mi ma i) \<noteq> j; \<not> j < i\<rbrakk> \<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 j
[PROOF STEP]
thus ?thesis
[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

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]
proof (simp only: offs_next_def split: if_split,
   (rule_tac conjI, blast, rule_tac impI)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>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; 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; 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; offs_set_next ns (x # xs) index key mi ma j \<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 j; 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; offs_set_next ns (x # xs) index key mi ma j \<noteq> {}\<rbrakk> \<Longrightarrow> ns[i := Suc (ns ! i)] ! Min (offs_set_next ns (x # xs) index key mi ma j) = ns ! Min (offs_set_next ns (x # xs) index key mi ma j)
[PROOF STEP]
assume "?B \<noteq> {}"
[PROOF STATE]
proof (state)
this:
offs_set_next ns (x # xs) index key mi ma j \<noteq> {}

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

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

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

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

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

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

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

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 j

goal:
No subgoals!
[PROOF STEP]
qed