[STATEMENT]
lemma umformung_OPT':
  assumes inlist: "set qs \<subseteq> set init"
  assumes dist: "distinct init"
  assumes qsStrat: "length qs = length Strat"
  assumes noStupid: "\<And>x l. x<length Strat \<Longrightarrow> l< length (snd (Strat ! x)) \<Longrightarrow> Suc ((snd (Strat ! x))!l)  < length init"
  shows "T\<^sub>p init qs Strat =
    (\<Sum>(x,y)\<in>{(x,y::('a::linorder)). x \<in> set init \<and> y\<in>set init \<and> x<y}.
          ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
(* have config_dist: "\<forall>n. \<forall>xa \<in> set_pmf (config\<^sub>p (I, S) qs init n). distinct (snd xa)"
      using dist config_rand_distinct by metis
*)

  (* ersten Teil umformen: *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "(\<Sum>i\<in>{..<length qs}.
    (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P (snd (Strat!i)) x y (steps' init qs Strat i)) )
                = (\<Sum>i\<in>{..<length qs}.
               (\<Sum>z\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P (snd (Strat!i)) (fst z) (snd z) (steps' init qs Strat i)) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>i<length qs. \<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i))
[PROOF STEP]
by(auto simp: split_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>i<length qs. \<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>i<length qs. \<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "\<dots>
       = (\<Sum>z\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}.
                (\<Sum>i\<in>{..<length qs}. ALG_P (snd (Strat!i)) (fst z) (snd z) (steps' init qs Strat i)) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. \<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i)) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i))
[PROOF STEP]
by(rule sum.swap)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i)) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i)) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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>{..<length qs}. ALG_P (snd (Strat!i)) x y (steps' init qs Strat i)) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))
[PROOF STEP]
by(auto simp: split_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) (fst z) (snd z) (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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}.
                ALG_Pxy Strat 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<length qs. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y)
[PROOF STEP]
unfolding ALG_P'_def ALG_Pxy_def
[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<length qs. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))
[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}. \<Sum>i<length qs. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y)
[PROOF STEP]
have paid_part: "(\<Sum>i\<in>{..<length qs}.
    (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P (snd (Strat!i)) x y (steps' init qs Strat i)) )
      = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}.
                ALG_Pxy Strat qs init x y)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y)

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

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
(* zweiten Teil umformen: *)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
let ?config = "(%i. swaps (snd (Strat!i)) (steps' init qs Strat i))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "(\<Sum>i\<in>{..<length qs}.
                (\<Sum>e\<in>set init. ALG e qs i (?config i, ())))
        = (\<Sum>e\<in>set init.
            (\<Sum>i\<in>{..<length qs}. ALG e qs i (?config i, ())))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>e\<in>set init. \<Sum>i<length qs. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
by(rule sum.swap)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>e\<in>set init. \<Sum>i<length qs. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>e\<in>set init. \<Sum>i<length qs. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>set init.
          (\<Sum>y\<in>set init.
            (\<Sum>i\<in>{i. i<length qs \<and> qs!i=y}. ALG e qs i (?config i,()))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>set init. \<Sum>i<length qs. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>e\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
have "(\<Sum>i<length qs. ALG x qs i (?config i, ()))
                = sum (%i. ALG x qs i (?config i, ())) {i. i<length qs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
by (simp add: lessThan_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
have "\<dots> = sum (%i. ALG x qs i (?config i, ()))
                        (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i\<in>(\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}). ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs xa (swaps (snd (Strat ! xa)) (steps' init qs Strat xa), ()) = ALG x qs xa (swaps (snd (Strat ! xa)) (steps' init qs Strat xa), ())
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
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 x qs xa (swaps (snd (Strat ! xa)) (steps' init qs Strat xa), ()) = ALG x qs xa (swaps (snd (Strat ! xa)) (steps' init qs Strat xa), ())
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

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 x qs xa (swaps (snd (Strat ! xa)) (steps' init qs Strat xa), ()) = ALG x qs xa (swaps (snd (Strat ! xa)) (steps' init qs Strat xa), ())
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length qs} = (\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y})
[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:
{i. i < length qs} = (\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y})

goal (1 subgoal):
 1. \<And>xa. xa \<in> (\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}) \<Longrightarrow> ALG x qs xa (swaps (snd (Strat ! xa)) (steps' init qs Strat xa), ()) = ALG x qs xa (swaps (snd (Strat ! xa)) (steps' init qs Strat xa), ())
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i\<in>(\<Union>y\<in>{y. y \<in> set init}. {i. i < length qs \<and> qs ! i = y}). ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
have "\<dots> = sum (%t. sum (%i. ALG x qs i (?config i, ())) {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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>t\<in>{y. y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = t. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>t\<in>{y. y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = t. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>t\<in>{y. y \<in> set init}. \<Sum>i | i < length qs \<and> qs ! i = t. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (2 subgoals):
 1. set init = set init
 2. \<And>x. x \<in> set init \<Longrightarrow> (\<Sum>i<length qs. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
have "\<dots> = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y.
                       ALG x qs i (?config i, ()))"
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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

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

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

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>set init. \<Sum>i<length qs. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>e\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 x qs i (?config i, ())))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
by (rule sum.cartesian_product)
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>set init. \<Sum>y\<in>set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>(x, y)\<in>set init \<times> set init. \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 x qs i (?config i, ())))"
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 x qs i (?config i, ())))" (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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
proof goal_cases
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = 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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = 0
[PROOF STEP]
by (auto simp add: split_def before_in_def)
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = 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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + 0
[PROOF STEP]
show ?case
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + 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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 x qs i (?config i, ()))
           + (\<Sum>i\<in>{i. i<length qs \<and> qs!i=x}. ALG y qs i (?config i, ())) )"
            (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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) \<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) \<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) \<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) \<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) \<circ> (\<lambda>(x, y). (y, x))) x = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
sum ((\<lambda>(x, y). \<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) \<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 y qs i (?config i, ()) + ALG x qs i (?config i, ())))"
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
let ?f="%i. ALG b qs i (?config i, ()) +
               ALG a qs i (?config i, ())"
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
let ?B="{i. i < length qs \<and> qs ! i = b}"
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
let ?A="{i. i < length qs \<and> qs ! i = a}"
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
have "(\<Sum>i\<in>?B \<union> ?A. ?f i)
               = (\<Sum>i\<in>?B. ?f i) + (\<Sum>i\<in>?A. ?f i) - (\<Sum>i\<in>?B \<inter> ?A. ?f i) "
[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 b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
apply(rule sum_Un_nat)
[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 b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>?B. ALG b qs i (?config i, ()) + ALG a qs i (?config i, ()))
                    + (\<Sum>i\<in>?A. ALG b qs i (?config i, ()) + ALG a qs i (?config i, ()))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) - (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<inter> {i. i < length qs \<and> qs ! i = a}. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>?B. ALG a qs i (?config i, ()))
                  + (\<Sum>i\<in>?A. ALG b qs i (?config i, ()))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[PROOF STEP]
by (auto simp: split_def before_in_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length qs \<and> qs ! i = b. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. (case x of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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 b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>i | i < length qs \<and> qs ! i = b. ALG a qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = a. ALG b qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. (case (a, b) of (x, y) \<Rightarrow> (\<Sum>i | i < length qs \<and> qs ! i = y. ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case (a, b) of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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}. (if b < qs ! i in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) + (if a < qs ! i in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0)) = (\<Sum>i | i < length qs \<and> qs ! i = b. if a < b in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) + (\<Sum>i | i < length qs \<and> qs ! i = a. if b < a in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) \<Longrightarrow> (\<Sum>i | i < length qs \<and> qs ! i = b. if a < b in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) + (\<Sum>i | i < length qs \<and> qs ! i = a. if b < a in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) = (\<Sum>i | i < length qs \<and> (qs ! i = b \<or> qs ! i = a). (if b < qs ! i in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) + (if a < qs ! i in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0))
[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}. (if b < qs ! i in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) + (if a < qs ! i in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0)) = (\<Sum>i | i < length qs \<and> qs ! i = b. if a < b in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) + (\<Sum>i | i < length qs \<and> qs ! i = a. if b < a in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) \<Longrightarrow> (\<Sum>i | i < length qs \<and> qs ! i = b. if a < b in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) + (\<Sum>i | i < length qs \<and> qs ! i = a. if b < a in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) = (\<Sum>i\<in>{i. i < length qs \<and> qs ! i = b} \<union> {i. i < length qs \<and> qs ! i = a}. (if b < qs ! i in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0) + (if a < qs ! i in swaps (snd (Strat ! i)) (steps' init qs Strat i) then 1 else 0))
[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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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 x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i | i < length qs \<and> qs ! i = x. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))) = (\<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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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_det Strat 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 y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x 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> (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (case x of (x, y) \<Rightarrow> ALGxy_det Strat qs init x y)
[PROOF STEP]
unfolding ALGxy_det_alternativ
[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 \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG'_det Strat qs init i y + ALG'_det Strat qs init i x)
[PROOF STEP]
unfolding ALG'_det_def
[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 \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (case x of (x, y) \<Rightarrow> \<Sum>i | i < length qs \<and> qs ! i \<in> {y, x}. ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()))
[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}. \<Sum>i | i < length qs \<and> (qs ! i = y \<or> qs ! i = x). ALG y qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ()) + ALG x qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y)
[PROOF STEP]
have blockingpart: "(\<Sum>i<length qs.
                         \<Sum>e\<in>set init.
                              ALG e qs i (?config i, ()))
                 = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}.
                         ALGxy_det Strat qs init x y) "
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y)

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

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
from Tp_darstellung[OF qsStrat]
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p ?init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' ?init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
have E0: "T\<^sub>p init qs Strat =
        (\<Sum>i\<in>{..<length qs}. t\<^sub>p (steps' init qs Strat i) (qs!i) (Strat!i))"
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p ?init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' ?init qs Strat i) (qs ! i) (Strat ! i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{..<length qs}.
                (\<Sum>e\<in>set (steps' init qs Strat i). ALG e qs i (swaps (snd (Strat!i)) (steps' init qs Strat i),()))
+ (\<Sum>(x,y)\<in>{(x,(y::('a::linorder))). x \<in> set (steps' init qs Strat i) \<and> y\<in>set (steps' init qs Strat i) \<and> x<y}. ALG_P (snd (Strat!i)) x y (steps' init qs Strat i)) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)) = (\<Sum>i<length qs. (\<Sum>e\<in>set (steps' init qs Strat i). ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set (steps' init qs Strat i) \<and> y \<in> set (steps' init qs Strat i) \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)))
[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> t\<^sub>p (steps' init qs Strat x) (qs ! x) (Strat ! x) = (\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> t\<^sub>p (steps' init qs Strat x) (qs ! x) (Strat ! x) = (\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))
[PROOF STEP]
apply (rule t\<^sub>p_sumofALGALGP)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> distinct (steps' init qs Strat x)
 2. \<And>x. x \<in> {..<length qs} \<Longrightarrow> qs ! x \<in> set (steps' init qs Strat x)
 3. \<And>x. x \<in> {..<length qs} \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length (steps' init qs Strat x)
[PROOF STEP]
apply(rule steps'_distinct2)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> length qs = length Strat
 2. \<And>x. x \<in> {..<length qs} \<Longrightarrow> x \<le> length Strat
 3. \<And>x. x \<in> {..<length qs} \<Longrightarrow> distinct init
 4. \<And>x. x \<in> {..<length qs} \<Longrightarrow> qs ! x \<in> set (steps' init qs Strat x)
 5. \<And>x. x \<in> {..<length qs} \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length (steps' init qs Strat x)
[PROOF STEP]
using dist qsStrat
[PROOF STATE]
proof (prove)
using this:
distinct init
length qs = length Strat

goal (5 subgoals):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> length qs = length Strat
 2. \<And>x. x \<in> {..<length qs} \<Longrightarrow> x \<le> length Strat
 3. \<And>x. x \<in> {..<length qs} \<Longrightarrow> distinct init
 4. \<And>x. x \<in> {..<length qs} \<Longrightarrow> qs ! x \<in> set (steps' init qs Strat x)
 5. \<And>x. x \<in> {..<length qs} \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length (steps' init qs Strat x)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> qs ! x \<in> set (steps' init qs Strat x)
 2. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length (steps' init qs Strat x)
[PROOF STEP]
apply(subst steps'_set)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> length qs = length Strat
 2. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> x \<le> length Strat
 3. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> qs ! x \<in> set init
 4. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length (steps' init qs Strat x)
[PROOF STEP]
using dist qsStrat inlist
[PROOF STATE]
proof (prove)
using this:
distinct init
length qs = length Strat
set qs \<subseteq> set init

goal (4 subgoals):
 1. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> length qs = length Strat
 2. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> x \<le> length Strat
 3. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> qs ! x \<in> set init
 4. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat\<rbrakk> \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length (steps' init qs Strat x)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat; set qs \<subseteq> set init\<rbrakk> \<Longrightarrow> qs ! x \<in> set init
 2. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat; set qs \<subseteq> set init\<rbrakk> \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length (steps' init qs Strat x)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat; set qs \<subseteq> set init\<rbrakk> \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length (steps' init qs Strat x)
[PROOF STEP]
apply(subst steps'_length)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x l. \<lbrakk>x < length Strat; distinct init; length qs = length Strat; set qs \<subseteq> set init\<rbrakk> \<Longrightarrow> length qs = length Strat
 2. \<And>x l. \<lbrakk>x < length Strat; distinct init; length qs = length Strat; set qs \<subseteq> set init\<rbrakk> \<Longrightarrow> x \<le> length Strat
 3. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat; set qs \<subseteq> set init\<rbrakk> \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length init
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat; set qs \<subseteq> set init\<rbrakk> \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length init
[PROOF STEP]
using noStupid
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x < length Strat; ?l < length (snd (Strat ! ?x))\<rbrakk> \<Longrightarrow> Suc (snd (Strat ! ?x) ! ?l) < length init

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < length Strat; distinct init; length qs = length Strat; set qs \<subseteq> set init\<rbrakk> \<Longrightarrow> \<forall>l<length (snd (Strat ! x)). Suc (snd (Strat ! x) ! l) < length init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)) = (\<Sum>i<length qs. (\<Sum>e\<in>set (steps' init qs Strat i). ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set (steps' init qs Strat i) \<and> y \<in> set (steps' init qs Strat i) \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)) = (\<Sum>i<length qs. (\<Sum>e\<in>set (steps' init qs Strat i). ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set (steps' init qs Strat i) \<and> y \<in> set (steps' init qs Strat i) \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{..<length qs}.
                (\<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat!i)) (steps' init qs Strat i),()))
+ (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P (snd (Strat!i)) x y (steps' init qs Strat i)) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. (\<Sum>e\<in>set (steps' init qs Strat i). ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set (steps' init qs Strat i) \<and> y \<in> set (steps' init qs Strat i) \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))) = (\<Sum>i<length qs. (\<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)))
[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> (\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x)) = (\<Sum>e\<in>set init. ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> (\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x)) = (\<Sum>e\<in>set init. ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> (\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x)) = (\<Sum>e\<in>set init. ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
x \<in> {..<length qs}

goal (1 subgoal):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> (\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x)) = (\<Sum>e\<in>set init. ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {..<length qs}
[PROOF STEP]
have "set (steps' init qs Strat x) = set init"
[PROOF STATE]
proof (prove)
using this:
x \<in> {..<length qs}

goal (1 subgoal):
 1. set (steps' init qs Strat x) = set init
[PROOF STEP]
apply(subst steps'_set)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. x \<in> {..<length qs} \<Longrightarrow> length qs = length Strat
 2. x \<in> {..<length qs} \<Longrightarrow> x \<le> length Strat
 3. x \<in> {..<length qs} \<Longrightarrow> set init = set init
[PROOF STEP]
using dist qsStrat 1
[PROOF STATE]
proof (prove)
using this:
distinct init
length qs = length Strat
x \<in> {..<length qs}

goal (3 subgoals):
 1. x \<in> {..<length qs} \<Longrightarrow> length qs = length Strat
 2. x \<in> {..<length qs} \<Longrightarrow> x \<le> length Strat
 3. x \<in> {..<length qs} \<Longrightarrow> set init = set init
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
set (steps' init qs Strat x) = set init

goal (1 subgoal):
 1. \<And>x. x \<in> {..<length qs} \<Longrightarrow> (\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x)) = (\<Sum>e\<in>set init. ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (steps' init qs Strat x) = set init
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (steps' init qs Strat x) = set init

goal (1 subgoal):
 1. (\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x)) = (\<Sum>e\<in>set init. ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>set (steps' init qs Strat x). ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(xa, y). xa \<in> set (steps' init qs Strat x) \<and> y \<in> set (steps' init qs Strat x) \<and> xa < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x)) = (\<Sum>e\<in>set init. ALG e qs x (swaps (snd (Strat ! x)) (steps' init qs Strat x), ())) + (\<Sum>(xa, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! x)) xa y (steps' init qs Strat x))

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

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. (\<Sum>e\<in>set (steps' init qs Strat i). ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set (steps' init qs Strat i) \<and> y \<in> set (steps' init qs Strat i) \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))) = (\<Sum>i<length qs. (\<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>{..<length qs}.
                (\<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat!i)) (steps' init qs Strat i), ())))
               + (\<Sum>i\<in>{..<length qs}.
               (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P (snd (Strat!i)) x y (steps' init qs Strat i)) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. (\<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))) = (\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))
[PROOF STEP]
by (simp add: sum.distrib split_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. (\<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))) = (\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. (\<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))) = (\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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}.
                         ALGxy_det Strat qs init x y)
               + (\<Sum>i\<in>{..<length qs}.
               (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P (snd (Strat!i)) x y (steps' init qs Strat i)) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))
[PROOF STEP]
by(simp only: blockingpart)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length qs. \<Sum>e\<in>set init. ALG e qs i (swaps (snd (Strat ! i)) (steps' init qs Strat i), ())) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i))

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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}.
                         ALGxy_det Strat qs init x y)
               + (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}.
                ALG_Pxy Strat 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}. ALGxy_det Strat qs init x y) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y)
[PROOF STEP]
by(simp only: paid_part)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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}. ALGxy_det Strat qs init x y) + (\<Sum>i<length qs. \<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (snd (Strat ! i)) x y (steps' init qs Strat i)) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat 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}.
                         ALGxy_det Strat qs init x y
               +   ALG_Pxy Strat 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}. ALGxy_det Strat qs init x y) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
by (simp add: sum.distrib split_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_Pxy Strat qs init x y) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)

goal (1 subgoal):
 1. T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T\<^sub>p init qs Strat = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y)

goal:
No subgoals!
[PROOF STEP]
qed