[STATEMENT]
lemma init_par_comp [simp]:
  "init (s \<langle>\<langle> t) = init s \<times> init t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init (s \<langle>\<langle> t) = init s \<times> init t
[PROOF STEP]
unfolding par_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<lparr>init = init s \<times> init t, trans = parp_sos (automaton.trans s) (automaton.trans t)\<rparr> = init s \<times> init t
[PROOF STEP]
by simp


[STATEMENT]
lemma node_sos_never_newpkt [simp]:
  assumes "(s, a, s') \<in> node_sos S"
    shows "a \<noteq> i:newpkt(d, di)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(s, a, s') \<in> node_sos S

goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
by cases auto


[STATEMENT]
lemma arrives_or_not:
  assumes "(NodeS i s R, ii\<not>ni:arrive(m), NodeS i' s' R') \<in> node_sos S"
    shows "(ii = {i} \<and> ni = {}) \<or> (ii = {} \<and> ni = {i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ii = {i} \<and> ni = {} \<or> ii = {} \<and> ni = {i}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(NodeS i s R, ii\<not>ni:arrive(m), NodeS i' s' R') \<in> node_sos S

goal (1 subgoal):
 1. ii = {i} \<and> ni = {} \<or> ii = {} \<and> ni = {i}
[PROOF STEP]
by rule simp_all


[STATEMENT]
lemma trans_node_comp:
  "trans (\<langle>i : np : R\<^sub>i\<rangle>) = node_sos (trans np)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans (\<langle>i : np : R\<^sub>i\<rangle>) = node_sos (automaton.trans np)
[PROOF STEP]
unfolding node_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans \<lparr>init = {NodeS i s R\<^sub>i |s. s \<in> init np}, trans = node_sos (automaton.trans np)\<rparr> = node_sos (automaton.trans np)
[PROOF STEP]
by simp


[STATEMENT]
lemma init_node_comp:
  "init (\<langle>i : np : R\<^sub>i\<rangle>) = {NodeS i s R\<^sub>i|s. s \<in> init np}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init (\<langle>i : np : R\<^sub>i\<rangle>) = {NodeS i s R\<^sub>i |s. s \<in> init np}
[PROOF STEP]
unfolding node_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<lparr>init = {NodeS i s R\<^sub>i |s. s \<in> init np}, trans = node_sos (automaton.trans np)\<rparr> = {NodeS i s R\<^sub>i |s. s \<in> init np}
[PROOF STEP]
by simp


[STATEMENT]
lemma trans_par_node_comp [simp]:
  "trans (\<langle>i : s \<langle>\<langle> t : R\<rangle>) = node_sos (parp_sos (trans s) (trans t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans (\<langle>i : s \<langle>\<langle> t : R\<rangle>) = node_sos (parp_sos (automaton.trans s) (automaton.trans t))
[PROOF STEP]
unfolding node_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans \<lparr>init = {NodeS i sa R |sa. sa \<in> init (s \<langle>\<langle> t)}, trans = node_sos (automaton.trans (s \<langle>\<langle> t))\<rparr> = node_sos (parp_sos (automaton.trans s) (automaton.trans t))
[PROOF STEP]
by simp


[STATEMENT]
lemma snd_par_node_comp [simp]:
  "init (\<langle>i : s \<langle>\<langle> t : R\<rangle>) = {NodeS i st R|st. st \<in> init s \<times> init t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init (\<langle>i : s \<langle>\<langle> t : R\<rangle>) = {NodeS i st R |st. st \<in> init s \<times> init t}
[PROOF STEP]
unfolding node_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<lparr>init = {NodeS i sa R |sa. sa \<in> init (s \<langle>\<langle> t)}, trans = node_sos (automaton.trans (s \<langle>\<langle> t))\<rparr> = {NodeS i st R |st. st \<in> init s \<times> init t}
[PROOF STEP]
by simp


[STATEMENT]
lemma node_sos_dest_is_net_state:
  assumes "(s, a, s') \<in> node_sos S"
    shows "\<exists>i' P' R'. s' = NodeS i' P' R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i' P' R'. s' = NodeS i' P' R'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(s, a, s') \<in> node_sos S

goal (1 subgoal):
 1. \<exists>i' P' R'. s' = NodeS i' P' R'
[PROOF STEP]
by induct auto


[STATEMENT]
lemma node_sos_dest:
  assumes "(NodeS i p R, a, s') \<in> node_sos S"
    shows "\<exists>P' R'. s' = NodeS i P' R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P' R'. s' = NodeS i P' R'
[PROOF STEP]
using assms assms [THEN node_sos_dest_is_net_state]
[PROOF STATE]
proof (prove)
using this:
(NodeS i p R, a, s') \<in> node_sos S
\<exists>i' P' R'. s' = NodeS i' P' R'

goal (1 subgoal):
 1. \<exists>P' R'. s' = NodeS i P' R'
[PROOF STEP]
by - (erule node_sos.cases, auto)


[STATEMENT]
lemma node_sos_states [elim]:
  assumes "(ns, a, ns') \<in> node_sos S"
  obtains i s R s' R' where "ns  = NodeS i s  R"
                        and "ns' = NodeS i s' R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i s R s' R'. \<lbrakk>ns = NodeS i s R; ns' = NodeS i s' R'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>i s R s' R'. \<lbrakk>ns = NodeS i s R; ns' = NodeS i s' R'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume [intro!]: "\<And>i s R s' R'. ns = NodeS i s R \<Longrightarrow> ns' = NodeS i s' R' \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>ns = NodeS ?i ?s ?R; ns' = NodeS ?i ?s' ?R'\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>i s R s' R'. \<lbrakk>ns = NodeS i s R; ns' = NodeS i s' R'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
(ns, a, ns') \<in> node_sos S
[PROOF STEP]
obtain i s R where "ns = NodeS i s R"
[PROOF STATE]
proof (prove)
using this:
(ns, a, ns') \<in> node_sos S

goal (1 subgoal):
 1. (\<And>i s R. ns = NodeS i s R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ns) auto
[PROOF STATE]
proof (state)
this:
ns = NodeS i s R

goal (1 subgoal):
 1. (\<And>i s R s' R'. \<lbrakk>ns = NodeS i s R; ns' = NodeS i s' R'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ns = NodeS i s R

goal (1 subgoal):
 1. (\<And>i s R s' R'. \<lbrakk>ns = NodeS i s R; ns' = NodeS i s' R'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
(ns, a, ns') \<in> node_sos S
ns = NodeS i s R
[PROOF STEP]
obtain s' R' where "ns' = NodeS i s' R'"
[PROOF STATE]
proof (prove)
using this:
(ns, a, ns') \<in> node_sos S
ns = NodeS i s R

goal (1 subgoal):
 1. (\<And>s' R'. ns' = NodeS i s' R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis node_sos_dest)
[PROOF STATE]
proof (state)
this:
ns' = NodeS i s' R'

goal (1 subgoal):
 1. (\<And>i s R s' R'. \<lbrakk>ns = NodeS i s R; ns' = NodeS i s' R'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ns = NodeS i s R
ns' = NodeS i s' R'
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
ns = NodeS i s R
ns' = NodeS i s' R'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma node_sos_cases [elim]:
  "(NodeS i p R, a, NodeS i p' R') \<in> node_sos S \<Longrightarrow>
  (\<And>m .       \<lbrakk> a = R:*cast(m);          R' = R; (p, broadcast m, p') \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>m D.      \<lbrakk> a = (R \<inter> D):*cast(m);    R' = R; (p, groupcast D m, p') \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>d m.      \<lbrakk> a = {d}:*cast(m);        R' = R; (p, unicast d m, p') \<in> S; d \<in> R \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>d.        \<lbrakk> a = \<tau>;                   R' = R; (p, \<not>unicast d, p') \<in> S; d \<notin> R \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>d.        \<lbrakk> a = i:deliver(d);        R' = R; (p, deliver d, p') \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>m.        \<lbrakk> a = {i}\<not>{}:arrive(m);    R' = R; (p, receive m, p') \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (            \<lbrakk> a = \<tau>;                   R' = R; (p, \<tau>, p') \<in> S \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>m.        \<lbrakk> a = {}\<not>{i}:arrive(m);    R' = R; p = p' \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i'.     \<lbrakk> a = connect(i, i');      R' = R \<union> {i'}; p = p' \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i'.     \<lbrakk> a = connect(i', i);      R' = R \<union> {i'}; p = p' \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i'.     \<lbrakk> a = disconnect(i, i');   R' = R - {i'}; p = p' \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i'.     \<lbrakk> a = disconnect(i', i);   R' = R - {i'}; p = p' \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i' i''. \<lbrakk> a = connect(i', i'');    R' = R; p = p'; i \<noteq> i'; i \<noteq> i'' \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  (\<And>i i' i''. \<lbrakk> a = disconnect(i', i''); R' = R; p = p'; i \<noteq> i'; i \<noteq> i'' \<rbrakk> \<Longrightarrow> P) \<Longrightarrow>
  P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(NodeS i p R, a, NodeS i p' R') \<in> node_sos S; \<And>m. \<lbrakk>a = R:*cast(m); R' = R; (p, broadcast m, p') \<in> S\<rbrakk> \<Longrightarrow> P; \<And>m D. \<lbrakk>a = (R \<inter> D):*cast(m); R' = R; (p, groupcast D m, p') \<in> S\<rbrakk> \<Longrightarrow> P; \<And>d m. \<lbrakk>a = {d}:*cast(m); R' = R; (p, unicast d m, p') \<in> S; d \<in> R\<rbrakk> \<Longrightarrow> P; \<And>d. \<lbrakk>a = \<tau>; R' = R; (p, \<not>unicast d, p') \<in> S; d \<notin> R\<rbrakk> \<Longrightarrow> P; \<And>d. \<lbrakk>a = i:deliver(d); R' = R; (p, deliver d, p') \<in> S\<rbrakk> \<Longrightarrow> P; \<And>m. \<lbrakk>a = {i}\<not>{}:arrive(m); R' = R; (p, receive m, p') \<in> S\<rbrakk> \<Longrightarrow> P; \<lbrakk>a = \<tau>; R' = R; (p, \<tau>, p') \<in> S\<rbrakk> \<Longrightarrow> P; \<And>m. \<lbrakk>a = {}\<not>{i}:arrive(m); R' = R; p = p'\<rbrakk> \<Longrightarrow> P; \<And>i i'. \<lbrakk>a = connect(i, i'); R' = R \<union> {i'}; p = p'\<rbrakk> \<Longrightarrow> P; \<And>i i'. \<lbrakk>a = connect(i', i); R' = R \<union> {i'}; p = p'\<rbrakk> \<Longrightarrow> P; \<And>i i'. \<lbrakk>a = disconnect(i, i'); R' = R - {i'}; p = p'\<rbrakk> \<Longrightarrow> P; \<And>i i'. \<lbrakk>a = disconnect(i', i); R' = R - {i'}; p = p'\<rbrakk> \<Longrightarrow> P; \<And>i i' i''. \<lbrakk>a = connect(i', i''); R' = R; p = p'; i \<noteq> i'; i \<noteq> i''\<rbrakk> \<Longrightarrow> P; \<And>i i' i''. \<lbrakk>a = disconnect(i', i''); R' = R; p = p'; i \<noteq> i'; i \<noteq> i''\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (erule node_sos.cases) simp_all


[STATEMENT]
lemma pnet_sos_never_newpkt:
  assumes "(st, a, st') \<in> pnet_sos S T"
      and "\<And>i d di a s s'. (s, a, s') \<in> S \<Longrightarrow> a \<noteq> i:newpkt(d, di)"
      and "\<And>i d di a t t'. (t, a, t') \<in> T \<Longrightarrow> a \<noteq> i:newpkt(d, di)"
    shows "a \<noteq> i:newpkt(d, di)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(st, a, st') \<in> pnet_sos S T

goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
by cases (auto dest!: assms(2-3))


[STATEMENT]
lemma pnet_node_init [elim, simp]:
  assumes "s \<in> init (pnet np \<langle>i; R\<rangle>)"
    shows "s \<in> { NodeS i s R |s. s \<in> init (np i)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> {NodeS i s R |s. s \<in> init (np i)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> init (pnet np \<langle>i; R\<rangle>)

goal (1 subgoal):
 1. s \<in> {NodeS i s R |s. s \<in> init (np i)}
[PROOF STEP]
by (simp add: node_comp_def)


[STATEMENT]
lemma pnet_node_init' [elim]:
 assumes "s \<in> init (pnet np \<langle>i; R\<rangle>)"
 obtains ns where "s = NodeS i ns R"
             and "ns \<in> init (np i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>s = NodeS i ns R; ns \<in> init (np i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> init (pnet np \<langle>i; R\<rangle>)

goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>s = NodeS i ns R; ns \<in> init (np i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: node_comp_def)


[STATEMENT]
lemma pnet_node_trans [elim, simp]:
  assumes "(s, a, s') \<in> trans (pnet np \<langle>i; R\<rangle>)"
    shows "(s, a, s') \<in> node_sos (trans (np i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, a, s') \<in> node_sos (automaton.trans (np i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(s, a, s') \<in> automaton.trans (pnet np \<langle>i; R\<rangle>)

goal (1 subgoal):
 1. (s, a, s') \<in> node_sos (automaton.trans (np i))
[PROOF STEP]
by (simp add: trans_node_comp)


[STATEMENT]
lemma pnet_never_newpkt':
  assumes "(s, a, s') \<in> trans (pnet np n)"
    shows "\<forall>i d di. a \<noteq> i:newpkt(d, di)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(s, a, s') \<in> automaton.trans (pnet np n)

goal (1 subgoal):
 1. \<forall>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
proof (induction n arbitrary: s a s')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i R s a s'. (s, a, s') \<in> automaton.trans (pnet np \<langle>i; R\<rangle>) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)
 2. \<And>n1 n2 s a s'. \<lbrakk>\<And>s a s'. (s, a, s') \<in> automaton.trans (pnet np n1) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di); \<And>s a s'. (s, a, s') \<in> automaton.trans (pnet np n2) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di); (s, a, s') \<in> automaton.trans (pnet np (n1 \<parallel> n2))\<rbrakk> \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
fix n1 n2 s a s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i R s a s'. (s, a, s') \<in> automaton.trans (pnet np \<langle>i; R\<rangle>) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)
 2. \<And>n1 n2 s a s'. \<lbrakk>\<And>s a s'. (s, a, s') \<in> automaton.trans (pnet np n1) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di); \<And>s a s'. (s, a, s') \<in> automaton.trans (pnet np n2) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di); (s, a, s') \<in> automaton.trans (pnet np (n1 \<parallel> n2))\<rbrakk> \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
assume IH1: "\<And>s a s'. (s, a, s') \<in> trans (pnet np n1) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)"
       and IH2: "\<And>s a s'. (s, a, s') \<in> trans (pnet np n2) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)"
       and "(s, a, s') \<in> trans (pnet np (n1 \<parallel> n2))"
[PROOF STATE]
proof (state)
this:
(?s, ?a, ?s') \<in> automaton.trans (pnet np n1) \<Longrightarrow> \<forall>i d di. ?a \<noteq> i:newpkt(d, di)
(?s, ?a, ?s') \<in> automaton.trans (pnet np n2) \<Longrightarrow> \<forall>i d di. ?a \<noteq> i:newpkt(d, di)
(s, a, s') \<in> automaton.trans (pnet np (n1 \<parallel> n2))

goal (2 subgoals):
 1. \<And>i R s a s'. (s, a, s') \<in> automaton.trans (pnet np \<langle>i; R\<rangle>) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)
 2. \<And>n1 n2 s a s'. \<lbrakk>\<And>s a s'. (s, a, s') \<in> automaton.trans (pnet np n1) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di); \<And>s a s'. (s, a, s') \<in> automaton.trans (pnet np n2) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di); (s, a, s') \<in> automaton.trans (pnet np (n1 \<parallel> n2))\<rbrakk> \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
show "\<forall>i d di. a \<noteq> i:newpkt(d, di)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
fix i d di
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
from \<open>(s, a, s') \<in> trans (pnet np (n1 \<parallel> n2))\<close>
[PROOF STATE]
proof (chain)
picking this:
(s, a, s') \<in> automaton.trans (pnet np (n1 \<parallel> n2))
[PROOF STEP]
have "(s, a, s') \<in> pnet_sos (trans (pnet np n1)) (trans (pnet np n2))"
[PROOF STATE]
proof (prove)
using this:
(s, a, s') \<in> automaton.trans (pnet np (n1 \<parallel> n2))

goal (1 subgoal):
 1. (s, a, s') \<in> pnet_sos (automaton.trans (pnet np n1)) (automaton.trans (pnet np n2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(s, a, s') \<in> pnet_sos (automaton.trans (pnet np n1)) (automaton.trans (pnet np n2))

goal (1 subgoal):
 1. \<And>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
thus "a \<noteq> i:newpkt(d, di)"
[PROOF STATE]
proof (prove)
using this:
(s, a, s') \<in> pnet_sos (automaton.trans (pnet np n1)) (automaton.trans (pnet np n2))

goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
by (rule pnet_sos_never_newpkt) (auto dest!: IH1 IH2)
[PROOF STATE]
proof (state)
this:
a \<noteq> i:newpkt(d, di)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i d di. a \<noteq> i:newpkt(d, di)

goal (1 subgoal):
 1. \<And>i R s a s'. (s, a, s') \<in> automaton.trans (pnet np \<langle>i; R\<rangle>) \<Longrightarrow> \<forall>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
qed (simp add: node_comps)


[STATEMENT]
lemma pnet_never_newpkt:
  assumes "(s, a, s') \<in> trans (pnet np n)"
    shows "a \<noteq> i:newpkt(d, di)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(s, a, s') \<in> automaton.trans (pnet np n)
[PROOF STEP]
have "\<forall>i d di. a \<noteq> i:newpkt(d, di)"
[PROOF STATE]
proof (prove)
using this:
(s, a, s') \<in> automaton.trans (pnet np n)

goal (1 subgoal):
 1. \<forall>i d di. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
by (rule pnet_never_newpkt')
[PROOF STATE]
proof (state)
this:
\<forall>i d di. a \<noteq> i:newpkt(d, di)

goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i d di. a \<noteq> i:newpkt(d, di)

goal (1 subgoal):
 1. a \<noteq> i:newpkt(d, di)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
a \<noteq> i:newpkt(d, di)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complete_no_cast [simp]:
  "(s, R:*cast(m), s') \<notin> cnet_sos T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, R:*cast(m), s') \<notin> cnet_sos T
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (s, R:*cast(m), s') \<in> cnet_sos T \<Longrightarrow> False
[PROOF STEP]
assume "(s, R:*cast(m), s') \<in> cnet_sos T"
[PROOF STATE]
proof (state)
this:
(s, R:*cast(m), s') \<in> cnet_sos T

goal (1 subgoal):
 1. (s, R:*cast(m), s') \<in> cnet_sos T \<Longrightarrow> False
[PROOF STEP]
hence "R:*cast(m) \<noteq> R:*cast(m)"
[PROOF STATE]
proof (prove)
using this:
(s, R:*cast(m), s') \<in> cnet_sos T

goal (1 subgoal):
 1. R:*cast(m) \<noteq> R:*cast(m)
[PROOF STEP]
by (rule cnet_sos.cases) auto
[PROOF STATE]
proof (state)
this:
R:*cast(m) \<noteq> R:*cast(m)

goal (1 subgoal):
 1. (s, R:*cast(m), s') \<in> cnet_sos T \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
R:*cast(m) \<noteq> R:*cast(m)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complete_no_arrive [simp]:
  "(s, ii\<not>ni:arrive(m), s') \<notin> cnet_sos T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, ii\<not>ni:arrive(m), s') \<notin> cnet_sos T
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (s, ii\<not>ni:arrive(m), s') \<in> cnet_sos T \<Longrightarrow> False
[PROOF STEP]
assume "(s, ii\<not>ni:arrive(m), s') \<in> cnet_sos T"
[PROOF STATE]
proof (state)
this:
(s, ii\<not>ni:arrive(m), s') \<in> cnet_sos T

goal (1 subgoal):
 1. (s, ii\<not>ni:arrive(m), s') \<in> cnet_sos T \<Longrightarrow> False
[PROOF STEP]
hence "ii\<not>ni:arrive(m) \<noteq> ii\<not>ni:arrive(m)"
[PROOF STATE]
proof (prove)
using this:
(s, ii\<not>ni:arrive(m), s') \<in> cnet_sos T

goal (1 subgoal):
 1. ii\<not>ni:arrive(m) \<noteq> ii\<not>ni:arrive(m)
[PROOF STEP]
by (rule cnet_sos.cases) auto
[PROOF STATE]
proof (state)
this:
ii\<not>ni:arrive(m) \<noteq> ii\<not>ni:arrive(m)

goal (1 subgoal):
 1. (s, ii\<not>ni:arrive(m), s') \<in> cnet_sos T \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
ii\<not>ni:arrive(m) \<noteq> ii\<not>ni:arrive(m)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sorted_list_len_lt: "x \<subset> y \<Longrightarrow> finite y \<Longrightarrow> length (sorted_list_of_set x) < length (sorted_list_of_set y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<subset> y; finite y\<rbrakk> \<Longrightarrow> length (sorted_list_of_set x) < length (sorted_list_of_set y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<subset> y; finite y\<rbrakk> \<Longrightarrow> length (sorted_list_of_set x) < length (sorted_list_of_set y)
[PROOF STEP]
let ?x = "sorted_list_of_set x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<subset> y; finite y\<rbrakk> \<Longrightarrow> length (sorted_list_of_set x) < length (sorted_list_of_set y)
[PROOF STEP]
let ?y = "sorted_list_of_set y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<subset> y; finite y\<rbrakk> \<Longrightarrow> length (sorted_list_of_set x) < length (sorted_list_of_set y)
[PROOF STEP]
assume x_y: "x \<subset> y" and fin_y: "finite y"
[PROOF STATE]
proof (state)
this:
x \<subset> y
finite y

goal (1 subgoal):
 1. \<lbrakk>x \<subset> y; finite y\<rbrakk> \<Longrightarrow> length (sorted_list_of_set x) < length (sorted_list_of_set y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<subset> y
finite y
[PROOF STEP]
have card_x_y: "card x < card y" and fin_x: "finite x"
[PROOF STATE]
proof (prove)
using this:
x \<subset> y
finite y

goal (1 subgoal):
 1. card x < card y &&& finite x
[PROOF STEP]
by (auto simp add:psubset_card_mono finite_subset)
[PROOF STATE]
proof (state)
this:
card x < card y
finite x

goal (1 subgoal):
 1. \<lbrakk>x \<subset> y; finite y\<rbrakk> \<Longrightarrow> length (sorted_list_of_set x) < length (sorted_list_of_set y)
[PROOF STEP]
with fin_y
[PROOF STATE]
proof (chain)
picking this:
finite y
card x < card y
finite x
[PROOF STEP]
have "length ?x = card x" and "length ?y = card y"
[PROOF STATE]
proof (prove)
using this:
finite y
card x < card y
finite x

goal (1 subgoal):
 1. length (sorted_list_of_set x) = card x &&& length (sorted_list_of_set y) = card y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (sorted_list_of_set x) = card x
length (sorted_list_of_set y) = card y

goal (1 subgoal):
 1. \<lbrakk>x \<subset> y; finite y\<rbrakk> \<Longrightarrow> length (sorted_list_of_set x) < length (sorted_list_of_set y)
[PROOF STEP]
with card_x_y
[PROOF STATE]
proof (chain)
picking this:
card x < card y
length (sorted_list_of_set x) = card x
length (sorted_list_of_set y) = card y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card x < card y
length (sorted_list_of_set x) = card x
length (sorted_list_of_set y) = card y

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_sorted_list:
  "wf ((\<lambda>(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ((\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
[PROOF STEP]
apply (unfold finite_psubset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ((\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B})
[PROOF STEP]
apply (rule wf_measure [THEN wf_subset])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B} \<subseteq> measure ?f1
[PROOF STEP]
apply (simp add: measure_def inv_image_def image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>a b. a \<subset> b \<and> finite b \<and> y = (sorted_list_of_set a, sorted_list_of_set b)} \<subseteq> {(x, y). ?f1 x < ?f1 y}
[PROOF STEP]
by (auto intro: sorted_list_len_lt)


[STATEMENT]
lemma sorted_list_psub:
  "sorted w \<longrightarrow>
   w \<noteq> [] \<longrightarrow>
   (sorted_list_of_set (set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sorted_Less.sorted w \<longrightarrow> w \<noteq> [] \<longrightarrow> (sorted_list_of_set (set (tl w)), w) \<in> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \<subset> B \<and> finite B}
[PROOF STEP]
proof(intro strip, simp add:image_iff)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Sorted_Less.sorted w; w \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b
[PROOF STEP]
assume sorted_w: "sorted w" and w_n_nil: "w \<noteq> []"
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted w
w \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>Sorted_Less.sorted w; w \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b
[PROOF STEP]
let ?a = "set (tl w)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Sorted_Less.sorted w; w \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b
[PROOF STEP]
let ?b = "set w"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Sorted_Less.sorted w; w \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b
[PROOF STEP]
from sorted_w
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted w
[PROOF STEP]
have sorted_tl_w: "sorted (tl w)" and dist: "distinct w"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted w

goal (1 subgoal):
 1. Sorted_Less.sorted (tl w) &&& distinct w
[PROOF STEP]
by (induct w) (auto simp add: sorted_wrt_append )
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (tl w)
distinct w

goal (1 subgoal):
 1. \<lbrakk>Sorted_Less.sorted w; w \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b
[PROOF STEP]
with w_n_nil
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> []
Sorted_Less.sorted (tl w)
distinct w
[PROOF STEP]
have a_psub_b: "?a \<subset> ?b"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> []
Sorted_Less.sorted (tl w)
distinct w

goal (1 subgoal):
 1. set (tl w) \<subset> set w
[PROOF STEP]
by (induct w)auto
[PROOF STATE]
proof (state)
this:
set (tl w) \<subset> set w

goal (1 subgoal):
 1. \<lbrakk>Sorted_Less.sorted w; w \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b
[PROOF STEP]
from sorted_w sorted_tl_w
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted w
Sorted_Less.sorted (tl w)
[PROOF STEP]
have "w = sorted_list_of_set ?b" and "tl w = sorted_list_of_set (set (tl w))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted w
Sorted_Less.sorted (tl w)

goal (1 subgoal):
 1. w = sorted_list_of_set (set w) &&& tl w = sorted_list_of_set (set (tl w))
[PROOF STEP]
by (auto simp add: sorted_less_set_eq)
[PROOF STATE]
proof (state)
this:
w = sorted_list_of_set (set w)
tl w = sorted_list_of_set (set (tl w))

goal (1 subgoal):
 1. \<lbrakk>Sorted_Less.sorted w; w \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b
[PROOF STEP]
with a_psub_b
[PROOF STATE]
proof (chain)
picking this:
set (tl w) \<subset> set w
w = sorted_list_of_set (set w)
tl w = sorted_list_of_set (set (tl w))
[PROOF STEP]
show "\<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b"
[PROOF STATE]
proof (prove)
using this:
set (tl w) \<subset> set w
w = sorted_list_of_set (set w)
tl w = sorted_list_of_set (set (tl w))

goal (1 subgoal):
 1. \<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a b. a \<subset> b \<and> finite b \<and> sorted_list_of_set (set (tl w)) = sorted_list_of_set a \<and> w = sorted_list_of_set b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_semi: "semilat(A,r,f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (A, r, f)
[PROOF STEP]
by(insert nodes_semi_is_semilat) (auto simp add:nodes_semi_def A_def r_def f_def)

\<comment>\<open>used by acc\_le\_listI\<close>


[STATEMENT]
lemma Cons_less_Conss [simp]:
  "x#xs [\<sqsubset>\<^sub>r] y#ys = (x \<sqsubset>\<^sub>r y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^sub>r] ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs [\<sqsubset>\<^bsub>r\<^esub>] y # ys) = (x \<sqsubset>\<^bsub>r\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys)
[PROOF STEP]
apply (unfold lesssub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs [\<sqsubseteq>\<^bsub>r\<^esub>] y # ys \<and> x # xs \<noteq> y # ys) = ((x \<sqsubseteq>\<^bsub>r\<^esub> y \<and> x \<noteq> y) \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<or> x = y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<and> xs \<noteq> ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
apply (unfold lesssub_def lesub_def r_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; Listn.le nodes_le xs ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> nodes_le y y
[PROOF STEP]
apply (simp only: nodes_le_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma acc_le_listI [intro!]:
  "acc r \<Longrightarrow> acc (Listn.le r) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acc r \<Longrightarrow> acc (Listn.le r)
[PROOF STEP]
apply (unfold acc_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y} \<Longrightarrow> wf {(y, x). x [\<sqsubset>\<^bsub>r\<^esub>] y}
[PROOF STEP]
apply (subgoal_tac "Wellfounded.wf(UN n. {(ys,xs).  size xs = n \<and> size ys = n \<and> xs <_(Listn.le r) ys})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})\<rbrakk> \<Longrightarrow> wf {(y, x). x [\<sqsubset>\<^bsub>r\<^esub>] y}
 2. wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply (erule wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y} \<Longrightarrow> {(y, x). x [\<sqsubset>\<^bsub>r\<^esub>] y} \<subseteq> (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
 2. wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply (blast intro: lesssub_lengthD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply (rule wf_UN)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
 2. \<And>n j. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; j \<in> UNIV; {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; j \<in> UNIV; {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (rename_tac m n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (case_tac "m=n")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}; m = n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 2. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}; m \<noteq> n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 3. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}; m \<noteq> n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (fast intro!: equals0I dest: not_sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (rename_tac n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = 0 \<and> length ys = 0 \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
 2. \<And>n na. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = na \<and> length ys = na \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc na \<and> length ys = Suc na \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (simp add: lesssub_def cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = na \<and> length ys = na \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc na \<and> length ys = Suc na \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (rename_tac k)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = k \<and> length ys = k \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc k \<and> length ys = Suc k \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (simp add: wf_eq_minimal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q)\<rbrakk> \<Longrightarrow> \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = Suc k \<and> length y = Suc k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q)
[PROOF STEP]
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q)\<rbrakk> \<Longrightarrow> \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k Q x. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); x \<in> Q\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q
[PROOF STEP]
apply (rename_tac M m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (case_tac "\<exists>x xs. size xs = k \<and> x#xs \<in> M")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule thin_rl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule thin_rl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; (\<exists>x. x \<in> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}) \<longrightarrow> (\<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M})\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (thin_tac "\<exists>x xs. P x xs" for P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m z xs. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<forall>y. z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; z # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (rename_tac maxA xs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; (\<exists>x. x \<in> {ys. length ys = length xs \<and> maxA # ys \<in> M}) \<longrightarrow> (\<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M})\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m maxA xs. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {ys. length ys = length xs \<and> maxA # ys \<in> M}
 2. \<And>k M m maxA xs. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (thin_tac "m \<in> M")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (thin_tac "maxA#xs \<in> M")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. ?z205 k M m maxA xs z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> ?z205 k M m maxA xs z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> ?z205 k M m maxA xs z \<in> M
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> ?z205 k M m maxA xs z \<in> M
 2. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. ?z205 k M m maxA xs z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> ?z205 k M m maxA xs z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. maxA # z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> maxA # z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z y ya ys yb ysa. \<lbrakk>\<forall>y. ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length ys = length xs \<and> length y = length xs \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> ya # ys \<in> M}; length ys = length xs; ya # ys \<in> M; ya # ys [\<sqsubset>\<^bsub>r\<^esub>] yb # ysa; length ys = length xs; length ysa = length xs; yb # ysa \<in> M\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M xs ya ys yb ysa. \<lbrakk>\<forall>y. ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> (\<forall>xsa. length xsa = length xs \<longrightarrow> y # xsa \<notin> M); \<forall>y. length y = length xs \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<sqsubset>\<^bsub>r\<^esub> yb \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] ysa \<or> ya = yb \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] ysa; length ys = length xs; length ysa = length xs; yb # ysa \<in> M\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_listn: "wf {(y,x). x \<sqsubset>\<^bsub>Listn.le r\<^esub> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x [\<sqsubset>\<^bsub>r\<^esub>] y}
[PROOF STEP]
by(insert acc_nodes_le acc_le_listI r_def)  (simp add:acc_def)


[STATEMENT]
lemma wf_listn': "wf {(y,x). x [\<sqsubset>\<^sub>r] y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x [\<sqsubset>\<^bsub>r\<^esub>] y}
[PROOF STEP]
by (rule wf_listn)


[STATEMENT]
lemma wf_listn_termination_rel:
  "wf ({(y,x). x \<sqsubset>\<^bsub>Listn.le r\<^esub> y}  <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ({(y, x). x [\<sqsubset>\<^bsub>r\<^esub>] y} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
[PROOF STEP]
by (insert wf_listn wf_sorted_list)  (fastforce dest:wf_lex_prod)


[STATEMENT]
lemma inA_is_sorted: "xs \<in> A \<Longrightarrow> sorted (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> A \<Longrightarrow> Sorted_Less.sorted (rev xs)
[PROOF STEP]
by (auto simp add:A_def sorted_less_sorted_list_of_set)


[STATEMENT]
lemma list_nA_lt_refl: "xs \<in> nlists n A \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> nlists n A \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<in> nlists n A \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
assume "xs \<in> nlists n A"
[PROOF STATE]
proof (state)
this:
xs \<in> nlists n A

goal (1 subgoal):
 1. xs \<in> nlists n A \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> nlists n A
[PROOF STEP]
have "set xs \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
xs \<in> nlists n A

goal (1 subgoal):
 1. set xs \<subseteq> A
[PROOF STEP]
by (rule nlistsE_set)
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> A

goal (1 subgoal):
 1. xs \<in> nlists n A \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set xs \<subseteq> A
[PROOF STEP]
have "\<forall>i<length xs. xs!i \<in> A"
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> A

goal (1 subgoal):
 1. \<forall>i<length xs. xs ! i \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. xs ! i \<in> A

goal (1 subgoal):
 1. xs \<in> nlists n A \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length xs. xs ! i \<in> A
[PROOF STEP]
have "\<forall>i<length xs. sorted (rev (xs!i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length xs. xs ! i \<in> A

goal (1 subgoal):
 1. \<forall>i<length xs. Sorted_Less.sorted (rev (xs ! i))
[PROOF STEP]
by (simp add:inA_is_sorted)
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. Sorted_Less.sorted (rev (xs ! i))

goal (1 subgoal):
 1. xs \<in> nlists n A \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length xs. Sorted_Less.sorted (rev (xs ! i))
[PROOF STEP]
show "xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length xs. Sorted_Less.sorted (rev (xs ! i))

goal (1 subgoal):
 1. xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs
[PROOF STEP]
by(unfold Listn.le_def lesub_def)
     (auto simp add:list_all2_conv_all_nth Listn.le_def r_def nodes_le_def)
[PROOF STATE]
proof (state)
this:
xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nil_inA: "[] \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> A
[PROOF STEP]
apply (unfold A_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
apply (subgoal_tac "{} \<in> Pow (set nodes)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {} \<in> Pow (set nodes) \<Longrightarrow> [] \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
 2. {} \<in> Pow (set nodes)
[PROOF STEP]
apply (subgoal_tac "[] = (\<lambda>x. rev (sorted_list_of_set x)) {}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>{} \<in> Pow (set nodes); [] = rev (sorted_list_of_set {})\<rbrakk> \<Longrightarrow> [] \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
 2. {} \<in> Pow (set nodes) \<Longrightarrow> [] = rev (sorted_list_of_set {})
 3. {} \<in> Pow (set nodes)
[PROOF STEP]
apply (fastforce intro:rev_image_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {} \<in> Pow (set nodes) \<Longrightarrow> [] = rev (sorted_list_of_set {})
 2. {} \<in> Pow (set nodes)
[PROOF STEP]
by auto


[STATEMENT]
lemma upt_n_in_pow_nodes: "{0..<n} \<in> Pow (set nodes)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<n} \<in> Pow (set nodes)
[PROOF STEP]
by(auto simp add:n_def nodes_def verts_set)


[STATEMENT]
lemma rev_all_inA: "rev [0..<n] \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [0..<n] \<in> A
[PROOF STEP]
proof(unfold A_def,simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rev [0..<n] \<in> (\<lambda>x. rev (sorted_list_of_set x)) ` Pow (set nodes)
[PROOF STEP]
let ?f = "\<lambda>x. rev (sorted_list_of_set x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rev [0..<n] \<in> (\<lambda>x. rev (sorted_list_of_set x)) ` Pow (set nodes)
[PROOF STEP]
have "rev [0..<n] =?f {0..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [0..<n] = rev (sorted_list_of_set {0..<n})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rev [0..<n] = rev (sorted_list_of_set {0..<n})

goal (1 subgoal):
 1. rev [0..<n] \<in> (\<lambda>x. rev (sorted_list_of_set x)) ` Pow (set nodes)
[PROOF STEP]
with upt_n_in_pow_nodes
[PROOF STATE]
proof (chain)
picking this:
{0..<n} \<in> Pow (set nodes)
rev [0..<n] = rev (sorted_list_of_set {0..<n})
[PROOF STEP]
show "rev [0..<n] \<in> ?f ` Pow (set nodes)"
[PROOF STATE]
proof (prove)
using this:
{0..<n} \<in> Pow (set nodes)
rev [0..<n] = rev (sorted_list_of_set {0..<n})

goal (1 subgoal):
 1. rev [0..<n] \<in> (\<lambda>x. rev (sorted_list_of_set x)) ` Pow (set nodes)
[PROOF STEP]
by (fastforce intro: image_eqI)
[PROOF STATE]
proof (state)
this:
rev [0..<n] \<in> (\<lambda>x. rev (sorted_list_of_set x)) ` Pow (set nodes)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma len_start_is_n: "length start = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length start = n
[PROOF STEP]
by (insert len_verts_gt0) (auto simp add:start_def n_def nodes_def dest:Suc_pred)


[STATEMENT]
lemma len_start_is_len_verts: "length start = length (g_V G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length start = length (g_V G)
[PROOF STEP]
using len_verts_gt0
[PROOF STATE]
proof (prove)
using this:
0 < length (g_V G)

goal (1 subgoal):
 1. length start = length (g_V G)
[PROOF STEP]
by (simp add:start_def)


[STATEMENT]
lemma start_len_gt_0: "length start > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length start
[PROOF STEP]
by (insert len_verts_gt0) (simp add:start_def)


[STATEMENT]
lemma start_subset_A: "set start \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set start \<subseteq> A
[PROOF STEP]
by(auto simp add:nil_inA rev_all_inA start_def)


[STATEMENT]
lemma start_in_A : "start \<in> (nlists n A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start \<in> nlists n A
[PROOF STEP]
by (insert start_subset_A len_start_is_n)(fastforce intro:nlistsI)


[STATEMENT]
lemma sorted_start_nth: "i < n \<Longrightarrow> sorted (rev (start!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> Sorted_Less.sorted (rev (start ! i))
[PROOF STEP]
apply(subgoal_tac "start!i \<in> A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < n; start ! i \<in> A\<rbrakk> \<Longrightarrow> Sorted_Less.sorted (rev (start ! i))
 2. i < n \<Longrightarrow> start ! i \<in> A
[PROOF STEP]
apply (fastforce dest:inA_is_sorted)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> start ! i \<in> A
[PROOF STEP]
by (auto simp add:start_subset_A  len_start_is_n)


[STATEMENT]
lemma start_nth0_empty: "start!0 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start ! 0 = []
[PROOF STEP]
by (simp add:start_def)


[STATEMENT]
lemma start_nth_lt0_all: "\<forall>p\<in>{1..< length start}. start!p = (rev [0..<n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>{1..<length start}. start ! p = rev [0..<n]
[PROOF STEP]
by (auto simp add:start_def)


[STATEMENT]
lemma in_nodes_lt_n: "x \<in> set (g_V G) \<Longrightarrow> x < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (g_V G) \<Longrightarrow> x < n
[PROOF STEP]
by (simp add:n_def nodes_def verts_set)


[STATEMENT]
lemma start_nth0_unstable_auxi: "\<not> [0] \<sqsubseteq>\<^bsub>r\<^esub> (rev [0..<n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> [0] \<sqsubseteq>\<^bsub>r\<^esub> rev [0..<n]
[PROOF STEP]
by (insert len_verts_gt1 verts_ge_Suc0)
  (auto simp add:r_def lesssub_def lesub_def nodes_le_def n_def nodes_def)


[STATEMENT]
lemma start_nth0_unstable: "\<not> stable r step start 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Typing_Framework_1.stable r step start 0
[PROOF STEP]
proof(rule notI,auto simp add: start_nth0_empty stable_def step_def exec_def transf_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>set (sorted_list_of_set (succs 0)). [0] \<sqsubseteq>\<^bsub>r\<^esub> start ! x \<Longrightarrow> False
[PROOF STEP]
assume ass: "\<forall>x\<in>set (sorted_list_of_set (succs 0)). [0] \<sqsubseteq>\<^bsub>r\<^esub> start ! x"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (sorted_list_of_set (succs 0)). [0] \<sqsubseteq>\<^bsub>r\<^esub> start ! x

goal (1 subgoal):
 1. \<forall>x\<in>set (sorted_list_of_set (succs 0)). [0] \<sqsubseteq>\<^bsub>r\<^esub> start ! x \<Longrightarrow> False
[PROOF STEP]
from succ_of_entry0
[PROOF STATE]
proof (chain)
picking this:
\<exists>s. (0, s) \<in> g_E G \<and> s \<noteq> 0
[PROOF STEP]
obtain s where "s \<in> succs 0" and "s \<noteq> 0 \<and> s \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s. (0, s) \<in> g_E G \<and> s \<noteq> 0

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> succs 0; s \<noteq> 0 \<and> s \<in> set (g_V G)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using head_is_vert
[PROOF STATE]
proof (prove)
using this:
\<exists>s. (0, s) \<in> g_E G \<and> s \<noteq> 0
(?u, ?v) \<in> g_E G \<Longrightarrow> ?v \<in> set (g_V G)

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> succs 0; s \<noteq> 0 \<and> s \<in> set (g_V G)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add:succs_def)
[PROOF STATE]
proof (state)
this:
s \<in> succs 0
s \<noteq> 0 \<and> s \<in> set (g_V G)

goal (1 subgoal):
 1. \<forall>x\<in>set (sorted_list_of_set (succs 0)). [0] \<sqsubseteq>\<^bsub>r\<^esub> start ! x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> succs 0
s \<noteq> 0 \<and> s \<in> set (g_V G)
[PROOF STEP]
have "s \<in> set (sorted_list_of_set (succs 0))"
        and "start!s = (rev [0..<n])"
[PROOF STATE]
proof (prove)
using this:
s \<in> succs 0
s \<noteq> 0 \<and> s \<in> set (g_V G)

goal (1 subgoal):
 1. s \<in> set (sorted_list_of_set (succs 0)) &&& start ! s = rev [0..<n]
[PROOF STEP]
using fin_succs verts_set len_verts_gt0
[PROOF STATE]
proof (prove)
using this:
s \<in> succs 0
s \<noteq> 0 \<and> s \<in> set (g_V G)
\<forall>v\<in>set (g_V G). finite (succs v)
set (g_V G) = {0..<length (g_V G)}
0 < length (g_V G)

goal (1 subgoal):
 1. s \<in> set (sorted_list_of_set (succs 0)) &&& start ! s = rev [0..<n]
[PROOF STEP]
by (auto simp add:start_def)
[PROOF STATE]
proof (state)
this:
s \<in> set (sorted_list_of_set (succs 0))
start ! s = rev [0..<n]

goal (1 subgoal):
 1. \<forall>x\<in>set (sorted_list_of_set (succs 0)). [0] \<sqsubseteq>\<^bsub>r\<^esub> start ! x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> set (sorted_list_of_set (succs 0))
start ! s = rev [0..<n]
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
s \<in> set (sorted_list_of_set (succs 0))
start ! s = rev [0..<n]

goal (1 subgoal):
 1. False
[PROOF STEP]
using ass start_nth0_unstable_auxi
[PROOF STATE]
proof (prove)
using this:
s \<in> set (sorted_list_of_set (succs 0))
start ! s = rev [0..<n]
\<forall>x\<in>set (sorted_list_of_set (succs 0)). [0] \<sqsubseteq>\<^bsub>r\<^esub> start ! x
\<not> [0] \<sqsubseteq>\<^bsub>r\<^esub> rev [0..<n]

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma start_nth_unstable:
  assumes "p \<in> {1 ..< length (g_V G)} "
      and "succs p \<noteq> {}"
    shows "\<not> stable r step start p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Typing_Framework_1.stable r step start p
[PROOF STEP]
proof (rule notI, unfold stable_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
let ?step_p = "step p (start ! p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
let ?rev_all = "rev[0..<length(g_V G)]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
assume sta: "\<forall>(q, \<tau>)\<in>set ?step_p. \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q"
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
p \<in> {1..<length (g_V G)}
[PROOF STEP]
have n_sorted: "\<not> sorted (rev (p # ?rev_all))"
                 and p:"p \<in> set (g_V G)" and "start!p = ?rev_all"
[PROOF STATE]
proof (prove)
using this:
p \<in> {1..<length (g_V G)}

goal (1 subgoal):
 1. \<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) &&& p \<in> set (g_V G) &&& start ! p = rev [0..<length (g_V G)]
[PROOF STEP]
using verts_set
[PROOF STATE]
proof (prove)
using this:
p \<in> {1..<length (g_V G)}
set (g_V G) = {0..<length (g_V G)}

goal (1 subgoal):
 1. \<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) &&& p \<in> set (g_V G) &&& start ! p = rev [0..<length (g_V G)]
[PROOF STEP]
by (auto simp add:n_def nodes_def start_def sorted_wrt_append)
[PROOF STATE]
proof (state)
this:
\<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)]))
p \<in> set (g_V G)
start ! p = rev [0..<length (g_V G)]

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
with sta
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q
\<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)]))
p \<in> set (g_V G)
start ! p = rev [0..<length (g_V G)]
[PROOF STEP]
have step_p: "\<forall>(q, \<tau>)\<in>set ?step_p. sorted (rev (p # ?rev_all)) \<or> (p # ?rev_all = start!q)"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q
\<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)]))
p \<in> set (g_V G)
start ! p = rev [0..<length (g_V G)]

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) \<or> p # rev [0..<length (g_V G)] = start ! q
[PROOF STEP]
by (auto simp add:step_def exec_def transf_def lesssub_def lesub_def r_def nodes_le_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) \<or> p # rev [0..<length (g_V G)] = start ! q

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
from assms(2) fin_succs p
[PROOF STATE]
proof (chain)
picking this:
succs p \<noteq> {}
\<forall>v\<in>set (g_V G). finite (succs v)
p \<in> set (g_V G)
[PROOF STEP]
obtain a b where a_b: "(a, b) \<in> set ?step_p"
[PROOF STATE]
proof (prove)
using this:
succs p \<noteq> {}
\<forall>v\<in>set (g_V G). finite (succs v)
p \<in> set (g_V G)

goal (1 subgoal):
 1. (\<And>a b. (a, b) \<in> set (step p (start ! p)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add:step_def exec_def transf_def)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> set (step p (start ! p))

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
with step_p
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) \<or> p # rev [0..<length (g_V G)] = start ! q
(a, b) \<in> set (step p (start ! p))
[PROOF STEP]
have "sorted (rev (p # ?rev_all)) \<or> (p # ?rev_all = start!a)"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) \<or> p # rev [0..<length (g_V G)] = start ! q
(a, b) \<in> set (step p (start ! p))

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) \<or> p # rev [0..<length (g_V G)] = start ! a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) \<or> p # rev [0..<length (g_V G)] = start ! a

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
with n_sorted
[PROOF STATE]
proof (chain)
picking this:
\<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)]))
Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) \<or> p # rev [0..<length (g_V G)] = start ! a
[PROOF STEP]
have eq_p_cons: "(p # ?rev_all = start!a)"
[PROOF STATE]
proof (prove)
using this:
\<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)]))
Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)])) \<or> p # rev [0..<length (g_V G)] = start ! a

goal (1 subgoal):
 1. p # rev [0..<length (g_V G)] = start ! a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p # rev [0..<length (g_V G)] = start ! a

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (g_V G)
[PROOF STEP]
have "\<forall>(q, \<tau>)\<in>set ?step_p. q < n"
[PROOF STATE]
proof (prove)
using this:
p \<in> set (g_V G)

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). q < n
[PROOF STEP]
using succ_in_G fin_succs verts_set n_def nodes_def
[PROOF STATE]
proof (prove)
using this:
p \<in> set (g_V G)
\<forall>v\<in>succs ?n. v \<in> set (g_V G)
\<forall>v\<in>set (g_V G). finite (succs v)
set (g_V G) = {0..<length (g_V G)}
n \<equiv> length nodes
nodes \<equiv> g_V G

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). q < n
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). q < n

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
with a_b
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> set (step p (start ! p))
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). q < n
[PROOF STEP]
have "a < n"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> set (step p (start ! p))
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). q < n

goal (1 subgoal):
 1. a < n
[PROOF STEP]
using len_start_is_n
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> set (step p (start ! p))
\<forall>(q, \<tau>)\<in>set (step p (start ! p)). q < n
length start = n

goal (1 subgoal):
 1. a < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a < n

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a < n
[PROOF STEP]
have "sorted (rev (start!a))"
[PROOF STATE]
proof (prove)
using this:
a < n

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (start ! a))
[PROOF STEP]
using sorted_start_nth
[PROOF STATE]
proof (prove)
using this:
a < n
?i < n \<Longrightarrow> Sorted_Less.sorted (rev (start ! ?i))

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (start ! a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (start ! a))

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (start ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> start ! q \<Longrightarrow> False
[PROOF STEP]
with eq_p_cons n_sorted
[PROOF STATE]
proof (chain)
picking this:
p # rev [0..<length (g_V G)] = start ! a
\<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)]))
Sorted_Less.sorted (rev (start ! a))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
p # rev [0..<length (g_V G)] = start ! a
\<not> Sorted_Less.sorted (rev (p # rev [0..<length (g_V G)]))
Sorted_Less.sorted (rev (start ! a))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma start_unstable_cond:
  assumes "succs p \<noteq> {} "
      and "p < length (g_V G)"
    shows "\<not> stable r step start p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Typing_Framework_1.stable r step start p
[PROOF STEP]
using assms start_nth0_unstable start_nth_unstable
[PROOF STATE]
proof (prove)
using this:
succs p \<noteq> {}
p < length (g_V G)
\<not> Typing_Framework_1.stable r step start 0
\<lbrakk>?p \<in> {1..<length (g_V G)}; succs ?p \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> Typing_Framework_1.stable r step start ?p

goal (1 subgoal):
 1. \<not> Typing_Framework_1.stable r step start p
[PROOF STEP]
by(cases "p = 0")  auto


[STATEMENT]
lemma unstable_start: "unstables r step start = sorted_list_of_set ({p. succs p \<noteq> {} \<and> p < length start})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unstables r step start = sorted_list_of_set {p. succs p \<noteq> {} \<and> p < length start}
[PROOF STEP]
using len_start_is_len_verts start_unstable_cond
[PROOF STATE]
proof (prove)
using this:
length start = length (g_V G)
\<lbrakk>succs ?p \<noteq> {}; ?p < length (g_V G)\<rbrakk> \<Longrightarrow> \<not> Typing_Framework_1.stable r step start ?p

goal (1 subgoal):
 1. unstables r step start = sorted_list_of_set {p. succs p \<noteq> {} \<and> p < length start}
[PROOF STEP]
by (subgoal_tac "{p. p < length start \<and> \<not> stable r step start p} = {p. succs p \<noteq> {} \<and> p < length start}")
     (auto simp add: unstables_def stable_def step_def exec_def)