[STATEMENT]
lemma no_interleaving_ordered:
  assumes "insert_ops ops"
    and "insert_seq start xs" and "insert_ops xs"
    and "insert_seq start ys" and "insert_ops ys"
    and "set xs \<subseteq> set ops" and "set ys \<subseteq> set ops"
    and "distinct (map fst xs @ map fst ys)"
    and "fst (hd xs) < fst (hd ys)"
    and "\<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)"
  shows "(\<forall>x \<in> set (map fst xs). \<forall>y \<in> set (map fst ys). list_order ops y x) \<and>
         (\<forall>r. start = Some r \<longrightarrow> (\<forall>x \<in> set (map fst xs). list_order ops r x) \<and>
                                 (\<forall>y \<in> set (map fst ys). list_order ops r y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set ops
set ys \<subseteq> set ops
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
proof(induction ops arbitrary: xs ys rule: List.rev_induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs xsa ys. \<lbrakk>\<And>xsa ys. \<lbrakk>insert_ops xs; insert_seq start xsa; insert_ops xsa; insert_seq start ys; insert_ops ys; set xsa \<subseteq> set xs; set ys \<subseteq> set xs; distinct (map fst xsa @ map fst ys); fst (hd xsa) < fst (hd ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins xs)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst xsa). \<forall>y\<in>set (map fst ys). list_order xs y x) \<and> (\<forall>r. start = Some r \<longrightarrow> Ball (set (map fst xsa)) (list_order xs r) \<and> Ball (set (map fst ys)) (list_order xs r)); insert_ops (xs @ [x]); insert_seq start xsa; insert_ops xsa; insert_seq start ys; insert_ops ys; set xsa \<subseteq> set (xs @ [x]); set ys \<subseteq> set (xs @ [x]); distinct (map fst xsa @ map fst ys); fst (hd xsa) < fst (hd ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins (xs @ [x]))\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>set (map fst xsa). \<forall>y\<in>set (map fst ys). list_order (xs @ [x]) y xa) \<and> (\<forall>r. start = Some r \<longrightarrow> Ball (set (map fst xsa)) (list_order (xs @ [x]) r) \<and> Ball (set (map fst ys)) (list_order (xs @ [x]) r))
[PROOF STEP]
case (snoc a ops)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops ops; insert_seq start ?xs; insert_ops ?xs; insert_seq start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ops; set ?ys \<subseteq> set ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>a\<in>set (map fst ?xs). list_order ops r a) \<and> (\<forall>a\<in>set (map fst ?ys). list_order ops r a))
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. \<And>x xs xsa ys. \<lbrakk>\<And>xsa ys. \<lbrakk>insert_ops xs; insert_seq start xsa; insert_ops xsa; insert_seq start ys; insert_ops ys; set xsa \<subseteq> set xs; set ys \<subseteq> set xs; distinct (map fst xsa @ map fst ys); fst (hd xsa) < fst (hd ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins xs)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst xsa). \<forall>y\<in>set (map fst ys). list_order xs y x) \<and> (\<forall>r. start = Some r \<longrightarrow> Ball (set (map fst xsa)) (list_order xs r) \<and> Ball (set (map fst ys)) (list_order xs r)); insert_ops (xs @ [x]); insert_seq start xsa; insert_ops xsa; insert_seq start ys; insert_ops ys; set xsa \<subseteq> set (xs @ [x]); set ys \<subseteq> set (xs @ [x]); distinct (map fst xsa @ map fst ys); fst (hd xsa) < fst (hd ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins (xs @ [x]))\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>set (map fst xsa). \<forall>y\<in>set (map fst ys). list_order (xs @ [x]) y xa) \<and> (\<forall>r. start = Some r \<longrightarrow> Ball (set (map fst xsa)) (list_order (xs @ [x]) r) \<and> Ball (set (map fst ys)) (list_order (xs @ [x]) r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>insert_ops ops; insert_seq start ?xs; insert_ops ?xs; insert_seq start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ops; set ?ys \<subseteq> set ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>a\<in>set (map fst ?xs). list_order ops r a) \<and> (\<forall>a\<in>set (map fst ?ys). list_order ops r a))
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))
[PROOF STEP]
have "insert_ops ops"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ops; insert_seq start ?xs; insert_ops ?xs; insert_seq start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ops; set ?ys \<subseteq> set ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>a\<in>set (map fst ?xs). list_order ops r a) \<and> (\<forall>a\<in>set (map fst ?ys). list_order ops r a))
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. insert_ops ops
[PROOF STEP]
using insert_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ops; insert_seq start ?xs; insert_ops ?xs; insert_seq start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ops; set ?ys \<subseteq> set ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>a\<in>set (map fst ?xs). list_order ops r a) \<and> (\<forall>a\<in>set (map fst ?ys). list_order ops r a))
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))
insert_ops (?xs @ [?x]) \<Longrightarrow> insert_ops ?xs

goal (1 subgoal):
 1. insert_ops ops
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_ops ops

goal (1 subgoal):
 1. \<And>x xs xsa ys. \<lbrakk>\<And>xsa ys. \<lbrakk>insert_ops xs; insert_seq start xsa; insert_ops xsa; insert_seq start ys; insert_ops ys; set xsa \<subseteq> set xs; set ys \<subseteq> set xs; distinct (map fst xsa @ map fst ys); fst (hd xsa) < fst (hd ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins xs)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst xsa). \<forall>y\<in>set (map fst ys). list_order xs y x) \<and> (\<forall>r. start = Some r \<longrightarrow> Ball (set (map fst xsa)) (list_order xs r) \<and> Ball (set (map fst ys)) (list_order xs r)); insert_ops (xs @ [x]); insert_seq start xsa; insert_ops xsa; insert_seq start ys; insert_ops ys; set xsa \<subseteq> set (xs @ [x]); set ys \<subseteq> set (xs @ [x]); distinct (map fst xsa @ map fst ys); fst (hd xsa) < fst (hd ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins (xs @ [x]))\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>set (map fst xsa). \<forall>y\<in>set (map fst ys). list_order (xs @ [x]) y xa) \<and> (\<forall>r. start = Some r \<longrightarrow> Ball (set (map fst xsa)) (list_order (xs @ [x]) r) \<and> Ball (set (map fst ys)) (list_order (xs @ [x]) r))
[PROOF STEP]
consider (a_in_xs) "a \<in> set xs" | (a_in_ys) "a \<in> set ys" | (neither) "a \<notin> set xs \<and> a \<notin> set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> set xs \<Longrightarrow> thesis; a \<in> set ys \<Longrightarrow> thesis; a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in> set xs \<Longrightarrow> ?thesis; a \<in> set ys \<Longrightarrow> ?thesis; a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x xs xsa ys. \<lbrakk>\<And>xsa ys. \<lbrakk>insert_ops xs; insert_seq start xsa; insert_ops xsa; insert_seq start ys; insert_ops ys; set xsa \<subseteq> set xs; set ys \<subseteq> set xs; distinct (map fst xsa @ map fst ys); fst (hd xsa) < fst (hd ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins xs)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst xsa). \<forall>y\<in>set (map fst ys). list_order xs y x) \<and> (\<forall>r. start = Some r \<longrightarrow> Ball (set (map fst xsa)) (list_order xs r) \<and> Ball (set (map fst ys)) (list_order xs r)); insert_ops (xs @ [x]); insert_seq start xsa; insert_ops xsa; insert_seq start ys; insert_ops ys; set xsa \<subseteq> set (xs @ [x]); set ys \<subseteq> set (xs @ [x]); distinct (map fst xsa @ map fst ys); fst (hd xsa) < fst (hd ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins (xs @ [x]))\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>set (map fst xsa). \<forall>y\<in>set (map fst ys). list_order (xs @ [x]) y xa) \<and> (\<forall>r. start = Some r \<longrightarrow> Ball (set (map fst xsa)) (list_order (xs @ [x]) r) \<and> Ball (set (map fst ys)) (list_order (xs @ [x]) r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<in> set xs \<Longrightarrow> ?thesis; a \<in> set ys \<Longrightarrow> ?thesis; a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<in> set xs \<Longrightarrow> ?thesis; a \<in> set ys \<Longrightarrow> ?thesis; a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
case a_in_xs
[PROOF STATE]
proof (state)
this:
a \<in> set xs

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set xs
[PROOF STEP]
have "a \<notin> set ys"
[PROOF STATE]
proof (prove)
using this:
a \<in> set xs

goal (1 subgoal):
 1. a \<notin> set ys
[PROOF STEP]
using snoc.prems(8)
[PROOF STATE]
proof (prove)
using this:
a \<in> set xs
distinct (map fst xs @ map fst ys)

goal (1 subgoal):
 1. a \<notin> set ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> set ys

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
hence "set ys \<subseteq> set ops"
[PROOF STATE]
proof (prove)
using this:
a \<notin> set ys

goal (1 subgoal):
 1. set ys \<subseteq> set ops
[PROOF STEP]
using snoc.prems(7) DiffE
[PROOF STATE]
proof (prove)
using this:
a \<notin> set ys
set ys \<subseteq> set (ops @ [a])
\<lbrakk>?c \<in> ?A - ?B; \<lbrakk>?c \<in> ?A; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. set ys \<subseteq> set ops
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ys \<subseteq> set ops

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
from a_in_xs
[PROOF STATE]
proof (chain)
picking this:
a \<in> set xs
[PROOF STEP]
have "a = last xs"
[PROOF STATE]
proof (prove)
using this:
a \<in> set xs

goal (1 subgoal):
 1. a = last xs
[PROOF STEP]
using insert_ops_subset_last snoc.prems
[PROOF STATE]
proof (prove)
using this:
a \<in> set xs
\<lbrakk>insert_ops (?xs @ [?x]); insert_ops ?ys; set ?ys \<subseteq> set (?xs @ [?x]); ?x \<in> set ?ys\<rbrakk> \<Longrightarrow> ?x = last ?ys
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. a = last xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = last xs

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have IH: "(\<forall>x \<in> set (map fst (butlast xs)). \<forall>y \<in> set (map fst ys).  list_order ops y x) \<and>
              (\<forall>r. start = Some r \<longrightarrow> (\<forall>x \<in> set (map fst (butlast xs)). list_order ops r x) \<and>
                                      (\<forall>y \<in> set (map fst          ys).  list_order ops r y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
proof(cases "xs = [a]")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
 2. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xs = [a]

goal (2 subgoals):
 1. xs = [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
 2. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs = [a]

goal (2 subgoals):
 1. xs = [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
 2. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
have "\<forall>r. start = Some r \<longrightarrow> (\<forall>y \<in> set (map fst ys). list_order ops r y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst ys). list_order ops r y)
[PROOF STEP]
using insert_seq_after_start \<open>insert_ops ops\<close> \<open>set ys \<subseteq> set ops\<close> snoc.prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ?ops; insert_seq (Some ?ref) ?xs; insert_ops ?xs; set ?xs \<subseteq> set ?ops; ?ref \<in> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst ?xs). list_order ?ops ?ref i
insert_ops ops
set ys \<subseteq> set ops
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. \<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst ys). list_order ops r y)
[PROOF STEP]
by (metis append_Nil2 calculation insert_seq_hd interp_ins_append_non_memb list.sel(1))
[PROOF STATE]
proof (state)
this:
\<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst ys). list_order ops r y)

goal (2 subgoals):
 1. xs = [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
 2. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs = [a]
\<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst ys). list_order ops r y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = [a]
\<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst ys). list_order ops r y)

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
case xs_longer: False
[PROOF STATE]
proof (state)
this:
xs \<noteq> [a]

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
from \<open>a = last xs\<close>
[PROOF STATE]
proof (chain)
picking this:
a = last xs
[PROOF STEP]
have "set (butlast xs) \<subseteq> set ops"
[PROOF STATE]
proof (prove)
using this:
a = last xs

goal (1 subgoal):
 1. set (butlast xs) \<subseteq> set ops
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
a = last xs
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. set (butlast xs) \<subseteq> set ops
[PROOF STEP]
by (simp add: distinct_fst subset_butlast)
[PROOF STATE]
proof (state)
this:
set (butlast xs) \<subseteq> set ops

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (butlast xs) \<subseteq> set ops

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
have "insert_seq start (butlast xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_seq start (butlast xs)
[PROOF STEP]
using insert_seq_butlast insert_seq_nonempty xs_longer \<open>a = last xs\<close> snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_seq ?start ?xs; ?xs \<noteq> []; ?xs \<noteq> [last ?xs]\<rbrakk> \<Longrightarrow> insert_seq ?start (butlast ?xs)
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
xs \<noteq> [a]
a = last xs
insert_seq start xs

goal (1 subgoal):
 1. insert_seq start (butlast xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
insert_seq start (butlast xs)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_seq start (butlast xs)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
have "insert_ops (butlast xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops (butlast xs)
[PROOF STEP]
using snoc.prems(2) snoc.prems(3) insert_ops_appendD
[PROOF STATE]
proof (prove)
using this:
insert_seq start xs
insert_ops xs
insert_ops (?xs @ ?ys) \<Longrightarrow> insert_ops ?xs

goal (1 subgoal):
 1. insert_ops (butlast xs)
[PROOF STEP]
by (metis append_butlast_last_id insert_seq_nonempty)
[PROOF STATE]
proof (state)
this:
insert_ops (butlast xs)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_ops (butlast xs)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
have "distinct (map fst (butlast xs) @ map fst ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (butlast xs) @ map fst ys)
[PROOF STEP]
using distinct_append_butlast1 snoc.prems(8)
[PROOF STATE]
proof (prove)
using this:
distinct (map fst ?xs @ map fst ?ys) \<Longrightarrow> distinct (map fst (butlast ?xs) @ map fst ?ys)
distinct (map fst xs @ map fst ys)

goal (1 subgoal):
 1. distinct (map fst (butlast xs) @ map fst ys)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (map fst (butlast xs) @ map fst ys)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (map fst (butlast xs) @ map fst ys)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
have "set ys \<subseteq> set ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys \<subseteq> set ops
[PROOF STEP]
using \<open>a \<notin> set ys\<close> \<open>set ys \<subseteq> set ops\<close>
[PROOF STATE]
proof (prove)
using this:
a \<notin> set ys
set ys \<subseteq> set ops

goal (1 subgoal):
 1. set ys \<subseteq> set ops
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set ys \<subseteq> set ops

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set ys \<subseteq> set ops

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
have "hd (butlast xs) = hd xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (butlast xs) = hd xs
[PROOF STEP]
by (metis append_butlast_last_id calculation(2) hd_append2 insert_seq_nonempty snoc.prems(2))
[PROOF STATE]
proof (state)
this:
hd (butlast xs) = hd xs

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
hence "fst (hd (butlast xs)) < fst (hd ys)"
[PROOF STATE]
proof (prove)
using this:
hd (butlast xs) = hd xs

goal (1 subgoal):
 1. fst (hd (butlast xs)) < fst (hd ys)
[PROOF STEP]
by (simp add: snoc.prems(9))
[PROOF STATE]
proof (state)
this:
fst (hd (butlast xs)) < fst (hd ys)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst (hd (butlast xs)) < fst (hd ys)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
have "\<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
assume "start = Some r"
[PROOF STATE]
proof (state)
this:
start = Some r

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
start = Some r
[PROOF STEP]
obtain xid where "hd xs = (xid, Some r)"
[PROOF STATE]
proof (prove)
using this:
start = Some r

goal (1 subgoal):
 1. (\<And>xid. hd xs = (xid, Some r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert_seq_hd snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
start = Some r
insert_seq ?start ?xs \<Longrightarrow> \<exists>oid. hd ?xs = (oid, ?start)
insert_seq start xs

goal (1 subgoal):
 1. (\<And>xid. hd xs = (xid, Some r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd xs = (xid, Some r)

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
hence "r < xid"
[PROOF STATE]
proof (prove)
using this:
hd xs = (xid, Some r)

goal (1 subgoal):
 1. r < xid
[PROOF STEP]
by (metis hd_in_set insert_ops_memb_ref_older insert_seq_nonempty snoc.prems(2) snoc.prems(3))
[PROOF STATE]
proof (state)
this:
r < xid

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r < xid

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
have "xid < fst a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xid < fst a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xid < fst a
[PROOF STEP]
have "xs = (butlast xs) @ [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = butlast xs @ [a]
[PROOF STEP]
using snoc.prems(2) insert_seq_nonempty \<open>a = last xs\<close>
[PROOF STATE]
proof (prove)
using this:
insert_seq start xs
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
a = last xs

goal (1 subgoal):
 1. xs = butlast xs @ [a]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs = butlast xs @ [a]

goal (1 subgoal):
 1. xid < fst a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs = butlast xs @ [a]

goal (1 subgoal):
 1. xid < fst a
[PROOF STEP]
have "(xid, Some r) \<in> set (butlast xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xid, Some r) \<in> set (butlast xs)
[PROOF STEP]
using \<open>hd xs = (xid, Some r)\<close> insert_seq_nonempty list.set_sel(1) snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
hd xs = (xid, Some r)
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
?a \<noteq> [] \<Longrightarrow> hd ?a \<in> set ?a
insert_seq start xs

goal (1 subgoal):
 1. (xid, Some r) \<in> set (butlast xs)
[PROOF STEP]
by (metis \<open>hd (butlast xs) = hd xs\<close> \<open>insert_seq start (butlast xs)\<close>)
[PROOF STATE]
proof (state)
this:
(xid, Some r) \<in> set (butlast xs)

goal (1 subgoal):
 1. xid < fst a
[PROOF STEP]
hence "xid \<in> set (map fst (butlast xs))"
[PROOF STATE]
proof (prove)
using this:
(xid, Some r) \<in> set (butlast xs)

goal (1 subgoal):
 1. xid \<in> set (map fst (butlast xs))
[PROOF STEP]
by (metis in_set_zipE zip_map_fst_snd)
[PROOF STATE]
proof (state)
this:
xid \<in> set (map fst (butlast xs))

goal (1 subgoal):
 1. xid < fst a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs = butlast xs @ [a]
xid \<in> set (map fst (butlast xs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = butlast xs @ [a]
xid \<in> set (map fst (butlast xs))

goal (1 subgoal):
 1. xid < fst a
[PROOF STEP]
using snoc.prems(3) last_op_greatest
[PROOF STATE]
proof (prove)
using this:
xs = butlast xs @ [a]
xid \<in> set (map fst (butlast xs))
insert_ops xs
\<lbrakk>insert_ops (?op_list @ [(?oid, ?oper)]); ?x \<in> set (map fst ?op_list)\<rbrakk> \<Longrightarrow> ?x < ?oid

goal (1 subgoal):
 1. xid < fst a
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
xid < fst a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xid < fst a

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r < xid
xid < fst a
[PROOF STEP]
have "r \<noteq> fst a"
[PROOF STATE]
proof (prove)
using this:
r < xid
xid < fst a

goal (1 subgoal):
 1. r \<noteq> fst a
[PROOF STEP]
using dual_order.asym
[PROOF STATE]
proof (prove)
using this:
r < xid
xid < fst a
\<lbrakk>?b < ?a; ?a < ?b\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. r \<noteq> fst a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<noteq> fst a

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
thus "r \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
r \<noteq> fst a

goal (1 subgoal):
 1. r \<in> set (interp_ins ops)
[PROOF STEP]
using snoc.prems(1) snoc.prems(10) interp_ins_maybe_grow2 \<open>start = Some r\<close>
[PROOF STATE]
proof (prove)
using this:
r \<noteq> fst a
insert_ops (ops @ [a])
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))
insert_ops (?xs @ [?x]) \<Longrightarrow> set (interp_ins (?xs @ [?x])) = set (interp_ins ?xs) \<or> set (interp_ins (?xs @ [?x])) = set (interp_ins ?xs) \<union> {fst ?x}
start = Some r

goal (1 subgoal):
 1. r \<in> set (interp_ins ops)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<in> set (interp_ins ops)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (butlast xs) \<subseteq> set ops
insert_seq start (butlast xs)
insert_ops (butlast xs)
distinct (map fst (butlast xs) @ map fst ys)
set ys \<subseteq> set ops
fst (hd (butlast xs)) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (butlast xs) \<subseteq> set ops
insert_seq start (butlast xs)
insert_ops (butlast xs)
distinct (map fst (butlast xs) @ map fst ys)
set ys \<subseteq> set ops
fst (hd (butlast xs)) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
using \<open>insert_ops ops\<close> snoc.IH snoc.prems(4) snoc.prems(5)
[PROOF STATE]
proof (prove)
using this:
set (butlast xs) \<subseteq> set ops
insert_seq start (butlast xs)
insert_ops (butlast xs)
distinct (map fst (butlast xs) @ map fst ys)
set ys \<subseteq> set ops
fst (hd (butlast xs)) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
insert_ops ops
\<lbrakk>insert_ops ops; insert_seq start ?xs; insert_ops ?xs; insert_seq start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ops; set ?ys \<subseteq> set ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>a\<in>set (map fst ?xs). list_order ops r a) \<and> (\<forall>a\<in>set (map fst ?ys). list_order ops r a))
insert_seq start ys
insert_ops ys

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have x_exists: "\<forall>x \<in> set (map fst (butlast xs)). x \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
proof(cases start)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. start = None \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
 2. \<And>a. start = Some a \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
start = None

goal (2 subgoals):
 1. start = None \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
 2. \<And>a. start = Some a \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
start = None

goal (2 subgoals):
 1. start = None \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
 2. \<And>a. start = Some a \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
have "set (butlast xs) \<subseteq> set ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (butlast xs) \<subseteq> set ops
[PROOF STEP]
using \<open>a = last xs\<close> distinct_map snoc.prems(6) snoc.prems(8) subset_butlast
[PROOF STATE]
proof (prove)
using this:
a = last xs
distinct (map ?f ?xs) = (distinct ?xs \<and> inj_on ?f (set ?xs))
set xs \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
\<lbrakk>set ?xs \<subseteq> set (?ys @ [?y]); last ?xs = ?y; distinct ?xs\<rbrakk> \<Longrightarrow> set (butlast ?xs) \<subseteq> set ?ys

goal (1 subgoal):
 1. set (butlast xs) \<subseteq> set ops
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set (butlast xs) \<subseteq> set ops

goal (2 subgoals):
 1. start = None \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
 2. \<And>a. start = Some a \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
start = None
set (butlast xs) \<subseteq> set ops
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
start = None
set (butlast xs) \<subseteq> set ops

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
using insert_seq_start_none \<open>insert_ops ops\<close> snoc.prems
[PROOF STATE]
proof (prove)
using this:
start = None
set (butlast xs) \<subseteq> set ops
\<lbrakk>insert_ops ?ops; insert_seq None ?xs; insert_ops ?xs; set ?xs \<subseteq> set ?ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst ?xs). i \<in> set (interp_ins ?ops)
insert_ops ops
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
by (metis append_butlast_last_id butlast.simps(2) empty_iff empty_set
            insert_ops_rem_last insert_seq_butlast insert_seq_nonempty list.simps(8))
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<And>a. start = Some a \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. start = Some a \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
case (Some a)
[PROOF STATE]
proof (state)
this:
start = Some a

goal (1 subgoal):
 1. \<And>a. start = Some a \<Longrightarrow> \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
start = Some a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
start = Some a

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
using IH list_order_memb2
[PROOF STATE]
proof (prove)
using this:
start = Some a
(\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
list_order ?ops ?x ?y \<Longrightarrow> ?y \<in> set (interp_ins ?ops)

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have "\<forall>y \<in> set (map fst ys). list_order (ops @ [a]) y (fst a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
proof(cases "xs = [a]")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
 2. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
case xs_a: True
[PROOF STATE]
proof (state)
this:
xs = [a]

goal (2 subgoals):
 1. xs = [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
 2. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
have "ys \<noteq> [] \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
assume "ys \<noteq> []"
[PROOF STATE]
proof (state)
this:
ys \<noteq> []

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys \<noteq> []
[PROOF STEP]
obtain yi where yi_def: "ys = (yi, start) # (tl ys)"
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []

goal (1 subgoal):
 1. (\<And>yi. ys = (yi, start) # tl ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis hd_Cons_tl insert_seq_hd snoc.prems(4))
[PROOF STATE]
proof (state)
this:
ys = (yi, start) # tl ys

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
hence "(yi, start) \<in> set ops"
[PROOF STATE]
proof (prove)
using this:
ys = (yi, start) # tl ys

goal (1 subgoal):
 1. (yi, start) \<in> set ops
[PROOF STEP]
by (metis \<open>set ys \<subseteq> set ops\<close> list.set_intros(1) subsetCE)
[PROOF STATE]
proof (state)
this:
(yi, start) \<in> set ops

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
hence "yi \<in> set (map fst ops)"
[PROOF STATE]
proof (prove)
using this:
(yi, start) \<in> set ops

goal (1 subgoal):
 1. yi \<in> set (map fst ops)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
yi \<in> set (map fst ops)

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
hence "yi < fst a"
[PROOF STATE]
proof (prove)
using this:
yi \<in> set (map fst ops)

goal (1 subgoal):
 1. yi < fst a
[PROOF STEP]
using snoc.prems(1) last_op_greatest
[PROOF STATE]
proof (prove)
using this:
yi \<in> set (map fst ops)
insert_ops (ops @ [a])
\<lbrakk>insert_ops (?op_list @ [(?oid, ?oper)]); ?x \<in> set (map fst ?op_list)\<rbrakk> \<Longrightarrow> ?x < ?oid

goal (1 subgoal):
 1. yi < fst a
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
yi < fst a

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yi < fst a

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
have "fst a < yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst a < yi
[PROOF STEP]
by (metis yi_def xs_a fst_conv list.sel(1) snoc.prems(9))
[PROOF STATE]
proof (state)
this:
fst a < yi

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
yi < fst a
fst a < yi
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
yi < fst a
fst a < yi

goal (1 subgoal):
 1. False
[PROOF STEP]
using less_not_sym
[PROOF STATE]
proof (prove)
using this:
yi < fst a
fst a < yi
?x < ?y \<Longrightarrow> \<not> ?y < ?x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ys \<noteq> [] \<Longrightarrow> False

goal (2 subgoals):
 1. xs = [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
 2. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
show "\<forall>y \<in> set (map fst ys). list_order (ops @ [a]) y (fst a)"
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> [] \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
using insert_seq_nonempty snoc.prems(4)
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> [] \<Longrightarrow> False
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
insert_seq start ys

goal (1 subgoal):
 1. \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
case xs_longer: False
[PROOF STATE]
proof (state)
this:
xs \<noteq> [a]

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
hence butlast_split: "butlast xs = (butlast (butlast xs)) @ [last (butlast xs)]"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> [a]

goal (1 subgoal):
 1. butlast xs = butlast (butlast xs) @ [last (butlast xs)]
[PROOF STEP]
using \<open>a = last xs\<close> insert_seq_butlast insert_seq_nonempty snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> [a]
a = last xs
\<lbrakk>insert_seq ?start ?xs; ?xs \<noteq> []; ?xs \<noteq> [last ?xs]\<rbrakk> \<Longrightarrow> insert_seq ?start (butlast ?xs)
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
insert_seq start xs

goal (1 subgoal):
 1. butlast xs = butlast (butlast xs) @ [last (butlast xs)]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
butlast xs = butlast (butlast xs) @ [last (butlast xs)]

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
hence ref_exists: "fst (last (butlast xs)) \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
butlast xs = butlast (butlast xs) @ [last (butlast xs)]

goal (1 subgoal):
 1. fst (last (butlast xs)) \<in> set (interp_ins ops)
[PROOF STEP]
using x_exists
[PROOF STATE]
proof (prove)
using this:
butlast xs = butlast (butlast xs) @ [last (butlast xs)]
\<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)

goal (1 subgoal):
 1. fst (last (butlast xs)) \<in> set (interp_ins ops)
[PROOF STEP]
by (metis last_in_set last_map map_is_Nil_conv snoc_eq_iff_butlast)
[PROOF STATE]
proof (state)
this:
fst (last (butlast xs)) \<in> set (interp_ins ops)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst (last (butlast xs)) \<in> set (interp_ins ops)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
from butlast_split
[PROOF STATE]
proof (chain)
picking this:
butlast xs = butlast (butlast xs) @ [last (butlast xs)]
[PROOF STEP]
have "xs = (butlast (butlast xs)) @ [last (butlast xs), a]"
[PROOF STATE]
proof (prove)
using this:
butlast xs = butlast (butlast xs) @ [last (butlast xs)]

goal (1 subgoal):
 1. xs = butlast (butlast xs) @ [last (butlast xs), a]
[PROOF STEP]
by (metis \<open>a = last xs\<close> append.assoc append_butlast_last_id butlast.simps(2)
            insert_seq_nonempty last_ConsL last_ConsR list.simps(3) snoc.prems(2))
[PROOF STATE]
proof (state)
this:
xs = butlast (butlast xs) @ [last (butlast xs), a]

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
hence "snd a = Some (fst (last (butlast xs)))"
[PROOF STATE]
proof (prove)
using this:
xs = butlast (butlast xs) @ [last (butlast xs), a]

goal (1 subgoal):
 1. snd a = Some (fst (last (butlast xs)))
[PROOF STEP]
using snoc.prems(2) insert_seq_last_ref
[PROOF STATE]
proof (prove)
using this:
xs = butlast (butlast xs) @ [last (butlast xs), a]
insert_seq start xs
insert_seq ?start (?xs @ [(?xi, ?xr), (?yi, ?yr)]) \<Longrightarrow> ?yr = Some ?xi

goal (1 subgoal):
 1. snd a = Some (fst (last (butlast xs)))
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
snd a = Some (fst (last (butlast xs)))

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
hence "list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)"
[PROOF STATE]
proof (prove)
using this:
snd a = Some (fst (last (butlast xs)))

goal (1 subgoal):
 1. list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)
[PROOF STEP]
using list_order_insert_ref ref_exists snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
snd a = Some (fst (last (butlast xs)))
\<lbrakk>insert_ops (?ops @ [(?oid, Some ?ref)]); ?ref \<in> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> list_order (?ops @ [(?oid, Some ?ref)]) ?ref ?oid
fst (last (butlast xs)) \<in> set (interp_ins ops)
insert_ops (ops @ [a])

goal (1 subgoal):
 1. list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
have "\<forall>y \<in> set (map fst ys). list_order ops y (fst (last (butlast xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>set (map fst ys). list_order ops y (fst (last (butlast xs)))
[PROOF STEP]
by (metis IH butlast_split last_in_set last_map map_is_Nil_conv snoc_eq_iff_butlast)
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (map fst ys). list_order ops y (fst (last (butlast xs)))

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
hence "\<forall>y \<in> set (map fst ys). list_order (ops @ [a]) y (fst (last (butlast xs)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set (map fst ys). list_order ops y (fst (last (butlast xs)))

goal (1 subgoal):
 1. \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst (last (butlast xs)))
[PROOF STEP]
using list_order_append snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set (map fst ys). list_order ops y (fst (last (butlast xs)))
\<lbrakk>insert_ops (?pre @ ?suf); list_order ?pre ?x ?y\<rbrakk> \<Longrightarrow> list_order (?pre @ ?suf) ?x ?y
insert_ops (ops @ [a])

goal (1 subgoal):
 1. \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst (last (butlast xs)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst (last (butlast xs)))

goal (1 subgoal):
 1. xs \<noteq> [a] \<Longrightarrow> \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst (last (butlast xs)) \<in> set (interp_ins ops)
list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst (last (butlast xs)))
[PROOF STEP]
show "\<forall>y \<in> set (map fst ys). list_order (ops @ [a]) y (fst a)"
[PROOF STATE]
proof (prove)
using this:
fst (last (butlast xs)) \<in> set (interp_ins ops)
list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst (last (butlast xs)))

goal (1 subgoal):
 1. \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
using list_order_trans snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
fst (last (butlast xs)) \<in> set (interp_ins ops)
list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst (last (butlast xs)))
\<lbrakk>insert_ops ?op_list; list_order ?op_list ?x ?y; list_order ?op_list ?y ?z\<rbrakk> \<Longrightarrow> list_order ?op_list ?x ?z
insert_ops (ops @ [a])

goal (1 subgoal):
 1. \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have map_fst_xs: "map fst xs = map fst (butlast xs) @ map fst [last xs]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst xs = map fst (butlast xs) @ map fst [last xs]
[PROOF STEP]
by (metis append_butlast_last_id insert_seq_nonempty map_append snoc.prems(2))
[PROOF STATE]
proof (state)
this:
map fst xs = map fst (butlast xs) @ map fst [last xs]

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
hence "set (map fst xs) = set (map fst (butlast xs)) \<union> {fst a}"
[PROOF STATE]
proof (prove)
using this:
map fst xs = map fst (butlast xs) @ map fst [last xs]

goal (1 subgoal):
 1. set (map fst xs) = set (map fst (butlast xs)) \<union> {fst a}
[PROOF STEP]
by (simp add: \<open>a = last xs\<close>)
[PROOF STATE]
proof (state)
this:
set (map fst xs) = set (map fst (butlast xs)) \<union> {fst a}

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (map fst xs) = set (map fst (butlast xs)) \<union> {fst a}

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have "\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. \<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)
[PROOF STEP]
by (cases start, auto simp add: insert_seq_after_start \<open>a = last xs\<close> map_fst_xs)
[PROOF STATE]
proof (state)
this:
\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)

goal (3 subgoals):
 1. a \<in> set xs \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 3. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
\<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
set (map fst xs) = set (map fst (butlast xs)) \<union> {fst a}
\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)
[PROOF STEP]
show "(\<forall>x \<in> set (map fst xs). \<forall>y \<in> set (map fst ys). list_order (ops @ [a]) y x) \<and>
          (\<forall>r. start = Some r \<longrightarrow> (\<forall>x \<in> set (map fst xs). list_order (ops @ [a]) r x) \<and>
                                  (\<forall>y \<in> set (map fst ys). list_order (ops @ [a]) r y))"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
\<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
set (map fst xs) = set (map fst (butlast xs)) \<union> {fst a}
\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>set (map fst (butlast xs)). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst (butlast xs)). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
\<forall>x\<in>set (map fst (butlast xs)). x \<in> set (interp_ins ops)
\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y (fst a)
set (map fst xs) = set (map fst (butlast xs)) \<union> {fst a}
\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)
insert_ops (ops @ [a])

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))
[PROOF STEP]
by (simp add: list_order_append)
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
case a_in_ys
[PROOF STATE]
proof (state)
this:
a \<in> set ys

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set ys
[PROOF STEP]
have "a \<notin> set xs"
[PROOF STATE]
proof (prove)
using this:
a \<in> set ys

goal (1 subgoal):
 1. a \<notin> set xs
[PROOF STEP]
using snoc.prems(8)
[PROOF STATE]
proof (prove)
using this:
a \<in> set ys
distinct (map fst xs @ map fst ys)

goal (1 subgoal):
 1. a \<notin> set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> set xs

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
hence "set xs \<subseteq> set ops"
[PROOF STATE]
proof (prove)
using this:
a \<notin> set xs

goal (1 subgoal):
 1. set xs \<subseteq> set ops
[PROOF STEP]
using snoc.prems(6) DiffE
[PROOF STATE]
proof (prove)
using this:
a \<notin> set xs
set xs \<subseteq> set (ops @ [a])
\<lbrakk>?c \<in> ?A - ?B; \<lbrakk>?c \<in> ?A; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. set xs \<subseteq> set ops
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> set ops

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
from a_in_ys
[PROOF STATE]
proof (chain)
picking this:
a \<in> set ys
[PROOF STEP]
have "a = last ys"
[PROOF STATE]
proof (prove)
using this:
a \<in> set ys

goal (1 subgoal):
 1. a = last ys
[PROOF STEP]
using insert_ops_subset_last snoc.prems
[PROOF STATE]
proof (prove)
using this:
a \<in> set ys
\<lbrakk>insert_ops (?xs @ [?x]); insert_ops ?ys; set ?ys \<subseteq> set (?xs @ [?x]); ?x \<in> set ?ys\<rbrakk> \<Longrightarrow> ?x = last ?ys
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. a = last ys
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = last ys

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have IH: "(\<forall>x \<in> set (map fst xs). \<forall>y \<in> set (map fst (butlast ys)).  list_order ops y x) \<and>
              (\<forall>r. start = Some r \<longrightarrow> (\<forall>x \<in> set (map fst          xs).  list_order ops r x) \<and>
                                      (\<forall>y \<in> set (map fst (butlast ys)). list_order ops r y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
proof(cases "ys = [a]")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
 2. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ys = [a]

goal (2 subgoals):
 1. ys = [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
 2. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys = [a]

goal (2 subgoals):
 1. ys = [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
 2. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
have "\<forall>r. start = Some r \<longrightarrow> (\<forall>y \<in> set (map fst xs). list_order ops r y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst xs). list_order ops r y)
[PROOF STEP]
using insert_seq_after_start \<open>insert_ops ops\<close> \<open>set xs \<subseteq> set ops\<close> snoc.prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ?ops; insert_seq (Some ?ref) ?xs; insert_ops ?xs; set ?xs \<subseteq> set ?ops; ?ref \<in> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst ?xs). list_order ?ops ?ref i
insert_ops ops
set xs \<subseteq> set ops
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. \<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst xs). list_order ops r y)
[PROOF STEP]
by (metis append_Nil2 calculation insert_seq_hd interp_ins_append_non_memb list.sel(1))
[PROOF STATE]
proof (state)
this:
\<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst xs). list_order ops r y)

goal (2 subgoals):
 1. ys = [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
 2. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ys = [a]
\<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst xs). list_order ops r y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = [a]
\<forall>r. start = Some r \<longrightarrow> (\<forall>y\<in>set (map fst xs). list_order ops r y)

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
case ys_longer: False
[PROOF STATE]
proof (state)
this:
ys \<noteq> [a]

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
from \<open>a = last ys\<close>
[PROOF STATE]
proof (chain)
picking this:
a = last ys
[PROOF STEP]
have "set (butlast ys) \<subseteq> set ops"
[PROOF STATE]
proof (prove)
using this:
a = last ys

goal (1 subgoal):
 1. set (butlast ys) \<subseteq> set ops
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
a = last ys
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. set (butlast ys) \<subseteq> set ops
[PROOF STEP]
by (simp add: distinct_fst subset_butlast)
[PROOF STATE]
proof (state)
this:
set (butlast ys) \<subseteq> set ops

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (butlast ys) \<subseteq> set ops

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
have "insert_seq start (butlast ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_seq start (butlast ys)
[PROOF STEP]
using insert_seq_butlast insert_seq_nonempty ys_longer \<open>a = last ys\<close> snoc.prems(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_seq ?start ?xs; ?xs \<noteq> []; ?xs \<noteq> [last ?xs]\<rbrakk> \<Longrightarrow> insert_seq ?start (butlast ?xs)
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
ys \<noteq> [a]
a = last ys
insert_seq start ys

goal (1 subgoal):
 1. insert_seq start (butlast ys)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
insert_seq start (butlast ys)

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_seq start (butlast ys)

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
have "insert_ops (butlast ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops (butlast ys)
[PROOF STEP]
using snoc.prems(4) snoc.prems(5) insert_ops_appendD
[PROOF STATE]
proof (prove)
using this:
insert_seq start ys
insert_ops ys
insert_ops (?xs @ ?ys) \<Longrightarrow> insert_ops ?xs

goal (1 subgoal):
 1. insert_ops (butlast ys)
[PROOF STEP]
by (metis append_butlast_last_id insert_seq_nonempty)
[PROOF STATE]
proof (state)
this:
insert_ops (butlast ys)

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_ops (butlast ys)

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
have "distinct (map fst xs @ map fst (butlast ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst xs @ map fst (butlast ys))
[PROOF STEP]
using distinct_append_butlast2 snoc.prems(8)
[PROOF STATE]
proof (prove)
using this:
distinct (map fst ?xs @ map fst ?ys) \<Longrightarrow> distinct (map fst ?xs @ map fst (butlast ?ys))
distinct (map fst xs @ map fst ys)

goal (1 subgoal):
 1. distinct (map fst xs @ map fst (butlast ys))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (map fst xs @ map fst (butlast ys))

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (map fst xs @ map fst (butlast ys))

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
have "set xs \<subseteq> set ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> set ops
[PROOF STEP]
using \<open>a \<notin> set xs\<close> \<open>set xs \<subseteq> set ops\<close>
[PROOF STATE]
proof (prove)
using this:
a \<notin> set xs
set xs \<subseteq> set ops

goal (1 subgoal):
 1. set xs \<subseteq> set ops
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> set ops

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> set ops

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
have "hd (butlast ys) = hd ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (butlast ys) = hd ys
[PROOF STEP]
by (metis append_butlast_last_id calculation(2) hd_append2 insert_seq_nonempty snoc.prems(4))
[PROOF STATE]
proof (state)
this:
hd (butlast ys) = hd ys

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
hence "fst (hd xs) < fst (hd (butlast ys))"
[PROOF STATE]
proof (prove)
using this:
hd (butlast ys) = hd ys

goal (1 subgoal):
 1. fst (hd xs) < fst (hd (butlast ys))
[PROOF STEP]
by (simp add: snoc.prems(9))
[PROOF STATE]
proof (state)
this:
fst (hd xs) < fst (hd (butlast ys))

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst (hd xs) < fst (hd (butlast ys))

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
have "\<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
assume "start = Some r"
[PROOF STATE]
proof (state)
this:
start = Some r

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
start = Some r
[PROOF STEP]
obtain yid where "hd ys = (yid, Some r)"
[PROOF STATE]
proof (prove)
using this:
start = Some r

goal (1 subgoal):
 1. (\<And>yid. hd ys = (yid, Some r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert_seq_hd snoc.prems(4)
[PROOF STATE]
proof (prove)
using this:
start = Some r
insert_seq ?start ?xs \<Longrightarrow> \<exists>oid. hd ?xs = (oid, ?start)
insert_seq start ys

goal (1 subgoal):
 1. (\<And>yid. hd ys = (yid, Some r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd ys = (yid, Some r)

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
hence "r < yid"
[PROOF STATE]
proof (prove)
using this:
hd ys = (yid, Some r)

goal (1 subgoal):
 1. r < yid
[PROOF STEP]
by (metis hd_in_set insert_ops_memb_ref_older insert_seq_nonempty snoc.prems(4) snoc.prems(5))
[PROOF STATE]
proof (state)
this:
r < yid

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r < yid

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
have "yid < fst a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yid < fst a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. yid < fst a
[PROOF STEP]
have "ys = (butlast ys) @ [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys = butlast ys @ [a]
[PROOF STEP]
using snoc.prems(4) insert_seq_nonempty \<open>a = last ys\<close>
[PROOF STATE]
proof (prove)
using this:
insert_seq start ys
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
a = last ys

goal (1 subgoal):
 1. ys = butlast ys @ [a]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ys = butlast ys @ [a]

goal (1 subgoal):
 1. yid < fst a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys = butlast ys @ [a]

goal (1 subgoal):
 1. yid < fst a
[PROOF STEP]
have "(yid, Some r) \<in> set (butlast ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (yid, Some r) \<in> set (butlast ys)
[PROOF STEP]
using \<open>hd ys = (yid, Some r)\<close> insert_seq_nonempty list.set_sel(1) snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
hd ys = (yid, Some r)
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
?a \<noteq> [] \<Longrightarrow> hd ?a \<in> set ?a
insert_seq start xs

goal (1 subgoal):
 1. (yid, Some r) \<in> set (butlast ys)
[PROOF STEP]
by (metis \<open>hd (butlast ys) = hd ys\<close> \<open>insert_seq start (butlast ys)\<close>)
[PROOF STATE]
proof (state)
this:
(yid, Some r) \<in> set (butlast ys)

goal (1 subgoal):
 1. yid < fst a
[PROOF STEP]
hence "yid \<in> set (map fst (butlast ys))"
[PROOF STATE]
proof (prove)
using this:
(yid, Some r) \<in> set (butlast ys)

goal (1 subgoal):
 1. yid \<in> set (map fst (butlast ys))
[PROOF STEP]
by (metis in_set_zipE zip_map_fst_snd)
[PROOF STATE]
proof (state)
this:
yid \<in> set (map fst (butlast ys))

goal (1 subgoal):
 1. yid < fst a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ys = butlast ys @ [a]
yid \<in> set (map fst (butlast ys))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = butlast ys @ [a]
yid \<in> set (map fst (butlast ys))

goal (1 subgoal):
 1. yid < fst a
[PROOF STEP]
using snoc.prems(5) last_op_greatest
[PROOF STATE]
proof (prove)
using this:
ys = butlast ys @ [a]
yid \<in> set (map fst (butlast ys))
insert_ops ys
\<lbrakk>insert_ops (?op_list @ [(?oid, ?oper)]); ?x \<in> set (map fst ?op_list)\<rbrakk> \<Longrightarrow> ?x < ?oid

goal (1 subgoal):
 1. yid < fst a
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
yid < fst a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
yid < fst a

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r < yid
yid < fst a
[PROOF STEP]
have "r \<noteq> fst a"
[PROOF STATE]
proof (prove)
using this:
r < yid
yid < fst a

goal (1 subgoal):
 1. r \<noteq> fst a
[PROOF STEP]
using dual_order.asym
[PROOF STATE]
proof (prove)
using this:
r < yid
yid < fst a
\<lbrakk>?b < ?a; ?a < ?b\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. r \<noteq> fst a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<noteq> fst a

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
thus "r \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
r \<noteq> fst a

goal (1 subgoal):
 1. r \<in> set (interp_ins ops)
[PROOF STEP]
using snoc.prems(1) snoc.prems(10) interp_ins_maybe_grow2 \<open>start = Some r\<close>
[PROOF STATE]
proof (prove)
using this:
r \<noteq> fst a
insert_ops (ops @ [a])
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))
insert_ops (?xs @ [?x]) \<Longrightarrow> set (interp_ins (?xs @ [?x])) = set (interp_ins ?xs) \<or> set (interp_ins (?xs @ [?x])) = set (interp_ins ?xs) \<union> {fst ?x}
start = Some r

goal (1 subgoal):
 1. r \<in> set (interp_ins ops)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<in> set (interp_ins ops)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (butlast ys) \<subseteq> set ops
insert_seq start (butlast ys)
insert_ops (butlast ys)
distinct (map fst xs @ map fst (butlast ys))
set xs \<subseteq> set ops
fst (hd xs) < fst (hd (butlast ys))
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (butlast ys) \<subseteq> set ops
insert_seq start (butlast ys)
insert_ops (butlast ys)
distinct (map fst xs @ map fst (butlast ys))
set xs \<subseteq> set ops
fst (hd xs) < fst (hd (butlast ys))
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
using \<open>insert_ops ops\<close> snoc.IH snoc.prems(2) snoc.prems(3)
[PROOF STATE]
proof (prove)
using this:
set (butlast ys) \<subseteq> set ops
insert_seq start (butlast ys)
insert_ops (butlast ys)
distinct (map fst xs @ map fst (butlast ys))
set xs \<subseteq> set ops
fst (hd xs) < fst (hd (butlast ys))
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
insert_ops ops
\<lbrakk>insert_ops ops; insert_seq start ?xs; insert_ops ?xs; insert_seq start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ops; set ?ys \<subseteq> set ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>a\<in>set (map fst ?xs). list_order ops r a) \<and> (\<forall>a\<in>set (map fst ?ys). list_order ops r a))
insert_seq start xs
insert_ops xs

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have "\<forall>x \<in> set (map fst xs). list_order (ops @ [a]) (fst a) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
proof(cases "ys = [a]")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
 2. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
case ys_a: True
[PROOF STATE]
proof (state)
this:
ys = [a]

goal (2 subgoals):
 1. ys = [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
 2. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys = [a]
[PROOF STEP]
show "\<forall>x \<in> set (map fst xs). list_order (ops @ [a]) (fst a) x"
[PROOF STATE]
proof (prove)
using this:
ys = [a]

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
proof(cases start)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ys = [a]; start = None\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
 2. \<And>aa. \<lbrakk>ys = [a]; start = Some aa\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
start = None

goal (2 subgoals):
 1. \<lbrakk>ys = [a]; start = None\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
 2. \<And>aa. \<lbrakk>ys = [a]; start = Some aa\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
start = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
start = None

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
using insert_seq_start_none list_order_insert_none snoc.prems
[PROOF STATE]
proof (prove)
using this:
start = None
\<lbrakk>insert_ops ?ops; insert_seq None ?xs; insert_ops ?xs; set ?xs \<subseteq> set ?ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst ?xs). i \<in> set (interp_ins ?ops)
\<lbrakk>insert_ops (?ops @ [(?oid, None)]); ?x \<in> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> list_order (?ops @ [(?oid, None)]) ?oid ?x
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
by (metis \<open>insert_ops ops\<close> \<open>set xs \<subseteq> set ops\<close> fst_conv insert_seq_hd list.sel(1) ys_a)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>ys = [a]; start = Some aa\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>ys = [a]; start = Some aa\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
case (Some r)
[PROOF STATE]
proof (state)
this:
start = Some r

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>ys = [a]; start = Some aa\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
start = Some r

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>ys = [a]; start = Some aa\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
start = Some r
[PROOF STEP]
have "\<forall>x \<in> set (map fst xs). list_order ops r x"
[PROOF STATE]
proof (prove)
using this:
start = Some r

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order ops r x
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
start = Some r
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order ops r x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). list_order ops r x

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>ys = [a]; start = Some aa\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
start = Some r
\<forall>x\<in>set (map fst xs). list_order ops r x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
start = Some r
\<forall>x\<in>set (map fst xs). list_order ops r x

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
using snoc.prems(1) snoc.prems(4) list_order_insert_between
[PROOF STATE]
proof (prove)
using this:
start = Some r
\<forall>x\<in>set (map fst xs). list_order ops r x
insert_ops (ops @ [a])
insert_seq start ys
\<lbrakk>insert_ops (?ops @ [(?oid, Some ?ref)]); list_order ?ops ?ref ?x\<rbrakk> \<Longrightarrow> list_order (?ops @ [(?oid, Some ?ref)]) ?oid ?x

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
by (metis fst_conv insert_seq_hd list.sel(1) ys_a)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
case ys_longer: False
[PROOF STATE]
proof (state)
this:
ys \<noteq> [a]

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
hence butlast_split: "butlast ys = (butlast (butlast ys)) @ [last (butlast ys)]"
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> [a]

goal (1 subgoal):
 1. butlast ys = butlast (butlast ys) @ [last (butlast ys)]
[PROOF STEP]
using \<open>a = last ys\<close> insert_seq_butlast insert_seq_nonempty snoc.prems(4)
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> [a]
a = last ys
\<lbrakk>insert_seq ?start ?xs; ?xs \<noteq> []; ?xs \<noteq> [last ?xs]\<rbrakk> \<Longrightarrow> insert_seq ?start (butlast ?xs)
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
insert_seq start ys

goal (1 subgoal):
 1. butlast ys = butlast (butlast ys) @ [last (butlast ys)]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
butlast ys = butlast (butlast ys) @ [last (butlast ys)]

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
butlast ys = butlast (butlast ys) @ [last (butlast ys)]

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
butlast ys = butlast (butlast ys) @ [last (butlast ys)]
[PROOF STEP]
have "ys = (butlast (butlast ys)) @ [last (butlast ys), a]"
[PROOF STATE]
proof (prove)
using this:
butlast ys = butlast (butlast ys) @ [last (butlast ys)]

goal (1 subgoal):
 1. ys = butlast (butlast ys) @ [last (butlast ys), a]
[PROOF STEP]
by (metis \<open>a = last ys\<close> append.assoc append_butlast_last_id butlast.simps(2)
            insert_seq_nonempty last_ConsL last_ConsR list.simps(3) snoc.prems(4))
[PROOF STATE]
proof (state)
this:
ys = butlast (butlast ys) @ [last (butlast ys), a]

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
hence "snd a = Some (fst (last (butlast ys)))"
[PROOF STATE]
proof (prove)
using this:
ys = butlast (butlast ys) @ [last (butlast ys), a]

goal (1 subgoal):
 1. snd a = Some (fst (last (butlast ys)))
[PROOF STEP]
using snoc.prems(4) insert_seq_last_ref
[PROOF STATE]
proof (prove)
using this:
ys = butlast (butlast ys) @ [last (butlast ys), a]
insert_seq start ys
insert_seq ?start (?xs @ [(?xi, ?xr), (?yi, ?yr)]) \<Longrightarrow> ?yr = Some ?xi

goal (1 subgoal):
 1. snd a = Some (fst (last (butlast ys)))
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
snd a = Some (fst (last (butlast ys)))

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
snd a = Some (fst (last (butlast ys)))

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
have "\<forall>x \<in> set (map fst xs). list_order ops (fst (last (butlast ys))) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order ops (fst (last (butlast ys))) x
[PROOF STEP]
by (metis IH butlast_split last_in_set last_map map_is_Nil_conv snoc_eq_iff_butlast)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). list_order ops (fst (last (butlast ys))) x

goal (1 subgoal):
 1. ys \<noteq> [a] \<Longrightarrow> \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
butlast ys = butlast (butlast ys) @ [last (butlast ys)]
snd a = Some (fst (last (butlast ys)))
\<forall>x\<in>set (map fst xs). list_order ops (fst (last (butlast ys))) x
[PROOF STEP]
show "\<forall>x \<in> set (map fst xs). list_order (ops @ [a]) (fst a) x"
[PROOF STATE]
proof (prove)
using this:
butlast ys = butlast (butlast ys) @ [last (butlast ys)]
snd a = Some (fst (last (butlast ys)))
\<forall>x\<in>set (map fst xs). list_order ops (fst (last (butlast ys))) x

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
using list_order_insert_between snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
butlast ys = butlast (butlast ys) @ [last (butlast ys)]
snd a = Some (fst (last (butlast ys)))
\<forall>x\<in>set (map fst xs). list_order ops (fst (last (butlast ys))) x
\<lbrakk>insert_ops (?ops @ [(?oid, Some ?ref)]); list_order ?ops ?ref ?x\<rbrakk> \<Longrightarrow> list_order (?ops @ [(?oid, Some ?ref)]) ?oid ?x
insert_ops (ops @ [a])

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have map_fst_xs: "map fst ys = map fst (butlast ys) @ map fst [last ys]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst ys = map fst (butlast ys) @ map fst [last ys]
[PROOF STEP]
by (metis append_butlast_last_id insert_seq_nonempty map_append snoc.prems(4))
[PROOF STATE]
proof (state)
this:
map fst ys = map fst (butlast ys) @ map fst [last ys]

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
hence "set (map fst ys) = set (map fst (butlast ys)) \<union> {fst a}"
[PROOF STATE]
proof (prove)
using this:
map fst ys = map fst (butlast ys) @ map fst [last ys]

goal (1 subgoal):
 1. set (map fst ys) = set (map fst (butlast ys)) \<union> {fst a}
[PROOF STEP]
by (simp add: \<open>a = last ys\<close>)
[PROOF STATE]
proof (state)
this:
set (map fst ys) = set (map fst (butlast ys)) \<union> {fst a}

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (map fst ys) = set (map fst (butlast ys)) \<union> {fst a}

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have "\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))

goal (1 subgoal):
 1. \<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)
[PROOF STEP]
by (cases start, auto simp add: insert_seq_after_start \<open>a = last ys\<close> map_fst_xs)
[PROOF STATE]
proof (state)
this:
\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)

goal (2 subgoals):
 1. a \<in> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
 2. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
set (map fst ys) = set (map fst (butlast ys)) \<union> {fst a}
\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)
[PROOF STEP]
show "(\<forall>x \<in> set (map fst xs). \<forall>y \<in> set (map fst ys). list_order (ops @ [a]) y x) \<and>
          (\<forall>r. start = Some r \<longrightarrow> (\<forall>x \<in> set (map fst xs). list_order (ops @ [a]) r x) \<and>
                                  (\<forall>y \<in> set (map fst ys). list_order (ops @ [a]) r y))"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
set (map fst ys) = set (map fst (butlast ys)) \<union> {fst a}
\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst (butlast ys)). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst (butlast ys)). list_order ops r y))
\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) (fst a) x
set (map fst ys) = set (map fst (butlast ys)) \<union> {fst a}
\<forall>r. start = Some r \<longrightarrow> list_order (ops @ [a]) r (fst a)
insert_ops (ops @ [a])

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))
[PROOF STEP]
by (simp add: list_order_append)
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))

goal (1 subgoal):
 1. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
case neither
[PROOF STATE]
proof (state)
this:
a \<notin> set xs \<and> a \<notin> set ys

goal (1 subgoal):
 1. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
hence "set xs \<subseteq> set ops" and "set ys \<subseteq> set ops"
[PROOF STATE]
proof (prove)
using this:
a \<notin> set xs \<and> a \<notin> set ys

goal (1 subgoal):
 1. set xs \<subseteq> set ops &&& set ys \<subseteq> set ops
[PROOF STEP]
using snoc.prems(6) snoc.prems(7) DiffE
[PROOF STATE]
proof (prove)
using this:
a \<notin> set xs \<and> a \<notin> set ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
\<lbrakk>?c \<in> ?A - ?B; \<lbrakk>?c \<in> ?A; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. set xs \<subseteq> set ops &&& set ys \<subseteq> set ops
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> set ops
set ys \<subseteq> set ops

goal (1 subgoal):
 1. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
have "(\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> (xs = [] \<and> ys = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
proof(cases xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
 2. \<And>a list. xs = a # list \<Longrightarrow> (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
 2. \<And>a list. xs = a # list \<Longrightarrow> (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
using insert_seq_nonempty snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
xs = []
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
insert_seq start xs

goal (1 subgoal):
 1. (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
case xs_nonempty: (Cons x xsa)
[PROOF STATE]
proof (state)
this:
xs = x # xsa

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
have "\<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
assume "start = Some r"
[PROOF STATE]
proof (state)
this:
start = Some r

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
start = Some r
[PROOF STEP]
obtain xi where "x = (xi, Some r)"
[PROOF STATE]
proof (prove)
using this:
start = Some r

goal (1 subgoal):
 1. (\<And>xi. x = (xi, Some r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert_seq_hd xs_nonempty snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
start = Some r
insert_seq ?start ?xs \<Longrightarrow> \<exists>oid. hd ?xs = (oid, ?start)
xs = x # xsa
insert_seq start xs

goal (1 subgoal):
 1. (\<And>xi. x = (xi, Some r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = (xi, Some r)

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
hence "(xi, Some r) \<in> set ops"
[PROOF STATE]
proof (prove)
using this:
x = (xi, Some r)

goal (1 subgoal):
 1. (xi, Some r) \<in> set ops
[PROOF STEP]
using \<open>set xs \<subseteq> set ops\<close> xs_nonempty
[PROOF STATE]
proof (prove)
using this:
x = (xi, Some r)
set xs \<subseteq> set ops
xs = x # xsa

goal (1 subgoal):
 1. (xi, Some r) \<in> set ops
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(xi, Some r) \<in> set ops

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
hence "r < xi"
[PROOF STATE]
proof (prove)
using this:
(xi, Some r) \<in> set ops

goal (1 subgoal):
 1. r < xi
[PROOF STEP]
using \<open>insert_ops ops\<close> insert_ops_memb_ref_older
[PROOF STATE]
proof (prove)
using this:
(xi, Some r) \<in> set ops
insert_ops ops
\<lbrakk>insert_ops ?op_list; (?oid, Some ?ref) \<in> set ?op_list\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. r < xi
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r < xi

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r < xi

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
have "xi \<in> set (map fst ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xi \<in> set (map fst ops)
[PROOF STEP]
using \<open>(xi, Some r) \<in> set ops\<close>
[PROOF STATE]
proof (prove)
using this:
(xi, Some r) \<in> set ops

goal (1 subgoal):
 1. xi \<in> set (map fst ops)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
xi \<in> set (map fst ops)

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
hence "xi < fst a"
[PROOF STATE]
proof (prove)
using this:
xi \<in> set (map fst ops)

goal (1 subgoal):
 1. xi < fst a
[PROOF STEP]
using last_op_greatest snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
xi \<in> set (map fst ops)
\<lbrakk>insert_ops (?op_list @ [(?oid, ?oper)]); ?x \<in> set (map fst ?op_list)\<rbrakk> \<Longrightarrow> ?x < ?oid
insert_ops (ops @ [a])

goal (1 subgoal):
 1. xi < fst a
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
xi < fst a

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r < xi
xi < fst a
[PROOF STEP]
have "fst a \<noteq> r"
[PROOF STATE]
proof (prove)
using this:
r < xi
xi < fst a

goal (1 subgoal):
 1. fst a \<noteq> r
[PROOF STEP]
using order.asym
[PROOF STATE]
proof (prove)
using this:
r < xi
xi < fst a
\<lbrakk>?a < ?b; ?b < ?a\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. fst a \<noteq> r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst a \<noteq> r

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst a \<noteq> r
[PROOF STEP]
show "r \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
fst a \<noteq> r

goal (1 subgoal):
 1. r \<in> set (interp_ins ops)
[PROOF STEP]
using snoc.prems(1) snoc.prems(10) interp_ins_maybe_grow2 \<open>start = Some r\<close>
[PROOF STATE]
proof (prove)
using this:
fst a \<noteq> r
insert_ops (ops @ [a])
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))
insert_ops (?xs @ [?x]) \<Longrightarrow> set (interp_ins (?xs @ [?x])) = set (interp_ins ?xs) \<or> set (interp_ins (?xs @ [?x])) = set (interp_ins ?xs) \<union> {fst ?x}
start = Some r

goal (1 subgoal):
 1. r \<in> set (interp_ins ops)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<in> set (interp_ins ops)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. (\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []

goal (1 subgoal):
 1. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
hence "(\<forall>x \<in> set (map fst xs). \<forall>y \<in> set (map fst ys). list_order ops y x) \<and>
           (\<forall>r. start = Some r \<longrightarrow> (\<forall>x \<in> set (map fst xs). list_order ops r x) \<and>
                                   (\<forall>y \<in> set (map fst ys). list_order ops r y))"
[PROOF STATE]
proof (prove)
using this:
(\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
using snoc.prems snoc.IH \<open>set xs \<subseteq> set ops\<close> \<open>set ys \<subseteq> set ops\<close>
[PROOF STATE]
proof (prove)
using this:
(\<forall>r. start = Some r \<longrightarrow> r \<in> set (interp_ins ops)) \<or> xs = [] \<and> ys = []
insert_ops (ops @ [a])
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set (ops @ [a])
set ys \<subseteq> set (ops @ [a])
distinct (map fst xs @ map fst ys)
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins (ops @ [a]))
\<lbrakk>insert_ops ops; insert_seq start ?xs; insert_ops ?xs; insert_seq start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ops; set ?ys \<subseteq> set ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>a\<in>set (map fst ?xs). list_order ops r a) \<and> (\<forall>a\<in>set (map fst ?ys). list_order ops r a))
set xs \<subseteq> set ops
set ys \<subseteq> set ops

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))

goal (1 subgoal):
 1. a \<notin> set xs \<and> a \<notin> set ys \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
[PROOF STEP]
show "(\<forall>x \<in> set (map fst xs). \<forall>y \<in> set (map fst ys). list_order (ops @ [a]) y x) \<and>
          (\<forall>r. start = Some r \<longrightarrow> (\<forall>x \<in> set (map fst xs). list_order (ops @ [a]) r x) \<and>
                                  (\<forall>y \<in> set (map fst ys). list_order (ops @ [a]) r y))"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order ops r x) \<and> (\<forall>y\<in>set (map fst ys). list_order ops r y))
insert_ops (ops @ [a])

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))
[PROOF STEP]
by (simp add: list_order_append)
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst xs). list_order (ops @ [a]) r x) \<and> (\<forall>y\<in>set (map fst ys). list_order (ops @ [a]) r y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order (ops @ [a]) y x) \<and> (\<forall>r. start = Some r \<longrightarrow> (\<forall>b\<in>set (map fst xs). list_order (ops @ [a]) r b) \<and> (\<forall>b\<in>set (map fst ys). list_order (ops @ [a]) r b))

goal:
No subgoals!
[PROOF STEP]
qed