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

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

goal (1 subgoal):
 1. \<lbrakk>n < length qs; n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' Strat (take n qs @ [qs ! n]) init n x y = ALG_P' (take n Strat @ [Strat ! n]) (take n qs @ [qs ! n]) init n x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < length Strat
[PROOF STEP]
have lS: "length (take n Strat) = n"
[PROOF STATE]
proof (prove)
using this:
n < length Strat

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

goal (1 subgoal):
 1. \<lbrakk>n < length qs; n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' Strat (take n qs @ [qs ! n]) init n x y = ALG_P' (take n Strat @ [Strat ! n]) (take n qs @ [qs ! n]) init n x y
[PROOF STEP]
have "(take n Strat @ [Strat ! n]) ! n =
      (take n Strat @ (Strat ! n) # []) ! length (take n Strat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (take n Strat @ [Strat ! n]) ! n = (take n Strat @ [Strat ! n]) ! length (take n Strat)
[PROOF STEP]
using lS
[PROOF STATE]
proof (prove)
using this:
length (take n Strat) = n

goal (1 subgoal):
 1. (take n Strat @ [Strat ! n]) ! n = (take n Strat @ [Strat ! n]) ! length (take n Strat)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(take n Strat @ [Strat ! n]) ! n = (take n Strat @ [Strat ! n]) ! length (take n Strat)

goal (1 subgoal):
 1. \<lbrakk>n < length qs; n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' Strat (take n qs @ [qs ! n]) init n x y = ALG_P' (take n Strat @ [Strat ! n]) (take n qs @ [qs ! n]) init n x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(take n Strat @ [Strat ! n]) ! n = (take n Strat @ [Strat ! n]) ! length (take n Strat)

goal (1 subgoal):
 1. \<lbrakk>n < length qs; n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' Strat (take n qs @ [qs ! n]) init n x y = ALG_P' (take n Strat @ [Strat ! n]) (take n qs @ [qs ! n]) init n x y
[PROOF STEP]
have "\<dots> = Strat ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (take n Strat @ [Strat ! n]) ! length (take n Strat) = Strat ! n
[PROOF STEP]
by(rule nth_append_length)
[PROOF STATE]
proof (state)
this:
(take n Strat @ [Strat ! n]) ! length (take n Strat) = Strat ! n

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

goal (1 subgoal):
 1. (take n Strat @ [Strat ! n]) ! n = Strat ! n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(take n Strat @ [Strat ! n]) ! n = Strat ! n

goal (1 subgoal):
 1. \<lbrakk>n < length qs; n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' Strat (take n qs @ [qs ! n]) init n x y = ALG_P' (take n Strat @ [Strat ! n]) (take n qs @ [qs ! n]) init n x y
[PROOF STEP]
obtain rest where rest: "Strat = (take n Strat @ [Strat ! n] @ rest)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>rest. Strat = take n Strat @ [Strat ! n] @ rest \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using S
[PROOF STATE]
proof (prove)
using this:
n < length Strat

goal (1 subgoal):
 1. (\<And>rest. Strat = take n Strat @ [Strat ! n] @ rest \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rest. Strat = take n Strat @ Strat ! n # rest \<Longrightarrow> thesis; n < length Strat\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using id_take_nth_drop
[PROOF STATE]
proof (prove)
using this:
?i < length ?xs \<Longrightarrow> ?xs = take ?i ?xs @ ?xs ! ?i # drop (Suc ?i) ?xs

goal (1 subgoal):
 1. \<lbrakk>\<And>rest. Strat = take n Strat @ Strat ! n # rest \<Longrightarrow> thesis; n < length Strat\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Strat = take n Strat @ [Strat ! n] @ rest

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

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

goal (1 subgoal):
 1. \<lbrakk>n < length qs; n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' Strat (take n qs @ [qs ! n]) init n x y = ALG_P' (take n Strat @ [Strat ! n]) (take n qs @ [qs ! n]) init n x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n]) n = steps' init (take n qs) (take n Strat) n

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

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

goal (1 subgoal):
 1. \<lbrakk>n < length qs; n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' Strat (take n qs @ [qs ! n]) init n x y = ALG_P' (take n Strat @ [Strat ! n]) (take n qs @ [qs ! n]) init n x y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n]) n = steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n] @ rest) n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n]) n = steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n] @ rest) n

goal (1 subgoal):
 1. ALG_P' Strat (take n qs @ [qs ! n]) init n x y = ALG_P' (take n Strat @ [Strat ! n]) (take n qs @ [qs ! n]) init n x y
[PROOF STEP]
unfolding ALG_P'_def tt
[PROOF STATE]
proof (prove)
using this:
steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n]) n = steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n] @ rest) n

goal (1 subgoal):
 1. ALG_P (snd (Strat ! n)) x y (steps' init (take n qs @ [qs ! n]) Strat n) = ALG_P (snd (Strat ! n)) x y (steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n]) n)
[PROOF STEP]
using rest
[PROOF STATE]
proof (prove)
using this:
steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n]) n = steps' init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n] @ rest) n
Strat = take n Strat @ [Strat ! n] @ rest

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>n < length qs; n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' Strat qs init n x y = ALG_P' (Strat @ r1) (qs @ r2) init n x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALG_P' Strat qs init n x y = ALG_P' (Strat @ r1) (qs @ r2) init n x y
[PROOF STEP]
unfolding ALG_P'_def tt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALG_P (snd ((Strat @ r1) ! n)) x y (steps' init qs Strat n) = ALG_P (snd ((Strat @ r1) ! n)) x y (steps' init (qs @ r2) (Strat @ r1) n)
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
steps' init qs Strat n = steps' init (qs @ r2) (Strat @ r1) n

goal (1 subgoal):
 1. ALG_P (snd ((Strat @ r1) ! n)) x y (steps' init qs Strat n) = ALG_P (snd ((Strat @ r1) ! n)) x y (steps' init (qs @ r2) (Strat @ r1) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ALG_P' Strat qs init n x y = ALG_P' (Strat @ r1) (qs @ r2) init n x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wegdamit: "length A < length Strat \<Longrightarrow> b \<notin> {x,y} \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y
    = ALGxy_det Strat A init x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
assume bn: "b \<notin> {x,y}"
[PROOF STATE]
proof (state)
this:
b \<notin> {x, y}

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
have "(A @ [b]) ! (length A) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A @ [b]) ! length A = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A @ [b]) ! length A = b

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
assume l: "length A < length Strat"
[PROOF STATE]
proof (state)
this:
length A < length Strat

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
term "%i. ALG'_det Strat (A @ [b]) init i y"
[PROOF STATE]
proof (state)
this:
length A < length Strat

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
have e: "\<And>i. i<length A \<Longrightarrow> (A @ [b]) ! i = A ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length A \<Longrightarrow> (A @ [b]) ! i = A ! i
[PROOF STEP]
by(auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
?i < length A \<Longrightarrow> (A @ [b]) ! ?i = A ! ?i

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
have "(\<Sum>i\<in> {..< length (A @ [b])}.
        if (A @ [b]) ! i \<in> {y, x}
        then ALG'_det Strat (A @ [b]) init i y +
             ALG'_det Strat (A @ [b]) init i x
        else 0) = (\<Sum>i\<in> {..< Suc(length (A))}.
        if (A @ [b]) ! i \<in> {y, x}
        then ALG'_det Strat (A @ [b]) init i y +
             ALG'_det Strat (A @ [b]) init i x
        else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length (A @ [b]). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<Suc (length A). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length (A @ [b]). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<Suc (length A). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0)

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length (A @ [b]). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<Suc (length A). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0)

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in> {..< (length (A))}.
        if (A @ [b]) ! i \<in> {y, x}
        then ALG'_det Strat (A @ [b]) init i y +
             ALG'_det Strat (A @ [b]) init i x
        else 0) + ( if (A @ [b]) ! (length A) \<in> {y, x}
        then ALG'_det Strat (A @ [b]) init (length A) y +
             ALG'_det Strat (A @ [b]) init (length A) x
        else 0) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<Suc (length A). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) + (if (A @ [b]) ! length A \<in> {y, x} then ALG'_det Strat (A @ [b]) init (length A) y + ALG'_det Strat (A @ [b]) init (length A) x else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<Suc (length A). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) + (if (A @ [b]) ! length A \<in> {y, x} then ALG'_det Strat (A @ [b]) init (length A) y + ALG'_det Strat (A @ [b]) init (length A) x else 0)

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
(* abspalten des letzten glieds *)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<Suc (length A). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) + (if (A @ [b]) ! length A \<in> {y, x} then ALG'_det Strat (A @ [b]) init (length A) y + ALG'_det Strat (A @ [b]) init (length A) x else 0)

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<Suc (length A). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) + (if (A @ [b]) ! length A \<in> {y, x} then ALG'_det Strat (A @ [b]) init (length A) y + ALG'_det Strat (A @ [b]) init (length A) x else 0)

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in> {..< (length (A))}.
        if (A @ [b]) ! i \<in> {y, x}
        then ALG'_det Strat (A @ [b]) init i y +
             ALG'_det Strat (A @ [b]) init i x
        else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) + (if (A @ [b]) ! length A \<in> {y, x} then ALG'_det Strat (A @ [b]) init (length A) y + ALG'_det Strat (A @ [b]) init (length A) x else 0) = (\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0)
[PROOF STEP]
using bn
[PROOF STATE]
proof (prove)
using this:
b \<notin> {x, y}

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

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) + (if (A @ [b]) ! length A \<in> {y, x} then ALG'_det Strat (A @ [b]) init (length A) y + ALG'_det Strat (A @ [b]) init (length A) x else 0) = (\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0)

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in> {..< (length (A))}.
          if A ! i \<in> {y, x}
          then ALG'_det Strat A init i y +
              ALG'_det Strat A init i x
              else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if A ! i \<in> {y, x} then ALG'_det Strat A init i y + ALG'_det Strat A init i x else 0)
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {..<length A} = {..<length A}
 2. \<And>xa. xa \<in> {..<length A} \<Longrightarrow> (if (A @ [b]) ! xa \<in> {y, x} then ALG'_det Strat (A @ [b]) init xa y + ALG'_det Strat (A @ [b]) init xa x else 0) = (if A ! xa \<in> {y, x} then ALG'_det Strat A init xa y + ALG'_det Strat A init xa x else 0)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {..<length A} \<Longrightarrow> (if (A @ [b]) ! xa \<in> {y, x} then ALG'_det Strat (A @ [b]) init xa y + ALG'_det Strat (A @ [b]) init xa x else 0) = (if A ! xa \<in> {y, x} then ALG'_det Strat A init xa y + ALG'_det Strat A init xa x else 0)
[PROOF STEP]
using l ALG'_det_append[where qs=A] e
[PROOF STATE]
proof (prove)
using this:
length A < length Strat
\<lbrakk>?n < length ?Strat; ?n < length A\<rbrakk> \<Longrightarrow> ALG'_det ?Strat (A @ ?a) ?init ?n ?x = ALG'_det ?Strat A ?init ?n ?x
?i < length A \<Longrightarrow> (A @ [b]) ! ?i = A ! ?i

goal (1 subgoal):
 1. \<And>xa. xa \<in> {..<length A} \<Longrightarrow> (if (A @ [b]) ! xa \<in> {y, x} then ALG'_det Strat (A @ [b]) init xa y + ALG'_det Strat (A @ [b]) init xa x else 0) = (if A ! xa \<in> {y, x} then ALG'_det Strat A init xa y + ALG'_det Strat A init xa x else 0)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<length A. if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if A ! i \<in> {y, x} then ALG'_det Strat A init i y + ALG'_det Strat A init i x else 0)

goal (1 subgoal):
 1. \<lbrakk>length A < length Strat; b \<notin> {x, y}\<rbrakk> \<Longrightarrow> ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<length (A @ [b]). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if A ! i \<in> {y, x} then ALG'_det Strat A init i y + ALG'_det Strat A init i x else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<length (A @ [b]). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if A ! i \<in> {y, x} then ALG'_det Strat A init i y + ALG'_det Strat A init i x else 0)

goal (1 subgoal):
 1. ALGxy_det Strat (A @ [b]) init x y = ALGxy_det Strat A init x y
[PROOF STEP]
unfolding ALGxy_det_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<length (A @ [b]). if (A @ [b]) ! i \<in> {y, x} then ALG'_det Strat (A @ [b]) init i y + ALG'_det Strat (A @ [b]) init i x else 0) = (\<Sum>i<length A. if A ! i \<in> {y, x} then ALG'_det Strat A init i y + ALG'_det Strat A init i x else 0)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ALG_P_split: "length qs < length Strat \<Longrightarrow> ALG_Pxy Strat (qs@[q]) init x y = ALG_Pxy Strat qs init x y
            +  ALG_P' Strat (qs@[q]) init (length qs) x y "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length qs < length Strat \<Longrightarrow> ALG_Pxy Strat (qs @ [q]) init x y = ALG_Pxy Strat qs init x y + ALG_P' Strat (qs @ [q]) init (length qs) x y
[PROOF STEP]
unfolding ALG_Pxy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length qs < length Strat \<Longrightarrow> (\<Sum>i<length (qs @ [q]). ALG_P' Strat (qs @ [q]) init i x y) = (\<Sum>i<length qs. ALG_P' Strat qs init i x y) + ALG_P' Strat (qs @ [q]) init (length qs) x y
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length qs < length Strat \<Longrightarrow> (\<Sum>i<length qs. ALG_P' Strat (qs @ [q]) init i x y) = (\<Sum>i<length qs. ALG_P' Strat qs init i x y)
[PROOF STEP]
apply(rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length qs < length Strat \<Longrightarrow> {..<length qs} = {..<length qs}
 2. \<And>xa. \<lbrakk>length qs < length Strat; xa \<in> {..<length qs}\<rbrakk> \<Longrightarrow> ALG_P' Strat (qs @ [q]) init xa x y = ALG_P' Strat qs init xa x y
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>length qs < length Strat; xa \<in> {..<length qs}\<rbrakk> \<Longrightarrow> ALG_P' Strat (qs @ [q]) init xa x y = ALG_P' Strat qs init xa x y
[PROOF STEP]
using ALG_P'_rest2[symmetric, of _ qs Strat "[]" "[q]"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n < length qs; ?n < length Strat\<rbrakk> \<Longrightarrow> ALG_P' (Strat @ []) (qs @ [q]) ?init ?n ?x ?y = ALG_P' Strat qs ?init ?n ?x ?y

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>length qs < length Strat; xa \<in> {..<length qs}\<rbrakk> \<Longrightarrow> ALG_P' Strat (qs @ [q]) init xa x y = ALG_P' Strat qs init xa x y
[PROOF STEP]
by(simp)


[STATEMENT]
lemma before_in_swap2:
 "dist_perm xs ys \<Longrightarrow> Suc n < size xs \<Longrightarrow> x\<noteq>y \<Longrightarrow>
  x < y in (swap n xs) \<longleftrightarrow>
  (~ x < y in xs \<and> (y = xs!n \<and> x = xs!Suc n)
      \<or> x < y in xs \<and> ~(y = xs!Suc n \<and> x = xs!n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dist_perm xs ys; Suc n < length xs; x \<noteq> y\<rbrakk> \<Longrightarrow> x < y in swap n xs = (\<not> x < y in xs \<and> y = xs ! n \<and> x = xs ! Suc n \<or> x < y in xs \<and> \<not> (y = xs ! Suc n \<and> x = xs ! n))
[PROOF STEP]
apply(simp add:before_in_def index_swap_distinct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dist_perm xs ys; Suc n < length xs; x \<noteq> y\<rbrakk> \<Longrightarrow> (x = xs ! Suc n \<longrightarrow> (xs ! Suc n = xs ! n \<longrightarrow> y \<noteq> xs ! n \<and> (y \<noteq> xs ! n \<longrightarrow> (Suc n < index xs y \<and> y \<in> set ys) = (index xs (xs ! n) < index xs y \<and> y \<in> set ys))) \<and> (xs ! Suc n \<noteq> xs ! n \<longrightarrow> y \<noteq> xs ! Suc n \<longrightarrow> (y = xs ! n \<longrightarrow> xs ! n \<in> set ys) \<and> (y \<noteq> xs ! n \<longrightarrow> (n < index xs y \<and> y \<in> set ys) = (index xs (xs ! Suc n) < index xs y \<and> y \<in> set ys)))) \<and> (x \<noteq> xs ! Suc n \<longrightarrow> (x = xs ! n \<longrightarrow> (y = xs ! Suc n \<longrightarrow> xs ! Suc n \<noteq> xs ! n) \<and> (y \<noteq> xs ! Suc n \<longrightarrow> (y = xs ! n \<longrightarrow> xs ! n \<noteq> xs ! Suc n) \<and> (y \<noteq> xs ! n \<longrightarrow> (Suc n < index xs y \<and> y \<in> set ys) = (index xs (xs ! n) < index xs y \<and> y \<in> set ys)))) \<and> (x \<noteq> xs ! n \<longrightarrow> (y = xs ! Suc n \<longrightarrow> (xs ! Suc n = xs ! n \<longrightarrow> (index xs x < Suc n \<and> xs ! n \<in> set ys) = (index xs x < index xs (xs ! n) \<and> xs ! n \<in> set ys)) \<and> (xs ! Suc n \<noteq> xs ! n \<longrightarrow> (index xs x < n \<and> xs ! Suc n \<in> set ys) = (index xs x < index xs (xs ! Suc n) \<and> xs ! Suc n \<in> set ys))) \<and> (y \<noteq> xs ! Suc n \<longrightarrow> y = xs ! n \<longrightarrow> (index xs x < Suc n \<and> xs ! n \<in> set ys) = (index xs x < index xs (xs ! n) \<and> xs ! n \<in> set ys))))
[PROOF STEP]
by (metis Suc_lessD Suc_lessI index_nth_id less_Suc_eq nth_mem yes)


[STATEMENT]
lemma projected_paid_same_effect:
  assumes
   d: "dist_perm s1 s1"
  and ee: "x\<noteq>y"
  and f: "set s2 = {x, y}"
  and g: "length s2 = 2"
  and h: "dist_perm s2 s2"
  shows "x < y in s1 = x < y in s2 \<Longrightarrow>
  x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2
[PROOF STEP]
proof (induct acs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps [] s1 = x < y in (swap 0 ^^ ALG_P [] x y s1) s2
 2. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
x < y in s1 = x < y in s2

goal (2 subgoals):
 1. x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps [] s1 = x < y in (swap 0 ^^ ALG_P [] x y s1) s2
 2. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < y in s1 = x < y in s2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x < y in s1 = x < y in s2

goal (1 subgoal):
 1. x < y in swaps [] s1 = x < y in (swap 0 ^^ ALG_P [] x y s1) s2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in swaps [] s1 = x < y in (swap 0 ^^ ALG_P [] x y s1) s2

goal (1 subgoal):
 1. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
case (Cons s ss)
[PROOF STATE]
proof (state)
this:
x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps ss s1 = x < y in (swap 0 ^^ ALG_P ss x y s1) s2
x < y in s1 = x < y in s2

goal (1 subgoal):
 1. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
from d
[PROOF STATE]
proof (chain)
picking this:
dist_perm s1 s1
[PROOF STEP]
have dd: "dist_perm (swaps ss s1) (swaps ss s1)"
[PROOF STATE]
proof (prove)
using this:
dist_perm s1 s1

goal (1 subgoal):
 1. dist_perm (swaps ss s1) (swaps ss s1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist_perm (swaps ss s1) (swaps ss s1)

goal (1 subgoal):
 1. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
set s2 = {x, y}
[PROOF STEP]
have ff: "set ((swap 0 ^^ ALG_P ss x y s1) s2) = {x, y}"
[PROOF STATE]
proof (prove)
using this:
set s2 = {x, y}

goal (1 subgoal):
 1. set ((swap 0 ^^ ALG_P ss x y s1) s2) = {x, y}
[PROOF STEP]
by (metis foldr_replicate swaps_inv)
[PROOF STATE]
proof (state)
this:
set ((swap 0 ^^ ALG_P ss x y s1) s2) = {x, y}

goal (1 subgoal):
 1. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
from g
[PROOF STATE]
proof (chain)
picking this:
length s2 = 2
[PROOF STEP]
have gg: "length ((swap 0 ^^ ALG_P ss x y s1) s2) = 2"
[PROOF STATE]
proof (prove)
using this:
length s2 = 2

goal (1 subgoal):
 1. length ((swap 0 ^^ ALG_P ss x y s1) s2) = 2
[PROOF STEP]
by (metis foldr_replicate swaps_inv)
[PROOF STATE]
proof (state)
this:
length ((swap 0 ^^ ALG_P ss x y s1) s2) = 2

goal (1 subgoal):
 1. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
from h
[PROOF STATE]
proof (chain)
picking this:
dist_perm s2 s2
[PROOF STEP]
have hh: "dist_perm ((swap 0 ^^ ALG_P ss x y s1) s2) ((swap 0 ^^ ALG_P ss x y s1) s2)"
[PROOF STATE]
proof (prove)
using this:
dist_perm s2 s2

goal (1 subgoal):
 1. dist_perm ((swap 0 ^^ ALG_P ss x y s1) s2) ((swap 0 ^^ ALG_P ss x y s1) s2)
[PROOF STEP]
by (metis foldr_replicate swaps_inv)
[PROOF STATE]
proof (state)
this:
dist_perm ((swap 0 ^^ ALG_P ss x y s1) s2) ((swap 0 ^^ ALG_P ss x y s1) s2)

goal (1 subgoal):
 1. \<And>a acs. \<lbrakk>x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps acs s1 = x < y in (swap 0 ^^ ALG_P acs x y s1) s2; x < y in s1 = x < y in s2\<rbrakk> \<Longrightarrow> x < y in swaps (a # acs) s1 = x < y in (swap 0 ^^ ALG_P (a # acs) x y s1) s2
[PROOF STEP]
show ?case (is "?LHS = ?RHS")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
proof (cases "Suc s < length (swaps ss s1) \<and> (((swaps ss s1)!s=x \<and> (swaps ss s1)!(Suc s)=y) \<or> ((swaps ss s1)!s=y \<and> (swaps ss s1)!(Suc s)=x))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)
[PROOF STEP]
have 1:" Suc s < length (swaps ss s1)"
          and 2: "(swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y
            \<or>  swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)"
[PROOF STATE]
proof (prove)
using this:
Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)

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

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)
[PROOF STEP]
have "ALG_P (s # ss) x y s1 =  1 + ALG_P ss x y s1"
[PROOF STATE]
proof (prove)
using this:
Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)

goal (1 subgoal):
 1. ALG_P (s # ss) x y s1 = 1 + ALG_P ss x y s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ALG_P (s # ss) x y s1 = 1 + ALG_P ss x y s1

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ALG_P (s # ss) x y s1 = 1 + ALG_P ss x y s1
[PROOF STEP]
have "?RHS = x < y in (swap 0) ((swap 0 ^^ ALG_P ss x y s1) s2)"
[PROOF STATE]
proof (prove)
using this:
ALG_P (s # ss) x y s1 = 1 + ALG_P ss x y s1

goal (1 subgoal):
 1. x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in swap 0 ((swap 0 ^^ ALG_P ss x y s1) s2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in swap 0 ((swap 0 ^^ ALG_P ss x y s1) s2)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in swap 0 ((swap 0 ^^ ALG_P ss x y s1) s2)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
have "\<dots> = (~ x < y in ((swap 0 ^^ ALG_P ss x y s1) s2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap 0 ((swap 0 ^^ ALG_P ss x y s1) s2) = (\<not> x < y in (swap 0 ^^ ALG_P ss x y s1) s2)
[PROOF STEP]
apply(rule swap0in2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. set ((swap 0 ^^ ALG_P ss x y s1) s2) = {x, y}
 2. x \<noteq> y
 3. length ((swap 0 ^^ ALG_P ss x y s1) s2) = 2
 4. dist_perm ((swap 0 ^^ ALG_P ss x y s1) s2) ((swap 0 ^^ ALG_P ss x y s1) s2)
[PROOF STEP]
by(fact)+
[PROOF STATE]
proof (state)
this:
x < y in swap 0 ((swap 0 ^^ ALG_P ss x y s1) s2) = (\<not> x < y in (swap 0 ^^ ALG_P ss x y s1) s2)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in swap 0 ((swap 0 ^^ ALG_P ss x y s1) s2) = (\<not> x < y in (swap 0 ^^ ALG_P ss x y s1) s2)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
have "\<dots> = (~ x < y in swaps ss s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> x < y in (swap 0 ^^ ALG_P ss x y s1) s2) = (\<not> x < y in swaps ss s1)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps ss s1 = x < y in (swap 0 ^^ ALG_P ss x y s1) s2
x < y in s1 = x < y in s2

goal (1 subgoal):
 1. (\<not> x < y in (swap 0 ^^ ALG_P ss x y s1) s2) = (\<not> x < y in swaps ss s1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<not> x < y in (swap 0 ^^ ALG_P ss x y s1) s2) = (\<not> x < y in swaps ss s1)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<not> x < y in (swap 0 ^^ ALG_P ss x y s1) s2) = (\<not> x < y in swaps ss s1)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
have "\<dots> = x < y in (swap s) (swaps ss s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> x < y in swaps ss s1) = x < y in swap s (swaps ss s1)
[PROOF STEP]
using 1  2 before_in_swap
[PROOF STATE]
proof (prove)
using this:
Suc s < length (swaps ss s1)
swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x
\<lbrakk>dist_perm ?xs ?ys; Suc ?n < length ?xs\<rbrakk> \<Longrightarrow> ?x < ?y in swap ?n ?xs = (?x < ?y in ?xs \<and> \<not> (?x = ?xs ! ?n \<and> ?y = ?xs ! Suc ?n) \<or> ?x = ?xs ! Suc ?n \<and> ?y = ?xs ! ?n)

goal (1 subgoal):
 1. (\<not> x < y in swaps ss s1) = x < y in swap s (swaps ss s1)
[PROOF STEP]
by (metis Suc_lessD before_id dd lessI no_before_inI)
[PROOF STATE]
proof (state)
this:
(\<not> x < y in swaps ss s1) = x < y in swap s (swaps ss s1)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
(* bad *)
[PROOF STATE]
proof (state)
this:
(\<not> x < y in swaps ss s1) = x < y in swap s (swaps ss s1)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<not> x < y in swaps ss s1) = x < y in swap s (swaps ss s1)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
have "\<dots> = ?LHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap s (swaps ss s1) = x < y in swaps (s # ss) s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in swap s (swaps ss s1) = x < y in swaps (s # ss) s1

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
 2. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in swaps (s # ss) s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in swaps (s # ss) s1

goal (1 subgoal):
 1. x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x))

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
note F=this
[PROOF STATE]
proof (state)
this:
\<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x))

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x))
[PROOF STEP]
have "ALG_P (s # ss) x y s1 =  ALG_P ss x y s1"
[PROOF STATE]
proof (prove)
using this:
\<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x))

goal (1 subgoal):
 1. ALG_P (s # ss) x y s1 = ALG_P ss x y s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ALG_P (s # ss) x y s1 = ALG_P ss x y s1

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ALG_P (s # ss) x y s1 = ALG_P ss x y s1
[PROOF STEP]
have "?RHS = x < y in ((swap 0 ^^ ALG_P ss x y s1) s2)"
[PROOF STATE]
proof (prove)
using this:
ALG_P (s # ss) x y s1 = ALG_P ss x y s1

goal (1 subgoal):
 1. x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in (swap 0 ^^ ALG_P ss x y s1) s2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in (swap 0 ^^ ALG_P ss x y s1) s2

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in (swap 0 ^^ ALG_P ss x y s1) s2

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
have "\<dots> = x < y in swaps ss s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in (swap 0 ^^ ALG_P ss x y s1) s2 = x < y in swaps ss s1
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
x < y in s1 = x < y in s2 \<Longrightarrow> x < y in swaps ss s1 = x < y in (swap 0 ^^ ALG_P ss x y s1) s2
x < y in s1 = x < y in s2

goal (1 subgoal):
 1. x < y in (swap 0 ^^ ALG_P ss x y s1) s2 = x < y in swaps ss s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in (swap 0 ^^ ALG_P ss x y s1) s2 = x < y in swaps ss s1

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in (swap 0 ^^ ALG_P ss x y s1) s2 = x < y in swaps ss s1

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
have "\<dots> = x < y in (swap s) (swaps ss s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
proof (cases "Suc s < length (swaps ss s1)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
 2. \<not> Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc s < length (swaps ss s1)

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
 2. \<not> Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
with F
[PROOF STATE]
proof (chain)
picking this:
\<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x))
Suc s < length (swaps ss s1)
[PROOF STEP]
have g: "swaps ss s1 ! s \<noteq> x \<or>
         swaps ss s1 ! Suc s \<noteq> y" and
        h: "swaps ss s1 ! s \<noteq> y \<or>
         swaps ss s1 ! Suc s \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
\<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x))
Suc s < length (swaps ss s1)

goal (1 subgoal):
 1. swaps ss s1 ! s \<noteq> x \<or> swaps ss s1 ! Suc s \<noteq> y &&& swaps ss s1 ! s \<noteq> y \<or> swaps ss s1 ! Suc s \<noteq> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaps ss s1 ! s \<noteq> x \<or> swaps ss s1 ! Suc s \<noteq> y
swaps ss s1 ! s \<noteq> y \<or> swaps ss s1 ! Suc s \<noteq> x

goal (2 subgoals):
 1. Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
 2. \<not> Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
unfolding before_in_swap[OF dd True, of x y]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swaps ss s1 = (x < y in swaps ss s1 \<and> \<not> (x = swaps ss s1 ! s \<and> y = swaps ss s1 ! Suc s) \<or> x = swaps ss s1 ! Suc s \<and> y = swaps ss s1 ! s)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swaps ss s1 = (x < y in swaps ss s1 \<and> (x = swaps ss s1 ! s \<longrightarrow> y \<noteq> swaps ss s1 ! Suc s) \<or> x = swaps ss s1 ! Suc s \<and> y = swaps ss s1 ! s)
[PROOF STEP]
using g h
[PROOF STATE]
proof (prove)
using this:
swaps ss s1 ! s \<noteq> x \<or> swaps ss s1 ! Suc s \<noteq> y
swaps ss s1 ! s \<noteq> y \<or> swaps ss s1 ! Suc s \<noteq> x

goal (1 subgoal):
 1. x < y in swaps ss s1 = (x < y in swaps ss s1 \<and> (x = swaps ss s1 ! s \<longrightarrow> y \<noteq> swaps ss s1 ! Suc s) \<or> x = swaps ss s1 ! Suc s \<and> y = swaps ss s1 ! s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in swaps ss s1 = x < y in swap s (swaps ss s1)

goal (1 subgoal):
 1. \<not> Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Suc s < length (swaps ss s1)

goal (1 subgoal):
 1. \<not> Suc s < length (swaps ss s1) \<Longrightarrow> x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Suc s < length (swaps ss s1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> Suc s < length (swaps ss s1)

goal (1 subgoal):
 1. x < y in swaps ss s1 = x < y in swap s (swaps ss s1)
[PROOF STEP]
unfolding swap_def
[PROOF STATE]
proof (prove)
using this:
\<not> Suc s < length (foldr (\<lambda>n xs. if Suc n < length xs then xs[n := xs ! Suc n, Suc n := xs ! n] else xs) ss s1)

goal (1 subgoal):
 1. x < y in foldr (\<lambda>n xs. if Suc n < length xs then xs[n := xs ! Suc n, Suc n := xs ! n] else xs) ss s1 = x < y in (if Suc s < length (foldr (\<lambda>n xs. if Suc n < length xs then xs[n := xs ! Suc n, Suc n := xs ! n] else xs) ss s1) then (foldr (\<lambda>n xs. if Suc n < length xs then xs[n := xs ! Suc n, Suc n := xs ! n] else xs) ss s1)[s := foldr (\<lambda>n xs. if Suc n < length xs then xs[n := xs ! Suc n, Suc n := xs ! n] else xs) ss s1 ! Suc s, Suc s := foldr (\<lambda>n xs. if Suc n < length xs then xs[n := xs ! Suc n, Suc n := xs ! n] else xs) ss s1 ! s] else foldr (\<lambda>n xs. if Suc n < length xs then xs[n := xs ! Suc n, Suc n := xs ! n] else xs) ss s1)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
x < y in swaps ss s1 = x < y in swap s (swaps ss s1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x < y in swaps ss s1 = x < y in swap s (swaps ss s1)

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in swaps ss s1 = x < y in swap s (swaps ss s1)

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
have "\<dots> = ?LHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap s (swaps ss s1) = x < y in swaps (s # ss) s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in swap s (swaps ss s1) = x < y in swaps (s # ss) s1

goal (1 subgoal):
 1. \<not> (Suc s < length (swaps ss s1) \<and> (swaps ss s1 ! s = x \<and> swaps ss s1 ! Suc s = y \<or> swaps ss s1 ! s = y \<and> swaps ss s1 ! Suc s = x)) \<Longrightarrow> x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in swaps (s # ss) s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2 = x < y in swaps (s # ss) s1

goal (1 subgoal):
 1. x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x < y in swaps (s # ss) s1 = x < y in (swap 0 ^^ ALG_P (s # ss) x y s1) s2

goal:
No subgoals!
[PROOF STEP]
qed


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