[STATEMENT]
lemma obligation1': assumes "map_pmf con s = Sum_pmf (8 / 10) Da Db"
    shows "config'_rand (COMB h) s qs =
    map_pmf noc (Sum_pmf (8 / 10) (config'_rand BIT Da qs)
                     (config'_rand (embed (rTS h)) Db qs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) s qs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db qs))
[PROOF STEP]
proof (induct qs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand (COMB h) s [] = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da []) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db []))
 2. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) s xs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da xs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db xs)) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) s (xs @ [x]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (xs @ [x])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (xs @ [x])))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand (COMB h) s [] = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da []) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db []))
 2. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) s xs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da xs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db xs)) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) s (xs @ [x]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (xs @ [x])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (xs @ [x])))
[PROOF STEP]
have "s = map_pmf noc (map_pmf con s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = map_pmf noc (map_pmf con s)
[PROOF STEP]
by(simp add: pmf.map_comp noccon)
[PROOF STATE]
proof (state)
this:
s = map_pmf noc (map_pmf con s)

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand (COMB h) s [] = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da []) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db []))
 2. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) s xs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da xs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db xs)) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) s (xs @ [x]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (xs @ [x])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (xs @ [x])))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
s = map_pmf noc (map_pmf con s)

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand (COMB h) s [] = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da []) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db []))
 2. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) s xs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da xs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db xs)) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) s (xs @ [x]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (xs @ [x])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (xs @ [x])))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
map_pmf con s = Sum_pmf (8 / 10) Da Db
[PROOF STEP]
have "\<dots> = map_pmf noc (Sum_pmf (8 / 10) Da Db)"
[PROOF STATE]
proof (prove)
using this:
map_pmf con s = Sum_pmf (8 / 10) Da Db

goal (1 subgoal):
 1. map_pmf noc (map_pmf con s) = map_pmf noc (Sum_pmf (8 / 10) Da Db)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_pmf noc (map_pmf con s) = map_pmf noc (Sum_pmf (8 / 10) Da Db)

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand (COMB h) s [] = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da []) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db []))
 2. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) s xs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da xs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db xs)) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) s (xs @ [x]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (xs @ [x])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (xs @ [x])))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
s = map_pmf noc (Sum_pmf (8 / 10) Da Db)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s = map_pmf noc (Sum_pmf (8 / 10) Da Db)

goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) s [] = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da []) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db []))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand (COMB h) s [] = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da []) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db []))

goal (1 subgoal):
 1. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) s xs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da xs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db xs)) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) s (xs @ [x]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (xs @ [x])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (xs @ [x])))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) s xs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da xs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db xs)) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) s (xs @ [x]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (xs @ [x])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (xs @ [x])))
[PROOF STEP]
case (snoc q qs)
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand (COMB h) s qs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db qs))

goal (1 subgoal):
 1. \<And>x xs. Partial_Cost_Model.config'_rand (COMB h) s xs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da xs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db xs)) \<Longrightarrow> Partial_Cost_Model.config'_rand (COMB h) s (xs @ [x]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (xs @ [x])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (xs @ [x])))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) s (qs @ [q]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (qs @ [q])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (qs @ [q])))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) s (qs @ [q]) = map_pmf noc (Sum_pmf (4 / 5) (Partial_Cost_Model.config'_rand BIT Da (qs @ [q])) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db (qs @ [q])))
[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) s qs) [q] = map_pmf noc (Sum_pmf (4 / 5) (Partial_Cost_Model.config'_rand BIT Da (qs @ [q])) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db (qs @ [q])))
[PROOF STEP]
apply(subst snoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand (COMB h) (map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db qs))) [q] = map_pmf noc (Sum_pmf (4 / 5) (Partial_Cost_Model.config'_rand BIT Da (qs @ [q])) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db (qs @ [q])))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf noc (Sum_pmf (4 / 5) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)) \<bind> (\<lambda>s. snd (COMB h) s q \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) = map_pmf noc (Sum_pmf (4 / 5) (Partial_Cost_Model.config'_rand BIT Da (qs @ [q])) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db (qs @ [q])))
[PROOF STEP]
unfolding Sum_pmf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs))) \<bind> (\<lambda>s. snd (COMB h) s q \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) = map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da (qs @ [q])) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db (qs @ [q]))))
[PROOF STEP]
apply(simp add:
          bind_assoc_pmf bind_return_pmf COMB_def COMB_step_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs))) \<bind> (\<lambda>s. (case snd s of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst s, b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst s, b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) = map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da (qs @ [q])) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db (qs @ [q]))))
[PROOF STEP]
apply(subst config'_rand_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs))) \<bind> (\<lambda>s. (case snd s of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst s, b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst s, b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) = map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db (qs @ [q]))))
[PROOF STEP]
apply(subst config'_rand_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs))) \<bind> (\<lambda>s. (case snd s of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst s, b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst s, b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) = map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) [q])))
[PROOF STEP]
apply(simp only: map_pmf_def[where f=noc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x)) \<bind> (\<lambda>s. (case snd s of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst s, b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst s, b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) [q])) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is')))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) [q])) \<bind> (\<lambda>x. return_pmf (noc x)))
[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> (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) [q])) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf (bernoulli_pmf (4 / 5)) \<Longrightarrow> (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) [q])) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp only: set_pmf_bernoulli UNIV_bool)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {False, True} \<Longrightarrow> (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]) else map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) [q])) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<Longrightarrow> map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is')))) \<bind> (\<lambda>x. return_pmf (noc x))
 2. \<And>x. \<not> x \<Longrightarrow> map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS h) s q) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is')))) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp only: map_pmf_def[where f=Inl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<Longrightarrow> Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>x. return_pmf (Inl x)) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) \<bind> (\<lambda>x. return_pmf (Inl x)) \<bind> (\<lambda>x. return_pmf (noc x))
 2. \<And>x. \<not> x \<Longrightarrow> map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS h) s q) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is')))) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<Longrightarrow> Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>x. (case snd (case x of (s, is) \<Rightarrow> (s, Inl is)) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc (Inl x)), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc (Inl x)), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (case x of (s, is) \<Rightarrow> (s, Inl is))) q a, is'))) = Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>x. BIT_step x q \<bind> (\<lambda>xa. (case xa of (a, is') \<Rightarrow> return_pmf (step (fst x) q a, is')) \<bind> (\<lambda>x. return_pmf (case x of (s, is) \<Rightarrow> (s, Inl is)))))
 2. \<And>x. \<not> x \<Longrightarrow> map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS h) s q) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is')))) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<Longrightarrow> Partial_Cost_Model.config'_rand BIT Da qs = Partial_Cost_Model.config'_rand BIT Da qs
 2. \<And>x xa. \<lbrakk>x; xa \<in> set_pmf (Partial_Cost_Model.config'_rand BIT Da qs)\<rbrakk> \<Longrightarrow> (case snd (case xa of (s, is) \<Rightarrow> (s, Inl is)) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc (Inl xa)), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc (Inl xa)), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (case xa of (s, is) \<Rightarrow> (s, Inl is))) q a, is')) = BIT_step xa q \<bind> (\<lambda>x. (case x of (a, is') \<Rightarrow> return_pmf (step (fst xa) q a, is')) \<bind> (\<lambda>x. return_pmf (case x of (s, is) \<Rightarrow> (s, Inl is))))
 3. \<And>x. \<not> x \<Longrightarrow> map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS h) s q) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is')))) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x; xa \<in> set_pmf (Partial_Cost_Model.config'_rand BIT Da qs)\<rbrakk> \<Longrightarrow> (case snd (case xa of (s, is) \<Rightarrow> (s, Inl is)) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc (Inl xa)), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc (Inl xa)), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (case xa of (s, is) \<Rightarrow> (s, Inl is))) q a, is')) = BIT_step xa q \<bind> (\<lambda>x. (case x of (a, is') \<Rightarrow> return_pmf (step (fst xa) q a, is')) \<bind> (\<lambda>x. return_pmf (case x of (s, is) \<Rightarrow> (s, Inl is))))
 2. \<And>x. \<not> x \<Longrightarrow> map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS h) s q) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is')))) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp add:  split_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x; xa \<in> set_pmf (Partial_Cost_Model.config'_rand BIT Da qs)\<rbrakk> \<Longrightarrow> map_pmf (\<lambda>p. (fst p, Inl (snd p))) (BIT_step xa q) \<bind> (\<lambda>p. return_pmf (step (fst xa) q (fst p), snd p)) = BIT_step xa q \<bind> (\<lambda>x. return_pmf (step (fst xa) q (fst x), snd x) \<bind> (\<lambda>x. return_pmf (fst x, Inl (snd x))))
 2. \<And>x. \<not> x \<Longrightarrow> map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS h) s q) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is')))) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf map_pmf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> x \<Longrightarrow> map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS h) s q) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is')))) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp only: map_pmf_def[where f=Inr])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> x \<Longrightarrow> Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>x. return_pmf (Inr x)) \<bind> (\<lambda>x. (case snd (noc x) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc x), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc x), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (noc x)) q a, is'))) = Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS h) s q) \<bind> (\<lambda>(a, is'). return_pmf (step (fst s) q a, is'))) \<bind> (\<lambda>x. return_pmf (Inr x)) \<bind> (\<lambda>x. return_pmf (noc x))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> x \<Longrightarrow> Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>x. (case snd (case x of (s, is) \<Rightarrow> (s, Inr is)) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc (Inr x)), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc (Inr x)), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (case x of (s, is) \<Rightarrow> (s, Inr is))) q a, is'))) = Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs \<bind> (\<lambda>x. (case snd (rTS h) x q of (a, is') \<Rightarrow> return_pmf (step (fst x) q a, is')) \<bind> (\<lambda>x. return_pmf (case x of (s, is) \<Rightarrow> (s, Inr is))))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<not> x \<Longrightarrow> Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs = Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs
 2. \<And>x xa. \<lbrakk>\<not> x; xa \<in> set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)\<rbrakk> \<Longrightarrow> (case snd (case xa of (s, is) \<Rightarrow> (s, Inr is)) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc (Inr xa)), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc (Inr xa)), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (case xa of (s, is) \<Rightarrow> (s, Inr is))) q a, is')) = (case snd (rTS h) xa q of (a, is') \<Rightarrow> return_pmf (step (fst xa) q a, is')) \<bind> (\<lambda>x. return_pmf (case x of (s, is) \<Rightarrow> (s, Inr is)))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<not> x; xa \<in> set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)\<rbrakk> \<Longrightarrow> (case snd (case xa of (s, is) \<Rightarrow> (s, Inr is)) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc (Inr xa)), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc (Inr xa)), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (step (fst (case xa of (s, is) \<Rightarrow> (s, Inr is))) q a, is')) = (case snd (rTS h) xa q of (a, is') \<Rightarrow> return_pmf (step (fst xa) q a, is')) \<bind> (\<lambda>x. return_pmf (case x of (s, is) \<Rightarrow> (s, Inr is)))
[PROOF STEP]
apply(simp add:  split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<not> x; xa \<in> set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS h) s), \<lambda>s r. return_pmf (snd (rTS h) s r)) Db qs)\<rbrakk> \<Longrightarrow> return_pmf (fst (TS_step_d xa q), Inr (snd (TS_step_d xa q))) \<bind> (\<lambda>p. return_pmf (step (fst xa) q (fst p), snd p)) = return_pmf (step (fst xa) q (fst (snd (rTS h) xa q)), snd (snd (rTS h) xa q)) \<bind> (\<lambda>x. return_pmf (fst x, Inr (snd x)))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf map_pmf_def rTS_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand (COMB h) s (qs @ [q]) = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da (qs @ [q])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) Db (qs @ [q])))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obligation1'':
    shows "config_rand (COMB h) init qs =
    map_pmf noc (Sum_pmf (8 / 10) (config_rand BIT init qs)
                     (config_rand (embed (rTS h)) init qs))"
[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 = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs) (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))
[PROOF STEP]
apply(rule obligation1')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf con (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) = Sum_pmf (8 / 10) (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is)))
[PROOF STEP]
apply(simp add: Sum_pmf_def COMB_def map_pmf_def bind_assoc_pmf bind_return_pmf split_def COMB_init_def del: COMB_init)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. (if x then map_pmf Inl (BIT_init init) else map_pmf Inr (return_pmf (fst (rTS h) init))) \<bind> (\<lambda>x. return_pmf (case x of Inl is \<Rightarrow> Inl (fst (init, x), is) | Inr is \<Rightarrow> Inr (fst (init, x), is)))) = bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) else map_pmf Inr (return_pmf (init, fst (rTS h) init)))
[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> (if x then map_pmf Inl (BIT_init init) else map_pmf Inr (return_pmf (fst (rTS h) init))) \<bind> (\<lambda>x. return_pmf (case x of Inl is \<Rightarrow> Inl (fst (init, x), is) | Inr is \<Rightarrow> Inr (fst (init, x), is))) = (if x then map_pmf Inl (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) else map_pmf Inr (return_pmf (init, fst (rTS h) init)))
[PROOF STEP]
by(auto simp add: split_def map_pmf_def bind_return_pmf bind_assoc_pmf)


[STATEMENT]
lemma obligation1: assumes "map_pmf con s = Sum_pmf (8 / 10) Da Db"
    shows "map_pmf con (config'_rand (COMB []) s qs) =
    Sum_pmf (8 / 10) (config'_rand BIT Da qs)
                     (config'_rand (embed (rTS [])) Db qs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
from obligation1'[OF assms]
[PROOF STATE]
proof (chain)
picking this:
Partial_Cost_Model.config'_rand (COMB ?h) s ?qs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da ?qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS ?h)) Db ?qs))
[PROOF STEP]
have "map_pmf con (config'_rand (COMB []) s qs)
      = map_pmf con (map_pmf noc (Sum_pmf (8 / 10) (config'_rand BIT Da qs)
                     (config'_rand (embed (rTS [])) Db qs)))"
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.config'_rand (COMB ?h) s ?qs = map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da ?qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS ?h)) Db ?qs))

goal (1 subgoal):
 1. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = map_pmf con (map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = map_pmf con (map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)))

goal (1 subgoal):
 1. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = map_pmf con (map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)))

goal (1 subgoal):
 1. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
have "\<dots> = Sum_pmf (8 / 10) (config'_rand BIT Da qs)
                     (config'_rand (embed (rTS [])) Db qs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf con (map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs))) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
apply(simp only: pmf.map_comp connoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf id (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_pmf con (map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs))) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)

goal (1 subgoal):
 1. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)

goal (1 subgoal):
 1. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma BIT_config'_fin: "finite (set_pmf s) \<Longrightarrow> finite (set_pmf (config'_rand BIT s qs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf s) \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand BIT s qs))
[PROOF STEP]
apply(induct qs rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (set_pmf s) \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand BIT s []))
 2. \<And>x xs. \<lbrakk>finite (set_pmf s) \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand BIT s xs)); finite (set_pmf s)\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand BIT s (xs @ [x])))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>finite (set_pmf s) \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand BIT s xs)); finite (set_pmf s)\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand BIT s (xs @ [x])))
[PROOF STEP]
by(simp add: config'_rand_append BIT_step_def)


[STATEMENT]
lemma TS_config'_fin: "finite (set_pmf s) \<Longrightarrow> finite (set_pmf (config'_rand (embed (rTS h)) s qs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf s) \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s qs))
[PROOF STEP]
apply(induct qs rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (set_pmf s) \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s []))
 2. \<And>x xs. \<lbrakk>finite (set_pmf s) \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s xs)); finite (set_pmf s)\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s (xs @ [x])))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>finite (set_pmf s) \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s xs)); finite (set_pmf s)\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) s (xs @ [x])))
[PROOF STEP]
by(simp add: config'_rand_append rTS_def TS_step_d_def)


[STATEMENT]
lemma obligation2: assumes "map_pmf con s = Sum_pmf (8 / 10) Da Db"
    and "finite (set_pmf Da)"
    and "finite (set_pmf Db)"
  shows "T\<^sub>p_on_rand' (COMB []) s qs =
    2 / 10 * T\<^sub>p_on_rand' (embed (rTS [])) Db qs +
    8 / 10 * T\<^sub>p_on_rand' BIT Da qs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs
[PROOF STEP]
proof (induct qs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. T\<^sub>p_on_rand' (COMB []) s [] = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db [] + 8 / 10 * T\<^sub>p_on_rand' BIT Da []
 2. \<And>x xs. T\<^sub>p_on_rand' (COMB []) s xs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db xs + 8 / 10 * T\<^sub>p_on_rand' BIT Da xs \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s (xs @ [x]) = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db (xs @ [x]) + 8 / 10 * T\<^sub>p_on_rand' BIT Da (xs @ [x])
[PROOF STEP]
case (snoc q qs)
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s qs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs

goal (2 subgoals):
 1. T\<^sub>p_on_rand' (COMB []) s [] = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db [] + 8 / 10 * T\<^sub>p_on_rand' BIT Da []
 2. \<And>x xs. T\<^sub>p_on_rand' (COMB []) s xs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db xs + 8 / 10 * T\<^sub>p_on_rand' BIT Da xs \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s (xs @ [x]) = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db (xs @ [x]) + 8 / 10 * T\<^sub>p_on_rand' BIT Da (xs @ [x])
[PROOF STEP]
have P: "T\<^sub>p_on_rand' (COMB []) (config'_rand (COMB []) s qs) [q]
      = 2 / 10 * T\<^sub>p_on_rand' (embed (rTS [])) (config'_rand (embed (rTS [])) Db qs) [q] +
          8 / 10 * T\<^sub>p_on_rand' BIT (config'_rand BIT Da qs) [q]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) (Partial_Cost_Model.config'_rand (COMB []) s qs) [q] = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) [q] + 8 / 10 * T\<^sub>p_on_rand' BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]
[PROOF STEP]
apply(subst obligation1'[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) (map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs))) [q] = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) [q] + 8 / 10 * T\<^sub>p_on_rand' BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]
[PROOF STEP]
unfolding Sum_pmf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) (map_pmf noc (bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)))) [q] = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) [q] + 8 / 10 * T\<^sub>p_on_rand' BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E (map_pmf noc (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs))) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp only: map_pmf_def[where f=noc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E (bernoulli_pmf (4 / 5) \<bind> (\<lambda>b. if b then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x)) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp add: bind_assoc_pmf )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E (bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))))) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(subst E_bernoulli3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. 0 < 4 / 5
 2. 4 / 5 < 1
 3. finite (set_pmf (bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))))))
 4. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 4 / 5 < 1
 2. finite (set_pmf (bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))))))
 3. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (set_pmf (bernoulli_pmf (4 / 5) \<bind> (\<lambda>x. (if x then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))))))
 2. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp add: set_pmf_bernoulli)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x. (x \<longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand BIT Da qs). \<Union>xa\<in>set_pmf (snd (COMB []) (case x of (s, is) \<Rightarrow> (s, Inl is)) q). set_pmf (case xa of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst (case x of (s, is) \<Rightarrow> (s, Inl is))) q a))))) \<and> (\<not> x \<longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs). \<Union>xa\<in>set_pmf (snd (COMB []) (case x of (s, is) \<Rightarrow> (s, Inr is)) q). set_pmf (case xa of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst (case x of (s, is) \<Rightarrow> (s, Inr is))) q a)))))
 2. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp add: BIT_step_def COMB_def COMB_step_def split_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x. (x \<longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand BIT Da qs). {real (t\<^sub>p (fst x) q (if fst (snd x) ! index (snd (snd x)) q then 0 else length (fst x), []))})) \<and> (\<not> x \<longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs). {real (t\<^sub>p (fst x) q (fst (TS_step_d x q)))}))
 2. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(safe)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<Longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand BIT Da qs). {real (t\<^sub>p (fst x) q (if fst (snd x) ! index (snd (snd x)) q then 0 else length (fst x), []))})
 2. \<And>x. \<not> x \<Longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs). {real (t\<^sub>p (fst x) q (fst (TS_step_d x q)))})
 3. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
using BIT_config'_fin[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf (Partial_Cost_Model.config'_rand BIT Da ?qs))

goal (3 subgoals):
 1. \<And>x. x \<Longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand BIT Da qs). {real (t\<^sub>p (fst x) q (if fst (snd x) ! index (snd (snd x)) q then 0 else length (fst x), []))})
 2. \<And>x. \<not> x \<Longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs). {real (t\<^sub>p (fst x) q (fst (TS_step_d x q)))})
 3. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<not> x \<Longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs). {real (t\<^sub>p (fst x) q (fst (TS_step_d x q)))})
 2. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
using TS_config'_fin[OF assms(3)]
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS ?h)) Db ?qs))

goal (2 subgoals):
 1. \<And>x. \<not> x \<Longrightarrow> finite (\<Union>x\<in>set_pmf (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs). {real (t\<^sub>p (fst x) q (fst (TS_step_d x q)))})
 2. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E ((if True then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (4 / 5) + E ((if False then map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) else map_pmf Inr (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * (1 - 4 / 5) = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E (map_pmf Inl (Partial_Cost_Model.config'_rand BIT Da qs) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * 4 / 5 + E (map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) / 5 = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp only: map_pmf_def[where f=Inl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>x. return_pmf (Inl x)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * 4 / 5 + E (map_pmf Inr (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) / 5 = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp only: map_pmf_def[where f=Inr])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>x. return_pmf (Inl x)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) * 4 / 5 + E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>x. return_pmf (Inr x)) \<bind> (\<lambda>x. return_pmf (noc x) \<bind> (\<lambda>s. snd (COMB []) s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a)))))) / 5 = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (snd (rTS []) s q) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf COMB_def COMB_step_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>x. (case snd (case x of (s, is) \<Rightarrow> (s, Inl is)) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc (Inl x)), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc (Inl x)), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst (case x of (s, is) \<Rightarrow> (s, Inl is))) q a))))) * 4 / 5 + E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>x. (case snd (case x of (s, is) \<Rightarrow> (s, Inr is)) of Inl b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inl c)) (BIT_step (fst (noc (Inr x)), b) q) | Inr b \<Rightarrow> map_pmf (\<lambda>((a, b), c). ((a, b), Inr c)) (return_pmf (TS_step_d (fst (noc (Inr x)), b) q))) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst (case x of (s, is) \<Rightarrow> (s, Inr is))) q a))))) / 5 = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. case snd (rTS []) s q of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst s) q a)))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) q a))))) / 5
[PROOF STEP]
apply(simp add: split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>x. map_pmf (\<lambda>p. (fst p, Inl (snd p))) (BIT_step x q) \<bind> (\<lambda>p. return_pmf (real (t\<^sub>p (fst x) q (fst p)))))) * 4 / 5 + E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>x. return_pmf (fst (TS_step_d x q), Inr (snd (TS_step_d x q))) \<bind> (\<lambda>p. return_pmf (real (t\<^sub>p (fst x) q (fst p)))))) / 5 = E (Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) Db qs \<bind> (\<lambda>s. return_pmf (real (t\<^sub>p (fst s) q (fst (snd (rTS []) s q)))))) / 5 + 4 * E (Partial_Cost_Model.config'_rand BIT Da qs \<bind> (\<lambda>s. BIT_step s q \<bind> (\<lambda>p. return_pmf (real (t\<^sub>p (fst s) q (fst p)))))) / 5
[PROOF STEP]
apply(simp add: rTS_def map_pmf_def bind_return_pmf bind_assoc_pmf COMB_def COMB_step_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) (Partial_Cost_Model.config'_rand (COMB []) s qs) [q] = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) [q] + 8 / 10 * T\<^sub>p_on_rand' BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]

goal (2 subgoals):
 1. T\<^sub>p_on_rand' (COMB []) s [] = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db [] + 8 / 10 * T\<^sub>p_on_rand' BIT Da []
 2. \<And>x xs. T\<^sub>p_on_rand' (COMB []) s xs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db xs + 8 / 10 * T\<^sub>p_on_rand' BIT Da xs \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) s (xs @ [x]) = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db (xs @ [x]) + 8 / 10 * T\<^sub>p_on_rand' BIT Da (xs @ [x])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s (qs @ [q]) = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db (qs @ [q]) + 8 / 10 * T\<^sub>p_on_rand' BIT Da (qs @ [q])
[PROOF STEP]
apply(simp only: T_on_rand'_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs + T\<^sub>p_on_rand' (COMB []) (Partial_Cost_Model.config'_rand (COMB []) s qs) [q] = 2 / 10 * (T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) [q]) + 8 / 10 * (T\<^sub>p_on_rand' BIT Da qs + T\<^sub>p_on_rand' BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q])
[PROOF STEP]
apply(subst snoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs + T\<^sub>p_on_rand' (COMB []) (Partial_Cost_Model.config'_rand (COMB []) s qs) [q] = 2 / 10 * (T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) [q]) + 8 / 10 * (T\<^sub>p_on_rand' BIT Da qs + T\<^sub>p_on_rand' BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q])
[PROOF STEP]
apply(subst P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs + (2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) [q] + 8 / 10 * T\<^sub>p_on_rand' BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q]) = 2 / 10 * (T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) [q]) + 8 / 10 * (T\<^sub>p_on_rand' BIT Da qs + T\<^sub>p_on_rand' BIT (Partial_Cost_Model.config'_rand BIT Da qs) [q])
[PROOF STEP]
by algebra
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s (qs @ [q]) = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db (qs @ [q]) + 8 / 10 * T\<^sub>p_on_rand' BIT Da (qs @ [q])

goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s [] = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db [] + 8 / 10 * T\<^sub>p_on_rand' BIT Da []
[PROOF STEP]
qed simp


[STATEMENT]
lemma Combination:
  fixes bit
  assumes "qs \<in> pattern" "a \<noteq> b" "{a, b} = {x, y}" "set qs \<subseteq> {a, b}"
    and "inv_COMB s a [x,y]"
    and TS: "\<And>s h. a \<noteq> b \<Longrightarrow> {a, b} = {x, y} \<Longrightarrow> TS_inv s a [x, y] \<Longrightarrow> set qs \<subseteq> {a, b}
      \<Longrightarrow> qs \<in> pattern \<Longrightarrow>
            TS_inv (config'_rand (embed (rTS h)) s qs) (last qs) [x, y]
          \<and> T\<^sub>p_on_rand' (embed (rTS h)) s qs = ts"
    and BIT: "\<And>s. a \<noteq> b \<Longrightarrow> {a, b} = {x, y} \<Longrightarrow> BIT_inv s a [x, y] \<Longrightarrow> set qs \<subseteq> {a, b}
      \<Longrightarrow> qs \<in> pattern \<Longrightarrow>
            BIT_inv (config'_rand BIT s qs) (last qs) [x, y]
          \<and> T\<^sub>p_on_rand' BIT s qs = bit"
    and OPT_cost: "a \<noteq> b \<Longrightarrow> qs \<in> pattern \<Longrightarrow> real (T\<^sub>p [a, b] qs (OPT2 qs [a, b])) = opt"
    and absch: "qs \<in> pattern \<Longrightarrow> 0.2 * ts + 0.8 * bit \<le> 1.6 * opt"
  shows "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 STATE]
proof (prove)
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 -
[PROOF STATE]
proof (state)
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]
let ?D = "map_pmf con s"
[PROOF STATE]
proof (state)
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]
from assms(5)
[PROOF STATE]
proof (chain)
picking this:
inv_COMB s a [x, y]
[PROOF STEP]
obtain Da Db where Daf: "finite (set_pmf Da)"
      and Dbf: "finite (set_pmf Db)"
      and D: "?D = Sum_pmf 0.8 Da Db"
             and B: "BIT_inv Da a [x,y]" and T: "TS_inv Db a [x,y]"
[PROOF STATE]
proof (prove)
using this:
inv_COMB s a [x, y]

goal (1 subgoal):
 1. (\<And>Da Db. \<lbrakk>finite (set_pmf Da); finite (set_pmf Db); map_pmf con s = Sum_pmf (8 / 10) Da Db; BIT_inv Da a [x, y]; TS_inv Db a [x, y]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding inv_COMB_def
[PROOF STATE]
proof (prove)
using this:
\<exists>Da Db. finite (set_pmf Da) \<and> finite (set_pmf Db) \<and> map_pmf con s = Sum_pmf (8 / 10) Da Db \<and> BIT_inv Da a [x, y] \<and> TS_inv Db a [x, y]

goal (1 subgoal):
 1. (\<And>Da Db. \<lbrakk>finite (set_pmf Da); finite (set_pmf Db); map_pmf con s = Sum_pmf (8 / 10) Da Db; BIT_inv Da a [x, y]; TS_inv Db a [x, y]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set_pmf Da)
finite (set_pmf Db)
map_pmf con s = Sum_pmf (8 / 10) Da Db
BIT_inv Da a [x, y]
TS_inv Db a [x, y]

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]
let ?Da' = "config'_rand BIT Da qs"
[PROOF STATE]
proof (state)
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]
from BIT[OF assms(2,3) B assms(4,1) ]
[PROOF STATE]
proof (chain)
picking this:
BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT Da qs = bit
[PROOF STEP]
have B': "BIT_inv ?Da' (last qs) [x, y]"
    and B_cost: "T\<^sub>p_on_rand' BIT Da qs = bit"
[PROOF STATE]
proof (prove)
using this:
BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' BIT Da qs = bit

goal (1 subgoal):
 1. BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y] &&& T\<^sub>p_on_rand' BIT Da qs = bit
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y]
T\<^sub>p_on_rand' BIT Da qs = bit

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]
let ?Db' = "config'_rand (embed (rTS [])) Db qs"
[PROOF STATE]
proof (state)
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]
(* ?hnlich *)
[PROOF STATE]
proof (state)
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]
from TS[OF assms(2,3) T assms(4,1)]
[PROOF STATE]
proof (chain)
picking this:
TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS ?h)) Db qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS ?h)) Db qs = ts
[PROOF STEP]
have T': "TS_inv ?Db' (last qs) [x, y]"
    and T_cost: "T\<^sub>p_on_rand' (embed (rTS [])) Db qs = ts"
[PROOF STATE]
proof (prove)
using this:
TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS ?h)) Db qs) (last qs) [x, y] \<and> T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS ?h)) Db qs = ts

goal (1 subgoal):
 1. TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y] &&& T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs = ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y]
T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs = ts

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]
have "T\<^sub>p_on_rand' (COMB []) s qs
        = 0.2 * T\<^sub>p_on_rand' (embed (rTS [])) Db qs
            + 0.8 * T\<^sub>p_on_rand' BIT Da qs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
map_pmf con s = Sum_pmf (8 / 10) Da Db

goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) s qs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs
[PROOF STEP]
apply(rule obligation2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (set_pmf Da)
 2. finite (set_pmf Db)
[PROOF STEP]
apply(fact Daf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf Db)
[PROOF STEP]
apply(fact Dbf)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s qs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs

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]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) s qs = 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs

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]
have "\<dots>  \<le> 1.6 * opt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs \<le> 16 / 10 * opt
[PROOF STEP]
by (simp only: B_cost T_cost absch[OF assms(1)])
[PROOF STATE]
proof (state)
this:
2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs \<le> 16 / 10 * opt

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]
also
[PROOF STATE]
proof (state)
this:
2 / 10 * T\<^sub>p_on_rand' (Partial_Cost_Model.embed (rTS [])) Db qs + 8 / 10 * T\<^sub>p_on_rand' BIT Da qs \<le> 16 / 10 * opt

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]
have "\<dots> = 1.6 * T\<^sub>p [a, b] qs (OPT2 qs [a, b])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 16 / 10 * opt = 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b]))
[PROOF STEP]
by (simp add: OPT_cost[OF assms(2,1)])
[PROOF STATE]
proof (state)
this:
16 / 10 * opt = 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [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]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b]))
[PROOF STEP]
have Comb_cost: "T\<^sub>p_on_rand' (COMB []) s qs \<le> 1.6 * T\<^sub>p [a, b] qs (OPT2 qs [a, b])"
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [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]))
[PROOF STEP]
.
[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]))

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]
have Comb_inv: "inv_COMB (config'_rand (COMB []) s qs) (last qs) [x, y]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [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 (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) Da Db \<and> BIT_inv Da (last qs) [x, y] \<and> TS_inv Db (last qs) [x, y]
[PROOF STEP]
apply(rule exI[where x="?Da'"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Db. finite (set_pmf (Partial_Cost_Model.config'_rand BIT Da qs)) \<and> finite (set_pmf Db) \<and> map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) Db \<and> BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y] \<and> TS_inv Db (last qs) [x, y]
[PROOF STEP]
apply(rule exI[where x="?Db'"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf (Partial_Cost_Model.config'_rand BIT Da qs)) \<and> finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)) \<and> map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) \<and> BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y] \<and> TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y]
[PROOF STEP]
apply(safe)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. finite (set_pmf (Partial_Cost_Model.config'_rand BIT Da qs))
 2. finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs))
 3. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
 4. BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y]
 5. TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y]
[PROOF STEP]
apply(rule BIT_config'_fin[OF Daf])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs))
 2. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
 3. BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y]
 4. TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y]
[PROOF STEP]
apply(rule TS_config'_fin[OF Dbf])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. map_pmf con (Partial_Cost_Model.config'_rand (COMB []) s qs) = Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT Da qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs)
 2. BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y]
 3. TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y]
[PROOF STEP]
apply(rule obligation1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. map_pmf con s = Sum_pmf (8 / 10) Da Db
 2. BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y]
 3. TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y]
[PROOF STEP]
apply(fact D)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. BIT_inv (Partial_Cost_Model.config'_rand BIT Da qs) (last qs) [x, y]
 2. TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y]
[PROOF STEP]
apply(fact B')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TS_inv (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) Db qs) (last qs) [x, y]
[PROOF STEP]
apply(fact T')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]

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]
from Comb_cost Comb_inv
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b]))
inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p_on_rand' (COMB []) s qs \<le> 16 / 10 * real (T\<^sub>p [a, b] qs (OPT2 qs [a, b]))
inv_COMB (Partial_Cost_Model.config'_rand (COMB []) s qs) (last qs) [x, y]

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]
by simp
[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