theory Invariants_H

lemma lookupAround2_char1:
  "(fst (lookupAround2 x s) = Some (y, v)) =
    (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None))" apply (simp    add: lookupAround2_def Let_def split_def lookupAround_def
           split del: if_split
               split: option.split) apply (intro conjI impI iffI) apply (clarsimp split: if_split_asm) apply (rule Max_prop) apply (simp add: order_less_imp_le) apply fastforce apply (clarsimp split: if_split_asm) apply (rule Max_prop) apply clarsimp apply fastforce apply (clarsimp split: if_split_asm) apply (subst(asm) Max_less_iff) apply simp apply fastforce apply (fastforce intro: order_neq_le_trans) apply (clarsimp cong: conj_cong) apply (rule conjI) apply fastforce apply (rule order_antisym) apply (subst Max_le_iff) apply simp apply fastforce apply clarsimp apply (rule ccontr) apply (fastforce simp add: linorder_not_le) apply (rule Max_ge) apply simp apply fastforce apply (intro allI impI iffI) apply clarsimp apply simp apply clarsimp apply (drule spec[where x=x]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (lookupAround2 x s) = Some (y, v)) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (1 subgoal):
 1. (s x = None \<longrightarrow> ((if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None))) \<and> (\<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None))) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> y \<le> x
 2. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> s y = Some v
 3. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 4. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 5. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (5 subgoals):
 1. \<And>xa ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> Max {k \<in> dom s. k < x} \<le> x
 2. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> s y = Some v
 3. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 4. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 5. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (6 subgoals):
 1. \<And>xa ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya; Max {k \<in> dom s. k < x} \<in> {k \<in> dom s. k < x}\<rbrakk> \<Longrightarrow> Max {k \<in> dom s. k < x} \<le> x
 2. \<And>xa ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> {k \<in> dom s. k < x} \<noteq> {}
 3. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> s y = Some v
 4. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 5. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 6. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (5 subgoals):
 1. \<And>xa ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> {k \<in> dom s. k < x} \<noteq> {}
 2. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> s y = Some v
 3. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 4. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 5. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> s y = Some v
 2. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 3. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 4. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (4 subgoals):
 1. \<And>xa ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> s (Max {k \<in> dom s. k < x}) = Some (the (s (Max {k \<in> dom s. k < x})))
 2. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 3. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 4. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (5 subgoals):
 1. \<And>xa ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya; Max {k \<in> dom s. k < x} \<in> {k \<in> dom s. k < x}\<rbrakk> \<Longrightarrow> s (Max {k \<in> dom s. k < x}) = Some (the (s (Max {k \<in> dom s. k < x})))
 2. \<And>xa ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> {k \<in> dom s. k < x} \<noteq> {}
 3. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 4. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 5. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (4 subgoals):
 1. \<And>xa ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> {k \<in> dom s. k < x} \<noteq> {}
 2. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 3. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 4. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s x = None; (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)\<rbrakk> \<Longrightarrow> \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None
 2. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<And>xa z ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya; Max {k \<in> dom s. k < x} < z; z \<le> x\<rbrakk> \<Longrightarrow> s z = None
 2. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (5 subgoals):
 1. \<And>xa z ya. \<lbrakk>z \<le> x; s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> finite {k \<in> dom s. k < x}
 2. \<And>xa z ya. \<lbrakk>z \<le> x; s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> {k \<in> dom s. k < x} \<noteq> {}
 3. \<And>xa z ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya; \<forall>a\<in>{k \<in> dom s. k < x}. a < z; z \<le> x\<rbrakk> \<Longrightarrow> s z = None
 4. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 5. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (4 subgoals):
 1. \<And>xa z ya. \<lbrakk>z \<le> x; s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya\<rbrakk> \<Longrightarrow> {k \<in> dom s. k < x} \<noteq> {}
 2. \<And>xa z ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya; \<forall>a\<in>{k \<in> dom s. k < x}. a < z; z \<le> x\<rbrakk> \<Longrightarrow> s z = None
 3. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 4. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<And>xa z ya. \<lbrakk>s x = None; y = Max {k \<in> dom s. k < x}; v = the (s (Max {k \<in> dom s. k < x})); xa < x; s xa = Some ya; \<forall>a\<in>{k \<in> dom s. k < x}. a < z; z \<le> x\<rbrakk> \<Longrightarrow> s z = None
 2. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s x = None; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> (if \<forall>xa. xa \<in> dom s \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom s. k < x}, the (s (Max {k \<in> dom s. k < x})))) = Some (y, v)
 2. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> (\<exists>xa. xa \<in> dom s \<and> xa < x) \<and> Max {k \<in> dom s. k < x} = y
 2. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> dom s \<and> xa < x
 2. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> Max {k \<in> dom s. k < x} = y
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> Max {k \<in> dom s. k < x} = y
 2. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> Max {k \<in> dom s. k < x} \<le> y
 2. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<le> Max {k \<in> dom s. k < x}
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> finite {k \<in> dom s. k < x}
 2. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> {k \<in> dom s. k < x} \<noteq> {}
 3. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> \<forall>a\<in>{k \<in> dom s. k < x}. a \<le> y
 4. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<le> Max {k \<in> dom s. k < x}
 5. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> {k \<in> dom s. k < x} \<noteq> {}
 2. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> \<forall>a\<in>{k \<in> dom s. k < x}. a \<le> y
 3. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<le> Max {k \<in> dom s. k < x}
 4. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> \<forall>a\<in>{k \<in> dom s. k < x}. a \<le> y
 2. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<le> Max {k \<in> dom s. k < x}
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<And>a ya. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None; a < x; s a = Some ya\<rbrakk> \<Longrightarrow> a \<le> y
 2. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<le> Max {k \<in> dom s. k < x}
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<And>a ya. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None; a < x; s a = Some ya; \<not> a \<le> y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<le> Max {k \<in> dom s. k < x}
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<le> Max {k \<in> dom s. k < x}
 2. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> finite {k \<in> dom s. k < x}
 2. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<in> {k \<in> dom s. k < x}
 3. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s x = None; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> y \<in> {k \<in> dom s. k < x}
 2. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (1 subgoal):
 1. \<forall>x2. s x = Some x2 \<longrightarrow> (x = y \<and> x2 = v) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>s x = Some x2; x = y \<and> x2 = v\<rbrakk> \<Longrightarrow> y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)
 2. \<And>x2. \<lbrakk>s x = Some x2; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> x = y \<and> x2 = v proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>s y = Some v; x = y; y < z; z \<le> y\<rbrakk> \<Longrightarrow> s z = None
 2. \<And>x2. \<lbrakk>s x = Some x2; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> x = y \<and> x2 = v proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>s x = Some x2; y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None)\<rbrakk> \<Longrightarrow> x = y \<and> x2 = v proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>s x = Some x2; y \<le> x; s y = Some v; \<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None\<rbrakk> \<Longrightarrow> x = y \<and> x2 = v proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>s x = Some x2; y \<le> x; s y = Some v; y < x \<and> x \<le> x \<longrightarrow> s x = None\<rbrakk> \<Longrightarrow> x = y \<and> x2 = v proof (prove)
goal:
No subgoals!