[STATEMENT]
lemma index_sum: assumes "distinct s" "q\<in>set s"
shows "index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
distinct s
q \<in> set s
[PROOF STEP]
have bia_empty: "before q s \<inter> ({q} \<union> after q s) = {}"
[PROOF STATE]
proof (prove)
using this:
distinct s
q \<in> set s

goal (1 subgoal):
 1. before q s \<inter> ({q} \<union> after q s) = {}
[PROOF STEP]
by(auto simp: before_in_def)
[PROOF STATE]
proof (state)
this:
before q s \<inter> ({q} \<union> after q s) = {}

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
from befaf[OF assms(2) assms(1)]
[PROOF STATE]
proof (chain)
picking this:
before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
have "(\<Sum>e\<in>set s. if e < q in s then 1::nat else 0)
    = (\<Sum>e\<in>(before q s \<union> {q} \<union> after q s). if e < q in s then 1 else 0)"
[PROOF STATE]
proof (prove)
using this:
before q s \<union> {q} \<union> after q s = set s

goal (1 subgoal):
 1. (\<Sum>e\<in>set s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>set s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>set s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0)
            + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
have "(\<Sum>e\<in>(before q s \<union> {q} \<union> after q s). if e < q in s then 1::nat else 0)
      = (\<Sum>e\<in>(before q s \<union> ({q} \<union> after q s)). if e < q in s then 1::nat else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s \<union> ({q} \<union> after q s). if e < q in s then 1 else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s \<union> ({q} \<union> after q s). if e < q in s then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s \<union> ({q} \<union> after q s). if e < q in s then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0)
          + (\<Sum>e\<in>({q} \<union> after q s). if e < q in s then 1 else 0)
          - (\<Sum>e\<in>(before q s \<inter> ({q} \<union> after q s)). if e < q in s then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> ({q} \<union> after q s). if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) - (\<Sum>e\<in>before q s \<inter> ({q} \<union> after q s). if e < q in s then 1 else 0)
[PROOF STEP]
apply(rule sum_Un_nat)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (before q s)
 2. finite ({q} \<union> after q s)
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s \<union> ({q} \<union> after q s). if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) - (\<Sum>e\<in>before q s \<inter> ({q} \<union> after q s). if e < q in s then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s \<union> ({q} \<union> after q s). if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) - (\<Sum>e\<in>before q s \<inter> ({q} \<union> after q s). if e < q in s then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0)
          + (\<Sum>e\<in>({q} \<union> after q s). if e < q in s then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) - (\<Sum>e\<in>before q s \<inter> ({q} \<union> after q s). if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0)
[PROOF STEP]
using bia_empty
[PROOF STATE]
proof (prove)
using this:
before q s \<inter> ({q} \<union> after q s) = {}

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) - (\<Sum>e\<in>before q s \<inter> ({q} \<union> after q s). if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) - (\<Sum>e\<in>before q s \<inter> ({q} \<union> after q s). if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) - (\<Sum>e\<in>before q s \<inter> ({q} \<union> after q s). if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0)
          + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
by (simp add: before_in_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s \<union> {q} \<union> after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>before q s. 1) + (\<Sum>e\<in>({q} \<union> after q s). 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. 1) + (\<Sum>e\<in>{q} \<union> after q s. 0)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q < q in s \<Longrightarrow> False
[PROOF STEP]
unfolding before_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index s q < index s q \<and> q \<in> set s \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. 1) + (\<Sum>e\<in>{q} \<union> after q s. 0)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s. if e < q in s then 1 else 0) + (\<Sum>e\<in>{q}. if e < q in s then 1 else 0) + (\<Sum>e\<in>after q s. if e < q in s then 1 else 0) = (\<Sum>e\<in>before q s. 1) + (\<Sum>e\<in>{q} \<union> after q s. 0)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = card (before q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>before q s. 1) + (\<Sum>e\<in>{q} \<union> after q s. 0) = card (before q s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s. 1) + (\<Sum>e\<in>{q} \<union> after q s. 0) = card (before q s)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>before q s. 1) + (\<Sum>e\<in>{q} \<union> after q s. 0) = card (before q s)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = card (set (take (index s q) s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (before q s) = card (set (take (index s q) s))
[PROOF STEP]
using before_conv_take[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
before q s = set (take (index s q) s)

goal (1 subgoal):
 1. card (before q s) = card (set (take (index s q) s))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (before q s) = card (set (take (index s q) s))

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (before q s) = card (set (take (index s q) s))

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = length (take (index s q) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set (take (index s q) s)) = length (take (index s q) s)
[PROOF STEP]
using distinct_card assms(1) distinct_take
[PROOF STATE]
proof (prove)
using this:
distinct ?xs \<Longrightarrow> card (set ?xs) = length ?xs
distinct s
distinct ?xs \<Longrightarrow> distinct (take ?i ?xs)

goal (1 subgoal):
 1. card (set (take (index s q) s)) = length (take (index s q) s)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card (set (take (index s q) s)) = length (take (index s q) s)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (set (take (index s q) s)) = length (take (index s q) s)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = min (length s) (index s q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (take (index s q) s) = min (length s) (index s q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (take (index s q) s) = min (length s) (index s q)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (take (index s q) s) = min (length s) (index s q)

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
have "\<dots> = index s q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length s) (index s q) = index s q
[PROOF STEP]
using index_le_size[of s q]
[PROOF STATE]
proof (prove)
using this:
index s q \<le> length s

goal (1 subgoal):
 1. min (length s) (index s q) = index s q
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
min (length s) (index s q) = index s q

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>e\<in>set s. if e < q in s then 1 else 0) = index s q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>e\<in>set s. if e < q in s then 1 else 0) = index s q

goal (1 subgoal):
 1. index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index s q = (\<Sum>e\<in>set s. if e < q in s then 1 else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma t\<^sub>p_sumofALG: "distinct (fst s) \<Longrightarrow> snd a = [] \<Longrightarrow> (qs!i)\<in>set (fst s)
    \<Longrightarrow> t\<^sub>p (fst s) (qs!i) a = (\<Sum>e\<in>set (fst s). ALG e qs i s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (fst s); snd a = []; qs ! i \<in> set (fst s)\<rbrakk> \<Longrightarrow> t\<^sub>p (fst s) (qs ! i) a = (\<Sum>e\<in>set (fst s). ALG e qs i s)
[PROOF STEP]
unfolding t\<^sub>p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (fst s); snd a = []; qs ! i \<in> set (fst s)\<rbrakk> \<Longrightarrow> (let (mf, sws) = a in index (swaps sws (fst s)) (qs ! i) + length sws) = (\<Sum>e\<in>set (fst s). ALG e qs i s)
[PROOF STEP]
apply(simp add: split_def )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (fst s); snd a = []; qs ! i \<in> set (fst s)\<rbrakk> \<Longrightarrow> index (fst s) (qs ! i) = (\<Sum>e\<in>set (fst s). if e < qs ! i in fst s then 1 else 0)
[PROOF STEP]
using index_sum
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct ?s; ?q \<in> set ?s\<rbrakk> \<Longrightarrow> index ?s ?q = (\<Sum>e\<in>set ?s. if e < ?q in ?s then 1 else 0)

goal (1 subgoal):
 1. \<lbrakk>distinct (fst s); snd a = []; qs ! i \<in> set (fst s)\<rbrakk> \<Longrightarrow> index (fst s) (qs ! i) = (\<Sum>e\<in>set (fst s). if e < qs ! i in fst s then 1 else 0)
[PROOF STEP]
by metis


[STATEMENT]
lemma t\<^sub>p_sumofALGreal: assumes "distinct (fst s)" "snd a = []" "qs!i \<in> set(fst s)"
shows "real(t\<^sub>p (fst s) (qs!i) a) = (\<Sum>e\<in>set (fst s). real(ALG e qs i s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
distinct (fst s)
snd a = []
qs ! i \<in> set (fst s)
[PROOF STEP]
have "real(t\<^sub>p (fst s) (qs!i) a) = real(\<Sum>e\<in>set (fst s). ALG e qs i s)"
[PROOF STATE]
proof (prove)
using this:
distinct (fst s)
snd a = []
qs ! i \<in> set (fst s)

goal (1 subgoal):
 1. real (t\<^sub>p (fst s) (qs ! i) a) = real (\<Sum>e\<in>set (fst s). ALG e qs i s)
[PROOF STEP]
using t\<^sub>p_sumofALG
[PROOF STATE]
proof (prove)
using this:
distinct (fst s)
snd a = []
qs ! i \<in> set (fst s)
\<lbrakk>distinct (fst ?s); snd ?a = []; ?qs ! ?i \<in> set (fst ?s)\<rbrakk> \<Longrightarrow> t\<^sub>p (fst ?s) (?qs ! ?i) ?a = (\<Sum>e\<in>set (fst ?s). ALG e ?qs ?i ?s)

goal (1 subgoal):
 1. real (t\<^sub>p (fst s) (qs ! i) a) = real (\<Sum>e\<in>set (fst s). ALG e qs i s)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
real (t\<^sub>p (fst s) (qs ! i) a) = real (\<Sum>e\<in>set (fst s). ALG e qs i s)

goal (1 subgoal):
 1. real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (t\<^sub>p (fst s) (qs ! i) a) = real (\<Sum>e\<in>set (fst s). ALG e qs i s)

goal (1 subgoal):
 1. real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (\<Sum>e\<in>set (fst s). ALG e qs i s) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (\<Sum>e\<in>set (fst s). ALG e qs i s) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))

goal (1 subgoal):
 1. real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))

goal (1 subgoal):
 1. real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real (t\<^sub>p (fst s) (qs ! i) a) = (\<Sum>e\<in>set (fst s). real (ALG e qs i s))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma steps'_steps: "length as = length qs \<Longrightarrow> steps' s as qs (length as) = steps s as qs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length as = length qs \<Longrightarrow> steps' s as qs (length as) = Partial_Cost_Model.steps s as qs
[PROOF STEP]
by(induct arbitrary: s rule: list_induct2, simp_all)


[STATEMENT]
lemma steps'_length: "length qs = length as \<Longrightarrow> n \<le> length as
  \<Longrightarrow> length (steps' s qs as n) = length s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length qs = length as; n \<le> length as\<rbrakk> \<Longrightarrow> length (steps' s qs as n) = length s
[PROOF STEP]
apply(induct qs as arbitrary: s  n rule: list_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s n. n \<le> length [] \<Longrightarrow> length (steps' s [] [] n) = length s
 2. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. n \<le> length ys \<Longrightarrow> length (steps' s xs ys n) = length s; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> length (steps' s (x # xs) (y # ys) n) = length s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. n \<le> length ys \<Longrightarrow> length (steps' s xs ys n) = length s; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> length (steps' s (x # xs) (y # ys) n) = length s
[PROOF STEP]
apply(case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. n \<le> length ys \<Longrightarrow> length (steps' s xs ys n) = length s; n \<le> length (y # ys); n = 0\<rbrakk> \<Longrightarrow> length (steps' s (x # xs) (y # ys) n) = length s
 2. \<And>x xs y ys s n nat. \<lbrakk>length xs = length ys; \<And>s n. n \<le> length ys \<Longrightarrow> length (steps' s xs ys n) = length s; n \<le> length (y # ys); n = Suc nat\<rbrakk> \<Longrightarrow> length (steps' s (x # xs) (y # ys) n) = length s
[PROOF STEP]
by (auto)


[STATEMENT]
lemma steps'_set: "length qs = length as \<Longrightarrow> n \<le> length as
  \<Longrightarrow> set (steps' s qs as n) = set s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length qs = length as; n \<le> length as\<rbrakk> \<Longrightarrow> set (steps' s qs as n) = set s
[PROOF STEP]
apply(induct qs as arbitrary: s  n rule: list_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s n. n \<le> length [] \<Longrightarrow> set (steps' s [] [] n) = set s
 2. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. n \<le> length ys \<Longrightarrow> set (steps' s xs ys n) = set s; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> set (steps' s (x # xs) (y # ys) n) = set s
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. n \<le> length ys \<Longrightarrow> set (steps' s xs ys n) = set s; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> set (steps' s (x # xs) (y # ys) n) = set s
[PROOF STEP]
apply(case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. n \<le> length ys \<Longrightarrow> set (steps' s xs ys n) = set s; n \<le> length (y # ys); n = 0\<rbrakk> \<Longrightarrow> set (steps' s (x # xs) (y # ys) n) = set s
 2. \<And>x xs y ys s n nat. \<lbrakk>length xs = length ys; \<And>s n. n \<le> length ys \<Longrightarrow> set (steps' s xs ys n) = set s; n \<le> length (y # ys); n = Suc nat\<rbrakk> \<Longrightarrow> set (steps' s (x # xs) (y # ys) n) = set s
[PROOF STEP]
by(auto simp: set_step)


[STATEMENT]
lemma steps'_distinct2: "length qs = length as \<Longrightarrow> n \<le> length as
  \<Longrightarrow>  distinct s \<Longrightarrow> distinct (steps' s qs as n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length qs = length as; n \<le> length as; distinct s\<rbrakk> \<Longrightarrow> distinct (steps' s qs as n)
[PROOF STEP]
apply(induct qs as arbitrary: s  n rule: list_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s n. \<lbrakk>n \<le> length []; distinct s\<rbrakk> \<Longrightarrow> distinct (steps' s [] [] n)
 2. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. \<lbrakk>n \<le> length ys; distinct s\<rbrakk> \<Longrightarrow> distinct (steps' s xs ys n); n \<le> length (y # ys); distinct s\<rbrakk> \<Longrightarrow> distinct (steps' s (x # xs) (y # ys) n)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. \<lbrakk>n \<le> length ys; distinct s\<rbrakk> \<Longrightarrow> distinct (steps' s xs ys n); n \<le> length (y # ys); distinct s\<rbrakk> \<Longrightarrow> distinct (steps' s (x # xs) (y # ys) n)
[PROOF STEP]
apply(case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. \<lbrakk>n \<le> length ys; distinct s\<rbrakk> \<Longrightarrow> distinct (steps' s xs ys n); n \<le> length (y # ys); distinct s; n = 0\<rbrakk> \<Longrightarrow> distinct (steps' s (x # xs) (y # ys) n)
 2. \<And>x xs y ys s n nat. \<lbrakk>length xs = length ys; \<And>s n. \<lbrakk>n \<le> length ys; distinct s\<rbrakk> \<Longrightarrow> distinct (steps' s xs ys n); n \<le> length (y # ys); distinct s; n = Suc nat\<rbrakk> \<Longrightarrow> distinct (steps' s (x # xs) (y # ys) n)
[PROOF STEP]
by(auto simp: distinct_step)


[STATEMENT]
lemma steps'_distinct: "length qs = length as \<Longrightarrow> length as = n
  \<Longrightarrow> distinct (steps' s qs as n) = distinct s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length qs = length as; length as = n\<rbrakk> \<Longrightarrow> distinct (steps' s qs as n) = distinct s
[PROOF STEP]
by (induct qs as arbitrary: s n rule: list_induct2) (fastforce simp add: distinct_step)+


[STATEMENT]
lemma steps'_dist_perm: "length qs = length as \<Longrightarrow> length as = n
  \<Longrightarrow> dist_perm s s \<Longrightarrow> dist_perm (steps' s qs as n) (steps' s qs as n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length qs = length as; length as = n; dist_perm s s\<rbrakk> \<Longrightarrow> dist_perm (steps' s qs as n) (steps' s qs as n)
[PROOF STEP]
using steps'_set steps'_distinct
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?qs = length ?as; ?n \<le> length ?as\<rbrakk> \<Longrightarrow> set (steps' ?s ?qs ?as ?n) = set ?s
\<lbrakk>length ?qs = length ?as; length ?as = ?n\<rbrakk> \<Longrightarrow> distinct (steps' ?s ?qs ?as ?n) = distinct ?s

goal (1 subgoal):
 1. \<lbrakk>length qs = length as; length as = n; dist_perm s s\<rbrakk> \<Longrightarrow> dist_perm (steps' s qs as n) (steps' s qs as n)
[PROOF STEP]
by blast


[STATEMENT]
lemma steps'_append: "length qs = length as \<Longrightarrow> length qs = n \<Longrightarrow> steps' s (qs@[q]) (as@[a]) (Suc n) = step (steps' s qs as n) q a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length qs = length as; length qs = n\<rbrakk> \<Longrightarrow> steps' s (qs @ [q]) (as @ [a]) (Suc n) = step (steps' s qs as n) q a
[PROOF STEP]
apply(induct qs as arbitrary: s  n rule: list_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s n. length [] = n \<Longrightarrow> steps' s ([] @ [q]) ([] @ [a]) (Suc n) = step (steps' s [] [] n) q a
 2. \<And>x xs y ys s n. \<lbrakk>length xs = length ys; \<And>s n. length xs = n \<Longrightarrow> steps' s (xs @ [q]) (ys @ [a]) (Suc n) = step (steps' s xs ys n) q a; length (x # xs) = n\<rbrakk> \<Longrightarrow> steps' s ((x # xs) @ [q]) ((y # ys) @ [a]) (Suc n) = step (steps' s (x # xs) (y # ys) n) q a
[PROOF STEP]
by auto


[STATEMENT]
lemma ALG'_det_append: "n < length Strat \<Longrightarrow> n < length qs \<Longrightarrow> ALG'_det Strat (qs@a) init n x
                        = ALG'_det Strat qs init n x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
assume qs: "n < length qs"
[PROOF STATE]
proof (state)
this:
n < length qs

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
assume S: "n < length Strat"
[PROOF STATE]
proof (state)
this:
n < length Strat

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
have tt: "(qs @ a) ! n = qs ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qs @ a) ! n = qs ! n
[PROOF STEP]
using qs
[PROOF STATE]
proof (prove)
using this:
n < length qs

goal (1 subgoal):
 1. (qs @ a) ! n = qs ! n
[PROOF STEP]
by (simp add: nth_append)
[PROOF STATE]
proof (state)
this:
(qs @ a) ! n = qs ! n

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
have "steps' init (take n qs) (take n Strat) n = steps' init ((take n qs) @ drop n qs) ((take n Strat) @ (drop n Strat)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps' init (take n qs) (take n Strat) n = steps' init (take n qs @ drop n qs) (take n Strat @ drop n Strat) n
[PROOF STEP]
apply(rule steps'_rests)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (take n qs) = length (take n Strat)
 2. n \<le> length (take n Strat)
[PROOF STEP]
using S qs
[PROOF STATE]
proof (prove)
using this:
n < length Strat
n < length qs

goal (2 subgoals):
 1. length (take n qs) = length (take n Strat)
 2. n \<le> length (take n Strat)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps' init (take n qs) (take n Strat) n = steps' init (take n qs @ drop n qs) (take n Strat @ drop n Strat) n

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
steps' init (take n qs) (take n Strat) n = steps' init (take n qs @ drop n qs) (take n Strat @ drop n Strat) n
[PROOF STEP]
have A: "steps' init (take n qs) (take n Strat) n = steps' init qs Strat n"
[PROOF STATE]
proof (prove)
using this:
steps' init (take n qs) (take n Strat) n = steps' init (take n qs @ drop n qs) (take n Strat @ drop n Strat) n

goal (1 subgoal):
 1. steps' init (take n qs) (take n Strat) n = steps' init qs Strat n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps' init (take n qs) (take n Strat) n = steps' init qs Strat n

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
have "steps' init (take n qs) (take n Strat) n = steps' init ((take n qs) @ ((drop n qs)@a)) ((take n Strat) @((drop n Strat)@[])) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps' init (take n qs) (take n Strat) n = steps' init (take n qs @ drop n qs @ a) (take n Strat @ drop n Strat @ []) n
[PROOF STEP]
apply(rule steps'_rests)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (take n qs) = length (take n Strat)
 2. n \<le> length (take n Strat)
[PROOF STEP]
using S qs
[PROOF STATE]
proof (prove)
using this:
n < length Strat
n < length qs

goal (2 subgoals):
 1. length (take n qs) = length (take n Strat)
 2. n \<le> length (take n Strat)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps' init (take n qs) (take n Strat) n = steps' init (take n qs @ drop n qs @ a) (take n Strat @ drop n Strat @ []) n

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
steps' init (take n qs) (take n Strat) n = steps' init (take n qs @ drop n qs @ a) (take n Strat @ drop n Strat @ []) n
[PROOF STEP]
have B: "steps' init (take n qs) (take n Strat) n = steps' init (qs@a) (Strat@[]) n"
[PROOF STATE]
proof (prove)
using this:
steps' init (take n qs) (take n Strat) n = steps' init (take n qs @ drop n qs @ a) (take n Strat @ drop n Strat @ []) n

goal (1 subgoal):
 1. steps' init (take n qs) (take n Strat) n = steps' init (qs @ a) (Strat @ []) n
[PROOF STEP]
by (metis append_assoc List.append_take_drop_id)
[PROOF STATE]
proof (state)
this:
steps' init (take n qs) (take n Strat) n = steps' init (qs @ a) (Strat @ []) n

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
from A B
[PROOF STATE]
proof (chain)
picking this:
steps' init (take n qs) (take n Strat) n = steps' init qs Strat n
steps' init (take n qs) (take n Strat) n = steps' init (qs @ a) (Strat @ []) n
[PROOF STEP]
have "steps' init qs Strat n = steps' init (qs@a) (Strat@[]) n"
[PROOF STATE]
proof (prove)
using this:
steps' init (take n qs) (take n Strat) n = steps' init qs Strat n
steps' init (take n qs) (take n Strat) n = steps' init (qs @ a) (Strat @ []) n

goal (1 subgoal):
 1. steps' init qs Strat n = steps' init (qs @ a) (Strat @ []) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps' init qs Strat n = steps' init (qs @ a) (Strat @ []) n

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
steps' init qs Strat n = steps' init (qs @ a) (Strat @ []) n
[PROOF STEP]
have C: "steps' init qs Strat n = steps' init (qs@a) Strat n"
[PROOF STATE]
proof (prove)
using this:
steps' init qs Strat n = steps' init (qs @ a) (Strat @ []) n

goal (1 subgoal):
 1. steps' init qs Strat n = steps' init (qs @ a) Strat n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps' init qs Strat n = steps' init (qs @ a) Strat n

goal (1 subgoal):
 1. \<lbrakk>n < length Strat; n < length qs\<rbrakk> \<Longrightarrow> ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x
[PROOF STEP]
unfolding ALG'_det_def C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALG x (qs @ a) n (swaps (snd (Strat ! n)) (steps' init (qs @ a) Strat n), ()) = ALG x qs n (swaps (snd (Strat ! n)) (steps' init (qs @ a) Strat n), ())
[PROOF STEP]
unfolding ALG.simps tt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x < qs ! n in fst (swaps (snd (Strat ! n)) (steps' init (qs @ a) Strat n), ()) then 1 else 0) = (if x < qs ! n in fst (swaps (snd (Strat ! n)) (steps' init (qs @ a) Strat n), ()) then 1 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ALG'_det Strat (qs @ a) init n x = ALG'_det Strat qs init n x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ALG'_refl: "qs!i = x \<Longrightarrow> ALG' A qs init i x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qs ! i = x \<Longrightarrow> ALG' A qs init i x = 0
[PROOF STEP]
unfolding ALG'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qs ! i = x \<Longrightarrow> E (map_pmf (\<lambda>xa. real (ALG x qs i xa)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs))) = 0
[PROOF STEP]
by(simp add: split_def before_in_def)


[STATEMENT]
lemma ALGxy_det_alternativ: "ALGxy_det A qs init x y
   =  (\<Sum>i\<in>{i. i<length qs \<and> (qs!i \<in> {y,x})}. ALG'_det A qs init i y + ALG'_det A qs init i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
have f: "{i. i<length qs} = {..<length qs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length qs} = {..<length qs}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
{i. i < length qs} = {..<length qs}

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
have e: "{i. i<length qs \<and> (qs!i \<in> {y,x})} = {i. i<length qs} \<inter> {i. (qs!i \<in> {y,x})}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length qs \<and> qs ! i \<in> {y, x}} = {i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i < length qs \<and> qs ! i \<in> {y, x}} = {i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
have "(\<Sum>i\<in>{i. i<length qs \<and> (qs!i \<in> {y,x})}. ALG'_det A qs init i y + ALG'_det A qs init i x)
    = (\<Sum>i\<in>{i. i<length qs} \<inter> {i. (qs!i \<in> {y,x})}. ALG'_det A qs init i y + ALG'_det A qs init i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x) = (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
unfolding e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG'_det A qs init i y + ALG'_det A qs init i x) = (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x) = (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG'_det A qs init i y + ALG'_det A qs init i x)

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x) = (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG'_det A qs init i y + ALG'_det A qs init i x)

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{i. i<length qs}. (if i \<in> {i. (qs!i \<in> {y,x})} then ALG'_det A qs init i y + ALG'_det A qs init i x
                                                    else 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG'_det A qs init i y + ALG'_det A qs init i x) = (\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0)
[PROOF STEP]
apply(rule sum.inter_restrict)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. i < length qs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG'_det A qs init i y + ALG'_det A qs init i x) = (\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0)

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG'_det A qs init i y + ALG'_det A qs init i x) = (\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0)

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{..<length qs}. (if i \<in> {i. (qs!i \<in> {y,x})} then ALG'_det A qs init i y + ALG'_det A qs init i x
                                                    else 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0) = (\<Sum>i<length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0)
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0) = (\<Sum>i<length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0) = (\<Sum>i<length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0)

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0) = (\<Sum>i<length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0)

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
have "\<dots> = ALGxy_det A qs init x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0) = ALGxy_det A qs init x y
[PROOF STEP]
unfolding ALGxy_det_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0) = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG'_det A qs init i y + ALG'_det A qs init i x else 0) = ALGxy_det A qs init x y

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x) = ALGxy_det A qs init x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x) = ALGxy_det A qs init x y

goal (1 subgoal):
 1. ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ALGxy_det A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det A qs init i y + ALG'_det A qs init i x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ALGxy_def2:
  "ALGxy A qs init x y = (\<Sum>i\<in>{i. i<length qs \<and> (qs!i \<in> {y,x})}. ALG' A qs init i y + ALG' A qs init i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
have a: "{i. i<length qs \<and> (qs!i \<in> {y,x})} = {..<length qs} \<inter> {i. (qs!i \<in> {y,x})}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length qs \<and> qs ! i \<in> {y, x}} = {..<length qs} \<inter> {i. qs ! i \<in> {y, x}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i < length qs \<and> qs ! i \<in> {y, x}} = {..<length qs} \<inter> {i. qs ! i \<in> {y, x}}

goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
unfolding ALGxy_def a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{..<length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x) = (\<Sum>i\<in>{..<length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ALGxy A qs init x y = (\<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG' A qs init i y + ALG' A qs init i x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ALGxy_append: "ALGxy A (rs@[r]) init x y =
      ALGxy A rs init x y + (if (r \<in> {y,x}) then ALG' A (rs@[r]) init (length rs) y + ALG' A (rs@[r]) init (length rs) x else 0 )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
have "ALGxy A (rs@[r]) init x y = (\<Sum>i\<in>{..<(Suc (length rs))} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}.
       ALG' A (rs @ [r]) init i y +
       ALG' A (rs @ [r]) init i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = (\<Sum>i\<in>{..<Suc (length rs)} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}. ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x)
[PROOF STEP]
unfolding ALGxy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{..<length (rs @ [r])} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}. ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x) = (\<Sum>i\<in>{..<Suc (length rs)} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}. ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
ALGxy A (rs @ [r]) init x y = (\<Sum>i\<in>{..<Suc (length rs)} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}. ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x)

goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ALGxy A (rs @ [r]) init x y = (\<Sum>i\<in>{..<Suc (length rs)} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}. ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x)

goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{..<(Suc (length rs))}. (if i\<in>{i. (rs @ [r]) ! i \<in> {y, x}} then
       ALG' A (rs @ [r]) init i y +
       ALG' A (rs @ [r]) init i x else 0) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{..<Suc (length rs)} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}. ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x) = (\<Sum>i<Suc (length rs). if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0)
[PROOF STEP]
apply(rule sum.inter_restrict)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {..<Suc (length rs)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{..<Suc (length rs)} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}. ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x) = (\<Sum>i<Suc (length rs). if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0)

goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{..<Suc (length rs)} \<inter> {i. (rs @ [r]) ! i \<in> {y, x}}. ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x) = (\<Sum>i<Suc (length rs). if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0)

goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{..<length rs}. (if i\<in>{i. (rs @ [r]) ! i \<in> {y, x}} then
       ALG' A (rs @ [r]) init i y +
       ALG' A (rs @ [r]) init i x else 0) ) + (if length rs\<in>{i. (rs @ [r]) ! i \<in> {y, x}} then
       ALG' A (rs @ [r]) init (length rs) y +
       ALG' A (rs @ [r]) init(length rs) x else 0) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<Suc (length rs). if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) = (\<Sum>i<length rs. if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) + (if length rs \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<Suc (length rs). if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) = (\<Sum>i<length rs. if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) + (if length rs \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)

goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<Suc (length rs). if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) = (\<Sum>i<length rs. if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) + (if length rs \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)

goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
have "\<dots> = ALGxy A rs init x y + (if r \<in> {y, x} then
       ALG' A (rs @ [r]) init (length rs) y +
       ALG' A (rs @ [r]) init(length rs) x else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length rs. if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) + (if length rs \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0) = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
apply(simp add: ALGxy_def sum.inter_restrict nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length rs. if rs ! i = y \<or> rs ! i = x then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) = (\<Sum>xa<length rs. if rs ! xa = y \<or> rs ! xa = x then ALG' A rs init xa y + ALG' A rs init xa x else 0)
[PROOF STEP]
unfolding ALG'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length rs. if rs ! i = y \<or> rs ! i = x then E (map_pmf (\<lambda>x. real (ALG y (rs @ [r]) i x)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i (rs @ [r])))) + E (map_pmf (\<lambda>xa. real (ALG x (rs @ [r]) i xa)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i (rs @ [r])))) else 0) = (\<Sum>xa<length rs. if rs ! xa = y \<or> rs ! xa = x then E (map_pmf (\<lambda>x. real (ALG y rs xa x)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa rs))) + E (map_pmf (\<lambda>xb. real (ALG x rs xa xb)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa rs))) else 0)
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {..<length rs} = {..<length rs}
 2. \<And>xa. xa \<in> {..<length rs} \<Longrightarrow> (if rs ! xa = y \<or> rs ! xa = x then E (map_pmf (\<lambda>x. real (ALG y (rs @ [r]) xa x)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa (rs @ [r])))) + E (map_pmf (\<lambda>xb. real (ALG x (rs @ [r]) xa xb)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa (rs @ [r])))) else 0) = (if rs ! xa = y \<or> rs ! xa = x then E (map_pmf (\<lambda>x. real (ALG y rs xa x)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa rs))) + E (map_pmf (\<lambda>xb. real (ALG x rs xa xb)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa rs))) else 0)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {..<length rs} \<Longrightarrow> (if rs ! xa = y \<or> rs ! xa = x then E (map_pmf (\<lambda>x. real (ALG y (rs @ [r]) xa x)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa (rs @ [r])))) + E (map_pmf (\<lambda>xb. real (ALG x (rs @ [r]) xa xb)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa (rs @ [r])))) else 0) = (if rs ! xa = y \<or> rs ! xa = x then E (map_pmf (\<lambda>x. real (ALG y rs xa x)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa rs))) + E (map_pmf (\<lambda>xb. real (ALG x rs xa xb)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take xa rs))) else 0)
[PROOF STEP]
by(auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length rs. if i \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init i y + ALG' A (rs @ [r]) init i x else 0) + (if length rs \<in> {i. (rs @ [r]) ! i \<in> {y, x}} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0) = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)

goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)

goal (1 subgoal):
 1. ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ALGxy A (rs @ [r]) init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ALGxy_wholerange: "ALGxy A qs init x y
    = (\<Sum>i<(length qs). (if qs ! i \<in> {y, x}
          then ALG' A qs init i y + ALG' A qs init i x
          else 0 ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
have "ALGxy A qs init x y
      = (\<Sum>i\<in> {i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}.
       ALG' A qs init i y + ALG' A qs init i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
unfolding ALGxy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{..<length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x) = (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {..<length qs} \<inter> {i. qs ! i \<in> {y, x}} = {i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}
 2. \<And>xa. xa \<in> {i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}} \<Longrightarrow> ALG' A qs init xa y + ALG' A qs init xa x = ALG' A qs init xa y + ALG' A qs init xa x
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {..<length qs} \<inter> {i. qs ! i = y \<or> qs ! i = x} = {i. i < length qs} \<inter> {i. qs ! i = y \<or> qs ! i = x}
 2. \<And>xa. xa \<in> {i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}} \<Longrightarrow> ALG' A qs init xa y + ALG' A qs init xa x = ALG' A qs init xa y + ALG' A qs init xa x
[PROOF STEP]
apply(blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}} \<Longrightarrow> ALG' A qs init xa y + ALG' A qs init xa x = ALG' A qs init xa y + ALG' A qs init xa x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ALGxy A qs init x y = (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x)

goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ALGxy A qs init x y = (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x)

goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{i. i < length qs}.  if i \<in> {i. qs ! i \<in> {y, x}}
                                    then ALG' A qs init i y + ALG' A qs init i x
                                    else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x) = (\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
by(rule sum.inter_restrict) simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x) = (\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG' A qs init i y + ALG' A qs init i x else 0)

goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < length qs} \<inter> {i. qs ! i \<in> {y, x}}. ALG' A qs init i y + ALG' A qs init i x) = (\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG' A qs init i y + ALG' A qs init i x else 0)

goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
have "\<dots> = (\<Sum>i<(length qs). (if qs ! i \<in> {y, x}
          then ALG' A qs init i y + ALG' A qs init i x
          else 0 ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG' A qs init i y + ALG' A qs init i x else 0) = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {i. i < length qs} = {..<length qs}
 2. \<And>xa. xa \<in> {..<length qs} \<Longrightarrow> (if xa \<in> {i. qs ! i \<in> {y, x}} then ALG' A qs init xa y + ALG' A qs init xa x else 0) = (if qs ! xa \<in> {y, x} then ALG' A qs init xa y + ALG' A qs init xa x else 0)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs. if i \<in> {i. qs ! i \<in> {y, x}} then ALG' A qs init i y + ALG' A qs init i x else 0) = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)

goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)

goal (1 subgoal):
 1. ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ALGxy A qs init x y = (\<Sum>i<length qs. if qs ! i \<in> {y, x} then ALG' A qs init i y + ALG' A qs init i x else 0)

goal:
No subgoals!
[PROOF STEP]
qed