[STATEMENT]
lemma umformung:
  fixes A :: "(('a::linorder) list,'is,'a,(nat * nat list)) alg_on_rand"
  assumes no_paid: "\<And>is s q. \<forall>((free,paid),_) \<in> (snd A (s,is) q). paid=[]"
  assumes inlist: "set qs \<subseteq> set init"
  assumes dist: "distinct init"
  assumes "\<And>x. x < length qs \<Longrightarrow> finite (set_pmf (config'' A qs init x))"
  shows "T\<^sub>p_on_rand A init qs =
    (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALGxy A qs init x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have config_dist: "\<forall>n. \<forall>xa \<in> set_pmf (config'' A qs init n). distinct (fst xa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<forall>xa\<in>set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take n qs)). distinct (fst xa)
[PROOF STEP]
using dist config_rand_distinct
[PROOF STATE]
proof (prove)
using this:
distinct init
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). distinct (fst x) = distinct ?init

goal (1 subgoal):
 1. \<forall>n. \<forall>xa\<in>set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take n qs)). distinct (fst xa)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>n. \<forall>xa\<in>set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take n qs)). distinct (fst xa)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have E0: "T\<^sub>p_on_rand A init qs =
        (\<Sum>i\<in>{..<length qs}. T\<^sub>p_on_rand_n A init qs i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs}
[PROOF STEP]
unfolding T_on_rand_as_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs} = sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs}

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs}

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have "\<dots> =
  (\<Sum>i<length qs.  E (bind_pmf (config'' A qs init i)
                          (\<lambda>s. bind_pmf (snd A s (qs ! i))
                            (\<lambda>(a, nis). return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs} = (\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s))))))
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {..<length qs} = {..<length qs}
 2. \<And>x. x \<in> {..<length qs} \<Longrightarrow> Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs x = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs) \<bind> (\<lambda>s. snd A s (qs ! x) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>xa\<in>set init. ALG xa qs x s)))))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs x = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs) \<bind> (\<lambda>s. snd A s (qs ! x) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>xa\<in>set init. ALG xa qs x s)))))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length qs \<Longrightarrow> E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs) \<bind> (\<lambda>s. snd A s (qs ! x) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) (qs ! x) a))))) = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs) \<bind> (\<lambda>s. snd A s (qs ! x) \<bind> (\<lambda>(a, nis). return_pmf (\<Sum>xa\<in>set init. real (if xa < qs ! x in fst s then 1 else 0)))))
[PROOF STEP]
apply(rule arg_cong[where f=E])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length qs \<Longrightarrow> Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs) \<bind> (\<lambda>s. snd A s (qs ! x) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) (qs ! x) a)))) = Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs) \<bind> (\<lambda>s. snd A s (qs ! x) \<bind> (\<lambda>(a, nis). return_pmf (\<Sum>xa\<in>set init. real (if xa < qs ! x in fst s then 1 else 0))))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x < length qs \<Longrightarrow> Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs) = Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)
 2. \<And>x xa. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs))\<rbrakk> \<Longrightarrow> snd A xa (qs ! x) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst xa) (qs ! x) a))) = snd A xa (qs ! x) \<bind> (\<lambda>(a, nis). return_pmf (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs))\<rbrakk> \<Longrightarrow> snd A xa (qs ! x) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst xa) (qs ! x) a))) = snd A xa (qs ! x) \<bind> (\<lambda>(a, nis). return_pmf (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0)))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs))\<rbrakk> \<Longrightarrow> snd A xa (qs ! x) = snd A xa (qs ! x)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (case xb of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst xa) (qs ! x) a))) = (case xb of (a, nis) \<Rightarrow> return_pmf (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (case xb of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst xa) (qs ! x) a))) = (case xb of (a, nis) \<Rightarrow> return_pmf (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0)))
[PROOF STEP]
apply(simp add: split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> real (t\<^sub>p (fst xa) (qs ! x) (fst xb)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
apply(subst t\<^sub>p_sumofALGreal)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> distinct (fst xa)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> snd (fst xb) = []
 3. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 4. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> distinct (fst xa)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> snd (fst xb) = []
 3. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 4. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x_ < length qs
xa_ \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x_ qs))
xb_ \<in> set_pmf (snd A xa_ (qs ! x_))

goal (4 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> distinct (fst xa)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> snd (fst xb) = []
 3. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 4. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x_ < length qs
xa_ \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x_ qs))
xb_ \<in> set_pmf (snd A xa_ (qs ! x_))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x_ < length qs
xa_ \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x_ qs))
xb_ \<in> set_pmf (snd A xa_ (qs ! x_))

goal (1 subgoal):
 1. distinct (fst xa_)
[PROOF STEP]
using config_dist
[PROOF STATE]
proof (prove)
using this:
x_ < length qs
xa_ \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x_ qs))
xb_ \<in> set_pmf (snd A xa_ (qs ! x_))
\<forall>n. \<forall>xa\<in>set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take n qs)). distinct (fst xa)

goal (1 subgoal):
 1. distinct (fst xa_)
[PROOF STEP]
by(metis)
[PROOF STATE]
proof (state)
this:
distinct (fst xa_)

goal (3 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> snd (fst xb) = []
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 3. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> snd (fst xb) = []
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 3. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
case (2 a b c)
[PROOF STATE]
proof (state)
this:
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))

goal (3 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> snd (fst xb) = []
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 3. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))

goal (1 subgoal):
 1. snd (fst c) = []
[PROOF STEP]
using no_paid[of "fst b" "snd b"]
[PROOF STATE]
proof (prove)
using this:
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))
\<forall>((free, paid), uu_)\<in>set_pmf (snd A (fst b, snd b) ?q). paid = []

goal (1 subgoal):
 1. snd (fst c) = []
[PROOF STEP]
by(auto simp add: split_def)
[PROOF STATE]
proof (state)
this:
snd (fst c) = []

goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
case (3 a b c)
[PROOF STATE]
proof (state)
this:
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))

goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
with config_rand_set
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). set (fst x) = set ?init
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))
[PROOF STEP]
have a: "set (fst b) = set init"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). set (fst x) = set ?init
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))

goal (1 subgoal):
 1. set (fst b) = set init
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
set (fst b) = set init

goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
with inlist
[PROOF STATE]
proof (chain)
picking this:
set qs \<subseteq> set init
set (fst b) = set init
[PROOF STEP]
have " set qs \<subseteq> set (fst b)"
[PROOF STATE]
proof (prove)
using this:
set qs \<subseteq> set init
set (fst b) = set init

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

goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> qs ! x \<in> set (fst xa)
 2. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))
set qs \<subseteq> set (fst b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))
set qs \<subseteq> set (fst b)

goal (1 subgoal):
 1. qs ! a \<in> set (fst b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qs ! a \<in> set (fst b)

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
case (4 a b c)
[PROOF STATE]
proof (state)
this:
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
with config_rand_set
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). set (fst x) = set ?init
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))
[PROOF STEP]
have a: "set (fst b) = set init"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). set (fst x) = set ?init
a < length qs
b \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take a qs))
c \<in> set_pmf (snd A b (qs ! a))

goal (1 subgoal):
 1. set (fst b) = set init
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
set (fst b) = set init

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>x < length qs; xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)); xb \<in> set_pmf (snd A xa (qs ! x))\<rbrakk> \<Longrightarrow> (\<Sum>e\<in>set (fst xa). real (ALG e qs x xa)) = (\<Sum>xb\<in>set init. real (if xb < qs ! x in fst xa then 1 else 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (fst b) = set init
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (fst b) = set init

goal (1 subgoal):
 1. (\<Sum>e\<in>set (fst b). real (ALG e qs a b)) = (\<Sum>x\<in>set init. real (if x < qs ! a in fst b then 1 else 0))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>set (fst b). real (ALG e qs a b)) = (\<Sum>x\<in>set init. real (if x < qs ! a in fst b then 1 else 0))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs} = (\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s))))))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
(* hier erst s, dann init *)
[PROOF STATE]
proof (state)
this:
sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs} = (\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s))))))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs) {..<length qs} = (\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s))))))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have "\<dots> = (\<Sum>i<length qs.
               E (map_pmf (\<lambda>(is, s). (real (\<Sum>x\<in>set init. ALG x qs i (is,s))))
                           (config'' A qs init i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s)))))) = (\<Sum>i<length qs. E (map_pmf (\<lambda>(is, s). real (\<Sum>x\<in>set init. ALG x qs i (is, s))) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs))))
[PROOF STEP]
apply(simp only: map_pmf_def split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>p. return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s)))))) = (\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>x. return_pmf (real (\<Sum>xa\<in>set init. ALG xa qs i (fst x, snd x))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s)))))) = (\<Sum>i<length qs. E (map_pmf (\<lambda>(is, s). real (\<Sum>x\<in>set init. ALG x qs i (is, s))) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs))))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, nis). return_pmf (real (\<Sum>x\<in>set init. ALG x qs i s)))))) = (\<Sum>i<length qs. E (map_pmf (\<lambda>(is, s). real (\<Sum>x\<in>set init. ALG x qs i (is, s))) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs))))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have E1: "\<dots> = (\<Sum>i<length qs. (\<Sum>x\<in>set init. ALG' A qs init i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. E (map_pmf (\<lambda>(is, s). real (\<Sum>x\<in>set init. ALG x qs i (is, s))) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs)))) = (\<Sum>i<length qs. sum (ALG' A qs init i) (set init))
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {..<length qs} = {..<length qs}
 2. \<And>x. x \<in> {..<length qs} \<Longrightarrow> E (map_pmf (\<lambda>(is, s). real (\<Sum>xa\<in>set init. ALG xa qs x (is, s))) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs))) = sum (ALG' A qs init x) (set init)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> E (map_pmf (\<lambda>(is, s). real (\<Sum>xa\<in>set init. ALG xa qs x (is, s))) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs))) = sum (ALG' A qs init x) (set init)
[PROOF STEP]
apply(simp add: split_def ALG'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length qs \<Longrightarrow> E (map_pmf (\<lambda>p. \<Sum>xa\<in>set init. real (if xa < qs ! x in fst p then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs))) = (\<Sum>xa\<in>set init. E (map_pmf (\<lambda>xb. real (if xa < qs ! x in fst xb then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs))))
[PROOF STEP]
apply(rule E_linear_sum_allg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length qs \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
by(rule assms(4))
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. E (map_pmf (\<lambda>(is, s). real (\<Sum>x\<in>set init. ALG x qs i (is, s))) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs)))) = (\<Sum>i<length qs. sum (ALG' A qs init i) (set init))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. E (map_pmf (\<lambda>(is, s). real (\<Sum>x\<in>set init. ALG x qs i (is, s))) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs)))) = (\<Sum>i<length qs. sum (ALG' A qs init i) (set init))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have E2: "\<dots> = (\<Sum>x\<in>set init.
          (\<Sum>i<length qs. ALG' A qs init i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. sum (ALG' A qs init i) (set init)) = (\<Sum>x\<in>set init. \<Sum>i<length qs. ALG' A qs init i x)
[PROOF STEP]
by(rule sum.swap)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. sum (ALG' A qs init i) (set init)) = (\<Sum>x\<in>set init. \<Sum>i<length qs. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
(* die summen tauschen *)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. sum (ALG' A qs init i) (set init)) = (\<Sum>x\<in>set init. \<Sum>i<length qs. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. sum (ALG' A qs init i) (set init)) = (\<Sum>x\<in>set init. \<Sum>i<length qs. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have E3: "\<dots> = (\<Sum>x\<in>set init.
          (\<Sum>y\<in>set init.
            (\<Sum>i\<in>{i. i<length qs \<and> qs!i=y}. ALG' A qs init i x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set init. \<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>x\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
proof (rule sum.cong, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
x \<in> set init

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
have "(\<Sum>i<length qs. ALG' A qs init i x)
                = sum (%i. ALG' A qs init i x) {i. i<length qs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>i | i < length qs. ALG' A qs init i x)
[PROOF STEP]
by (metis lessThan_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>i | i < length qs. ALG' A qs init i x)

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>i | i < length qs. ALG' A qs init i x)

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
have "\<dots> = sum (%i. ALG' A qs init i x)
                        (\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length qs. ALG' A qs init i x) = (\<Sum>i\<in>(\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}). ALG' A qs init i x)
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {i. i < length qs} = (\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y})
 2. \<And>xa. xa \<in> (\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}) \<Longrightarrow> ALG' A qs init xa x = ALG' A qs init xa x
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length qs \<Longrightarrow> qs ! x \<in> set init
[PROOF STEP]
using inlist
[PROOF STATE]
proof (prove)
using this:
set qs \<subseteq> set init

goal (1 subgoal):
 1. \<And>x. x < length qs \<Longrightarrow> qs ! x \<in> set init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs. ALG' A qs init i x) = (\<Sum>i\<in>(\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}). ALG' A qs init i x)

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs. ALG' A qs init i x) = (\<Sum>i\<in>(\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}). ALG' A qs init i x)

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
have "\<dots> = sum (%t. sum (%i. ALG' A qs init i x) {i. i<length qs \<and> qs ! i = t}) {y. y\<in> set init}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>(\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}). ALG' A qs init i x) = (\<Sum>t\<in>{y. y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = t. ALG' A qs init i x)
[PROOF STEP]
apply(rule sum.UNION_disjoint)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {y. y \<in> set init}
 2. \<forall>i\<in>{y. y \<in> set init}. finite {ia. ia < length qs \<and> qs ! ia = i}
 3. \<forall>i\<in>{y. y \<in> set init}. \<forall>j\<in>{y. y \<in> set init}. i \<noteq> j \<longrightarrow> {ia. ia < length qs \<and> qs ! ia = i} \<inter> {i. i < length qs \<and> qs ! i = j} = {}
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set init. \<forall>j\<in>set init. i \<noteq> j \<longrightarrow> {ia. ia < length qs \<and> qs ! ia = i} \<inter> {i. i < length qs \<and> qs ! i = j} = {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>(\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}). ALG' A qs init i x) = (\<Sum>t\<in>{y. y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = t. ALG' A qs init i x)

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>(\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}). ALG' A qs init i x) = (\<Sum>t\<in>{y. y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = t. ALG' A qs init i x)

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
have "\<dots> = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y.
                       ALG' A qs init i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>t\<in>{y. y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = t. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>t\<in>{y. y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = t. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. (\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. set init = set init
[PROOF STEP]
qed (simp)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set init. \<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>x\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set init. \<Sum>i<length qs. ALG' A qs init i x) = (\<Sum>x\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in> (set init \<times> set init).
            (\<Sum>i\<in>{i. i<length qs \<and> qs!i=y}. ALG' A qs init i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
by (rule sum.cartesian_product)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in> {(x,y). x\<in>set init \<and> y\<in> set init}.
            (\<Sum>i\<in>{i. i<length qs \<and> qs!i=y}. ALG' A qs init i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have E4: "\<dots> = (\<Sum>(x,y)\<in>{(x,y). x\<in>set init \<and> y\<in> set init \<and> x\<noteq>y}.
            (\<Sum>i\<in>{i. i<length qs \<and> qs!i=y}. ALG' A qs init i x))" (is "(\<Sum>(x,y)\<in> ?L. ?f x y) = (\<Sum>(x,y)\<in> ?R. ?f x y)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
let ?M = "{(x,y). x\<in>set init \<and> y\<in> set init \<and> x=y}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
have A: "?L = ?R \<union> ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> set init \<and> y \<in> set init} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set init \<and> y \<in> set init} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}

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

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
have "(\<Sum>(x,y)\<in> ?L. ?f x y) = (\<Sum>(x,y)\<in> ?R \<union> ?M. ?f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
by(simp only: A)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

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

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in> ?R. ?f x y) + (\<Sum>(x,y)\<in> ?M. ?f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
apply(rule sum.union_disjoint)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}
 2. finite {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}
 3. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<inter> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y} = {}
[PROOF STEP]
apply(rule finite_subset[where B="set init \<times> set init"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<subseteq> set init \<times> set init
 2. finite (set init \<times> set init)
 3. finite {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}
 4. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<inter> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y} = {}
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}
[PROOF STEP]
apply(rule finite_subset[where B="set init \<times> set init"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y} \<subseteq> set init \<times> set init
 2. finite (set init \<times> set init)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

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

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
have "(\<Sum>(x,y)\<in> ?M. ?f x y) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = 0
[PROOF STEP]
apply(rule sum.neutral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = 0
[PROOF STEP]
by (auto simp add: ALG'_refl)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x = y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = 0

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}.
            (\<Sum>i\<in>{i. i<length qs \<and> qs!i=y}. ALG' A qs init i x)
           + (\<Sum>i\<in>{i. i<length qs \<and> qs!i=x}. ALG' A qs init i y) )"
            (is "(\<Sum>(x,y)\<in> ?L. ?f x y) = (\<Sum>(x,y)\<in> ?R. ?f x y +  ?f y x)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
let ?R' = "{(x,y). x \<in> set init \<and> y\<in>set init \<and> y<x}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
have A: "?L = ?R \<union> ?R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}

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

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
have C: "?R' = (%(x,y). (y, x)) ` ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x} = (\<lambda>(x, y). (y, x)) ` {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x} = (\<lambda>(x, y). (y, x)) ` {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
have D: "(\<Sum>(x,y)\<in> ?R'. ?f x y) = (\<Sum>(x,y)\<in> ?R. ?f y x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)
[PROOF STEP]
have "(\<Sum>(x,y)\<in> ?R'. ?f x y) = (\<Sum>(x,y)\<in> (%(x,y). (y, x)) ` ?R. ?f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>(\<lambda>(x, y). (y, x)) ` {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
by(simp only: C)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>(\<lambda>(x, y). (y, x)) ` {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

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

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)
[PROOF STEP]
have "(\<Sum>z\<in> (%(x,y). (y, x)) ` ?R. (%(x,y). ?f x y) z) = (\<Sum>z\<in>?R. ((%(x,y). ?f x y) \<circ> (%(x,y). (y, x))) z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>z\<in>(\<lambda>(x, y). (y, x)) ` {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. case z of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) \<circ> (\<lambda>(x, y). (y, x))) {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}
[PROOF STEP]
apply(rule sum.reindex)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>(x, y). (y, x)) {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}
[PROOF STEP]
by(fact swap_inj_on)
[PROOF STATE]
proof (state)
this:
(\<Sum>z\<in>(\<lambda>(x, y). (y, x)) ` {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. case z of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) \<circ> (\<lambda>(x, y). (y, x))) {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>z\<in>(\<lambda>(x, y). (y, x)) ` {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. case z of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) \<circ> (\<lambda>(x, y). (y, x))) {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)
[PROOF STEP]
have "\<dots> = (\<Sum>z\<in>?R. (%(x,y). ?f y x) z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) \<circ> (\<lambda>(x, y). (y, x))) {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. case z of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}
 2. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) \<circ> (\<lambda>(x, y). (y, x))) x = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) \<circ> (\<lambda>(x, y). (y, x))) {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. case z of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
have "(\<Sum>(x,y)\<in> ?L. ?f x y) = (\<Sum>(x,y)\<in> ?R \<union> ?R'. ?f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
by(simp only: A)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

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

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in> ?R. ?f x y) + (\<Sum>(x,y)\<in> ?R'. ?f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)
[PROOF STEP]
apply(rule sum.union_disjoint)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}
 2. finite {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}
 3. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x} = {}
[PROOF STEP]
apply(rule finite_subset[where B="set init \<times> set init"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<subseteq> set init \<times> set init
 2. finite (set init \<times> set init)
 3. finite {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}
 4. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x} = {}
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}
[PROOF STEP]
apply(rule finite_subset[where B="set init \<times> set init"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x} \<subseteq> set init \<times> set init
 2. finite (set init \<times> set init)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x)

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

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in> ?R. ?f x y) + (\<Sum>(x,y)\<in> ?R. ?f y x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)
[PROOF STEP]
by(simp only: D)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> y < x}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)

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

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in> ?R. ?f x y + ?f y x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))
[PROOF STEP]
by(simp add: split_def sum.distrib[symmetric])
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}. \<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y))

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have E5: "\<dots> = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}.
            (\<Sum>i\<in>{i. i<length qs \<and> (qs!i=y \<or> qs!i=x)}. ALG' A qs init i y + ALG' A qs init i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = 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. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}
 2. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}
[PROOF STEP]
obtain a b where x: "x=(a,b)" and a: "a \<in> set init" "b \<in> set init" "a < b"
[PROOF STATE]
proof (prove)
using this:
x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = (a, b); a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (a, b)
a \<in> set init
b \<in> set init
a < b

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (a, b)
a \<in> set init
b \<in> set init
a < b
[PROOF STEP]
have "a\<noteq>b"
[PROOF STATE]
proof (prove)
using this:
x = (a, b)
a \<in> set init
b \<in> set init
a < b

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

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> b
[PROOF STEP]
have disj: "{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a} = {}"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. {i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a} = {}

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
have unio: "{i. i < length qs \<and> (qs ! i = b \<or> qs ! i = a)}
            = {i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length qs \<and> (qs ! i = b \<or> qs ! i = a)} = {i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i < length qs \<and> (qs ! i = b \<or> qs ! i = a)} = {i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
have "(\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union>
          {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b +
               ALG' A qs init i a)
               = (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b}. ALG' A qs init i b +
               ALG' A qs init i a) + (\<Sum>i\<in>
          {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b +
               ALG' A qs init i a) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter>
          {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b +
               ALG' A qs init i a) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a)
[PROOF STEP]
apply(rule sum_Un)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {i. i < length qs \<and> qs ! i = b}
 2. finite {i. i < length qs \<and> qs ! i = a}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a)

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a)

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b}. ALG' A qs init i b +
               ALG' A qs init i a) + (\<Sum>i\<in>
          {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b +
               ALG' A qs init i a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a)
[PROOF STEP]
using disj
[PROOF STATE]
proof (prove)
using this:
{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a} = {}

goal (1 subgoal):
 1. (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a)

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a)

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b}. ALG' A qs init i a)
         + (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b)
[PROOF STEP]
by (auto simp: ALG'_refl)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i b + ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b)

goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<Longrightarrow> (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b)

goal (1 subgoal):
 1. (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b)

goal (1 subgoal):
 1. (case (a, b) of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case (a, b) of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)
[PROOF STEP]
apply(simp add: split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b) \<Longrightarrow> (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b) = (\<Sum>i | i < length qs \<and> (qs ! i = b \<or> qs ! i = a). ALG' A qs init i b + ALG' A qs init i a)
[PROOF STEP]
unfolding unio
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b) \<Longrightarrow> (\<Sum>i | i < length qs \<and> qs ! i = b. ALG' A qs init i a) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG' A qs init i b) = (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. ALG' A qs init i b + ALG' A qs init i a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (\<Sum>i | i < length qs \<and> qs ! i = y. ALG' A qs init i x) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG' A qs init i y)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
have E6: "\<dots> = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}.
                  ALGxy A qs init x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
unfolding ALGxy_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> 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]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG' A qs init i y + ALG' A qs init i x) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)

goal:
No subgoals!
[PROOF STEP]
qed