[STATEMENT]
lemma umf_pair: assumes
   0: "pairwise A"
  assumes 1: "\<And>is s q. \<forall>((free,paid),_) \<in> (snd A (s, is) q). paid=[]"
  assumes 2: "set qs \<subseteq> set init"
  assumes 3: "distinct init"
  assumes 4: "\<And>x. x<length qs \<Longrightarrow> finite (set_pmf (config'' A qs init x))"
   shows "T\<^sub>p_on_rand A init qs
      = (\<Sum>(x,y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand A (Lxy init {x,y}) (Lxy qs {x,y}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[PROOF STEP]
have " T\<^sub>p_on_rand A init qs = (\<Sum>(x,y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)
[PROOF STEP]
by(simp only: umformung[OF 1 2 3 4])
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALGxy A qs init x y)

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

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand A (Lxy init {x,y}) (Lxy qs {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 A qs init x y) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {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> ALGxy A qs init x y) = (case x of (x, y) \<Rightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[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> ALGxy A qs init x y) = (case x of (x, y) \<Rightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[PROOF STEP]
using 0[unfolded pairwise_def] 2 3
[PROOF STATE]
proof (prove)
using this:
\<forall>init. distinct init \<longrightarrow> (\<forall>qs\<in>{xs. set xs \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) = ALGxy A qs init x y)
set qs \<subseteq> set init
distinct init

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> ALGxy A qs init x y) = (case x of (x, y) \<Rightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[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}. ALGxy A qs init x y) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ALG_P_erwischt_alle:
  assumes dinit: "distinct init"
  shows
  "\<forall>l< length sws. Suc (sws!l) < length init \<Longrightarrow> length sws
        = (\<Sum>(x,y)\<in>{(x,y). x \<in> set (init::('a::linorder) list) \<and> y\<in>set init \<and> x<y}. ALG_P sws x y init)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init)
[PROOF STEP]
proof (induct sws)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
case (Cons s ss)
[PROOF STATE]
proof (state)
this:
\<forall>l<length ss. Suc (ss ! l) < length init \<Longrightarrow> length ss = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P ss x y init)
\<forall>l<length (s # ss). Suc ((s # ss) ! l) < length init

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l<length ss. Suc (ss ! l) < length init \<Longrightarrow> length ss = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P ss x y init)
\<forall>l<length (s # ss). Suc ((s # ss) ! l) < length init
[PROOF STEP]
have isininit: "Suc s < length init"
[PROOF STATE]
proof (prove)
using this:
\<forall>l<length ss. Suc (ss ! l) < length init \<Longrightarrow> length ss = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P ss x y init)
\<forall>l<length (s # ss). Suc ((s # ss) ! l) < length init

goal (1 subgoal):
 1. Suc s < length init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc s < length init

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
\<forall>l<length ss. Suc (ss ! l) < length init \<Longrightarrow> length ss = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P ss x y init)
\<forall>l<length (s # ss). Suc ((s # ss) ! l) < length init
[PROOF STEP]
have "\<forall>l<length ss. Suc (ss ! l)  < length init"
[PROOF STATE]
proof (prove)
using this:
\<forall>l<length ss. Suc (ss ! l) < length init \<Longrightarrow> length ss = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P ss x y init)
\<forall>l<length (s # ss). Suc ((s # ss) ! l) < length init

goal (1 subgoal):
 1. \<forall>l<length ss. Suc (ss ! l) < length init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l<length ss. Suc (ss ! l) < length init

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
note iH=Cons(1)[OF this]
[PROOF STATE]
proof (state)
this:
length ss = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P ss x y init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
let ?expr = "(\<lambda>x y. (if Suc s < length (swaps ss init)
                          then (if ((swaps ss init)!s=x \<and> (swaps ss init)!(Suc s)=y) \<or> ((swaps ss init)!s=y \<and> (swaps ss init)!(Suc s)=x)
                                then 1::nat
                                else 0)
                          else 0))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
let ?expr2 = "(\<lambda>x y. (if ((swaps ss init)!s=x \<and> (swaps ss init)!(Suc s)=y) \<or> ((swaps ss init)!s=y \<and> (swaps ss init)!(Suc s)=x)
                                then 1
                                else 0))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
let ?expr3 = "(%x y.  ((swaps ss init)!s=x \<and> (swaps ss init)!(Suc s)=y)
                    \<or> ((swaps ss init)!s=y \<and> (swaps ss init)!(Suc s)=x))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
let ?co' = "swaps ss init"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
from dinit
[PROOF STATE]
proof (chain)
picking this:
distinct init
[PROOF STEP]
have dco: "distinct ?co'"
[PROOF STATE]
proof (prove)
using this:
distinct init

goal (1 subgoal):
 1. distinct (swaps ss init)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (swaps ss init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
let ?expr4 = "(\<lambda>z. (if z\<in>{(x,y). ?expr3 x y}
                                then 1
                                else 0))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have scoinit: "set ?co' = set init"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (swaps ss init) = set init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (swaps ss init) = set init

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
from isininit
[PROOF STATE]
proof (chain)
picking this:
Suc s < length init
[PROOF STEP]
have isT: "Suc s < length ?co'"
[PROOF STATE]
proof (prove)
using this:
Suc s < length init

goal (1 subgoal):
 1. Suc s < length (swaps ss init)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc s < length (swaps ss init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc s < length (swaps ss init)
[PROOF STEP]
have isT2: "Suc s < length init"
[PROOF STATE]
proof (prove)
using this:
Suc s < length (swaps ss init)

goal (1 subgoal):
 1. Suc s < length init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc s < length init

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc s < length init
[PROOF STEP]
have isT3: "s < length init"
[PROOF STATE]
proof (prove)
using this:
Suc s < length init

goal (1 subgoal):
 1. s < length init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s < length init

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s < length init
[PROOF STEP]
have isT6: "s < length ?co'"
[PROOF STATE]
proof (prove)
using this:
s < length init

goal (1 subgoal):
 1. s < length (swaps ss init)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s < length (swaps ss init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
from isT2
[PROOF STATE]
proof (chain)
picking this:
Suc s < length init
[PROOF STEP]
have isT7: "Suc s < length ?co'"
[PROOF STATE]
proof (prove)
using this:
Suc s < length init

goal (1 subgoal):
 1. Suc s < length (swaps ss init)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc s < length (swaps ss init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
from isT6
[PROOF STATE]
proof (chain)
picking this:
s < length (swaps ss init)
[PROOF STEP]
have a: "?co'!s \<in> set ?co'"
[PROOF STATE]
proof (prove)
using this:
s < length (swaps ss init)

goal (1 subgoal):
 1. swaps ss init ! s \<in> set (swaps ss init)
[PROOF STEP]
by (rule nth_mem)
[PROOF STATE]
proof (state)
this:
swaps ss init ! s \<in> set (swaps ss init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
swaps ss init ! s \<in> set (swaps ss init)
[PROOF STEP]
have a: "?co'!s \<in> set init"
[PROOF STATE]
proof (prove)
using this:
swaps ss init ! s \<in> set (swaps ss init)

goal (1 subgoal):
 1. swaps ss init ! s \<in> set init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaps ss init ! s \<in> set init

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
from isT7
[PROOF STATE]
proof (chain)
picking this:
Suc s < length (swaps ss init)
[PROOF STEP]
have "?co'! (Suc s) \<in> set ?co'"
[PROOF STATE]
proof (prove)
using this:
Suc s < length (swaps ss init)

goal (1 subgoal):
 1. swaps ss init ! Suc s \<in> set (swaps ss init)
[PROOF STEP]
by (rule nth_mem)
[PROOF STATE]
proof (state)
this:
swaps ss init ! Suc s \<in> set (swaps ss init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
swaps ss init ! Suc s \<in> set (swaps ss init)
[PROOF STEP]
have b: "?co'!(Suc s) \<in> set init"
[PROOF STATE]
proof (prove)
using this:
swaps ss init ! Suc s \<in> set (swaps ss init)

goal (1 subgoal):
 1. swaps ss init ! Suc s \<in> set init
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaps ss init ! Suc s \<in> set init

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have  "{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}
                          \<inter> {(x,y). ?expr3 x y}
     = {(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y
                              \<and>  (?co'!s=x \<and> ?co'!(Suc s)=y
                                  \<or> ?co'!s=y \<and> ?co'!(Suc s)=x)}"
[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). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> (swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = 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). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> (swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x)}

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> (swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x)}

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have "\<dots> = {(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y
                              \<and>  ?co'!s=x \<and> ?co'!(Suc s)=y }
                           \<union>
                  {(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y
                              \<and>   ?co'!s=y \<and> ?co'!(Suc s)=x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> (swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x)} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> (swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x)} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> (swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x)} = {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have "\<dots> = {(x,y). x<y \<and> ?co'!s=x \<and> ?co'!(Suc s)=y}
                           \<union>
                  {(x,y). x<y \<and> ?co'!s=y \<and> ?co'!(Suc s)=x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
swaps ss init ! s \<in> set init
swaps ss init ! Suc s \<in> set init

goal (1 subgoal):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}
[PROOF STEP]
have c1: "{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y} \<inter> {(x,y). ?expr3 x y}
      = {(x,y). x<y \<and> ?co'!s=x \<and> ?co'!(Suc s)=y}
                           \<union>
                  {(x,y). x<y \<and> ?co'!s=y \<and> ?co'!(Suc s)=x}"
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}

goal (1 subgoal):
 1. {(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have c2: "card ({(x,y). x<y \<and> ?co'!s=x \<and> ?co'!(Suc s)=y}
                           \<union>
                  {(x,y). x<y \<and> ?co'!s=y \<and> ?co'!(Suc s)=x}) = 1" (is "card (?A \<union> ?B) = 1")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
proof (cases "?co'!s<?co'!(Suc s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
 2. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
swaps ss init ! s < swaps ss init ! Suc s

goal (2 subgoals):
 1. swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
 2. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
swaps ss init ! s < swaps ss init ! Suc s
[PROOF STEP]
have a: "?A = { (?co'!s, ?co'!(Suc s)) }"
          and b: "?B = {} "
[PROOF STATE]
proof (prove)
using this:
swaps ss init ! s < swaps ss init ! Suc s

goal (1 subgoal):
 1. {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} = {(swaps ss init ! s, swaps ss init ! Suc s)} &&& {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} = {(swaps ss init ! s, swaps ss init ! Suc s)}
{(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {}

goal (2 subgoals):
 1. swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
 2. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
have c: "?A \<union> ?B = { (?co'!s, ?co'!(Suc s)) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! s, swaps ss init ! Suc s)}
[PROOF STEP]
apply(simp only: a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(swaps ss init ! s, swaps ss init ! Suc s)} \<union> {} = {(swaps ss init ! s, swaps ss init ! Suc s)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! s, swaps ss init ! Suc s)}

goal (2 subgoals):
 1. swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
 2. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
have "card (?A \<union> ?B) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
unfolding c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {(swaps ss init ! s, swaps ss init ! Suc s)} = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal (2 subgoals):
 1. swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
 2. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal (1 subgoal):
 1. card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal (1 subgoal):
 1. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> swaps ss init ! s < swaps ss init ! Suc s

goal (1 subgoal):
 1. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> swaps ss init ! s < swaps ss init ! Suc s
[PROOF STEP]
have a: "?A = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> swaps ss init ! s < swaps ss init ! Suc s

goal (1 subgoal):
 1. {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} = {}

goal (1 subgoal):
 1. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
have b: "?B = { (?co'!(Suc s), ?co'!s) } "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! Suc s, swaps ss init ! s)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! Suc s, swaps ss init ! s)}
[PROOF STEP]
from dco distinct_conv_nth[of "?co'"]
[PROOF STATE]
proof (chain)
picking this:
distinct (swaps ss init)
distinct (swaps ss init) = (\<forall>i<length (swaps ss init). \<forall>j<length (swaps ss init). i \<noteq> j \<longrightarrow> swaps ss init ! i \<noteq> swaps ss init ! j)
[PROOF STEP]
have "swaps ss init ! s \<noteq> swaps ss init ! (Suc s)"
[PROOF STATE]
proof (prove)
using this:
distinct (swaps ss init)
distinct (swaps ss init) = (\<forall>i<length (swaps ss init). \<forall>j<length (swaps ss init). i \<noteq> j \<longrightarrow> swaps ss init ! i \<noteq> swaps ss init ! j)

goal (1 subgoal):
 1. swaps ss init ! s \<noteq> swaps ss init ! Suc s
[PROOF STEP]
using isT2 isT3
[PROOF STATE]
proof (prove)
using this:
distinct (swaps ss init)
distinct (swaps ss init) = (\<forall>i<length (swaps ss init). \<forall>j<length (swaps ss init). i \<noteq> j \<longrightarrow> swaps ss init ! i \<noteq> swaps ss init ! j)
Suc s < length init
s < length init

goal (1 subgoal):
 1. swaps ss init ! s \<noteq> swaps ss init ! Suc s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
swaps ss init ! s \<noteq> swaps ss init ! Suc s

goal (1 subgoal):
 1. {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! Suc s, swaps ss init ! s)}
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> swaps ss init ! s < swaps ss init ! Suc s
swaps ss init ! s \<noteq> swaps ss init ! Suc s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> swaps ss init ! s < swaps ss init ! Suc s
swaps ss init ! s \<noteq> swaps ss init ! Suc s

goal (1 subgoal):
 1. {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! Suc s, swaps ss init ! s)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! Suc s, swaps ss init ! s)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! Suc s, swaps ss init ! s)}

goal (1 subgoal):
 1. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
have c: "?A \<union> ?B = { (?co'!(Suc s), ?co'!s) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! Suc s, swaps ss init ! s)}
[PROOF STEP]
apply(simp only: a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<union> {(swaps ss init ! Suc s, swaps ss init ! s)} = {(swaps ss init ! Suc s, swaps ss init ! s)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} = {(swaps ss init ! Suc s, swaps ss init ! s)}

goal (1 subgoal):
 1. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
have "card (?A \<union> ?B) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
unfolding c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {(swaps ss init ! Suc s, swaps ss init ! s)} = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal (1 subgoal):
 1. \<not> swaps ss init ! s < swaps ss init ! Suc s \<Longrightarrow> card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal (1 subgoal):
 1. card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have yeah: "(\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ?expr x y) = (1::nat)"
[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}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[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 < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
have "(\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ?expr x y)
        = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ?expr2 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}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0)
[PROOF STEP]
using isT
[PROOF STATE]
proof (prove)
using this:
Suc s < length (swaps ss init)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0)
[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}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[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}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>z\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ?expr2 (fst z) (snd z))"
[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}. if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if swaps ss init ! s = fst z \<and> swaps ss init ! Suc s = snd z \<or> swaps ss init ! s = snd z \<and> swaps ss init ! Suc s = fst z then 1 else 0)
[PROOF STEP]
by(simp add: 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}. if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if swaps ss init ! s = fst z \<and> swaps ss init ! Suc s = snd z \<or> swaps ss init ! s = snd z \<and> swaps ss init ! Suc s = fst z then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[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}. if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if swaps ss init ! s = fst z \<and> swaps ss init ! Suc s = snd z \<or> swaps ss init ! s = snd z \<and> swaps ss init ! Suc s = fst z then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>z\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ?expr4 z)"
[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}. if swaps ss init ! s = fst z \<and> swaps ss init ! Suc s = snd z \<or> swaps ss init ! s = snd z \<and> swaps ss init ! Suc s = fst z then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if z \<in> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} then 1 else 0)
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if swaps ss init ! s = fst z \<and> swaps ss init ! Suc s = snd z \<or> swaps ss init ! s = snd z \<and> swaps ss init ! Suc s = fst z then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if z \<in> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[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}. if swaps ss init ! s = fst z \<and> swaps ss init ! Suc s = snd z \<or> swaps ss init ! s = snd z \<and> swaps ss init ! Suc s = fst z then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if z \<in> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>z\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}
                          \<inter>{(x,y). ?expr3 x y} . 1)"
[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}. if z \<in> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}. 1)
[PROOF STEP]
apply(rule sum.inter_restrict[symmetric])
[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>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if z \<in> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}. 1)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[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}. if z \<in> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x} then 1 else 0) = (\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}. 1)

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
have "\<dots> = card ({(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}
                          \<inter> {(x,y). ?expr3 x y})"
[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} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}. 1) = card ({(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>z\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}. 1) = card ({(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x})

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[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} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}. 1) = card ({(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x})

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
have "\<dots> = card ({(x,y). x<y \<and> ?co'!s=x \<and> ?co'!(Suc s)=y}
                           \<union>
                  {(x,y). x<y \<and> ?co'!s=y \<and> ?co'!(Suc s)=x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x})
[PROOF STEP]
by(simp only: c1)
[PROOF STATE]
proof (state)
this:
card ({(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x})

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y} \<inter> {(x, y). swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x})

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
have "\<dots> = (1::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
using c2
[PROOF STATE]
proof (prove)
using this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal (1 subgoal):
 1. card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({(x, y). x < y \<and> swaps ss init ! s = x \<and> swaps ss init ! Suc s = y} \<union> {(x, y). x < y \<and> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x}) = 1

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[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 < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[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 < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1

goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1

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}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) = 1

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have "length (s # ss) = 1 + length ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (s # ss) = 1 + length ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (s # ss) = 1 + length ss

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (s # ss) = 1 + length ss

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have "\<dots> = 1 + (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P ss x y init)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + length ss = 1 + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init)
[PROOF STEP]
using iH
[PROOF STATE]
proof (prove)
using this:
length ss = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P ss x y init)

goal (1 subgoal):
 1. 1 + length ss = 1 + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 + length ss = 1 + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + length ss = 1 + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ?expr x y)
            + (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P ss x y init)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init)
[PROOF STEP]
by(simp only: yeah)
[PROOF STATE]
proof (state)
this:
1 + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ?expr x y + ALG_P ss x y init)"
    (is "?A + ?B = ?C")
[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}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + ALG_P ss x y init)
[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}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + ALG_P ss x y init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[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}. if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P ss x y init) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. (if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + ALG_P ss x y init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
have "\<dots> = (\<Sum>(x,y)\<in>{(x,y). x \<in> set init \<and> y\<in>set init \<and> x<y}. ALG_P (s#ss) x y init)"
[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}. (if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + ALG_P ss x y init) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (s # ss) x y 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}. (if Suc s < length (swaps ss init) then if swaps ss init ! s = x \<and> swaps ss init ! Suc s = y \<or> swaps ss init ! s = y \<and> swaps ss init ! Suc s = x then 1 else 0 else 0) + ALG_P ss x y init) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (s # ss) x y init)

goal (2 subgoals):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
 2. \<And>a sws. \<lbrakk>\<forall>l<length sws. Suc (sws ! l) < length init \<Longrightarrow> length sws = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P sws x y init); \<forall>l<length (a # sws). Suc ((a # sws) ! l) < length init\<rbrakk> \<Longrightarrow> length (a # sws) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (a # sws) x y init)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (s # ss) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (s # ss) x y init)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length (s # ss) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P (s # ss) x y init)

goal (1 subgoal):
 1. length (s # ss) = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P (s # ss) x y init)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length (s # ss) = (\<Sum> | case  of (x, y) \<Rightarrow> x \<in> set init \<and> y \<in> set init \<and> x < y. case  of (x, y) \<Rightarrow> ALG_P (s # ss) x y init)

goal (1 subgoal):
 1. \<forall>l<length []. Suc ([] ! l) < length init \<Longrightarrow> length [] = (\<Sum>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. ALG_P [] x y init)
[PROOF STEP]
qed (simp)


[STATEMENT]
lemma t\<^sub>p_sumofALGALGP:
assumes "distinct s" "(qs!i)\<in>set s"
  and "\<forall>l< length (snd a). Suc ((snd a)!l) < length s"
shows "t\<^sub>p s (qs!i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s,()))
      + (\<Sum>(x,y)\<in>{(x::('a::linorder),y). x \<in> set s \<and> y\<in>set s \<and> x<y}. ALG_P (snd a) x y s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sub>p s (qs ! i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t\<^sub>p s (qs ! i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
(* paid exchanges *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t\<^sub>p s (qs ! i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
have pe: "length (snd a)
        = (\<Sum>(x,y)\<in>{(x,y). x \<in> set s \<and> y\<in>set s \<and> x<y}. ALG_P (snd a) x y s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (snd a) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
apply(rule ALG_P_erwischt_alle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct s
 2. \<forall>l<length (snd a). Suc (snd a ! l) < length s
[PROOF STEP]
by(fact)+
[PROOF STATE]
proof (state)
this:
length (snd a) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)

goal (1 subgoal):
 1. t\<^sub>p s (qs ! i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
(* access cost *)
[PROOF STATE]
proof (state)
this:
length (snd a) = (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)

goal (1 subgoal):
 1. t\<^sub>p s (qs ! i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
have ac: "index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s,()))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))
[PROOF STEP]
have "index (swaps (snd a) s) (qs ! i)
        = (\<Sum>e\<in>set (swaps (snd a) s). if e < (qs ! i) in (swaps (snd a) s) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set (swaps (snd a) s). if e < qs ! i in swaps (snd a) s then 1 else 0)
[PROOF STEP]
apply(rule index_sum)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct (swaps (snd a) s)
 2. qs ! i \<in> set (swaps (snd a) s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct s
qs ! i \<in> set s
\<forall>l<length (snd a). Suc (snd a ! l) < length s

goal (2 subgoals):
 1. distinct (swaps (snd a) s)
 2. qs ! i \<in> set (swaps (snd a) s)
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set (swaps (snd a) s). if e < qs ! i in swaps (snd a) s then 1 else 0)

goal (1 subgoal):
 1. index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set (swaps (snd a) s). if e < qs ! i in swaps (snd a) s then 1 else 0)

goal (1 subgoal):
 1. index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s,()))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>set (swaps (snd a) s). if e < qs ! i in swaps (snd a) s then 1 else 0) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>set (swaps (snd a) s). if e < qs ! i in swaps (snd a) s then 1 else 0) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))

goal (1 subgoal):
 1. index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))

goal (1 subgoal):
 1. index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
index (swaps (snd a) s) (qs ! i) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ()))

goal (1 subgoal):
 1. t\<^sub>p s (qs ! i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t\<^sub>p s (qs ! i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
unfolding t\<^sub>p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let (mf, sws) = a in index (swaps sws s) (qs ! i) + length sws) = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)
[PROOF STEP]
apply (simp add: split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index (swaps (snd a) s) (qs ! i) + length (snd a) = (\<Sum>e\<in>set s. if e < qs ! i in swaps (snd a) s then 1 else 0) + (\<Sum>x\<in>{p. fst p \<in> set s \<and> snd p \<in> set s \<and> fst p < snd p}. ALG_P (snd a) (fst x) (snd x) s)
[PROOF STEP]
unfolding ac pe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s) = (\<Sum>e\<in>set s. if e < qs ! i in swaps (snd a) s then 1 else 0) + (\<Sum>x\<in>{p. fst p \<in> set s \<and> snd p \<in> set s \<and> fst p < snd p}. ALG_P (snd a) (fst x) (snd x) s)
[PROOF STEP]
by (simp add: split_def)
[PROOF STATE]
proof (state)
this:
t\<^sub>p s (qs ! i) a = (\<Sum>e\<in>set s. ALG e qs i (swaps (snd a) s, ())) + (\<Sum>(x, y)\<in>{(x, y). x \<in> set s \<and> y \<in> set s \<and> x < y}. ALG_P (snd a) x y s)

goal:
No subgoals!
[PROOF STEP]
qed