[STATEMENT]
lemma offs_pred_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"
  shows "offs_pred (ns[i := Suc (ns ! i)]) ub xs index key mi ma"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_pred (ns[i := Suc (ns ! i)]) ub xs index key mi ma
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
offs_pred ns ub (x # xs) index key mi ma

goal (1 subgoal):
 1. offs_pred (ns[i := Suc (ns ! i)]) ub xs index key mi ma
[PROOF STEP]
proof (simp add: offs_pred_def, rule_tac allI, rule_tac impI, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>\<forall>i<length ns. offs_num (length ns) (x # xs) index key mi ma i \<le> offs_next ns ub (x # xs) index key mi ma i - ns ! i; ia < length ns; offs_pred ns ub (x # xs) index key mi ma\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma ia \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma ia - ns[i := Suc (ns ! i)] ! ia
[PROOF STEP]
let ?ns' = "ns[i := Suc (ns ! i)]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>\<forall>i<length ns. offs_num (length ns) (x # xs) index key mi ma i \<le> offs_next ns ub (x # xs) index key mi ma i - ns ! i; ia < length ns; offs_pred ns ub (x # xs) index key mi ma\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma ia \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma ia - ns[i := Suc (ns ! i)] ! ia
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>\<forall>i<length ns. offs_num (length ns) (x # xs) index key mi ma i \<le> offs_next ns ub (x # xs) index key mi ma i - ns ! i; ia < length ns; offs_pred ns ub (x # xs) index key mi ma\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma ia \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma ia - ns[i := Suc (ns ! i)] ! ia
[PROOF STEP]
assume
   "\<forall>j < length ns. offs_num (length ns) (x # xs) index key mi ma j \<le>
      offs_next ns ub (x # xs) index key mi ma j - ns ! j" and
   "j < length ns"
[PROOF STATE]
proof (state)
this:
\<forall>j<length ns. offs_num (length ns) (x # xs) index key mi ma j \<le> offs_next ns ub (x # xs) index key mi ma j - ns ! j
j < length ns

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

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

goal (1 subgoal):
 1. \<And>ia. \<lbrakk>\<forall>i<length ns. offs_num (length ns) (x # xs) index key mi ma i \<le> offs_next ns ub (x # xs) index key mi ma i - ns ! i; ia < length ns; offs_pred ns ub (x # xs) index key mi ma\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma ia \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma ia - ns[i := Suc (ns ! i)] ! ia
[PROOF STEP]
from B and C
[PROOF STATE]
proof (chain)
picking this:
index key x (length ns) mi ma = i
i < length ns
[PROOF STEP]
show "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:
index key x (length ns) mi ma = i
i < length ns

goal (1 subgoal):
 1. offs_num (length ns) xs index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j - ns[i := Suc (ns ! i)] ! j
[PROOF STEP]
proof (cases "j = i", case_tac [2] "0 < offs_num (length ns) xs index key mi ma j",
   simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>j = i; index key x (length ns) mi ma = i; i < length ns\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma i \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i - Suc (ns ! i)
 2. \<lbrakk>j \<noteq> i; 0 < offs_num (length ns) xs index key mi ma j; index key x (length ns) mi ma = i; i < length ns\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j - ns ! j
[PROOF STEP]
assume "j = i"
[PROOF STATE]
proof (state)
this:
j = i

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

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

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

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

goal (2 subgoals):
 1. \<lbrakk>j = i; index key x (length ns) mi ma = i; i < length ns\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma i \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i - Suc (ns ! i)
 2. \<lbrakk>j \<noteq> i; 0 < offs_num (length ns) xs index key mi ma j; index key x (length ns) mi ma = i; i < length ns\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j - ns ! j
[PROOF STEP]
have "offs_next ns ub (x # xs) index key mi ma i \<le>
      offs_next ?ns' ub xs index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma i \<le> offs_next (ns[i := Suc (ns ! i)]) ub 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. offs_next ns ub (x # xs) index key mi ma i \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i
[PROOF STEP]
by (rule_tac offs_pred_next_cons [OF A _ C], simp_all add:
       offs_num_cons)
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma i \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>j \<noteq> i; 0 < offs_num (length ns) xs index key mi ma j; index key x (length ns) mi ma = i; i < length ns\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j - ns ! j
[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. \<lbrakk>j \<noteq> i; 0 < offs_num (length ns) xs index key mi ma j; index key x (length ns) mi ma = i; i < length ns\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j - ns ! j
[PROOF STEP]
hence "offs_next ns ub (x # xs) index key mi ma j \<le>
      offs_next ?ns' ub xs index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) 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]
using B
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma j
index key x (length ns) mi ma = i

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 (rule_tac offs_pred_next_cons [OF A _ C], simp_all add:
       offs_num_cons)
[PROOF STATE]
proof (state)
this:
offs_next ns ub (x # xs) index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j

goal (1 subgoal):
 1. \<lbrakk>j \<noteq> i; 0 < offs_num (length ns) xs index key mi ma j; index key x (length ns) mi ma = i; i < length ns\<rbrakk> \<Longrightarrow> offs_num (length ns) xs index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j - ns ! j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub (x # xs) index key mi ma j - ns ! j
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 "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:
offs_num (length ns) xs index key mi ma j \<le> offs_next ns ub (x # xs) index key mi ma j - ns ! j
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_num (length ns) xs index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j - ns ! j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offs_num (length ns) xs index key mi ma j \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma j - ns ! j

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_next_zero:
  assumes
    A: "i < length ns" and
    B: "offs_num (length ns) xs index key mi ma i = 0" and
    C: "offs_set_prev ns xs index key mi ma i = {}"
  shows "offs_next ns ub xs index key mi ma 0 =
    offs_next ns ub xs index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub xs index key mi ma 0 = offs_next ns ub xs index key mi ma i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_next ns ub xs index key mi ma 0 = offs_next ns ub xs index key mi ma i
[PROOF STEP]
have "offs_set_next ns xs index key mi ma 0 =
    offs_set_next ns xs index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_set_next ns xs index key mi ma 0 = offs_set_next ns xs index key mi ma i
[PROOF STEP]
proof (rule set_eqI, rule iffI, simp_all, (erule conjE)+, rule ccontr, simp add:
   not_less)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < length ns; 0 < x; 0 < offs_num (length ns) xs index key mi ma x; x \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < length ns; 0 < x; 0 < offs_num (length ns) xs index key mi ma x; x \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume D: "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>x. \<lbrakk>x < length ns; 0 < x; 0 < offs_num (length ns) xs index key mi ma x; x \<le> i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "j \<le> i"
[PROOF STATE]
proof (state)
this:
j \<le> i

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

goal (1 subgoal):
 1. j < i \<or> j = i
[PROOF STEP]
by (simp add: le_less)
[PROOF STATE]
proof (state)
this:
j < i \<or> j = i

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. offs_next ns ub xs index key mi ma 0 = offs_next ns ub xs index key mi ma i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
offs_set_next ns xs index key mi ma 0 = offs_set_next ns xs index key mi ma i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_next_zero_cons_eq:
  assumes
    A: "index key x (length ns) mi ma = i" and
    B: "offs_num (length ns) (x # xs) index key mi ma 0 = 0" and
    C: "offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}"
      (is "?A \<noteq> _")
  shows "offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 =
    offs_next ns ub (x # xs) index key mi ma 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
have D: "Min ?A \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (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 C
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma i \<noteq> {}

goal (1 subgoal):
 1. Min (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 Min_in, simp)
[PROOF STATE]
proof (state)
this:
Min (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. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (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. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
have E: "0 < Min ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Min (offs_set_prev ns (x # xs) index key mi ma i)
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min (offs_set_prev ns (x # xs) index key mi ma i) = 0 \<Longrightarrow> False
[PROOF STEP]
assume "Min ?A = 0"
[PROOF STATE]
proof (state)
this:
Min (offs_set_prev ns (x # xs) index key mi ma i) = 0

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < Min (offs_set_prev 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 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_prev ns (x # xs) index key mi ma i
0 < Min (offs_set_prev ns (x # xs) index key mi ma i)
[PROOF STEP]
have "Min ?A \<in> offs_set_next ns (x # xs) index key mi ma 0"
    (is "_ \<in> ?B")
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_prev ns (x # xs) index key mi ma i
0 < Min (offs_set_prev ns (x # xs) index key mi ma i)

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

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

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_next ns (x # xs) index key mi ma 0
[PROOF STEP]
have "Min ?B = Min ?A"
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_next ns (x # xs) index key mi ma 0

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) (x # xs) index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "i < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ns
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Min (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. i < length ns
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < length ns

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) (x # xs) index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "Min ?A < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Min (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. Min (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (offs_set_prev ns (x # xs) index key mi ma i) < i

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

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

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

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

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) (x # xs) index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i < length ns
j < i
0 < offs_num (length ns) (x # xs) index key mi ma j
[PROOF STEP]
have "j \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
i < length ns
j < i
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 (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) (x # xs) index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) (x # xs) index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "Min ?A \<le> j"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_prev ns (x # xs) index key mi ma i

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma 0) = Min (offs_set_prev 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 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma 0) = Min (offs_set_prev 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 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
have "Min ?A \<in> offs_set_next (ns[i := Suc (ns ! i)])
    xs index key mi ma 0"
    (is "_ \<in> ?C")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (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 0
[PROOF STEP]
using D and E
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_prev ns (x # xs) index key mi ma i
0 < Min (offs_set_prev ns (x # xs) index key mi ma i)

goal (1 subgoal):
 1. Min (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 0
[PROOF STEP]
by (auto, simp add: offs_num_cons A [symmetric])
[PROOF STATE]
proof (state)
this:
Min (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 0

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (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 0

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Min (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 0
[PROOF STEP]
have "Min ?C = Min ?A"
[PROOF STATE]
proof (prove)
using this:
Min (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 0

goal (1 subgoal):
 1. Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma 0) = Min (offs_set_prev ns (x # xs) index key mi ma i)
[PROOF STEP]
proof (subst Min_eq_iff, simp, blast, simp, rule_tac allI, rule_tac impI,
   (erule_tac conjE)+, rule_tac ccontr, simp add: not_le)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) xs index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) xs index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume F: "j < Min ?A"
[PROOF STATE]
proof (state)
this:
j < Min (offs_set_prev ns (x # xs) index key mi ma i)

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) xs index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "i < length ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ns
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Min (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. i < length ns
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < length ns

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) xs index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "Min ?A < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Min (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. Min (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (offs_set_prev ns (x # xs) index key mi ma i) < i

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

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

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

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) xs index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[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>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) xs index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "0 < offs_num (length ns) (x # xs) index key mi ma j"
[PROOF STATE]
proof (prove)
using this:
0 < offs_num (length ns) xs index key mi ma j

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) xs index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i < length ns
j < i
0 < offs_num (length ns) (x # xs) index key mi ma j
[PROOF STEP]
have "j \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
i < length ns
j < i
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 (1 subgoal):
 1. \<And>xa. \<lbrakk>Min (offs_set_prev ns (x # xs) index key mi ma i) < length ns; 0 < offs_num (length ns) xs index key mi ma (Min (offs_set_prev ns (x # xs) index key mi ma i)); 0 < xa; 0 < offs_num (length ns) xs index key mi ma xa; xa < Min (offs_set_prev ns (x # xs) index key mi ma i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "Min ?A \<le> j"
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_prev ns (x # xs) index key mi ma i

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma 0) = Min (offs_set_prev 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 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma 0) = Min (offs_set_prev 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 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
have "Min ?A < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Min (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. Min (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (offs_set_prev ns (x # xs) index key mi ma i) < i

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_next ns (x # xs) index key mi ma 0
Min (offs_set_next ns (x # xs) index key mi ma 0) = Min (offs_set_prev ns (x # xs) index key mi ma i)
Min (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 0
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma 0) = Min (offs_set_prev ns (x # xs) index key mi ma i)
Min (offs_set_prev ns (x # xs) index key mi ma i) < i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Min (offs_set_prev ns (x # xs) index key mi ma i) \<in> offs_set_next ns (x # xs) index key mi ma 0
Min (offs_set_next ns (x # xs) index key mi ma 0) = Min (offs_set_prev ns (x # xs) index key mi ma i)
Min (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 0
Min (offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma 0) = Min (offs_set_prev ns (x # xs) index key mi ma i)
Min (offs_set_prev ns (x # xs) index key mi ma i) < i

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
by (simp only: offs_next_def split: if_split,
     (rule_tac conjI, blast, rule_tac impI)+, simp)
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_next_zero_cons_neq:
  assumes
    A: "index key x (length ns) mi ma = i" and
    B: "i < length ns" and
    C: "0 < i" and
    D: "offs_set_prev ns (x # xs) index key mi ma i = {}"
  shows "offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 =
    (if 0 < offs_num (length ns) xs index key mi ma i
     then Suc (ns ! i)
     else offs_next ns ub (x # xs) index key mi ma i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = (if 0 < offs_num (length ns) xs index key mi ma i then Suc (ns ! i) else offs_next ns ub (x # xs) index key mi ma i)
[PROOF 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 0 = 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
let ?ns' = "ns[i := Suc (ns ! i)]"
[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 0 = 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 0 = 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 0 = 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 0 = 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' xs index key mi ma 0 =
    offs_set_next ns (x # xs) index key mi ma 0"
[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 0 = offs_set_next ns (x # xs) index key mi ma 0
[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 0 = offs_set_next ns (x # xs) index key mi ma 0

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 0 = 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 0 = 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 0 = offs_set_next ns (x # xs) index key mi ma 0

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 0 = 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
have "i \<in> offs_set_next ns (x # xs) index key mi ma 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> offs_set_next ns (x # xs) index key mi ma 0
[PROOF STEP]
using A and B and C
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i
i < length ns
0 < i

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

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 0 = 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<in> offs_set_next ns (x # xs) index key mi ma 0

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 0 = 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
i \<in> offs_set_next ns (x # xs) index key mi ma 0
[PROOF STEP]
have
   "Min (offs_set_next ns (x # xs) index key mi ma 0) = i"
[PROOF STATE]
proof (prove)
using this:
i \<in> offs_set_next ns (x # xs) index key mi ma 0

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

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

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 (1 subgoal):
 1. \<And>xa. \<lbrakk>i < length ns; 0 < offs_num (length ns) (x # xs) index key mi ma i; 0 < xa; 0 < offs_num (length ns) (x # xs) index key mi ma xa; xa < i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_prev ns (x # xs) index key mi ma i

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (offs_set_next ns (x # xs) index key mi ma 0) = 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 0 = 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 0 = 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 0 = offs_set_next ns (x # xs) index key mi ma 0
i \<in> offs_set_next ns (x # xs) index key mi ma 0
Min (offs_set_next ns (x # xs) index key mi ma 0) = i
[PROOF STEP]
show "offs_next ?ns' ub xs index key mi ma 0 = Suc (ns ! i)"
[PROOF STATE]
proof (prove)
using this:
offs_set_next (ns[i := Suc (ns ! i)]) xs index key mi ma 0 = offs_set_next ns (x # xs) index key mi ma 0
i \<in> offs_set_next ns (x # xs) index key mi ma 0
Min (offs_set_next ns (x # xs) index key mi ma 0) = i

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = Suc (ns ! i)
[PROOF STEP]
by (simp only: offs_next_def split: if_split, rule_tac conjI, rule_tac [!] impI,
     simp_all)
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = 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 0 = 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
let ?ns' = "ns[i := Suc (ns ! 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 0 = 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
moreover
[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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
have "offs_set_prev ?ns' xs index key mi ma i = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_set_prev (ns[i := Suc (ns ! i)]) xs index key mi ma i = {}
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
offs_set_prev ns (x # xs) index key mi ma i = {}

goal (1 subgoal):
 1. offs_set_prev (ns[i := Suc (ns ! i)]) xs index key mi ma i = {}
[PROOF STEP]
by (simp add: offs_num_cons split: if_split_asm, blast)
[PROOF STATE]
proof (state)
this:
offs_set_prev (ns[i := Suc (ns ! i)]) 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_num (length ns) xs index key mi ma i = 0
offs_set_prev (ns[i := Suc (ns ! i)]) xs index key mi ma i = {}
[PROOF STEP]
have "offs_next ?ns' ub xs index key mi ma 0 =
    offs_next ?ns' ub xs index key mi ma i"
[PROOF STATE]
proof (prove)
using this:
offs_num (length ns) xs index key mi ma i = 0
offs_set_prev (ns[i := Suc (ns ! i)]) xs index key mi ma i = {}

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

goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i
[PROOF STEP]
by (rule_tac offs_next_zero, simp_all)
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next (ns[i := Suc (ns ! i)]) ub 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next (ns[i := Suc (ns ! i)]) ub 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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
have "offs_next ?ns' ub xs index key mi ma i =
    offs_next ns ub (x # xs) index key mi ma i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
using A and B and D
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i
i < length ns
offs_set_prev 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 i = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
by (rule_tac offs_next_cons_eq, simp_all add:
     offs_num_cons)
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i = offs_next ns ub (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 0 = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i = offs_next ns ub (x # xs) index key mi ma i
[PROOF STEP]
show "offs_next ?ns' ub xs index key mi ma 0 =
    offs_next ns ub (x # xs) index key mi ma i"
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma i = offs_next ns ub (x # xs) index key mi ma i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_pred_zero_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: "i < length ns" and
    D: "0 < i" and
    E: "offs_set_prev ns (x # xs) index key mi ma i = {}"
  shows "offs_next ns ub (x # xs) index key mi ma 0 <
    offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0"
  (is "?M < ?N")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
have "i \<in> offs_set_next ns (x # xs) index key mi ma 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> offs_set_next ns (x # xs) index key mi ma 0
[PROOF STEP]
using B and C and D
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i
i < length ns
0 < i

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

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

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

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

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

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 (1 subgoal):
 1. \<And>xa. \<lbrakk>i < length ns; 0 < offs_num (length ns) (x # xs) index key mi ma i; 0 < xa; 0 < offs_num (length ns) (x # xs) index key mi ma xa; xa < i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
j \<in> offs_set_prev ns (x # xs) index key mi ma i

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

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

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

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<in> offs_set_next ns (x # xs) index key mi ma 0
Min (offs_set_next ns (x # xs) index key mi ma 0) = i
[PROOF STEP]
have F: "?M = ns ! i"
[PROOF STATE]
proof (prove)
using this:
i \<in> offs_set_next ns (x # xs) index key mi ma 0
Min (offs_set_next ns (x # xs) index key mi ma 0) = i

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

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[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 0 = (if 0 < offs_num (length ns) xs index key mi ma i then Suc (ns ! i) else offs_next ns ub (x # xs) index key mi ma i)
[PROOF STEP]
using B and C and D and E
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i
i < length ns
0 < i
offs_set_prev 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 0 = (if 0 < offs_num (length ns) xs index key mi ma i then Suc (ns ! i) else offs_next ns ub (x # xs) index key mi ma i)
[PROOF STEP]
by (rule offs_next_zero_cons_neq)
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = (if 0 < offs_num (length ns) xs index key mi ma i then Suc (ns ! i) else offs_next ns ub (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = (if 0 < offs_num (length ns) xs index key mi ma i then Suc (ns ! i) else offs_next ns ub (x # xs) index key mi ma i)

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

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

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

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 0 = offs_next ns ub (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[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 0 = offs_next ns ub (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[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 0 = 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 0 = offs_next ns ub (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = 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 0 = offs_next ns ub (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[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 B
[PROOF STATE]
proof (prove)
using this:
index key x (length ns) mi ma = i

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 C], simp add: offs_num_cons)
[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 0 = offs_next ns ub (x # xs) index key mi ma i\<rbrakk> \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = 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 0 = 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 0 < offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = 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 0 = ns ! i

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offs_pred_zero_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: "offs_num (length ns) (x # xs) index key mi ma 0 = 0"
  shows "offs_next ns ub (x # xs) index key mi ma 0 \<le>
    offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0"
  (is "?M \<le> ?N")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
proof (cases "offs_set_prev ns (x # xs) index key mi ma i = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. offs_set_prev ns (x # xs) index key mi ma i = {} \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
 2. offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
offs_set_prev ns (x # xs) index key mi ma i = {}

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

goal (1 subgoal):
 1. 0 < i
[PROOF STEP]
by (rule_tac ccontr, simp add: offs_num_cons)
[PROOF STATE]
proof (state)
this:
0 < i

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

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

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

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

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

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

goal (1 subgoal):
 1. offs_set_prev ns (x # xs) index key mi ma i \<noteq> {} \<Longrightarrow> offs_next ns ub (x # xs) index key mi ma 0 \<le> offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0
[PROOF STEP]
hence "?N = ?M"
[PROOF STATE]
proof (prove)
using this:
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 0 = offs_next ns ub (x # xs) index key mi ma 0
[PROOF STEP]
by (rule offs_next_zero_cons_eq [OF B D])
[PROOF STATE]
proof (state)
this:
offs_next (ns[i := Suc (ns ! i)]) ub xs index key mi ma 0 = offs_next ns ub (x # xs) index key mi ma 0

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma replicate_count:
 "count (mset (replicate n x)) x = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (mset (replicate n x)) x = n
[PROOF STEP]
by (induction n, simp_all)