[STATEMENT]
lemma arc_in_partition:
  assumes "arc x"
    shows "x \<le> -y \<or> x \<le> --y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - y \<or> x \<le> - - y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> - y \<or> x \<le> - - y
[PROOF STEP]
have 1: "x * top * x\<^sup>T \<le> 1 \<and> x\<^sup>T * top * x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x)
[PROOF STEP]
using assms arc_expanded
[PROOF STATE]
proof (prove)
using this:
arc x
arc ?x = (coreflexive (?x * top * ?x\<^sup>T) \<and> coreflexive (?x\<^sup>T * top * ?x) \<and> times_top_class.total (top * ?x))

goal (1 subgoal):
 1. coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x)

goal (1 subgoal):
 1. x \<le> - y \<or> x \<le> - - y
[PROOF STEP]
have "\<not> x \<le> --y \<longrightarrow> x \<le> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x \<le> - - y \<longrightarrow> x \<le> - y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
assume "\<not> x \<le> --y"
[PROOF STATE]
proof (state)
this:
\<not> x \<le> - - y

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
hence "x \<sqinter> -y \<noteq> bot"
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> - - y

goal (1 subgoal):
 1. x \<sqinter> - y \<noteq> bot
[PROOF STEP]
using pseudo_complement
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> - - y
(?x \<sqinter> ?y = bot) = (?x \<le> - ?y)

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

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
hence "top * (x \<sqinter> -y) * top = top"
[PROOF STATE]
proof (prove)
using this:
x \<sqinter> - y \<noteq> bot

goal (1 subgoal):
 1. times_top_class.total (top * (x \<sqinter> - y))
[PROOF STEP]
using assms arc_regular tarski
[PROOF STATE]
proof (prove)
using this:
x \<sqinter> - y \<noteq> bot
arc x
arc ?x \<Longrightarrow> regular ?x
\<lbrakk>regular ?x; ?x \<noteq> bot\<rbrakk> \<Longrightarrow> times_top_class.total (top * ?x)

goal (1 subgoal):
 1. times_top_class.total (top * (x \<sqinter> - y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
times_top_class.total (top * (x \<sqinter> - y))

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
hence "x = x \<sqinter> top * (x \<sqinter> -y) * top"
[PROOF STATE]
proof (prove)
using this:
times_top_class.total (top * (x \<sqinter> - y))

goal (1 subgoal):
 1. x = x \<sqinter> top * (x \<sqinter> - y) * top
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = x \<sqinter> top * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = x \<sqinter> top * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... \<le> x \<sqinter> x * ((x \<sqinter> -y) * top)\<^sup>T * (x \<sqinter> -y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> top * (x \<sqinter> - y) * top \<le> x \<sqinter> x * ((x \<sqinter> - y) * top)\<^sup>T * (x \<sqinter> - y) * top
[PROOF STEP]
by (metis dedekind_2 inf.cobounded1 inf.boundedI inf_commute mult_assoc inf.absorb2 top.extremum)
[PROOF STATE]
proof (state)
this:
x \<sqinter> top * (x \<sqinter> - y) * top \<le> x \<sqinter> x * ((x \<sqinter> - y) * top)\<^sup>T * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> top * (x \<sqinter> - y) * top \<le> x \<sqinter> x * ((x \<sqinter> - y) * top)\<^sup>T * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... = x \<sqinter> x * top * (x\<^sup>T \<sqinter> -y\<^sup>T) * (x \<sqinter> -y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> x * ((x \<sqinter> - y) * top)\<^sup>T * (x \<sqinter> - y) * top = x \<sqinter> x * top * (x\<^sup>T \<sqinter> - y\<^sup>T) * (x \<sqinter> - y) * top
[PROOF STEP]
by (simp add: comp_associative conv_complement conv_dist_comp conv_dist_inf)
[PROOF STATE]
proof (state)
this:
x \<sqinter> x * ((x \<sqinter> - y) * top)\<^sup>T * (x \<sqinter> - y) * top = x \<sqinter> x * top * (x\<^sup>T \<sqinter> - y\<^sup>T) * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> x * ((x \<sqinter> - y) * top)\<^sup>T * (x \<sqinter> - y) * top = x \<sqinter> x * top * (x\<^sup>T \<sqinter> - y\<^sup>T) * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... \<le> x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> -y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> x * top * (x\<^sup>T \<sqinter> - y\<^sup>T) * (x \<sqinter> - y) * top \<le> x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> - y) * top
[PROOF STEP]
using inf.sup_right_isotone mult_left_isotone mult_right_isotone
[PROOF STATE]
proof (prove)
using this:
?y \<le> ?x \<Longrightarrow> ?z \<sqinter> ?y \<le> ?z \<sqinter> ?x
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

goal (1 subgoal):
 1. x \<sqinter> x * top * (x\<^sup>T \<sqinter> - y\<^sup>T) * (x \<sqinter> - y) * top \<le> x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> - y) * top
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<sqinter> x * top * (x\<^sup>T \<sqinter> - y\<^sup>T) * (x \<sqinter> - y) * top \<le> x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> x * top * (x\<^sup>T \<sqinter> - y\<^sup>T) * (x \<sqinter> - y) * top \<le> x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... \<le> x \<sqinter> 1 * (x \<sqinter> -y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> - y) * top \<le> x \<sqinter> (1::'a) * (x \<sqinter> - y) * top
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x)

goal (1 subgoal):
 1. x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> - y) * top \<le> x \<sqinter> (1::'a) * (x \<sqinter> - y) * top
[PROOF STEP]
by (metis comp_associative comp_isotone inf.sup_right_isotone mult_1_left mult_semi_associative)
[PROOF STATE]
proof (state)
this:
x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> - y) * top \<le> x \<sqinter> (1::'a) * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> x * top * x\<^sup>T * (x \<sqinter> - y) * top \<le> x \<sqinter> (1::'a) * (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... = x \<sqinter> (x \<sqinter> -y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> (1::'a) * (x \<sqinter> - y) * top = x \<sqinter> (x \<sqinter> - y) * top
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sqinter> (1::'a) * (x \<sqinter> - y) * top = x \<sqinter> (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> (1::'a) * (x \<sqinter> - y) * top = x \<sqinter> (x \<sqinter> - y) * top

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... \<le> (x \<sqinter> -y) * ((x \<sqinter> -y)\<^sup>T * x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> (x \<sqinter> - y) * top \<le> (x \<sqinter> - y) * ((x \<sqinter> - y)\<^sup>T * x)
[PROOF STEP]
by (metis dedekind_1 inf_commute inf_top_right)
[PROOF STATE]
proof (state)
this:
x \<sqinter> (x \<sqinter> - y) * top \<le> (x \<sqinter> - y) * ((x \<sqinter> - y)\<^sup>T * x)

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> (x \<sqinter> - y) * top \<le> (x \<sqinter> - y) * ((x \<sqinter> - y)\<^sup>T * x)

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... \<le> (x \<sqinter> -y) * (x\<^sup>T * x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> - y) * ((x \<sqinter> - y)\<^sup>T * x) \<le> (x \<sqinter> - y) * (x\<^sup>T * x)
[PROOF STEP]
by (simp add: conv_dist_inf mult_left_isotone mult_right_isotone)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - y) * ((x \<sqinter> - y)\<^sup>T * x) \<le> (x \<sqinter> - y) * (x\<^sup>T * x)

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - y) * ((x \<sqinter> - y)\<^sup>T * x) \<le> (x \<sqinter> - y) * (x\<^sup>T * x)

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... \<le> (x \<sqinter> -y) * (x\<^sup>T * top * x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> - y) * (x\<^sup>T * x) \<le> (x \<sqinter> - y) * (x\<^sup>T * top * x)
[PROOF STEP]
by (simp add: mult_assoc mult_right_isotone top_left_mult_increasing)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - y) * (x\<^sup>T * x) \<le> (x \<sqinter> - y) * (x\<^sup>T * top * x)

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - y) * (x\<^sup>T * x) \<le> (x \<sqinter> - y) * (x\<^sup>T * top * x)

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
have "... \<le> x \<sqinter> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> - y) * (x\<^sup>T * top * x) \<le> x \<sqinter> - y
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
coreflexive (x * top * x\<^sup>T) \<and> coreflexive (x\<^sup>T * top * x)

goal (1 subgoal):
 1. (x \<sqinter> - y) * (x\<^sup>T * top * x) \<le> x \<sqinter> - y
[PROOF STEP]
by (metis mult_right_isotone mult_1_right)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> - y) * (x\<^sup>T * top * x) \<le> x \<sqinter> - y

goal (1 subgoal):
 1. \<not> x \<le> - - y \<Longrightarrow> x \<le> - y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<le> x \<sqinter> - y
[PROOF STEP]
show "x \<le> -y"
[PROOF STATE]
proof (prove)
using this:
x \<le> x \<sqinter> - y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> x \<le> - - y \<longrightarrow> x \<le> - y

goal (1 subgoal):
 1. x \<le> - y \<or> x \<le> - - y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> - - y \<longrightarrow> x \<le> - y

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma non_bot_arc_in_partition_xor:
  assumes "arc x"
      and "x \<noteq> bot"
    shows "(x \<le> -y \<and> \<not> x \<le> --y) \<or> (\<not> x \<le> -y \<and> x \<le> --y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - y \<and> \<not> x \<le> - - y \<or> \<not> x \<le> - y \<and> x \<le> - - y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> - y \<and> \<not> x \<le> - - y \<or> \<not> x \<le> - y \<and> x \<le> - - y
[PROOF STEP]
have "x \<le> -y \<and> x \<le> --y \<longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - y \<and> x \<le> - - y \<longrightarrow> False
[PROOF STEP]
by (simp add: assms(2) inf_absorb1 shunting_1_pp)
[PROOF STATE]
proof (state)
this:
x \<le> - y \<and> x \<le> - - y \<longrightarrow> False

goal (1 subgoal):
 1. x \<le> - y \<and> \<not> x \<le> - - y \<or> \<not> x \<le> - y \<and> x \<le> - - y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> - y \<and> x \<le> - - y \<longrightarrow> False

goal (1 subgoal):
 1. x \<le> - y \<and> \<not> x \<le> - - y \<or> \<not> x \<le> - y \<and> x \<le> - - y
[PROOF STEP]
using assms(1) arc_in_partition
[PROOF STATE]
proof (prove)
using this:
x \<le> - y \<and> x \<le> - - y \<longrightarrow> False
arc x
arc ?x \<Longrightarrow> ?x \<le> - ?y \<or> ?x \<le> - - ?y

goal (1 subgoal):
 1. x \<le> - y \<and> \<not> x \<le> - - y \<or> \<not> x \<le> - y \<and> x \<le> - - y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<le> - y \<and> \<not> x \<le> - - y \<or> \<not> x \<le> - y \<and> x \<le> - - y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_in_vector_or_pseudo_complement:
  assumes "point p"
      and "vector v"
    shows "p \<le> --v \<or> p \<le> -v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> - - v \<or> p \<le> - v
[PROOF STEP]
proof (rule disjCI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> - - v
[PROOF STEP]
assume "\<not>(p \<le> -v)"
[PROOF STATE]
proof (state)
this:
\<not> p \<le> - v

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> - - v
[PROOF STEP]
hence "top * (p \<sqinter> --v) = top"
[PROOF STATE]
proof (prove)
using this:
\<not> p \<le> - v

goal (1 subgoal):
 1. surjective (p \<sqinter> - - v)
[PROOF STEP]
by (smt assms bijective_regular regular_closed_inf regular_closed_p shunting_1_pp tarski vector_complement_closed vector_inf_closed vector_mult_closed)
[PROOF STATE]
proof (state)
this:
surjective (p \<sqinter> - - v)

goal (1 subgoal):
 1. \<not> p \<le> - v \<Longrightarrow> p \<le> - - v
[PROOF STEP]
thus "p \<le> --v"
[PROOF STATE]
proof (prove)
using this:
surjective (p \<sqinter> - - v)

goal (1 subgoal):
 1. p \<le> - - v
[PROOF STEP]
by (metis assms(1) epm_3 inf.absorb_iff1 inf.cobounded1 inf_top.right_neutral)
[PROOF STATE]
proof (state)
this:
p \<le> - - v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_points:
  assumes "point x"
    and "point y"
    and "x \<noteq> y"
  shows "x \<sqinter> y = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> y = bot
[PROOF STEP]
by (metis assms order.antisym comp_bijective_complement inf.sup_monoid.add_commute mult_left_one pseudo_complement regular_one_closed point_in_vector_or_pseudo_complement)


[STATEMENT]
lemma point_in_vector_or_complement:
  assumes "point p"
      and "vector v"
      and "regular v"
    shows "p \<le> v \<or> p \<le> -v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> v \<or> p \<le> - v
[PROOF STEP]
using assms point_in_vector_or_pseudo_complement
[PROOF STATE]
proof (prove)
using this:
point p
vector v
regular v
\<lbrakk>point ?p; vector ?v\<rbrakk> \<Longrightarrow> ?p \<le> - - ?v \<or> ?p \<le> - ?v

goal (1 subgoal):
 1. p \<le> v \<or> p \<le> - v
[PROOF STEP]
by fastforce


[STATEMENT]
lemma point_in_vector_sup:
  assumes "point p"
      and "vector v"
      and "regular v"
      and "p \<le> v \<squnion> w"
    shows "p \<le> v \<or> p \<le> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> v \<or> p \<le> w
[PROOF STEP]
by (metis assms inf.absorb1 shunting_var_p sup_commute point_in_vector_or_complement)


[STATEMENT]
lemma point_atomic_vector:
  assumes "point x"
    and "vector y"
    and "regular y"
    and "y \<le> x"
  shows "y = x \<or> y = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = x \<or> y = bot
[PROOF STEP]
proof (cases "x \<le> -y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> - y \<Longrightarrow> y = x \<or> y = bot
 2. \<not> x \<le> - y \<Longrightarrow> y = x \<or> y = bot
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<le> - y

goal (2 subgoals):
 1. x \<le> - y \<Longrightarrow> y = x \<or> y = bot
 2. \<not> x \<le> - y \<Longrightarrow> y = x \<or> y = bot
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> - y

goal (1 subgoal):
 1. y = x \<or> y = bot
[PROOF STEP]
using assms(4) inf.absorb2 pseudo_complement
[PROOF STATE]
proof (prove)
using this:
x \<le> - y
y \<le> x
?b \<le> ?a \<Longrightarrow> ?a \<sqinter> ?b = ?b
(?x \<sqinter> ?y = bot) = (?x \<le> - ?y)

goal (1 subgoal):
 1. y = x \<or> y = bot
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y = x \<or> y = bot

goal (1 subgoal):
 1. \<not> x \<le> - y \<Longrightarrow> y = x \<or> y = bot
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<le> - y \<Longrightarrow> y = x \<or> y = bot
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x \<le> - y

goal (1 subgoal):
 1. \<not> x \<le> - y \<Longrightarrow> y = x \<or> y = bot
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> - y

goal (1 subgoal):
 1. y = x \<or> y = bot
[PROOF STEP]
using assms point_in_vector_or_pseudo_complement
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> - y
point x
vector y
regular y
y \<le> x
\<lbrakk>point ?p; vector ?v\<rbrakk> \<Longrightarrow> ?p \<le> - - ?v \<or> ?p \<le> - ?v

goal (1 subgoal):
 1. y = x \<or> y = bot
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y = x \<or> y = bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_in_vector_or_complement_2:
  assumes "point x"
    and "vector y"
    and "regular y"
    and "\<not> y \<le> -x"
  shows "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
using assms point_in_vector_or_pseudo_complement p_antitone_iff
[PROOF STATE]
proof (prove)
using this:
point x
vector y
regular y
\<not> y \<le> - x
\<lbrakk>point ?p; vector ?v\<rbrakk> \<Longrightarrow> ?p \<le> - - ?v \<or> ?p \<le> - ?v
(?x \<le> - ?y) = (?y \<le> - ?x)

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by fastforce


[STATEMENT]
lemma arc_in_arc_or_complement:
  assumes "arc x"
      and "arc y"
      and "\<not> x \<le> y"
    shows "x \<le> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - y
[PROOF STEP]
using assms arc_in_partition arc_regular
[PROOF STATE]
proof (prove)
using this:
arc x
arc y
\<not> x \<le> y
arc ?x \<Longrightarrow> ?x \<le> - ?y \<or> ?x \<le> - - ?y
arc ?x \<Longrightarrow> regular ?x

goal (1 subgoal):
 1. x \<le> - y
[PROOF STEP]
by force


[STATEMENT]
lemma arc_in_sup_arc:
  assumes "arc x"
      and "arc y"
      and "x \<le> z \<squnion> y"
    shows "x \<le> z \<or> x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> z \<or> x \<le> y
[PROOF STEP]
proof (cases "x \<le> y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
 2. \<not> x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
 2. \<not> x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. x \<le> z \<or> x \<le> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> z \<or> x \<le> y

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x \<le> y

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
[PROOF STEP]
hence "x \<le> -y"
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> y

goal (1 subgoal):
 1. x \<le> - y
[PROOF STEP]
using assms(1,2) arc_in_arc_or_complement
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> y
arc x
arc y
\<lbrakk>arc ?x; arc ?y; \<not> ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x \<le> - ?y

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

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
[PROOF STEP]
hence "x \<le> -y \<sqinter> (z \<squnion> y)"
[PROOF STATE]
proof (prove)
using this:
x \<le> - y

goal (1 subgoal):
 1. x \<le> - y \<sqinter> (z \<squnion> y)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
x \<le> - y
x \<le> z \<squnion> y

goal (1 subgoal):
 1. x \<le> - y \<sqinter> (z \<squnion> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> - y \<sqinter> (z \<squnion> y)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
[PROOF STEP]
hence "x \<le> z"
[PROOF STATE]
proof (prove)
using this:
x \<le> - y \<sqinter> (z \<squnion> y)

goal (1 subgoal):
 1. x \<le> z
[PROOF STEP]
by (metis inf.boundedE inf.sup_monoid.add_commute maddux_3_13 sup_commute)
[PROOF STATE]
proof (state)
this:
x \<le> z

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x \<le> z \<or> x \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> z

goal (1 subgoal):
 1. x \<le> z \<or> x \<le> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> z \<or> x \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma different_arc_in_sup_arc:
  assumes "arc x"
      and "arc y"
      and "x \<le> z \<squnion> y"
      and "x \<noteq> y"
    shows "x \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> z
[PROOF STEP]
have "x \<le> -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - y
[PROOF STEP]
using arc_in_arc_or_complement assms(1,2,4) order.eq_iff p_antitone_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>arc ?x; arc ?y; \<not> ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x \<le> - ?y
arc x
arc y
x \<noteq> y
(?a = ?b) = (?a \<le> ?b \<and> ?b \<le> ?a)
(?x \<le> - ?y) = (?y \<le> - ?x)

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

goal (1 subgoal):
 1. x \<le> z
[PROOF STEP]
hence "x \<le> -y \<sqinter> (z \<squnion> y)"
[PROOF STATE]
proof (prove)
using this:
x \<le> - y

goal (1 subgoal):
 1. x \<le> - y \<sqinter> (z \<squnion> y)
[PROOF STEP]
using assms arc_in_sup_arc
[PROOF STATE]
proof (prove)
using this:
x \<le> - y
arc x
arc y
x \<le> z \<squnion> y
x \<noteq> y
\<lbrakk>arc ?x; arc ?y; ?x \<le> ?z \<squnion> ?y\<rbrakk> \<Longrightarrow> ?x \<le> ?z \<or> ?x \<le> ?y

goal (1 subgoal):
 1. x \<le> - y \<sqinter> (z \<squnion> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> - y \<sqinter> (z \<squnion> y)

goal (1 subgoal):
 1. x \<le> z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> - y \<sqinter> (z \<squnion> y)

goal (1 subgoal):
 1. x \<le> z
[PROOF STEP]
by (metis order_lesseq_imp p_inf_sup_below sup_commute)
[PROOF STATE]
proof (state)
this:
x \<le> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arc_not_bot:
  "arc x \<Longrightarrow> x \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc x \<Longrightarrow> x \<noteq> bot
[PROOF STEP]
using consistent mult_right_zero
[PROOF STATE]
proof (prove)
using this:
bot \<noteq> top
?x * bot = bot

goal (1 subgoal):
 1. arc x \<Longrightarrow> x \<noteq> bot
[PROOF STEP]
by auto


[STATEMENT]
lemma point_not_bot:
  "point p \<Longrightarrow> p \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point p \<Longrightarrow> p \<noteq> bot
[PROOF STEP]
using consistent
[PROOF STATE]
proof (prove)
using this:
bot \<noteq> top

goal (1 subgoal):
 1. point p \<Longrightarrow> p \<noteq> bot
[PROOF STEP]
by force


[STATEMENT]
lemma arc_in_partition_xor:
  "arc x \<Longrightarrow> (x \<le> -y \<and> \<not> x \<le> --y) \<or> (\<not> x \<le> -y \<and> x \<le> --y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arc x \<Longrightarrow> x \<le> - y \<and> \<not> x \<le> - - y \<or> \<not> x \<le> - y \<and> x \<le> - - y
[PROOF STEP]
by (simp add: non_bot_arc_in_partition_xor arc_not_bot)


[STATEMENT]
lemma obs_intraE:
  assumes "n' \<in> obs_intra n S"
  obtains as where "n -as\<rightarrow>\<^sub>\<iota>* n'" and "\<forall>nx \<in> set(sourcenodes as). nx \<notin> S" and "n' \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as. \<lbrakk>n -as\<rightarrow>\<^sub>\<iota>* n'; \<forall>nx\<in>set (sourcenodes as). nx \<notin> S; n' \<in> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>n' \<in> obs_intra n S\<close>
[PROOF STATE]
proof (prove)
using this:
n' \<in> obs_intra n S

goal (1 subgoal):
 1. (\<And>as. \<lbrakk>n -as\<rightarrow>\<^sub>\<iota>* n'; \<forall>nx\<in>set (sourcenodes as). nx \<notin> S; n' \<in> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:obs_intra.cases)


[STATEMENT]
lemma n_in_obs_intra:
  assumes "valid_node n" and "n \<in> S" shows "obs_intra n S = {n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
from \<open>valid_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node n
[PROOF STEP]
have "n -[]\<rightarrow>* n"
[PROOF STATE]
proof (prove)
using this:
valid_node n

goal (1 subgoal):
 1. n -[]\<rightarrow>* n
[PROOF STEP]
by(rule empty_path)
[PROOF STATE]
proof (state)
this:
n -[]\<rightarrow>* n

goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
hence "n -[]\<rightarrow>\<^sub>\<iota>* n"
[PROOF STATE]
proof (prove)
using this:
n -[]\<rightarrow>* n

goal (1 subgoal):
 1. n -[]\<rightarrow>\<^sub>\<iota>* n
[PROOF STEP]
by(simp add:intra_path_def)
[PROOF STATE]
proof (state)
this:
n -[]\<rightarrow>\<^sub>\<iota>* n

goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
with \<open>n \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> S
n -[]\<rightarrow>\<^sub>\<iota>* n
[PROOF STEP]
have "n \<in> obs_intra n S"
[PROOF STATE]
proof (prove)
using this:
n \<in> S
n -[]\<rightarrow>\<^sub>\<iota>* n

goal (1 subgoal):
 1. n \<in> obs_intra n S
[PROOF STEP]
by(fastforce elim:obs_intra_elem simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
n \<in> obs_intra n S

goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n \<in> obs_intra n S

goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
fix n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
assume "n' \<in> obs_intra n S"
[PROOF STATE]
proof (state)
this:
n' \<in> obs_intra n S

goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
have "n' = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' = n
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n' \<noteq> n \<Longrightarrow> False
[PROOF STEP]
assume "n' \<noteq> n"
[PROOF STATE]
proof (state)
this:
n' \<noteq> n

goal (1 subgoal):
 1. n' \<noteq> n \<Longrightarrow> False
[PROOF STEP]
from \<open>n' \<in> obs_intra n S\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<in> obs_intra n S
[PROOF STEP]
obtain as where "n -as\<rightarrow>\<^sub>\<iota>* n'"
        and "\<forall>nx \<in> set(sourcenodes as). nx \<notin> S"
        and "n' \<in> S"
[PROOF STATE]
proof (prove)
using this:
n' \<in> obs_intra n S

goal (1 subgoal):
 1. (\<And>as. \<lbrakk>n -as\<rightarrow>\<^sub>\<iota>* n'; \<forall>nx\<in>set (sourcenodes as). nx \<notin> S; n' \<in> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:obs_intra.cases)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>\<^sub>\<iota>* n'
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S
n' \<in> S

goal (1 subgoal):
 1. n' \<noteq> n \<Longrightarrow> False
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -as\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. n -as\<rightarrow>* n'
[PROOF STEP]
by(simp add:intra_path_def)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n'

goal (1 subgoal):
 1. n' \<noteq> n \<Longrightarrow> False
[PROOF STEP]
from this \<open>\<forall>nx \<in> set(sourcenodes as). nx \<notin> S\<close> \<open>n' \<noteq> n\<close> \<open>n \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S
n' \<noteq> n
n \<in> S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S
n' \<noteq> n
n \<in> S

goal (1 subgoal):
 1. False
[PROOF STEP]
proof(induct rule:path.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>nx\<in>set (sourcenodes []). nx \<notin> S; n \<noteq> n; n \<in> S\<rbrakk> \<Longrightarrow> False
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>nx\<in>set (sourcenodes as). nx \<notin> S; n' \<noteq> n''; n'' \<in> S\<rbrakk> \<Longrightarrow> False; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S; n' \<noteq> n; n \<in> S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Cons_path n'' as n' a n)
[PROOF STATE]
proof (state)
this:
n'' -as\<rightarrow>* n'
\<lbrakk>\<forall>nx\<in>set (sourcenodes as). nx \<notin> S; n' \<noteq> n''; n'' \<in> S\<rbrakk> \<Longrightarrow> False
valid_edge a
sourcenode a = n
targetnode a = n''
\<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S
n' \<noteq> n
n \<in> S

goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>nx\<in>set (sourcenodes []). nx \<notin> S; n \<noteq> n; n \<in> S\<rbrakk> \<Longrightarrow> False
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>nx\<in>set (sourcenodes as). nx \<notin> S; n' \<noteq> n''; n'' \<in> S\<rbrakk> \<Longrightarrow> False; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S; n' \<noteq> n; n \<in> S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>\<forall>nx\<in>set (sourcenodes (a#as)). nx \<notin> S\<close> \<open>sourcenode a = n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S
sourcenode a = n
[PROOF STEP]
have "n \<notin> S"
[PROOF STATE]
proof (prove)
using this:
\<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S
sourcenode a = n

goal (1 subgoal):
 1. n \<notin> S
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
n \<notin> S

goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>nx\<in>set (sourcenodes []). nx \<notin> S; n \<noteq> n; n \<in> S\<rbrakk> \<Longrightarrow> False
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>nx\<in>set (sourcenodes as). nx \<notin> S; n' \<noteq> n''; n'' \<in> S\<rbrakk> \<Longrightarrow> False; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S; n' \<noteq> n; n \<in> S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>n \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> S
n \<notin> S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<in> S
n \<notin> S

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>nx\<in>set (sourcenodes []). nx \<notin> S; n \<noteq> n; n \<in> S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n' = n

goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?n'2 \<in> obs_intra n S \<Longrightarrow> ?n'2 = n

goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
with \<open>n \<in> obs_intra n S\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> obs_intra n S
?n'2 \<in> obs_intra n S \<Longrightarrow> ?n'2 = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> obs_intra n S
?n'2 \<in> obs_intra n S \<Longrightarrow> ?n'2 = n

goal (1 subgoal):
 1. obs_intra n S = {n}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
obs_intra n S = {n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_obs_intra_valid:
  assumes "n' \<in> obs_intra n S" shows "valid_node n" and "valid_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_node n &&& valid_node n'
[PROOF STEP]
using \<open>n' \<in> obs_intra n S\<close>
[PROOF STATE]
proof (prove)
using this:
n' \<in> obs_intra n S

goal (1 subgoal):
 1. valid_node n &&& valid_node n'
[PROOF STEP]
by(auto elim!:obs_intraE intro:path_valid_node simp:intra_path_def)


[STATEMENT]
lemma edge_obs_intra_subset:
  assumes "valid_edge a" and "intra_kind (kind a)" and "sourcenode a \<notin> S"
  shows "obs_intra (targetnode a) S \<subseteq> obs_intra (sourcenode a) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_intra (targetnode a) S \<subseteq> obs_intra (sourcenode a) S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> obs_intra (targetnode a) S \<Longrightarrow> x \<in> obs_intra (sourcenode a) S
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> obs_intra (targetnode a) S \<Longrightarrow> x \<in> obs_intra (sourcenode a) S
[PROOF STEP]
assume "n \<in> obs_intra (targetnode a) S"
[PROOF STATE]
proof (state)
this:
n \<in> obs_intra (targetnode a) S

goal (1 subgoal):
 1. \<And>x. x \<in> obs_intra (targetnode a) S \<Longrightarrow> x \<in> obs_intra (sourcenode a) S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> obs_intra (targetnode a) S
[PROOF STEP]
obtain as where "targetnode a -as\<rightarrow>\<^sub>\<iota>* n"
    and all:"\<forall>nx \<in> set(sourcenodes as). nx \<notin> S" and "n \<in> S"
[PROOF STATE]
proof (prove)
using this:
n \<in> obs_intra (targetnode a) S

goal (1 subgoal):
 1. (\<And>as. \<lbrakk>targetnode a -as\<rightarrow>\<^sub>\<iota>* n; \<forall>nx\<in>set (sourcenodes as). nx \<notin> S; n \<in> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule obs_intraE)
[PROOF STATE]
proof (state)
this:
targetnode a -as\<rightarrow>\<^sub>\<iota>* n
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S
n \<in> S

goal (1 subgoal):
 1. \<And>x. x \<in> obs_intra (targetnode a) S \<Longrightarrow> x \<in> obs_intra (sourcenode a) S
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>intra_kind (kind a)\<close> \<open>targetnode a -as\<rightarrow>\<^sub>\<iota>* n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
intra_kind (kind a)
targetnode a -as\<rightarrow>\<^sub>\<iota>* n
[PROOF STEP]
have "sourcenode a -[a]@as\<rightarrow>\<^sub>\<iota>* n"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
intra_kind (kind a)
targetnode a -as\<rightarrow>\<^sub>\<iota>* n

goal (1 subgoal):
 1. sourcenode a -[a] @ as\<rightarrow>\<^sub>\<iota>* n
[PROOF STEP]
by(fastforce intro:Cons_path simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
sourcenode a -[a] @ as\<rightarrow>\<^sub>\<iota>* n

goal (1 subgoal):
 1. \<And>x. x \<in> obs_intra (targetnode a) S \<Longrightarrow> x \<in> obs_intra (sourcenode a) S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sourcenode a -[a] @ as\<rightarrow>\<^sub>\<iota>* n

goal (1 subgoal):
 1. \<And>x. x \<in> obs_intra (targetnode a) S \<Longrightarrow> x \<in> obs_intra (sourcenode a) S
[PROOF STEP]
from all \<open>sourcenode a \<notin> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S
sourcenode a \<notin> S
[PROOF STEP]
have "\<forall>nx \<in> set(sourcenodes (a#as)). nx \<notin> S"
[PROOF STATE]
proof (prove)
using this:
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S
sourcenode a \<notin> S

goal (1 subgoal):
 1. \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S

goal (1 subgoal):
 1. \<And>x. x \<in> obs_intra (targetnode a) S \<Longrightarrow> x \<in> obs_intra (sourcenode a) S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sourcenode a -[a] @ as\<rightarrow>\<^sub>\<iota>* n
\<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S
[PROOF STEP]
show "n \<in> obs_intra (sourcenode a) S"
[PROOF STATE]
proof (prove)
using this:
sourcenode a -[a] @ as\<rightarrow>\<^sub>\<iota>* n
\<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S

goal (1 subgoal):
 1. n \<in> obs_intra (sourcenode a) S
[PROOF STEP]
using \<open>n \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
sourcenode a -[a] @ as\<rightarrow>\<^sub>\<iota>* n
\<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> S
n \<in> S

goal (1 subgoal):
 1. n \<in> obs_intra (sourcenode a) S
[PROOF STEP]
by(fastforce intro:obs_intra_elem)
[PROOF STATE]
proof (state)
this:
n \<in> obs_intra (sourcenode a) S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_obs_intra_subset:
  assumes "n -as\<rightarrow>\<^sub>\<iota>* n'" and "\<forall>n' \<in> set(sourcenodes as). n' \<notin> S"
  shows "obs_intra n' S \<subseteq> obs_intra n S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -as\<rightarrow>* n'" and "\<forall>a \<in> set as. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. n -as\<rightarrow>* n' &&& \<forall>a\<in>set as. intra_kind (kind a)
[PROOF STEP]
by(simp_all add:intra_path_def)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n'
\<forall>a\<in>set as. intra_kind (kind a)

goal (1 subgoal):
 1. obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
from this \<open>\<forall>n' \<in> set(sourcenodes as). n' \<notin> S\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
\<forall>a\<in>set as. intra_kind (kind a)
\<forall>n'\<in>set (sourcenodes as). n' \<notin> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
\<forall>a\<in>set as. intra_kind (kind a)
\<forall>n'\<in>set (sourcenodes as). n' \<notin> S

goal (1 subgoal):
 1. obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
proof(induct rule:path.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes []). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n S \<subseteq> obs_intra n S
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
case (Cons_path n'' as n' a n)
[PROOF STATE]
proof (state)
this:
n'' -as\<rightarrow>* n'
\<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S
valid_edge a
sourcenode a = n
targetnode a = n''
\<forall>a\<in>set (a # as). intra_kind (kind a)
\<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S

goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes []). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n S \<subseteq> obs_intra n S
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
note IH = \<open>\<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk>
      \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S

goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes []). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n S \<subseteq> obs_intra n S
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
from \<open>\<forall>n'\<in>set (sourcenodes (a#as)). n' \<notin> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S
[PROOF STEP]
have all:"\<forall>n'\<in>set (sourcenodes as). n' \<notin> S" and "sourcenode a \<notin> S"
[PROOF STATE]
proof (prove)
using this:
\<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S

goal (1 subgoal):
 1. \<forall>n'\<in>set (sourcenodes as). n' \<notin> S &&& sourcenode a \<notin> S
[PROOF STEP]
by(simp_all add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>n'\<in>set (sourcenodes as). n' \<notin> S
sourcenode a \<notin> S

goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes []). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n S \<subseteq> obs_intra n S
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
from \<open>\<forall>a \<in> set (a#as). intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set (a # as). intra_kind (kind a)
[PROOF STEP]
have "intra_kind (kind a)" and "\<forall>a \<in> set as. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # as). intra_kind (kind a)

goal (1 subgoal):
 1. intra_kind (kind a) &&& \<forall>a\<in>set as. intra_kind (kind a)
[PROOF STEP]
by(simp_all add:intra_path_def)
[PROOF STATE]
proof (state)
this:
intra_kind (kind a)
\<forall>a\<in>set as. intra_kind (kind a)

goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes []). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n S \<subseteq> obs_intra n S
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
from IH[OF \<open>\<forall>a \<in> set as. intra_kind (kind a)\<close> all]
[PROOF STATE]
proof (chain)
picking this:
obs_intra n' S \<subseteq> obs_intra n'' S
[PROOF STEP]
have "obs_intra n' S \<subseteq> obs_intra n'' S"
[PROOF STATE]
proof (prove)
using this:
obs_intra n' S \<subseteq> obs_intra n'' S

goal (1 subgoal):
 1. obs_intra n' S \<subseteq> obs_intra n'' S
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
obs_intra n' S \<subseteq> obs_intra n'' S

goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes []). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n S \<subseteq> obs_intra n S
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>intra_kind (kind a)\<close> \<open>targetnode a = n''\<close>
      \<open>sourcenode a = n\<close> \<open>sourcenode a \<notin> S\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
intra_kind (kind a)
targetnode a = n''
sourcenode a = n
sourcenode a \<notin> S
[PROOF STEP]
have "obs_intra n'' S \<subseteq> obs_intra n S"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
intra_kind (kind a)
targetnode a = n''
sourcenode a = n
sourcenode a \<notin> S

goal (1 subgoal):
 1. obs_intra n'' S \<subseteq> obs_intra n S
[PROOF STEP]
by(fastforce dest:edge_obs_intra_subset)
[PROOF STATE]
proof (state)
this:
obs_intra n'' S \<subseteq> obs_intra n S

goal (2 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes []). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n S \<subseteq> obs_intra n S
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes as). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n'' S; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n'\<in>set (sourcenodes (a # as)). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
with \<open>obs_intra n' S \<subseteq> obs_intra n'' S\<close>
[PROOF STATE]
proof (chain)
picking this:
obs_intra n' S \<subseteq> obs_intra n'' S
obs_intra n'' S \<subseteq> obs_intra n S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
obs_intra n' S \<subseteq> obs_intra n'' S
obs_intra n'' S \<subseteq> obs_intra n S

goal (1 subgoal):
 1. obs_intra n' S \<subseteq> obs_intra n S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
obs_intra n' S \<subseteq> obs_intra n S

goal (1 subgoal):
 1. \<And>n. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n'\<in>set (sourcenodes []). n' \<notin> S\<rbrakk> \<Longrightarrow> obs_intra n S \<subseteq> obs_intra n S
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
obs_intra n' S \<subseteq> obs_intra n S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_ex_obs_intra:
  assumes "n -as\<rightarrow>\<^sub>\<iota>* n'" and "n' \<in> S"
  obtains m where "m \<in> obs_intra n S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> obs_intra n S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
show "\<exists>m. m \<in> obs_intra n S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
proof(cases "\<forall>nx \<in> set(sourcenodes as). nx \<notin> S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>nx\<in>set (sourcenodes as). nx \<notin> S \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
 2. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S

goal (2 subgoals):
 1. \<forall>nx\<in>set (sourcenodes as). nx \<notin> S \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
 2. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
with \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>n' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n' \<in> S
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S
[PROOF STEP]
have "n' \<in> obs_intra n S"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n' \<in> S
\<forall>nx\<in>set (sourcenodes as). nx \<notin> S

goal (1 subgoal):
 1. n' \<in> obs_intra n S
[PROOF STEP]
by -(rule obs_intra_elem)
[PROOF STATE]
proof (state)
this:
n' \<in> obs_intra n S

goal (2 subgoals):
 1. \<forall>nx\<in>set (sourcenodes as). nx \<notin> S \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
 2. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n' \<in> obs_intra n S

goal (1 subgoal):
 1. \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>m. m \<in> obs_intra n S

goal (1 subgoal):
 1. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S)

goal (1 subgoal):
 1. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
hence "\<exists>nx \<in> set(sourcenodes as). nx \<in> S"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S)

goal (1 subgoal):
 1. \<exists>nx\<in>set (sourcenodes as). nx \<in> S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>nx\<in>set (sourcenodes as). nx \<in> S

goal (1 subgoal):
 1. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>nx\<in>set (sourcenodes as). nx \<in> S
[PROOF STEP]
obtain nx ns ns' where "sourcenodes as = ns@nx#ns'"
      and "nx \<in> S" and "\<forall>n' \<in> set ns. n' \<notin> S"
[PROOF STATE]
proof (prove)
using this:
\<exists>nx\<in>set (sourcenodes as). nx \<in> S

goal (1 subgoal):
 1. (\<And>ns nx ns'. \<lbrakk>sourcenodes as = ns @ nx # ns'; nx \<in> S; \<forall>n'\<in>set ns. n' \<notin> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:split_list_first_propE)
[PROOF STATE]
proof (state)
this:
sourcenodes as = ns @ nx # ns'
nx \<in> S
\<forall>n'\<in>set ns. n' \<notin> S

goal (1 subgoal):
 1. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
from \<open>sourcenodes as = ns@nx#ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenodes as = ns @ nx # ns'
[PROOF STEP]
obtain as' a as''
      where "ns = sourcenodes as'"
      and "as = as'@a#as''" and "sourcenode a = nx"
[PROOF STATE]
proof (prove)
using this:
sourcenodes as = ns @ nx # ns'

goal (1 subgoal):
 1. (\<And>as' a as''. \<lbrakk>ns = sourcenodes as'; as = as' @ a # as''; sourcenode a = nx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
ns = sourcenodes as'
as = as' @ a # as''
sourcenode a = nx

goal (1 subgoal):
 1. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
with \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
ns = sourcenodes as'
as = as' @ a # as''
sourcenode a = nx
[PROOF STEP]
have "n -as'\<rightarrow>\<^sub>\<iota>* nx"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
ns = sourcenodes as'
as = as' @ a # as''
sourcenode a = nx

goal (1 subgoal):
 1. n -as'\<rightarrow>\<^sub>\<iota>* nx
[PROOF STEP]
by(fastforce dest:path_split simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
n -as'\<rightarrow>\<^sub>\<iota>* nx

goal (1 subgoal):
 1. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
with \<open>nx \<in> S\<close> \<open>\<forall>n' \<in> set ns. n' \<notin> S\<close> \<open>ns = sourcenodes as'\<close>
[PROOF STATE]
proof (chain)
picking this:
nx \<in> S
\<forall>n'\<in>set ns. n' \<notin> S
ns = sourcenodes as'
n -as'\<rightarrow>\<^sub>\<iota>* nx
[PROOF STEP]
have "nx \<in> obs_intra n S"
[PROOF STATE]
proof (prove)
using this:
nx \<in> S
\<forall>n'\<in>set ns. n' \<notin> S
ns = sourcenodes as'
n -as'\<rightarrow>\<^sub>\<iota>* nx

goal (1 subgoal):
 1. nx \<in> obs_intra n S
[PROOF STEP]
by(fastforce intro:obs_intra_elem)
[PROOF STATE]
proof (state)
this:
nx \<in> obs_intra n S

goal (1 subgoal):
 1. \<not> (\<forall>nx\<in>set (sourcenodes as). nx \<notin> S) \<Longrightarrow> \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
nx \<in> obs_intra n S

goal (1 subgoal):
 1. \<exists>m. m \<in> obs_intra n S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>m. m \<in> obs_intra n S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m. m \<in> obs_intra n S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obsI:
  assumes "n' \<in> obs_intra n S"
  and "\<forall>nx \<in> set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S"
  shows "\<lbrakk>ns = nsx@n#nsx'; \<forall>xs x xs'. nsx = xs@x#xs' \<and> obs_intra x S \<noteq> {}
     \<longrightarrow> (\<exists>x'' \<in> set (xs'@[n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk>
  \<Longrightarrow> n'#nsx' \<in> obs ns S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs ns S
[PROOF STEP]
proof(induct ns arbitrary:nsx)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>nsx. \<lbrakk>[] = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs [] S
 2. \<And>a ns nsx. \<lbrakk>\<And>nsx. \<lbrakk>ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs ns S; a # ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs (a # ns) S
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>xs = ?nsx @ n # nsx'; \<forall>xs x xs'. ?nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs xs S
x # xs = nsx @ n # nsx'
\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)

goal (2 subgoals):
 1. \<And>nsx. \<lbrakk>[] = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs [] S
 2. \<And>a ns nsx. \<lbrakk>\<And>nsx. \<lbrakk>ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs ns S; a # ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs (a # ns) S
[PROOF STEP]
note IH = \<open>\<And>nsx. \<lbrakk>xs = nsx@n#nsx';
    \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow>
    (\<exists>x''\<in>set (xs'@[n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk>
    \<Longrightarrow> n'#nsx' \<in> obs xs S\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>xs = ?nsx @ n # nsx'; \<forall>xs x xs'. ?nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs xs S

goal (2 subgoals):
 1. \<And>nsx. \<lbrakk>[] = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs [] S
 2. \<And>a ns nsx. \<lbrakk>\<And>nsx. \<lbrakk>ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs ns S; a # ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs (a # ns) S
[PROOF STEP]
note nsx = \<open>\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow>
    (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<close>
[PROOF STATE]
proof (state)
this:
\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)

goal (2 subgoals):
 1. \<And>nsx. \<lbrakk>[] = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs [] S
 2. \<And>a ns nsx. \<lbrakk>\<And>nsx. \<lbrakk>ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs ns S; a # ns = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs (a # ns) S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
proof(cases nsx)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nsx = [] \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
 2. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
nsx = []

goal (2 subgoals):
 1. nsx = [] \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
 2. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
with \<open>x#xs = nsx@n#nsx'\<close>
[PROOF STATE]
proof (chain)
picking this:
x # xs = nsx @ n # nsx'
nsx = []
[PROOF STEP]
have "n = x" and "xs = nsx'"
[PROOF STATE]
proof (prove)
using this:
x # xs = nsx @ n # nsx'
nsx = []

goal (1 subgoal):
 1. n = x &&& xs = nsx'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
n = x
xs = nsx'

goal (2 subgoals):
 1. nsx = [] \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
 2. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
with \<open>n' \<in> obs_intra n S\<close>
      \<open>\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
n = x
xs = nsx'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
n = x
xs = nsx'

goal (1 subgoal):
 1. n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
by(fastforce simp:Let_def)
[PROOF STATE]
proof (state)
this:
n' # nsx' \<in> obs (x # xs) S

goal (1 subgoal):
 1. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
case (Cons z zs)
[PROOF STATE]
proof (state)
this:
nsx = z # zs

goal (1 subgoal):
 1. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
with \<open>x#xs = nsx@n#nsx'\<close>
[PROOF STATE]
proof (chain)
picking this:
x # xs = nsx @ n # nsx'
nsx = z # zs
[PROOF STEP]
have [simp]:"x = z" "xs = zs@n#nsx'"
[PROOF STATE]
proof (prove)
using this:
x # xs = nsx @ n # nsx'
nsx = z # zs

goal (1 subgoal):
 1. x = z &&& xs = zs @ n # nsx'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
x = z
xs = zs @ n # nsx'

goal (1 subgoal):
 1. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
from nsx Cons
[PROOF STATE]
proof (chain)
picking this:
\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)
nsx = z # zs
[PROOF STEP]
have "\<forall>xs x xs'. zs = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow>
      (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)"
[PROOF STATE]
proof (prove)
using this:
\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)
nsx = z # zs

goal (1 subgoal):
 1. \<forall>xs x xs'. zs = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)
[PROOF STEP]
by clarsimp(erule_tac x="z#xs" in allE,auto)
[PROOF STATE]
proof (state)
this:
\<forall>xs x xs'. zs = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)

goal (1 subgoal):
 1. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
from IH[OF \<open>xs = zs@n#nsx'\<close> this]
[PROOF STATE]
proof (chain)
picking this:
n' # nsx' \<in> obs xs S
[PROOF STEP]
have "n'#nsx' \<in> obs xs S"
[PROOF STATE]
proof (prove)
using this:
n' # nsx' \<in> obs xs S

goal (1 subgoal):
 1. n' # nsx' \<in> obs xs S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n' # nsx' \<in> obs xs S

goal (1 subgoal):
 1. \<And>a list. nsx = a # list \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
proof(cases "obs_intra z S = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. obs_intra z S = {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
 2. obs_intra z S \<noteq> {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
obs_intra z S = {}

goal (2 subgoals):
 1. obs_intra z S = {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
 2. obs_intra z S \<noteq> {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
with Cons \<open>n'#nsx' \<in> obs xs S\<close>
[PROOF STATE]
proof (chain)
picking this:
nsx = z # zs
n' # nsx' \<in> obs xs S
obs_intra z S = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nsx = z # zs
n' # nsx' \<in> obs xs S
obs_intra z S = {}

goal (1 subgoal):
 1. n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
by(simp add:Let_def)
[PROOF STATE]
proof (state)
this:
n' # nsx' \<in> obs (x # xs) S

goal (1 subgoal):
 1. obs_intra z S \<noteq> {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. obs_intra z S \<noteq> {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
obs_intra z S \<noteq> {}

goal (1 subgoal):
 1. obs_intra z S \<noteq> {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
from nsx Cons
[PROOF STATE]
proof (chain)
picking this:
\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)
nsx = z # zs
[PROOF STEP]
have "obs_intra z S \<noteq> {} \<longrightarrow>
        (\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)"
[PROOF STATE]
proof (prove)
using this:
\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)
nsx = z # zs

goal (1 subgoal):
 1. obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)

goal (1 subgoal):
 1. obs_intra z S \<noteq> {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
obs_intra z S \<noteq> {}
obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)
[PROOF STEP]
have "\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S"
[PROOF STATE]
proof (prove)
using this:
obs_intra z S \<noteq> {}
obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)

goal (1 subgoal):
 1. \<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S

goal (1 subgoal):
 1. obs_intra z S \<noteq> {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
with \<open>xs = zs@n#nsx'\<close>
[PROOF STATE]
proof (chain)
picking this:
xs = zs @ n # nsx'
\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S
[PROOF STEP]
have "\<exists>n' \<in> set xs. \<exists>nx. call_of_return_node n' nx \<and> nx \<notin> S"
[PROOF STATE]
proof (prove)
using this:
xs = zs @ n # nsx'
\<exists>x''\<in>set (zs @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S

goal (1 subgoal):
 1. \<exists>n'\<in>set xs. \<exists>nx. call_of_return_node n' nx \<and> nx \<notin> S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>n'\<in>set xs. \<exists>nx. call_of_return_node n' nx \<and> nx \<notin> S

goal (1 subgoal):
 1. obs_intra z S \<noteq> {} \<Longrightarrow> n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
with Cons \<open>n'#nsx' \<in> obs xs S\<close>
[PROOF STATE]
proof (chain)
picking this:
nsx = z # zs
n' # nsx' \<in> obs xs S
\<exists>n'\<in>set xs. \<exists>nx. call_of_return_node n' nx \<and> nx \<notin> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nsx = z # zs
n' # nsx' \<in> obs xs S
\<exists>n'\<in>set xs. \<exists>nx. call_of_return_node n' nx \<and> nx \<notin> S

goal (1 subgoal):
 1. n' # nsx' \<in> obs (x # xs) S
[PROOF STEP]
by(simp add:Let_def)
[PROOF STATE]
proof (state)
this:
n' # nsx' \<in> obs (x # xs) S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n' # nsx' \<in> obs (x # xs) S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n' # nsx' \<in> obs (x # xs) S

goal (1 subgoal):
 1. \<And>nsx. \<lbrakk>[] = nsx @ n # nsx'; \<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set (xs' @ [n]). \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S)\<rbrakk> \<Longrightarrow> n' # nsx' \<in> obs [] S
[PROOF STEP]
qed simp