[STATEMENT]
lemma mrconcNone: "applied_rule_rev C x p = None \<Longrightarrow>
                                applied_rule_rev C x (b#p) = applied_rule_rev C x [b]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x p = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # p) = applied_rule_rev C x [b]
[PROOF STEP]
proof (induct p rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. applied_rule_rev C x [] = \<bottom> \<Longrightarrow> applied_rule_rev C x [b] = applied_rule_rev C x [b]
 2. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # xs) = applied_rule_rev C x [b]; applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = applied_rule_rev C x [b]
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x [] = \<bottom>

goal (2 subgoals):
 1. applied_rule_rev C x [] = \<bottom> \<Longrightarrow> applied_rule_rev C x [b] = applied_rule_rev C x [b]
 2. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # xs) = applied_rule_rev C x [b]; applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = applied_rule_rev C x [b]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x [b] = applied_rule_rev C x [b]
[PROOF STEP]
by (simp add: applied_rule_rev_def)
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x [b] = applied_rule_rev C x [b]

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # xs) = applied_rule_rev C x [b]; applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = applied_rule_rev C x [b]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # xs) = applied_rule_rev C x [b]; applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = applied_rule_rev C x [b]
[PROOF STEP]
case (snoc ys y)
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]
applied_rule_rev C x (y @ [ys]) = \<bottom>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>applied_rule_rev C x xs = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # xs) = applied_rule_rev C x [b]; applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # xs @ [xa]) = applied_rule_rev C x [b]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]
applied_rule_rev C x (y @ [ys]) = \<bottom>

goal (1 subgoal):
 1. applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
proof (cases "x \<in> dom (C ys)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]; applied_rule_rev C x (y @ [ys]) = \<bottom>; x \<in> dom (C ys)\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
 2. \<lbrakk>applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]; applied_rule_rev C x (y @ [ys]) = \<bottom>; x \<notin> dom (C ys)\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> dom (C ys)

goal (2 subgoals):
 1. \<lbrakk>applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]; applied_rule_rev C x (y @ [ys]) = \<bottom>; x \<in> dom (C ys)\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
 2. \<lbrakk>applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]; applied_rule_rev C x (y @ [ys]) = \<bottom>; x \<notin> dom (C ys)\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
using True snoc
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (C ys)
applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]
applied_rule_rev C x (y @ [ys]) = \<bottom>

goal (1 subgoal):
 1. applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
by (auto simp: applied_rule_rev_def)
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]

goal (1 subgoal):
 1. \<lbrakk>applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]; applied_rule_rev C x (y @ [ys]) = \<bottom>; x \<notin> dom (C ys)\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]; applied_rule_rev C x (y @ [ys]) = \<bottom>; x \<notin> dom (C ys)\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> dom (C ys)

goal (1 subgoal):
 1. \<lbrakk>applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]; applied_rule_rev C x (y @ [ys]) = \<bottom>; x \<notin> dom (C ys)\<rbrakk> \<Longrightarrow> applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
using False snoc
[PROOF STATE]
proof (prove)
using this:
x \<notin> dom (C ys)
applied_rule_rev C x y = \<bottom> \<Longrightarrow> applied_rule_rev C x (b # y) = applied_rule_rev C x [b]
applied_rule_rev C x (y @ [ys]) = \<bottom>

goal (1 subgoal):
 1. applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]
[PROOF STEP]
by (auto simp: applied_rule_rev_def)
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
applied_rule_rev C x (b # y @ [ys]) = applied_rule_rev C x [b]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mreq_endNone: "\<lbrakk>applied_rule_rev C x b = None; applied_rule_rev C x c = None\<rbrakk> \<Longrightarrow>
     applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>applied_rule_rev C x b = \<bottom>; applied_rule_rev C x c = \<bottom>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (a # b) = applied_rule_rev C x (a # c)
[PROOF STEP]
by (metis mrconcNone)


[STATEMENT]
lemma mreq_end2: "applied_rule_rev C x b = applied_rule_rev C x c \<Longrightarrow>
     applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x b = applied_rule_rev C x c \<Longrightarrow> applied_rule_rev C x (a # b) = applied_rule_rev C x (a # c)
[PROOF STEP]
apply (case_tac "applied_rule_rev C x b = None")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>applied_rule_rev C x b = applied_rule_rev C x c; applied_rule_rev C x b = \<bottom>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (a # b) = applied_rule_rev C x (a # c)
 2. \<lbrakk>applied_rule_rev C x b = applied_rule_rev C x c; applied_rule_rev C x b \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> applied_rule_rev C x (a # b) = applied_rule_rev C x (a # c)
[PROOF STEP]
apply (auto intro: mreq_end mreq_endNone)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mreq_end3: "applied_rule_rev C x p \<noteq> None \<Longrightarrow>
                  applied_rule_rev C x (b # p) = applied_rule_rev C x (p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev C x p \<noteq> \<bottom> \<Longrightarrow> applied_rule_rev C x (b # p) = applied_rule_rev C x p
[PROOF STEP]
by (auto simp: mrconc)


[STATEMENT]
lemma mrNoneMT: "\<lbrakk>r \<in> set p; applied_rule_rev C x p = None\<rbrakk> \<Longrightarrow>
                              x \<notin> dom (C r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> set p; applied_rule_rev C x p = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
proof (induct p rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>r \<in> set []; applied_rule_rev C x [] = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
 2. \<And>xa xs. \<lbrakk>\<lbrakk>r \<in> set xs; applied_rule_rev C x xs = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (xs @ [xa]); applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
r \<in> set []
applied_rule_rev C x [] = \<bottom>

goal (2 subgoals):
 1. \<lbrakk>r \<in> set []; applied_rule_rev C x [] = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
 2. \<And>xa xs. \<lbrakk>\<lbrakk>r \<in> set xs; applied_rule_rev C x xs = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (xs @ [xa]); applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom (C r)
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
using this:
r \<in> set []
applied_rule_rev C x [] = \<bottom>

goal (1 subgoal):
 1. x \<notin> dom (C r)
[PROOF STEP]
by (simp add: applied_rule_rev_def)
[PROOF STATE]
proof (state)
this:
x \<notin> dom (C r)

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>r \<in> set xs; applied_rule_rev C x xs = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (xs @ [xa]); applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>r \<in> set xs; applied_rule_rev C x xs = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (xs @ [xa]); applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
case (snoc y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
r \<in> set (ys @ [y])
applied_rule_rev C x (ys @ [y]) = \<bottom>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>r \<in> set xs; applied_rule_rev C x xs = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (xs @ [xa]); applied_rule_rev C x (xs @ [xa]) = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom (C r)
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
r \<in> set (ys @ [y])
applied_rule_rev C x (ys @ [y]) = \<bottom>

goal (1 subgoal):
 1. x \<notin> dom (C r)
[PROOF STEP]
proof (cases "r \<in> set ys")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (ys @ [y]); applied_rule_rev C x (ys @ [y]) = \<bottom>; r \<in> set ys\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
 2. \<lbrakk>\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (ys @ [y]); applied_rule_rev C x (ys @ [y]) = \<bottom>; r \<notin> set ys\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r \<in> set ys

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (ys @ [y]); applied_rule_rev C x (ys @ [y]) = \<bottom>; r \<in> set ys\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
 2. \<lbrakk>\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (ys @ [y]); applied_rule_rev C x (ys @ [y]) = \<bottom>; r \<notin> set ys\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom (C r)
[PROOF STEP]
using snoc True
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
r \<in> set (ys @ [y])
applied_rule_rev C x (ys @ [y]) = \<bottom>
r \<in> set ys

goal (1 subgoal):
 1. x \<notin> dom (C r)
[PROOF STEP]
by (simp add: applied_rule_rev_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
x \<notin> dom (C r)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (ys @ [y]); applied_rule_rev C x (ys @ [y]) = \<bottom>; r \<notin> set ys\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (ys @ [y]); applied_rule_rev C x (ys @ [y]) = \<bottom>; r \<notin> set ys\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r \<notin> set ys

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r); r \<in> set (ys @ [y]); applied_rule_rev C x (ys @ [y]) = \<bottom>; r \<notin> set ys\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom (C r)
[PROOF STEP]
using snoc False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>r \<in> set ys; applied_rule_rev C x ys = \<bottom>\<rbrakk> \<Longrightarrow> x \<notin> dom (C r)
r \<in> set (ys @ [y])
applied_rule_rev C x (ys @ [y]) = \<bottom>
r \<notin> set ys

goal (1 subgoal):
 1. x \<notin> dom (C r)
[PROOF STEP]
by (simp add: applied_rule_rev_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
x \<notin> dom (C r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<notin> dom (C r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list2listNMT:  "x \<noteq> [] \<Longrightarrow> map sem x \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> [] \<Longrightarrow> map sem x \<noteq> []
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> []; x = []\<rbrakk> \<Longrightarrow> map sem x \<noteq> []
 2. \<And>a list. \<lbrakk>x \<noteq> []; x = a # list\<rbrakk> \<Longrightarrow> map sem x \<noteq> []
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma two_conc: "(prod_list x (y#ys) p r d) = ((r o_f ((p x y) o d))#(prod_list x ys p r d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<Otimes>\<^sub>L y # ys) p r d = (r o\<^sub>f (p x y \<circ> d)) # (x \<Otimes>\<^sub>L ys) p r d
[PROOF STEP]
by simp


[STATEMENT]
lemma is_distr_orD: "is_distr (\<Otimes>\<^sub>\<or>\<^sub>D) d r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_distr (\<Otimes>\<^sub>\<or>\<^sub>D) d r
[PROOF STEP]
apply (simp add: is_distr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>N P1 P2. d o\<^sub>f (N \<Otimes>\<^sub>\<or>\<^sub>D P1 \<Oplus> P2 \<circ> r) = (d o\<^sub>f (N \<Otimes>\<^sub>\<or>\<^sub>D P1 \<circ> r)) \<Oplus> (d o\<^sub>f (N \<Otimes>\<^sub>\<or>\<^sub>D P2 \<circ> r))
[PROOF STEP]
apply (rule allI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N P1 P2. d o\<^sub>f (N \<Otimes>\<^sub>\<or>\<^sub>D P1 \<Oplus> P2 \<circ> r) = (d o\<^sub>f (N \<Otimes>\<^sub>\<or>\<^sub>D P1 \<circ> r)) \<Oplus> (d o\<^sub>f (N \<Otimes>\<^sub>\<or>\<^sub>D P2 \<circ> r))
[PROOF STEP]
apply (rule distr_orD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N P1 P2. P1 \<Oplus> P2 = P1 \<Oplus> P2
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_distr_2: "is_distr (\<Otimes>\<^sub>2) d r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_distr (\<Otimes>\<^sub>2) d r
[PROOF STEP]
apply (simp add: is_distr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>N P1 P2. d o\<^sub>f (N \<Otimes>\<^sub>2 P1 \<Oplus> P2 \<circ> r) = (d o\<^sub>f (N \<Otimes>\<^sub>2 P1 \<circ> r)) \<Oplus> (d o\<^sub>f (N \<Otimes>\<^sub>2 P2 \<circ> r))
[PROOF STEP]
apply (rule allI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N P1 P2. d o\<^sub>f (N \<Otimes>\<^sub>2 P1 \<Oplus> P2 \<circ> r) = (d o\<^sub>f (N \<Otimes>\<^sub>2 P1 \<circ> r)) \<Oplus> (d o\<^sub>f (N \<Otimes>\<^sub>2 P2 \<circ> r))
[PROOF STEP]
apply (rule distr_or2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N P1 P2. P1 \<Oplus> P2 = P1 \<Oplus> P2
[PROOF STEP]
by simp


[STATEMENT]
lemma is_strict_2: "is_strict (\<Otimes>\<^sub>2) d r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_strict (\<Otimes>\<^sub>2) d r
[PROOF STEP]
apply (simp only: is_strict_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P1. d o\<^sub>f (P1 \<Otimes>\<^sub>2 \<emptyset> \<circ> r) = \<emptyset>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d o\<^sub>f (\<emptyset> \<circ> r) = \<emptyset>
[PROOF STEP]
apply (simp add: policy_range_comp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma domStart: "t \<in> dom p1 \<Longrightarrow> (p1 \<Oplus> p2) t = p1 t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> dom p1 \<Longrightarrow> (p1 \<Oplus> p2) t = p1 t
[PROOF STEP]
apply (simp add: map_add_dom_app_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma notDom: "x \<in> dom A \<Longrightarrow> \<not> A x = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> dom A \<Longrightarrow> A x \<noteq> \<bottom>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Norm_Distr_1:  "((r o_f (((\<Otimes>\<^sub>1) P1 (list2policy P2)) o d)) x =
                                                   ((list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>1) r d)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
proof (induct P2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>1) r d) x
 2. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>1) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>1) r d) x
 2. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>1) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
by (simp add: policy_range_comp_def  list2policy_def)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>1) r d) x

goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>1) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>1) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x

goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>1) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
proof (cases "x \<in> dom (r o_f ((P1 \<Otimes>\<^sub>1 p) \<circ> d))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x; x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
 2. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))

goal (2 subgoals):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x; x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
 2. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
by (auto simp: list2policy_def policy_range_comp_def  prod_1_def
          split: option.splits decision.splits prod.splits)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x

goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))

goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
using Cons False
[PROOF STATE]
proof (prove)
using this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>1) r d) x
x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>1 p \<circ> d))

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x
[PROOF STEP]
by (auto simp: list2policy_def policy_range_comp_def  map_add_dom_app_simps(3) prod_1_def
          split: option.splits decision.splits prod.splits)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>1 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>1) r d) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Norm_Distr_2: "((r o_f (((\<Otimes>\<^sub>2) P1 (list2policy P2)) o d)) x =
                               ((list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>2) r d)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
proof (induct P2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>2) r d) x
 2. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>2) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>2) r d) x
 2. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>2) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
by (simp add: policy_range_comp_def  list2policy_def)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>2) r d) x

goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>2) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>2) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x

goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>2) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
proof (cases "x \<in> dom (r o_f ((P1 \<Otimes>\<^sub>2 p) \<circ> d))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x; x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
 2. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))

goal (2 subgoals):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x; x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
 2. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
by (auto simp: list2policy_def prod_2_def policy_range_comp_def
          split: option.splits decision.splits prod.splits)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x

goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))

goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
using Cons False
[PROOF STATE]
proof (prove)
using this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>2) r d) x
x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>2 p \<circ> d))

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x
[PROOF STEP]
by (auto simp:  policy_range_comp_def  list2policy_def map_add_dom_app_simps(3) prod_2_def
          split: option.splits decision.splits prod.splits)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>2 list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>2) r d) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Norm_Distr_A: "((r o_f (((\<Otimes>\<^sub>\<or>\<^sub>A) P1 (list2policy P2)) o d)) x =
                                                 ((list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
proof (induct P2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
 2. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
 2. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
by (simp add: policy_range_comp_def  list2policy_def)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x

goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x

goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
proof (cases "x \<in> dom (r o_f ((P1 \<Otimes>\<^sub>\<or>\<^sub>A p) \<circ> d))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x; x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
 2. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))

goal (2 subgoals):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x; x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
 2. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
by (auto simp: policy_range_comp_def  list2policy_def prod_orA_def
          split: option.splits decision.splits prod.splits)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x

goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))

goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
using Cons False
[PROOF STATE]
proof (prove)
using this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A p \<circ> d))

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x
[PROOF STEP]
by (auto simp: policy_range_comp_def  list2policy_def map_add_dom_app_simps(3) prod_orA_def
          split: option.splits decision.splits prod.splits)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>A list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>A) r d) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Norm_Distr_D: "((r o_f (((\<Otimes>\<^sub>\<or>\<^sub>D) P1 (list2policy P2)) o d)) x =
                                                  ((list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
proof (induct P2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
 2. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
 2. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
by (simp add: policy_range_comp_def  list2policy_def)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy [] \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L []) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x

goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x

goal (1 subgoal):
 1. \<And>a P2. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy P2 \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (a # P2) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L a # P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
proof (cases "x \<in> dom (r o_f ((P1 \<Otimes>\<^sub>\<or>\<^sub>D p) \<circ> d))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x; x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
 2. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))

goal (2 subgoals):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x; x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
 2. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
by (auto simp: policy_range_comp_def  list2policy_def prod_orD_def
          split: option.splits decision.splits prod.splits)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x

goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))

goal (1 subgoal):
 1. \<lbrakk>(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x; x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))\<rbrakk> \<Longrightarrow> (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
using Cons False
[PROOF STATE]
proof (prove)
using this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy ps \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
x \<notin> dom (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D p \<circ> d))

goal (1 subgoal):
 1. (r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x
[PROOF STEP]
by (auto simp: policy_range_comp_def  list2policy_def map_add_dom_app_simps(3) prod_orD_def
          split: option.splits decision.splits prod.splits)
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(r o\<^sub>f (P1 \<Otimes>\<^sub>\<or>\<^sub>D list2policy (p # ps) \<circ> d)) x = list2policy ((P1 \<Otimes>\<^sub>L p # ps) (\<Otimes>\<^sub>\<or>\<^sub>D) r d) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma domSubsetDistr1: "dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>1 B) o (\<lambda> x. (x,x))) = dom B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>1 B) \<circ> (\<lambda>x. (x, x))) = dom B
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. dom A = UNIV \<Longrightarrow> (x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>1 B) \<circ> (\<lambda>x. (x, x)))) = (x \<in> dom B)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom A = UNIV; x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>1 B) \<circ> (\<lambda>x. (x, x)))\<rbrakk> \<Longrightarrow> x \<in> dom B
 2. \<And>x. \<lbrakk>dom A = UNIV; x \<in> dom B\<rbrakk> \<Longrightarrow> x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>1 B) \<circ> (\<lambda>x. (x, x)))
[PROOF STEP]
apply (auto simp: prod_1_def policy_range_comp_def dom_def
      split: decision.splits option.splits prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma domSubsetDistr2: "dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>2 B) o (\<lambda> x. (x,x))) = dom B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>2 B) \<circ> (\<lambda>x. (x, x))) = dom B
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. dom A = UNIV \<Longrightarrow> (x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>2 B) \<circ> (\<lambda>x. (x, x)))) = (x \<in> dom B)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom A = UNIV; x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>2 B) \<circ> (\<lambda>x. (x, x)))\<rbrakk> \<Longrightarrow> x \<in> dom B
 2. \<And>x. \<lbrakk>dom A = UNIV; x \<in> dom B\<rbrakk> \<Longrightarrow> x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>2 B) \<circ> (\<lambda>x. (x, x)))
[PROOF STEP]
apply (auto simp: prod_2_def policy_range_comp_def dom_def
      split: decision.splits option.splits prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma domSubsetDistrA: "dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>\<or>\<^sub>A B) o (\<lambda> x. (x,x))) = dom B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>\<or>\<^sub>A B) \<circ> (\<lambda>x. (x, x))) = dom B
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. dom A = UNIV \<Longrightarrow> (x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>\<or>\<^sub>A B) \<circ> (\<lambda>x. (x, x)))) = (x \<in> dom B)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom A = UNIV; x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>\<or>\<^sub>A B) \<circ> (\<lambda>x. (x, x)))\<rbrakk> \<Longrightarrow> x \<in> dom B
 2. \<And>x. \<lbrakk>dom A = UNIV; x \<in> dom B\<rbrakk> \<Longrightarrow> x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>\<or>\<^sub>A B) \<circ> (\<lambda>x. (x, x)))
[PROOF STEP]
apply (auto simp: prod_orA_def policy_range_comp_def dom_def
      split: decision.splits option.splits prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma domSubsetDistrD: "dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>\<or>\<^sub>D B) o (\<lambda> x. (x,x))) = dom B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom A = UNIV \<Longrightarrow> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>\<or>\<^sub>D B) \<circ> (\<lambda>x. (x, x))) = dom B
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. dom A = UNIV \<Longrightarrow> (x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>\<or>\<^sub>D B) \<circ> (\<lambda>x. (x, x)))) = (x \<in> dom B)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom A = UNIV; x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>\<or>\<^sub>D B) \<circ> (\<lambda>x. (x, x)))\<rbrakk> \<Longrightarrow> x \<in> dom B
 2. \<And>x. \<lbrakk>dom A = UNIV; x \<in> dom B\<rbrakk> \<Longrightarrow> x \<in> dom ((\<lambda>(x, y). x) o\<^sub>f (A \<Otimes>\<^sub>\<or>\<^sub>D B) \<circ> (\<lambda>x. (x, x)))
[PROOF STEP]
apply (auto simp: prod_orD_def policy_range_comp_def dom_def
      split: decision.splits option.splits prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oseq_no_change_on_send:
  fixes \<sigma> s a \<sigma>' s'
  assumes "((\<sigma>, s), a, (\<sigma>', s')) \<in> oseqp_sos \<Gamma> i"
  shows "case a of
           broadcast m     \<Rightarrow> \<sigma>' i = \<sigma> i
         | groupcast ips m \<Rightarrow> \<sigma>' i = \<sigma> i
         | unicast ips m   \<Rightarrow> \<sigma>' i = \<sigma> i
         | \<not>unicast ips    \<Rightarrow> \<sigma>' i = \<sigma> i
         | send m          \<Rightarrow> \<sigma>' i = \<sigma> i
         | deliver m       \<Rightarrow> \<sigma>' i = \<sigma> i
         | _ \<Rightarrow> True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case a of receive ma \<Rightarrow> True | \<tau>\<^sub>s \<Rightarrow> True | _ \<Rightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), a, \<sigma>', s') \<in> oseqp_sos \<Gamma> i

goal (1 subgoal):
 1. case a of receive ma \<Rightarrow> True | \<tau>\<^sub>s \<Rightarrow> True | _ \<Rightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
by induction simp_all


[STATEMENT]
lemma qmsg_no_change_on_send_or_receive:
    fixes \<sigma> s a \<sigma>' s'
  assumes "((\<sigma>, s), a, (\<sigma>', s')) \<in> oparp_sos i (oseqp_sos \<Gamma> i) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)"
      and "a \<noteq> \<tau>"
    shows "\<sigma>' i = \<sigma> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' i = \<sigma> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma>' i = \<sigma> i
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, s), a, \<sigma>', s') \<in> oparp_sos i (oseqp_sos \<Gamma> i) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)
[PROOF STEP]
obtain p q p' q'
      where "((\<sigma>, (p, q)), a, (\<sigma>', (p', q'))) \<in> oparp_sos i (oseqp_sos \<Gamma> i) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, s), a, \<sigma>', s') \<in> oparp_sos i (oseqp_sos \<Gamma> i) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. (\<And>p q p' q'. ((\<sigma>, p, q), a, \<sigma>', p', q') \<in> oparp_sos i (oseqp_sos \<Gamma> i) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases s, cases s', simp)
[PROOF STATE]
proof (state)
this:
((\<sigma>, p, q), a, \<sigma>', p', q') \<in> oparp_sos i (oseqp_sos \<Gamma> i) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. \<sigma>' i = \<sigma> i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, p, q), a, \<sigma>', p', q') \<in> oparp_sos i (oseqp_sos \<Gamma> i) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. \<sigma>' i = \<sigma> i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; \<And>m. a \<noteq> receive m; q' = q\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
 2. \<lbrakk>(q, a, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; (q, send m, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
assume "((\<sigma>, p), a, (\<sigma>', p')) \<in> oseqp_sos \<Gamma> i"
         and "\<And>m. a \<noteq> receive m"
[PROOF STATE]
proof (state)
this:
((\<sigma>, p), a, \<sigma>', p') \<in> oseqp_sos \<Gamma> i
a \<noteq> receive ?m

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; \<And>m. a \<noteq> receive m; q' = q\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
 2. \<lbrakk>(q, a, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; (q, send m, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
with \<open>a \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> \<tau>
((\<sigma>, p), a, \<sigma>', p') \<in> oseqp_sos \<Gamma> i
a \<noteq> receive ?m
[PROOF STEP]
show "\<sigma>' i = \<sigma> i"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> \<tau>
((\<sigma>, p), a, \<sigma>', p') \<in> oseqp_sos \<Gamma> i
a \<noteq> receive ?m

goal (1 subgoal):
 1. \<sigma>' i = \<sigma> i
[PROOF STEP]
by - (drule oseq_no_change_on_send, cases a, auto)
[PROOF STATE]
proof (state)
this:
\<sigma>' i = \<sigma> i

goal (2 subgoals):
 1. \<lbrakk>(q, a, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; (q, send m, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(q, a, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; (q, send m, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
assume "(q, a, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G"
         and "\<sigma>' i = \<sigma> i"
[PROOF STATE]
proof (state)
this:
(q, a, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G
\<sigma>' i = \<sigma> i

goal (2 subgoals):
 1. \<lbrakk>(q, a, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; (q, send m, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
thus "\<sigma>' i = \<sigma> i"
[PROOF STATE]
proof (prove)
using this:
(q, a, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G
\<sigma>' i = \<sigma> i

goal (1 subgoal):
 1. \<sigma>' i = \<sigma> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma>' i = \<sigma> i

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; (q, send m, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; (q, send m, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
assume "a = \<tau>"
[PROOF STATE]
proof (state)
this:
a = \<tau>

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> oseqp_sos \<Gamma> i; (q, send m, q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> \<sigma>' i = \<sigma> i
[PROOF STEP]
with \<open>a \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> \<tau>
a = \<tau>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<noteq> \<tau>
a = \<tau>

goal (1 subgoal):
 1. \<sigma>' i = \<sigma> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>' i = \<sigma> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma>' i = \<sigma> i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qmsg_msgs_not_empty:
  "qmsg \<TTurnstile> onl \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>(msgs, l). l = ()-:1 \<longrightarrow> msgs \<noteq> [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmsg \<TTurnstile> onl \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>(msgs, l). l = ()-:1 \<longrightarrow> msgs \<noteq> [])
[PROOF STEP]
by inv_cterms


[STATEMENT]
lemma qmsg_send_from_queue:
  "qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, _). sendmsg (\<lambda>m. m\<in>set msgs) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, uu_). sendmsg (\<lambda>m. m \<in> set msgs) a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, uu_). sendmsg (\<lambda>m. m \<in> set msgs) a)
[PROOF STEP]
have "qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>((msgs, _), a, _). sendmsg (\<lambda>m. m\<in>set msgs) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>((msgs, uu_), a, uu_). sendmsg (\<lambda>m. m \<in> set msgs) a)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF qmsg_wf qmsg_msgs_not_empty])
[PROOF STATE]
proof (state)
this:
qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>((msgs, uu_), a, uu_). sendmsg (\<lambda>m. m \<in> set msgs) a)

goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, uu_). sendmsg (\<lambda>m. m \<in> set msgs) a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>((msgs, uu_), a, uu_). sendmsg (\<lambda>m. m \<in> set msgs) a)

goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, uu_). sendmsg (\<lambda>m. m \<in> set msgs) a)
[PROOF STEP]
by (rule step_invariant_weakenE) (auto dest!: onllD)
[PROOF STATE]
proof (state)
this:
qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, uu_). sendmsg (\<lambda>m. m \<in> set msgs) a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qmsg_queue_contents:
  "qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, (msgs', q')). case a of
                                             receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m])
                                           | _ \<Rightarrow> set msgs' \<subseteq> set msgs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, msgs', q'). case a of receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m]) | _ \<Rightarrow> set msgs' \<subseteq> set msgs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, msgs', q'). case a of receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m]) | _ \<Rightarrow> set msgs' \<subseteq> set msgs)
[PROOF STEP]
have "qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>((msgs, q), a, (msgs', q')).
                                     case a of
                                       receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m])
                                     | _ \<Rightarrow> set msgs' \<subseteq> set msgs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>((msgs, q), a, msgs', q'). case a of receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m]) | _ \<Rightarrow> set msgs' \<subseteq> set msgs)
[PROOF STEP]
by (inv_cterms) (clarsimp simp add: in_set_tl)+
[PROOF STATE]
proof (state)
this:
qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>((msgs, q), a, msgs', q'). case a of receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m]) | _ \<Rightarrow> set msgs' \<subseteq> set msgs)

goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, msgs', q'). case a of receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m]) | _ \<Rightarrow> set msgs' \<subseteq> set msgs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>((msgs, q), a, msgs', q'). case a of receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m]) | _ \<Rightarrow> set msgs' \<subseteq> set msgs)

goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, msgs', q'). case a of receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m]) | _ \<Rightarrow> set msgs' \<subseteq> set msgs)
[PROOF STEP]
by (rule step_invariant_weakenE) (auto dest!: onllD)
[PROOF STATE]
proof (state)
this:
qmsg \<TTurnstile>\<^sub>A (\<lambda>((msgs, q), a, msgs', q'). case a of receive m \<Rightarrow> set msgs' \<subseteq> set (msgs @ [m]) | _ \<Rightarrow> set msgs' \<subseteq> set msgs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qmsg_send_receive_or_tau:
  "qmsg \<TTurnstile>\<^sub>A (\<lambda>(_, a, _). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>(uu_, a, uu_). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>(uu_, a, uu_). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)
[PROOF STEP]
have "qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>(_, a, _). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>(uu_, a, uu_). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)
[PROOF STEP]
by inv_cterms
[PROOF STATE]
proof (state)
this:
qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>(uu_, a, uu_). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)

goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>(uu_, a, uu_). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
qmsg \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G (\<lambda>(uu_, a, uu_). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)

goal (1 subgoal):
 1. qmsg \<TTurnstile>\<^sub>A (\<lambda>(uu_, a, uu_). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)
[PROOF STEP]
by rule (auto dest!: onllD)
[PROOF STATE]
proof (state)
this:
qmsg \<TTurnstile>\<^sub>A (\<lambda>(uu_, a, uu_). \<exists>m. a = send m \<or> a = receive m \<or> a = \<tau>)

goal:
No subgoals!
[PROOF STEP]
qed