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

goal (2 subgoals):
 1. \<lbrakk>length xs \<le> l Leaf - 1; length ys = length xs; well_shaped Leaf; well_valued0 (xs @ as) Leaf\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node x1 x2 x3 t1 t2) - 1; length ys = length xs; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 (xs @ as) (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) (Node x1 x2 x3 t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1
\<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
length xs \<le> l (Node i j a t1 t2) - 1
length ys = length xs
well_shaped (Node i j a t1 t2)
well_valued0 (xs @ as) (Node i j a t1 t2)
[PROOF STEP]
have well_valued0_t1: "well_valued0 (ys @ as) t1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1
\<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
length xs \<le> l (Node i j a t1 t2) - 1
length ys = length xs
well_shaped (Node i j a t1 t2)
well_valued0 (xs @ as) (Node i j a t1 t2)

goal (1 subgoal):
 1. well_valued0 (ys @ as) t1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_valued0 (ys @ as) t1

goal (2 subgoals):
 1. \<lbrakk>length xs \<le> l Leaf - 1; length ys = length xs; well_shaped Leaf; well_valued0 (xs @ as) Leaf\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node x1 x2 x3 t1 t2) - 1; length ys = length xs; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 (xs @ as) (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) (Node x1 x2 x3 t1 t2)
[PROOF STEP]
from Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1
\<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
length xs \<le> l (Node i j a t1 t2) - 1
length ys = length xs
well_shaped (Node i j a t1 t2)
well_valued0 (xs @ as) (Node i j a t1 t2)
[PROOF STEP]
have "well_valued0 (ys @ as) t2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1
\<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
length xs \<le> l (Node i j a t1 t2) - 1
length ys = length xs
well_shaped (Node i j a t1 t2)
well_valued0 (xs @ as) (Node i j a t1 t2)

goal (1 subgoal):
 1. well_valued0 (ys @ as) t2
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); a = None\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
 2. \<And>aa. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); a = Some aa\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
a = None

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); a = None\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
 2. \<And>aa. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); a = Some aa\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
[PROOF STEP]
with Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1
\<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
length xs \<le> l (Node i j a t1 t2) - 1
length ys = length xs
well_shaped (Node i j a t1 t2)
well_valued0 (xs @ as) (Node i j a t1 t2)
a = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1
\<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
length xs \<le> l (Node i j a t1 t2) - 1
length ys = length xs
well_shaped (Node i j a t1 t2)
well_valued0 (xs @ as) (Node i j a t1 t2)
a = None

goal (1 subgoal):
 1. well_valued0 (ys @ as) t2
[PROOF STEP]
by auto
        (metis One_nat_def Suc_pred diff_Suc_1 le_Suc_eq le_Suc_ex trans_le_add1 tree.exhaust_sel well_shaped.simps(2))
[PROOF STATE]
proof (state)
this:
well_valued0 (ys @ as) t2

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); a = Some aa\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); a = Some aa\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
[PROOF STEP]
case (Some a')
[PROOF STATE]
proof (state)
this:
a = Some a'

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); a = Some aa\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
[PROOF STEP]
with Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1
\<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
length xs \<le> l (Node i j a t1 t2) - 1
length ys = length xs
well_shaped (Node i j a t1 t2)
well_valued0 (xs @ as) (Node i j a t1 t2)
a = Some a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1
\<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2
length xs \<le> l (Node i j a t1 t2) - 1
length ys = length xs
well_shaped (Node i j a t1 t2)
well_valued0 (xs @ as) (Node i j a t1 t2)
a = Some a'

goal (1 subgoal):
 1. well_valued0 (ys @ as) t2
[PROOF STEP]
by auto
        (metis One_nat_def diff_Suc_1 diff_le_self le_trans tree.exhaust_sel well_shaped.simps(2))
[PROOF STATE]
proof (state)
this:
well_valued0 (ys @ as) t2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
well_valued0 (ys @ as) t2

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

goal (1 subgoal):
 1. well_valued0 (ys @ as) (Node i j a t1 t2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); well_valued0 (ys @ as) t1; well_valued0 (ys @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) (Node i j a t1 t2)
[PROOF STEP]
have f1: "0 < i \<and> j \<le> length (xs @ as) \<and> (a = None \<or> a = Some (SWA.sum (xs @ as) i j)) \<and> well_valued0 (xs @ as) t1 \<and> well_valued0 (xs @ as) t2 \<and> (t2 = Leaf \<or> val t2 \<noteq> None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < i \<and> j \<le> length (xs @ as) \<and> (a = None \<or> a = Some (SWA.sum (xs @ as) i j)) \<and> well_valued0 (xs @ as) t1 \<and> well_valued0 (xs @ as) t2 \<and> (t2 = Leaf \<or> val t2 \<noteq> None)
[PROOF STEP]
by (meson \<open>well_valued0 (xs @ as) (Node i j a t1 t2)\<close> well_valued0.simps(2))
[PROOF STATE]
proof (state)
this:
0 < i \<and> j \<le> length (xs @ as) \<and> (a = None \<or> a = Some (SWA.sum (xs @ as) i j)) \<and> well_valued0 (xs @ as) t1 \<and> well_valued0 (xs @ as) t2 \<and> (t2 = Leaf \<or> val t2 \<noteq> None)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); well_valued0 (ys @ as) t1; well_valued0 (ys @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) (Node i j a t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < i \<and> j \<le> length (xs @ as) \<and> (a = None \<or> a = Some (SWA.sum (xs @ as) i j)) \<and> well_valued0 (xs @ as) t1 \<and> well_valued0 (xs @ as) t2 \<and> (t2 = Leaf \<or> val t2 \<noteq> None)
[PROOF STEP]
have f2: "j \<le> length (ys @ as)"
[PROOF STATE]
proof (prove)
using this:
0 < i \<and> j \<le> length (xs @ as) \<and> (a = None \<or> a = Some (SWA.sum (xs @ as) i j)) \<and> well_valued0 (xs @ as) t1 \<and> well_valued0 (xs @ as) t2 \<and> (t2 = Leaf \<or> val t2 \<noteq> None)

goal (1 subgoal):
 1. j \<le> length (ys @ as)
[PROOF STEP]
by (simp add: \<open>length ys = length xs\<close>)
[PROOF STATE]
proof (state)
this:
j \<le> length (ys @ as)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); well_valued0 (ys @ as) t1; well_valued0 (ys @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) (Node i j a t1 t2)
[PROOF STEP]
have "a = None \<or> a = Some (SWA.sum (ys @ as) i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = None \<or> a = Some (SWA.sum (ys @ as) i j)
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
0 < i \<and> j \<le> length (xs @ as) \<and> (a = None \<or> a = Some (SWA.sum (xs @ as) i j)) \<and> well_valued0 (xs @ as) t1 \<and> well_valued0 (xs @ as) t2 \<and> (t2 = Leaf \<or> val t2 \<noteq> None)

goal (1 subgoal):
 1. a = None \<or> a = Some (SWA.sum (ys @ as) i j)
[PROOF STEP]
by (metis Node.prems(1) Node.prems(2) Node.prems(3) One_nat_def Suc_pred le_imp_less_Suc sum_eq_sum_prepend tree.sel(2) well_shaped.simps(2))
[PROOF STATE]
proof (state)
this:
a = None \<or> a = Some (SWA.sum (ys @ as) i j)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>length xs \<le> l t1 - 1; length ys = length xs; well_shaped t1; well_valued0 (xs @ as) t1\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t1; \<lbrakk>length xs \<le> l t2 - 1; length ys = length xs; well_shaped t2; well_valued0 (xs @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) t2; length xs \<le> l (Node i j a t1 t2) - 1; length ys = length xs; well_shaped (Node i j a t1 t2); well_valued0 (xs @ as) (Node i j a t1 t2); well_valued0 (ys @ as) t1; well_valued0 (ys @ as) t2\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) (Node i j a t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = None \<or> a = Some (SWA.sum (ys @ as) i j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = None \<or> a = Some (SWA.sum (ys @ as) i j)

goal (1 subgoal):
 1. well_valued0 (ys @ as) (Node i j a t1 t2)
[PROOF STEP]
using f2 f1 \<open>well_valued0 (ys @ as) t2\<close> well_valued0.simps(2) well_valued0_t1
[PROOF STATE]
proof (prove)
using this:
a = None \<or> a = Some (SWA.sum (ys @ as) i j)
j \<le> length (ys @ as)
0 < i \<and> j \<le> length (xs @ as) \<and> (a = None \<or> a = Some (SWA.sum (xs @ as) i j)) \<and> well_valued0 (xs @ as) t1 \<and> well_valued0 (xs @ as) t2 \<and> (t2 = Leaf \<or> val t2 \<noteq> None)
well_valued0 (ys @ as) t2
well_valued0 ?as (Node ?i ?j ?a ?t ?u) = (0 < ?i \<and> ?j \<le> length ?as \<and> (?a \<noteq> None \<longrightarrow> ?a = Some (SWA.sum ?as ?i ?j)) \<and> well_valued0 ?as ?t \<and> well_valued0 ?as ?u \<and> (?u = Leaf \<or> val ?u \<noteq> None))
well_valued0 (ys @ as) t1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
well_valued0 (ys @ as) (Node i j a t1 t2)

goal (1 subgoal):
 1. \<lbrakk>length xs \<le> l Leaf - 1; length ys = length xs; well_shaped Leaf; well_valued0 (xs @ as) Leaf\<rbrakk> \<Longrightarrow> well_valued0 (ys @ as) Leaf
[PROOF STEP]
qed simp


[STATEMENT]
lemma valid_prepend: "\<lbrakk>length xs \<le> l t - 1; length ys = length xs; valid (xs @ as) t\<rbrakk> \<Longrightarrow> valid (ys @ as) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs \<le> l t - 1; length ys = length xs; valid (xs @ as) t\<rbrakk> \<Longrightarrow> valid (ys @ as) t
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs \<le> l t - 1; length ys = length xs; well_shaped t \<and> well_valued (xs @ as) t\<rbrakk> \<Longrightarrow> well_shaped t \<and> well_valued (ys @ as) t
[PROOF STEP]
by (auto intro: well_valued0_prepend)


[STATEMENT]
lemma take_eq_append_take_take_drop: "m \<le> n \<Longrightarrow> take n xs = take m xs @ take (n-m) (drop m xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> take n xs = take m xs @ take (n - m) (drop m xs)
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m \<le> n \<Longrightarrow> take n [] = take m [] @ take (n - m) (drop m [])
 2. \<And>a xs. \<lbrakk>m \<le> n \<Longrightarrow> take n xs = take m xs @ take (n - m) (drop m xs); m \<le> n\<rbrakk> \<Longrightarrow> take n (a # xs) = take m (a # xs) @ take (n - m) (drop m (a # xs))
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
m \<le> n \<Longrightarrow> take n xs = take m xs @ take (n - m) (drop m xs)
m \<le> n

goal (2 subgoals):
 1. m \<le> n \<Longrightarrow> take n [] = take m [] @ take (n - m) (drop m [])
 2. \<And>a xs. \<lbrakk>m \<le> n \<Longrightarrow> take n xs = take m xs @ take (n - m) (drop m xs); m \<le> n\<rbrakk> \<Longrightarrow> take n (a # xs) = take m (a # xs) @ take (n - m) (drop m (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<le> n \<Longrightarrow> take n xs = take m xs @ take (n - m) (drop m xs)
m \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m \<le> n \<Longrightarrow> take n xs = take m xs @ take (n - m) (drop m xs)
m \<le> n

goal (1 subgoal):
 1. take n (a # xs) = take m (a # xs) @ take (n - m) (drop m (a # xs))
[PROOF STEP]
by (metis le_add_diff_inverse take_add)
[PROOF STATE]
proof (state)
this:
take n (a # xs) = take m (a # xs) @ take (n - m) (drop m (a # xs))

goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> take n [] = take m [] @ take (n - m) (drop m [])
[PROOF STEP]
qed simp


[STATEMENT]
lemma well_valued0_take_r: "\<lbrakk>well_shaped t; well_valued0 as t\<rbrakk> \<Longrightarrow> well_valued0 (take (r t) as) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; well_valued0 as t\<rbrakk> \<Longrightarrow> well_valued0 (take (r t) 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 (take (r Leaf) as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (take (r (Node x1 x2 x3 t1 t2)) 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 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) 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 (take (r Leaf) as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (take (r (Node x1 x2 x3 t1 t2)) as) (Node x1 x2 x3 t1 t2)
[PROOF STEP]
from Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
[PROOF STEP]
have well_valued0_t1: "well_valued0 (take j as) t1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) 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 (take j as) t1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2; well_shaped (Node i j a t1 t2); well_valued0 as (Node i j a t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (take j as) t1
[PROOF STEP]
from Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
[PROOF STEP]
have "r t1 \<le> j"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)

goal (1 subgoal):
 1. r t1 \<le> j
[PROOF STEP]
using r_lchild_le_r
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
well_shaped ?t \<Longrightarrow> r (lchild ?t) \<le> r ?t

goal (1 subgoal):
 1. r t1 \<le> j
[PROOF STEP]
by (metis tree.sel(4) tree.sel(8))
[PROOF STATE]
proof (state)
this:
r t1 \<le> j

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2; well_shaped (Node i j a t1 t2); well_valued0 as (Node i j a t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (take j as) t1
[PROOF STEP]
with Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r t1 \<le> j
[PROOF STEP]
have "take j as = take (r t1) as @ take (j - r t1) (drop (r t1) as)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r t1 \<le> j

goal (1 subgoal):
 1. take j as = take (r t1) as @ take (j - r t1) (drop (r t1) as)
[PROOF STEP]
using take_eq_append_take_take_drop[of "r t1" j as]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r t1 \<le> j
r t1 \<le> j \<Longrightarrow> take j as = take (r t1) as @ take (j - r t1) (drop (r t1) as)

goal (1 subgoal):
 1. take j as = take (r t1) as @ take (j - r t1) (drop (r t1) as)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take j as = take (r t1) as @ take (j - r t1) (drop (r t1) as)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2; well_shaped (Node i j a t1 t2); well_valued0 as (Node i j a t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (take j as) t1
[PROOF STEP]
with Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
take j as = take (r t1) as @ take (j - r t1) (drop (r t1) as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
take j as = take (r t1) as @ take (j - r t1) (drop (r t1) as)

goal (1 subgoal):
 1. well_valued0 (take j as) t1
[PROOF STEP]
by (auto intro!: well_valued0_append)
[PROOF STATE]
proof (state)
this:
well_valued0 (take j as) t1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
well_valued0 (take j as) t1

goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf\<rbrakk> \<Longrightarrow> well_valued0 (take (r Leaf) as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (take (r (Node x1 x2 x3 t1 t2)) as) (Node x1 x2 x3 t1 t2)
[PROOF STEP]
from Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
[PROOF STEP]
have well_valued0_t2: "well_valued0 (take j as) t2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) 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 (take j as) t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_valued0 (take j as) t2

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

goal (1 subgoal):
 1. fold (+) (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0)) = fold (+) (rev (map ((!) (take (r t2) as)) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0))
[PROOF STEP]
by (intro arg_cong[where f="\<lambda>xs. fold _ xs _"]) auto
[PROOF STATE]
proof (state)
this:
fold (+) (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0)) = fold (+) (rev (map ((!) (take (r t2) as)) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0))

goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf\<rbrakk> \<Longrightarrow> well_valued0 (take (r Leaf) as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (take (r (Node x1 x2 x3 t1 t2)) as) (Node x1 x2 x3 t1 t2)
[PROOF STEP]
from Node well_valued0_t1 well_valued0_t2 sum_eq
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
well_valued0 (take j as) t1
well_valued0 (take j as) t2
fold (+) (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0)) = fold (+) (rev (map ((!) (take (r t2) as)) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1\<rbrakk> \<Longrightarrow> well_valued0 (take (r t1) as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2\<rbrakk> \<Longrightarrow> well_valued0 (take (r t2) as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
well_valued0 (take j as) t1
well_valued0 (take j as) t2
fold (+) (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0)) = fold (+) (rev (map ((!) (take (r t2) as)) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0))

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

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


[STATEMENT]
lemma valid_take_r: "valid as t \<Longrightarrow> valid (take (r t) as) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid as t \<Longrightarrow> valid (take (r t) 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 (take (r t) as) t
[PROOF STEP]
by (auto intro: well_valued0_take_r)


[STATEMENT]
lemma well_valued0_butlast: "\<lbrakk>well_shaped t; well_valued0 as t; r t < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; well_valued0 as t; r t < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf; r Leaf < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast 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; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) < length as

goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf; r Leaf < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) (Node x1 x2 x3 t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) < length as
[PROOF STEP]
have r_le_length: "j \<le> length (butlast as)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) < length as

goal (1 subgoal):
 1. j \<le> length (butlast as)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j \<le> length (butlast as)

goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf; r Leaf < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) (Node x1 x2 x3 t1 t2)
[PROOF STEP]
from Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) < length as
[PROOF STEP]
have "i > 0"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) < length as

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

goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf; r Leaf < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1; \<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2; well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); r (Node x1 x2 x3 t1 t2) < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) (Node x1 x2 x3 t1 t2)
[PROOF STEP]
with r_le_length Node
[PROOF STATE]
proof (chain)
picking this:
j \<le> length (butlast as)
\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) < length as
0 < i
[PROOF STEP]
have sum_eq: "sum as i j = sum (butlast as) i j"
[PROOF STATE]
proof (prove)
using this:
j \<le> length (butlast as)
\<lbrakk>well_shaped t1; well_valued0 as t1; r t1 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t1
\<lbrakk>well_shaped t2; well_valued0 as t2; r t2 < length as\<rbrakk> \<Longrightarrow> well_valued0 (butlast as) t2
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
r (Node i j a t1 t2) < length as
0 < i

goal (1 subgoal):
 1. SWA.sum as i j = SWA.sum (butlast as) i j
[PROOF STEP]
by (metis append_butlast_last_id le_zero_eq less_imp_le_nat list.size(3) neq_iff
      sum_eq_sum_append well_shaped.simps(2))
[PROOF STATE]
proof (state)
this:
SWA.sum as i j = SWA.sum (butlast as) i j

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

goal (1 subgoal):
 1. r t1 < length as
[PROOF STEP]
by (metis dual_order.strict_trans2 r_lchild_le_r tree.sel(8))
[PROOF STATE]
proof (state)
this:
r t1 < length as

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

goal (1 subgoal):
 1. well_valued0 (butlast as) (Node i j a t1 t2)
[PROOF STEP]
by (metis (no_types, lifting) dual_order.strict_iff_order sum_eq tree.sel(10) tree.sel(4)
      well_shaped.simps(2) well_shaped_rchild well_valued0.simps(2))
[PROOF STATE]
proof (state)
this:
well_valued0 (butlast as) (Node i j a t1 t2)

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


[STATEMENT]
lemma well_valued0_append_butlast_lchild: "\<lbrakk>well_shaped t; well_valued0 as t\<rbrakk> \<Longrightarrow>
  well_valued0 (butlast as @ [last as + x]) (lchild t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; well_valued0 as t\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
[PROOF STEP]
proof (cases t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>well_shaped t; well_valued0 as t; t = Leaf\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>well_shaped t; well_valued0 as t; t = Node x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
[PROOF STEP]
case (Node i j a t1 t2)
[PROOF STATE]
proof (state)
this:
t = Node i j a t1 t2

goal (2 subgoals):
 1. \<lbrakk>well_shaped t; well_valued0 as t; t = Leaf\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>well_shaped t; well_valued0 as t; t = Node x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
[PROOF STEP]
assume assms: "well_shaped t" "well_valued0 as t"
[PROOF STATE]
proof (state)
this:
well_shaped t
well_valued0 as t

goal (2 subgoals):
 1. \<lbrakk>well_shaped t; well_valued0 as t; t = Leaf\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>well_shaped t; well_valued0 as t; t = Node x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
[PROOF STEP]
from Node assms
[PROOF STATE]
proof (chain)
picking this:
t = Node i j a t1 t2
well_shaped t
well_valued0 as t
[PROOF STEP]
have "r t1 < length as"
[PROOF STATE]
proof (prove)
using this:
t = Node i j a t1 t2
well_shaped t
well_valued0 as t

goal (1 subgoal):
 1. r t1 < length as
[PROOF STEP]
by (fastforce dest: well_shaped_lr)
[PROOF STATE]
proof (state)
this:
r t1 < length as

goal (2 subgoals):
 1. \<lbrakk>well_shaped t; well_valued0 as t; t = Leaf\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>well_shaped t; well_valued0 as t; t = Node x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
[PROOF STEP]
with Node assms
[PROOF STATE]
proof (chain)
picking this:
t = Node i j a t1 t2
well_shaped t
well_valued0 as t
r t1 < length as
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Node i j a t1 t2
well_shaped t
well_valued0 as t
r t1 < length as

goal (1 subgoal):
 1. well_valued0 (butlast as @ [last as + x]) (lchild t)
[PROOF STEP]
by (auto simp: well_valued0_butlast well_valued0_append)
[PROOF STATE]
proof (state)
this:
well_valued0 (butlast as @ [last as + x]) (lchild t)

goal (1 subgoal):
 1. \<lbrakk>well_shaped t; well_valued0 as t; t = Leaf\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (lchild t)
[PROOF STEP]
qed simp


[STATEMENT]
lemma sum_update_rightmost: "\<lbrakk>0 < i; i \<le> j; length as = j\<rbrakk> \<Longrightarrow>
  sum as i j + x = sum (butlast as @ [last as + x]) i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < i; i \<le> j; length as = j\<rbrakk> \<Longrightarrow> SWA.sum as i j + x = SWA.sum (butlast as @ [last as + x]) i j
[PROOF STEP]
by (cases as)
    (auto simp: nth_append[abs_def] fold_add_add last_conv_nth nth_Cons' nth_butlast
     intro!: arg_cong2[where f="(+)"] arg_cong[where f="\<lambda>xs. fold _ xs _"])


[STATEMENT]
lemma well_valued0_update_rightmost: "\<lbrakk>well_shaped t; well_valued0 as t; length as = r t\<rbrakk> \<Longrightarrow>
  well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; well_valued0 as t; length as = r t\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t)
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf; length as = r Leaf\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) Leaf)
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node x1 x2 x3 t1 t2))
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
well_shaped Leaf
well_valued0 as Leaf
length as = r Leaf

goal (2 subgoals):
 1. \<lbrakk>well_shaped Leaf; well_valued0 as Leaf; length as = r Leaf\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) Leaf)
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node x1 x2 x3 t1 t2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_shaped Leaf
well_valued0 as Leaf
length as = r Leaf
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
well_shaped Leaf
well_valued0 as Leaf
length as = r Leaf

goal (1 subgoal):
 1. well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) Leaf)
[PROOF STEP]
by (auto simp add: valid_Leaf)
[PROOF STATE]
proof (state)
this:
well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) Leaf)

goal (1 subgoal):
 1. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node x1 x2 x3 t1 t2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (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; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)

goal (1 subgoal):
 1. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node x1 x2 x3 t1 t2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)

goal (1 subgoal):
 1. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node x1 x2 x3 t1 t2))
[PROOF STEP]
from Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)
[PROOF STEP]
have well_valued0_t1: "well_valued0 (butlast as @ [last as + x]) t1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)

goal (1 subgoal):
 1. well_valued0 (butlast as @ [last as + x]) t1
[PROOF STEP]
using well_valued0_append_butlast_lchild
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)
\<lbrakk>well_shaped ?t; well_valued0 ?as ?t\<rbrakk> \<Longrightarrow> well_valued0 (butlast ?as @ [last ?as + ?x]) (lchild ?t)

goal (1 subgoal):
 1. well_valued0 (butlast as @ [last as + x]) t1
[PROOF STEP]
by (metis tree.sel(8))
[PROOF STATE]
proof (state)
this:
well_valued0 (butlast as @ [last as + x]) t1

goal (1 subgoal):
 1. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node x1 x2 x3 t1 t2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
well_valued0 (butlast as @ [last as + x]) t1

goal (1 subgoal):
 1. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node x1 x2 x3 t1 t2))
[PROOF STEP]
from Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)
[PROOF STEP]
have well_valued0_t2:
    "well_valued0 (butlast as @ [last as + x]) (update_rightmost ((\<lambda>a. a + x)) t2)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)

goal (1 subgoal):
 1. well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
[PROOF STEP]
by (metis \<open>well_valued0 (butlast as @ [last as + x]) t1\<close> dual_order.strict_iff_order
      tree.sel(4) update_rightmost.simps(1) well_shaped.simps(2) well_valued0.simps(2))
[PROOF STATE]
proof (state)
this:
well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)

goal (1 subgoal):
 1. \<And>x1 x2 x3 t1 t2. \<lbrakk>\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1); \<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2); well_shaped (Node x1 x2 x3 t1 t2); well_valued0 as (Node x1 x2 x3 t1 t2); length as = r (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node x1 x2 x3 t1 t2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)
well_valued0 (butlast as @ [last as + x]) t1
well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t1; well_valued0 as t1; length as = r t1\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t1)
\<lbrakk>well_shaped t2; well_valued0 as t2; length as = r t2\<rbrakk> \<Longrightarrow> well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)
well_shaped (Node i j a t1 t2)
well_valued0 as (Node i j a t1 t2)
length as = r (Node i j a t1 t2)
well_valued0 (butlast as @ [last as + x]) t1
well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t2)

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

goal (1 subgoal):
 1. well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node i j a t1 t2))
[PROOF STEP]
by (cases a) (auto simp: val_update_rightmost_neq_None)
[PROOF STATE]
proof (state)
this:
well_valued0 (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) (Node i j a t1 t2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_update_rightmost: "\<lbrakk>valid as t; length as = r t\<rbrakk> \<Longrightarrow>
  valid (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid as t; length as = r t\<rbrakk> \<Longrightarrow> valid (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t)
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t \<and> well_valued as t; length as = r t\<rbrakk> \<Longrightarrow> well_shaped (update_rightmost (\<lambda>a. a + x) t) \<and> well_valued (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t)
[PROOF STEP]
using well_valued0_update_rightmost
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped ?t; well_valued0 ?as ?t; length ?as = r ?t\<rbrakk> \<Longrightarrow> well_valued0 (butlast ?as @ [last ?as + ?x]) (update_rightmost (\<lambda>a. a + ?x) ?t)

goal (1 subgoal):
 1. \<lbrakk>well_shaped t \<and> well_valued as t; length as = r t\<rbrakk> \<Longrightarrow> well_shaped (update_rightmost (\<lambda>a. a + x) t) \<and> well_valued (butlast as @ [last as + x]) (update_rightmost (\<lambda>a. a + x) t)
[PROOF STEP]
by (metis update_rightmost.simps(1) val_update_rightmost_neq_None well_shaped_update_rightmost)


[STATEMENT]
lemma ZeroHeightMultiElimAux[rule_format]:
  "(M, l, s, k, ll, r) \<in> MStep \<Longrightarrow> 0=k \<longrightarrow> (r=s \<and> ll=l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, ll, r) \<in> MStep \<Longrightarrow> 0 = k \<longrightarrow> r = s \<and> ll = l
[PROOF STEP]
by (erule MStep.induct, simp_all)


[STATEMENT]
lemma ZeroHeightMultiElim: "(M,l,s,0,ll,r) \<in> MStep \<Longrightarrow> r=s \<and> ll=l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, 0, ll, r) \<in> MStep \<Longrightarrow> r = s \<and> ll = l
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, 0, ll, r) \<in> MStep \<Longrightarrow> r = s \<and> ll = l
[PROOF STEP]
by (erule ZeroHeightMultiElimAux, simp)


[STATEMENT]
lemma MultiSplitAux[rule_format]:
  "(M, l, s, k, ll, t) \<in> MStep \<Longrightarrow>
    1 \<le> k \<longrightarrow> (\<exists> n m r l1. (M,l,s,n,l1,r):Step \<and>
                        (M,l1,r,m,ll,t):MStep \<and> Suc m +n =k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, ll, t) \<in> MStep \<Longrightarrow> 1 \<le> k \<longrightarrow> (\<exists>n m r l1. (M, l, s, n, l1, r) \<in> Step \<and> (M, l1, r, m, ll, t) \<in> MStep \<and> Suc m + n = k)
[PROOF STEP]
apply (erule MStep.induct, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m a aa b l1a. (M, l1, r, n, l1a, a, aa, b) \<in> Step \<and> (M, l1a, (a, aa, b), m, l2, t) \<in> MStep \<and> Suc (m + n) = k); m = Suc (k + n)\<rbrakk> \<Longrightarrow> \<exists>na m a aa b l1. (M, l, s, na, l1, a, aa, b) \<in> Step \<and> (M, l1, (a, aa, b), m, l2, t) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k)\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply (case_tac k, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb l2 af ag bc. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), 0, l2, af, ag, bc) \<in> MStep\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = n
 2. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply (drule ZeroHeightMultiElim[simplified], clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> \<exists>na m af ag bc l1a. ((a, aa, b), l, (ab, ac, ba), na, l1a, af, ag, bc) \<in> Step \<and> ((a, aa, b), l1a, (af, ag, bc), m, l1, ad, ae, bb) \<in> MStep \<and> m + na = n
 2. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply (rule, rule,rule, rule,rule, rule, rule, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> ((a, aa, b), l1, (ad, ae, bb), ?m16 a aa b l ab ac ba n l1 ad ae bb, l1, ad, ae, bb) \<in> MStep \<and> ?m16 a aa b l ab ac ba n l1 ad ae bb + n = n
 2. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply (rule,rule MS_zero)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> ?m16 a aa b l ab ac ba n l1 ad ae bb = 0
 2. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> (ad, ae, bb) = (ad, ae, bb)
 3. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> l1 = l1
 4. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> ?m16 a aa b l ab ac ba n l1 ad ae bb + n = n
 5. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> (ad, ae, bb) = (ad, ae, bb)
 2. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> l1 = l1
 3. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> 0 + n = n
 4. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> l1 = l1
 2. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> 0 + n = n
 3. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb. ((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step \<Longrightarrow> 0 + n = n
 2. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb l1. ((a, aa, b), l, (ab, ac, ba), na, l1, ad, ae, bb) \<in> Step \<and> ((a, aa, b), l1, (ad, ae, bb), m, l2, af, ag, bc) \<in> MStep \<and> m + na = k + n
[PROOF STEP]
apply (rule, rule,rule, rule,rule, rule,rule,assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> ((a, aa, b), l1, (ad, ae, bb), ?m39 a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat, l2, af, ag, bc) \<in> MStep \<and> ?m39 a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat + n = k + n
[PROOF STEP]
apply (rule,assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; Suc 0 \<le> k \<longrightarrow> (\<exists>n m ab ac ba l1a. ((a, aa, b), l1, (ad, ae, bb), n, l1a, ab, ac, ba) \<in> Step \<and> ((a, aa, b), l1a, (ab, ac, ba), m, l2, af, ag, bc) \<in> MStep \<and> Suc (m + n) = k); k = Suc nat\<rbrakk> \<Longrightarrow> k + n = k + n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MultiSplit:
  "\<lbrakk>(M, l, s, k, ll, t) \<in> MStep; 1 \<le> k\<rbrakk> \<Longrightarrow>
  \<exists> n m r l1. (M,l,s,n,l1,r):Step \<and> (M,l1,r,m,ll,t):MStep \<and> Suc m + n =k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, k, ll, t) \<in> MStep; 1 \<le> k\<rbrakk> \<Longrightarrow> \<exists>n m r l1. (M, l, s, n, l1, r) \<in> Step \<and> (M, l1, r, m, ll, t) \<in> MStep \<and> Suc m + n = k
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, k, ll, t) \<in> MStep; 1 \<le> k\<rbrakk> \<Longrightarrow> \<exists>n m r l1. (M, l, s, n, l1, r) \<in> Step \<and> (M, l1, r, m, ll, t) \<in> MStep \<and> Suc m + n = k
[PROOF STEP]
by (erule MultiSplitAux, assumption)


[STATEMENT]
lemma MStep_returnElimAux[rule_format]:
"(M,l,s,k,ll,t) \<in> MStep \<Longrightarrow>
 (get_ins M l = Some vreturn \<longrightarrow> t=s \<and> ll=l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, ll, t) \<in> MStep \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s \<and> ll = l
[PROOF STEP]
apply (erule MStep.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k t s ll l M. \<lbrakk>k = 0; t = s; ll = l\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s \<and> ll = l
 2. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; get_ins M l1 = Some vreturn \<longrightarrow> t = r \<and> l2 = l1; m = Suc k + n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s \<and> l2 = l
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; get_ins M l1 = Some vreturn \<longrightarrow> t = r \<and> l2 = l1; m = Suc k + n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s \<and> l2 = l
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, l1, ad, ae, bb) \<in> Step; ((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; get_ins (a, aa, b) l1 = Some vreturn \<longrightarrow> af = ad \<and> ag = ae \<and> bc = bb \<and> l2 = l1; get_ins (a, aa, b) l = Some vreturn\<rbrakk> \<Longrightarrow> af = ab \<and> ag = ac \<and> bc = ba \<and> l2 = l
[PROOF STEP]
apply (drule RetElim1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc. \<lbrakk>((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; get_ins (a, aa, b) l1 = Some vreturn \<longrightarrow> af = ad \<and> ag = ae \<and> bc = bb \<and> l2 = l1; get_ins (a, aa, b) l = Some vreturn\<rbrakk> \<Longrightarrow> get_ins (a, aa, b) l = Some vreturn
 2. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc. \<lbrakk>((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; get_ins (a, aa, b) l1 = Some vreturn \<longrightarrow> af = ad \<and> ag = ae \<and> bc = bb \<and> l2 = l1; get_ins (a, aa, b) l = Some vreturn; False\<rbrakk> \<Longrightarrow> af = ab \<and> ag = ac \<and> bc = ba \<and> l2 = l
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b l ab ac ba n l1 ad ae bb k l2 af ag bc. \<lbrakk>((a, aa, b), l1, (ad, ae, bb), k, l2, af, ag, bc) \<in> MStep; get_ins (a, aa, b) l1 = Some vreturn \<longrightarrow> af = ad \<and> ag = ae \<and> bc = bb \<and> l2 = l1; get_ins (a, aa, b) l = Some vreturn; False\<rbrakk> \<Longrightarrow> af = ab \<and> ag = ac \<and> bc = ba \<and> l2 = l
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MStep_returnElim:
  "\<lbrakk>(M,l,s,k,ll,t) \<in> MStep; get_ins M l = Some vreturn\<rbrakk> \<Longrightarrow> t=s \<and> ll = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, k, ll, t) \<in> MStep; get_ins M l = Some vreturn\<rbrakk> \<Longrightarrow> t = s \<and> ll = l
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, k, ll, t) \<in> MStep; get_ins M l = Some vreturn\<rbrakk> \<Longrightarrow> t = s \<and> ll = l
[PROOF STEP]
by (erule MStep_returnElimAux, assumption)


[STATEMENT]
lemma MultiAppAux[rule_format]:
"(M,l,s,k,l1,r):MStep \<Longrightarrow>
  (\<forall> n t l2. (M,l1,r,n,l2,t):Step \<longrightarrow> (M,l,s,Suc k+n,l2,t):MStep)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, l1, r) \<in> MStep \<Longrightarrow> \<forall>n t l2. (M, l1, r, n, l2, t) \<in> Step \<longrightarrow> (M, l, s, Suc k + n, l2, t) \<in> MStep
[PROOF STEP]
apply (erule MStep.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k t s ll l M. \<lbrakk>k = 0; t = s; ll = l\<rbrakk> \<Longrightarrow> \<forall>n ta l2. (M, ll, t, n, l2, ta) \<in> Step \<longrightarrow> (M, l, s, Suc k + n, l2, ta) \<in> MStep
 2. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l, s, Suc m + n, l2a, ta) \<in> MStep
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ab ac ba l ad ae bb n af ag bc l2. ((ad, ae, bb), l, (ab, ac, ba), n, l2, af, ag, bc) \<in> Step \<Longrightarrow> ((ad, ae, bb), l, (ab, ac, ba), Suc n, l2, af, ag, bc) \<in> MStep
 2. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l, s, Suc m + n, l2a, ta) \<in> MStep
[PROOF STEP]
apply (erule MS_step)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ab ac ba l ad ae bb n af ag bc l2. ((ad, ae, bb), l2, (af, ag, bc), ?k20 ab ac ba l ad ae bb n af ag bc l2, l2, af, ag, bc) \<in> MStep
 2. \<And>ab ac ba l ad ae bb n af ag bc l2. Suc n = Suc (?k20 ab ac ba l ad ae bb n af ag bc l2) + n
 3. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l, s, Suc m + n, l2a, ta) \<in> MStep
[PROOF STEP]
apply (rule MS_zero)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ab ac ba l ad ae bb n af ag bc l2. ?k20 ab ac ba l ad ae bb n af ag bc l2 = 0
 2. \<And>ab ac ba l ad ae bb n af ag bc l2. (af, ag, bc) = (af, ag, bc)
 3. \<And>ab ac ba l ad ae bb n af ag bc l2. l2 = l2
 4. \<And>ab ac ba l ad ae bb n af ag bc l2. Suc n = Suc (?k20 ab ac ba l ad ae bb n af ag bc l2) + n
 5. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l, s, Suc m + n, l2a, ta) \<in> MStep
[PROOF STEP]
apply (simp,simp, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l, s, Suc m + n, l2a, ta) \<in> MStep
[PROOF STEP]
apply (rule, rule, rule, rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step\<rbrakk> \<Longrightarrow> (M, l, s, Suc m + na, l2a, ta) \<in> MStep
[PROOF STEP]
apply (erule MS_step)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step\<rbrakk> \<Longrightarrow> (M, l1, r, ?k36 M l s n l1 r k l2 t m na ta l2a, l2a, ta) \<in> MStep
 2. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step\<rbrakk> \<Longrightarrow> Suc m + na = Suc (?k36 M l s n l1 r k l2 t m na ta l2a) + n
[PROOF STEP]
apply (erule_tac x=na in allE, erule_tac x=ta in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step; \<forall>l2a. (M, l2, t, na, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + na, l2a, ta) \<in> MStep\<rbrakk> \<Longrightarrow> (M, l1, r, ?k36 M l s n l1 r k l2 t m na ta l2a, l2a, ta) \<in> MStep
 2. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step\<rbrakk> \<Longrightarrow> Suc m + na = Suc (?k36 M l s n l1 r k l2 t m na ta l2a) + n
[PROOF STEP]
apply (erule_tac x=l2a in allE , erule impE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step\<rbrakk> \<Longrightarrow> (M, l2, t, na, l2a, ta) \<in> Step
 2. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step; (M, l1, r, Suc k + na, l2a, ta) \<in> MStep\<rbrakk> \<Longrightarrow> (M, l1, r, ?k36 M l s n l1 r k l2 t m na ta l2a, l2a, ta) \<in> MStep
 3. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step\<rbrakk> \<Longrightarrow> Suc m + na = Suc (?k36 M l s n l1 r k l2 t m na ta l2a) + n
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step; (M, l1, r, Suc k + na, l2a, ta) \<in> MStep\<rbrakk> \<Longrightarrow> (M, l1, r, ?k36 M l s n l1 r k l2 t m na ta l2a, l2a, ta) \<in> MStep
 2. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step\<rbrakk> \<Longrightarrow> Suc m + na = Suc (?k36 M l s n l1 r k l2 t m na ta l2a) + n
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m na ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; \<forall>n ta l2a. (M, l2, t, n, l2a, ta) \<in> Step \<longrightarrow> (M, l1, r, Suc k + n, l2a, ta) \<in> MStep; m = Suc k + n; (M, l2, t, na, l2a, ta) \<in> Step\<rbrakk> \<Longrightarrow> Suc m + na = Suc (Suc k + na) + n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MultiApp:
  "\<lbrakk>(M,l,s,k,l1,r):MStep; (M,l1,r,n,l2,t):Step\<rbrakk> \<Longrightarrow> (M,l,s,Suc k+n,l2,t):MStep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, k, l1, r) \<in> MStep; (M, l1, r, n, l2, t) \<in> Step\<rbrakk> \<Longrightarrow> (M, l, s, Suc k + n, l2, t) \<in> MStep
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, k, l1, r) \<in> MStep; (M, l1, r, n, l2, t) \<in> Step\<rbrakk> \<Longrightarrow> (M, l, s, Suc k + n, l2, t) \<in> MStep
[PROOF STEP]
by (erule MultiAppAux, assumption)


[STATEMENT]
lemma MStep_Compose_Aux:"(M,l,s,n,l1,r):MStep \<Longrightarrow> (\<forall> k t l2. (M,l1,r,k,l2,t):MStep \<longrightarrow> (M,l,s,n + k,l2,t):MStep)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, n, l1, r) \<in> MStep \<Longrightarrow> \<forall>k t l2. (M, l1, r, k, l2, t) \<in> MStep \<longrightarrow> (M, l, s, n + k, l2, t) \<in> MStep
[PROOF STEP]
apply (erule MStep.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k t s ll l M. \<lbrakk>k = 0; t = s; ll = l\<rbrakk> \<Longrightarrow> \<forall>ka ta l2. (M, ll, t, ka, l2, ta) \<in> MStep \<longrightarrow> (M, l, s, k + ka, l2, ta) \<in> MStep
 2. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>ka ta l2a. (M, l2, t, ka, l2a, ta) \<in> MStep \<longrightarrow> (M, l1, r, k + ka, l2a, ta) \<in> MStep; m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>k ta l2a. (M, l2, t, k, l2a, ta) \<in> MStep \<longrightarrow> (M, l, s, m + k, l2a, ta) \<in> MStep
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>ka ta l2a. (M, l2, t, ka, l2a, ta) \<in> MStep \<longrightarrow> (M, l1, r, k + ka, l2a, ta) \<in> MStep; m = Suc k + n\<rbrakk> \<Longrightarrow> \<forall>k ta l2a. (M, l2, t, k, l2a, ta) \<in> MStep \<longrightarrow> (M, l, s, m + k, l2a, ta) \<in> MStep
[PROOF STEP]
apply (rule, rule, rule, rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m ka ta l2a. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; \<forall>ka ta l2a. (M, l2, t, ka, l2a, ta) \<in> MStep \<longrightarrow> (M, l1, r, k + ka, l2a, ta) \<in> MStep; m = Suc k + n; (M, l2, t, ka, l2a, ta) \<in> MStep\<rbrakk> \<Longrightarrow> (M, l, s, m + ka, l2a, ta) \<in> MStep
[PROOF STEP]
apply (erule_tac x=ka in allE, erule_tac x=ta in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m ka ta l2a. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, l2a, ta) \<in> MStep; \<forall>l2a. (M, l2, t, ka, l2a, ta) \<in> MStep \<longrightarrow> (M, l1, r, k + ka, l2a, ta) \<in> MStep\<rbrakk> \<Longrightarrow> (M, l, s, m + ka, l2a, ta) \<in> MStep
[PROOF STEP]
apply (erule_tac x=l2a in allE, erule impE, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m ka ta l2a. \<lbrakk>(M, l, s, n, l1, r) \<in> Step; (M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, l2a, ta) \<in> MStep; (M, l1, r, k + ka, l2a, ta) \<in> MStep\<rbrakk> \<Longrightarrow> (M, l, s, m + ka, l2a, ta) \<in> MStep
[PROOF STEP]
apply (erule MS_step, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M l s n l1 r k l2 t m ka ta l2a. \<lbrakk>(M, l1, r, k, l2, t) \<in> MStep; m = Suc k + n; (M, l2, t, ka, l2a, ta) \<in> MStep; (M, l1, r, k + ka, l2a, ta) \<in> MStep\<rbrakk> \<Longrightarrow> m + ka = Suc (k + ka) + n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MStep_Compose:
  "\<lbrakk>(M,l,s,n,l1,r):MStep; (M,l1,r,k,l2,t):MStep; nk=n+k\<rbrakk>
  \<Longrightarrow> (M,l,s,nk,l2,t):MStep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, l1, r) \<in> MStep; (M, l1, r, k, l2, t) \<in> MStep; nk = n + k\<rbrakk> \<Longrightarrow> (M, l, s, nk, l2, t) \<in> MStep
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, l1, r) \<in> MStep; (M, l1, r, k, l2, t) \<in> MStep; nk = n + k\<rbrakk> \<Longrightarrow> (M, l, s, nk, l2, t) \<in> MStep
[PROOF STEP]
by (drule MStep_Compose_Aux, fastforce)