[STATEMENT]
lemma pairwise_property_lemma:
  assumes
relativeorder: "(\<And>init qs. distinct init \<Longrightarrow> qs \<in> {xs. set xs \<subseteq> set init}
    \<Longrightarrow> (\<And>x y. (x,y)\<in> {(x,y). x \<in> set init \<and> y\<in>set init \<and> x\<noteq>y}
                \<Longrightarrow> x \<noteq> y
                \<Longrightarrow> Pbefore_in x y A qs init = Pbefore_in x y A (Lxy qs {x,y}) (Lxy init {x,y})
        ))"
and nopaid: "\<And>xa r. \<forall>z\<in> set_pmf(snd A xa r). snd(fst z) = []"
shows "pairwise A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List_Factoring.pairwise A
[PROOF STEP]
unfolding pairwise_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>init. distinct init \<longrightarrow> (\<forall>qs\<in>{xs. set xs \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) = ALGxy A qs init x y)
[PROOF STEP]
proof (clarify, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
case (1 init rs x y)
[PROOF STATE]
proof (state)
this:
distinct init
set rs \<subseteq> set init
x \<in> set init
y \<in> set init
x < y

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct init
set rs \<subseteq> set init
x \<in> set init
y \<in> set init
x < y
[PROOF STEP]
have xny: "x\<noteq>y"
[PROOF STATE]
proof (prove)
using this:
distinct init
set rs \<subseteq> set init
x \<in> set init
y \<in> set init
x < y

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

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
note dinit=1(1)
[PROOF STATE]
proof (state)
this:
distinct init

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct init
[PROOF STEP]
have dLyx: "distinct (Lxy init {y,x})"
[PROOF STATE]
proof (prove)
using this:
distinct init

goal (1 subgoal):
 1. distinct (Lxy init {y, x})
[PROOF STEP]
by(rule Lxy_distinct)
[PROOF STATE]
proof (state)
this:
distinct (Lxy init {y, x})

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
from dinit
[PROOF STATE]
proof (chain)
picking this:
distinct init
[PROOF STEP]
have dLxy: "distinct (Lxy init {x,y})"
[PROOF STATE]
proof (prove)
using this:
distinct init

goal (1 subgoal):
 1. distinct (Lxy init {x, y})
[PROOF STEP]
by(rule Lxy_distinct)
[PROOF STATE]
proof (state)
this:
distinct (Lxy init {x, y})

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
have setLxy: "set (Lxy init {x, y}) = {x,y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Lxy init {x, y}) = {x, y}
[PROOF STEP]
apply(subst Lxy_set_filter)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y} \<inter> set init = {x, y}
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
distinct init
set rs \<subseteq> set init
x \<in> set init
y \<in> set init
x < y

goal (1 subgoal):
 1. {x, y} \<inter> set init = {x, y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (Lxy init {x, y}) = {x, y}

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
have setLyx: "set (Lxy init {y, x}) = {x,y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Lxy init {y, x}) = {x, y}
[PROOF STEP]
apply(subst Lxy_set_filter)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y, x} \<inter> set init = {x, y}
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
distinct init
set rs \<subseteq> set init
x \<in> set init
y \<in> set init
x < y

goal (1 subgoal):
 1. {y, x} \<inter> set init = {x, y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (Lxy init {y, x}) = {x, y}

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
have lengthLyx:" length  (Lxy init {y, x}) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Lxy init {y, x}) = 2
[PROOF STEP]
using setLyx distinct_card[OF dLyx] xny
[PROOF STATE]
proof (prove)
using this:
set (Lxy init {y, x}) = {x, y}
card (set (Lxy init {y, x})) = length (Lxy init {y, x})
x \<noteq> y

goal (1 subgoal):
 1. length (Lxy init {y, x}) = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (Lxy init {y, x}) = 2

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
have lengthLxy:" length  (Lxy init {x, y}) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Lxy init {x, y}) = 2
[PROOF STEP]
using setLxy distinct_card[OF dLxy] xny
[PROOF STATE]
proof (prove)
using this:
set (Lxy init {x, y}) = {x, y}
card (set (Lxy init {x, y})) = length (Lxy init {x, y})
x \<noteq> y

goal (1 subgoal):
 1. length (Lxy init {x, y}) = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (Lxy init {x, y}) = 2

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
have aee: "{x,y} = {y,x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y} = {y, x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x, y} = {y, x}

goal (1 subgoal):
 1. \<And>init qs a b. \<lbrakk>distinct init; set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) = ALGxy A qs init a b
[PROOF STEP]
from 1(2)
[PROOF STATE]
proof (chain)
picking this:
set rs \<subseteq> set init
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set rs \<subseteq> set init

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = ALGxy A rs init x y
[PROOF STEP]
proof(induct rs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy [] {x, y}) = ALGxy A [] init x y
 2. \<And>xa xs. \<lbrakk>set xs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy xs {x, y}) = ALGxy A xs init x y; set (xs @ [xa]) \<subseteq> set init\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (xs @ [xa]) {x, y}) = ALGxy A (xs @ [xa]) init x y
[PROOF STEP]
case (snoc r rs)
[PROOF STATE]
proof (state)
this:
set rs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = ALGxy A rs init x y
set (rs @ [r]) \<subseteq> set init

goal (2 subgoals):
 1. set [] \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy [] {x, y}) = ALGxy A [] init x y
 2. \<And>xa xs. \<lbrakk>set xs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy xs {x, y}) = ALGxy A xs init x y; set (xs @ [xa]) \<subseteq> set init\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (xs @ [xa]) {x, y}) = ALGxy A (xs @ [xa]) init x y
[PROOF STEP]
have b: "Pbefore_in x y A rs init = Pbefore_in x y A (Lxy rs {x,y}) (Lxy init {x,y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pbefore_in x y A rs init = Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y})
[PROOF STEP]
apply(rule relativeorder)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. distinct init
 2. rs \<in> {xs. set xs \<subseteq> set init}
 3. (x, y) \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}
 4. x \<noteq> y
[PROOF STEP]
using snoc 1 xny
[PROOF STATE]
proof (prove)
using this:
set rs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = ALGxy A rs init x y
set (rs @ [r]) \<subseteq> set init
distinct init
set rs__ \<subseteq> set init
x \<in> set init
y \<in> set init
x < y
x \<noteq> y

goal (4 subgoals):
 1. distinct init
 2. rs \<in> {xs. set xs \<subseteq> set init}
 3. (x, y) \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}
 4. x \<noteq> y
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
Pbefore_in x y A rs init = Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y})

goal (2 subgoals):
 1. set [] \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy [] {x, y}) = ALGxy A [] init x y
 2. \<And>xa xs. \<lbrakk>set xs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy xs {x, y}) = ALGxy A xs init x y; set (xs @ [xa]) \<subseteq> set init\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (xs @ [xa]) {x, y}) = ALGxy A (xs @ [xa]) init x y
[PROOF STEP]
show ?case (is "?L (rs @ [r]) = ?R (rs @ [r])")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
proof(cases "r\<in>{x,y}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r \<in> {x, y}

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
note xyrequest=this
[PROOF STATE]
proof (state)
this:
r \<in> {x, y}

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
let ?expr = "E (Partial_Cost_Model.config'_rand A
        (fst A (Lxy init {x, y}) \<bind>
         (\<lambda>is. return_pmf (Lxy init {x, y}, is)))
        (Lxy rs {x, y}) \<bind>
       (\<lambda>s. snd A s r \<bind>
            (\<lambda>(a, is').
                return_pmf
                 (real (t\<^sub>p (fst s) r a)))))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
let ?expr2 = "ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
from xyrequest
[PROOF STATE]
proof (chain)
picking this:
r \<in> {x, y}
[PROOF STEP]
have "?L (rs @ [r]) = ?L rs + ?expr"
[PROOF STATE]
proof (prove)
using this:
r \<in> {x, y}

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))))
[PROOF STEP]
by(simp add: Lxy_snoc T_on_rand'_append)
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))))

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))))

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
have "\<dots> = ?L rs + ?expr2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
proof(cases "r=x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r = x

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
let ?projS ="config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
let ?S = "(config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
have "?projS \<bind> (\<lambda>s. snd A s r
                           \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))
              = ?projS \<bind> (\<lambda>s. return_pmf (real (index (fst s) r)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r)))
[PROOF STEP]
proof (rule bind_pmf_cong, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> snd A xa r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst xa) r a))) = return_pmf (real (index (fst xa) r))
[PROOF STEP]
case (2 z)
[PROOF STATE]
proof (state)
this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}))

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> snd A xa r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst xa) r a))) = return_pmf (real (index (fst xa) r))
[PROOF STEP]
have "snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. snd A z r = snd A z r
 2. \<And>x. x \<in> set_pmf (snd A z r) \<Longrightarrow> (case x of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf (snd A z r) \<Longrightarrow> (case x of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))
[PROOF STEP]
using nopaid[of z r]
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>set_pmf (snd A z r). snd (fst z) = []

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf (snd A z r) \<Longrightarrow> (case x of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))
[PROOF STEP]
by(simp add: split_def t\<^sub>p_def)
[PROOF STATE]
proof (state)
this:
snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> snd A xa r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst xa) r a))) = return_pmf (real (index (fst xa) r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))

goal (1 subgoal):
 1. snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))
[PROOF STEP]
by(simp add: bind_return_pmf)
[PROOF STATE]
proof (state)
this:
snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))

goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r)))

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r)))

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
have "\<dots> = map_pmf (%b. (if b then 0::real else 1)) (Pbefore_in x y A (Lxy rs {x,y}) (Lxy init {x,y}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y}))
[PROOF STEP]
unfolding Pbefore_in_def map_pmf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)) \<bind> (\<lambda>x. return_pmf (if x then 0 else 1))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>xa. return_pmf (if x < y in fst xa then 0 else 1))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 0 else 1)
[PROOF STEP]
apply(simp add: aee)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 0 else 1)
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 0 else 1)
[PROOF STEP]
case (1 z)
[PROOF STATE]
proof (state)
this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}))

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 0 else 1)
[PROOF STEP]
have " (if x < y in fst z then 0 else 1) = (index (fst z) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x < y in fst z then 0 else 1) = index (fst z) x
[PROOF STEP]
apply(rule before_in_index1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. set (fst z) = {x, y}
 2. length (fst z) = 2
 3. x \<noteq> y
[PROOF STEP]
using 1 config_rand_set setLxy
[PROOF STATE]
proof (prove)
using this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}))
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). set (fst x) = set ?init
set (Lxy init {x, y}) = {x, y}

goal (3 subgoals):
 1. set (fst z) = {x, y}
 2. length (fst z) = 2
 3. x \<noteq> y
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (fst z) = 2
 2. x \<noteq> y
[PROOF STEP]
using 1 config_rand_length lengthLxy
[PROOF STATE]
proof (prove)
using this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}))
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). length (fst x) = length ?init
length (Lxy init {x, y}) = 2

goal (2 subgoals):
 1. length (fst z) = 2
 2. x \<noteq> y
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
using xny
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if x < y in fst z then 0 else 1) = index (fst z) x

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 0 else 1)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
r = x
(if x < y in fst z then 0 else 1) = index (fst z) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r = x
(if x < y in fst z then 0 else 1) = index (fst z) x

goal (1 subgoal):
 1. return_pmf (real (index (fst z) r)) = return_pmf (if x < y in fst z then 0 else 1)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
return_pmf (real (index (fst z) r)) = return_pmf (if x < y in fst z then 0 else 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y}))

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y}))

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
have "\<dots> = map_pmf (%b. (if b then 0::real else 1)) (Pbefore_in x y A rs init)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y})) = map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A rs init)
[PROOF STEP]
by(simp add: b)
[PROOF STATE]
proof (state)
this:
map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y})) = map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A rs init)

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y})) = map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A rs init)

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
have "\<dots> = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A rs init) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
apply(simp add: Pbefore_in_def map_pmf_comp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>xa. if x < y in fst xa then 0 else 1) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
proof (rule map_pmf_cong, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs = Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs) \<Longrightarrow> (if x < y in fst xa then 0 else 1) = real (if y < x in fst xa then 1 else 0)
[PROOF STEP]
case (2 z)
[PROOF STATE]
proof (state)
this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs = Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs) \<Longrightarrow> (if x < y in fst xa then 0 else 1) = real (if y < x in fst xa then 1 else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
have set_z: "set (fst z) = set init"
[PROOF STATE]
proof (prove)
using this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)

goal (1 subgoal):
 1. set (fst z) = set init
[PROOF STEP]
using config_rand_set
[PROOF STATE]
proof (prove)
using this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). set (fst x) = set ?init

goal (1 subgoal):
 1. set (fst z) = set init
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
set (fst z) = set init

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs = Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs) \<Longrightarrow> (if x < y in fst xa then 0 else 1) = real (if y < x in fst xa then 1 else 0)
[PROOF STEP]
have "(\<not> x < y in fst z) = y < x in fst z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> x < y in fst z) = y < x in fst z
[PROOF STEP]
apply(subst not_before_in)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. x \<in> set (fst z)
 2. y \<in> set (fst z)
 3. (y < x in fst z \<or> x = y) = y < x in fst z
[PROOF STEP]
using set_z 1(3,4) xny
[PROOF STATE]
proof (prove)
using this:
set (fst z) = set init
x \<in> set init
y \<in> set init
x \<noteq> y

goal (3 subgoals):
 1. x \<in> set (fst z)
 2. y \<in> set (fst z)
 3. (y < x in fst z \<or> x = y) = y < x in fst z
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
(\<not> x < y in fst z) = y < x in fst z

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs = Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs) \<Longrightarrow> (if x < y in fst xa then 0 else 1) = real (if y < x in fst xa then 1 else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<not> x < y in fst z) = y < x in fst z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<not> x < y in fst z) = y < x in fst z

goal (1 subgoal):
 1. (if x < y in fst z then 0 else 1) = real (if y < x in fst z then 1 else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if x < y in fst z then 0 else 1) = real (if y < x in fst z then 1 else 0)

goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs = Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
map_pmf (\<lambda>b. if b then 0 else 1) (Pbefore_in x y A rs init) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
have a: "?projS \<bind> (\<lambda>s. snd A s x
                           \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a))))
                  = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) ?S"
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)

goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s x \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a)))) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
r = x

goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s x \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a)))) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s x \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a)))) = map_pmf (\<lambda>xa. real (if y < x in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)

goal (2 subgoals):
 1. r = x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
 2. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
r = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = x

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
apply(simp add: ALG'_refl nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = x \<Longrightarrow> E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s x \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a))))) = ALG' A (rs @ [x]) init (length rs) y
[PROOF STEP]
unfolding ALG'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = x \<Longrightarrow> E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s x \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) x a))))) = E (map_pmf (\<lambda>xa. real (ALG y (rs @ [x]) (length rs) xa)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take (length rs) (rs @ [x]))))
[PROOF STEP]
by(simp add: a)
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r \<noteq> x

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
with xyrequest
[PROOF STATE]
proof (chain)
picking this:
r \<in> {x, y}
r \<noteq> x
[PROOF STEP]
have request: "r=y"
[PROOF STATE]
proof (prove)
using this:
r \<in> {x, y}
r \<noteq> x

goal (1 subgoal):
 1. r = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r = y

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
let ?projS ="config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
let ?S = "(config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
have "?projS \<bind> (\<lambda>s. snd A s r
                           \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))
              = ?projS \<bind> (\<lambda>s. return_pmf (real (index (fst s) r)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r)))
[PROOF STEP]
proof (rule bind_pmf_cong, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> snd A xa r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst xa) r a))) = return_pmf (real (index (fst xa) r))
[PROOF STEP]
case (2 z)
[PROOF STATE]
proof (state)
this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}))

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> snd A xa r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst xa) r a))) = return_pmf (real (index (fst xa) r))
[PROOF STEP]
have "snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. snd A z r = snd A z r
 2. \<And>x. x \<in> set_pmf (snd A z r) \<Longrightarrow> (case x of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf (snd A z r) \<Longrightarrow> (case x of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))
[PROOF STEP]
using nopaid[of z r]
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>set_pmf (snd A z r). snd (fst z) = []

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf (snd A z r) \<Longrightarrow> (case x of (a, is') \<Rightarrow> return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))
[PROOF STEP]
by(simp add: split_def t\<^sub>p_def)
[PROOF STATE]
proof (state)
this:
snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))

goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> snd A xa r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst xa) r a))) = return_pmf (real (index (fst xa) r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = snd A z r \<bind> (\<lambda>x. return_pmf (real (index (fst z) r)))

goal (1 subgoal):
 1. snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))
[PROOF STEP]
by(simp add: bind_return_pmf)
[PROOF STATE]
proof (state)
this:
snd A z r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst z) r a))) = return_pmf (real (index (fst z) r))

goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r)))

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r)))

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
have "\<dots> = map_pmf (%b. (if b then 1::real else 0)) (Pbefore_in x y A (Lxy rs {x,y}) (Lxy init {x,y}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y}))
[PROOF STEP]
unfolding Pbefore_in_def map_pmf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)) \<bind> (\<lambda>x. return_pmf (if x then 1 else 0))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>xa. return_pmf (if x < y in fst xa then 1 else 0))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 1 else 0)
[PROOF STEP]
apply(simp add: aee)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 1 else 0)
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 1 else 0)
[PROOF STEP]
case (1 z)
[PROOF STATE]
proof (state)
this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}))

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 1 else 0)
[PROOF STEP]
have " (if x < y in fst z then 1 else 0) = (index (fst z) y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x < y in fst z then 1 else 0) = index (fst z) y
[PROOF STEP]
apply(rule before_in_index2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. set (fst z) = {x, y}
 2. length (fst z) = 2
 3. x \<noteq> y
[PROOF STEP]
using 1 config_rand_set setLxy
[PROOF STATE]
proof (prove)
using this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}))
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). set (fst x) = set ?init
set (Lxy init {x, y}) = {x, y}

goal (3 subgoals):
 1. set (fst z) = {x, y}
 2. length (fst z) = 2
 3. x \<noteq> y
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (fst z) = 2
 2. x \<noteq> y
[PROOF STEP]
using 1 config_rand_length lengthLxy
[PROOF STATE]
proof (prove)
using this:
z \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}))
\<forall>x\<in>set_pmf (Partial_Cost_Model.config'_rand ?A (fst ?A ?init \<bind> (\<lambda>is. return_pmf (?init, is))) ?qs). length (fst x) = length ?init
length (Lxy init {x, y}) = 2

goal (2 subgoals):
 1. length (fst z) = 2
 2. x \<noteq> y
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
using xny
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if x < y in fst z then 1 else 0) = index (fst z) y

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})) \<Longrightarrow> return_pmf (real (index (fst xa) r)) = return_pmf (if x < y in fst xa then 1 else 0)
[PROOF STEP]
with request
[PROOF STATE]
proof (chain)
picking this:
r = y
(if x < y in fst z then 1 else 0) = index (fst z) y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r = y
(if x < y in fst z then 1 else 0) = index (fst z) y

goal (1 subgoal):
 1. return_pmf (real (index (fst z) r)) = return_pmf (if x < y in fst z then 1 else 0)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
return_pmf (real (index (fst z) r)) = return_pmf (if x < y in fst z then 1 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y}))

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. return_pmf (real (index (fst s) r))) = map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y}))

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
have "\<dots> = map_pmf (%b. (if b then 1::real else 0)) (Pbefore_in x y A rs init)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y})) = map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A rs init)
[PROOF STEP]
by(simp add: b)
[PROOF STATE]
proof (state)
this:
map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y})) = map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A rs init)

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A (Lxy rs {x, y}) (Lxy init {x, y})) = map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A rs init)

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
have "\<dots> = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A rs init) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
apply(simp add: Pbefore_in_def map_pmf_comp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>xa. if x < y in fst xa then 1 else 0) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
apply (rule map_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs = Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs
 2. \<And>xa. xa \<in> set_pmf (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs) \<Longrightarrow> (if x < y in fst xa then 1 else 0) = real (if x < y in fst xa then 1 else 0)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
map_pmf (\<lambda>b. if b then 1 else 0) (Pbefore_in x y A rs init) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
have a: "?projS \<bind> (\<lambda>s. snd A s y
                           \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a))))
                  = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) ?S"
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)

goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s y \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a)))) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
using request
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a)))) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
r = y

goal (1 subgoal):
 1. Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s y \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a)))) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s y \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a)))) = map_pmf (\<lambda>xa. real (if x < y in fst xa then 1 else 0)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) rs)

goal (1 subgoal):
 1. r \<noteq> x \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
from request
[PROOF STATE]
proof (chain)
picking this:
r = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = y

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
apply(simp add: ALG'_refl nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = y \<Longrightarrow> E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s y \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a))))) = ALG' A (rs @ [y]) init (length rs) x
[PROOF STEP]
unfolding ALG'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = y \<Longrightarrow> E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s y \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) y a))))) = E (map_pmf (\<lambda>xa. real (ALG x (rs @ [y]) (length rs) xa)) (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take (length rs) (rs @ [y]))))
[PROOF STEP]
by(simp add: a)
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + E (Partial_Cost_Model.config'_rand A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) \<bind> (\<lambda>s. snd A s r \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) r a))))) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
have "\<dots> = ?R rs + ?expr2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x) = ALGxy A rs init x y + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
set rs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = ALGxy A rs init x y
set (rs @ [r]) \<subseteq> set init

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x) = ALGxy A rs init x y + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x) = ALGxy A rs init x y + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x) = ALGxy A rs init x y + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x)

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
r \<in> {x, y}
[PROOF STEP]
have "\<dots> = ?R (rs@[r])"
[PROOF STATE]
proof (prove)
using this:
r \<in> {x, y}

goal (1 subgoal):
 1. ALGxy A rs init x y + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
apply(subst ALGxy_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> {x, y} \<Longrightarrow> ALGxy A rs init x y + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x) = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
ALGxy A rs init x y + (ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x) = ALGxy A (rs @ [r]) init x y

goal (2 subgoals):
 1. r \<in> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
 2. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y

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

goal (1 subgoal):
 1. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r \<notin> {x, y}

goal (1 subgoal):
 1. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<notin> {x, y}
[PROOF STEP]
have "?L (rs @ [r]) = ?L rs"
[PROOF STATE]
proof (prove)
using this:
r \<notin> {x, y}

goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
[PROOF STEP]
apply(subst Lxy_snoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (if r \<in> {x, y} then Lxy rs {x, y} @ [r] else Lxy rs {x, y}) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})

goal (1 subgoal):
 1. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y})

goal (1 subgoal):
 1. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
have "\<dots> = ?R rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = ALGxy A rs init x y
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
set rs \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = ALGxy A rs init x y
set (rs @ [r]) \<subseteq> set init

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

goal (1 subgoal):
 1. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = ALGxy A rs init x y

goal (1 subgoal):
 1. r \<notin> {x, y} \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
have "\<dots> = ?R (rs @ [r])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy A rs init x y = ALGxy A (rs @ [r]) init x y
[PROOF STEP]
apply(subst ALGxy_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ALGxy A rs init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
r \<notin> {x, y}

goal (1 subgoal):
 1. ALGxy A rs init x y = ALGxy A rs init x y + (if r \<in> {y, x} then ALG' A (rs @ [r]) init (length rs) y + ALG' A (rs @ [r]) init (length rs) x else 0)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
ALGxy A rs init x y = ALGxy A (rs @ [r]) init x y

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy (rs @ [r]) {x, y}) = ALGxy A (rs @ [r]) init x y

goal (1 subgoal):
 1. set [] \<subseteq> set init \<Longrightarrow> T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy [] {x, y}) = ALGxy A [] init x y
[PROOF STEP]
qed (simp add: ALGxy_def)
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' A (fst A (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy rs {x, y}) = ALGxy A rs init x y

goal:
No subgoals!
[PROOF STEP]
qed