[STATEMENT]
lemma obsE [consumes 2]:
  assumes "ns' \<in> obs ns S" and "\<forall>n \<in> set (tl ns). return_node n"
  obtains nsx n nsx' n' where "ns = nsx@n#nsx'" and "ns' = n'#nsx'"
  and "n' \<in> obs_intra n S"
  and "\<forall>nx \<in> set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S"
  and "\<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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>nsx n nsx' n'. \<lbrakk>ns = nsx @ n # nsx'; ns' = n' # nsx'; n' \<in> obs_intra n S; \<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S; \<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
from \<open>ns' \<in> obs ns S\<close> \<open>\<forall>n \<in> set (tl ns). return_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
ns' \<in> obs ns S
Ball (set (tl ns)) return_node
[PROOF STEP]
show "\<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and>
    n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and>
    (\<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))"
[PROOF STATE]
proof (prove)
using this:
ns' \<in> obs ns S
Ball (set (tl ns)) return_node

goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
proof(induct ns)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ns' \<in> obs [] S; Ball (set (tl [])) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. [] = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<And>a ns. \<lbrakk>\<lbrakk>ns' \<in> obs ns S; Ball (set (tl ns)) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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)); ns' \<in> obs (a # ns) S; Ball (set (tl (a # ns))) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. a # ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ns' \<in> obs [] S
Ball (set (tl [])) return_node

goal (2 subgoals):
 1. \<lbrakk>ns' \<in> obs [] S; Ball (set (tl [])) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. [] = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<And>a ns. \<lbrakk>\<lbrakk>ns' \<in> obs ns S; Ball (set (tl ns)) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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)); ns' \<in> obs (a # ns) S; Ball (set (tl (a # ns))) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. a # ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ns' \<in> obs [] S
Ball (set (tl [])) return_node

goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. [] = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. [] = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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 (1 subgoal):
 1. \<And>a ns. \<lbrakk>\<lbrakk>ns' \<in> obs ns S; Ball (set (tl ns)) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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)); ns' \<in> obs (a # ns) S; Ball (set (tl (a # ns))) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. a # ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ns. \<lbrakk>\<lbrakk>ns' \<in> obs ns S; Ball (set (tl ns)) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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)); ns' \<in> obs (a # ns) S; Ball (set (tl (a # ns))) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. a # ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
case (Cons nx ns'')
[PROOF STATE]
proof (state)
this:
\<lbrakk>ns' \<in> obs ns'' S; Ball (set (tl ns'')) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
ns' \<in> obs (nx # ns'') S
Ball (set (tl (nx # ns''))) return_node

goal (1 subgoal):
 1. \<And>a ns. \<lbrakk>\<lbrakk>ns' \<in> obs ns S; Ball (set (tl ns)) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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)); ns' \<in> obs (a # ns) S; Ball (set (tl (a # ns))) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. a # ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
note IH = \<open>\<lbrakk>ns' \<in> obs ns'' S; \<forall>a\<in>set (tl ns''). return_node a\<rbrakk>
      \<Longrightarrow> \<exists>nsx n nsx' n'. ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and>
      n' \<in> obs_intra n S \<and>
      (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and>
      (\<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:
\<lbrakk>ns' \<in> obs ns'' S; Ball (set (tl ns'')) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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 (1 subgoal):
 1. \<And>a ns. \<lbrakk>\<lbrakk>ns' \<in> obs ns S; Ball (set (tl ns)) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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)); ns' \<in> obs (a # ns) S; Ball (set (tl (a # ns))) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. a # ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
from \<open>\<forall>a\<in>set (tl (nx # ns'')). return_node a\<close>
[PROOF STATE]
proof (chain)
picking this:
Ball (set (tl (nx # ns''))) return_node
[PROOF STEP]
have "\<forall>n \<in> set ns''. return_node n"
[PROOF STATE]
proof (prove)
using this:
Ball (set (tl (nx # ns''))) return_node

goal (1 subgoal):
 1. Ball (set ns'') return_node
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ball (set ns'') return_node

goal (1 subgoal):
 1. \<And>a ns. \<lbrakk>\<lbrakk>ns' \<in> obs ns S; Ball (set (tl ns)) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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)); ns' \<in> obs (a # ns) S; Ball (set (tl (a # ns))) return_node\<rbrakk> \<Longrightarrow> \<exists>nsx n nsx' n'. a # ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
proof(cases ns'')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ns'' = [] \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<And>a list. ns'' = a # list \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ns'' = []

goal (2 subgoals):
 1. ns'' = [] \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<And>a list. ns'' = a # list \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with \<open>ns' \<in> obs (nx#ns'') S\<close>
[PROOF STATE]
proof (chain)
picking this:
ns' \<in> obs (nx # ns'') S
ns'' = []
[PROOF STEP]
obtain x where "ns' = [x]" and "x \<in> obs_intra nx S"
[PROOF STATE]
proof (prove)
using this:
ns' \<in> obs (nx # ns'') S
ns'' = []

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>ns' = [x]; x \<in> obs_intra nx S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp:Let_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
ns' = [x]
x \<in> obs_intra nx S

goal (2 subgoals):
 1. ns'' = [] \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<And>a list. ns'' = a # list \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with Nil
[PROOF STATE]
proof (chain)
picking this:
ns'' = []
ns' = [x]
x \<in> obs_intra nx S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns'' = []
ns' = [x]
x \<in> obs_intra nx S

goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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 (1 subgoal):
 1. \<And>a list. ns'' = a # list \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ns'' = a # list \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
ns'' = a_ # list_

goal (1 subgoal):
 1. \<And>a list. ns'' = a # list \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with \<open>\<forall>n \<in> set ns''. return_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
Ball (set ns'') return_node
ns'' = a_ # list_
[PROOF STEP]
have "\<forall>a\<in>set (tl ns''). return_node a"
[PROOF STATE]
proof (prove)
using this:
Ball (set ns'') return_node
ns'' = a_ # list_

goal (1 subgoal):
 1. Ball (set (tl ns'')) return_node
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ball (set (tl ns'')) return_node

goal (1 subgoal):
 1. \<And>a list. ns'' = a # list \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
proof(cases "\<exists>n' \<in> set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S

goal (2 subgoals):
 1. \<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with \<open>ns' \<in> obs (nx#ns'') S\<close>
[PROOF STATE]
proof (chain)
picking this:
ns' \<in> obs (nx # ns'') S
\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S
[PROOF STEP]
have "ns' \<in> obs ns'' S"
[PROOF STATE]
proof (prove)
using this:
ns' \<in> obs (nx # ns'') S
\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S

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

goal (2 subgoals):
 1. \<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
from IH[OF this \<open>\<forall>a\<in>set (tl ns''). return_node a\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>nsx n nsx' n'. ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
obtain nsx n nsx' n' where split:"ns'' = nsx @ n # nsx'"
          "ns' = n' # nsx'" "n' \<in> obs_intra n S"
          "\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S"
          and imp:"\<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)"
[PROOF STATE]
proof (prove)
using this:
\<exists>nsx n nsx' n'. ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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 (1 subgoal):
 1. (\<And>nsx n nsx' n'. \<lbrakk>ns'' = nsx @ n # nsx'; ns' = n' # nsx'; n' \<in> obs_intra n S; \<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S; \<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns'' = nsx @ n # nsx'
ns' = n' # nsx'
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
\<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. \<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
from True \<open>ns'' = nsx @ n # nsx'\<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:
\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S
ns'' = nsx @ n # nsx'
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
[PROOF STEP]
have "(\<exists>nx'. call_of_return_node n nx' \<and> nx' \<notin> S) \<or>
          (\<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S)"
[PROOF STATE]
proof (prove)
using this:
\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S
ns'' = nsx @ n # nsx'
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S

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

goal (2 subgoals):
 1. \<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>nx'. call_of_return_node n nx' \<and> nx' \<notin> S) \<or> (\<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S)

goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>nx'. call_of_return_node n nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
assume "\<exists>nx'. call_of_return_node n nx' \<and> nx' \<notin> S"
[PROOF STATE]
proof (state)
this:
\<exists>nx'. call_of_return_node n nx' \<and> nx' \<notin> S

goal (2 subgoals):
 1. \<exists>nx'. call_of_return_node n nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. \<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with split
[PROOF STATE]
proof (chain)
picking this:
ns'' = nsx @ n # nsx'
ns' = n' # nsx'
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
\<exists>nx'. call_of_return_node n nx' \<and> nx' \<notin> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns'' = nsx @ n # nsx'
ns' = n' # nsx'
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
\<exists>nx'. call_of_return_node n nx' \<and> nx' \<notin> S

goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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 (1 subgoal):
 1. \<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
assume "\<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S"
[PROOF STATE]
proof (state)
this:
\<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S

goal (1 subgoal):
 1. \<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with imp
[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)
\<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S
[PROOF STEP]
have "\<forall>xs x xs'. nx#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)"
[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)
\<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S

goal (1 subgoal):
 1. \<forall>xs x xs'. nx # 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)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n' nx' xs x xs'. \<lbrakk>\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>nx. call_of_return_node n nx \<and> nx \<notin> S) \<or> (\<exists>x''\<in>set xs'. \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S); n' \<in> set nsx; call_of_return_node n' nx'; nx' \<notin> S; nx # nsx = xs @ x # xs'; obs_intra x S \<noteq> {}; \<forall>x''\<in>set xs'. \<forall>nx. call_of_return_node x'' nx \<longrightarrow> nx \<in> S\<rbrakk> \<Longrightarrow> \<exists>nx. call_of_return_node n nx \<and> nx \<notin> S
[PROOF STEP]
apply(case_tac xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n' nx' xs x xs'. \<lbrakk>\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>nx. call_of_return_node n nx \<and> nx \<notin> S) \<or> (\<exists>x''\<in>set xs'. \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S); n' \<in> set nsx; call_of_return_node n' nx'; nx' \<notin> S; nx # nsx = xs @ x # xs'; obs_intra x S \<noteq> {}; \<forall>x''\<in>set xs'. \<forall>nx. call_of_return_node x'' nx \<longrightarrow> nx \<in> S; xs = []\<rbrakk> \<Longrightarrow> \<exists>nx. call_of_return_node n nx \<and> nx \<notin> S
 2. \<And>n' nx' xs x xs' a list. \<lbrakk>\<forall>xs x xs'. nsx = xs @ x # xs' \<and> obs_intra x S \<noteq> {} \<longrightarrow> (\<exists>nx. call_of_return_node n nx \<and> nx \<notin> S) \<or> (\<exists>x''\<in>set xs'. \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S); n' \<in> set nsx; call_of_return_node n' nx'; nx' \<notin> S; nx # nsx = xs @ x # xs'; obs_intra x S \<noteq> {}; \<forall>x''\<in>set xs'. \<forall>nx. call_of_return_node x'' nx \<longrightarrow> nx \<in> S; xs = a # list\<rbrakk> \<Longrightarrow> \<exists>nx. call_of_return_node n nx \<and> nx \<notin> S
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nx' x xs' list xa. \<lbrakk>\<forall>xs xa xs'a. list @ x # xs' = xs @ xa # xs'a \<and> obs_intra xa S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set xs'a. \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S); call_of_return_node x nx'; nx' \<notin> S; nsx = list @ x # xs'; \<forall>x''\<in>set xs'. \<forall>nx. call_of_return_node x'' nx \<longrightarrow> nx \<in> S; \<forall>nx. call_of_return_node n nx \<longrightarrow> nx \<in> S; xa \<in> obs_intra x S\<rbrakk> \<Longrightarrow> False
 2. \<And>n' nx' x xs' list xa. \<lbrakk>\<forall>xs xa xs'a. list @ x # xs' = xs @ xa # xs'a \<and> obs_intra xa S \<noteq> {} \<longrightarrow> (\<exists>x''\<in>set xs'a. \<exists>nx. call_of_return_node x'' nx \<and> nx \<notin> S); call_of_return_node n' nx'; nx' \<notin> S; nsx = list @ x # xs'; \<forall>x''\<in>set xs'. \<forall>nx. call_of_return_node x'' nx \<longrightarrow> nx \<in> S; \<forall>nx. call_of_return_node n nx \<longrightarrow> nx \<in> S; xa \<in> obs_intra x S; n' \<in> set list\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(erule_tac x="list" in allE,auto)+
[PROOF STATE]
proof (state)
this:
\<forall>xs x xs'. nx # 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 (1 subgoal):
 1. \<exists>n'\<in>set nsx. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with split Cons
[PROOF STATE]
proof (chain)
picking this:
ns'' = nsx @ n # nsx'
ns' = n' # nsx'
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
ns'' = a_ # list_
\<forall>xs x xs'. nx # 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)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns'' = nsx @ n # nsx'
ns' = n' # nsx'
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
ns'' = a_ # list_
\<forall>xs x xs'. nx # 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 (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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 (1 subgoal):
 1. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S)

goal (1 subgoal):
 1. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
hence "\<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S)

goal (1 subgoal):
 1. \<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S

goal (1 subgoal):
 1. \<not> (\<exists>n'\<in>set ns''. \<exists>nx'. call_of_return_node n' nx' \<and> nx' \<notin> S) \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
proof(cases "obs_intra nx S = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. obs_intra nx S = {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
obs_intra nx S = {}

goal (2 subgoals):
 1. obs_intra nx S = {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with \<open>ns' \<in> obs (nx#ns'') S\<close>
[PROOF STATE]
proof (chain)
picking this:
ns' \<in> obs (nx # ns'') S
obs_intra nx S = {}
[PROOF STEP]
have "ns' \<in> obs ns'' S"
[PROOF STATE]
proof (prove)
using this:
ns' \<in> obs (nx # ns'') S
obs_intra nx S = {}

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

goal (2 subgoals):
 1. obs_intra nx S = {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
from IH[OF this \<open>\<forall>a\<in>set (tl ns''). return_node a\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>nsx n nsx' n'. ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
obtain nsx n nsx' n' where split:"ns'' = nsx @ n # nsx'"
            "ns' = n' # nsx'" "n' \<in> obs_intra n S"
            "\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S"
            and imp:"\<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)"
[PROOF STATE]
proof (prove)
using this:
\<exists>nsx n nsx' n'. ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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 (1 subgoal):
 1. (\<And>nsx n nsx' n'. \<lbrakk>ns'' = nsx @ n # nsx'; ns' = n' # nsx'; n' \<in> obs_intra n S; \<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S; \<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns'' = nsx @ n # nsx'
ns' = n' # nsx'
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
\<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. obs_intra nx S = {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
from True imp Cons
[PROOF STATE]
proof (chain)
picking this:
obs_intra nx S = {}
\<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)
ns'' = a_ # list_
[PROOF STEP]
have "\<forall>xs x xs'. nx#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)"
[PROOF STATE]
proof (prove)
using this:
obs_intra nx S = {}
\<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)
ns'' = a_ # list_

goal (1 subgoal):
 1. \<forall>xs x xs'. nx # 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)
[PROOF STEP]
by clarsimp (hypsubst_thin,case_tac xs,clarsimp+,erule_tac x="list" in allE,auto)
[PROOF STATE]
proof (state)
this:
\<forall>xs x xs'. nx # 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. obs_intra nx S = {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
 2. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with split Cons
[PROOF STATE]
proof (chain)
picking this:
ns'' = nsx @ n # nsx'
ns' = n' # nsx'
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
ns'' = a_ # list_
\<forall>xs x xs'. nx # 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)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns'' = nsx @ n # nsx'
ns' = n' # nsx'
n' \<in> obs_intra n S
\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S
ns'' = a_ # list_
\<forall>xs x xs'. nx # 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 (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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 (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
obs_intra nx S \<noteq> {}

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with \<open>\<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S\<close>
            \<open>ns' \<in> obs (nx # ns'') S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S
ns' \<in> obs (nx # ns'') S
obs_intra nx S \<noteq> {}
[PROOF STEP]
obtain nx'' where "ns' = nx''#ns''" and "nx'' \<in> obs_intra nx S"
[PROOF STATE]
proof (prove)
using this:
\<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S
ns' \<in> obs (nx # ns'') S
obs_intra nx S \<noteq> {}

goal (1 subgoal):
 1. (\<And>nx''. \<lbrakk>ns' = nx'' # ns''; nx'' \<in> obs_intra nx S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce simp:Let_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
ns' = nx'' # ns''
nx'' \<in> obs_intra nx S

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ns' = nx'' # ns''
nx'' \<in> obs_intra nx S

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
fix n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
assume "n'\<in>set ns''"
[PROOF STATE]
proof (state)
this:
n' \<in> set ns''

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with \<open>\<forall>n \<in> set ns''. return_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
Ball (set ns'') return_node
n' \<in> set ns''
[PROOF STEP]
have "return_node n'"
[PROOF STATE]
proof (prove)
using this:
Ball (set ns'') return_node
n' \<in> set ns''

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

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
hence "\<exists>!n''. call_of_return_node n' n''"
[PROOF STATE]
proof (prove)
using this:
return_node n'

goal (1 subgoal):
 1. \<exists>!n''. call_of_return_node n' n''
[PROOF STEP]
by(rule return_node_call_of_return_node)
[PROOF STATE]
proof (state)
this:
\<exists>!n''. call_of_return_node n' n''

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
from \<open>n'\<in>set ns''\<close>
              \<open>\<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<in> set ns''
\<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S
[PROOF STEP]
have "\<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S"
[PROOF STATE]
proof (prove)
using this:
n' \<in> set ns''
\<forall>n'\<in>set ns''. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S

goal (1 subgoal):
 1. \<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with \<open>\<exists>!n''. call_of_return_node n' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>!n''. call_of_return_node n' n''
\<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S
[PROOF STEP]
have "\<exists>n''. call_of_return_node n' n'' \<and> n'' \<in> S"
[PROOF STATE]
proof (prove)
using this:
\<exists>!n''. call_of_return_node n' n''
\<forall>nx'. call_of_return_node n' nx' \<longrightarrow> nx' \<in> S

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

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?n'2 \<in> set ns'' \<Longrightarrow> \<exists>n''. call_of_return_node ?n'2 n'' \<and> n'' \<in> S

goal (1 subgoal):
 1. obs_intra nx S \<noteq> {} \<Longrightarrow> \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
with \<open>ns' = nx''#ns''\<close> \<open>nx'' \<in> obs_intra nx S\<close>
[PROOF STATE]
proof (chain)
picking this:
ns' = nx'' # ns''
nx'' \<in> obs_intra nx S
?n'2 \<in> set ns'' \<Longrightarrow> \<exists>n''. call_of_return_node ?n'2 n'' \<and> n'' \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns' = nx'' # ns''
nx'' \<in> obs_intra nx S
?n'2 \<in> set ns'' \<Longrightarrow> \<exists>n''. call_of_return_node ?n'2 n'' \<and> n'' \<in> S

goal (1 subgoal):
 1. \<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. nx # ns'' = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nsx n nsx' n'. ns = nsx @ n # nsx' \<and> ns' = n' # nsx' \<and> n' \<in> obs_intra n S \<and> (\<forall>nx\<in>set nsx'. \<exists>nx'. call_of_return_node nx nx' \<and> nx' \<in> S) \<and> (\<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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_sqrt_1:
  fixes z::complex
  assumes "z \<noteq> 0"
  shows "z = 1 / z \<longleftrightarrow> z = 1 \<or> z = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z = 1 / z) = (z = 1 \<or> z = - 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. (z = 1 / z) = (z = 1 \<or> z = - 1)
[PROOF STEP]
using nonzero_eq_divide_eq square_eq_iff
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
?c \<noteq> (0::?'a) \<Longrightarrow> (?a = ?b / ?c) = (?a * ?c = ?b)
(?a * ?a = ?b * ?b) = (?a = ?b \<or> ?a = - ?b)

goal (1 subgoal):
 1. (z = 1 / z) = (z = 1 \<or> z = - 1)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma pell_valuation_nonneg [simp]: "fst z \<ge> 0 \<Longrightarrow> snd z \<ge> 0 \<Longrightarrow> pell_valuation z \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> fst z; 0 \<le> snd z\<rbrakk> \<Longrightarrow> 0 \<le> pell_valuation z
[PROOF STEP]
by (auto simp: pell_valuation_def case_prod_unfold)