[STATEMENT]
lemma valid_fold_combine: "\<lbrakk>0 < fst w; ts = h # ts'; \<forall>t \<in> set ts. valid t; adjacent (fst w, l h - 1) ts';
    valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow>
      valid (fold combine ts' z) \<and>
      l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w
[PROOF STEP]
proof (induction ts' arbitrary: z ts h)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>z ts h. \<lbrakk>0 < fst w; ts = [h]; Ball (set ts) local.valid; adjacent (fst w, l h - 1) []; local.valid z; z \<noteq> Leaf; l z = (case [] of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine [] z) \<and> l (fold combine [] z) = fst w \<and> r (fold combine [] z) = snd w
 2. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
0 < fst w
ts = [h]
Ball (set ts) local.valid
adjacent (fst w, l h - 1) []
local.valid z
z \<noteq> Leaf
l z = (case [] of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r z = snd w

goal (2 subgoals):
 1. \<And>z ts h. \<lbrakk>0 < fst w; ts = [h]; Ball (set ts) local.valid; adjacent (fst w, l h - 1) []; local.valid z; z \<noteq> Leaf; l z = (case [] of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine [] z) \<and> l (fold combine [] z) = fst w \<and> r (fold combine [] z) = snd w
 2. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
ts = [h]
Ball (set ts) local.valid
adjacent (fst w, l h - 1) []
local.valid z
z \<noteq> Leaf
l z = (case [] of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r z = snd w
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < fst w
ts = [h]
Ball (set ts) local.valid
adjacent (fst w, l h - 1) []
local.valid z
z \<noteq> Leaf
l z = (case [] of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r z = snd w

goal (1 subgoal):
 1. local.valid (fold combine [] z) \<and> l (fold combine [] z) = fst w \<and> r (fold combine [] z) = snd w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.valid (fold combine [] z) \<and> l (fold combine [] z) = fst w \<and> r (fold combine [] z) = snd w

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
case (Cons a ts')
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < fst w; ?ts = ?h # ts'; Ball (set ?ts) local.valid; adjacent (fst w, l ?h - 1) ts'; local.valid ?z; ?z \<noteq> Leaf; l ?z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r ?z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' ?z) \<and> l (fold combine ts' ?z) = fst w \<and> r (fold combine ts' ?z) = snd w
0 < fst w
ts = h # a # ts'
Ball (set ts) local.valid
adjacent (fst w, l h - 1) (a # ts')
local.valid z
z \<noteq> Leaf
l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r z = snd w

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < fst w; ?ts = ?h # ts'; Ball (set ?ts) local.valid; adjacent (fst w, l ?h - 1) ts'; local.valid ?z; ?z \<noteq> Leaf; l ?z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r ?z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' ?z) \<and> l (fold combine ts' ?z) = fst w \<and> r (fold combine ts' ?z) = snd w
0 < fst w
ts = h # a # ts'
Ball (set ts) local.valid
adjacent (fst w, l h - 1) (a # ts')
local.valid z
z \<noteq> Leaf
l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r z = snd w

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
from Cons(3-4)
[PROOF STATE]
proof (chain)
picking this:
ts = h # a # ts'
Ball (set ts) local.valid
[PROOF STEP]
have "valid a"
[PROOF STATE]
proof (prove)
using this:
ts = h # a # ts'
Ball (set ts) local.valid

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

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.valid a

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
from Cons(5)
[PROOF STATE]
proof (chain)
picking this:
adjacent (fst w, l h - 1) (a # ts')
[PROOF STEP]
have "adjacent (fst w, l a - Suc 0) ts'"
[PROOF STATE]
proof (prove)
using this:
adjacent (fst w, l h - 1) (a # ts')

goal (1 subgoal):
 1. adjacent (fst w, l a - Suc 0) ts'
[PROOF STEP]
unfolding adjacent_Cons
[PROOF STATE]
proof (prove)
using this:
a \<noteq> Leaf \<and> r a = snd (fst w, l h - 1) \<and> (case ts' of [] \<Rightarrow> l a = fst (fst w, l h - 1) | u # us \<Rightarrow> adjacent (fst (fst w, l h - 1), r u) ts' \<and> l a = Suc (r u))

goal (1 subgoal):
 1. adjacent (fst w, l a - Suc 0) ts'
[PROOF STEP]
by (auto split: list.splits)
[PROOF STATE]
proof (state)
this:
adjacent (fst w, l a - Suc 0) ts'

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
adjacent (fst w, l a - Suc 0) ts'

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
from Cons(2-6,8)
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
ts = h # a # ts'
Ball (set ts) local.valid
adjacent (fst w, l h - 1) (a # ts')
local.valid z
l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
[PROOF STEP]
have "valid (combine a z)"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
ts = h # a # ts'
Ball (set ts) local.valid
adjacent (fst w, l h - 1) (a # ts')
local.valid z
l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))

goal (1 subgoal):
 1. local.valid (combine a z)
[PROOF STEP]
unfolding adjacent_Cons
[PROOF STATE]
proof (prove)
using this:
0 < fst w
ts = h # a # ts'
Ball (set ts) local.valid
a \<noteq> Leaf \<and> r a = snd (fst w, l h - 1) \<and> (case ts' of [] \<Rightarrow> l a = fst (fst w, l h - 1) | u # us \<Rightarrow> adjacent (fst (fst w, l h - 1), r u) ts' \<and> l a = Suc (r u))
local.valid z
l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))

goal (1 subgoal):
 1. local.valid (combine a z)
[PROOF STEP]
by (intro valid_combine_if_valid) (auto split: list.splits)
[PROOF STATE]
proof (state)
this:
local.valid (combine a z)

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.valid (combine a z)

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
from Cons(5,7)
[PROOF STATE]
proof (chain)
picking this:
adjacent (fst w, l h - 1) (a # ts')
z \<noteq> Leaf
[PROOF STEP]
have "combine a z \<noteq> Leaf"
[PROOF STATE]
proof (prove)
using this:
adjacent (fst w, l h - 1) (a # ts')
z \<noteq> Leaf

goal (1 subgoal):
 1. combine a z \<noteq> Leaf
[PROOF STEP]
by (intro combine_neq_Leaf_if_both_non_Leaf) (simp_all add: adjacent_Cons)
[PROOF STATE]
proof (state)
this:
combine a z \<noteq> Leaf

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
combine a z \<noteq> Leaf

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
from Cons(5,7)
[PROOF STATE]
proof (chain)
picking this:
adjacent (fst w, l h - 1) (a # ts')
z \<noteq> Leaf
[PROOF STEP]
have "l (combine a z) = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))"
[PROOF STATE]
proof (prove)
using this:
adjacent (fst w, l h - 1) (a # ts')
z \<noteq> Leaf

goal (1 subgoal):
 1. l (combine a z) = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
[PROOF STEP]
by (auto simp add: adjacent_def combine_non_Leaves split: list.splits)
[PROOF STATE]
proof (state)
this:
l (combine a z) = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l (combine a z) = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
from Cons(5,7,9)
[PROOF STATE]
proof (chain)
picking this:
adjacent (fst w, l h - 1) (a # ts')
z \<noteq> Leaf
r z = snd w
[PROOF STEP]
have "r (combine a z) = snd w"
[PROOF STATE]
proof (prove)
using this:
adjacent (fst w, l h - 1) (a # ts')
z \<noteq> Leaf
r z = snd w

goal (1 subgoal):
 1. r (combine a z) = snd w
[PROOF STEP]
by (subst r_combine_non_Leaves) (auto simp add: adjacent_def)
[PROOF STATE]
proof (state)
this:
r (combine a z) = snd w

goal (1 subgoal):
 1. \<And>a ts' z ts h. \<lbrakk>\<And>z ts h. \<lbrakk>0 < fst w; ts = h # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) ts'; local.valid z; z \<noteq> Leaf; l z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' z) \<and> l (fold combine ts' z) = fst w \<and> r (fold combine ts' z) = snd w; 0 < fst w; ts = h # a # ts'; Ball (set ts) local.valid; adjacent (fst w, l h - 1) (a # ts'); local.valid z; z \<noteq> Leaf; l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < fst w; ?ts = ?h # ts'; Ball (set ?ts) local.valid; adjacent (fst w, l ?h - 1) ts'; local.valid ?z; ?z \<noteq> Leaf; l ?z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r ?z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' ?z) \<and> l (fold combine ts' ?z) = fst w \<and> r (fold combine ts' ?z) = snd w
0 < fst w
ts = h # a # ts'
Ball (set ts) local.valid
adjacent (fst w, l h - 1) (a # ts')
local.valid z
z \<noteq> Leaf
l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r z = snd w
local.valid a
adjacent (fst w, l a - Suc 0) ts'
local.valid (combine a z)
combine a z \<noteq> Leaf
l (combine a z) = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r (combine a z) = snd w
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < fst w; ?ts = ?h # ts'; Ball (set ?ts) local.valid; adjacent (fst w, l ?h - 1) ts'; local.valid ?z; ?z \<noteq> Leaf; l ?z = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1)); r ?z = snd w\<rbrakk> \<Longrightarrow> local.valid (fold combine ts' ?z) \<and> l (fold combine ts' ?z) = fst w \<and> r (fold combine ts' ?z) = snd w
0 < fst w
ts = h # a # ts'
Ball (set ts) local.valid
adjacent (fst w, l h - 1) (a # ts')
local.valid z
z \<noteq> Leaf
l z = (case a # ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r z = snd w
local.valid a
adjacent (fst w, l a - Suc 0) ts'
local.valid (combine a z)
combine a z \<noteq> Leaf
l (combine a z) = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
r (combine a z) = snd w

goal (1 subgoal):
 1. local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.valid (fold combine (a # ts') z) \<and> l (fold combine (a # ts') z) = fst w \<and> r (fold combine (a # ts') z) = snd w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_fold_combine_Leaf:
  assumes "0 < fst w" "ts = h # ts'" "\<forall>t \<in> set ts. valid t" "adjacent w ts"
  shows "valid (fold combine ts Leaf) \<and>
  l (fold combine ts Leaf) = fst w \<and> r (fold combine ts Leaf) = snd w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.valid (fold combine ts Leaf) \<and> l (fold combine ts Leaf) = fst w \<and> r (fold combine ts Leaf) = snd w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.valid (fold combine ts Leaf) \<and> l (fold combine ts Leaf) = fst w \<and> r (fold combine ts Leaf) = snd w
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
ts = h # ts'
[PROOF STEP]
have "fold combine ts Leaf = fold combine ts' h"
[PROOF STATE]
proof (prove)
using this:
ts = h # ts'

goal (1 subgoal):
 1. fold combine ts Leaf = fold combine ts' h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fold combine ts Leaf = fold combine ts' h

goal (1 subgoal):
 1. local.valid (fold combine ts Leaf) \<and> l (fold combine ts Leaf) = fst w \<and> r (fold combine ts Leaf) = snd w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fold combine ts Leaf = fold combine ts' h

goal (1 subgoal):
 1. local.valid (fold combine ts Leaf) \<and> l (fold combine ts Leaf) = fst w \<and> r (fold combine ts Leaf) = snd w
[PROOF STEP]
have "valid (fold combine ts' h) \<and>
    l (fold combine ts' h) = fst w \<and> r (fold combine ts' h) = snd w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.valid (fold combine ts' h) \<and> l (fold combine ts' h) = fst w \<and> r (fold combine ts' h) = snd w
[PROOF STEP]
proof (rule valid_fold_combine)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. 0 < fst w
 2. ?ts = ?h # ts'
 3. Ball (set ?ts) local.valid
 4. adjacent (fst w, l ?h - 1) ts'
 5. local.valid h
 6. h \<noteq> Leaf
 7. l h = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
 8. r h = snd w
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
ts = h # ts'
Ball (set ts) local.valid
adjacent w ts
[PROOF STEP]
show "0 < fst w" "ts = h # ts'" "\<forall>t \<in> set ts. valid t" "valid h" "h \<noteq> Leaf" "r h = snd w"
      "l h = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
ts = h # ts'
Ball (set ts) local.valid
adjacent w ts

goal (1 subgoal):
 1. (0 < fst w &&& ts = h # ts' &&& Ball (set ts) local.valid) &&& (local.valid h &&& h \<noteq> Leaf) &&& r h = snd w &&& l h = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))
[PROOF STEP]
by (simp_all add: adjacent_Cons list.case_eq_if)
[PROOF STATE]
proof (state)
this:
0 < fst w
ts = h # ts'
Ball (set ts) local.valid
local.valid h
h \<noteq> Leaf
r h = snd w
l h = (case ts' of [] \<Rightarrow> fst w | t\<^sub>1 # ts'' \<Rightarrow> Suc (r t\<^sub>1))

goal (1 subgoal):
 1. adjacent (fst w, l h - 1) ts'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
ts = h # ts'
Ball (set ts) local.valid
adjacent w ts
[PROOF STEP]
show "adjacent (fst w, l h - 1) ts'"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
ts = h # ts'
Ball (set ts) local.valid
adjacent w ts

goal (1 subgoal):
 1. adjacent (fst w, l h - 1) ts'
[PROOF STEP]
by (metis One_nat_def adjacent_Cons_implies_adjacent prod.collapse)
[PROOF STATE]
proof (state)
this:
adjacent (fst w, l h - 1) ts'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.valid (fold combine ts' h) \<and> l (fold combine ts' h) = fst w \<and> r (fold combine ts' h) = snd w

goal (1 subgoal):
 1. local.valid (fold combine ts Leaf) \<and> l (fold combine ts Leaf) = fst w \<and> r (fold combine ts Leaf) = snd w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fold combine ts Leaf = fold combine ts' h
local.valid (fold combine ts' h) \<and> l (fold combine ts' h) = fst w \<and> r (fold combine ts' h) = snd w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fold combine ts Leaf = fold combine ts' h
local.valid (fold combine ts' h) \<and> l (fold combine ts' h) = fst w \<and> r (fold combine ts' h) = snd w

goal (1 subgoal):
 1. local.valid (fold combine ts Leaf) \<and> l (fold combine ts Leaf) = fst w \<and> r (fold combine ts Leaf) = snd w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.valid (fold combine ts Leaf) \<and> l (fold combine ts Leaf) = fst w \<and> r (fold combine ts Leaf) = snd w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjacent_atomics_nonempty_reusables:
  fixes x :: "'a tree" and xs :: "'a tree list"
  assumes a1: "0 < fst w"
      and a2: "l t \<le> fst w"
      and a3: "r t \<le> snd w"
      and a4: "valid t"
      and a5: "reusables t w = x # xs"
  shows "adjacent (Suc (r x), snd w) (atomics (max (fst w) (Suc (r t))) (snd w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
have f6: "\<forall>p ts. adjacent p ts = ((Leaf::'a tree) \<notin> set ts \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst p \<and> r (hd ts) = snd p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p ts. adjacent p ts = (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst p \<and> r (hd ts) = snd p))
[PROOF STEP]
using adjacent_def
[PROOF STATE]
proof (prove)
using this:
adjacent ?w ?ts = (Leaf \<notin> set ?ts \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast ?ts) (tl ?ts) \<and> (?ts = [] \<or> l (last ?ts) = fst ?w \<and> r (hd ?ts) = snd ?w))

goal (1 subgoal):
 1. \<forall>p ts. adjacent p ts = (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst p \<and> r (hd ts) = snd p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p ts. adjacent p ts = (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst p \<and> r (hd ts) = snd p))

goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p ts. adjacent p ts = (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst p \<and> r (hd ts) = snd p))
[PROOF STEP]
have f7: "Leaf \<notin> set (atomics (max (fst w) (Suc (r t))) (snd w)) \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast (atomics (max (fst w) (Suc (r t))) (snd w))) (tl (atomics (max (fst w) (Suc (r t))) (snd w))) \<and> (atomics (max (fst w) (Suc (r t))) (snd w) = [] \<or> l (last (atomics (max (fst w) (Suc (r t))) (snd w))) = fst (max (fst w) (Suc (r t)), snd w) \<and> r (hd (atomics (max (fst w) (Suc (r t))) (snd w))) = snd (max (fst w) (Suc (r t)), snd w))"
[PROOF STATE]
proof (prove)
using this:
\<forall>p ts. adjacent p ts = (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst p \<and> r (hd ts) = snd p))

goal (1 subgoal):
 1. Leaf \<notin> set (local.atomics (max (fst w) (Suc (r t))) (snd w)) \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast (local.atomics (max (fst w) (Suc (r t))) (snd w))) (tl (local.atomics (max (fst w) (Suc (r t))) (snd w))) \<and> (local.atomics (max (fst w) (Suc (r t))) (snd w) = [] \<or> l (last (local.atomics (max (fst w) (Suc (r t))) (snd w))) = fst (max (fst w) (Suc (r t)), snd w) \<and> r (hd (local.atomics (max (fst w) (Suc (r t))) (snd w))) = snd (max (fst w) (Suc (r t)), snd w))
[PROOF STEP]
using adjacent_atomics
[PROOF STATE]
proof (prove)
using this:
\<forall>p ts. adjacent p ts = (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst p \<and> r (hd ts) = snd p))
adjacent (?i, ?j) (local.atomics ?i ?j)

goal (1 subgoal):
 1. Leaf \<notin> set (local.atomics (max (fst w) (Suc (r t))) (snd w)) \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast (local.atomics (max (fst w) (Suc (r t))) (snd w))) (tl (local.atomics (max (fst w) (Suc (r t))) (snd w))) \<and> (local.atomics (max (fst w) (Suc (r t))) (snd w) = [] \<or> l (last (local.atomics (max (fst w) (Suc (r t))) (snd w))) = fst (max (fst w) (Suc (r t)), snd w) \<and> r (hd (local.atomics (max (fst w) (Suc (r t))) (snd w))) = snd (max (fst w) (Suc (r t)), snd w))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
Leaf \<notin> set (local.atomics (max (fst w) (Suc (r t))) (snd w)) \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast (local.atomics (max (fst w) (Suc (r t))) (snd w))) (tl (local.atomics (max (fst w) (Suc (r t))) (snd w))) \<and> (local.atomics (max (fst w) (Suc (r t))) (snd w) = [] \<or> l (last (local.atomics (max (fst w) (Suc (r t))) (snd w))) = fst (max (fst w) (Suc (r t)), snd w) \<and> r (hd (local.atomics (max (fst w) (Suc (r t))) (snd w))) = snd (max (fst w) (Suc (r t)), snd w))

goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
have "adjacent (fst w, r t) (reusables t w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
using a4 a3 a2 a1
[PROOF STATE]
proof (prove)
using this:
local.valid t
r t \<le> snd w
l t \<le> fst w
0 < fst w

goal (1 subgoal):
 1. adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
by (simp add: adjacent_reusables valid_def)
[PROOF STATE]
proof (state)
this:
adjacent (fst w, r t) (reusables t w)

goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
have f8: "r x = r t"
[PROOF STATE]
proof (prove)
using this:
adjacent (fst w, r t) (reusables t w)

goal (1 subgoal):
 1. r x = r t
[PROOF STEP]
using a5
[PROOF STATE]
proof (prove)
using this:
adjacent (fst w, r t) (reusables t w)
reusables t w = x # xs

goal (1 subgoal):
 1. r x = r t
[PROOF STEP]
by (simp add: adjacent_Cons)
[PROOF STATE]
proof (state)
this:
r x = r t

goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
have "max (fst w) (Suc (r t)) = Suc (r t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (fst w) (Suc (r t)) = Suc (r t)
[PROOF STEP]
using a5
[PROOF STATE]
proof (prove)
using this:
reusables t w = x # xs

goal (1 subgoal):
 1. max (fst w) (Suc (r t)) = Suc (r t)
[PROOF STEP]
by (metis (no_types) Suc_n_not_le_n list.simps(3) max.bounded_iff max_def_raw not_le_imp_less reusables.simps)
[PROOF STATE]
proof (state)
this:
max (fst w) (Suc (r t)) = Suc (r t)

goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max (fst w) (Suc (r t)) = Suc (r t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
max (fst w) (Suc (r t)) = Suc (r t)

goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
using f8 f7 f6
[PROOF STATE]
proof (prove)
using this:
max (fst w) (Suc (r t)) = Suc (r t)
r x = r t
Leaf \<notin> set (local.atomics (max (fst w) (Suc (r t))) (snd w)) \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast (local.atomics (max (fst w) (Suc (r t))) (snd w))) (tl (local.atomics (max (fst w) (Suc (r t))) (snd w))) \<and> (local.atomics (max (fst w) (Suc (r t))) (snd w) = [] \<or> l (last (local.atomics (max (fst w) (Suc (r t))) (snd w))) = fst (max (fst w) (Suc (r t)), snd w) \<and> r (hd (local.atomics (max (fst w) (Suc (r t))) (snd w))) = snd (max (fst w) (Suc (r t)), snd w))
\<forall>p ts. adjacent p ts = (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t ta. l t = Suc (r ta)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst p \<and> r (hd ts) = snd p))

goal (1 subgoal):
 1. adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
adjacent (Suc (r x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjacent_Cons_r: "adjacent (a, r t) (x # xs) \<Longrightarrow> adjacent (a, r x) (x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent (a, r t) (x # xs) \<Longrightarrow> adjacent (a, r x) (x # xs)
[PROOF STEP]
by (simp add: adjacent_Cons)


[STATEMENT]
lemma adjacent_Cons_r2:
  "adjacent (fst w, r t) (x # xs) \<Longrightarrow> 0 < fst w \<Longrightarrow> fst w \<le> snd w \<Longrightarrow> r t \<le> snd w \<Longrightarrow>
   atomics (max (fst w) (Suc (r t))) (snd w) = [] \<Longrightarrow>
   adjacent w (x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>adjacent (fst w, r t) (x # xs); 0 < fst w; fst w \<le> snd w; r t \<le> snd w; local.atomics (max (fst w) (Suc (r t))) (snd w) = []\<rbrakk> \<Longrightarrow> adjacent w (x # xs)
[PROOF STEP]
by (metis (no_types, lifting) atomics_def adjacent_def append_is_Nil_conv diff_Suc_Suc diff_zero le_Suc_eq list.simps(3) map_is_Nil_conv max_Suc_Suc max_def_raw prod.sel(1) prod.sel(2) rev_is_Nil_conv upt.simps(2))


[STATEMENT]
lemma adjacent_append_atomics_reusables:
  "\<lbrakk>0 < fst w; fst w \<le> snd w; valid t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow>
    adjacent w (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; fst w \<le> snd w; local.valid t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)
[PROOF STEP]
using adjacent_atomics_nonempty_reusables[of w t] reusables_neq_Nil_if_well_shaped_and_overlapping[of t w]
    adjacent_atomics[of "fst w" "snd w"] adjacent_reusables[of w t]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < fst w; l t \<le> fst w; r t \<le> snd w; local.valid t; reusables t w = ?x # ?xs\<rbrakk> \<Longrightarrow> adjacent (Suc (r ?x), snd w) (local.atomics (max (fst w) (Suc (r t))) (snd w))
\<lbrakk>well_shaped t; l t \<le> fst w; r t \<le> snd w; fst w \<le> r t\<rbrakk> \<Longrightarrow> reusables t w \<noteq> []
adjacent (fst w, snd w) (local.atomics (fst w) (snd w))
\<lbrakk>0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)

goal (1 subgoal):
 1. \<lbrakk>0 < fst w; fst w \<le> snd w; local.valid t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)
[PROOF STEP]
by (intro adjacent_appendI) (auto simp: valid_def max.absorb1 atomize_not
    elim: adjacent_Cons_r adjacent_Cons_r2 split: list.splits nat.splits)


[STATEMENT]
lemma valid_append_atomics_reusables: "\<lbrakk>0 < fst w; valid t; l t \<le> fst w; r t \<le> snd w; snd w \<le> length as\<rbrakk> \<Longrightarrow>
  \<forall>t \<in> set (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w). valid t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; local.valid t; l t \<le> fst w; r t \<le> snd w; snd w \<le> length as\<rbrakk> \<Longrightarrow> Ball (set (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)) local.valid
[PROOF STEP]
by (auto simp only: set_append valid_reusables dest: valid_atomics split: if_splits)


[STATEMENT]
lemma append_atomics_reusables_neq_Nil: "\<lbrakk>0 < fst w; fst w \<le> snd w; valid t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow>
  atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; fst w \<le> snd w; local.valid t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w \<noteq> []
[PROOF STEP]
by (simp add: reusables_neq_Nil_if_well_shaped_and_overlapping valid_def atomics_def)


[STATEMENT]
lemma valid_slide:
  assumes "0 < fst w" "fst w \<le> snd w" "valid t" "l t \<le> fst w" "r t \<le> snd w" "snd w \<le> length as"
  shows "valid (slide t w) \<and> l (slide t w) = fst w \<and> r (slide t w) = snd w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.valid (local.slide t w) \<and> l (local.slide t w) = fst w \<and> r (local.slide t w) = snd w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.valid (local.slide t w) \<and> l (local.slide t w) = fst w \<and> r (local.slide t w) = snd w
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as
[PROOF STEP]
have non_empty: "atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as

goal (1 subgoal):
 1. local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w \<noteq> []
[PROOF STEP]
using append_atomics_reusables_neq_Nil
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as
\<lbrakk>0 < fst ?w; fst ?w \<le> snd ?w; local.valid ?t; l ?t \<le> fst ?w; r ?t \<le> snd ?w\<rbrakk> \<Longrightarrow> local.atomics (max (fst ?w) (Suc (r ?t))) (snd ?w) @ reusables ?t ?w \<noteq> []

goal (1 subgoal):
 1. local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w \<noteq> []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w \<noteq> []

goal (1 subgoal):
 1. local.valid (local.slide t w) \<and> l (local.slide t w) = fst w \<and> r (local.slide t w) = snd w
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as
[PROOF STEP]
have adjacent: "adjacent w (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as

goal (1 subgoal):
 1. adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)
[PROOF STEP]
using adjacent_append_atomics_reusables
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as
\<lbrakk>0 < fst ?w; fst ?w \<le> snd ?w; local.valid ?t; l ?t \<le> fst ?w; r ?t \<le> snd ?w\<rbrakk> \<Longrightarrow> adjacent ?w (local.atomics (max (fst ?w) (Suc (r ?t))) (snd ?w) @ reusables ?t ?w)

goal (1 subgoal):
 1. adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)

goal (1 subgoal):
 1. local.valid (local.slide t w) \<and> l (local.slide t w) = fst w \<and> r (local.slide t w) = snd w
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as
[PROOF STEP]
have valid: "\<forall>t \<in> set (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w). valid t"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as

goal (1 subgoal):
 1. Ball (set (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)) local.valid
[PROOF STEP]
using valid_append_atomics_reusables
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
local.valid t
l t \<le> fst w
r t \<le> snd w
snd w \<le> length as
\<lbrakk>0 < fst ?w; local.valid ?t; l ?t \<le> fst ?w; r ?t \<le> snd ?w; snd ?w \<le> length as\<rbrakk> \<Longrightarrow> Ball (set (local.atomics (max (fst ?w) (Suc (r ?t))) (snd ?w) @ reusables ?t ?w)) local.valid

goal (1 subgoal):
 1. Ball (set (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)) local.valid
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ball (set (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)) local.valid

goal (1 subgoal):
 1. local.valid (local.slide t w) \<and> l (local.slide t w) = fst w \<and> r (local.slide t w) = snd w
[PROOF STEP]
have *: "slide t w = fold combine (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.slide t w = fold combine (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf
[PROOF STEP]
by (simp add: slide_def)
[PROOF STATE]
proof (state)
this:
local.slide t w = fold combine (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf

goal (1 subgoal):
 1. local.valid (local.slide t w) \<and> l (local.slide t w) = fst w \<and> r (local.slide t w) = snd w
[PROOF STEP]
from assms(1) non_empty adjacent valid
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w \<noteq> []
adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)
Ball (set (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)) local.valid
[PROOF STEP]
show "valid (slide t w) \<and> l (slide t w) = fst w \<and> r (slide t w) = snd w"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w \<noteq> []
adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)
Ball (set (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)) local.valid

goal (1 subgoal):
 1. local.valid (local.slide t w) \<and> l (local.slide t w) = fst w \<and> r (local.slide t w) = snd w
[PROOF STEP]
unfolding * neq_Nil_conv
[PROOF STATE]
proof (prove)
using this:
0 < fst w
\<exists>y ys. local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w = y # ys
adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)
Ball (set (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)) local.valid

goal (1 subgoal):
 1. local.valid (fold combine (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf) \<and> l (fold combine (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf) = fst w \<and> r (fold combine (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf) = snd w
[PROOF STEP]
using valid_fold_combine_Leaf
[PROOF STATE]
proof (prove)
using this:
0 < fst w
\<exists>y ys. local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w = y # ys
adjacent w (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)
Ball (set (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)) local.valid
\<lbrakk>0 < fst ?w; ?ts = ?h # ?ts'; Ball (set ?ts) local.valid; adjacent ?w ?ts\<rbrakk> \<Longrightarrow> local.valid (fold combine ?ts Leaf) \<and> l (fold combine ?ts Leaf) = fst ?w \<and> r (fold combine ?ts Leaf) = snd ?w

goal (1 subgoal):
 1. local.valid (fold combine (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf) \<and> l (fold combine (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf) = fst w \<and> r (fold combine (local.atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf) = snd w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.valid (local.slide t w) \<and> l (local.slide t w) = fst w \<and> r (local.slide t w) = snd w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iterate_eq_map_sum: "\<lbrakk>valid t; windows as xs; (case xs of [] \<Rightarrow> True | x # xs' \<Rightarrow> l t \<le> fst x \<and> r t \<le> snd x)\<rbrakk> \<Longrightarrow>
  iterate t xs = map (\<lambda>w. sum (fst w) (snd w)) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.valid t; windows as xs; case xs of [] \<Rightarrow> True | x # xs' \<Rightarrow> l t \<le> fst x \<and> r t \<le> snd x\<rbrakk> \<Longrightarrow> local.iterate t xs = map (\<lambda>w. local.sum (fst w) (snd w)) xs
[PROOF STEP]
by (induction xs arbitrary: t)
    (auto simp: valid_slide windows_def window_def val_eq_Some_sum_if_valid_neq_Leaf neq_Leaf_if_l_gt0 split: list.split)


[STATEMENT]
theorem correctness: "windows as ws \<Longrightarrow> sliding_window = map (\<lambda>w. sum (fst w) (snd w)) ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. windows as ws \<Longrightarrow> local.sliding_window = map (\<lambda>w. local.sum (fst w) (snd w)) ws
[PROOF STEP]
by (auto simp only: sliding_window_def intro!: iterate_eq_map_sum)
    (auto simp: valid_def split: list.split)


[STATEMENT]
lemma slide_eq_slide':
  assumes "0 < fst w" "fst w \<le> snd w" "valid as t" "r t = length as" "l t \<le> fst w" "r t \<le> snd w" "snd w \<le> length (as @ as')"
  shows "slide (as @ as') t w = slide' as' t w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slide (as @ as') t w = slide' as' t w
[PROOF STEP]
proof (cases "r t = snd w")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r t = snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
 2. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r t = snd w

goal (2 subgoals):
 1. r t = snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
 2. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
r t = snd w
[PROOF STEP]
have *: "atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = []"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
r t = snd w

goal (1 subgoal):
 1. atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = []

goal (2 subgoals):
 1. r t = snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
 2. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
from True assms
[PROOF STATE]
proof (chain)
picking this:
r t = snd w
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
[PROOF STEP]
have "atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)) = []"
[PROOF STATE]
proof (prove)
using this:
r t = snd w
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')

goal (1 subgoal):
 1. atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)) = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)) = []

goal (2 subgoals):
 1. r t = snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
 2. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = []
atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)) = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = []
atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)) = []

goal (1 subgoal):
 1. slide (as @ as') t w = slide' as' t w
[PROOF STEP]
unfolding slide_def slide'_def atomics_def
[PROOF STATE]
proof (prove)
using this:
atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = []
atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)) = []

goal (1 subgoal):
 1. (let ts = atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1; ts' = reusables t w in fold combine (ts @ ts') Leaf) = (let ts = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)); ts' = reusables t w in fold combine (ts @ ts') Leaf)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slide (as @ as') t w = slide' as' t w

goal (1 subgoal):
 1. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r t \<noteq> snd w

goal (1 subgoal):
 1. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
r t \<noteq> snd w
[PROOF STEP]
have "r t < snd w"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
r t \<noteq> snd w

goal (1 subgoal):
 1. r t < snd w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r t < snd w

goal (1 subgoal):
 1. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
r t < snd w
[PROOF STEP]
have "atomic' (as @ as') (snd w) (snd w - Suc 0) = atomic' as' (snd w) (snd w - Suc (length as))"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
r t < snd w

goal (1 subgoal):
 1. atomic' (as @ as') (snd w) (snd w - Suc 0) = atomic' as' (snd w) (snd w - Suc (length as))
[PROOF STEP]
by (simp add: leD nth_append)
[PROOF STATE]
proof (state)
this:
atomic' (as @ as') (snd w) (snd w - Suc 0) = atomic' as' (snd w) (snd w - Suc (length as))

goal (1 subgoal):
 1. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
atomic' (as @ as') (snd w) (snd w - Suc 0) = atomic' as' (snd w) (snd w - Suc (length as))
[PROOF STEP]
have *: "\<forall>i. i \<in> set ([max (fst w) (Suc (length as))..<snd w]) \<longrightarrow> atomic' (as @ as') i (i - Suc 0) = atomic' as' i (i - Suc (length as))"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
atomic' (as @ as') (snd w) (snd w - Suc 0) = atomic' as' (snd w) (snd w - Suc (length as))

goal (1 subgoal):
 1. \<forall>i. i \<in> set [max (fst w) (Suc (length as))..<snd w] \<longrightarrow> atomic' (as @ as') i (i - Suc 0) = atomic' as' i (i - Suc (length as))
[PROOF STEP]
by (auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<in> set [max (fst w) (Suc (length as))..<snd w] \<longrightarrow> atomic' (as @ as') i (i - Suc 0) = atomic' as' i (i - Suc (length as))

goal (1 subgoal):
 1. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. i \<in> set [max (fst w) (Suc (length as))..<snd w] \<longrightarrow> atomic' (as @ as') i (i - Suc 0) = atomic' as' i (i - Suc (length as))
[PROOF STEP]
have "map (\<lambda>i. atomic' (as @ as') i (i - Suc 0)) (rev [max (fst w) (Suc (length as))..<snd w]) = map (\<lambda>b. atomic' as' b (b - Suc (r t))) (rev [max (fst w) (Suc (r t))..<snd w])"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i \<in> set [max (fst w) (Suc (length as))..<snd w] \<longrightarrow> atomic' (as @ as') i (i - Suc 0) = atomic' as' i (i - Suc (length as))

goal (1 subgoal):
 1. map (\<lambda>i. atomic' (as @ as') i (i - Suc 0)) (rev [max (fst w) (Suc (length as))..<snd w]) = map (\<lambda>b. atomic' as' b (b - Suc (r t))) (rev [max (fst w) (Suc (r t))..<snd w])
[PROOF STEP]
by (simp add: assms(4))
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. atomic' (as @ as') i (i - Suc 0)) (rev [max (fst w) (Suc (length as))..<snd w]) = map (\<lambda>b. atomic' as' b (b - Suc (r t))) (rev [max (fst w) (Suc (r t))..<snd w])

goal (1 subgoal):
 1. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
map (\<lambda>i. atomic' (as @ as') i (i - Suc 0)) (rev [max (fst w) (Suc (length as))..<snd w]) = map (\<lambda>b. atomic' as' b (b - Suc (r t))) (rev [max (fst w) (Suc (r t))..<snd w])
[PROOF STEP]
have "atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t))"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
r t = length as
l t \<le> fst w
r t \<le> snd w
snd w \<le> length (as @ as')
map (\<lambda>i. atomic' (as @ as') i (i - Suc 0)) (rev [max (fst w) (Suc (length as))..<snd w]) = map (\<lambda>b. atomic' as' b (b - Suc (r t))) (rev [max (fst w) (Suc (r t))..<snd w])

goal (1 subgoal):
 1. atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t))
[PROOF STEP]
by (auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t))

goal (1 subgoal):
 1. r t \<noteq> snd w \<Longrightarrow> slide (as @ as') t w = slide' as' t w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t))

goal (1 subgoal):
 1. slide (as @ as') t w = slide' as' t w
[PROOF STEP]
unfolding slide_def slide'_def atomics_def
[PROOF STATE]
proof (prove)
using this:
atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t))

goal (1 subgoal):
 1. (let ts = atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1; ts' = reusables t w in fold combine (ts @ ts') Leaf) = (let ts = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)); ts' = reusables t w in fold combine (ts @ ts') Leaf)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
slide (as @ as') t w = slide' as' t w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_eq_sum_append: "\<lbrakk>0 < i; i \<le> j; j \<le> length as\<rbrakk> \<Longrightarrow> sum as i j = sum (as @ as') i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; j \<le> length as\<rbrakk> \<Longrightarrow> SWA.sum as i j = SWA.sum (as @ as') i j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; j \<le> length as\<rbrakk> \<Longrightarrow> SWA.sum as i j = SWA.sum (as @ as') i j
[PROOF STEP]
assume assms: "0 < i" "i \<le> j" "j \<le> length as"
[PROOF STATE]
proof (state)
this:
0 < i
i \<le> j
j \<le> length as

goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; j \<le> length as\<rbrakk> \<Longrightarrow> SWA.sum as i j = SWA.sum (as @ as') i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < i
i \<le> j
j \<le> length as
[PROOF STEP]
have *: "rev (map ((!) as) [i - Suc 0..<j - Suc 0]) = rev (map ((!) (as@as')) [i - Suc 0..<j - Suc 0])"
[PROOF STATE]
proof (prove)
using this:
0 < i
i \<le> j
j \<le> length as

goal (1 subgoal):
 1. rev (map ((!) as) [i - Suc 0..<j - Suc 0]) = rev (map ((!) (as @ as')) [i - Suc 0..<j - Suc 0])
[PROOF STEP]
by (auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
rev (map ((!) as) [i - Suc 0..<j - Suc 0]) = rev (map ((!) (as @ as')) [i - Suc 0..<j - Suc 0])

goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; j \<le> length as\<rbrakk> \<Longrightarrow> SWA.sum as i j = SWA.sum (as @ as') i j
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < i
i \<le> j
j \<le> length as
[PROOF STEP]
have "as ! (j - Suc 0) = (as @ as') ! (j - Suc 0)"
[PROOF STATE]
proof (prove)
using this:
0 < i
i \<le> j
j \<le> length as

goal (1 subgoal):
 1. as ! (j - Suc 0) = (as @ as') ! (j - Suc 0)
[PROOF STEP]
by (auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
as ! (j - Suc 0) = (as @ as') ! (j - Suc 0)

goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; j \<le> length as\<rbrakk> \<Longrightarrow> SWA.sum as i j = SWA.sum (as @ as') i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as ! (j - Suc 0) = (as @ as') ! (j - Suc 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as ! (j - Suc 0) = (as @ as') ! (j - Suc 0)

goal (1 subgoal):
 1. SWA.sum as i j = SWA.sum (as @ as') i j
[PROOF STEP]
by (simp add: *)
[PROOF STATE]
proof (state)
this:
SWA.sum as i j = SWA.sum (as @ as') i j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma well_valued0_append: "\<lbrakk>well_shaped t; well_valued0 as t\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; well_valued0 as t\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') (Node x1 x2 x3 t1 t2)
[PROOF STEP]
case (Node i j a t1 t2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)

goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') (Node x1 x2 x3 t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)

goal (1 subgoal):
 1. well_valued0 (as @ as') (Node i j a t1 t2)
[PROOF STEP]
using sum_eq_sum_append
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
\<lbrakk>0 < ?i; ?i \<le> ?j; ?j \<le> length ?as\<rbrakk> \<Longrightarrow> SWA.sum ?as ?i ?j = SWA.sum (?as @ ?as') ?i ?j

goal (1 subgoal):
 1. well_valued0 (as @ as') (Node i j a t1 t2)
[PROOF STEP]
by (auto 4 0)
[PROOF STATE]
proof (state)
this:
well_valued0 (as @ as') (Node i j a t1 t2)

goal (1 subgoal):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf\<rbrakk> \<Longrightarrow> well_valued0 (as @ as') Leaf
[PROOF STEP]
qed simp


[STATEMENT]
lemma valid_append: "valid as t \<Longrightarrow> valid (as @ as') t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid as t \<Longrightarrow> valid (as @ as') t
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped t \<and> well_valued as t \<Longrightarrow> well_shaped t \<and> well_valued (as @ as') t
[PROOF STEP]
by (auto intro: well_valued0_append)


[STATEMENT]
lemma valid_slide_append: "\<lbrakk>0 < fst w; fst w \<le> snd w; valid as t; l t \<le> fst w; r t \<le> snd w; snd w \<le> length as + length as'\<rbrakk> \<Longrightarrow>
  valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; fst w \<le> snd w; valid as t; l t \<le> fst w; r t \<le> snd w; snd w \<le> length as + length as'\<rbrakk> \<Longrightarrow> valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w
[PROOF STEP]
by (auto simp: valid_append valid_slide)


[STATEMENT]
theorem valid_slide':
  assumes "0 < fst w" "fst w \<le> snd w" "valid as t" "length as = r t" "length as' \<ge> snd w - r t" "l t \<le> fst w" "r t \<le> snd w"
  shows "valid (as @ as') (slide' as' t w) \<and> l (slide' as' t w) = fst w \<and> r (slide' as' t w) = snd w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid (as @ as') (slide' as' t w) \<and> l (slide' as' t w) = fst w \<and> r (slide' as' t w) = snd w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid (as @ as') (slide' as' t w) \<and> l (slide' as' t w) = fst w \<and> r (slide' as' t w) = snd w
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
valid as t
length as = r t
snd w - r t \<le> length as'
l t \<le> fst w
r t \<le> snd w
[PROOF STEP]
have "valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w"
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
length as = r t
snd w - r t \<le> length as'
l t \<le> fst w
r t \<le> snd w

goal (1 subgoal):
 1. valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w
[PROOF STEP]
using valid_slide_append
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
length as = r t
snd w - r t \<le> length as'
l t \<le> fst w
r t \<le> snd w
\<lbrakk>0 < fst ?w; fst ?w \<le> snd ?w; valid ?as ?t; l ?t \<le> fst ?w; r ?t \<le> snd ?w; snd ?w \<le> length ?as + length ?as'\<rbrakk> \<Longrightarrow> valid (?as @ ?as') (slide (?as @ ?as') ?t ?w) \<and> l (slide (?as @ ?as') ?t ?w) = fst ?w \<and> r (slide (?as @ ?as') ?t ?w) = snd ?w

goal (1 subgoal):
 1. valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w
[PROOF STEP]
by (metis add_le_cancel_left le_add_diff_inverse)
[PROOF STATE]
proof (state)
this:
valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w

goal (1 subgoal):
 1. valid (as @ as') (slide' as' t w) \<and> l (slide' as' t w) = fst w \<and> r (slide' as' t w) = snd w
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
fst w \<le> snd w
valid as t
length as = r t
snd w - r t \<le> length as'
l t \<le> fst w
r t \<le> snd w
valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
length as = r t
snd w - r t \<le> length as'
l t \<le> fst w
r t \<le> snd w
valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w

goal (1 subgoal):
 1. valid (as @ as') (slide' as' t w) \<and> l (slide' as' t w) = fst w \<and> r (slide' as' t w) = snd w
[PROOF STEP]
using slide_eq_slide'
[PROOF STATE]
proof (prove)
using this:
0 < fst w
fst w \<le> snd w
valid as t
length as = r t
snd w - r t \<le> length as'
l t \<le> fst w
r t \<le> snd w
valid (as @ as') (slide (as @ as') t w) \<and> l (slide (as @ as') t w) = fst w \<and> r (slide (as @ as') t w) = snd w
\<lbrakk>0 < fst ?w; fst ?w \<le> snd ?w; valid ?as ?t; r ?t = length ?as; l ?t \<le> fst ?w; r ?t \<le> snd ?w; snd ?w \<le> length (?as @ ?as')\<rbrakk> \<Longrightarrow> slide (?as @ ?as') ?t ?w = slide' ?as' ?t ?w

goal (1 subgoal):
 1. valid (as @ as') (slide' as' t w) \<and> l (slide' as' t w) = fst w \<and> r (slide' as' t w) = snd w
[PROOF STEP]
by (metis add_le_cancel_left le_add_diff_inverse length_append)
[PROOF STATE]
proof (state)
this:
valid (as @ as') (slide' as' t w) \<and> l (slide' as' t w) = fst w \<and> r (slide' as' t w) = snd w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_tree_eq_Leaf_iff: "map_tree f t = Leaf \<longleftrightarrow> t = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_tree f t = Leaf) = (t = Leaf)
[PROOF STEP]
by simp


[STATEMENT]
lemma l_map_tree_eq_l[simp]: "l (map_tree f t) = l t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l (map_tree f t) = l t
[PROOF STEP]
by (cases t)
    (auto split: option.splits)


[STATEMENT]
lemma r_map_tree_eq_r[simp]: "r (map_tree f t) = r t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r (map_tree f t) = r t
[PROOF STEP]
by (cases t)
    (auto split: option.splits)


[STATEMENT]
lemma val_map_tree_neq_None: "val t \<noteq> None \<Longrightarrow> val (map_tree f t) \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val t \<noteq> None \<Longrightarrow> val (map_tree f t) \<noteq> None
[PROOF STEP]
by (cases t) auto


[STATEMENT]
lemma well_shaped_map_tree: "well_shaped t \<Longrightarrow> well_shaped (map_tree f t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped t \<Longrightarrow> well_shaped (map_tree f t)
[PROOF STEP]
by (induction t)
    (auto split: option.split)


[STATEMENT]
lemma fold_distr: "(\<forall>x y. f (x + y) = f x + f y) \<Longrightarrow> f (fold (+) list e) = fold (+) (map f list) (f e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. f (x + y) = f x + f y \<Longrightarrow> f (fold (+) list e) = fold (+) (map f list) (f e)
[PROOF STEP]
by (induction list arbitrary: e) auto


[STATEMENT]
lemma map_rev_map_nth_eq: "\<forall>x \<in> set xs. x < length as \<Longrightarrow> map f (rev (map ((!) as) xs)) = rev (map ((!) (map f as)) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. x < length as \<Longrightarrow> map f (rev (map ((!) as) xs)) = rev (map ((!) (map f as)) xs)
[PROOF STEP]
by (simp add: rev_map)


[STATEMENT]
lemma f_nth_eq_map_f_nth: "\<lbrakk>as \<noteq> []; length as \<ge> n\<rbrakk> \<Longrightarrow> f (as ! (n - Suc 0)) = map f as ! (n - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>as \<noteq> []; n \<le> length as\<rbrakk> \<Longrightarrow> f (as ! (n - Suc 0)) = map f as ! (n - Suc 0)
[PROOF STEP]
by (cases "n = length as") auto


[STATEMENT]
lemma well_valued0_map_map_tree:
   "\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t; well_valued0 as t; r t \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow>
     well_shaped (map_tree f t) \<and> well_valued0 (map f as) (map_tree f t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t; well_valued0 as t; r t \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_shaped (map_tree f t) \<and> well_valued0 (map f as) (map_tree f t)
[PROOF STEP]
proof (rule conjI[OF well_shaped_map_tree], assumption, induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped Leaf; well_valued0 as Leaf; r Leaf \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f Leaf)
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1); \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2); \<forall>x y. f (x + y) = f x + f y; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f (Node x1 x2 x3 t1 t2))
[PROOF STEP]
case (Node i j a t1 t2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1)
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2)
\<forall>x y. f (x + y) = f x + f y
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) \<le> length as
as \<noteq> []

goal (2 subgoals):
 1. \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped Leaf; well_valued0 as Leaf; r Leaf \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f Leaf)
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1); \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2); \<forall>x y. f (x + y) = f x + f y; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f (Node x1 x2 x3 t1 t2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1)
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2)
\<forall>x y. f (x + y) = f x + f y
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) \<le> length as
as \<noteq> []
[PROOF STEP]
have "map f (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) =
    rev (map ((!) (map f as)) [l t1 - Suc 0..<r t2 - Suc 0])"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1)
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2)
\<forall>x y. f (x + y) = f x + f y
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) \<le> length as
as \<noteq> []

goal (1 subgoal):
 1. map f (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) = rev (map ((!) (map f as)) [l t1 - Suc 0..<r t2 - Suc 0])
[PROOF STEP]
by (subst map_rev_map_nth_eq) auto
[PROOF STATE]
proof (state)
this:
map f (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) = rev (map ((!) (map f as)) [l t1 - Suc 0..<r t2 - Suc 0])

goal (2 subgoals):
 1. \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped Leaf; well_valued0 as Leaf; r Leaf \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f Leaf)
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1); \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2); \<forall>x y. f (x + y) = f x + f y; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f (Node x1 x2 x3 t1 t2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map f (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) = rev (map ((!) (map f as)) [l t1 - Suc 0..<r t2 - Suc 0])

goal (2 subgoals):
 1. \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped Leaf; well_valued0 as Leaf; r Leaf \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f Leaf)
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1); \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2); \<forall>x y. f (x + y) = f x + f y; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f (Node x1 x2 x3 t1 t2))
[PROOF STEP]
from Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1)
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2)
\<forall>x y. f (x + y) = f x + f y
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) \<le> length as
as \<noteq> []
[PROOF STEP]
have "r t1 \<le> length as"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1)
\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2)
\<forall>x y. f (x + y) = f x + f y
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) \<le> length as
as \<noteq> []

goal (1 subgoal):
 1. r t1 \<le> length as
[PROOF STEP]
by (cases t1) auto
[PROOF STATE]
proof (state)
this:
r t1 \<le> length as

goal (2 subgoals):
 1. \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped Leaf; well_valued0 as Leaf; r Leaf \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f Leaf)
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t1; well_valued0 as t1; r t1 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t1); \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped t2; well_valued0 as t2; r t2 \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f t2); \<forall>x y. f (x + y) = f x + f y; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f (Node x1 x2 x3 t1 t2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map f (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) = rev (map ((!) (map f as)) [l t1 - Suc 0..<r t2 - Suc 0])
r t1 \<le> length as
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
map f (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) = rev (map ((!) (map f as)) [l t1 - Suc 0..<r t2 - Suc 0])
r t1 \<le> length as

goal (1 subgoal):
 1. well_valued0 (map f as) (map_tree f (Node i j a t1 t2))
[PROOF STEP]
using Node(3-7)
[PROOF STATE]
proof (prove)
using this:
map f (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) = rev (map ((!) (map f as)) [l t1 - Suc 0..<r t2 - Suc 0])
r t1 \<le> length as
\<forall>x y. f (x + y) = f x + f y
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) \<le> length as
as \<noteq> []

goal (1 subgoal):
 1. well_valued0 (map f as) (map_tree f (Node i j a t1 t2))
[PROOF STEP]
by (auto simp: fold_distr[of f] val_map_tree_neq_None
      well_shaped_map_tree intro!: Node(1,2))
[PROOF STATE]
proof (state)
this:
well_valued0 (map f as) (map_tree f (Node i j a t1 t2))

goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. f (x + y) = f x + f y; well_shaped Leaf; well_valued0 as Leaf; r Leaf \<le> length as; as \<noteq> []\<rbrakk> \<Longrightarrow> well_valued0 (map f as) (map_tree f Leaf)
[PROOF STEP]
qed simp


[STATEMENT]
lemma valid_map_map_tree:
  assumes "\<forall>x y. f (x + y) = f x + f y" "valid as t" "r t \<le> length as"
  shows "valid (map f as) (map_tree f t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid (map f as) (map_tree f t)
[PROOF STEP]
proof (cases "as \<noteq> []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as \<noteq> [] \<Longrightarrow> valid (map f as) (map_tree f t)
 2. \<not> as \<noteq> [] \<Longrightarrow> valid (map f as) (map_tree f t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as \<noteq> []

goal (2 subgoals):
 1. as \<noteq> [] \<Longrightarrow> valid (map f as) (map_tree f t)
 2. \<not> as \<noteq> [] \<Longrightarrow> valid (map f as) (map_tree f t)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. f (x + y) = f x + f y
valid as t
r t \<le> length as
as \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. f (x + y) = f x + f y
valid as t
r t \<le> length as
as \<noteq> []

goal (1 subgoal):
 1. valid (map f as) (map_tree f t)
[PROOF STEP]
by (metis map_tree_eq_Leaf_iff val_map_tree_neq_None valid_def well_valued0_map_map_tree)
[PROOF STATE]
proof (state)
this:
valid (map f as) (map_tree f t)

goal (1 subgoal):
 1. \<not> as \<noteq> [] \<Longrightarrow> valid (map f as) (map_tree f t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> as \<noteq> [] \<Longrightarrow> valid (map f as) (map_tree f t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> as \<noteq> []

goal (1 subgoal):
 1. \<not> as \<noteq> [] \<Longrightarrow> valid (map f as) (map_tree f t)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. f (x + y) = f x + f y
valid as t
r t \<le> length as
\<not> as \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. f (x + y) = f x + f y
valid as t
r t \<le> length as
\<not> as \<noteq> []

goal (1 subgoal):
 1. valid (map f as) (map_tree f t)
[PROOF STEP]
by (metis le_zero_eq list.size(3) tree.exhaust_sel map_tree_eq_Leaf_iff valid_Leaf valid_def well_shaped.simps(2) well_valued0.simps(2))
[PROOF STATE]
proof (state)
this:
valid (map f as) (map_tree f t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_Nil_iff: "valid [] t \<longleftrightarrow> t = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid [] t = (t = Leaf)
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (well_shaped t \<and> well_valued [] t) = (t = Leaf)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. well_shaped t \<and> well_valued [] t \<Longrightarrow> t = Leaf
 2. t = Leaf \<Longrightarrow> well_shaped t \<and> well_valued [] t
[PROOF STEP]
assume "well_shaped t \<and> well_valued [] t"
[PROOF STATE]
proof (state)
this:
well_shaped t \<and> well_valued [] t

goal (2 subgoals):
 1. well_shaped t \<and> well_valued [] t \<Longrightarrow> t = Leaf
 2. t = Leaf \<Longrightarrow> well_shaped t \<and> well_valued [] t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_shaped t \<and> well_valued [] t
[PROOF STEP]
show "t = Leaf"
[PROOF STATE]
proof (prove)
using this:
well_shaped t \<and> well_valued [] t

goal (1 subgoal):
 1. t = Leaf
[PROOF STEP]
by (metis le_neq_implies_less list.size(3) not_less_zero tree.collapse well_shaped.simps(2) well_valued0.simps(2))
[PROOF STATE]
proof (state)
this:
t = Leaf

goal (1 subgoal):
 1. t = Leaf \<Longrightarrow> well_shaped t \<and> well_valued [] t
[PROOF STEP]
qed simp


[STATEMENT]
lemma update_rightmost_eq_Leaf_iff: "update_rightmost f t = Leaf \<longleftrightarrow> t = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (update_rightmost f t = Leaf) = (t = Leaf)
[PROOF STEP]
by (cases t)
    (auto split: option.splits)


[STATEMENT]
lemma l_update_rightmost_eq_l[simp]: "l (update_rightmost f t) = l t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l (update_rightmost f t) = l t
[PROOF STEP]
by (cases t)
    (auto split: option.splits)


[STATEMENT]
lemma r_update_rightmost_eq_r[simp]: "r (update_rightmost f t) = r t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r (update_rightmost f t) = r t
[PROOF STEP]
by (cases t)
    (auto split: option.splits)


[STATEMENT]
lemma val_update_rightmost_neq_None: "val t \<noteq> None \<Longrightarrow> val (update_rightmost f t) \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val t \<noteq> None \<Longrightarrow> val (update_rightmost f t) \<noteq> None
[PROOF STEP]
by (cases t) auto


[STATEMENT]
lemma well_shaped_update_rightmost: "well_shaped t \<Longrightarrow> well_shaped (update_rightmost f t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped t \<Longrightarrow> well_shaped (update_rightmost f t)
[PROOF STEP]
by (induction t)
    (auto simp: update_rightmost_eq_Leaf_iff split: option.split)


[STATEMENT]
lemma sum_eq_sum_prepend: "\<lbrakk>0 < i; i \<le> j; length xs < i; length ys = length xs\<rbrakk> \<Longrightarrow> sum (xs @ as) i j = sum (ys @ as) i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; length xs < i; length ys = length xs\<rbrakk> \<Longrightarrow> SWA.sum (xs @ as) i j = SWA.sum (ys @ as) i j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; length xs < i; length ys = length xs\<rbrakk> \<Longrightarrow> SWA.sum (xs @ as) i j = SWA.sum (ys @ as) i j
[PROOF STEP]
assume assms: "0 < i" "i \<le> j" "length xs < i" "length ys = length xs"
[PROOF STATE]
proof (state)
this:
0 < i
i \<le> j
length xs < i
length ys = length xs

goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; length xs < i; length ys = length xs\<rbrakk> \<Longrightarrow> SWA.sum (xs @ as) i j = SWA.sum (ys @ as) i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < i
i \<le> j
length xs < i
length ys = length xs
[PROOF STEP]
have *: "rev (map ((!) (xs @ as)) [i - Suc 0..<j - Suc 0]) = rev (map ((!) (ys @ as)) [i - Suc 0..<j - Suc 0])"
[PROOF STATE]
proof (prove)
using this:
0 < i
i \<le> j
length xs < i
length ys = length xs

goal (1 subgoal):
 1. rev (map ((!) (xs @ as)) [i - Suc 0..<j - Suc 0]) = rev (map ((!) (ys @ as)) [i - Suc 0..<j - Suc 0])
[PROOF STEP]
by (auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
rev (map ((!) (xs @ as)) [i - Suc 0..<j - Suc 0]) = rev (map ((!) (ys @ as)) [i - Suc 0..<j - Suc 0])

goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; length xs < i; length ys = length xs\<rbrakk> \<Longrightarrow> SWA.sum (xs @ as) i j = SWA.sum (ys @ as) i j
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < i
i \<le> j
length xs < i
length ys = length xs
[PROOF STEP]
have "(xs @ as) ! (j - Suc 0) = (ys @ as) ! (j - Suc 0)"
[PROOF STATE]
proof (prove)
using this:
0 < i
i \<le> j
length xs < i
length ys = length xs

goal (1 subgoal):
 1. (xs @ as) ! (j - Suc 0) = (ys @ as) ! (j - Suc 0)
[PROOF STEP]
by (auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
(xs @ as) ! (j - Suc 0) = (ys @ as) ! (j - Suc 0)

goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; length xs < i; length ys = length xs\<rbrakk> \<Longrightarrow> SWA.sum (xs @ as) i j = SWA.sum (ys @ as) i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(xs @ as) ! (j - Suc 0) = (ys @ as) ! (j - Suc 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(xs @ as) ! (j - Suc 0) = (ys @ as) ! (j - Suc 0)

goal (1 subgoal):
 1. SWA.sum (xs @ as) i j = SWA.sum (ys @ as) i j
[PROOF STEP]
by (simp add: *)
[PROOF STATE]
proof (state)
this:
SWA.sum (xs @ as) i j = SWA.sum (ys @ as) i j

goal:
No subgoals!
[PROOF STEP]
qed