[STATEMENT]
theorem COMB_OPT2':  "(x::nat) \<noteq> y \<Longrightarrow> set \<sigma> \<subseteq> {x,y}
     \<Longrightarrow> T\<^sub>p_on_rand (COMB []) [x,y] \<sigma>  \<le> 1.6 * real (T\<^sub>p_opt [x,y] \<sigma>) + 1.6"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) [x, y] \<bind> (\<lambda>is. return_pmf ([x, y], is))) \<sigma> \<le> 16 / 10 * real (T\<^sub>p_opt [x, y] \<sigma>) + 16 / 10
[PROOF STEP]
proof (rule Phase_partitioning_general[where P="inv_COMB"], goal_cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> 0 \<le> 16 / 10
 3. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> set \<sigma> \<subseteq> {x, y}
 4. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> inv_COMB (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) x [x, y]
 5. \<And>a b \<sigma>' s. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}; \<sigma>' \<in> Lxx a b; a \<noteq> b; {a, b} = {x, y}; inv_COMB s a [x, y]; set \<sigma>' \<subseteq> {a, b}\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s \<sigma>' \<le> 16 / 10 * real (T\<^sub>p [a, b] \<sigma>' (OPT2 \<sigma>' [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s \<sigma>') (last \<sigma>') [x, y]
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
x \<noteq> y
set \<sigma> \<subseteq> {x, y}

goal (5 subgoals):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> 0 \<le> 16 / 10
 3. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> set \<sigma> \<subseteq> {x, y}
 4. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> inv_COMB (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) x [x, y]
 5. \<And>a b \<sigma>' s. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}; \<sigma>' \<in> Lxx a b; a \<noteq> b; {a, b} = {x, y}; inv_COMB s a [x, y]; set \<sigma>' \<subseteq> {a, b}\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s \<sigma>' \<le> 16 / 10 * real (T\<^sub>p [a, b] \<sigma>' (OPT2 \<sigma>' [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s \<sigma>') (last \<sigma>') [x, y]
[PROOF STEP]
let ?initBIT ="(map_pmf (Pair [x, y]) (fst BIT [x, y]))"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> 0 \<le> 16 / 10
 3. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> set \<sigma> \<subseteq> {x, y}
 4. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> inv_COMB (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) x [x, y]
 5. \<And>a b \<sigma>' s. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}; \<sigma>' \<in> Lxx a b; a \<noteq> b; {a, b} = {x, y}; inv_COMB s a [x, y]; set \<sigma>' \<subseteq> {a, b}\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s \<sigma>' \<le> 16 / 10 * real (T\<^sub>p [a, b] \<sigma>' (OPT2 \<sigma>' [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s \<sigma>') (last \<sigma>') [x, y]
[PROOF STEP]
let ?initTS ="(map_pmf (Pair [x, y]) (fst (embed (rTS [])) [x, y]))"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> 0 \<le> 16 / 10
 3. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> set \<sigma> \<subseteq> {x, y}
 4. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> inv_COMB (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) x [x, y]
 5. \<And>a b \<sigma>' s. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}; \<sigma>' \<in> Lxx a b; a \<noteq> b; {a, b} = {x, y}; inv_COMB s a [x, y]; set \<sigma>' \<subseteq> {a, b}\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s \<sigma>' \<le> 16 / 10 * real (T\<^sub>p [a, b] \<sigma>' (OPT2 \<sigma>' [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s \<sigma>') (last \<sigma>') [x, y]
[PROOF STEP]
show  "inv_COMB (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) x [x, y]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_COMB (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) x [x, y]
[PROOF STEP]
unfolding inv_COMB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Da Db. finite (set_pmf Da) \<and> finite (set_pmf Db) \<and> map_pmf con (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) = Sum_pmf (8 / 10) Da Db \<and> BIT_inv Da x [x, y] \<and> TS_inv Db x [x, y]
[PROOF STEP]
apply(rule exI[where x="?initBIT"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Db. finite (set_pmf (map_pmf (Pair [x, y]) (fst BIT [x, y]))) \<and> finite (set_pmf Db) \<and> map_pmf con (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) = Sum_pmf (8 / 10) (map_pmf (Pair [x, y]) (fst BIT [x, y])) Db \<and> BIT_inv (map_pmf (Pair [x, y]) (fst BIT [x, y])) x [x, y] \<and> TS_inv Db x [x, y]
[PROOF STEP]
apply(rule exI[where x="?initTS"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf (map_pmf (Pair [x, y]) (fst BIT [x, y]))) \<and> finite (set_pmf (map_pmf (Pair [x, y]) (fst (Partial_Cost_Model.embed (rTS [])) [x, y]))) \<and> map_pmf con (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) = Sum_pmf (8 / 10) (map_pmf (Pair [x, y]) (fst BIT [x, y])) (map_pmf (Pair [x, y]) (fst (Partial_Cost_Model.embed (rTS [])) [x, y])) \<and> BIT_inv (map_pmf (Pair [x, y]) (fst BIT [x, y])) x [x, y] \<and> TS_inv (map_pmf (Pair [x, y]) (fst (Partial_Cost_Model.embed (rTS [])) [x, y])) x [x, y]
[PROOF STEP]
apply(simp only: BIT_inv_initial[OF 4(1)] )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf (map_pmf (Pair [x, y]) (fst BIT [x, y]))) \<and> finite (set_pmf (map_pmf (Pair [x, y]) (fst (Partial_Cost_Model.embed (rTS [])) [x, y]))) \<and> map_pmf con (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) = Sum_pmf (8 / 10) (map_pmf (Pair [x, y]) (fst BIT [x, y])) (map_pmf (Pair [x, y]) (fst (Partial_Cost_Model.embed (rTS [])) [x, y])) \<and> True \<and> TS_inv (map_pmf (Pair [x, y]) (fst (Partial_Cost_Model.embed (rTS [])) [x, y])) x [x, y]
[PROOF STEP]
apply(simp add: map_pmf_def bind_return_pmf bind_assoc_pmf COMB_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union>xa\<in>set_pmf (BIT_init [x, y]). {([x, y], xa)}) \<and> bernoulli_pmf (4 / 5) \<bind> (\<lambda>xa. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xb. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xc. return_pmf (case if xa then Inl ([xc, xb], [x, y]) else Inr [] of Inl is \<Rightarrow> Inl ([x, y], is) | Inr is \<Rightarrow> Inr ([x, y], is))))) = Sum_pmf (4 / 5) (BIT_init [x, y] \<bind> (\<lambda>xa. return_pmf ([x, y], xa))) (return_pmf ([x, y], fst (rTS []) [x, y])) \<and> TS_inv' ([x, y], fst (rTS []) [x, y]) x [x, y]
[PROOF STEP]
apply(simp add: Sum_pmf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union>xa\<in>set_pmf (BIT_init [x, y]). {([x, y], xa)}) \<and> bernoulli_pmf (4 / 5) \<bind> (\<lambda>xa. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xb. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xc. return_pmf (case if xa then Inl ([xc, xb], [x, y]) else Inr [] of Inl is \<Rightarrow> Inl ([x, y], is) | Inr is \<Rightarrow> Inr ([x, y], is))))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (BIT_init [x, y] \<bind> (\<lambda>xa. return_pmf ([x, y], xa))) else map_pmf Inr (return_pmf ([x, y], fst (rTS []) [x, y]))) \<and> TS_inv' ([x, y], fst (rTS []) [x, y]) x [x, y]
[PROOF STEP]
apply(safe)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite (\<Union>xa\<in>set_pmf (BIT_init [x, y]). {([x, y], xa)})
 2. bernoulli_pmf (4 / 5) \<bind> (\<lambda>xa. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xb. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xc. return_pmf (case if xa then Inl ([xc, xb], [x, y]) else Inr [] of Inl is \<Rightarrow> Inl ([x, y], is) | Inr is \<Rightarrow> Inr ([x, y], is))))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (BIT_init [x, y] \<bind> (\<lambda>xa. return_pmf ([x, y], xa))) else map_pmf Inr (return_pmf ([x, y], fst (rTS []) [x, y])))
 3. TS_inv' ([x, y], fst (rTS []) [x, y]) x [x, y]
[PROOF STEP]
apply(simp add: BIT_init_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>xa. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xb. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xc. return_pmf (case if xa then Inl ([xc, xb], [x, y]) else Inr [] of Inl is \<Rightarrow> Inl ([x, y], is) | Inr is \<Rightarrow> Inr ([x, y], is))))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (BIT_init [x, y] \<bind> (\<lambda>xa. return_pmf ([x, y], xa))) else map_pmf Inr (return_pmf ([x, y], fst (rTS []) [x, y])))
 2. TS_inv' ([x, y], fst (rTS []) [x, y]) x [x, y]
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. bernoulli_pmf (4 / 5) = bernoulli_pmf (4 / 5)
 2. \<And>xa. xa \<in> set_pmf (bernoulli_pmf (4 / 5)) \<Longrightarrow> bernoulli_pmf (1 / 2) \<bind> (\<lambda>xb. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xc. return_pmf (case if xa then Inl ([xc, xb], [x, y]) else Inr [] of Inl is \<Rightarrow> Inl ([x, y], is) | Inr is \<Rightarrow> Inr ([x, y], is)))) = (if xa then map_pmf Inl (BIT_init [x, y] \<bind> (\<lambda>xa. return_pmf ([x, y], xa))) else map_pmf Inr (return_pmf ([x, y], fst (rTS []) [x, y])))
 3. TS_inv' ([x, y], fst (rTS []) [x, y]) x [x, y]
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> set_pmf (bernoulli_pmf (4 / 5)) \<Longrightarrow> bernoulli_pmf (1 / 2) \<bind> (\<lambda>xb. bernoulli_pmf (1 / 2) \<bind> (\<lambda>xc. return_pmf (case if xa then Inl ([xc, xb], [x, y]) else Inr [] of Inl is \<Rightarrow> Inl ([x, y], is) | Inr is \<Rightarrow> Inr ([x, y], is)))) = (if xa then map_pmf Inl (BIT_init [x, y] \<bind> (\<lambda>xa. return_pmf ([x, y], xa))) else map_pmf Inr (return_pmf ([x, y], fst (rTS []) [x, y])))
 2. TS_inv' ([x, y], fst (rTS []) [x, y]) x [x, y]
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf rTS_def map_pmf_def BIT_init_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TS_inv' ([x, y], fst (rTS []) [x, y]) x [x, y]
[PROOF STEP]
apply(simp add: TS_inv_def rTS_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
inv_COMB (map_pmf (Pair [x, y]) (fst (COMB []) [x, y])) x [x, y]

goal (4 subgoals):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> 0 \<le> 16 / 10
 3. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> set \<sigma> \<subseteq> {x, y}
 4. \<And>a b \<sigma>' s. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}; \<sigma>' \<in> Lxx a b; a \<noteq> b; {a, b} = {x, y}; inv_COMB s a [x, y]; set \<sigma>' \<subseteq> {a, b}\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s \<sigma>' \<le> 16 / 10 * real (T\<^sub>p [a, b] \<sigma>' (OPT2 \<sigma>' [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s \<sigma>') (last \<sigma>') [x, y]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> 0 \<le> 16 / 10
 3. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> set \<sigma> \<subseteq> {x, y}
 4. \<And>a b \<sigma>' s. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}; \<sigma>' \<in> Lxx a b; a \<noteq> b; {a, b} = {x, y}; inv_COMB s a [x, y]; set \<sigma>' \<subseteq> {a, b}\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s \<sigma>' \<le> 16 / 10 * real (T\<^sub>p [a, b] \<sigma>' (OPT2 \<sigma>' [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s \<sigma>') (last \<sigma>') [x, y]
[PROOF STEP]
case (5 a b qs s)
[PROOF STATE]
proof (state)
this:
x \<noteq> y
set \<sigma> \<subseteq> {x, y}
qs \<in> Lxx a b
a \<noteq> b
{a, b} = {x, y}
inv_COMB s a [x, y]
set qs \<subseteq> {a, b}

goal (4 subgoals):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> 0 \<le> 16 / 10
 3. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> set \<sigma> \<subseteq> {x, y}
 4. \<And>a b \<sigma>' s. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}; \<sigma>' \<in> Lxx a b; a \<noteq> b; {a, b} = {x, y}; inv_COMB s a [x, y]; set \<sigma>' \<subseteq> {a, b}\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s \<sigma>' \<le> 16 / 10 * real (T\<^sub>p [a, b] \<sigma>' (OPT2 \<sigma>' [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s \<sigma>') (last \<sigma>') [x, y]
[PROOF STEP]
from 5(3)
[PROOF STATE]
proof (chain)
picking this:
qs \<in> Lxx a b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
qs \<in> Lxx a b

goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
proof (rule LxxE, goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 3. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 4. qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom b])

goal (4 subgoals):
 1. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 3. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 4. qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom b])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom b])

goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(rule Combination)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. a \<noteq> b
 2. {a, b} = {x, y}
 3. set qs \<subseteq> {a, b}
 4. inv_COMB s a [x, y]
 5. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts
 6. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit
 7. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 8. qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * ?ts + 8 / 10 * ?bit \<le> 16 / 10 * ?opt
[PROOF STEP]
apply(fact)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts
 2. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit
 3. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 4. qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * ?ts + 8 / 10 * ?bit \<le> 16 / 10 * ?opt
[PROOF STEP]
using TS_a''
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<noteq> ?y; {?x, ?y} = {?x0.0, ?y0.0}; TS_inv ?s ?x [?x0.0, ?y0.0]; set ?qs \<subseteq> {?x, ?y}; ?qs \<in> lang (seq [question (Atom ?x), Atom ?y, Atom ?y])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS ?h0.0)) ?s ?qs) (last ?qs) [?x0.0, ?y0.0] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS ?h0.0)) ?s ?qs = 2

goal (4 subgoals):
 1. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts
 2. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit
 3. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 4. qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * ?ts + 8 / 10 * ?bit \<le> 16 / 10 * ?opt
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit
 2. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 3. qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * 2 + 8 / 10 * ?bit \<le> 16 / 10 * ?opt
[PROOF STEP]
apply(fact bit_a'')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [question (Atom a), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * 2 + 8 / 10 * (15 / 10) \<le> 16 / 10 * ?opt
[PROOF STEP]
apply(fact OPT2_A')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * 2 + 8 / 10 * (15 / 10) \<le> 16 / 10 * 1
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]

goal (3 subgoals):
 1. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 3. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 3. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
qs \<in> lang (seq [Atom a, Atom a])

goal (3 subgoals):
 1. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 3. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qs \<in> lang (seq [Atom a, Atom a])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
qs \<in> lang (seq [Atom a, Atom a])

goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(rule Combination)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. a \<noteq> b
 2. {a, b} = {x, y}
 3. set qs \<subseteq> {a, b}
 4. inv_COMB s a [x, y]
 5. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts
 6. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit
 7. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 8. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> 2 / 10 * ?ts + 8 / 10 * ?bit \<le> 16 / 10 * ?opt
[PROOF STEP]
apply(fact)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts
 2. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit
 3. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 4. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> 2 / 10 * ?ts + 8 / 10 * ?bit \<le> 16 / 10 * ?opt
[PROOF STEP]
apply(fact TS_d'')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit
 2. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 3. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> 2 / 10 * 0 + 8 / 10 * ?bit \<le> 16 / 10 * ?opt
[PROOF STEP]
apply(fact bit_d')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt
 2. qs \<in> lang (seq [Atom a, Atom a]) \<Longrightarrow> 2 / 10 * 0 + 8 / 10 * 0 \<le> 16 / 10 * ?opt
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]

goal (2 subgoals):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])

goal (2 subgoals):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])
[PROOF STEP]
have "qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])
              \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])"
[PROOF STATE]
proof (prove)
using this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])

goal (1 subgoal):
 1. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])

goal (2 subgoals):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])

goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(rule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(erule Combination)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. a \<noteq> b
 2. {a, b} = {x, y}
 3. set qs \<subseteq> {a, b}
 4. inv_COMB s a [x, y]
 5. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts3
 6. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit3
 7. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt3
 8. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * ?ts3 + 8 / 10 * ?bit3 \<le> 16 / 10 * ?opt3
 9. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(fact)+
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts3
 2. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit3
 3. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt3
 4. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * ?ts3 + 8 / 10 * ?bit3 \<le> 16 / 10 * ?opt3
 5. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(fact TS_b1'')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit3
 2. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt3
 3. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * real (length qs - 2) + 8 / 10 * ?bit3 \<le> 16 / 10 * ?opt3
 4. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(fact bit_b''1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt3
 2. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * real (length qs - 2) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs) - 5 / 10) \<le> 16 / 10 * ?opt3
 3. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(fact OPT2_B1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * real (length qs - 2) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs) - 5 / 10) \<le> 16 / 10 * (real (length qs) / 2)
 2. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(simp add: ring_distribs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(erule Combination)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. a \<noteq> b
 2. {a, b} = {x, y}
 3. set qs \<subseteq> {a, b}
 4. inv_COMB s a [x, y]
 5. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts39
 6. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit39
 7. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt39
 8. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * ?ts39 + 8 / 10 * ?bit39 \<le> 16 / 10 * ?opt39
[PROOF STEP]
apply(fact)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts39
 2. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit39
 3. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt39
 4. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * ?ts39 + 8 / 10 * ?bit39 \<le> 16 / 10 * ?opt39
[PROOF STEP]
apply(fact TS_b2'')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit39
 2. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt39
 3. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * real (length qs - 3) + 8 / 10 * ?bit39 \<le> 16 / 10 * ?opt39
[PROOF STEP]
apply(fact bit_b''2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt39
 2. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * real (length qs - 3) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs - 1) - 5 / 10) \<le> 16 / 10 * ?opt39
[PROOF STEP]
apply(fact OPT2_B2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom b, Atom b]) \<Longrightarrow> 2 / 10 * real (length qs - 3) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs - 1) - 5 / 10) \<le> 16 / 10 * (real (length qs - 1) / 2)
[PROOF STEP]
apply(simp add: ring_distribs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]

goal (1 subgoal):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])

goal (1 subgoal):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])
[PROOF STEP]
have len: "length qs \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])

goal (1 subgoal):
 1. 2 \<le> length qs
[PROOF STEP]
by(auto simp add: conc_def)
[PROOF STATE]
proof (state)
this:
2 \<le> length qs

goal (1 subgoal):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
have len2: "qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])
                  \<Longrightarrow> length qs \<ge> 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 3 \<le> length qs
[PROOF STEP]
by (auto simp add: conc_def)
[PROOF STATE]
proof (state)
this:
qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 3 \<le> length qs

goal (1 subgoal):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])
[PROOF STEP]
have "qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])
              \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])"
[PROOF STATE]
proof (prove)
using this:
qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])

goal (1 subgoal):
 1. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])

goal (1 subgoal):
 1. qs \<in> lang (seq [question (Atom a), Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<or> qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])

goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(rule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
 2. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(erule Combination)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. a \<noteq> b
 2. {a, b} = {x, y}
 3. set qs \<subseteq> {a, b}
 4. inv_COMB s a [x, y]
 5. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts3
 6. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit3
 7. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt3
 8. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * ?ts3 + 8 / 10 * ?bit3 \<le> 16 / 10 * ?opt3
 9. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(fact)+
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts3
 2. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit3
 3. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt3
 4. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * ?ts3 + 8 / 10 * ?bit3 \<le> 16 / 10 * ?opt3
 5. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(fact TS_c1'')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit3
 2. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt3
 3. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * real (length qs - 2) + 8 / 10 * ?bit3 \<le> 16 / 10 * ?opt3
 4. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(fact bit_c''1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt3
 2. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * real (length qs - 2) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs) - 5 / 10) \<le> 16 / 10 * ?opt3
 3. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(fact OPT2_C1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * real (length qs - 2) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs) - 5 / 10) \<le> 16 / 10 * (real (length qs - 1) / 2)
 2. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
2 \<le> length qs

goal (2 subgoals):
 1. qs \<in> lang (seq [Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * real (length qs - 2) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs) - 5 / 10) \<le> 16 / 10 * (real (length qs - 1) / 2)
 2. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(simp add: ring_distribs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
apply(erule Combination)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. a \<noteq> b
 2. {a, b} = {x, y}
 3. set qs \<subseteq> {a, b}
 4. inv_COMB s a [x, y]
 5. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts85
 6. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit85
 7. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt85
 8. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * ?ts85 + 8 / 10 * ?bit85 \<le> 16 / 10 * ?opt85
[PROOF STEP]
apply(fact)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s h. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; TS_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS h)) s qs = ?ts85
 2. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit85
 3. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt85
 4. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * ?ts85 + 8 / 10 * ?bit85 \<le> 16 / 10 * ?opt85
[PROOF STEP]
apply(fact TS_c2'')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>a \<noteq> b; {a, b} = {x, y}; BIT_inv s a [x, y]; set qs \<subseteq> {a, b}; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT s qs = ?bit85
 2. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt85
 3. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * real (length qs - 3) + 8 / 10 * ?bit85 \<le> 16 / 10 * ?opt85
[PROOF STEP]
apply(fact bit_c''2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a])\<rbrakk> \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = ?opt85
 2. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * real (length qs - 3) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs - 1) - 5 / 10) \<le> 16 / 10 * ?opt85
[PROOF STEP]
apply(fact OPT2_C2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * real (length qs - 3) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs - 1) - 5 / 10) \<le> 16 / 10 * (real (length qs - 2) / 2)
[PROOF STEP]
using len2
[PROOF STATE]
proof (prove)
using this:
qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 3 \<le> length qs

goal (1 subgoal):
 1. qs \<in> lang (seq [Atom a, Atom b, Atom a, Star (Times (Atom b) (Atom a)), Atom a]) \<Longrightarrow> 2 / 10 * real (length qs - 3) + 8 / 10 * (75 / 10\<^sup>2 * real (length qs - 1) - 5 / 10) \<le> 16 / 10 * (real (length qs - 2) / 2)
[PROOF STEP]
apply(simp add: ring_distribs conc_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) \<and> inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]

goal (3 subgoals):
 1. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> 0 \<le> 16 / 10
 3. \<lbrakk>x \<noteq> y; set \<sigma> \<subseteq> {x, y}\<rbrakk> \<Longrightarrow> set \<sigma> \<subseteq> {x, y}
[PROOF STEP]
qed (simp_all)


[STATEMENT]
lemma config_rand_COMB: "config_rand (COMB h) init qs = do {
                    (b::bool) \<leftarrow> (bernoulli_pmf 0.8);
                    (b1,b2) \<leftarrow>  (config_rand BIT init qs);
                    (t1,t2) \<leftarrow>  (config_rand (embed (rTS h)) init qs);
                    return_pmf (if b then  (b1, Inl b2) else (t1, Inr t2))
                    }" (is "?LHS = ?RHS")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) qs = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
proof (induct qs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) [] = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) [] \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) [] \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
 2. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) xs = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2))))) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) [] = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) [] \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) [] \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
 2. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) xs = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2))))) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) [] = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) [] \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) [] \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
apply(simp add: BIT_init_def COMB_def rTS_def map_pmf_def bind_return_pmf bind_assoc_pmf )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. bv (length init) \<bind> (\<lambda>xa. return_pmf (init, if x then Inl (xa, init) else Inr h))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. bv (length init) \<bind> (\<lambda>x. return_pmf (if b then (init, Inl (x, init)) else (init, Inr h))))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bernoulli_pmf (4 / 5) = bernoulli_pmf (4 / 5)
 2. \<And>x. x \<in> set_pmf (bernoulli_pmf (4 / 5)) \<Longrightarrow> bv (length init) \<bind> (\<lambda>xa. return_pmf (init, if x then Inl (xa, init) else Inr h)) = bv (length init) \<bind> (\<lambda>xa. return_pmf (if x then (init, Inl (xa, init)) else (init, Inr h)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf (bernoulli_pmf (4 / 5)) \<Longrightarrow> bv (length init) \<bind> (\<lambda>xa. return_pmf (init, if x then Inl (xa, init) else Inr h)) = bv (length init) \<bind> (\<lambda>xa. return_pmf (if x then (init, Inl (xa, init)) else (init, Inr h)))
[PROOF STEP]
apply(simp only: set_pmf_bernoulli)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> bv (length init) \<bind> (\<lambda>xa. return_pmf (init, if x then Inl (xa, init) else Inr h)) = bv (length init) \<bind> (\<lambda>xa. return_pmf (if x then (init, Inl (xa, init)) else (init, Inr h)))
[PROOF STEP]
apply(case_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> UNIV; x\<rbrakk> \<Longrightarrow> bv (length init) \<bind> (\<lambda>xa. return_pmf (init, if x then Inl (xa, init) else Inr h)) = bv (length init) \<bind> (\<lambda>xa. return_pmf (if x then (init, Inl (xa, init)) else (init, Inr h)))
 2. \<And>x. \<lbrakk>x \<in> UNIV; \<not> x\<rbrakk> \<Longrightarrow> bv (length init) \<bind> (\<lambda>xa. return_pmf (init, if x then Inl (xa, init) else Inr h)) = bv (length init) \<bind> (\<lambda>xa. return_pmf (if x then (init, Inl (xa, init)) else (init, Inr h)))
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) [] = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) [] \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) [] \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))

goal (1 subgoal):
 1. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) xs = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2))))) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) xs = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2))))) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
case (snoc q qs)
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) qs = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))

goal (1 subgoal):
 1. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) xs = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) xs \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2))))) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (xs @ [x]) \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
apply(simp add: take_Suc_conv_app_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (fst (rTS h) init) \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
apply(subst config'_rand_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) (Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) qs) [q] = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (fst (rTS h) init) \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
apply(subst snoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) (bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))) [q] = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (fst (rTS h) init) \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (fst (rTS h) init) \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2))))) \<bind> (\<lambda>s. snd (COMB h) s q \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (fst (rTS h) init) \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf split_def config'_rand_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xb. snd (COMB h) (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb))) q \<bind> (\<lambda>p. return_pmf (step (fst (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb)))) q (fst p), snd p))))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>x. BIT_step x q \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xb. return_pmf (if b then (fst (step (fst x) q (fst xa), snd xa), Inl (snd (step (fst x) q (fst xa), snd xa))) else (fst (step (fst xb) q (fst (snd (rTS h) xb q)), snd (snd (rTS h) xb q)), Inr (snd (step (fst xb) q (fst (snd (rTS h) xb q)), snd (snd (rTS h) xb q)))))))))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bernoulli_pmf (4 / 5) = bernoulli_pmf (4 / 5)
 2. \<And>x. x \<in> set_pmf (bernoulli_pmf (4 / 5)) \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xb. snd (COMB h) (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb))) q \<bind> (\<lambda>p. return_pmf (step (fst (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb)))) q (fst p), snd p)))) = Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. BIT_step xa q \<bind> (\<lambda>xb. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xc. return_pmf (if x then (fst (step (fst xa) q (fst xb), snd xb), Inl (snd (step (fst xa) q (fst xb), snd xb))) else (fst (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q)), Inr (snd (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q))))))))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf (bernoulli_pmf (4 / 5)) \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xb. snd (COMB h) (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb))) q \<bind> (\<lambda>p. return_pmf (step (fst (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb)))) q (fst p), snd p)))) = Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. BIT_step xa q \<bind> (\<lambda>xb. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xc. return_pmf (if x then (fst (step (fst xa) q (fst xb), snd xb), Inl (snd (step (fst xa) q (fst xb), snd xb))) else (fst (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q)), Inr (snd (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q))))))))
[PROOF STEP]
apply(simp only: set_pmf_bernoulli)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xb. snd (COMB h) (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb))) q \<bind> (\<lambda>p. return_pmf (step (fst (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb)))) q (fst p), snd p)))) = Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. BIT_step xa q \<bind> (\<lambda>xb. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xc. return_pmf (if x then (fst (step (fst xa) q (fst xb), snd xb), Inl (snd (step (fst xa) q (fst xb), snd xb))) else (fst (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q)), Inr (snd (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q))))))))
[PROOF STEP]
apply(case_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> UNIV; x\<rbrakk> \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xb. snd (COMB h) (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb))) q \<bind> (\<lambda>p. return_pmf (step (fst (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb)))) q (fst p), snd p)))) = Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. BIT_step xa q \<bind> (\<lambda>xb. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xc. return_pmf (if x then (fst (step (fst xa) q (fst xb), snd xb), Inl (snd (step (fst xa) q (fst xb), snd xb))) else (fst (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q)), Inr (snd (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q))))))))
 2. \<And>x. \<lbrakk>x \<in> UNIV; \<not> x\<rbrakk> \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xb. snd (COMB h) (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb))) q \<bind> (\<lambda>p. return_pmf (step (fst (if x then (fst xa, Inl (snd xa)) else (fst xb, Inr (snd xb)))) q (fst p), snd p)))) = Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. BIT_step xa q \<bind> (\<lambda>xb. Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (return_pmf (init, fst (rTS h) init)) qs \<bind> (\<lambda>xc. return_pmf (if x then (fst (step (fst xa) q (fst xb), snd xb), Inl (snd (step (fst xa) q (fst xb), snd xb))) else (fst (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q)), Inr (snd (step (fst xc) q (fst (snd (rTS h) xc q)), snd (snd (rTS h) xc q))))))))
[PROOF STEP]
by(simp_all add: COMB_def COMB_step_def rTS_def map_pmf_def split_def bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) = bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>a. case a of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (qs @ [q]) \<bind> (\<lambda>a. case a of (t1, t2) \<Rightarrow> return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma COMB_no_paid: " \<forall>((free, paid), t)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>((free, paid), t)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
[PROOF STEP]
apply(simp add:  COMB_def COMB_step_def split_def BIT_step_def TS_step_d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set_pmf (case is of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (s, is), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (s, is), b) q))). snd (fst x) = []
[PROOF STEP]
apply(case_tac "is")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. is = Inl a \<Longrightarrow> \<forall>x\<in>set_pmf (case is of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (s, is), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (s, is), b) q))). snd (fst x) = []
 2. \<And>b. is = Inr b \<Longrightarrow> \<forall>x\<in>set_pmf (case is of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (s, is), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (s, is), b) q))). snd (fst x) = []
[PROOF STEP]
by(simp_all add: BIT_step_def TS_step_d_def)