[STATEMENT]
lemma bounded_exec':
  fixes ss w a b
  assumes w_n_nil: " w \<noteq> [] "
       and step_hdw: " (a, b) \<in> set (step (hd w) (ss ! hd w)) "
       and w_lt_n:"\<forall>p\<in>set w. p < n "
      shows" a < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w \<noteq> []
(a, b) \<in> set (step (hd w) (ss ! hd w))
\<forall>p\<in>set w. p < n

goal (1 subgoal):
 1. a < n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>w \<noteq> []; (a, b) \<in> set (step (hd w) (ss ! hd w)); \<forall>p\<in>set w. p < n\<rbrakk> \<Longrightarrow> a < n
[PROOF STEP]
from w_lt_n
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set w. p < n
[PROOF STEP]
have "hd w < n"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set w. p < n

goal (1 subgoal):
 1. hd w < n
[PROOF STEP]
using w_n_nil
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set w. p < n
w \<noteq> []

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

goal (1 subgoal):
 1. \<lbrakk>w \<noteq> []; (a, b) \<in> set (step (hd w) (ss ! hd w)); \<forall>p\<in>set w. p < n\<rbrakk> \<Longrightarrow> a < n
[PROOF STEP]
with bounded_exec
[PROOF STATE]
proof (chain)
picking this:
bounded step n
hd w < n
[PROOF STEP]
have "( \<forall>\<tau>. \<forall>(q,\<tau>') \<in> set (step (hd w) \<tau>). q<n)"
[PROOF STATE]
proof (prove)
using this:
bounded step n
hd w < n

goal (1 subgoal):
 1. \<forall>\<tau>. \<forall>(q, \<tau>')\<in>set (step (hd w) \<tau>). q < n
[PROOF STEP]
by (auto simp add:bounded_def)
[PROOF STATE]
proof (state)
this:
\<forall>\<tau>. \<forall>(q, \<tau>')\<in>set (step (hd w) \<tau>). q < n

goal (1 subgoal):
 1. \<lbrakk>w \<noteq> []; (a, b) \<in> set (step (hd w) (ss ! hd w)); \<forall>p\<in>set w. p < n\<rbrakk> \<Longrightarrow> a < n
[PROOF STEP]
with step_hdw
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> set (step (hd w) (ss ! hd w))
\<forall>\<tau>. \<forall>(q, \<tau>')\<in>set (step (hd w) \<tau>). q < n
[PROOF STEP]
show "a < n"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> set (step (hd w) (ss ! hd w))
\<forall>\<tau>. \<forall>(q, \<tau>')\<in>set (step (hd w) \<tau>). q < n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_dom_w:
  assumes "wf_dom ss w"
  shows "sorted w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sorted_Less.sorted w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. Sorted_Less.sorted w
[PROOF STEP]
by (auto simp add:wf_dom_def)


[STATEMENT]
lemma wf_dom_w2:
  assumes "wf_dom ss w"
  shows "(\<forall>x\<in>set w. x < n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set w. x < n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. \<forall>x\<in>set w. x < n
[PROOF STEP]
by (auto simp add:wf_dom_def)


[STATEMENT]
lemma wf_dom_len_eq:
  assumes "wf_dom ss w"
  shows "(length ss = n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ss = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. length ss = n
[PROOF STEP]
by (auto simp add:wf_dom_def)


[STATEMENT]
lemma  wf_dom_inA:
  assumes "wf_dom ss w"
  shows "ss \<in> nlists n A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss \<in> nlists n A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. ss \<in> nlists n A
[PROOF STEP]
by (auto simp add:wf_dom_def intro: nlistsI)


[STATEMENT]
lemma wf_dom_le:
  assumes wf_ss_w: "wf_dom ss w"
  shows "ss [\<sqsubseteq>\<^bsub>r\<^esub>] ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss [\<sqsubseteq>\<^bsub>r\<^esub>] ss
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. ss [\<sqsubseteq>\<^bsub>r\<^esub>] ss
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_dom ss w \<Longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ss
[PROOF STEP]
from wf_ss_w
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
[PROOF STEP]
have  "\<forall>i<length ss. ss!i \<in> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

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

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

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

goal (1 subgoal):
 1. wf_dom ss w \<Longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ss
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length ss. Sorted_Less.sorted (rev (ss ! i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length ss. Sorted_Less.sorted (rev (ss ! i))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pres_transf:
  "\<forall>ss\<in>A. p < n \<longrightarrow> (\<forall>x<length ss. p > ss!x) \<longrightarrow> transf p ss \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ss\<in>A. p < n \<longrightarrow> (\<forall>x<length ss. ss ! x < p) \<longrightarrow> transf p ss \<in> A
[PROOF STEP]
proof(intro strip, unfold transf_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ss. \<lbrakk>ss \<in> A; p < n; \<forall>x<length ss. ss ! x < p\<rbrakk> \<Longrightarrow> p # ss \<in> A
[PROOF STEP]
fix ss
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ss. \<lbrakk>ss \<in> A; p < n; \<forall>x<length ss. ss ! x < p\<rbrakk> \<Longrightarrow> p # ss \<in> A
[PROOF STEP]
assume  p_lt_n: "p < n" and p_gt:  "\<forall>x<length ss. ss!x < p" and \<tau>_in_A: "ss \<in> A"
[PROOF STATE]
proof (state)
this:
p < n
\<forall>x<length ss. ss ! x < p
ss \<in> A

goal (1 subgoal):
 1. \<And>ss. \<lbrakk>ss \<in> A; p < n; \<forall>x<length ss. ss ! x < p\<rbrakk> \<Longrightarrow> p # ss \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p < n
\<forall>x<length ss. ss ! x < p
ss \<in> A
[PROOF STEP]
have "set ss \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
p < n
\<forall>x<length ss. ss ! x < p
ss \<in> A

goal (1 subgoal):
 1. set ss \<subseteq> set nodes
[PROOF STEP]
by (unfold A_def) (rule inpow_subset_nodes)
[PROOF STATE]
proof (state)
this:
set ss \<subseteq> set nodes

goal (1 subgoal):
 1. \<And>ss. \<lbrakk>ss \<in> A; p < n; \<forall>x<length ss. ss ! x < p\<rbrakk> \<Longrightarrow> p # ss \<in> A
[PROOF STEP]
with p_lt_n
[PROOF STATE]
proof (chain)
picking this:
p < n
set ss \<subseteq> set nodes
[PROOF STEP]
have p_\<tau>_in: "set (p # ss) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
p < n
set ss \<subseteq> set nodes

goal (1 subgoal):
 1. set (p # ss) \<subseteq> set nodes
[PROOF STEP]
by (auto simp add:n_def nodes_def verts_set)
[PROOF STATE]
proof (state)
this:
set (p # ss) \<subseteq> set nodes

goal (1 subgoal):
 1. \<And>ss. \<lbrakk>ss \<in> A; p < n; \<forall>x<length ss. ss ! x < p\<rbrakk> \<Longrightarrow> p # ss \<in> A
[PROOF STEP]
from \<tau>_in_A
[PROOF STATE]
proof (chain)
picking this:
ss \<in> A
[PROOF STEP]
have sorted_\<tau>: "sorted (rev ss)"
[PROOF STATE]
proof (prove)
using this:
ss \<in> A

goal (1 subgoal):
 1. Sorted_Less.sorted (rev ss)
[PROOF STEP]
by (simp add:inA_is_sorted)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev ss)

goal (1 subgoal):
 1. \<And>ss. \<lbrakk>ss \<in> A; p < n; \<forall>x<length ss. ss ! x < p\<rbrakk> \<Longrightarrow> p # ss \<in> A
[PROOF STEP]
with p_gt
[PROOF STATE]
proof (chain)
picking this:
\<forall>x<length ss. ss ! x < p
Sorted_Less.sorted (rev ss)
[PROOF STEP]
have "sorted (rev (p # ss))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x<length ss. ss ! x < p
Sorted_Less.sorted (rev ss)

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (p # ss))
[PROOF STEP]
using Cons_sorted_less_nth
[PROOF STATE]
proof (prove)
using this:
\<forall>x<length ss. ss ! x < p
Sorted_Less.sorted (rev ss)
\<lbrakk>\<forall>x<length ?xs. ?xs ! x < ?p; Sorted_Less.sorted (rev ?xs)\<rbrakk> \<Longrightarrow> Sorted_Less.sorted (rev (?p # ?xs))

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (p # ss))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (p # ss))

goal (1 subgoal):
 1. \<And>ss. \<lbrakk>ss \<in> A; p < n; \<forall>x<length ss. ss ! x < p\<rbrakk> \<Longrightarrow> p # ss \<in> A
[PROOF STEP]
with p_\<tau>_in
[PROOF STATE]
proof (chain)
picking this:
set (p # ss) \<subseteq> set nodes
Sorted_Less.sorted (rev (p # ss))
[PROOF STEP]
show "(p # ss) \<in> A"
[PROOF STATE]
proof (prove)
using this:
set (p # ss) \<subseteq> set nodes
Sorted_Less.sorted (rev (p # ss))

goal (1 subgoal):
 1. p # ss \<in> A
[PROOF STEP]
by (unfold A_def) (fastforce intro: subset_nodes_inpow)
[PROOF STATE]
proof (state)
this:
p # ss \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pres_exec:
  assumes "(q,\<tau>) \<in> set (step p (ss!p))"
      and "\<forall>n \<in> set (ss!p). p > n"
      and "ss!p \<in> A"
      and "p < n"
    shows "\<tau> \<in> A "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(q, \<tau>) \<in> set (step p (ss ! p))
\<forall>n\<in>set (ss ! p). n < p
ss ! p \<in> A
p < n

goal (1 subgoal):
 1. \<tau> \<in> A
[PROOF STEP]
by (auto simp add:step_def exec_def pres_transf)


[STATEMENT]
lemma wf_hd_neq_all:
  assumes wf_ss_w: "wf_dom ss w "
      and w_n_nil: "w \<noteq> [] "
    shows " ss!(hd w) \<noteq> rev [0..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss ! hd w \<noteq> rev [0..<n]
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ss ! hd w \<noteq> rev [0..<n] \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ss ! hd w \<noteq>  (rev [0..<n])"
[PROOF STATE]
proof (state)
this:
\<not> ss ! hd w \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<not> ss ! hd w \<noteq> rev [0..<n] \<Longrightarrow> False
[PROOF STEP]
note x = this
[PROOF STATE]
proof (state)
this:
\<not> ss ! hd w \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<not> ss ! hd w \<noteq> rev [0..<n] \<Longrightarrow> False
[PROOF STEP]
from wf_ss_w
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
[PROOF STEP]
have "\<forall>x\<in> set w. x < n" and "sorted w"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. \<forall>x\<in>set w. x < n &&& Sorted_Less.sorted w
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set w. x < n
Sorted_Less.sorted w

goal (1 subgoal):
 1. \<not> ss ! hd w \<noteq> rev [0..<n] \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set w. x < n
Sorted_Less.sorted w
[PROOF STEP]
have "hd w < n" and y:"\<forall>x \<in> set w. x \<ge> hd w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set w. x < n
Sorted_Less.sorted w

goal (1 subgoal):
 1. hd w < n &&& \<forall>x\<in>set w. hd w \<le> x
[PROOF STEP]
using w_n_nil
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set w. x < n
Sorted_Less.sorted w
w \<noteq> []

goal (1 subgoal):
 1. hd w < n &&& \<forall>x\<in>set w. hd w \<le> x
[PROOF STEP]
by (induct w) (auto simp add:sorted_wrt_append)
[PROOF STATE]
proof (state)
this:
hd w < n
\<forall>x\<in>set w. hd w \<le> x

goal (1 subgoal):
 1. \<not> ss ! hd w \<noteq> rev [0..<n] \<Longrightarrow> False
[PROOF STEP]
with wf_ss_w x
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
\<not> ss ! hd w \<noteq> rev [0..<n]
hd w < n
\<forall>x\<in>set w. hd w \<le> x
[PROOF STEP]
have  "(\<exists>x\<in> set w. (x,hd w)\<in> g_E G \<and> x < hd w)"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
\<not> ss ! hd w \<noteq> rev [0..<n]
hd w < n
\<forall>x\<in>set w. hd w \<le> x

goal (1 subgoal):
 1. \<exists>x\<in>set w. (x, hd w) \<in> g_E G \<and> x < hd w
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set w. (x, hd w) \<in> g_E G \<and> x < hd w

goal (1 subgoal):
 1. \<not> ss ! hd w \<noteq> rev [0..<n] \<Longrightarrow> False
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set w. hd w \<le> x
\<exists>x\<in>set w. (x, hd w) \<in> g_E G \<and> x < hd w
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set w. hd w \<le> x
\<exists>x\<in>set w. (x, hd w) \<in> g_E G \<and> x < hd w

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pres_wf_exec:
  fixes ss w a b
  assumes wf_ss_w: "wf_dom ss w "
      and w_n_nil: "w \<noteq> [] "
    shows "\<forall>(q,\<tau>) \<in> set (step (hd w) (ss!(hd w))). \<tau> \<in> A "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). \<tau> \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd w) (ss ! hd w)). \<tau> \<in> A
[PROOF STEP]
proof(intro strip, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> set (step (hd w) (ss ! hd w)); wf_dom ss w; w \<noteq> []\<rbrakk> \<Longrightarrow> b \<in> A
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> set (step (hd w) (ss ! hd w)); wf_dom ss w; w \<noteq> []\<rbrakk> \<Longrightarrow> b \<in> A
[PROOF STEP]
assume a_b: "(a, b) \<in> set (step (hd w) (ss ! hd w))"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> set (step (hd w) (ss ! hd w))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> set (step (hd w) (ss ! hd w)); wf_dom ss w; w \<noteq> []\<rbrakk> \<Longrightarrow> b \<in> A
[PROOF STEP]
from wf_ss_w
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
[PROOF STEP]
have sorted_w: "sorted w" and hd_w_lt_n: "hd w < n"
    and ss_hdw_inA: "ss!hd w \<in> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w

goal (1 subgoal):
 1. Sorted_Less.sorted w &&& hd w < n &&& ss ! hd w \<in> A
[PROOF STEP]
using w_n_nil
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []

goal (1 subgoal):
 1. Sorted_Less.sorted w &&& hd w < n &&& ss ! hd w \<in> A
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted w
hd w < n
ss ! hd w \<in> A

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> set (step (hd w) (ss ! hd w)); wf_dom ss w; w \<noteq> []\<rbrakk> \<Longrightarrow> b \<in> A
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
w \<noteq> []
[PROOF STEP]
have ss_hd_w_neq_all: "ss!hd w \<noteq> (rev [0..<n])"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
w \<noteq> []

goal (1 subgoal):
 1. ss ! hd w \<noteq> rev [0..<n]
[PROOF STEP]
by (rule wf_hd_neq_all)
[PROOF STATE]
proof (state)
this:
ss ! hd w \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> set (step (hd w) (ss ! hd w)); wf_dom ss w; w \<noteq> []\<rbrakk> \<Longrightarrow> b \<in> A
[PROOF STEP]
with wf_ss_w hd_w_lt_n
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
hd w < n
ss ! hd w \<noteq> rev [0..<n]
[PROOF STEP]
have "\<forall>x\<in>set (ss!hd w). hd w > x"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
hd w < n
ss ! hd w \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<forall>x\<in>set (ss ! hd w). x < hd w
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (ss ! hd w). x < hd w

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> set (step (hd w) (ss ! hd w)); wf_dom ss w; w \<noteq> []\<rbrakk> \<Longrightarrow> b \<in> A
[PROOF STEP]
with ss_hdw_inA hd_w_lt_n a_b
[PROOF STATE]
proof (chain)
picking this:
ss ! hd w \<in> A
hd w < n
(a, b) \<in> set (step (hd w) (ss ! hd w))
\<forall>x\<in>set (ss ! hd w). x < hd w
[PROOF STEP]
show "b \<in> A"
[PROOF STATE]
proof (prove)
using this:
ss ! hd w \<in> A
hd w < n
(a, b) \<in> set (step (hd w) (ss ! hd w))
\<forall>x\<in>set (ss ! hd w). x < hd w

goal (1 subgoal):
 1. b \<in> A
[PROOF STEP]
using pres_exec
[PROOF STATE]
proof (prove)
using this:
ss ! hd w \<in> A
hd w < n
(a, b) \<in> set (step (hd w) (ss ! hd w))
\<forall>x\<in>set (ss ! hd w). x < hd w
\<lbrakk>(?q, ?\<tau>) \<in> set (step ?p (?ss ! ?p)); \<forall>n\<in>set (?ss ! ?p). n < ?p; ?ss ! ?p \<in> A; ?p < n\<rbrakk> \<Longrightarrow> ?\<tau> \<in> A

goal (1 subgoal):
 1. b \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma propa_dom_invariant_auxi:
  assumes wf_a_b: "wf_dom a b" and b_n_nil: "b \<noteq> [] "
    shows "a!hd b \<noteq> rev [0..<n] \<and>
           sorted (rev (hd b # (a!hd b))) \<and>
           set (hd b # (a!hd b)) \<subseteq> set nodes \<and>
           hd b # (a!hd b) \<in> A \<and>
           (\<forall>(q, \<tau>)\<in>set (step (hd b) (a!hd b)). q < length a \<and> \<tau> \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []

goal (1 subgoal):
 1. a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
b \<noteq> []
[PROOF STEP]
have "a!hd b \<in> (rev \<circ> sorted_list_of_set) ` (Pow (set nodes))"
              and  sorted_hdb: "sorted (rev (a!hd b))"
              and hd_b_lt_n: "hd b < n"
              and sorted_b: "sorted b"
              and len_eq: "length a = n"
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []

goal (1 subgoal):
 1. (a ! hd b \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes) &&& Sorted_Less.sorted (rev (a ! hd b))) &&& hd b < n &&& Sorted_Less.sorted b &&& length a = n
[PROOF STEP]
by (auto simp add:A_def wf_dom_def)
[PROOF STATE]
proof (state)
this:
a ! hd b \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
Sorted_Less.sorted (rev (a ! hd b))
hd b < n
Sorted_Less.sorted b
length a = n

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a ! hd b \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
Sorted_Less.sorted (rev (a ! hd b))
hd b < n
Sorted_Less.sorted b
length a = n
[PROOF STEP]
have as_subset_nodes: "set (a!hd b) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
a ! hd b \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
Sorted_Less.sorted (rev (a ! hd b))
hd b < n
Sorted_Less.sorted b
length a = n

goal (1 subgoal):
 1. set (a ! hd b) \<subseteq> set nodes
[PROOF STEP]
by (auto simp add:inpow_subset_nodes)
[PROOF STATE]
proof (state)
this:
set (a ! hd b) \<subseteq> set nodes

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
with n_def verts_set assms nodes_def
[PROOF STATE]
proof (chain)
picking this:
n \<equiv> length nodes
set (g_V G) = {0..<length (g_V G)}
wf_dom a b
b \<noteq> []
nodes \<equiv> g_V G
set (a ! hd b) \<subseteq> set nodes
[PROOF STEP]
have hdb_cons_subset_nodes: "set (hd b # (a!hd b)) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
n \<equiv> length nodes
set (g_V G) = {0..<length (g_V G)}
wf_dom a b
b \<noteq> []
nodes \<equiv> g_V G
set (a ! hd b) \<subseteq> set nodes

goal (1 subgoal):
 1. set (hd b # a ! hd b) \<subseteq> set nodes
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
set (hd b # a ! hd b) \<subseteq> set nodes

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (hd b # a ! hd b) \<subseteq> set nodes
[PROOF STEP]
have hdb_subset_n: "set (hd b # (a!hd b)) \<subseteq> {0..<n}"
[PROOF STATE]
proof (prove)
using this:
set (hd b # a ! hd b) \<subseteq> set nodes

goal (1 subgoal):
 1. set (hd b # a ! hd b) \<subseteq> {0..<n}
[PROOF STEP]
using nodes_def verts_set n_def
[PROOF STATE]
proof (prove)
using this:
set (hd b # a ! hd b) \<subseteq> set nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}
n \<equiv> length nodes

goal (1 subgoal):
 1. set (hd b # a ! hd b) \<subseteq> {0..<n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (hd b # a ! hd b) \<subseteq> {0..<n}

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
from wf_a_b b_n_nil
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
b \<noteq> []
[PROOF STEP]
have a_hd_b_neq_all: "a!hd b \<noteq> (rev [0..<n])"
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []

goal (1 subgoal):
 1. a ! hd b \<noteq> rev [0..<n]
[PROOF STEP]
using wf_hd_neq_all
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []
\<lbrakk>wf_dom ?ss ?w; ?w \<noteq> []\<rbrakk> \<Longrightarrow> ?ss ! hd ?w \<noteq> rev [0..<n]

goal (1 subgoal):
 1. a ! hd b \<noteq> rev [0..<n]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a ! hd b \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
with wf_a_b hd_b_lt_n sorted_hdb
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
hd b < n
Sorted_Less.sorted (rev (a ! hd b))
a ! hd b \<noteq> rev [0..<n]
[PROOF STEP]
have sorted_hd_b_cons: "sorted (rev (hd b # (a!hd b)))"
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
hd b < n
Sorted_Less.sorted (rev (a ! hd b))
a ! hd b \<noteq> rev [0..<n]

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (hd b # a ! hd b))
[PROOF STEP]
by (fastforce simp add: wf_dom_def dest: Cons_sorted_less)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (hd b # a ! hd b))

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
from hdb_cons_subset_nodes
[PROOF STATE]
proof (chain)
picking this:
set (hd b # a ! hd b) \<subseteq> set nodes
[PROOF STEP]
have  "set ((hd b # (a!hd b))) \<in> Pow (set (g_V G))"
[PROOF STATE]
proof (prove)
using this:
set (hd b # a ! hd b) \<subseteq> set nodes

goal (1 subgoal):
 1. set (hd b # a ! hd b) \<in> Pow (set (g_V G))
[PROOF STEP]
by (auto simp add:nodes_def)
[PROOF STATE]
proof (state)
this:
set (hd b # a ! hd b) \<in> Pow (set (g_V G))

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (hd b # a ! hd b) \<in> Pow (set (g_V G))
[PROOF STEP]
have pow1: "set ((hd b # (a!hd b))) \<subseteq> set nodes"
[PROOF STATE]
proof (prove)
using this:
set (hd b # a ! hd b) \<in> Pow (set (g_V G))

goal (1 subgoal):
 1. set (hd b # a ! hd b) \<subseteq> set nodes
[PROOF STEP]
by (auto simp add:nodes_def)
[PROOF STATE]
proof (state)
this:
set (hd b # a ! hd b) \<subseteq> set nodes

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
from hdb_cons_subset_nodes sorted_hd_b_cons
[PROOF STATE]
proof (chain)
picking this:
set (hd b # a ! hd b) \<subseteq> set nodes
Sorted_Less.sorted (rev (hd b # a ! hd b))
[PROOF STEP]
have "hd b # (a!hd b) \<in> (rev \<circ> sorted_list_of_set) ` (Pow (set nodes))"
[PROOF STATE]
proof (prove)
using this:
set (hd b # a ! hd b) \<subseteq> set nodes
Sorted_Less.sorted (rev (hd b # a ! hd b))

goal (1 subgoal):
 1. hd b # a ! hd b \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
by (fastforce intro: subset_nodes_inpow)
[PROOF STATE]
proof (state)
this:
hd b # a ! hd b \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd b # a ! hd b \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)
[PROOF STEP]
have hd_b_cons_in_A: "(hd b # (a!hd b)) \<in> A"
[PROOF STATE]
proof (prove)
using this:
hd b # a ! hd b \<in> (rev \<circ> sorted_list_of_set) ` Pow (set nodes)

goal (1 subgoal):
 1. hd b # a ! hd b \<in> A
[PROOF STEP]
by (unfold A_def ) (auto simp add:nodes_def)
[PROOF STATE]
proof (state)
this:
hd b # a ! hd b \<in> A

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
have "(\<forall>p<n. \<forall>\<tau>. \<forall>(q,\<tau>') \<in> set (step p \<tau>). q<n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p<n. \<forall>\<tau>. \<forall>(q, \<tau>')\<in>set (step p \<tau>). q < n
[PROOF STEP]
using bounded_exec
[PROOF STATE]
proof (prove)
using this:
bounded step n

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

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
with hd_b_lt_n
[PROOF STATE]
proof (chain)
picking this:
hd b < n
\<forall>p<n. \<forall>\<tau>. \<forall>(q, \<tau>')\<in>set (step p \<tau>). q < n
[PROOF STEP]
have bounded: "\<forall>(q,\<tau>') \<in> set (step (hd b) (a!hd b)). q<n"
[PROOF STATE]
proof (prove)
using this:
hd b < n
\<forall>p<n. \<forall>\<tau>. \<forall>(q, \<tau>')\<in>set (step p \<tau>). q < n

goal (1 subgoal):
 1. \<forall>(q, \<tau>')\<in>set (step (hd b) (a ! hd b)). q < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>')\<in>set (step (hd b) (a ! hd b)). q < n

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
from wf_a_b b_n_nil
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
b \<noteq> []
[PROOF STEP]
have pres: "\<forall>(q, \<tau>)\<in>set(step (hd b) (a!hd b)). \<tau> \<in> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). \<tau> \<in> A
[PROOF STEP]
by (rule pres_wf_exec)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). \<tau> \<in> A

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
with bounded pres
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>')\<in>set (step (hd b) (a ! hd b)). q < n
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). \<tau> \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). \<tau> \<in> A
[PROOF STEP]
have step_pres_bounded: "\<forall>(q, \<tau>)\<in>set (step (hd b) (a!hd b)). q < length a \<and> \<tau> \<in> A "
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>')\<in>set (step (hd b) (a ! hd b)). q < n
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). \<tau> \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). \<tau> \<in> A

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

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A

goal (1 subgoal):
 1. \<lbrakk>wf_dom a b; b \<noteq> []\<rbrakk> \<Longrightarrow> a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
with a_hd_b_neq_all sorted_hd_b_cons hdb_cons_subset_nodes hd_b_cons_in_A
[PROOF STATE]
proof (chain)
picking this:
a ! hd b \<noteq> rev [0..<n]
Sorted_Less.sorted (rev (hd b # a ! hd b))
set (hd b # a ! hd b) \<subseteq> set nodes
hd b # a ! hd b \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a ! hd b \<noteq> rev [0..<n]
Sorted_Less.sorted (rev (hd b # a ! hd b))
set (hd b # a ! hd b) \<subseteq> set nodes
hd b # a ! hd b \<in> A
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A

goal (1 subgoal):
 1. a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a ! hd b \<noteq> rev [0..<n] \<and> Sorted_Less.sorted (rev (hd b # a ! hd b)) \<and> set (hd b # a ! hd b) \<subseteq> set nodes \<and> hd b # a ! hd b \<in> A \<and> (\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A)

goal:
No subgoals!
[PROOF STEP]
qed