[STATEMENT]
lemma T1_7:
assumes "T\<^sub>p init qs Strat = T\<^sub>p_opt init qs" "length Strat = length qs"
  "x \<noteq> (y::('a::linorder))" "x\<in> set init" "y \<in> set init" "distinct init"
  "set qs \<subseteq> set init"
shows "T\<^sub>p_opt (Lxy init {x,y}) (Lxy qs {x,y})
  \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
have A:"length qs \<le> length qs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length qs \<le> length qs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length qs \<le> length qs

goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
have B:"  x \<noteq> y "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p init qs Strat = T\<^sub>p_opt init qs
length Strat = length qs
x \<noteq> y
x \<in> set init
y \<in> set init
distinct init
set qs \<subseteq> set init

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
from T1_7'[OF assms(1,2), of "length qs" x y, OF A B assms(4-7)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>Strat2 sws. length Strat2 = length (Lxy (take (length qs) qs) {x, y}) \<and> x < y in steps' init (take (length qs) qs) (take (length qs) Strat) (length qs) = x < y in swaps sws (steps' (Lxy init {x, y}) (Lxy (take (length qs) qs) {x, y}) Strat2 (length Strat2)) \<and> T\<^sub>p (Lxy init {x, y}) (Lxy (take (length qs) qs) {x, y}) Strat2 + length sws = ALGxy_det Strat (take (length qs) qs) init x y + ALG_Pxy Strat (take (length qs) qs) init x y
[PROOF STEP]
obtain Strat2 sws where
      len: "length Strat2 = length (Lxy qs {x, y})"
     and "x < y in steps' init qs (take (length qs) Strat)
         (length qs) = x < y in swaps sws (steps' (Lxy init {x,y})
           (Lxy qs {x, y}) Strat2 (length Strat2))"
     and Tp: "T\<^sub>p (Lxy init {x,y}) (Lxy qs {x, y}) Strat2 + length sws
        =  ALGxy_det Strat qs init x y
         + ALG_Pxy Strat qs init x y"
[PROOF STATE]
proof (prove)
using this:
\<exists>Strat2 sws. length Strat2 = length (Lxy (take (length qs) qs) {x, y}) \<and> x < y in steps' init (take (length qs) qs) (take (length qs) Strat) (length qs) = x < y in swaps sws (steps' (Lxy init {x, y}) (Lxy (take (length qs) qs) {x, y}) Strat2 (length Strat2)) \<and> T\<^sub>p (Lxy init {x, y}) (Lxy (take (length qs) qs) {x, y}) Strat2 + length sws = ALGxy_det Strat (take (length qs) qs) init x y + ALG_Pxy Strat (take (length qs) qs) init x y

goal (1 subgoal):
 1. (\<And>Strat2 sws. \<lbrakk>length Strat2 = length (Lxy qs {x, y}); x < y in steps' init qs (take (length qs) Strat) (length qs) = x < y in swaps sws (steps' (Lxy init {x, y}) (Lxy qs {x, y}) Strat2 (length Strat2)); T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2 + length sws = ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length Strat2 = length (Lxy qs {x, y})
x < y in steps' init qs (take (length qs) Strat) (length qs) = x < y in swaps sws (steps' (Lxy init {x, y}) (Lxy qs {x, y}) Strat2 (length Strat2))
T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2 + length sws = ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y

goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
have "T\<^sub>p_opt (Lxy init {x,y}) (Lxy qs {x,y}) \<le> T\<^sub>p (Lxy init {x,y}) (Lxy qs {x, y}) Strat2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2
[PROOF STEP]
unfolding T_opt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> {T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) as |as. length as = length (Lxy qs {x, y})} \<le> T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2
[PROOF STEP]
apply(rule cInf_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2 \<in> {T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) as |as. length as = length (Lxy qs {x, y})}
 2. bdd_below {T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) as |as. length as = length (Lxy qs {x, y})}
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
length Strat2 = length (Lxy qs {x, y})

goal (2 subgoals):
 1. T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2 \<in> {T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) as |as. length as = length (Lxy qs {x, y})}
 2. bdd_below {T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) as |as. length as = length (Lxy qs {x, y})}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2

goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2

goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
have "\<dots> \<le> ALGxy_det Strat qs init x y
         + ALG_Pxy Strat qs init x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2 \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
using Tp
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p (Lxy init {x, y}) (Lxy qs {x, y}) Strat2 + length sws = ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y

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

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

goal (1 subgoal):
 1. T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y}) \<le> ALGxy_det Strat qs init x y + ALG_Pxy Strat qs init x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma T_snoc: "length rs = length as
       \<Longrightarrow>  T init (rs@[r]) (as@[a])
        = T init rs as + t\<^sub>p (steps' init rs as (length rs)) r a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length rs = length as \<Longrightarrow> T\<^sub>p init (rs @ [r]) (as @ [a]) = T\<^sub>p init rs as + t\<^sub>p (steps' init rs as (length rs)) r a
[PROOF STEP]
apply(induct rs as arbitrary: init rule: list_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>init. T\<^sub>p init ([] @ [r]) ([] @ [a]) = T\<^sub>p init [] [] + t\<^sub>p (steps' init [] [] (length [])) r a
 2. \<And>x xs y ys init. \<lbrakk>length xs = length ys; \<And>init. T\<^sub>p init (xs @ [r]) (ys @ [a]) = T\<^sub>p init xs ys + t\<^sub>p (steps' init xs ys (length xs)) r a\<rbrakk> \<Longrightarrow> T\<^sub>p init ((x # xs) @ [r]) ((y # ys) @ [a]) = T\<^sub>p init (x # xs) (y # ys) + t\<^sub>p (steps' init (x # xs) (y # ys) (length (x # xs))) r a
[PROOF STEP]
by simp_all


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


[STATEMENT]
lemma steps'_take:
  assumes "n<length qs" "length qs = length Strat"
  shows "steps' init (take n qs) (take n Strat) n
      = steps' init qs Strat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps' init (take n qs) (take n Strat) n = steps' init qs Strat n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. steps' init (take n qs) (take n Strat) n = steps' init qs Strat n
[PROOF STEP]
have "steps' init qs 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 qs Strat n = steps' init (take n qs @ drop n qs) (take n Strat @ drop n Strat) n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
steps' init qs 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]
also
[PROOF STATE]
proof (state)
this:
steps' init qs 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]
have "\<dots> = steps' init (take n qs) (take n Strat) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps' init (take n qs @ drop n qs) (take n Strat @ drop n Strat) n = steps' init (take n qs) (take n Strat) n
[PROOF STEP]
apply(subst steps'_rests[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. length (take n qs) = length (take n Strat)
 2. n \<le> length (take n Strat)
 3. steps' init (take n qs) (take n Strat) n = steps' init (take n qs) (take n Strat) n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n < length qs
length qs = length Strat

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

goal (1 subgoal):
 1. steps' init (take n qs) (take n Strat) n = steps' init qs Strat n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
steps' init qs Strat n = steps' init (take n qs) (take n Strat) n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps' init qs Strat n = steps' init (take n qs) (take n Strat) n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Tp_darstellung: "length qs = length Strat
        \<Longrightarrow> T\<^sub>p init qs Strat =
        (\<Sum>i\<in>{..<length qs}. t\<^sub>p (steps' init qs Strat i) (qs!i) (Strat!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length qs = length Strat \<Longrightarrow> T\<^sub>p init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length qs = length Strat \<Longrightarrow> T\<^sub>p init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
assume a[simp]: "length qs = length Strat"
[PROOF STATE]
proof (state)
this:
length qs = length Strat

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

goal (1 subgoal):
 1. length qs = length Strat \<Longrightarrow> T\<^sub>p init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length qs = length Strat \<Longrightarrow> T\<^sub>p init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
have "n\<le>length qs
        \<Longrightarrow> T\<^sub>p init (take n qs) (take n Strat) =
        (\<Sum>i\<in>{..<n}. t\<^sub>p (steps' init qs Strat i) (qs!i) (Strat!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length qs \<Longrightarrow> T\<^sub>p init (take n qs) (take n Strat) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
apply(induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> length qs \<Longrightarrow> T\<^sub>p init (take 0 qs) (take 0 Strat) = (\<Sum>i<0. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
 2. \<And>n. \<lbrakk>n \<le> length qs \<Longrightarrow> T\<^sub>p init (take n qs) (take n Strat) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)); Suc n \<le> length qs\<rbrakk> \<Longrightarrow> T\<^sub>p init (take (Suc n) qs) (take (Suc n) Strat) = (\<Sum>i<Suc n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> length qs \<Longrightarrow> T\<^sub>p init (take n qs) (take n Strat) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)); Suc n \<le> length qs\<rbrakk> \<Longrightarrow> T\<^sub>p init (take (Suc n) qs) (take (Suc n) Strat) = (\<Sum>i<Suc n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
apply(simp add: take_Suc_conv_app_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>T\<^sub>p init (take n qs) (take n Strat) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)); Suc n \<le> length Strat\<rbrakk> \<Longrightarrow> T\<^sub>p init (take n qs @ [qs ! n]) (take n Strat @ [Strat ! n]) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)) + t\<^sub>p (steps' init qs Strat n) (qs ! n) (Strat ! n)
[PROOF STEP]
apply(subst T_snoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>T\<^sub>p init (take n qs) (take n Strat) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)); Suc n \<le> length Strat\<rbrakk> \<Longrightarrow> length (take n qs) = length (take n Strat)
 2. \<And>n. \<lbrakk>T\<^sub>p init (take n qs) (take n Strat) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)); Suc n \<le> length Strat\<rbrakk> \<Longrightarrow> T\<^sub>p init (take n qs) (take n Strat) + t\<^sub>p (steps' init (take n qs) (take n Strat) (length (take n qs))) (qs ! n) (Strat ! n) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)) + t\<^sub>p (steps' init qs Strat n) (qs ! n) (Strat ! n)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>T\<^sub>p init (take n qs) (take n Strat) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)); Suc n \<le> length Strat\<rbrakk> \<Longrightarrow> T\<^sub>p init (take n qs) (take n Strat) + t\<^sub>p (steps' init (take n qs) (take n Strat) (length (take n qs))) (qs ! n) (Strat ! n) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i)) + t\<^sub>p (steps' init qs Strat n) (qs ! n) (Strat ! n)
[PROOF STEP]
by(simp add: min_def steps'_take)
[PROOF STATE]
proof (state)
this:
n \<le> length qs \<Longrightarrow> T\<^sub>p init (take n qs) (take n Strat) = (\<Sum>i<n. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))

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

goal (1 subgoal):
 1. length qs = length Strat \<Longrightarrow> T\<^sub>p init qs Strat = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
from a this[of "length qs"]
[PROOF STATE]
proof (chain)
picking this:
length qs = length Strat
length qs \<le> length qs \<Longrightarrow> T\<^sub>p init (take (length qs) qs) (take (length qs) Strat) = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length qs = length Strat
length qs \<le> length qs \<Longrightarrow> T\<^sub>p init (take (length qs) qs) (take (length qs) Strat) = (\<Sum>i<length qs. t\<^sub>p (steps' init qs Strat i) (qs ! i) (Strat ! i))

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

goal:
No subgoals!
[PROOF STEP]
qed