[STATEMENT]
lemma map_to_sorted_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 11)"
  assumes TSL: "SIDE_GEN_ALGO (is_map_to_sorted_list R Rk Rv Rs tsl)"
  shows "(\<lambda>s. RETURN (tsl s), map_to_sorted_list R)
    \<in> \<langle>Rk,Rv\<rangle>Rs \<rightarrow> \<langle>\<langle>\<langle>Rk,Rv\<rangle>prod_rel\<rangle>list_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. RETURN (tsl s), map_to_sorted_list R) \<in> \<langle>Rk, Rv\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel\<rangle>nres_rel
[PROOF STEP]
proof (intro fun_relI nres_relI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk, Rv\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R a')
[PROOF STEP]
fix s s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk, Rv\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R a')
[PROOF STEP]
assume "(s,s')\<in>\<langle>Rk,Rv\<rangle>Rs"
[PROOF STATE]
proof (state)
this:
(s, s') \<in> \<langle>Rk, Rv\<rangle>Rs

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk, Rv\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R a')
[PROOF STEP]
with TSL
[PROOF STATE]
proof (chain)
picking this:
SIDE_GEN_ALGO (is_map_to_sorted_list R Rk Rv Rs tsl)
(s, s') \<in> \<langle>Rk, Rv\<rangle>Rs
[PROOF STEP]
obtain l' where
    R1: "(tsl s, l') \<in> \<langle>\<langle>Rk,Rv\<rangle>prod_rel\<rangle>list_rel"
      and R2: "RETURN l' \<le> map_to_sorted_list R s'"
[PROOF STATE]
proof (prove)
using this:
SIDE_GEN_ALGO (is_map_to_sorted_list R Rk Rv Rs tsl)
(s, s') \<in> \<langle>Rk, Rv\<rangle>Rs

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl s, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> map_to_sorted_list R s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_map_to_sorted_list_def map_to_sorted_list_def autoref_tag_defs
[PROOF STATE]
proof (prove)
using this:
\<forall>m m'. (m, m') \<in> \<langle>Rk, Rv\<rangle>Rs \<longrightarrow> (\<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel R) (map_to_set m'))
(s, s') \<in> \<langle>Rk, Rv\<rangle>Rs

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl s, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (key_rel R) (map_to_set s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(tsl s, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel
RETURN l' \<le> map_to_sorted_list R s'

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk, Rv\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R a')
[PROOF STEP]
have "RETURN (tsl s) \<le> \<Down>(\<langle>\<langle>Rk,Rv\<rangle>prod_rel\<rangle>list_rel) (RETURN l')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (tsl s) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (RETURN l')
[PROOF STEP]
apply (rule RETURN_refine)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (tsl s, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (RETURN l')

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk, Rv\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R a')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (RETURN l')

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk, Rv\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R a')
[PROOF STEP]
note R2
[PROOF STATE]
proof (state)
this:
RETURN l' \<le> map_to_sorted_list R s'

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk, Rv\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R a')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R s')
[PROOF STEP]
show
    "RETURN (tsl s) \<le> \<Down> (\<langle>\<langle>Rk,Rv\<rangle>prod_rel\<rangle>list_rel) (map_to_sorted_list R s')"
[PROOF STATE]
proof (prove)
using this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R s')

goal (1 subgoal):
 1. RETURN (tsl s) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R s')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel) (map_to_sorted_list R s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_to_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 10)"
  assumes TSL: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs tsl)"
  shows "(\<lambda>s. RETURN (tsl s), map_to_sorted_list (\<lambda>_ _. True))
    \<in> \<langle>Rk,Rv\<rangle>Rs \<rightarrow> \<langle>\<langle>\<langle>Rk,Rv\<rangle>prod_rel\<rangle>list_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. RETURN (tsl s), map_to_sorted_list (\<lambda>_ _. True)) \<in> \<langle>Rk, Rv\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel\<rangle>nres_rel
[PROOF STEP]
using assms(2-)
[PROOF STATE]
proof (prove)
using this:
SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs tsl)

goal (1 subgoal):
 1. (\<lambda>s. RETURN (tsl s), map_to_sorted_list (\<lambda>_ _. True)) \<in> \<langle>Rk, Rv\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel\<rangle>nres_rel
[PROOF STEP]
unfolding is_map_to_list_def
[PROOF STATE]
proof (prove)
using this:
SIDE_GEN_ALGO (is_map_to_sorted_list (\<lambda>_ _. True) Rk Rv Rs tsl)

goal (1 subgoal):
 1. (\<lambda>s. RETURN (tsl s), map_to_sorted_list (\<lambda>_ _. True)) \<in> \<langle>Rk, Rv\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel\<rangle>nres_rel
[PROOF STEP]
by (rule map_to_sorted_list_by_tsl[OF PRIO_TAGI])


[STATEMENT]
lemma proper_it_mono_dres_pair:
  assumes PR: "proper_it' it it'"
  assumes A: "\<And>k v x. f k v x \<le> f' k v x"
  shows "
    it' s (case_dres False False c) (\<lambda>(k,v) s. s \<bind> f k v) \<sigma>
    \<le> it' s (case_dres False False c) (\<lambda>(k,v) s. s \<bind> f' k v) \<sigma>" (is "?a \<le> ?b")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
from proper_itE[OF PR[THEN proper_it'D]]
[PROOF STATE]
proof (chain)
picking this:
(\<And>l. \<lbrakk>it ?s1 = foldli l; it' ?s1 = foldli l\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain l where
    A_FMT:
      "?a = foldli l (case_dres False False c) (\<lambda>(k,v) s. s \<bind> f k v) \<sigma>"
        (is "_ = ?a'")
    and B_FMT:
      "?b = foldli l (case_dres False False c) (\<lambda>(k,v) s. s \<bind> f' k v) \<sigma>"
        (is "_ = ?b'")
[PROOF STATE]
proof (prove)
using this:
(\<And>l. \<lbrakk>it ?s1 = foldli l; it' ?s1 = foldli l\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>; it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
f ?k ?v ?x \<le> f' ?k ?v ?x
[PROOF STEP]
have A': "\<And>kv x. case_prod f kv x \<le> case_prod f' kv x"
[PROOF STATE]
proof (prove)
using this:
f ?k ?v ?x \<le> f' ?k ?v ?x

goal (1 subgoal):
 1. \<And>kv x. (case kv of (x, xa) \<Rightarrow> f x xa) x \<le> (case kv of (x, xa) \<Rightarrow> f' x xa) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(case ?kv of (x, xa) \<Rightarrow> f x xa) ?x \<le> (case ?kv of (x, xa) \<Rightarrow> f' x xa) ?x

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
note A_FMT
[PROOF STATE]
proof (state)
this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
have
    "?a' = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> case_prod f kv) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa)) \<sigma>
[PROOF STEP]
apply (fo_rule fun_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa))
[PROOF STEP]
apply (fo_rule arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(k, v) s. s \<bind> f k v) = (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa)) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa)) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
note foldli_mono_dres[OF A']
[PROOF STATE]
proof (state)
this:
foldli ?l (case_dres False False ?c) (\<lambda>x s. s \<bind> (\<lambda>xa. (case ?kv1 x xa of (x, xa) \<Rightarrow> f x xa) (?x1 x xa))) ?\<sigma> \<le> foldli ?l (case_dres False False ?c) (\<lambda>x s. s \<bind> (\<lambda>xa. (case ?kv1 x xa of (x, xa) \<Rightarrow> f' x xa) (?x1 x xa))) ?\<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldli ?l (case_dres False False ?c) (\<lambda>x s. s \<bind> (\<lambda>xa. (case ?kv1 x xa of (x, xa) \<Rightarrow> f x xa) (?x1 x xa))) ?\<sigma> \<le> foldli ?l (case_dres False False ?c) (\<lambda>x s. s \<bind> (\<lambda>xa. (case ?kv1 x xa of (x, xa) \<Rightarrow> f' x xa) (?x1 x xa))) ?\<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
have
    "foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> case_prod f' kv) \<sigma> = ?b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
apply (fo_rule fun_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v)
[PROOF STEP]
apply (fo_rule arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) = (\<lambda>(k, v) s. s \<bind> f' k v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
note B_FMT[symmetric]
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma> = it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_it_mono_dres_pair_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "\<And>k v x. flat_ge (f k v x) (f' k v x)"
  shows "
    flat_ge (it' s (case_dres False False c) (\<lambda>(k,v) s. s \<bind> f k v) \<sigma>)
      (it' s (case_dres False False c) (\<lambda>(k,v) s. s \<bind> f' k v) \<sigma>)"
      (is "flat_ge ?a ?b")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
from proper_itE[OF PR[THEN proper_it'D]]
[PROOF STATE]
proof (chain)
picking this:
(\<And>l. \<lbrakk>it ?s1 = foldli l; it' ?s1 = foldli l\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain l where
    A_FMT:
      "?a = foldli l (case_dres False False c) (\<lambda>(k,v) s. s \<bind> f k v) \<sigma>"
        (is "_ = ?a'")
    and B_FMT:
      "?b = foldli l (case_dres False False c) (\<lambda>(k,v) s. s \<bind> f' k v) \<sigma>"
        (is "_ = ?b'")
[PROOF STATE]
proof (prove)
using this:
(\<And>l. \<lbrakk>it ?s1 = foldli l; it' ?s1 = foldli l\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>; it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
flat_ge (f ?k ?v ?x) (f' ?k ?v ?x)
[PROOF STEP]
have A': "\<And>kv x. flat_ge (case_prod f kv x) (case_prod f' kv x)"
[PROOF STATE]
proof (prove)
using this:
flat_ge (f ?k ?v ?x) (f' ?k ?v ?x)

goal (1 subgoal):
 1. \<And>kv x. flat_ge ((case kv of (x, xa) \<Rightarrow> f x xa) x) ((case kv of (x, xa) \<Rightarrow> f' x xa) x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
flat_ge ((case ?kv of (x, xa) \<Rightarrow> f x xa) ?x) ((case ?kv of (x, xa) \<Rightarrow> f' x xa) ?x)

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
note A_FMT
[PROOF STATE]
proof (state)
this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
have
    "?a' = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> case_prod f kv) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa)) \<sigma>
[PROOF STEP]
apply (fo_rule fun_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa))
[PROOF STEP]
apply (fo_rule arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(k, v) s. s \<bind> f k v) = (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa)) \<sigma>

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma> = foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f x xa)) \<sigma>

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
note foldli_mono_dres_flat[OF A']
[PROOF STATE]
proof (state)
this:
flat_ge (foldli ?l (case_dres False False ?c) (\<lambda>x s. s \<bind> (\<lambda>xa. (case ?kv1 x xa of (x, xa) \<Rightarrow> f x xa) (?x1 x xa))) ?\<sigma>) (foldli ?l (case_dres False False ?c) (\<lambda>x s. s \<bind> (\<lambda>xa. (case ?kv1 x xa of (x, xa) \<Rightarrow> f' x xa) (?x1 x xa))) ?\<sigma>)

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
flat_ge (foldli ?l (case_dres False False ?c) (\<lambda>x s. s \<bind> (\<lambda>xa. (case ?kv1 x xa of (x, xa) \<Rightarrow> f x xa) (?x1 x xa))) ?\<sigma>) (foldli ?l (case_dres False False ?c) (\<lambda>x s. s \<bind> (\<lambda>xa. (case ?kv1 x xa of (x, xa) \<Rightarrow> f' x xa) (?x1 x xa))) ?\<sigma>)

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
have
    "foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> case_prod f' kv) \<sigma> = ?b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>
[PROOF STEP]
apply (fo_rule fun_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v)
[PROOF STEP]
apply (fo_rule arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) = (\<lambda>(k, v) s. s \<bind> f' k v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>kv s. s \<bind> (case kv of (x, xa) \<Rightarrow> f' x xa)) \<sigma> = foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
note B_FMT[symmetric]
[PROOF STATE]
proof (state)
this:
foldli l (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma> = it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)

goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
flat_ge (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f k v) \<sigma>) (it' s (case_dres False False c) (\<lambda>(k, v) s. s \<bind> f' k v) \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_it_mono_dres:
  assumes PR: "proper_it' it it'"
  assumes A: "\<And>kv x. f kv x \<le> f' kv x"
  shows "
    it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma>
    \<le> it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>
[PROOF STEP]
apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it s = foldli l; it' s = foldli l\<rbrakk> \<Longrightarrow> it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma> \<le> it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>
[PROOF STEP]
apply (erule_tac t="it' s" in ssubst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. it s = foldli l \<Longrightarrow> foldli l (\<lambda>a. case a of dRETURN a \<Rightarrow> c a | _ \<Rightarrow> False) (\<lambda>a aa. aa \<bind> f a) \<sigma> \<le> foldli l (\<lambda>a. case a of dRETURN a \<Rightarrow> c a | _ \<Rightarrow> False) (\<lambda>a aa. aa \<bind> f' a) \<sigma>
[PROOF STEP]
apply (rule foldli_mono_dres[OF A])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma proper_it_mono_dres_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "\<And>kv x. flat_ge (f kv x) (f' kv x)"
  shows "
    flat_ge (it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma>)
      (it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat_ge (it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma>) (it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>)
[PROOF STEP]
apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it s = foldli l; it' s = foldli l\<rbrakk> \<Longrightarrow> flat_ge (it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma>) (it' s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>)
[PROOF STEP]
apply (erule_tac t="it' s" in ssubst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. it s = foldli l \<Longrightarrow> flat_ge (foldli l (\<lambda>a. case a of dRETURN a \<Rightarrow> c a | _ \<Rightarrow> False) (\<lambda>a aa. aa \<bind> f a) \<sigma>) (foldli l (\<lambda>a. case a of dRETURN a \<Rightarrow> c a | _ \<Rightarrow> False) (\<lambda>a aa. aa \<bind> f' a) \<sigma>)
[PROOF STEP]
apply (rule foldli_mono_dres_flat[OF A])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pi'_dom[icf_proper_iteratorI]: "proper_it' it it'
  \<Longrightarrow> proper_it' (map_iterator_dom o it) (map_iterator_dom o it')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' it it' \<Longrightarrow> proper_it' (map_iterator_dom \<circ> it) (map_iterator_dom \<circ> it')
[PROOF STEP]
apply (rule proper_it'I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. proper_it' it it' \<Longrightarrow> proper_it ((map_iterator_dom \<circ> it) s) ((map_iterator_dom \<circ> it') s)
[PROOF STEP]
apply (simp add: comp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. proper_it' it it' \<Longrightarrow> proper_it (map_iterator_dom (it s)) (map_iterator_dom (it' s))
[PROOF STEP]
apply (rule icf_proper_iteratorI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. proper_it' it it' \<Longrightarrow> proper_it (it s) (it' s)
[PROOF STEP]
apply (erule proper_it'D)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma proper_it_mono_dres_dom:
  assumes PR: "proper_it' it it'"
  assumes A: "\<And>kv x. f kv x \<le> f' kv x"
  shows "
    (map_iterator_dom o it') s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma>
    \<le>
    (map_iterator_dom o it') s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_iterator_dom \<circ> it') s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma> \<le> (map_iterator_dom \<circ> it') s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>
[PROOF STEP]
apply (rule proper_it_mono_dres)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper_it' ?it (map_iterator_dom \<circ> it')
 2. \<And>kv x. f kv x \<le> f' kv x
[PROOF STEP]
apply (rule icf_proper_iteratorI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper_it' ?it12 it'
 2. \<And>kv x. f kv x \<le> f' kv x
[PROOF STEP]
by fact+


[STATEMENT]
lemma proper_it_mono_dres_dom_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "\<And>kv x. flat_ge (f kv x) (f' kv x)"
  shows "flat_ge
    ((map_iterator_dom o it') s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma>)
    ((map_iterator_dom o it') s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flat_ge ((map_iterator_dom \<circ> it') s (case_dres False False c) (\<lambda>kv s. s \<bind> f kv) \<sigma>) ((map_iterator_dom \<circ> it') s (case_dres False False c) (\<lambda>kv s. s \<bind> f' kv) \<sigma>)
[PROOF STEP]
apply (rule proper_it_mono_dres_flat)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper_it' ?it (map_iterator_dom \<circ> it')
 2. \<And>kv x. flat_ge (f kv x) (f' kv x)
[PROOF STEP]
apply (rule icf_proper_iteratorI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper_it' ?it12 it'
 2. \<And>kv x. flat_ge (f kv x) (f' kv x)
[PROOF STEP]
by fact+


[STATEMENT]
lemma length_hideDupsRec[simp]: "\<And>x. length(hideDupsRec x xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. |hideDupsRec x xs| = |xs|
[PROOF STEP]
by(induct xs) auto


[STATEMENT]
lemma length_hideDups[simp]: "length(hideDups xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |hideDups xs| = |xs|
[PROOF STEP]
by(cases xs) simp_all


[STATEMENT]
lemma length_indexToVertexList[simp]:
 "length(indexToVertexList x y xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |indexToVertexList x y xs| = |xs|
[PROOF STEP]
by(simp add:indexToVertexList_def)


[STATEMENT]
lemma increasing1: "\<And> as x. increasing ls \<Longrightarrow> ls = as @ x # cs @ y # bs \<Longrightarrow> x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>as x. \<lbrakk>increasing ls; ls = as @ x # [] @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>a cs as x. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (a # cs) @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
increasing ls
ls = as @ x # [] @ y # bs

goal (2 subgoals):
 1. \<And>as x. \<lbrakk>increasing ls; ls = as @ x # [] @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>a cs as x. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (a # cs) @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
increasing ls
ls = as @ x # [] @ y # bs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
increasing ls
ls = as @ x # [] @ y # bs

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by (auto simp: increasing_def)
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (1 subgoal):
 1. \<And>a cs as x. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (a # cs) @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs as x. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (a # cs) @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>increasing ls; ls = ?as @ ?x # cs @ y # bs\<rbrakk> \<Longrightarrow> ?x \<le> y
increasing ls
ls = as @ x # (c # cs) @ y # bs

goal (1 subgoal):
 1. \<And>a cs as x. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (a # cs) @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>increasing ls; ls = ?as @ ?x # cs @ y # bs\<rbrakk> \<Longrightarrow> ?x \<le> y
increasing ls
ls = as @ x # (c # cs) @ y # bs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>increasing ls; ls = ?as @ ?x # cs @ y # bs\<rbrakk> \<Longrightarrow> ?x \<le> y
increasing ls
ls = as @ x # (c # cs) @ y # bs

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
apply (subgoal_tac "c \<le> y")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (c # cs) @ y # bs; c \<le> y\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (c # cs) @ y # bs\<rbrakk> \<Longrightarrow> c \<le> y
[PROOF STEP]
apply (force simp: increasing_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (c # cs) @ y # bs\<rbrakk> \<Longrightarrow> c \<le> y
[PROOF STEP]
apply (rule_tac Cons)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (c # cs) @ y # bs\<rbrakk> \<Longrightarrow> increasing ls
 2. \<lbrakk>\<And>as x. \<lbrakk>increasing ls; ls = as @ x # cs @ y # bs\<rbrakk> \<Longrightarrow> x \<le> y; increasing ls; ls = as @ x # (c # cs) @ y # bs\<rbrakk> \<Longrightarrow> ls = ?as18 @ c # cs @ y # bs
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
x \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma increasing2: "increasing (as@bs) \<Longrightarrow> x \<in> set as \<Longrightarrow> y \<in> set bs \<Longrightarrow> x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>increasing (as @ bs); x \<in> set as; y \<in> set bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>increasing (as @ bs); x \<in> set as; y \<in> set bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
assume n:"increasing (as@bs)" and x:"x \<in> set as" and y: "y \<in> set bs"
[PROOF STATE]
proof (state)
this:
increasing (as @ bs)
x \<in> set as
y \<in> set bs

goal (1 subgoal):
 1. \<lbrakk>increasing (as @ bs); x \<in> set as; y \<in> set bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> set as
[PROOF STEP]
obtain as' as'' where as: "as = as' @ x # as''"
[PROOF STATE]
proof (prove)
using this:
x \<in> set as

goal (1 subgoal):
 1. (\<And>as' as''. as = as' @ x # as'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: in_set_conv_decomp)
[PROOF STATE]
proof (state)
this:
as = as' @ x # as''

goal (1 subgoal):
 1. \<lbrakk>increasing (as @ bs); x \<in> set as; y \<in> set bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y \<in> set bs
[PROOF STEP]
obtain bs' bs'' where bs: "bs = bs' @ y # bs''"
[PROOF STATE]
proof (prove)
using this:
y \<in> set bs

goal (1 subgoal):
 1. (\<And>bs' bs''. bs = bs' @ y # bs'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: in_set_conv_decomp)
[PROOF STATE]
proof (state)
this:
bs = bs' @ y # bs''

goal (1 subgoal):
 1. \<lbrakk>increasing (as @ bs); x \<in> set as; y \<in> set bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
from n as bs
[PROOF STATE]
proof (chain)
picking this:
increasing (as @ bs)
as = as' @ x # as''
bs = bs' @ y # bs''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
increasing (as @ bs)
as = as' @ x # as''
bs = bs' @ y # bs''

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
apply (auto intro!: increasing1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>increasing (as' @ x # as'' @ bs' @ y # bs''); as = as' @ x # as''; bs = bs' @ y # bs''\<rbrakk> \<Longrightarrow> as' @ x # as'' @ bs' @ y # bs'' = ?as3 @ x # ?cs3 @ y # ?bs3
[PROOF STEP]
apply (subgoal_tac "as' @ x # as'' @ bs' @ y # bs'' = as' @ x # (as'' @ bs') @ y # bs''")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>increasing (as' @ x # as'' @ bs' @ y # bs''); as = as' @ x # as''; bs = bs' @ y # bs''; as' @ x # as'' @ bs' @ y # bs'' = as' @ x # (as'' @ bs') @ y # bs''\<rbrakk> \<Longrightarrow> as' @ x # as'' @ bs' @ y # bs'' = ?as3 @ x # ?cs3 @ y # ?bs3
 2. \<lbrakk>increasing (as' @ x # as'' @ bs' @ y # bs''); as = as' @ x # as''; bs = bs' @ y # bs''\<rbrakk> \<Longrightarrow> as' @ x # as'' @ bs' @ y # bs'' = as' @ x # (as'' @ bs') @ y # bs''
[PROOF STEP]
by (assumption) auto
[PROOF STATE]
proof (state)
this:
x \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma increasing3: "\<forall> as bs. (ls = as @ bs \<longrightarrow> (\<forall> x \<in> set as. \<forall> y \<in> set bs. x \<le> y)) \<Longrightarrow> increasing (ls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>as bs. ls = as @ bs \<longrightarrow> (\<forall>x\<in>set as. \<forall>y\<in>set bs. x \<le> y) \<Longrightarrow> increasing ls
[PROOF STEP]
apply (simp add: increasing_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>as bs. ls = as @ bs \<longrightarrow> (\<forall>x\<in>set as. \<forall>y\<in>set bs. x \<le> y) \<Longrightarrow> \<forall>x y. (\<exists>as bs. ls = as @ x # y # bs) \<longrightarrow> x \<le> y
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y as bs. \<lbrakk>\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y); ls = as @ x # y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y as bs. \<lbrakk>\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y); ls = as @ x # y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
fix as bs x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y as bs. \<lbrakk>\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y); ls = as @ x # y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
assume p: "\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y)"
[PROOF STATE]
proof (state)
this:
\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y)

goal (1 subgoal):
 1. \<And>x y as bs. \<lbrakk>\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y); ls = as @ x # y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y)
[PROOF STEP]
have p': "\<And> asa bsa. as @ x # y # bs = asa @ bsa \<Longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y)"
[PROOF STATE]
proof (prove)
using this:
\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y)

goal (1 subgoal):
 1. \<And>asa bsa. as @ x # y # bs = asa @ bsa \<Longrightarrow> \<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
as @ x # y # bs = ?asa @ ?bsa \<Longrightarrow> \<forall>x\<in>set ?asa. \<forall>y\<in>set ?bsa. x \<le> y

goal (1 subgoal):
 1. \<And>x y as bs. \<lbrakk>\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y); ls = as @ x # y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as @ x # y # bs = ?asa @ ?bsa \<Longrightarrow> \<forall>x\<in>set ?asa. \<forall>y\<in>set ?bsa. x \<le> y
[PROOF STEP]
have "(\<forall>x\<in>set (as @ [x]). \<forall>y\<in>set (y # bs). x \<le> y)"
[PROOF STATE]
proof (prove)
using this:
as @ x # y # bs = ?asa @ ?bsa \<Longrightarrow> \<forall>x\<in>set ?asa. \<forall>y\<in>set ?bsa. x \<le> y

goal (1 subgoal):
 1. \<forall>x\<in>set (as @ [x]). \<forall>y\<in>set (y # bs). x \<le> y
[PROOF STEP]
by (rule_tac p') auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (as @ [x]). \<forall>y\<in>set (y # bs). x \<le> y

goal (1 subgoal):
 1. \<And>x y as bs. \<lbrakk>\<forall>asa bsa. as @ x # y # bs = asa @ bsa \<longrightarrow> (\<forall>x\<in>set asa. \<forall>y\<in>set bsa. x \<le> y); ls = as @ x # y # bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set (as @ [x]). \<forall>y\<in>set (y # bs). x \<le> y
[PROOF STEP]
show "x \<le> y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (as @ [x]). \<forall>y\<in>set (y # bs). x \<le> y

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by (auto simp: increasing_def)
[PROOF STATE]
proof (state)
this:
x \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma increasing4: "increasing (as@bs) \<Longrightarrow> increasing as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. increasing (as @ bs) \<Longrightarrow> increasing as
[PROOF STEP]
apply (simp add: increasing_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (\<exists>asa bsa. as @ bs = asa @ x # y # bsa) \<longrightarrow> x \<le> y \<Longrightarrow> \<forall>x y. (\<exists>asa bs. as = asa @ x # y # bs) \<longrightarrow> x \<le> y
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y asa bsa. \<lbrakk>\<forall>xa ya. (\<exists>as bsb. (asa @ x # y # bsa) @ bs = as @ xa # ya # bsb) \<longrightarrow> xa \<le> ya; as = asa @ x # y # bsa\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
by auto


[STATEMENT]
lemma increasing5: "increasing (as@bs) \<Longrightarrow> increasing bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. increasing (as @ bs) \<Longrightarrow> increasing bs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. increasing (as @ bs) \<Longrightarrow> increasing bs
[PROOF STEP]
assume nd: "increasing (as@bs)"
[PROOF STATE]
proof (state)
this:
increasing (as @ bs)

goal (1 subgoal):
 1. increasing (as @ bs) \<Longrightarrow> increasing bs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
increasing (as @ bs)
[PROOF STEP]
have r: "\<And> x y asa bsa. (\<exists>asa bsa. as @ bs = asa @ x # y # bsa) \<Longrightarrow> x \<le> y"
[PROOF STATE]
proof (prove)
using this:
increasing (as @ bs)

goal (1 subgoal):
 1. \<And>x y asa bsa. \<exists>asa bsa. as @ bs = asa @ x # y # bsa \<Longrightarrow> x \<le> y
[PROOF STEP]
by (auto simp: increasing_def)
[PROOF STATE]
proof (state)
this:
\<exists>asa bsa. as @ bs = asa @ ?x # ?y # bsa \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. increasing (as @ bs) \<Longrightarrow> increasing bs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. increasing bs
[PROOF STEP]
apply (clarsimp simp add: increasing_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y as bsa. bs = as @ x # y # bsa \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (rule_tac r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y asa bsa. bs = asa @ x # y # bsa \<Longrightarrow> \<exists>asa bsa. as @ bs = asa @ x # y # bsa
[PROOF STEP]
apply (rule_tac x="as @ _" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y asa bsa. bs = asa @ x # y # bsa \<Longrightarrow> \<exists>bsaa. as @ bs = (as @ ?uu15 x y asa bsa) @ x # y # bsaa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
increasing bs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enumBase_length: "ls \<in> set (enumBase nmax) \<Longrightarrow> length ls = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumBase nmax) \<Longrightarrow> |ls| = 1
[PROOF STEP]
by (auto simp: enumBase_def)


[STATEMENT]
lemma enumBase_bound: "\<forall>y \<in> set (enumBase nmax). \<forall>z \<in> set y. z \<le> nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>set (enumBase nmax). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
by (auto simp: enumBase_def)


[STATEMENT]
lemma enumAppend_bound: "ls \<in> set ((enumAppend nmax) lss) \<Longrightarrow>
 \<forall> y \<in> set lss. \<forall> z \<in> set y. z \<le> nmax \<Longrightarrow> x \<in> set ls \<Longrightarrow> x \<le>  nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumAppend nmax lss); \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax; x \<in> set ls\<rbrakk> \<Longrightarrow> x \<le> nmax
[PROOF STEP]
by (auto simp add: enumAppend_def split: if_split_asm)


[STATEMENT]
lemma enumAppend_bound_rec: "ls \<in> set (((enumAppend nmax) ^^ n) lss) \<Longrightarrow>
  \<forall> y \<in> set lss. \<forall> z \<in> set y. z \<le> nmax \<Longrightarrow> x \<in> set ls \<Longrightarrow> x \<le>  nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax; x \<in> set ls\<rbrakk> \<Longrightarrow> x \<le> nmax
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax; x \<in> set ls\<rbrakk> \<Longrightarrow> x \<le> nmax
[PROOF STEP]
assume ls: "ls \<in> set ((enumAppend nmax ^^ n) lss)" and lss: "\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax" and x: "x \<in> set ls"
[PROOF STATE]
proof (state)
this:
ls \<in> set ((enumAppend nmax ^^ n) lss)
\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax
x \<in> set ls

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax; x \<in> set ls\<rbrakk> \<Longrightarrow> x \<le> nmax
[PROOF STEP]
have ind:"\<And> lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall> y \<in> set (((enumAppend nmax) ^^ n) lss). \<forall> z \<in> set y. z \<le> nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ 0) lss). \<forall>z\<in>set y. z \<le> nmax
 2. \<And>n lss. \<lbrakk>\<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax; \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ Suc n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax

goal (2 subgoals):
 1. \<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ 0) lss). \<forall>z\<in>set y. z \<le> nmax
 2. \<And>n lss. \<lbrakk>\<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax; \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ Suc n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax

goal (1 subgoal):
 1. \<forall>y\<in>set ((enumAppend nmax ^^ 0) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set ((enumAppend nmax ^^ 0) lss). \<forall>z\<in>set y. z \<le> nmax

goal (1 subgoal):
 1. \<And>n lss. \<lbrakk>\<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax; \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ Suc n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n lss. \<lbrakk>\<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax; \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ Suc n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set ?lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) ?lss). \<forall>z\<in>set y. z \<le> nmax
\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax

goal (1 subgoal):
 1. \<And>n lss. \<lbrakk>\<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax; \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ Suc n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>set ((enumAppend nmax ^^ Suc n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
apply (intro ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>y \<in> set ((enumAppend nmax ^^ Suc n) lss); z \<in> set y\<rbrakk> \<Longrightarrow> z \<le> nmax
[PROOF STEP]
apply (rule enumAppend_bound)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y z. \<lbrakk>y \<in> set ((enumAppend nmax ^^ Suc n) lss); z \<in> set y\<rbrakk> \<Longrightarrow> ?ls2 y z \<in> set (enumAppend nmax (?lss2 y z))
 2. \<And>y z. \<lbrakk>y \<in> set ((enumAppend nmax ^^ Suc n) lss); z \<in> set y\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (?lss2 y z). \<forall>z\<in>set y. z \<le> nmax
 3. \<And>y z. \<lbrakk>y \<in> set ((enumAppend nmax ^^ Suc n) lss); z \<in> set y\<rbrakk> \<Longrightarrow> z \<in> set (?ls2 y z)
[PROOF STEP]
by (auto intro!: Suc)
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set ((enumAppend nmax ^^ Suc n) lss). \<forall>z\<in>set y. z \<le> nmax

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set ?lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) ?lss). \<forall>z\<in>set y. z \<le> nmax

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax; x \<in> set ls\<rbrakk> \<Longrightarrow> x \<le> nmax
[PROOF STEP]
with lss
[PROOF STATE]
proof (chain)
picking this:
\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax
\<forall>y\<in>set ?lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) ?lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
have "\<forall> y \<in> set (((enumAppend nmax) ^^ n) lss). \<forall> z \<in> set y. z \<le> nmax"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax
\<forall>y\<in>set ?lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) ?lss). \<forall>z\<in>set y. z \<le> nmax

goal (1 subgoal):
 1. \<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
apply (rule_tac ind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax; \<And>lss. \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax \<Longrightarrow> \<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax\<rbrakk> \<Longrightarrow> \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<forall>y\<in>set lss. \<forall>z\<in>set y. z \<le> nmax; x \<in> set ls\<rbrakk> \<Longrightarrow> x \<le> nmax
[PROOF STEP]
with ls x
[PROOF STATE]
proof (chain)
picking this:
ls \<in> set ((enumAppend nmax ^^ n) lss)
x \<in> set ls
\<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ls \<in> set ((enumAppend nmax ^^ n) lss)
x \<in> set ls
\<forall>y\<in>set ((enumAppend nmax ^^ n) lss). \<forall>z\<in>set y. z \<le> nmax

goal (1 subgoal):
 1. x \<le> nmax
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<le> nmax

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enumAppend_increase_rec:
  "\<And> m as bs. ls \<in> set (((enumAppend nmax) ^^ m) (enumBase nmax)) \<Longrightarrow>
  as @ bs = ls \<Longrightarrow>  \<forall> x \<in> set as. \<forall> y \<in> set bs. x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m as bs. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = ls\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>y\<in>set bs. x \<le> y
[PROOF STEP]
apply (induct ls rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m as bs. \<lbrakk>[] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. Ball (set bs) ((\<le>) x)
 2. \<And>x xs m as bs. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. Ball (set bs) ((\<le>) x); xs @ [x] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs @ [x]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. Ball (set bs) ((\<le>) x)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs m as bs. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. Ball (set bs) ((\<le>) x); xs @ [x] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs @ [x]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. Ball (set bs) ((\<le>) x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs m as bs xa xb. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
apply (case_tac "m")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs m as bs xa xb. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = 0\<rbrakk> \<Longrightarrow> xa \<le> xb
 2. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs m as bs xa xb. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumBase nmax); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = 0\<rbrakk> \<Longrightarrow> xa \<le> xb
 2. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
apply (drule_tac enumBase_length)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs m as bs xa xb. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = 0; |xs @ [x]| = 1\<rbrakk> \<Longrightarrow> xa \<le> xb
 2. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
apply (case_tac as)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xs m as bs xa xb. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = 0; |xs @ [x]| = 1; as = []\<rbrakk> \<Longrightarrow> xa \<le> xb
 2. \<And>x xs m as bs xa xb a list. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = 0; |xs @ [x]| = 1; as = a # list\<rbrakk> \<Longrightarrow> xa \<le> xb
 3. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
fix x xs m as bs xa xb n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
assume ih: "\<And>m as bs.
           \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk>
           \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa"
    and xs:"xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))"
    and asbs: "as @ bs = xs @ [x]" and xa:"xa \<in> set as" and xb: "xb \<in> set bs" and m: "m = Suc n"
[PROOF STATE]
proof (state)
this:
\<lbrakk>xs \<in> set ((enumAppend nmax ^^ ?m) (enumBase nmax)); ?as @ ?bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ?as. \<forall>xa\<in>set ?bs. x \<le> xa
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))
as @ bs = xs @ [x]
xa \<in> set as
xb \<in> set bs
m = Suc n

goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
from ih
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>xs \<in> set ((enumAppend nmax ^^ ?m) (enumBase nmax)); ?as @ ?bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ?as. \<forall>xa\<in>set ?bs. x \<le> xa
[PROOF STEP]
have ih2: "\<And> as bs x y. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ n) (enumBase nmax)); as @ bs = xs; x \<in> set as; y \<in> set bs\<rbrakk>
           \<Longrightarrow> x \<le> y"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>xs \<in> set ((enumAppend nmax ^^ ?m) (enumBase nmax)); ?as @ ?bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ?as. \<forall>xa\<in>set ?bs. x \<le> xa

goal (1 subgoal):
 1. \<And>as bs x y. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ n) (enumBase nmax)); as @ bs = xs; x \<in> set as; y \<in> set bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>xs \<in> set ((enumAppend nmax ^^ n) (enumBase nmax)); ?as @ ?bs = xs; ?x \<in> set ?as; ?y \<in> set ?bs\<rbrakk> \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
from xb
[PROOF STATE]
proof (chain)
picking this:
xb \<in> set bs
[PROOF STEP]
have "bs \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
xb \<in> set bs

goal (1 subgoal):
 1. bs \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bs \<noteq> []

goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bs \<noteq> []
[PROOF STEP]
obtain bs' b where bs': "bs = bs' @ [b]"
[PROOF STATE]
proof (prove)
using this:
bs \<noteq> []

goal (1 subgoal):
 1. (\<And>bs' b. bs = bs' @ [b] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases rule: rev_exhaust)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>bs' b. bs = bs' @ [b] \<Longrightarrow> thesis; bs \<noteq> []; ?xs3 = []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>ys y. \<lbrakk>\<And>bs' b. bs = bs' @ [b] \<Longrightarrow> thesis; bs \<noteq> []; ?xs3 = ys @ [y]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bs = bs' @ [b]

goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
with asbs
[PROOF STATE]
proof (chain)
picking this:
as @ bs = xs @ [x]
bs = bs' @ [b]
[PROOF STEP]
have beq:"b = x"
[PROOF STATE]
proof (prove)
using this:
as @ bs = xs @ [x]
bs = bs' @ [b]

goal (1 subgoal):
 1. b = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = x

goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
from bs' asbs
[PROOF STATE]
proof (chain)
picking this:
bs = bs' @ [b]
as @ bs = xs @ [x]
[PROOF STEP]
have xs': "as @ bs' = xs"
[PROOF STATE]
proof (prove)
using this:
bs = bs' @ [b]
as @ bs = xs @ [x]

goal (1 subgoal):
 1. as @ bs' = xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
as @ bs' = xs

goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
with xs
[PROOF STATE]
proof (chain)
picking this:
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))
as @ bs' = xs
[PROOF STEP]
have "xa \<le> x"
[PROOF STATE]
proof (prove)
using this:
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))
as @ bs' = xs

goal (1 subgoal):
 1. xa \<le> x
[PROOF STEP]
proof (cases "xs" rule: rev_exhaust)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); as @ bs' = xs; xs = []\<rbrakk> \<Longrightarrow> xa \<le> x
 2. \<And>ys y. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); as @ bs' = xs; xs = ys @ [y]\<rbrakk> \<Longrightarrow> xa \<le> x
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); as @ bs' = xs; xs = []\<rbrakk> \<Longrightarrow> xa \<le> x
 2. \<And>ys y. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); as @ bs' = xs; xs = ys @ [y]\<rbrakk> \<Longrightarrow> xa \<le> x
[PROOF STEP]
with xa xs'
[PROOF STATE]
proof (chain)
picking this:
xa \<in> set as
as @ bs' = xs
xs = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xa \<in> set as
as @ bs' = xs
xs = []

goal (1 subgoal):
 1. xa \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xa \<le> x

goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); as @ bs' = xs; xs = ys @ [y]\<rbrakk> \<Longrightarrow> xa \<le> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); as @ bs' = xs; xs = ys @ [y]\<rbrakk> \<Longrightarrow> xa \<le> x
[PROOF STEP]
case (snoc ys y)
[PROOF STATE]
proof (state)
this:
xs = ys @ [y]

goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); as @ bs' = xs; xs = ys @ [y]\<rbrakk> \<Longrightarrow> xa \<le> x
[PROOF STEP]
have "xa \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa \<le> y
[PROOF STEP]
proof (cases "xa = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xa = y \<Longrightarrow> xa \<le> y
 2. xa \<noteq> y \<Longrightarrow> xa \<le> y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xa = y

goal (2 subgoals):
 1. xa = y \<Longrightarrow> xa \<le> y
 2. xa \<noteq> y \<Longrightarrow> xa \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xa = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xa = y

goal (1 subgoal):
 1. xa \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xa \<le> y

goal (1 subgoal):
 1. xa \<noteq> y \<Longrightarrow> xa \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xa \<noteq> y \<Longrightarrow> xa \<le> y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xa \<noteq> y

goal (1 subgoal):
 1. xa \<noteq> y \<Longrightarrow> xa \<le> y
[PROOF STEP]
from xa xs'
[PROOF STATE]
proof (chain)
picking this:
xa \<in> set as
as @ bs' = xs
[PROOF STEP]
have "xa \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
xa \<in> set as
as @ bs' = xs

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

goal (1 subgoal):
 1. xa \<noteq> y \<Longrightarrow> xa \<le> y
[PROOF STEP]
with False snoc
[PROOF STATE]
proof (chain)
picking this:
xa \<noteq> y
xs = ys @ [y]
xa \<in> set xs
[PROOF STEP]
have "xa \<in> set ys"
[PROOF STATE]
proof (prove)
using this:
xa \<noteq> y
xs = ys @ [y]
xa \<in> set xs

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

goal (1 subgoal):
 1. xa \<noteq> y \<Longrightarrow> xa \<le> y
[PROOF STEP]
with xs snoc
[PROOF STATE]
proof (chain)
picking this:
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))
xs = ys @ [y]
xa \<in> set ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))
xs = ys @ [y]
xa \<in> set ys

goal (1 subgoal):
 1. xa \<le> y
[PROOF STEP]
apply (rule_tac ih2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); xs = ys @ [y]; xa \<in> set ys\<rbrakk> \<Longrightarrow> xs \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
 2. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); xs = ys @ [y]; xa \<in> set ys\<rbrakk> \<Longrightarrow> ?as3 @ ?bs3 = xs
 3. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); xs = ys @ [y]; xa \<in> set ys\<rbrakk> \<Longrightarrow> xa \<in> set ?as3
 4. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); xs = ys @ [y]; xa \<in> set ys\<rbrakk> \<Longrightarrow> y \<in> set ?bs3
[PROOF STEP]
by (auto simp: enumAppend_def)
[PROOF STATE]
proof (state)
this:
xa \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xa \<le> y

goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax))); as @ bs' = xs; xs = ys @ [y]\<rbrakk> \<Longrightarrow> xa \<le> x
[PROOF STEP]
with xs snoc
[PROOF STATE]
proof (chain)
picking this:
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))
xs = ys @ [y]
xa \<le> y
[PROOF STEP]
show "xa \<le> x"
[PROOF STATE]
proof (prove)
using this:
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))
xs = ys @ [y]
xa \<le> y

goal (1 subgoal):
 1. xa \<le> x
[PROOF STEP]
by (auto simp: enumAppend_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
xa \<le> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xa \<le> x

goal (1 subgoal):
 1. \<And>x xs m as bs xa xb nat. \<lbrakk>\<And>m as bs. \<lbrakk>xs \<in> set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>xa\<in>set bs. x \<le> xa; xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ nat) (enumBase nmax))); as @ bs = xs @ [x]; xa \<in> set as; xb \<in> set bs; m = Suc nat\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xa \<le> x
[PROOF STEP]
show "xa \<le> xb"
[PROOF STATE]
proof (prove)
using this:
xa \<le> x

goal (1 subgoal):
 1. xa \<le> xb
[PROOF STEP]
apply (cases "xb = b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xa \<le> x; xb = b\<rbrakk> \<Longrightarrow> xa \<le> xb
 2. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
apply (simp add: beq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xa \<le> xb
[PROOF STEP]
proof (rule_tac ih2)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xs \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
 2. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> ?as2 @ ?bs2 = xs
 3. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xa \<in> set ?as2
 4. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xb \<in> set ?bs2
[PROOF STEP]
from xs
[PROOF STATE]
proof (chain)
picking this:
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))
[PROOF STEP]
show "xs \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))"
[PROOF STATE]
proof (prove)
using this:
xs @ [x] \<in> set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))

goal (1 subgoal):
 1. xs \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))
[PROOF STEP]
by (auto simp: enumAppend_def)
[PROOF STATE]
proof (state)
this:
xs \<in> set ((enumAppend nmax ^^ n) (enumBase nmax))

goal (3 subgoals):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> ?as2 @ ?bs2 = xs
 2. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xa \<in> set ?as2
 3. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xb \<in> set ?bs2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> ?as2 @ ?bs2 = xs
 2. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xa \<in> set ?as2
 3. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xb \<in> set ?bs2
[PROOF STEP]
from xs'
[PROOF STATE]
proof (chain)
picking this:
as @ bs' = xs
[PROOF STEP]
show "as @ bs' = xs"
[PROOF STATE]
proof (prove)
using this:
as @ bs' = xs

goal (1 subgoal):
 1. as @ bs' = xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
as @ bs' = xs

goal (2 subgoals):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xa \<in> set as
 2. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xb \<in> set bs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xa \<in> set as
 2. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xb \<in> set bs'
[PROOF STEP]
from xa
[PROOF STATE]
proof (chain)
picking this:
xa \<in> set as
[PROOF STEP]
show "xa \<in> set as"
[PROOF STATE]
proof (prove)
using this:
xa \<in> set as

goal (1 subgoal):
 1. xa \<in> set as
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xa \<in> set as

goal (1 subgoal):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xb \<in> set bs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xb \<in> set bs'
[PROOF STEP]
assume "xb \<noteq> b"
[PROOF STATE]
proof (state)
this:
xb \<noteq> b

goal (1 subgoal):
 1. \<lbrakk>xa \<le> x; xb \<noteq> b\<rbrakk> \<Longrightarrow> xb \<in> set bs'
[PROOF STEP]
with xb bs'
[PROOF STATE]
proof (chain)
picking this:
xb \<in> set bs
bs = bs' @ [b]
xb \<noteq> b
[PROOF STEP]
show "xb \<in> set bs'"
[PROOF STATE]
proof (prove)
using this:
xb \<in> set bs
bs = bs' @ [b]
xb \<noteq> b

goal (1 subgoal):
 1. xb \<in> set bs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xb \<in> set bs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xa \<le> xb

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enumAppend_length1: "\<And>ls. ls \<in> set ((enumAppend nmax ^^ n) lss) \<Longrightarrow>
 (\<forall>l \<in> set lss. |l| = k) \<Longrightarrow> |ls| = k + n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ls. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<forall>l\<in>set lss. |l| = k\<rbrakk> \<Longrightarrow> |ls| = k + n
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ls. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ 0) lss); \<forall>l\<in>set lss. |l| = k\<rbrakk> \<Longrightarrow> |ls| = k + 0
 2. \<And>n ls. \<lbrakk>\<And>ls. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<forall>l\<in>set lss. |l| = k\<rbrakk> \<Longrightarrow> |ls| = k + n; ls \<in> set ((enumAppend nmax ^^ Suc n) lss); \<forall>l\<in>set lss. |l| = k\<rbrakk> \<Longrightarrow> |ls| = k + Suc n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n ls. \<lbrakk>\<And>ls. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<forall>l\<in>set lss. |l| = k\<rbrakk> \<Longrightarrow> |ls| = k + n; ls \<in> set ((enumAppend nmax ^^ Suc n) lss); \<forall>l\<in>set lss. |l| = k\<rbrakk> \<Longrightarrow> |ls| = k + Suc n
[PROOF STEP]
by (auto simp add:enumAppend_def split: if_split_asm)


[STATEMENT]
lemma enumAppend_length2: "\<And>ls. ls \<in> set ((enumAppend nmax ^^ n) lss) \<Longrightarrow>
 (\<And>l. l \<in> set lss \<Longrightarrow> |l| = k) \<Longrightarrow> K = k + n \<Longrightarrow> |ls| = K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ls. \<lbrakk>ls \<in> set ((enumAppend nmax ^^ n) lss); \<And>l. l \<in> set lss \<Longrightarrow> |l| = k; K = k + n\<rbrakk> \<Longrightarrow> |ls| = K
[PROOF STEP]
by (auto simp add: enumAppend_length1)


[STATEMENT]
lemma enum_enumerator:
 "enum i j = enumerator i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Enumerator.enum i j = enumerator i j
[PROOF STEP]
by(simp add: enum_def enumTab_def tabulate2_def tabulate_def)


[STATEMENT]
lemma enumerator_hd: "ls \<in> set (enumerator m n) \<Longrightarrow> hd ls = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m n) \<Longrightarrow> hd ls = 0
[PROOF STEP]
by (auto simp: enumerator_def split: if_split_asm)


[STATEMENT]
lemma enumerator_last: "ls \<in> set (enumerator m n) \<Longrightarrow> last ls = (n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m n) \<Longrightarrow> last ls = n - 1
[PROOF STEP]
by (auto simp: enumerator_def split: if_split_asm)


[STATEMENT]
lemma enumerator_length: "ls \<in> set (enumerator m n) \<Longrightarrow> 2 \<le> length ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m n) \<Longrightarrow> 2 \<le> |ls|
[PROOF STEP]
by (auto simp: enumerator_def split: if_split_asm)


[STATEMENT]
lemma enumerator_not_empty[dest]: "ls \<in> set (enumerator m n) \<Longrightarrow> ls \<noteq>  []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m n) \<Longrightarrow> ls \<noteq> []
[PROOF STEP]
apply (subgoal_tac "2 \<le> length ls")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ls \<in> set (enumerator m n); 2 \<le> |ls|\<rbrakk> \<Longrightarrow> ls \<noteq> []
 2. ls \<in> set (enumerator m n) \<Longrightarrow> 2 \<le> |ls|
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m n) \<Longrightarrow> 2 \<le> |ls|
[PROOF STEP]
by (rule enumerator_length)


[STATEMENT]
lemma enumerator_length2: "ls \<in> set (enumerator m n) \<Longrightarrow> 2 < m \<Longrightarrow> length ls = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m n); 2 < m\<rbrakk> \<Longrightarrow> |ls| = m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m n); 2 < m\<rbrakk> \<Longrightarrow> |ls| = m
[PROOF STEP]
assume ls:"ls \<in> set (enumerator m n)" and m: "2 < m"
[PROOF STATE]
proof (state)
this:
ls \<in> set (enumerator m n)
2 < m

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m n); 2 < m\<rbrakk> \<Longrightarrow> |ls| = m
[PROOF STEP]
define k where "k = m - 3"
[PROOF STATE]
proof (state)
this:
k = m - 3

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m n); 2 < m\<rbrakk> \<Longrightarrow> |ls| = m
[PROOF STEP]
with m
[PROOF STATE]
proof (chain)
picking this:
2 < m
k = m - 3
[PROOF STEP]
have k: "m = k + 3"
[PROOF STATE]
proof (prove)
using this:
2 < m
k = m - 3

goal (1 subgoal):
 1. m = k + 3
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
m = k + 3

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m n); 2 < m\<rbrakk> \<Longrightarrow> |ls| = m
[PROOF STEP]
with ls
[PROOF STATE]
proof (chain)
picking this:
ls \<in> set (enumerator m n)
m = k + 3
[PROOF STEP]
have "ls \<in> set (enumerator (k+3) n)"
[PROOF STATE]
proof (prove)
using this:
ls \<in> set (enumerator m n)
m = k + 3

goal (1 subgoal):
 1. ls \<in> set (enumerator (k + 3) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls \<in> set (enumerator (k + 3) n)

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m n); 2 < m\<rbrakk> \<Longrightarrow> |ls| = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ls \<in> set (enumerator (k + 3) n)
[PROOF STEP]
have "length ls = k + 3"
[PROOF STATE]
proof (prove)
using this:
ls \<in> set (enumerator (k + 3) n)

goal (1 subgoal):
 1. |ls| = k + 3
[PROOF STEP]
apply (auto simp: enumerator_def enumBase_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is. \<lbrakk>is \<in> set ((enumAppend (n - 2) ^^ k) (map (\<lambda>i. [i]) [0..<n - 2] @ [[n - 2]])); ls = 0 # is @ [n - Suc 0]\<rbrakk> \<Longrightarrow> |is| = Suc k
[PROOF STEP]
apply (erule enumAppend_length2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is l. \<lbrakk>ls = 0 # is @ [n - Suc 0]; l \<in> set (map (\<lambda>i. [i]) [0..<n - 2] @ [[n - 2]])\<rbrakk> \<Longrightarrow> |l| = ?k5 is
 2. \<And>is. ls = 0 # is @ [n - Suc 0] \<Longrightarrow> Suc k = ?k5 is + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|ls| = k + 3

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m n); 2 < m\<rbrakk> \<Longrightarrow> |ls| = m
[PROOF STEP]
with k
[PROOF STATE]
proof (chain)
picking this:
m = k + 3
|ls| = k + 3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m = k + 3
|ls| = k + 3

goal (1 subgoal):
 1. |ls| = m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|ls| = m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enumerator_bound: "ls \<in> set (enumerator m nmax) \<Longrightarrow>
 0 < nmax \<Longrightarrow> x \<in> set ls \<Longrightarrow> x < nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m nmax); 0 < nmax; x \<in> set ls\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply (auto simp: enumerator_def split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is. \<lbrakk>0 < nmax; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); ls = 0 # is @ [nmax - Suc 0]; x \<in> set is\<rbrakk> \<Longrightarrow> x < nmax
[PROOF STEP]
apply (subgoal_tac "x \<le> nmax - 2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>is. \<lbrakk>0 < nmax; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); ls = 0 # is @ [nmax - Suc 0]; x \<in> set is; x \<le> nmax - 2\<rbrakk> \<Longrightarrow> x < nmax
 2. \<And>is. \<lbrakk>0 < nmax; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); ls = 0 # is @ [nmax - Suc 0]; x \<in> set is\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is. \<lbrakk>0 < nmax; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); ls = 0 # is @ [nmax - Suc 0]; x \<in> set is\<rbrakk> \<Longrightarrow> x \<le> nmax - 2
[PROOF STEP]
apply (rule_tac enumAppend_bound_rec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>is. \<lbrakk>0 < nmax; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); ls = 0 # is @ [nmax - Suc 0]; x \<in> set is\<rbrakk> \<Longrightarrow> ?ls33 is \<in> set ((enumAppend (nmax - 2) ^^ ?n33 is) (?lss33 is))
 2. \<And>is. \<lbrakk>0 < nmax; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); ls = 0 # is @ [nmax - Suc 0]; x \<in> set is\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (?lss33 is). \<forall>z\<in>set y. z \<le> nmax - 2
 3. \<And>is. \<lbrakk>0 < nmax; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); ls = 0 # is @ [nmax - Suc 0]; x \<in> set is\<rbrakk> \<Longrightarrow> x \<in> set (?ls33 is)
[PROOF STEP]
by(auto simp:enumBase_simps)


[STATEMENT]
lemma enumerator_bound3: "ls \<in> set (enumerator m nmax) \<Longrightarrow> 1 < nmax \<Longrightarrow> last (butlast ls) < nmax - Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax\<rbrakk> \<Longrightarrow> last (butlast ls) < nmax - Suc 0
[PROOF STEP]
apply (case_tac "ls" rule: rev_exhaust)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax; ls = []\<rbrakk> \<Longrightarrow> last (butlast ls) < nmax - Suc 0
 2. \<And>ys y. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax; ls = ys @ [y]\<rbrakk> \<Longrightarrow> last (butlast ls) < nmax - Suc 0
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax; ls = ys @ [y]\<rbrakk> \<Longrightarrow> last (butlast ls) < nmax - Suc 0
[PROOF STEP]
apply (rule_tac enumerator_bound2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ys y. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax; ls = ys @ [y]\<rbrakk> \<Longrightarrow> ?ls8 ys y \<in> set (enumerator (?m8 ys y) nmax)
 2. \<And>ys y. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax; ls = ys @ [y]\<rbrakk> \<Longrightarrow> 1 < nmax
 3. \<And>ys y. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax; ls = ys @ [y]\<rbrakk> \<Longrightarrow> last (butlast ls) \<in> set (butlast (?ls8 ys y))
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax; ls = ys @ [y]\<rbrakk> \<Longrightarrow> 1 < nmax
 2. \<And>ys y. \<lbrakk>ls \<in> set (enumerator m nmax); 1 < nmax; ls = ys @ [y]\<rbrakk> \<Longrightarrow> last (butlast ls) \<in> set (butlast ls)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>ys @ [y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = ys @ [y]\<rbrakk> \<Longrightarrow> last ys \<in> set ys
[PROOF STEP]
apply (case_tac "ys" rule: rev_exhaust)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>ys @ [y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = ys @ [y]; ys = []\<rbrakk> \<Longrightarrow> last ys \<in> set ys
 2. \<And>ys y ysa ya. \<lbrakk>ys @ [y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = ys @ [y]; ys = ysa @ [ya]\<rbrakk> \<Longrightarrow> last ys \<in> set ys
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>[y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = [y]; ys = []\<rbrakk> \<Longrightarrow> False
 2. \<And>ys y ysa ya. \<lbrakk>ys @ [y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = ys @ [y]; ys = ysa @ [ya]\<rbrakk> \<Longrightarrow> last ys \<in> set ys
[PROOF STEP]
apply (subgoal_tac "2 \<le> length (ys @ [y])")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ys y. \<lbrakk>[y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = [y]; ys = []; 2 \<le> |ys @ [y]|\<rbrakk> \<Longrightarrow> False
 2. \<And>ys y. \<lbrakk>[y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = [y]; ys = []\<rbrakk> \<Longrightarrow> 2 \<le> |ys @ [y]|
 3. \<And>ys y ysa ya. \<lbrakk>ys @ [y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = ys @ [y]; ys = ysa @ [ya]\<rbrakk> \<Longrightarrow> last ys \<in> set ys
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>[y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = [y]; ys = []\<rbrakk> \<Longrightarrow> 2 \<le> |ys @ [y]|
 2. \<And>ys y ysa ya. \<lbrakk>ys @ [y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = ys @ [y]; ys = ysa @ [ya]\<rbrakk> \<Longrightarrow> last ys \<in> set ys
[PROOF STEP]
apply (rule_tac enumerator_length)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>[y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = [y]; ys = []\<rbrakk> \<Longrightarrow> ys @ [y] \<in> set (enumerator (?m11 ys y) (?n11 ys y))
 2. \<And>ys y ysa ya. \<lbrakk>ys @ [y] \<in> set (enumerator m nmax); Suc 0 < nmax; ls = ys @ [y]; ys = ysa @ [ya]\<rbrakk> \<Longrightarrow> last ys \<in> set ys
[PROOF STEP]
by auto


[STATEMENT]
lemma enumerator_increase: "\<And> as bs. ls \<in> set (enumerator m nmax) \<Longrightarrow>  as @ bs = ls \<Longrightarrow> \<forall> x \<in> set as. \<forall> y \<in> set bs. x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>ls \<in> set (enumerator m nmax); as @ bs = ls\<rbrakk> \<Longrightarrow> \<forall>x\<in>set as. \<forall>y\<in>set bs. x \<le> y
[PROOF STEP]
apply (auto simp: enumerator_def del: Nat.diff_is_0_eq' split: if_split_asm intro: enumAppend_increase_rec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs is x y. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; as @ bs = 0 # is @ [nmax - Suc 0]; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x \<in> set as; y \<in> set bs\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (case_tac as)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs is x y. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; as @ bs = 0 # is @ [nmax - Suc 0]; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x \<in> set as; y \<in> set bs; as = []\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>as bs is x y a list. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; as @ bs = 0 # is @ [nmax - Suc 0]; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x \<in> set as; y \<in> set bs; as = a # list\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs is x y a list. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; as @ bs = 0 # is @ [nmax - Suc 0]; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x \<in> set as; y \<in> set bs; as = a # list\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs is x y list. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; list @ bs = is @ [nmax - Suc 0]; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x = 0 \<or> x \<in> set list; y \<in> set bs; as = 0 # list\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (case_tac bs rule: rev_exhaust)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs is x y list. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; list @ bs = is @ [nmax - Suc 0]; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x = 0 \<or> x \<in> set list; y \<in> set bs; as = 0 # list; bs = []\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<And>as bs is x y list ys ya. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; list @ bs = is @ [nmax - Suc 0]; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x = 0 \<or> x \<in> set list; y \<in> set bs; as = 0 # list; bs = ys @ [ya]\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs is x y list ys ya. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; list @ bs = is @ [nmax - Suc 0]; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x = 0 \<or> x \<in> set list; y \<in> set bs; as = 0 # list; bs = ys @ [ya]\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs is x y list ys. \<lbrakk>ls = 0 # is @ [nmax - Suc 0]; list @ ys = is; is \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x = 0 \<or> x \<in> set list; y = nmax - Suc 0 \<or> y \<in> set ys; as = 0 # list; bs = ys @ [nmax - Suc 0]\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x list ys. \<lbrakk>ls = 0 # list @ ys @ [nmax - Suc 0]; list @ ys \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x \<in> set list\<rbrakk> \<Longrightarrow> x \<le> nmax - Suc 0
 2. \<And>x y list ys. \<lbrakk>ls = 0 # list @ ys @ [nmax - Suc 0]; list @ ys \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x \<in> set list; y \<in> set ys\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (drule_tac enumAppend_bound_rec)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x list ys. \<lbrakk>ls = 0 # list @ ys @ [nmax - Suc 0]; x \<in> set list\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (enumBase (nmax - 2)). \<forall>z\<in>set y. z \<le> nmax - 2
 2. \<And>x list ys. \<lbrakk>ls = 0 # list @ ys @ [nmax - Suc 0]; x \<in> set list\<rbrakk> \<Longrightarrow> ?x17 x list ys \<in> set (list @ ys)
 3. \<And>x list ys. \<lbrakk>ls = 0 # list @ ys @ [nmax - Suc 0]; x \<in> set list; ?x17 x list ys \<le> nmax - 2\<rbrakk> \<Longrightarrow> x \<le> nmax - Suc 0
 4. \<And>x y list ys. \<lbrakk>ls = 0 # list @ ys @ [nmax - Suc 0]; list @ ys \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x \<in> set list; y \<in> set ys\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
apply (auto simp:enumBase_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y list ys. \<lbrakk>ls = 0 # list @ ys @ [nmax - Suc 0]; list @ ys \<in> set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2))); x \<in> set list; y \<in> set ys\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
by (auto dest!: enumAppend_increase_rec)


[STATEMENT]
lemma enumerator_increasing: "ls \<in> set (enumerator m nmax) \<Longrightarrow> increasing ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax) \<Longrightarrow> increasing ls
[PROOF STEP]
apply (rule increasing3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> set (enumerator m nmax) \<Longrightarrow> \<forall>as bs. ls = as @ bs \<longrightarrow> (\<forall>x\<in>set as. \<forall>y\<in>set bs. x \<le> y)
[PROOF STEP]
by (auto dest: enumerator_increase)


[STATEMENT]
lemma incrIndexList_1lem[simp]: "incrIndexList ls m nmax \<Longrightarrow> Suc 0 < m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> Suc 0 < m
[PROOF STEP]
by (unfold incrIndexList_def) simp


[STATEMENT]
lemma incrIndexList_1len[simp]: "incrIndexList ls m nmax \<Longrightarrow> Suc 0 < nmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> Suc 0 < nmax
[PROOF STEP]
by (unfold incrIndexList_def) simp


[STATEMENT]
lemma incrIndexList_help2[simp]: "incrIndexList ls m nmax \<Longrightarrow> hd ls = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList ls m nmax \<Longrightarrow> hd ls = 0
[PROOF STEP]
by (unfold incrIndexList_def) simp


[STATEMENT]
lemma incrIndexList_help21[simp]: "incrIndexList (l # ls) m nmax \<Longrightarrow> l = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incrIndexList (l # ls) m nmax \<Longrightarrow> l = 0
[PROOF STEP]
by (auto dest: incrIndexList_help2)