[STATEMENT]
lemma map_\<I>_rsuml_lsumr [simp]: "map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) = ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) = (\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3
[PROOF STEP]
proof(rule \<I>_eqI[OF Set.set_eqI], goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. (x \<in> outs_\<I> (map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)))) = (x \<in> outs_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3))
 2. \<And>x. x \<in> outs_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) \<Longrightarrow> responses_\<I> (map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3))) x = responses_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) x
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. (x \<in> outs_\<I> (map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)))) = (x \<in> outs_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3))
 2. \<And>x. x \<in> outs_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) \<Longrightarrow> responses_\<I> (map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3))) x = responses_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> outs_\<I> (map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)))) = (x \<in> outs_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3))
[PROOF STEP]
by(cases x rule: rsuml.cases) auto
[PROOF STATE]
proof (state)
this:
(x \<in> outs_\<I> (map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)))) = (x \<in> outs_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3))

goal (1 subgoal):
 1. \<And>x. x \<in> outs_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) \<Longrightarrow> responses_\<I> (map_\<I> rsuml lsumr (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3))) x = responses_\<I> ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) x
[PROOF STEP]
qed (auto simp add: image_image)


[STATEMENT]
lemma map_\<I>_lsumr_rsuml [simp]: "map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) = (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) = \<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)
[PROOF STEP]
proof(rule \<I>_eqI[OF Set.set_eqI], goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. (x \<in> outs_\<I> (map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3))) = (x \<in> outs_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)))
 2. \<And>x. x \<in> outs_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) \<Longrightarrow> responses_\<I> (map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3)) x = responses_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) x
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. (x \<in> outs_\<I> (map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3))) = (x \<in> outs_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)))
 2. \<And>x. x \<in> outs_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) \<Longrightarrow> responses_\<I> (map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3)) x = responses_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> outs_\<I> (map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3))) = (x \<in> outs_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)))
[PROOF STEP]
by(cases x rule: lsumr.cases) auto
[PROOF STATE]
proof (state)
this:
(x \<in> outs_\<I> (map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3))) = (x \<in> outs_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)))

goal (1 subgoal):
 1. \<And>x. x \<in> outs_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) \<Longrightarrow> responses_\<I> (map_\<I> lsumr rsuml ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3)) x = responses_\<I> (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) x
[PROOF STEP]
qed (auto simp add: image_image)


[STATEMENT]
lemma map_\<I>_swap_sum [simp]: "map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2) = \<I>2 \<oplus>\<^sub>\<I> \<I>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2) = \<I>2 \<oplus>\<^sub>\<I> \<I>1
[PROOF STEP]
proof(rule \<I>_eqI[OF Set.set_eqI], goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. (x \<in> outs_\<I> (map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2))) = (x \<in> outs_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1))
 2. \<And>x. x \<in> outs_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1) \<Longrightarrow> responses_\<I> (map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2)) x = responses_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1) x
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. (x \<in> outs_\<I> (map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2))) = (x \<in> outs_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1))
 2. \<And>x. x \<in> outs_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1) \<Longrightarrow> responses_\<I> (map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2)) x = responses_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> outs_\<I> (map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2))) = (x \<in> outs_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1))
[PROOF STEP]
by(cases x) auto
[PROOF STATE]
proof (state)
this:
(x \<in> outs_\<I> (map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2))) = (x \<in> outs_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1))

goal (1 subgoal):
 1. \<And>x. x \<in> outs_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1) \<Longrightarrow> responses_\<I> (map_\<I> swap_sum swap_sum (\<I>1 \<oplus>\<^sub>\<I> \<I>2)) x = responses_\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>1) x
[PROOF STEP]
qed (auto simp add: image_image)


[STATEMENT]
lemma WT_parallel_resource1_wiring [WT_intro]: "\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3), \<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<turnstile>\<^sub>C parallel_resource1_wiring \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3), \<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<turnstile>\<^sub>C parallel_resource1_wiring \<surd>
[PROOF STEP]
unfolding parallel_resource1_wiring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3), \<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<turnstile>\<^sub>C swap_lassocr \<surd>
[PROOF STEP]
by(rule WT_swap_lassocr)


[STATEMENT]
lemma plossless_rassocl\<^sub>C [plossless_intro]: "plossless_converter (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) rassocl\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_converter (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) rassocl\<^sub>C
[PROOF STEP]
by coinduction (auto simp add: rassocl\<^sub>C_def)


[STATEMENT]
lemma plossless_lassocr\<^sub>C [plossless_intro]: "plossless_converter ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) lassocr\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_converter ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) lassocr\<^sub>C
[PROOF STEP]
by coinduction (auto simp add: lassocr\<^sub>C_def)


[STATEMENT]
lemma plossless_swap_lassocr [plossless_intro]:
  "plossless_converter (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) (\<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3)) swap_lassocr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_converter (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) (\<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3)) swap_lassocr
[PROOF STEP]
unfolding swap_lassocr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_converter (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) (\<I>2 \<oplus>\<^sub>\<I> (\<I>1 \<oplus>\<^sub>\<I> \<I>3)) (rassocl\<^sub>C \<odot> (swap\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> lassocr\<^sub>C)
[PROOF STEP]
by(rule plossless_intro WT_intro)+


[STATEMENT]
lemma rsuml_lsumr_parallel_converter2:
  "map_converter id id rsuml lsumr ((conv1 |\<^sub>= conv2) |\<^sub>= conv3) =
   map_converter rsuml lsumr id id (conv1 |\<^sub>= conv2 |\<^sub>= conv3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_converter id id rsuml lsumr ((conv1 |\<^sub>= conv2) |\<^sub>= conv3) = map_converter rsuml lsumr id id (conv1 |\<^sub>= conv2 |\<^sub>= conv3)
[PROOF STEP]
by(coinduction arbitrary: conv1 conv2 conv3, clarsimp split!: sum.split simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric])
    ((subst left_gpv_map[where h=id] | subst right_gpv_map[where h=id])+
      , simp add:gpv.map_comp sum.map_id0 o_def prod.map_comp id_def[symmetric]
      , subst map_gpv'_map_gpv_swap, (subst rsuml_lsumr_left_gpv_left_gpv | subst rsuml_lsumr_left_gpv_right_gpv | subst rsuml_lsumr_right_gpv)
      , auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+


[STATEMENT]
lemma comp_lassocr\<^sub>C: "((conv1 |\<^sub>= conv2) |\<^sub>= conv3) \<odot> lassocr\<^sub>C = lassocr\<^sub>C \<odot> (conv1 |\<^sub>= conv2 |\<^sub>= conv3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((conv1 |\<^sub>= conv2) |\<^sub>= conv3) \<odot> lassocr\<^sub>C = lassocr\<^sub>C \<odot> (conv1 |\<^sub>= conv2 |\<^sub>= conv3)
[PROOF STEP]
unfolding lassocr\<^sub>C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((conv1 |\<^sub>= conv2) |\<^sub>= conv3) \<odot> map_converter rsuml lsumr id id 1\<^sub>C = map_converter rsuml lsumr id id 1\<^sub>C \<odot> (conv1 |\<^sub>= conv2 |\<^sub>= conv3)
[PROOF STEP]
by(subst comp_converter_map_converter2)
    (simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left rsuml_lsumr_parallel_converter2)


[STATEMENT]
lemma lsumr_rsuml_parallel_converter2:
  "map_converter id id lsumr rsuml (conv1 |\<^sub>= (conv2 |\<^sub>= conv3)) =
   map_converter lsumr rsuml id id ((conv1 |\<^sub>= conv2) |\<^sub>= conv3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_converter id id lsumr rsuml (conv1 |\<^sub>= conv2 |\<^sub>= conv3) = map_converter lsumr rsuml id id ((conv1 |\<^sub>= conv2) |\<^sub>= conv3)
[PROOF STEP]
by(coinduction arbitrary: conv1 conv2 conv3, clarsimp split!: sum.split simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric])
    ((subst left_gpv_map[where h=id] | subst right_gpv_map[where h=id])+
      , simp add:gpv.map_comp sum.map_id0 o_def prod.map_comp id_def[symmetric]
      , subst map_gpv'_map_gpv_swap, (subst lsumr_rsuml_left_gpv | subst lsumr_rsuml_right_gpv_left_gpv | subst lsumr_rsuml_right_gpv_right_gpv)
      , auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+


[STATEMENT]
lemma comp_rassocl\<^sub>C:
  "(conv1 |\<^sub>= conv2 |\<^sub>= conv3) \<odot> rassocl\<^sub>C = rassocl\<^sub>C \<odot> ((conv1 |\<^sub>= conv2) |\<^sub>= conv3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (conv1 |\<^sub>= conv2 |\<^sub>= conv3) \<odot> rassocl\<^sub>C = rassocl\<^sub>C \<odot> ((conv1 |\<^sub>= conv2) |\<^sub>= conv3)
[PROOF STEP]
unfolding rassocl\<^sub>C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (conv1 |\<^sub>= conv2 |\<^sub>= conv3) \<odot> map_converter lsumr rsuml id id 1\<^sub>C = map_converter lsumr rsuml id id 1\<^sub>C \<odot> ((conv1 |\<^sub>= conv2) |\<^sub>= conv3)
[PROOF STEP]
by(subst comp_converter_map_converter2)
    (simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left lsumr_rsuml_parallel_converter2)


[STATEMENT]
lemma swap_sum_right_gpv:
  "map_gpv' id swap_sum swap_sum (right_gpv gpv) = left_gpv gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_gpv' id swap_sum swap_sum (right_gpv gpv) = left_gpv gpv
[PROOF STEP]
by(coinduction arbitrary: gpv)
    (auto 4 3 simp add: spmf_rel_map generat.rel_map intro!: rel_spmf_reflI rel_generat_reflI rel_funI split: sum.split intro: exI[where x=Fail])


[STATEMENT]
lemma swap_sum_left_gpv:
  "map_gpv' id swap_sum swap_sum (left_gpv gpv) = right_gpv gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_gpv' id swap_sum swap_sum (left_gpv gpv) = right_gpv gpv
[PROOF STEP]
by(coinduction arbitrary: gpv)
    (auto 4 3 simp add: spmf_rel_map generat.rel_map intro!: rel_spmf_reflI rel_generat_reflI rel_funI split: sum.split intro: exI[where x=Fail])


[STATEMENT]
lemma swap_sum_parallel_converter2:
  "map_converter id id swap_sum swap_sum (conv1 |\<^sub>= conv2) =
   map_converter swap_sum swap_sum id id (conv2 |\<^sub>= conv1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_converter id id swap_sum swap_sum (conv1 |\<^sub>= conv2) = map_converter swap_sum swap_sum id id (conv2 |\<^sub>= conv1)
[PROOF STEP]
by(coinduction arbitrary: conv1 conv2, clarsimp simp add: rel_fun_def map_gpv_conv_map_gpv'[symmetric] split!: sum.split)
    (subst map_gpv'_map_gpv_swap, (subst swap_sum_right_gpv | subst swap_sum_left_gpv),
      auto 4 4 intro!: gpv.rel_refl_strong simp add: gpv.rel_map)+


[STATEMENT]
lemma comp_swap\<^sub>C: "(conv1 |\<^sub>= conv2) \<odot> swap\<^sub>C = swap\<^sub>C \<odot> (conv2 |\<^sub>= conv1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (conv1 |\<^sub>= conv2) \<odot> swap\<^sub>C = swap\<^sub>C \<odot> (conv2 |\<^sub>= conv1)
[PROOF STEP]
unfolding swap\<^sub>C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (conv1 |\<^sub>= conv2) \<odot> map_converter swap_sum swap_sum id id 1\<^sub>C = map_converter swap_sum swap_sum id id 1\<^sub>C \<odot> (conv2 |\<^sub>= conv1)
[PROOF STEP]
by(subst comp_converter_map_converter2)
    (simp add: comp_converter_id_right comp_converter_map1_out comp_converter_id_left swap_sum_parallel_converter2)


[STATEMENT]
lemma comp_swap_lassocr: "(conv1 |\<^sub>= conv2 |\<^sub>= conv3) \<odot> swap_lassocr = swap_lassocr \<odot> (conv2 |\<^sub>= conv1 |\<^sub>= conv3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (conv1 |\<^sub>= conv2 |\<^sub>= conv3) \<odot> swap_lassocr = swap_lassocr \<odot> (conv2 |\<^sub>= conv1 |\<^sub>= conv3)
[PROOF STEP]
unfolding swap_lassocr_def comp_rassocl\<^sub>C' comp_converter_assoc comp_converter_parallel2' comp_swap\<^sub>C' comp_converter_id_right
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rassocl\<^sub>C \<odot> (swap\<^sub>C \<odot> (conv2 |\<^sub>= conv1) |\<^sub>= conv3) \<odot> lassocr\<^sub>C = rassocl\<^sub>C \<odot> (swap\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> lassocr\<^sub>C \<odot> (conv2 |\<^sub>= conv1 |\<^sub>= conv3)
[PROOF STEP]
by(subst (9) comp_converter_id_left[symmetric], subst comp_converter_parallel2[symmetric])
    (simp add: comp_converter_assoc comp_lassocr\<^sub>C)


[STATEMENT]
lemma comp_parallel_wiring:
  "((C1 |\<^sub>= C2) |\<^sub>= (C3 |\<^sub>= C4)) \<odot> parallel_wiring = parallel_wiring \<odot> ((C1 |\<^sub>= C3) |\<^sub>= (C2 |\<^sub>= C4))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((C1 |\<^sub>= C2) |\<^sub>= C3 |\<^sub>= C4) \<odot> parallel_wiring = parallel_wiring \<odot> ((C1 |\<^sub>= C3) |\<^sub>= C2 |\<^sub>= C4)
[PROOF STEP]
unfolding parallel_wiring_def comp_lassocr\<^sub>C' comp_converter_assoc comp_converter_parallel2' comp_swap_lassocr'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lassocr\<^sub>C \<odot> (C1 \<odot> 1\<^sub>C |\<^sub>= swap_lassocr \<odot> (C3 |\<^sub>= C2 |\<^sub>= C4)) \<odot> rassocl\<^sub>C = lassocr\<^sub>C \<odot> (1\<^sub>C |\<^sub>= swap_lassocr) \<odot> rassocl\<^sub>C \<odot> ((C1 |\<^sub>= C3) |\<^sub>= C2 |\<^sub>= C4)
[PROOF STEP]
by(subst comp_converter_id_right[THEN trans, OF comp_converter_id_left[symmetric]], subst comp_converter_parallel2[symmetric])
    (simp add: comp_converter_assoc comp_rassocl\<^sub>C)


[STATEMENT]
lemma attach_converter_of_resource_conv_parallel_resource:
  "converter_of_resource res |\<^sub>\<propto> 1\<^sub>C \<rhd> res' = res \<parallel> res'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. converter_of_resource res |\<^sub>\<propto> 1\<^sub>C \<rhd> res' = res \<parallel> res'
[PROOF STEP]
by(coinduction arbitrary: res res')
    (auto 4 3 simp add: rel_fun_def map_lift_spmf spmf.map_comp o_def prod.map_comp spmf_rel_map bind_map_spmf map_spmf_conv_bind_spmf[symmetric] split_def split!: sum.split intro!: rel_spmf_reflI)


[STATEMENT]
lemma attach_converter_of_resource_conv_parallel_resource2:
  " 1\<^sub>C |\<^sub>\<propto> converter_of_resource res \<rhd> res' = res' \<parallel> res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>C |\<^sub>\<propto> converter_of_resource res \<rhd> res' = res' \<parallel> res
[PROOF STEP]
by(coinduction arbitrary: res res')
    (auto 4 3 simp add: rel_fun_def map_lift_spmf spmf.map_comp o_def prod.map_comp spmf_rel_map bind_map_spmf map_spmf_conv_bind_spmf[symmetric] split_def split!: sum.split intro!: rel_spmf_reflI)


[STATEMENT]
lemma plossless_parallel_wiring [plossless_intro]:
  "plossless_converter ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> (\<I>3 \<oplus>\<^sub>\<I> \<I>4)) ((\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>4)) parallel_wiring"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_converter ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> (\<I>3 \<oplus>\<^sub>\<I> \<I>4)) ((\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>4)) parallel_wiring
[PROOF STEP]
unfolding parallel_wiring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_converter ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> (\<I>3 \<oplus>\<^sub>\<I> \<I>4)) ((\<I>1 \<oplus>\<^sub>\<I> \<I>3) \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>4)) (lassocr\<^sub>C \<odot> (1\<^sub>C |\<^sub>= swap_lassocr) \<odot> rassocl\<^sub>C)
[PROOF STEP]
by(rule plossless_intro WT_intro)+


[STATEMENT]
lemma run_converter_lassocr [simp]:
  "run_converter lassocr\<^sub>C x = Pause (rsuml x) (\<lambda>x. Done (lsumr x, lassocr\<^sub>C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_converter lassocr\<^sub>C x = Pause (rsuml x) (\<lambda>x. Done (lsumr x, lassocr\<^sub>C))
[PROOF STEP]
by(simp add: lassocr\<^sub>C_def o_def)


[STATEMENT]
lemma run_converter_rassocl [simp]:
  "run_converter rassocl\<^sub>C x = Pause (lsumr x) (\<lambda>x. Done (rsuml x, rassocl\<^sub>C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_converter rassocl\<^sub>C x = Pause (lsumr x) (\<lambda>x. Done (rsuml x, rassocl\<^sub>C))
[PROOF STEP]
by(simp add: rassocl\<^sub>C_def o_def)


[STATEMENT]
lemma run_converter_swap [simp]: "run_converter swap\<^sub>C x = Pause (swap_sum x) (\<lambda>x. Done (swap_sum x, swap\<^sub>C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_converter swap\<^sub>C x = Pause (swap_sum x) (\<lambda>x. Done (swap_sum x, swap\<^sub>C))
[PROOF STEP]
by(simp add: swap\<^sub>C_def o_def)


[STATEMENT]
lemma run_converter_swap_lassocr [simp]:
  "run_converter swap_lassocr x = Pause (lassocr_swap_sum x) (
     case lsumr x of Inl _ \<Rightarrow> (\<lambda>y. case lsumr y of Inl _ \<Rightarrow> Done (lassocr_swap_sum y, swap_lassocr) | _ \<Rightarrow> Fail)
          | Inr _ \<Rightarrow> (\<lambda>y. case lsumr y of Inl _ \<Rightarrow> Fail | Inr _ \<Rightarrow> Done (lassocr_swap_sum y, swap_lassocr)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_converter swap_lassocr x = Pause (lassocr_swap_sum x) (case lsumr x of Inl x \<Rightarrow> \<lambda>y. case lsumr y of Inl x \<Rightarrow> Done (lassocr_swap_sum y, swap_lassocr) | Inr b \<Rightarrow> Fail | Inr x \<Rightarrow> \<lambda>y. case lsumr y of Inl x \<Rightarrow> Fail | Inr x \<Rightarrow> Done (lassocr_swap_sum y, swap_lassocr))
[PROOF STEP]
by(subst sum.case_distrib[where h="\<lambda>x. inline _ x _"] |
      simp add: bind_rpv_def inline_map_gpv split_def map_gpv_conv_bind[symmetric] swap_lassocr_def o_def cong del: sum.case_cong)+
    (cases x rule: lsumr.cases, simp_all add: o_def lassocr_swap_sum_def gpv.map_comp fun_eq_iff cong: sum.case_cong split: sum.split)


[STATEMENT]
lemma run_converter_parallel_wiring:
  "run_converter parallel_wiring x = Pause (parallel_sum_wiring x) (
    case rsuml x of Inl _ \<Rightarrow> (\<lambda>y. case rsuml y of Inl _ \<Rightarrow> Done (parallel_sum_wiring y, parallel_wiring) | _ \<Rightarrow> Fail)
                | Inr x \<Rightarrow> (case lsumr x of Inl _ \<Rightarrow> (\<lambda>y. case rsuml y of Inl _ \<Rightarrow> Fail | Inr x \<Rightarrow> (case lsumr x of Inl _ \<Rightarrow> Done (parallel_sum_wiring y, parallel_wiring) | Inr _ \<Rightarrow> Fail))
                                          | Inr _ \<Rightarrow> (\<lambda>y. case rsuml y of Inl _ \<Rightarrow> Fail | Inr x \<Rightarrow> (case lsumr x of Inl _ \<Rightarrow> Fail | Inr _ \<Rightarrow> Done (parallel_sum_wiring y, parallel_wiring)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_converter parallel_wiring x = Pause (parallel_sum_wiring x) (case rsuml x of Inl x \<Rightarrow> \<lambda>y. case rsuml y of Inl x \<Rightarrow> Done (parallel_sum_wiring y, parallel_wiring) | Inr b \<Rightarrow> Fail | Inr x \<Rightarrow> case lsumr x of Inl x \<Rightarrow> \<lambda>y. case rsuml y of Inl x \<Rightarrow> Fail | Inr x \<Rightarrow> case lsumr x of Inl x \<Rightarrow> Done (parallel_sum_wiring y, parallel_wiring) | Inr x \<Rightarrow> Fail | Inr x \<Rightarrow> \<lambda>y. case rsuml y of Inl x \<Rightarrow> Fail | Inr x \<Rightarrow> case lsumr x of Inl x \<Rightarrow> Fail | Inr x \<Rightarrow> Done (parallel_sum_wiring y, parallel_wiring))
[PROOF STEP]
by(simp add: parallel_wiring_def o_def cong del: sum.case_cong add: split_def map_gpv_conv_bind[symmetric])
    (subst sum.case_distrib[where h="\<lambda>x. right_rpv x _"] |
      subst sum.case_distrib[where h="\<lambda>x. inline _ x _"] |
      subst sum.case_distrib[where h=right_gpv] |
      (auto simp add: inline_map_gpv bind_rpv_def  gpv.map_comp fun_eq_iff parallel_sum_wiring_def
        parallel_wiring_def[symmetric] sum.case_distrib o_def intro: sym cong del: sum.case_cong split!: sum.split))+


[STATEMENT]
lemma bound_lassocr\<^sub>C [interaction_bound]: "interaction_any_bounded_converter lassocr\<^sub>C 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter lassocr\<^sub>C 1
[PROOF STEP]
unfolding lassocr\<^sub>C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter (map_converter rsuml lsumr id id 1\<^sub>C) 1
[PROOF STEP]
by interaction_bound_converter simp


[STATEMENT]
lemma bound_rassocl\<^sub>C [interaction_bound]: "interaction_any_bounded_converter rassocl\<^sub>C 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter rassocl\<^sub>C 1
[PROOF STEP]
unfolding rassocl\<^sub>C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter (map_converter lsumr rsuml id id 1\<^sub>C) 1
[PROOF STEP]
by interaction_bound_converter simp


[STATEMENT]
lemma bound_swap\<^sub>C [interaction_bound]: "interaction_any_bounded_converter swap\<^sub>C 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter swap\<^sub>C 1
[PROOF STEP]
unfolding swap\<^sub>C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter (map_converter swap_sum swap_sum id id 1\<^sub>C) 1
[PROOF STEP]
by interaction_bound_converter simp


[STATEMENT]
lemma bound_swap_rassocl [interaction_bound]: "interaction_any_bounded_converter swap_rassocl 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter swap_rassocl 1
[PROOF STEP]
unfolding swap_rassocl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter (lassocr\<^sub>C \<odot> (1\<^sub>C |\<^sub>= swap\<^sub>C) \<odot> rassocl\<^sub>C) 1
[PROOF STEP]
by interaction_bound_converter simp


[STATEMENT]
lemma bound_swap_lassocr [interaction_bound]: "interaction_any_bounded_converter swap_lassocr 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter swap_lassocr 1
[PROOF STEP]
unfolding swap_lassocr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter (rassocl\<^sub>C \<odot> (swap\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> lassocr\<^sub>C) 1
[PROOF STEP]
by interaction_bound_converter simp


[STATEMENT]
lemma bound_parallel_wiring [interaction_bound]: "interaction_any_bounded_converter parallel_wiring 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter parallel_wiring 1
[PROOF STEP]
unfolding parallel_wiring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter (lassocr\<^sub>C \<odot> (1\<^sub>C |\<^sub>= swap_lassocr) \<odot> rassocl\<^sub>C) 1
[PROOF STEP]
by interaction_bound_converter simp


[STATEMENT]
lemma wiringD:
  assumes "wiring \<I> \<I>' cnv (f, g)"
  shows wiringD_eq: "\<I>,\<I>' \<turnstile>\<^sub>C cnv \<sim> map_converter id id f g 1\<^sub>C"
    and wiringD_WT: "\<I>,\<I>' \<turnstile>\<^sub>C cnv \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>,\<I>' \<turnstile>\<^sub>C cnv \<sim> map_converter id id f g 1\<^sub>C &&& \<I>, \<I>' \<turnstile>\<^sub>C cnv \<surd>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wiring \<I> \<I>' cnv (f, g)

goal (1 subgoal):
 1. \<I>,\<I>' \<turnstile>\<^sub>C cnv \<sim> map_converter id id f g 1\<^sub>C &&& \<I>, \<I>' \<turnstile>\<^sub>C cnv \<surd>
[PROOF STEP]
by(cases, blast)+


[STATEMENT]
lemma apply_wiring_simps: "apply_wiring (f, g) = map_fun id (map_fun f (map_spmf (map_prod g id)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_wiring (f, g) = map_fun id (map_fun f (map_spmf (map_prod g id)))
[PROOF STEP]
by(simp add: apply_wiring_def)


[STATEMENT]
lemma attach_wiring_resource_of_oracle:
  assumes wiring: "wiring \<I>1 \<I>2 conv fg"
    and WT: "\<I>2 \<turnstile>res RES res s \<surd>"
    and outs: "outs_\<I> \<I>1 = UNIV"
  shows "conv \<rhd> RES res s = RES (apply_wiring fg res) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
using wiring
[PROOF STATE]
proof (prove)
using this:
wiring \<I>1 \<I>2 conv fg

goal (1 subgoal):
 1. conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g. \<lbrakk>fg = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
case (wiring f g)
[PROOF STATE]
proof (state)
this:
fg = (f, g)
\<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C
\<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>fg = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
have "\<I>_full,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>_full,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C
[PROOF STEP]
using wiring(2)
[PROOF STATE]
proof (prove)
using this:
\<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C

goal (1 subgoal):
 1. \<I>_full,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C
[PROOF STEP]
by(rule eq_\<I>_converter_mono)(simp_all add: le_\<I>_def outs)
[PROOF STATE]
proof (state)
this:
\<I>_full,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>fg = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
with WT
[PROOF STATE]
proof (chain)
picking this:
\<I>2 \<turnstile>res RES res s \<surd>
\<I>_full,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C
[PROOF STEP]
have "conv \<rhd> RES res s = map_converter id id f g 1\<^sub>C \<rhd> RES res s"
[PROOF STATE]
proof (prove)
using this:
\<I>2 \<turnstile>res RES res s \<surd>
\<I>_full,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C

goal (1 subgoal):
 1. conv \<rhd> RES res s = map_converter id id f g 1\<^sub>C \<rhd> RES res s
[PROOF STEP]
by(rule eq_\<I>_attach)
[PROOF STATE]
proof (state)
this:
conv \<rhd> RES res s = map_converter id id f g 1\<^sub>C \<rhd> RES res s

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>fg = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
conv \<rhd> RES res s = map_converter id id f g 1\<^sub>C \<rhd> RES res s

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>fg = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
have "\<dots> = RES (apply_wiring fg res) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_converter id id f g 1\<^sub>C \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
by(simp add: attach_map_converter map_resource_resource_of_oracle prod.map_id0 option.map_id0 map_fun_id apply_wiring_def wiring(1))
[PROOF STATE]
proof (state)
this:
map_converter id id f g 1\<^sub>C \<rhd> RES res s = RES (apply_wiring fg res) s

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>fg = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
conv \<rhd> RES res s = RES (apply_wiring fg res) s

goal (1 subgoal):
 1. conv \<rhd> RES res s = RES (apply_wiring fg res) s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
conv \<rhd> RES res s = RES (apply_wiring fg res) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wiring_id_converter [simp, wiring_intro]: "wiring \<I> \<I> 1\<^sub>C (id, id)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring \<I> \<I> 1\<^sub>C (id, id)
[PROOF STEP]
using wiring.intros[of \<I> \<I> "1\<^sub>C" id id]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<I>,\<I> \<turnstile>\<^sub>C 1\<^sub>C \<sim> map_converter id id id id 1\<^sub>C; \<I>, \<I> \<turnstile>\<^sub>C 1\<^sub>C \<surd>\<rbrakk> \<Longrightarrow> wiring \<I> \<I> 1\<^sub>C (id, id)

goal (1 subgoal):
 1. wiring \<I> \<I> 1\<^sub>C (id, id)
[PROOF STEP]
by(simp add: eq_\<I>_converter_reflI)


[STATEMENT]
lemma apply_wiring_id [simp]: "apply_wiring (id, id) res = res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_wiring (id, id) res = res
[PROOF STEP]
by(simp add: apply_wiring_simps prod.map_id0 option.map_id0 map_fun_id)


[STATEMENT]
lemma attach_wiring_simps: "attach_wiring (f, g) = map_fun id (map_fun f (map_gpv (map_prod g id) id))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. attach_wiring (f, g) = map_fun id (map_fun f (map_gpv (map_prod g id) id))
[PROOF STEP]
by(simp add: attach_wiring_def)


[STATEMENT]
lemma comp_wiring_converter_of_callee:
  assumes wiring: "wiring \<I>1 \<I>2 conv w"
    and WT: "\<I>2, \<I>3 \<turnstile>\<^sub>C CNV callee s \<surd>"
  shows "\<I>1, \<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
using wiring
[PROOF STATE]
proof (prove)
using this:
wiring \<I>1 \<I>2 conv w

goal (1 subgoal):
 1. \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g. \<lbrakk>w = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
case (wiring f g)
[PROOF STATE]
proof (state)
this:
w = (f, g)
\<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C
\<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>w = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
from wiring(2)
[PROOF STATE]
proof (chain)
picking this:
\<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C
[PROOF STEP]
have "\<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> map_converter id id f g 1\<^sub>C \<odot> CNV callee s"
[PROOF STATE]
proof (prove)
using this:
\<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C

goal (1 subgoal):
 1. \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> map_converter id id f g 1\<^sub>C \<odot> CNV callee s
[PROOF STEP]
by(rule eq_\<I>_comp_cong)(rule eq_\<I>_converter_reflI[OF WT])
[PROOF STATE]
proof (state)
this:
\<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> map_converter id id f g 1\<^sub>C \<odot> CNV callee s

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>w = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> map_converter id id f g 1\<^sub>C \<odot> CNV callee s

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>w = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
have "map_converter id id f g 1\<^sub>C \<odot> CNV callee s = map_converter f g id id (CNV callee s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_converter id id f g 1\<^sub>C \<odot> CNV callee s = map_converter f g id id (CNV callee s)
[PROOF STEP]
by(subst comp_converter_map_converter1)(simp add: comp_converter_id_left)
[PROOF STATE]
proof (state)
this:
map_converter id id f g 1\<^sub>C \<odot> CNV callee s = map_converter f g id id (CNV callee s)

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>w = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_converter id id f g 1\<^sub>C \<odot> CNV callee s = map_converter f g id id (CNV callee s)

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>w = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
have "\<dots> = CNV (attach_wiring w callee) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_converter f g id id (CNV callee s) = CNV (attach_wiring w callee) s
[PROOF STEP]
by(simp add: map_converter_of_callee attach_wiring_simps wiring(1) map_gpv_conv_map_gpv')
[PROOF STATE]
proof (state)
this:
map_converter f g id id (CNV callee s) = CNV (attach_wiring w callee) s

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>w = (f, g); \<I>1,\<I>2 \<turnstile>\<^sub>C conv \<sim> map_converter id id f g 1\<^sub>C; \<I>1, \<I>2 \<turnstile>\<^sub>C conv \<surd>\<rbrakk> \<Longrightarrow> \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s

goal (1 subgoal):
 1. \<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<I>1,\<I>3 \<turnstile>\<^sub>C conv \<odot> CNV callee s \<sim> CNV (attach_wiring w callee) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_wiring_simps: "comp_wiring (f, g) (f', g') = (f' \<circ> f, g \<circ> g')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<circ>\<^sub>w (f', g') = (f' \<circ> f, g \<circ> g')
[PROOF STEP]
by(simp add: comp_wiring_def)


[STATEMENT]
lemma wiring_comp_converterI [wiring_intro]:
  "wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')" if "wiring \<I> \<I>' conv1 fg" "wiring \<I>' \<I>'' conv2 fg'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
from that(1)
[PROOF STATE]
proof (chain)
picking this:
wiring \<I> \<I>' conv1 fg
[PROOF STEP]
obtain f g
    where conv1: "\<I>,\<I>' \<turnstile>\<^sub>C conv1 \<sim> map_converter id id f g 1\<^sub>C"
      and WT1: "\<I>, \<I>' \<turnstile>\<^sub>C conv1 \<surd>"
      and [simp]: "fg = (f, g)"
[PROOF STATE]
proof (prove)
using this:
wiring \<I> \<I>' conv1 fg

goal (1 subgoal):
 1. (\<And>f g. \<lbrakk>\<I>,\<I>' \<turnstile>\<^sub>C conv1 \<sim> map_converter id id f g 1\<^sub>C; \<I>, \<I>' \<turnstile>\<^sub>C conv1 \<surd>; fg = (f, g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
\<I>,\<I>' \<turnstile>\<^sub>C conv1 \<sim> map_converter id id f g 1\<^sub>C
\<I>, \<I>' \<turnstile>\<^sub>C conv1 \<surd>
fg = (f, g)

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
from that(2)
[PROOF STATE]
proof (chain)
picking this:
wiring \<I>' \<I>'' conv2 fg'
[PROOF STEP]
obtain f' g'
    where conv2: "\<I>',\<I>'' \<turnstile>\<^sub>C conv2 \<sim> map_converter id id f' g' 1\<^sub>C"
      and WT2: "\<I>', \<I>'' \<turnstile>\<^sub>C conv2 \<surd>"
      and [simp]: "fg' = (f', g')"
[PROOF STATE]
proof (prove)
using this:
wiring \<I>' \<I>'' conv2 fg'

goal (1 subgoal):
 1. (\<And>f' g'. \<lbrakk>\<I>',\<I>'' \<turnstile>\<^sub>C conv2 \<sim> map_converter id id f' g' 1\<^sub>C; \<I>', \<I>'' \<turnstile>\<^sub>C conv2 \<surd>; fg' = (f', g')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
\<I>',\<I>'' \<turnstile>\<^sub>C conv2 \<sim> map_converter id id f' g' 1\<^sub>C
\<I>', \<I>'' \<turnstile>\<^sub>C conv2 \<surd>
fg' = (f', g')

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
have *: "(fg \<circ>\<^sub>w fg') = (f' \<circ> f, g \<circ> g')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fg \<circ>\<^sub>w fg' = (f' \<circ> f, g \<circ> g')
[PROOF STEP]
by(simp add: comp_wiring_simps)
[PROOF STATE]
proof (state)
this:
fg \<circ>\<^sub>w fg' = (f' \<circ> f, g \<circ> g')

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
have "\<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<sim> map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<sim> map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C
[PROOF STEP]
using conv1 conv2
[PROOF STATE]
proof (prove)
using this:
\<I>,\<I>' \<turnstile>\<^sub>C conv1 \<sim> map_converter id id f g 1\<^sub>C
\<I>',\<I>'' \<turnstile>\<^sub>C conv2 \<sim> map_converter id id f' g' 1\<^sub>C

goal (1 subgoal):
 1. \<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<sim> map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C
[PROOF STEP]
by(rule eq_\<I>_comp_cong)
[PROOF STATE]
proof (state)
this:
\<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<sim> map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<sim> map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
have "map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C = map_converter id id (f' \<circ> f) (g \<circ> g') 1\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C = map_converter id id (f' \<circ> f) (g \<circ> g') 1\<^sub>C
[PROOF STEP]
by(simp add: comp_converter_map_converter2 comp_converter_id_right)
[PROOF STATE]
proof (state)
this:
map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C = map_converter id id (f' \<circ> f) (g \<circ> g') 1\<^sub>C

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_converter id id f g 1\<^sub>C \<odot> map_converter id id f' g' 1\<^sub>C = map_converter id id (f' \<circ> f) (g \<circ> g') 1\<^sub>C

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
have "\<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>, \<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<surd>
[PROOF STEP]
using WT1 WT2
[PROOF STATE]
proof (prove)
using this:
\<I>, \<I>' \<turnstile>\<^sub>C conv1 \<surd>
\<I>', \<I>'' \<turnstile>\<^sub>C conv2 \<surd>

goal (1 subgoal):
 1. \<I>, \<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<surd>
[PROOF STEP]
by(rule WT_converter_comp)
[PROOF STATE]
proof (state)
this:
\<I>, \<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<surd>

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<sim> map_converter id id (f' \<circ> f) (g \<circ> g') 1\<^sub>C
\<I>, \<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<surd>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<sim> map_converter id id (f' \<circ> f) (g \<circ> g') 1\<^sub>C
\<I>, \<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<surd>

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
\<I>,\<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<sim> map_converter id id (f' \<circ> f) (g \<circ> g') 1\<^sub>C
\<I>, \<I>'' \<turnstile>\<^sub>C conv1 \<odot> conv2 \<surd>

goal (1 subgoal):
 1. wiring \<I> \<I>'' (conv1 \<odot> conv2) (f' \<circ> f, g \<circ> g')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
wiring \<I> \<I>'' (conv1 \<odot> conv2) (fg \<circ>\<^sub>w fg')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parallel2_wiring_simps:
  "parallel2_wiring (f, g) (f', g') = (map_sum f f', map_sum g g')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) |\<^sub>w (f', g') = (map_sum f f', map_sum g g')
[PROOF STEP]
by(simp add: parallel2_wiring_def)


[STATEMENT]
lemma wiring_parallel_converter2 [simp, wiring_intro]:
  assumes "wiring \<I>1 \<I>1' conv1 fg"
    and "wiring \<I>2 \<I>2' conv2 fg'"
  shows "wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
wiring \<I>1 \<I>1' conv1 fg
[PROOF STEP]
obtain f1 g1
    where conv1: "\<I>1,\<I>1' \<turnstile>\<^sub>C conv1 \<sim> map_converter id id f1 g1 1\<^sub>C"
      and WT1: "\<I>1, \<I>1' \<turnstile>\<^sub>C conv1 \<surd>"
      and [simp]: "fg = (f1, g1)"
[PROOF STATE]
proof (prove)
using this:
wiring \<I>1 \<I>1' conv1 fg

goal (1 subgoal):
 1. (\<And>f1 g1. \<lbrakk>\<I>1,\<I>1' \<turnstile>\<^sub>C conv1 \<sim> map_converter id id f1 g1 1\<^sub>C; \<I>1, \<I>1' \<turnstile>\<^sub>C conv1 \<surd>; fg = (f1, g1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
\<I>1,\<I>1' \<turnstile>\<^sub>C conv1 \<sim> map_converter id id f1 g1 1\<^sub>C
\<I>1, \<I>1' \<turnstile>\<^sub>C conv1 \<surd>
fg = (f1, g1)

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
wiring \<I>2 \<I>2' conv2 fg'
[PROOF STEP]
obtain f2 g2
    where conv2: "\<I>2,\<I>2' \<turnstile>\<^sub>C conv2 \<sim> map_converter id id f2 g2 1\<^sub>C"
      and WT2: "\<I>2, \<I>2' \<turnstile>\<^sub>C conv2 \<surd>"
      and [simp]: "fg' = (f2, g2)"
[PROOF STATE]
proof (prove)
using this:
wiring \<I>2 \<I>2' conv2 fg'

goal (1 subgoal):
 1. (\<And>f2 g2. \<lbrakk>\<I>2,\<I>2' \<turnstile>\<^sub>C conv2 \<sim> map_converter id id f2 g2 1\<^sub>C; \<I>2, \<I>2' \<turnstile>\<^sub>C conv2 \<surd>; fg' = (f2, g2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
\<I>2,\<I>2' \<turnstile>\<^sub>C conv2 \<sim> map_converter id id f2 g2 1\<^sub>C
\<I>2, \<I>2' \<turnstile>\<^sub>C conv2 \<surd>
fg' = (f2, g2)

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
from eq_\<I>_converterD_WT1[OF conv1 WT1]
[PROOF STATE]
proof (chain)
picking this:
\<I>1, \<I>1' \<turnstile>\<^sub>C map_converter id id f1 g1 1\<^sub>C \<surd>
[PROOF STEP]
have \<I>1: "\<I>1 \<le> map_\<I> f1 g1 \<I>1'"
[PROOF STATE]
proof (prove)
using this:
\<I>1, \<I>1' \<turnstile>\<^sub>C map_converter id id f1 g1 1\<^sub>C \<surd>

goal (1 subgoal):
 1. \<I>1 \<le> map_\<I> f1 g1 \<I>1'
[PROOF STEP]
by(rule WT_map_converter_idD)
[PROOF STATE]
proof (state)
this:
\<I>1 \<le> map_\<I> f1 g1 \<I>1'

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
from eq_\<I>_converterD_WT1[OF conv2 WT2]
[PROOF STATE]
proof (chain)
picking this:
\<I>2, \<I>2' \<turnstile>\<^sub>C map_converter id id f2 g2 1\<^sub>C \<surd>
[PROOF STEP]
have \<I>2: "\<I>2 \<le> map_\<I> f2 g2 \<I>2'"
[PROOF STATE]
proof (prove)
using this:
\<I>2, \<I>2' \<turnstile>\<^sub>C map_converter id id f2 g2 1\<^sub>C \<surd>

goal (1 subgoal):
 1. \<I>2 \<le> map_\<I> f2 g2 \<I>2'
[PROOF STEP]
by(rule WT_map_converter_idD)
[PROOF STATE]
proof (state)
this:
\<I>2 \<le> map_\<I> f2 g2 \<I>2'

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
have WT': "\<I>1 \<oplus>\<^sub>\<I> \<I>2, \<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> \<I>2, \<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C \<surd>
[PROOF STEP]
by(auto intro!: WT_converter_map_converter WT_converter_mono[OF WT_converter_id order_refl] \<I>1 \<I>2)
[PROOF STATE]
proof (state)
this:
\<I>1 \<oplus>\<^sub>\<I> \<I>2, \<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C \<surd>

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
have "\<I>1 \<oplus>\<^sub>\<I> \<I>2, \<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C conv1 |\<^sub>= conv2 \<sim> map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C conv1 |\<^sub>= conv2 \<sim> map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C
[PROOF STEP]
using conv1 conv2
[PROOF STATE]
proof (prove)
using this:
\<I>1,\<I>1' \<turnstile>\<^sub>C conv1 \<sim> map_converter id id f1 g1 1\<^sub>C
\<I>2,\<I>2' \<turnstile>\<^sub>C conv2 \<sim> map_converter id id f2 g2 1\<^sub>C

goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C conv1 |\<^sub>= conv2 \<sim> map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C
[PROOF STEP]
by(rule parallel_converter2_eq_\<I>_cong)
[PROOF STATE]
proof (state)
this:
\<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C conv1 |\<^sub>= conv2 \<sim> map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C conv1 |\<^sub>= conv2 \<sim> map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
have "map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C = (1\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C = (1\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C
[PROOF STEP]
by(simp add: parallel_converter2_map2_out parallel_converter2_map1_out map_sum.comp sum.map_id0 comp_converter_map_converter2[of _ id id, simplified] comp_converter_id_right)
[PROOF STATE]
proof (state)
this:
map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C = (1\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_converter id id f1 g1 1\<^sub>C |\<^sub>= map_converter id id f2 g2 1\<^sub>C = (1\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
have "\<I>1 \<oplus>\<^sub>\<I> \<I>2, \<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C \<dots> \<sim> 1\<^sub>C \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C (1\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C \<sim> 1\<^sub>C \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C
[PROOF STEP]
by(rule eq_\<I>_comp_cong[OF parallel_converter2_id_id])(rule eq_\<I>_converter_reflI[OF WT'])
[PROOF STATE]
proof (state)
this:
\<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C (1\<^sub>C |\<^sub>= 1\<^sub>C) \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C \<sim> 1\<^sub>C \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C conv1 |\<^sub>= conv2 \<sim> 1\<^sub>C \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C conv1 |\<^sub>= conv2 \<sim> 1\<^sub>C \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
using WT1 WT2
[PROOF STATE]
proof (prove)
using this:
\<I>1 \<oplus>\<^sub>\<I> \<I>2,\<I>1' \<oplus>\<^sub>\<I> \<I>2' \<turnstile>\<^sub>C conv1 |\<^sub>= conv2 \<sim> 1\<^sub>C \<odot> map_converter id id (map_sum f1 f2) (map_sum g1 g2) 1\<^sub>C
\<I>1, \<I>1' \<turnstile>\<^sub>C conv1 \<surd>
\<I>2, \<I>2' \<turnstile>\<^sub>C conv2 \<surd>

goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')
[PROOF STEP]
by(auto simp add: parallel2_wiring_simps comp_converter_id_left intro!: wiringI WT_converter_parallel_converter2)
[PROOF STATE]
proof (state)
this:
wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>1' \<oplus>\<^sub>\<I> \<I>2') (conv1 |\<^sub>= conv2) (fg |\<^sub>w fg')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_parallel2 [simp]:
  "apply_wiring (fg |\<^sub>w fg') (res1 \<oplus>\<^sub>O res2) = (apply_wiring fg res1 \<oplus>\<^sub>O apply_wiring fg' res2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_wiring (fg |\<^sub>w fg') (res1 \<oplus>\<^sub>O res2) = apply_wiring fg res1 \<oplus>\<^sub>O apply_wiring fg' res2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. apply_wiring (fg |\<^sub>w fg') (res1 \<oplus>\<^sub>O res2) = apply_wiring fg res1 \<oplus>\<^sub>O apply_wiring fg' res2
[PROOF STEP]
have[simp]: "fg = (f1, g1) \<Longrightarrow> fg' = (f2, g2) \<Longrightarrow>
       map_spmf (map_prod (map_sum g1 g2) id) ((res1 \<oplus>\<^sub>O res2) s (map_sum f1 f2 q)) =
       ((\<lambda>s q. map_spmf (map_prod g1 id) (res1 s (f1 q))) \<oplus>\<^sub>O (\<lambda>s q. map_spmf (map_prod g2 id) (res2 s (f2 q)))) s q" for f1 g1 f2 g2 s q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fg = (f1, g1); fg' = (f2, g2)\<rbrakk> \<Longrightarrow> map_spmf (map_prod (map_sum g1 g2) id) ((res1 \<oplus>\<^sub>O res2) s (map_sum f1 f2 q)) = ((\<lambda>s q. map_spmf (map_prod g1 id) (res1 s (f1 q))) \<oplus>\<^sub>O (\<lambda>s q. map_spmf (map_prod g2 id) (res2 s (f2 q)))) s q
[PROOF STEP]
by(cases q)(simp_all add: spmf.map_comp o_def apfst_def prod.map_comp split!:sum.splits)
[PROOF STATE]
proof (state)
this:
\<lbrakk>fg = (?f1.0, ?g1.0); fg' = (?f2.0, ?g2.0)\<rbrakk> \<Longrightarrow> map_spmf (map_prod (map_sum ?g1.0 ?g2.0) id) ((res1 \<oplus>\<^sub>O res2) ?s (map_sum ?f1.0 ?f2.0 ?q)) = ((\<lambda>s q. map_spmf (map_prod ?g1.0 id) (res1 s (?f1.0 q))) \<oplus>\<^sub>O (\<lambda>s q. map_spmf (map_prod ?g2.0 id) (res2 s (?f2.0 q)))) ?s ?q

goal (1 subgoal):
 1. apply_wiring (fg |\<^sub>w fg') (res1 \<oplus>\<^sub>O res2) = apply_wiring fg res1 \<oplus>\<^sub>O apply_wiring fg' res2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_wiring (fg |\<^sub>w fg') (res1 \<oplus>\<^sub>O res2) = apply_wiring fg res1 \<oplus>\<^sub>O apply_wiring fg' res2
[PROOF STEP]
by(cases fg; cases fg') (clarsimp simp add: parallel2_wiring_simps apply_wiring_simps fun_eq_iff map_fun_def o_def)
[PROOF STATE]
proof (state)
this:
apply_wiring (fg |\<^sub>w fg') (res1 \<oplus>\<^sub>O res2) = apply_wiring fg res1 \<oplus>\<^sub>O apply_wiring fg' res2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_comp_wiring [simp]: "apply_wiring (fg \<circ>\<^sub>w fg') res = apply_wiring fg (apply_wiring fg' res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_wiring (fg \<circ>\<^sub>w fg') res = apply_wiring fg (apply_wiring fg' res)
[PROOF STEP]
by(cases fg; cases fg')(simp add: comp_wiring_simps apply_wiring_simps map_fun_def fun_eq_iff spmf.map_comp prod.map_comp o_def id_def)


[STATEMENT]
lemma wiring_lassocr [simp, wiring_intro]:
  "wiring ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) lassocr\<^sub>C lassocr\<^sub>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) lassocr\<^sub>C lassocr\<^sub>w
[PROOF STEP]
unfolding lassocr\<^sub>C_def lassocr\<^sub>w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) (map_converter rsuml lsumr id id 1\<^sub>C) (rsuml, lsumr)
[PROOF STEP]
by(subst map_converter_id_move_right)(auto intro!: wiringI eq_\<I>_converter_reflI WT_converter_map_converter)


[STATEMENT]
lemma wiring_rassocl [simp, wiring_intro]:
  "wiring (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) rassocl\<^sub>C rassocl\<^sub>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) rassocl\<^sub>C rassocl\<^sub>w
[PROOF STEP]
unfolding rassocl\<^sub>C_def rassocl\<^sub>w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> (\<I>2 \<oplus>\<^sub>\<I> \<I>3)) ((\<I>1 \<oplus>\<^sub>\<I> \<I>2) \<oplus>\<^sub>\<I> \<I>3) (map_converter lsumr rsuml id id 1\<^sub>C) (lsumr, rsuml)
[PROOF STEP]
by(subst map_converter_id_move_right)(auto intro!: wiringI eq_\<I>_converter_reflI WT_converter_map_converter)


[STATEMENT]
lemma wiring_swap [simp, wiring_intro]: "wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>2 \<oplus>\<^sub>\<I> \<I>1) swap\<^sub>C swap\<^sub>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>2 \<oplus>\<^sub>\<I> \<I>1) swap\<^sub>C swap\<^sub>w
[PROOF STEP]
unfolding swap\<^sub>C_def swap\<^sub>w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wiring (\<I>1 \<oplus>\<^sub>\<I> \<I>2) (\<I>2 \<oplus>\<^sub>\<I> \<I>1) (map_converter swap_sum swap_sum id id 1\<^sub>C) (swap_sum, swap_sum)
[PROOF STEP]
by(subst map_converter_id_move_right)(auto intro!: wiringI eq_\<I>_converter_reflI WT_converter_map_converter)


[STATEMENT]
lemma apply_lassocr\<^sub>w [simp]: "apply_wiring lassocr\<^sub>w (res1 \<oplus>\<^sub>O res2 \<oplus>\<^sub>O res3) = (res1 \<oplus>\<^sub>O res2) \<oplus>\<^sub>O res3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_wiring lassocr\<^sub>w (res1 \<oplus>\<^sub>O res2 \<oplus>\<^sub>O res3) = (res1 \<oplus>\<^sub>O res2) \<oplus>\<^sub>O res3
[PROOF STEP]
by(simp add: apply_wiring_def lassocr\<^sub>w_def map_rsuml_plus_oracle)


[STATEMENT]
lemma apply_rassocl\<^sub>w [simp]: "apply_wiring rassocl\<^sub>w ((res1 \<oplus>\<^sub>O res2) \<oplus>\<^sub>O res3) = res1 \<oplus>\<^sub>O res2 \<oplus>\<^sub>O res3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_wiring rassocl\<^sub>w ((res1 \<oplus>\<^sub>O res2) \<oplus>\<^sub>O res3) = res1 \<oplus>\<^sub>O res2 \<oplus>\<^sub>O res3
[PROOF STEP]
by(simp add: apply_wiring_def rassocl\<^sub>w_def map_lsumr_plus_oracle)


[STATEMENT]
lemma apply_swap\<^sub>w [simp]: "apply_wiring swap\<^sub>w (res1 \<oplus>\<^sub>O res2) = res2 \<oplus>\<^sub>O res1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_wiring swap\<^sub>w (res1 \<oplus>\<^sub>O res2) = res2 \<oplus>\<^sub>O res1
[PROOF STEP]
by(simp add: apply_wiring_def swap\<^sub>w_def map_swap_sum_plus_oracle)


[STATEMENT]
lemma  dep_var_set_self_empty:
  fixes PROB vs
  assumes "dep_var_set PROB vs vs"
  shows "(vs = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB vs vs

goal (1 subgoal):
 1. vs = {}
[PROOF STEP]
unfolding dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
disjnt vs vs \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs \<and> dep PROB v1 v2)

goal (1 subgoal):
 1. vs = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. disjnt vs vs \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs \<and> dep PROB v1 v2) \<Longrightarrow> vs = {}
[PROOF STEP]
obtain v1 v2 where
    "v1 \<in> vs" "v2 \<in> vs" "disjnt vs vs" "dep PROB v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> vs; v2 \<in> vs; disjnt vs vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB vs vs

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> vs; v2 \<in> vs; disjnt vs vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
disjnt vs vs \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs \<and> dep PROB v1 v2)

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> vs; v2 \<in> vs; disjnt vs vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<in> vs
v2 \<in> vs
disjnt vs vs
dep PROB v1 v2

goal (1 subgoal):
 1. disjnt vs vs \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs \<and> dep PROB v1 v2) \<Longrightarrow> vs = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> vs
v2 \<in> vs
disjnt vs vs
dep PROB v1 v2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v1 \<in> vs
v2 \<in> vs
disjnt vs vs
dep PROB v1 v2

goal (1 subgoal):
 1. vs = {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vs = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DEP_REFL:
  fixes PROB
  shows "reflexive (\<lambda>v v'. dep PROB v v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive (dep PROB)
[PROOF STEP]
unfolding dep_def reflexive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<exists>a. a \<in> PROB \<and> (x \<in> fmdom' (fst a) \<and> x \<in> fmdom' (snd a) \<or> x \<in> fmdom' (snd a) \<and> x \<in> fmdom' (snd a))) \<or> x = x
[PROOF STEP]
by presburger

\<comment> \<open>NOTE added lemma.\<close>


[STATEMENT]
lemma NEQ_DEP_IMP_IN_DOM_i:
  fixes a v
  assumes "a \<in> PROB" "v \<in> fmdom' (fst a)"
  shows "v \<in> prob_dom PROB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
have "v \<in> fmdom' (fst a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> fmdom' (fst a)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (fst a)

goal (1 subgoal):
 1. v \<in> fmdom' (fst a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> fmdom' (fst a)

goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> fmdom' (fst a)

goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
have "fmdom' (fst a) \<subseteq> prob_dom PROB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmdom' (fst a) \<subseteq> prob_dom PROB
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB

goal (1 subgoal):
 1. fmdom' (fst a) \<subseteq> prob_dom PROB
[PROOF STEP]
unfolding prob_dom_def action_dom_def
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB

goal (1 subgoal):
 1. fmdom' (fst a) \<subseteq> (\<Union>(s1, s2)\<in>PROB. fmdom' s1 \<union> fmdom' s2)
[PROOF STEP]
using case_prod_beta'
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB
(\<lambda>(x, y). ?f x y) = (\<lambda>x. ?f (fst x) (snd x))

goal (1 subgoal):
 1. fmdom' (fst a) \<subseteq> (\<Union>(s1, s2)\<in>PROB. fmdom' s1 \<union> fmdom' s2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fmdom' (fst a) \<subseteq> prob_dom PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<in> fmdom' (fst a)
fmdom' (fst a) \<subseteq> prob_dom PROB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (fst a)
fmdom' (fst a) \<subseteq> prob_dom PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> prob_dom PROB

goal:
No subgoals!
[PROOF STEP]
qed

\<comment> \<open>NOTE added lemma.\<close>


[STATEMENT]
lemma NEQ_DEP_IMP_IN_DOM_ii:
  fixes a v
  assumes "a \<in> PROB" "v \<in> fmdom' (snd a)"
  shows "v \<in> prob_dom PROB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
have "v \<in> fmdom' (snd a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> fmdom' (snd a)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> fmdom' (snd a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
have "fmdom' (snd a) \<subseteq> prob_dom PROB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmdom' (snd a) \<subseteq> prob_dom PROB
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB

goal (1 subgoal):
 1. fmdom' (snd a) \<subseteq> prob_dom PROB
[PROOF STEP]
unfolding prob_dom_def action_dom_def
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB

goal (1 subgoal):
 1. fmdom' (snd a) \<subseteq> (\<Union>(s1, s2)\<in>PROB. fmdom' s1 \<union> fmdom' s2)
[PROOF STEP]
using case_prod_beta'
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB
(\<lambda>(x, y). ?f x y) = (\<lambda>x. ?f (fst x) (snd x))

goal (1 subgoal):
 1. fmdom' (snd a) \<subseteq> (\<Union>(s1, s2)\<in>PROB. fmdom' s1 \<union> fmdom' s2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fmdom' (snd a) \<subseteq> prob_dom PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<in> fmdom' (snd a)
fmdom' (snd a) \<subseteq> prob_dom PROB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (snd a)
fmdom' (snd a) \<subseteq> prob_dom PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> prob_dom PROB

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma NEQ_DEP_IMP_IN_DOM:
  fixes PROB :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) set" and  v v'
  assumes "\<not>(v = v')" "(dep PROB v v')"
  shows "(v \<in> (prob_dom PROB) \<and> v' \<in> (prob_dom PROB))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<noteq> v'
dep PROB v v'

goal (1 subgoal):
 1. v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
unfolding dep_def
[PROOF STATE]
proof (prove)
using this:
v \<noteq> v'
(\<exists>a. a \<in> PROB \<and> (v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a))) \<or> v = v'

goal (1 subgoal):
 1. v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
using FDOM_pre_subset_prob_dom_pair FDOM_eff_subset_prob_dom_pair
[PROOF STATE]
proof (prove)
using this:
v \<noteq> v'
(\<exists>a. a \<in> PROB \<and> (v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a))) \<or> v = v'
?a \<in> ?PROB \<Longrightarrow> fmdom' (fst ?a) \<subseteq> prob_dom ?PROB
?a \<in> ?PROB \<Longrightarrow> fmdom' (snd ?a) \<subseteq> prob_dom ?PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>v \<noteq> v'; (\<exists>a. a \<in> PROB \<and> (v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a))) \<or> v = v'; \<And>a PROB. a \<in> PROB \<Longrightarrow> fmdom' (fst a) \<subseteq> prob_dom PROB; \<And>a PROB. a \<in> PROB \<Longrightarrow> fmdom' (snd a) \<subseteq> prob_dom PROB\<rbrakk> \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
obtain a where 1:
    "a \<in> PROB"
    "(v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> PROB; v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<noteq> v'
dep PROB v v'

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> PROB; v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dep_def
[PROOF STATE]
proof (prove)
using this:
v \<noteq> v'
(\<exists>a. a \<in> PROB \<and> (v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a))) \<or> v = v'

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> PROB; v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> PROB
v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)

goal (1 subgoal):
 1. \<lbrakk>v \<noteq> v'; (\<exists>a. a \<in> PROB \<and> (v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a))) \<or> v = v'; \<And>a PROB. a \<in> PROB \<Longrightarrow> fmdom' (fst a) \<subseteq> prob_dom PROB; \<And>a PROB. a \<in> PROB \<Longrightarrow> fmdom' (snd a) \<subseteq> prob_dom PROB\<rbrakk> \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> PROB
v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)
[PROOF STEP]
consider
    (i) "v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a)"
    | (ii) "v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)"
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB
v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)

goal (1 subgoal):
 1. \<lbrakk>v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> thesis; v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> ?thesis; v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<lbrakk>v \<noteq> v'; (\<exists>a. a \<in> PROB \<and> (v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a))) \<or> v = v'; \<And>a PROB. a \<in> PROB \<Longrightarrow> fmdom' (fst a) \<subseteq> prob_dom PROB; \<And>a PROB. a \<in> PROB \<Longrightarrow> fmdom' (snd a) \<subseteq> prob_dom PROB\<rbrakk> \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> ?thesis; v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> ?thesis; v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
 2. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
case i
[PROOF STATE]
proof (state)
this:
v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a)

goal (2 subgoals):
 1. v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
 2. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a)
[PROOF STEP]
have "v \<in> fmdom' (fst a)" "v' \<in> fmdom' (snd a)"
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> fmdom' (fst a) &&& v' \<in> fmdom' (snd a)
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
v \<in> fmdom' (fst a)
v' \<in> fmdom' (snd a)

goal (2 subgoals):
 1. v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
 2. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> fmdom' (fst a)
v' \<in> fmdom' (snd a)
[PROOF STEP]
have "v \<in> prob_dom PROB"  "v' \<in> prob_dom PROB"
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (fst a)
v' \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> prob_dom PROB &&& v' \<in> prob_dom PROB
[PROOF STEP]
using 1 NEQ_DEP_IMP_IN_DOM_i NEQ_DEP_IMP_IN_DOM_ii
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (fst a)
v' \<in> fmdom' (snd a)
a \<in> PROB
v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)
\<lbrakk>?a \<in> ?PROB; ?v \<in> fmdom' (fst ?a)\<rbrakk> \<Longrightarrow> ?v \<in> prob_dom ?PROB
\<lbrakk>?a \<in> ?PROB; ?v \<in> fmdom' (snd ?a)\<rbrakk> \<Longrightarrow> ?v \<in> prob_dom ?PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB &&& v' \<in> prob_dom PROB
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
v \<in> prob_dom PROB
v' \<in> prob_dom PROB

goal (2 subgoals):
 1. v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
 2. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> prob_dom PROB
v' \<in> prob_dom PROB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> prob_dom PROB
v' \<in> prob_dom PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB

goal (1 subgoal):
 1. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
case ii
[PROOF STATE]
proof (state)
this:
v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)
[PROOF STEP]
have "v \<in> fmdom' (snd a)" "v' \<in> fmdom' (snd a)"
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> fmdom' (snd a) &&& v' \<in> fmdom' (snd a)
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
v \<in> fmdom' (snd a)
v' \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> fmdom' (snd a)
v' \<in> fmdom' (snd a)
[PROOF STEP]
have "v \<in> prob_dom PROB"  "v' \<in> prob_dom PROB"
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (snd a)
v' \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v \<in> prob_dom PROB &&& v' \<in> prob_dom PROB
[PROOF STEP]
using 1 NEQ_DEP_IMP_IN_DOM_ii
[PROOF STATE]
proof (prove)
using this:
v \<in> fmdom' (snd a)
v' \<in> fmdom' (snd a)
a \<in> PROB
v \<in> fmdom' (fst a) \<and> v' \<in> fmdom' (snd a) \<or> v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a)
\<lbrakk>?a \<in> ?PROB; ?v \<in> fmdom' (snd ?a)\<rbrakk> \<Longrightarrow> ?v \<in> prob_dom ?PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB &&& v' \<in> prob_dom PROB
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
v \<in> prob_dom PROB
v' \<in> prob_dom PROB

goal (1 subgoal):
 1. v \<in> fmdom' (snd a) \<and> v' \<in> fmdom' (snd a) \<Longrightarrow> v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> prob_dom PROB
v' \<in> prob_dom PROB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> prob_dom PROB
v' \<in> prob_dom PROB

goal (1 subgoal):
 1. v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<in> prob_dom PROB \<and> v' \<in> prob_dom PROB

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dep_sos_imp_mem_dep:
  fixes PROB S vs
  assumes "(dep_var_set PROB (\<Union> S) vs)"
  shows "(\<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
obtain v1 v2 where obtain_v1_v2: "v1 \<in> \<Union>S" "v2 \<in> vs" "disjnt (\<Union>S) vs" "dep PROB v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> \<Union> S; v2 \<in> vs; disjnt (\<Union> S) vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms dep_var_set_def[of PROB "\<Union> S" vs]
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB (\<Union> S) vs
dep_var_set PROB (\<Union> S) vs \<equiv> disjnt (\<Union> S) vs \<and> (\<exists>v1 v2. v1 \<in> \<Union> S \<and> v2 \<in> vs \<and> dep PROB v1 v2)

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> \<Union> S; v2 \<in> vs; disjnt (\<Union> S) vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<in> \<Union> S
v2 \<in> vs
disjnt (\<Union> S) vs
dep PROB v1 v2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v1 \<in> \<Union> S
v2 \<in> vs
disjnt (\<Union> S) vs
dep PROB v1 v2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v1 \<in> \<Union> S
v2 \<in> vs
disjnt (\<Union> S) vs
dep PROB v1 v2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
fix vs'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
assume "vs' \<in> S"
[PROOF STATE]
proof (state)
this:
vs' \<in> S

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vs' \<in> S

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
have "vs' \<subseteq> (\<Union>S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs' \<subseteq> \<Union> S
[PROOF STEP]
using calculation Union_upper
[PROOF STATE]
proof (prove)
using this:
vs' \<in> S
?B \<in> ?A \<Longrightarrow> ?B \<subseteq> \<Union> ?A

goal (1 subgoal):
 1. vs' \<subseteq> \<Union> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vs' \<subseteq> \<Union> S

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vs' \<in> S
vs' \<subseteq> \<Union> S
[PROOF STEP]
have "disjnt vs' vs"
[PROOF STATE]
proof (prove)
using this:
vs' \<in> S
vs' \<subseteq> \<Union> S

goal (1 subgoal):
 1. disjnt vs' vs
[PROOF STEP]
using obtain_v1_v2(3) disjnt_subset1
[PROOF STATE]
proof (prove)
using this:
vs' \<in> S
vs' \<subseteq> \<Union> S
disjnt (\<Union> S) vs
\<lbrakk>disjnt ?X ?Y; ?Z \<subseteq> ?X\<rbrakk> \<Longrightarrow> disjnt ?Z ?Y

goal (1 subgoal):
 1. disjnt vs' vs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
disjnt vs' vs

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?vs'2 \<in> S \<Longrightarrow> disjnt ?vs'2 vs

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> \<Union> S
v2 \<in> vs
disjnt (\<Union> S) vs
dep PROB v1 v2
?vs'2 \<in> S \<Longrightarrow> disjnt ?vs'2 vs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v1 \<in> \<Union> S
v2 \<in> vs
disjnt (\<Union> S) vs
dep PROB v1 v2
?vs'2 \<in> S \<Longrightarrow> disjnt ?vs'2 vs

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs
[PROOF STEP]
unfolding dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
v1 \<in> \<Union> S
v2 \<in> vs
disjnt (\<Union> S) vs
dep PROB v1 v2
?vs'2 \<in> S \<Longrightarrow> disjnt ?vs'2 vs

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> dep PROB v1 v2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs' vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dep_union_imp_or_dep:
  fixes PROB vs vs' vs''
  assumes "(dep_var_set PROB vs (vs' \<union> vs''))"
  shows "(dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
obtain v1 v2 where
    obtain_v1_v2: "v1 \<in> vs" "v2 \<in> vs' \<union> vs''" "disjnt vs (vs' \<union> vs'')" "dep PROB v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> vs; v2 \<in> vs' \<union> vs''; disjnt vs (vs' \<union> vs''); dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms dep_var_set_def[of PROB vs "(vs' \<union> vs'')"]
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB vs (vs' \<union> vs'')
dep_var_set PROB vs (vs' \<union> vs'') \<equiv> disjnt vs (vs' \<union> vs'') \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<union> vs'' \<and> dep PROB v1 v2)

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> vs; v2 \<in> vs' \<union> vs''; disjnt vs (vs' \<union> vs''); dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
      \<comment> \<open>NOTE The proofs for the cases introduced here yield the goal's left and right side
    respectively.\<close>
[PROOF STATE]
proof (state)
this:
v1 \<in> vs
v2 \<in> vs' \<union> vs''
disjnt vs (vs' \<union> vs'')
dep PROB v1 v2

goal (1 subgoal):
 1. dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
consider (i) "v2 \<in> vs'" | (ii) "v2 \<in> vs''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v2 \<in> vs' \<Longrightarrow> thesis; v2 \<in> vs'' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using obtain_v1_v2(2)
[PROOF STATE]
proof (prove)
using this:
v2 \<in> vs' \<union> vs''

goal (1 subgoal):
 1. \<lbrakk>v2 \<in> vs' \<Longrightarrow> thesis; v2 \<in> vs'' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>v2 \<in> vs' \<Longrightarrow> ?thesis; v2 \<in> vs'' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>v2 \<in> vs' \<Longrightarrow> ?thesis; v2 \<in> vs'' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>v2 \<in> vs' \<Longrightarrow> ?thesis; v2 \<in> vs'' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v2 \<in> vs' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
 2. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
case i
[PROOF STATE]
proof (state)
this:
v2 \<in> vs'

goal (2 subgoals):
 1. v2 \<in> vs' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
 2. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
have "vs' \<subseteq> vs' \<union> vs''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs' \<subseteq> vs' \<union> vs''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vs' \<subseteq> vs' \<union> vs''

goal (2 subgoals):
 1. v2 \<in> vs' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
 2. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vs' \<subseteq> vs' \<union> vs''

goal (2 subgoals):
 1. v2 \<in> vs' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
 2. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
have "disjnt (vs' \<union> vs'') vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjnt (vs' \<union> vs'') vs
[PROOF STEP]
using obtain_v1_v2(3) disjnt_sym
[PROOF STATE]
proof (prove)
using this:
disjnt vs (vs' \<union> vs'')
disjnt ?A ?B \<Longrightarrow> disjnt ?B ?A

goal (1 subgoal):
 1. disjnt (vs' \<union> vs'') vs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
disjnt (vs' \<union> vs'') vs

goal (2 subgoals):
 1. v2 \<in> vs' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
 2. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vs' \<subseteq> vs' \<union> vs''
disjnt (vs' \<union> vs'') vs
[PROOF STEP]
have "disjnt vs vs'"
[PROOF STATE]
proof (prove)
using this:
vs' \<subseteq> vs' \<union> vs''
disjnt (vs' \<union> vs'') vs

goal (1 subgoal):
 1. disjnt vs vs'
[PROOF STEP]
using disjnt_subset1 disjnt_sym
[PROOF STATE]
proof (prove)
using this:
vs' \<subseteq> vs' \<union> vs''
disjnt (vs' \<union> vs'') vs
\<lbrakk>disjnt ?X ?Y; ?Z \<subseteq> ?X\<rbrakk> \<Longrightarrow> disjnt ?Z ?Y
disjnt ?A ?B \<Longrightarrow> disjnt ?B ?A

goal (1 subgoal):
 1. disjnt vs vs'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
disjnt vs vs'

goal (2 subgoals):
 1. v2 \<in> vs' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
 2. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
disjnt vs vs'
[PROOF STEP]
have "dep_var_set PROB vs vs'"
[PROOF STATE]
proof (prove)
using this:
disjnt vs vs'

goal (1 subgoal):
 1. dep_var_set PROB vs vs'
[PROOF STEP]
unfolding dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
disjnt vs vs'

goal (1 subgoal):
 1. disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> dep PROB v1 v2)
[PROOF STEP]
using obtain_v1_v2(1, 4) i
[PROOF STATE]
proof (prove)
using this:
disjnt vs vs'
v1 \<in> vs
dep PROB v1 v2
v2 \<in> vs'

goal (1 subgoal):
 1. disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> dep PROB v1 v2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dep_var_set PROB vs vs'

goal (2 subgoals):
 1. v2 \<in> vs' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
 2. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dep_var_set PROB vs vs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB vs vs'

goal (1 subgoal):
 1. dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''

goal (1 subgoal):
 1. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
case ii
[PROOF STATE]
proof (state)
this:
v2 \<in> vs''

goal (1 subgoal):
 1. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v2 \<in> vs''
[PROOF STEP]
have "vs'' \<subseteq> vs' \<union> vs''"
[PROOF STATE]
proof (prove)
using this:
v2 \<in> vs''

goal (1 subgoal):
 1. vs'' \<subseteq> vs' \<union> vs''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vs'' \<subseteq> vs' \<union> vs''

goal (1 subgoal):
 1. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vs'' \<subseteq> vs' \<union> vs''

goal (1 subgoal):
 1. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
have "disjnt (vs' \<union> vs'') vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjnt (vs' \<union> vs'') vs
[PROOF STEP]
using obtain_v1_v2(3) disjnt_sym
[PROOF STATE]
proof (prove)
using this:
disjnt vs (vs' \<union> vs'')
disjnt ?A ?B \<Longrightarrow> disjnt ?B ?A

goal (1 subgoal):
 1. disjnt (vs' \<union> vs'') vs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
disjnt (vs' \<union> vs'') vs

goal (1 subgoal):
 1. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vs'' \<subseteq> vs' \<union> vs''
disjnt (vs' \<union> vs'') vs
[PROOF STEP]
have "disjnt vs vs''"
[PROOF STATE]
proof (prove)
using this:
vs'' \<subseteq> vs' \<union> vs''
disjnt (vs' \<union> vs'') vs

goal (1 subgoal):
 1. disjnt vs vs''
[PROOF STEP]
using disjnt_subset1 disjnt_sym
[PROOF STATE]
proof (prove)
using this:
vs'' \<subseteq> vs' \<union> vs''
disjnt (vs' \<union> vs'') vs
\<lbrakk>disjnt ?X ?Y; ?Z \<subseteq> ?X\<rbrakk> \<Longrightarrow> disjnt ?Z ?Y
disjnt ?A ?B \<Longrightarrow> disjnt ?B ?A

goal (1 subgoal):
 1. disjnt vs vs''
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
disjnt vs vs''

goal (1 subgoal):
 1. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
disjnt vs vs''
[PROOF STEP]
have "dep_var_set PROB vs vs''"
[PROOF STATE]
proof (prove)
using this:
disjnt vs vs''

goal (1 subgoal):
 1. dep_var_set PROB vs vs''
[PROOF STEP]
unfolding dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
disjnt vs vs''

goal (1 subgoal):
 1. disjnt vs vs'' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs'' \<and> dep PROB v1 v2)
[PROOF STEP]
using obtain_v1_v2(1, 4) ii
[PROOF STATE]
proof (prove)
using this:
disjnt vs vs''
v1 \<in> vs
dep PROB v1 v2
v2 \<in> vs''

goal (1 subgoal):
 1. disjnt vs vs'' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs'' \<and> dep PROB v1 v2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dep_var_set PROB vs vs''

goal (1 subgoal):
 1. v2 \<in> vs'' \<Longrightarrow> dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dep_var_set PROB vs vs''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB vs vs''

goal (1 subgoal):
 1. dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dep_var_set PROB vs vs' \<or> dep_var_set PROB vs vs''

goal:
No subgoals!
[PROOF STEP]
qed

\<comment> \<open>NOTE This is symmetrical to `dep\_sos\_imp\_mem\_dep` w.r.t to `vs` and @{term "\<Union> S"}.\<close>