[STATEMENT]
lemma dom_iter_properties:
  "iter f step start (unstables r step start) = (ss, w) \<longrightarrow>
   ss!0 = [] \<and>
   (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss!p \<noteq> (rev [0..<n]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<longrightarrow> ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<Longrightarrow> ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
assume iter: "iter f step start (unstables r step start) = (ss, w)"
[PROOF STATE]
proof (state)
this:
iter f step start (unstables r step start) = (ss, w)

goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<Longrightarrow> ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
with iter_dom_properties iter_dom_properties2
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> ?ss' \<in> nlists n A
iter f step start (unstables r step start) = (ss, w)
[PROOF STEP]
have "wf_dom ss w"
   and stas: "stables r step ss"
   and start_le_ss: "start [\<sqsubseteq>\<^sub>r] ss"
   and ss_inA: "ss \<in> nlists n A"
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> ?ss' \<in> nlists n A
iter f step start (unstables r step start) = (ss, w)

goal (1 subgoal):
 1. (wf_dom ss w &&& stables r step ss) &&& start [\<sqsubseteq>\<^bsub>r\<^esub>] ss &&& ss \<in> nlists n A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_dom ss w
stables r step ss
start [\<sqsubseteq>\<^bsub>r\<^esub>] ss
ss \<in> nlists n A

goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<Longrightarrow> ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
stables r step ss
start [\<sqsubseteq>\<^bsub>r\<^esub>] ss
ss \<in> nlists n A
[PROOF STEP]
have len_ss_n: "length ss = n"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
stables r step ss
start [\<sqsubseteq>\<^bsub>r\<^esub>] ss
ss \<in> nlists n A

goal (1 subgoal):
 1. length ss = n
[PROOF STEP]
by (auto simp only:nlists_def)
[PROOF STATE]
proof (state)
this:
length ss = n

goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<Longrightarrow> ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
from start_le_ss
[PROOF STATE]
proof (chain)
picking this:
start [\<sqsubseteq>\<^bsub>r\<^esub>] ss
[PROOF STEP]
have "start!0 \<sqsubseteq>\<^sub>r ss!0"
[PROOF STATE]
proof (prove)
using this:
start [\<sqsubseteq>\<^bsub>r\<^esub>] ss

goal (1 subgoal):
 1. start ! 0 \<sqsubseteq>\<^bsub>r\<^esub> ss ! 0
[PROOF STEP]
using start_len_gt_0
[PROOF STATE]
proof (prove)
using this:
start [\<sqsubseteq>\<^bsub>r\<^esub>] ss
0 < length start

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

goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<Longrightarrow> ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
start ! 0 \<sqsubseteq>\<^bsub>r\<^esub> ss ! 0
[PROOF STEP]
have ss_0th: "ss!0 = []"
[PROOF STATE]
proof (prove)
using this:
start ! 0 \<sqsubseteq>\<^bsub>r\<^esub> ss ! 0

goal (1 subgoal):
 1. ss ! 0 = []
[PROOF STEP]
by (auto simp add:r_def nodes_le_def lesssub_def lesub_def start_def)
[PROOF STATE]
proof (state)
this:
ss ! 0 = []

goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<Longrightarrow> ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
have "(\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq>  (rev [0..<n]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
proof(intro strip, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume p_lt_n: "p < n" and p_neq_0: "p\<noteq>0" and ss_p_eq_all: "\<not> ss ! p \<noteq> rev [0..<n]"
[PROOF STATE]
proof (state)
this:
p < n
p \<noteq> 0
\<not> ss ! p \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with stas len_ss_n
[PROOF STATE]
proof (chain)
picking this:
stables r step ss
length ss = n
p < n
p \<noteq> 0
\<not> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
have step_sta: "\<forall>(q,\<tau>) \<in> set (step p (ss!p)). \<tau> \<sqsubseteq>\<^sub>r ss!q"
[PROOF STATE]
proof (prove)
using this:
stables r step ss
length ss = n
p < n
p \<noteq> 0
\<not> ss ! p \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (ss ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> ss ! q
[PROOF STEP]
by (simp add: stables_def stable_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step p (ss ! p)). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> ss ! q

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from p_lt_n len_start_is_n verts_set
[PROOF STATE]
proof (chain)
picking this:
p < n
length start = n
set (g_V G) = {0..<length (g_V G)}
[PROOF STEP]
have p_is_vert: "p \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
p < n
length start = n
set (g_V G) = {0..<length (g_V G)}

goal (1 subgoal):
 1. p \<in> set (g_V G)
[PROOF STEP]
by (auto simp add:n_def nodes_def)
[PROOF STATE]
proof (state)
this:
p \<in> set (g_V G)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (g_V G)
[PROOF STEP]
have step_p: "\<forall>(q,\<tau>) \<in> set (step p (ss!p)). q \<in> succs p"
[PROOF STATE]
proof (prove)
using this:
p \<in> set (g_V G)

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step p (ss ! p)). q \<in> succs p
[PROOF STEP]
using fin_succs
[PROOF STATE]
proof (prove)
using this:
p \<in> set (g_V G)
\<forall>v\<in>set (g_V G). finite (succs v)

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

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from p_is_vert p_neq_0 dfst
[PROOF STATE]
proof (chain)
picking this:
p \<in> set (g_V G)
p \<noteq> 0
\<forall>v\<in>set (g_V G) - {0}. \<exists>prev. (prev, v) \<in> g_E G \<and> prev < v
[PROOF STEP]
obtain prev where "(prev, p) \<in> g_E G" and prev_lt_p: "prev < p"
[PROOF STATE]
proof (prove)
using this:
p \<in> set (g_V G)
p \<noteq> 0
\<forall>v\<in>set (g_V G) - {0}. \<exists>prev. (prev, v) \<in> g_E G \<and> prev < v

goal (1 subgoal):
 1. (\<And>prev. \<lbrakk>(prev, p) \<in> g_E G; prev < p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(prev, p) \<in> g_E G
prev < p

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(prev, p) \<in> g_E G
prev < p
[PROOF STEP]
have prev_lt_n: "prev < n"
         and prev_p: "p \<in> succs prev"
         and "prev \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
(prev, p) \<in> g_E G
prev < p

goal (1 subgoal):
 1. prev < n &&& p \<in> succs prev &&& prev \<in> set (g_V G)
[PROOF STEP]
using p_lt_n tail_is_vert
[PROOF STATE]
proof (prove)
using this:
(prev, p) \<in> g_E G
prev < p
p < n
(?u, ?v) \<in> g_E G \<Longrightarrow> ?u \<in> set (g_V G)

goal (1 subgoal):
 1. prev < n &&& p \<in> succs prev &&& prev \<in> set (g_V G)
[PROOF STEP]
by (auto simp add:succs_def)
[PROOF STATE]
proof (state)
this:
prev < n
p \<in> succs prev
prev \<in> set (g_V G)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prev < n
p \<in> succs prev
prev \<in> set (g_V G)
[PROOF STEP]
have fin_suc_prev : "finite (succs prev)"
[PROOF STATE]
proof (prove)
using this:
prev < n
p \<in> succs prev
prev \<in> set (g_V G)

goal (1 subgoal):
 1. finite (succs prev)
[PROOF STEP]
using fin_succs
[PROOF STATE]
proof (prove)
using this:
prev < n
p \<in> succs prev
prev \<in> set (g_V G)
\<forall>v\<in>set (g_V G). finite (succs v)

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

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?prev_\<tau> = "ss!prev"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from prev_lt_n stas \<open>length ss = n\<close>
[PROOF STATE]
proof (chain)
picking this:
prev < n
stables r step ss
length ss = n
[PROOF STEP]
have "stable r step ss prev"
[PROOF STATE]
proof (prove)
using this:
prev < n
stables r step ss
length ss = n

goal (1 subgoal):
 1. Typing_Framework_1.stable r step ss prev
[PROOF STEP]
by (auto simp add:stables_def)
[PROOF STATE]
proof (state)
this:
Typing_Framework_1.stable r step ss prev

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Typing_Framework_1.stable r step ss prev
[PROOF STEP]
have "\<forall>(q,\<tau>) \<in> set (step prev ?prev_\<tau>). (prev # ?prev_\<tau>) \<sqsubseteq>\<^sub>r ss!q"
[PROOF STATE]
proof (prove)
using this:
Typing_Framework_1.stable r step ss prev

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step prev (ss ! prev)). prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! q
[PROOF STEP]
by (auto simp add: stable_def transf_def step_def exec_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step prev (ss ! prev)). prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! q

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with prev_p
[PROOF STATE]
proof (chain)
picking this:
p \<in> succs prev
\<forall>(q, \<tau>)\<in>set (step prev (ss ! prev)). prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! q
[PROOF STEP]
have "(prev # ?prev_\<tau>) \<sqsubseteq>\<^bsub>r\<^esub> ss ! p"
[PROOF STATE]
proof (prove)
using this:
p \<in> succs prev
\<forall>(q, \<tau>)\<in>set (step prev (ss ! prev)). prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! q

goal (1 subgoal):
 1. prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! p
[PROOF STEP]
using fin_suc_prev
[PROOF STATE]
proof (prove)
using this:
p \<in> succs prev
\<forall>(q, \<tau>)\<in>set (step prev (ss ! prev)). prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! q
finite (succs prev)

goal (1 subgoal):
 1. prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! p
[PROOF STEP]
by (auto simp add: stable_def transf_def step_def exec_def)
[PROOF STATE]
proof (state)
this:
prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! p

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with ss_p_eq_all
[PROOF STATE]
proof (chain)
picking this:
\<not> ss ! p \<noteq> rev [0..<n]
prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! p
[PROOF STEP]
have "sorted (rev (prev # ?prev_\<tau>)) \<and> {0..<n} \<subseteq> set (prev # ?prev_\<tau>) \<or> (prev # ss ! prev) =  (rev [0..<n])"
[PROOF STATE]
proof (prove)
using this:
\<not> ss ! p \<noteq> rev [0..<n]
prev # ss ! prev \<sqsubseteq>\<^bsub>r\<^esub> ss ! p

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (prev # ss ! prev)) \<and> {0..<n} \<subseteq> set (prev # ss ! prev) \<or> prev # ss ! prev = rev [0..<n]
[PROOF STEP]
by (auto simp add:r_def lesssub_def lesub_def nodes_le_def)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (prev # ss ! prev)) \<and> {0..<n} \<subseteq> set (prev # ss ! prev) \<or> prev # ss ! prev = rev [0..<n]

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (prev # ss ! prev)) \<and> {0..<n} \<subseteq> set (prev # ss ! prev) \<or> prev # ss ! prev = rev [0..<n]
[PROOF STEP]
have "sorted (rev (prev # ?prev_\<tau>)) \<and> {0..<n} \<subseteq> set (prev # ?prev_\<tau>)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (prev # ss ! prev)) \<and> {0..<n} \<subseteq> set (prev # ss ! prev) \<or> prev # ss ! prev = rev [0..<n]

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (prev # ss ! prev)) \<and> {0..<n} \<subseteq> set (prev # ss ! prev)
[PROOF STEP]
by(rule disjE)  auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (prev # ss ! prev)) \<and> {0..<n} \<subseteq> set (prev # ss ! prev)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (prev # ss ! prev)) \<and> {0..<n} \<subseteq> set (prev # ss ! prev)
[PROOF STEP]
have sorted_rev: "sorted (rev (prev # ?prev_\<tau>))"
          and pres_subset: "{0..<n} \<subseteq> set (prev # ?prev_\<tau>)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (prev # ss ! prev)) \<and> {0..<n} \<subseteq> set (prev # ss ! prev)

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (prev # ss ! prev)) &&& {0..<n} \<subseteq> set (prev # ss ! prev)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (rev (prev # ss ! prev))
{0..<n} \<subseteq> set (prev # ss ! prev)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (prev # ss ! prev))
{0..<n} \<subseteq> set (prev # ss ! prev)
[PROOF STEP]
have prev_set: "\<forall>x\<in> set ?prev_\<tau>. x < prev"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (prev # ss ! prev))
{0..<n} \<subseteq> set (prev # ss ! prev)

goal (1 subgoal):
 1. \<forall>x\<in>set (ss ! prev). x < prev
[PROOF STEP]
by (induct ?prev_\<tau>) (auto simp add:sorted_wrt_append)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (ss ! prev). x < prev

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from p_lt_n prev_lt_p
[PROOF STATE]
proof (chain)
picking this:
p < n
prev < p
[PROOF STEP]
have "prev < n - 1"
[PROOF STATE]
proof (prove)
using this:
p < n
prev < p

goal (1 subgoal):
 1. prev < n - 1
[PROOF STEP]
using n_def nodes_def len_verts_gt0
[PROOF STATE]
proof (prove)
using this:
p < n
prev < p
n \<equiv> length nodes
nodes \<equiv> g_V G
0 < length (g_V G)

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

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with prev_set
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set (ss ! prev). x < prev
prev < n - 1
[PROOF STEP]
have prev_lt_n: "\<forall>x\<in>set(prev # ?prev_\<tau>). x < n - 1"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (ss ! prev). x < prev
prev < n - 1

goal (1 subgoal):
 1. \<forall>x\<in>set (prev # ss ! prev). x < n - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (prev # ss ! prev). x < n - 1

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from pres_subset
[PROOF STATE]
proof (chain)
picking this:
{0..<n} \<subseteq> set (prev # ss ! prev)
[PROOF STEP]
have "n - 1 \<in> set (prev # ?prev_\<tau>)"
[PROOF STATE]
proof (prove)
using this:
{0..<n} \<subseteq> set (prev # ss ! prev)

goal (1 subgoal):
 1. n - 1 \<in> set (prev # ss ! prev)
[PROOF STEP]
using n_def nodes_def len_verts_gt0
[PROOF STATE]
proof (prove)
using this:
{0..<n} \<subseteq> set (prev # ss ! prev)
n \<equiv> length nodes
nodes \<equiv> g_V G
0 < length (g_V G)

goal (1 subgoal):
 1. n - 1 \<in> set (prev # ss ! prev)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n - 1 \<in> set (prev # ss ! prev)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p < n; p \<noteq> 0; \<not> ss ! p \<noteq> rev [0..<n]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with prev_lt_n
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set (prev # ss ! prev). x < n - 1
n - 1 \<in> set (prev # ss ! prev)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (prev # ss ! prev). x < n - 1
n - 1 \<in> set (prev # ss ! prev)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n]

goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<Longrightarrow> ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
with ss_0th
[PROOF STATE]
proof (chain)
picking this:
ss ! 0 = []
\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
show " ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])"
[PROOF STATE]
proof (prove)
using this:
ss ! 0 = []
\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n]

goal (1 subgoal):
 1. ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ss ! 0 = [] \<and> (\<forall>p<n. p \<noteq> 0 \<longrightarrow> ss ! p \<noteq> rev [0..<n])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dom_iter_properties2:
  "iter f step start (unstables r step start) = (ss,w) \<longrightarrow> (\<forall>p<n.  ss!p \<noteq> (rev [0..<n]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter f step start (unstables r step start) = (ss, w) \<longrightarrow> (\<forall>p<n. ss ! p \<noteq> rev [0..<n])
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>iter f step start (unstables r step start) = (ss, w); p < n\<rbrakk> \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>iter f step start (unstables r step start) = (ss, w); p < n\<rbrakk> \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
assume iter: "iter f step start (unstables r step start) = (ss, w)" and p: "p < n"
[PROOF STATE]
proof (state)
this:
iter f step start (unstables r step start) = (ss, w)
p < n

goal (1 subgoal):
 1. \<And>p. \<lbrakk>iter f step start (unstables r step start) = (ss, w); p < n\<rbrakk> \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
show "ss ! p \<noteq> (rev [0..<n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
proof(cases "p = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
 2. p \<noteq> 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p = 0

goal (2 subgoals):
 1. p = 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
 2. p \<noteq> 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
with iter
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (ss, w)
p = 0
[PROOF STEP]
have "ss!p = []"
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (ss, w)
p = 0

goal (1 subgoal):
 1. ss ! p = []
[PROOF STEP]
by  (auto simp add:dom_iter_properties)
[PROOF STATE]
proof (state)
this:
ss ! p = []

goal (2 subgoals):
 1. p = 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
 2. p \<noteq> 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss ! p = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ss ! p = []

goal (1 subgoal):
 1. ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
using n_def nodes_def len_verts_gt0
[PROOF STATE]
proof (prove)
using this:
ss ! p = []
n \<equiv> length nodes
nodes \<equiv> g_V G
0 < length (g_V G)

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

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
with iter p
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (ss, w)
p < n
p \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (ss, w)
p < n
p \<noteq> 0

goal (1 subgoal):
 1. ss ! p \<noteq> rev [0..<n]
[PROOF STEP]
by (auto simp add:dom_iter_properties)
[PROOF STATE]
proof (state)
this:
ss ! p \<noteq> rev [0..<n]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ss ! p \<noteq> rev [0..<n]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kildall_dom_properties:
  "kildall r f step start \<in> nlists n A \<and>
   stables r step (kildall r f step start) \<and>
   start [\<sqsubseteq>\<^sub>r] (kildall r f step start) \<and>
   (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow> (kildall r f step start) [\<sqsubseteq>\<^sub>r] ts)"  (is "PROP ?P")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kildall r f step start \<in> nlists n A \<and> stables r step (kildall r f step start) \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] kildall r f step start \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> kildall r f step start [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
[PROOF STEP]
by (case_tac "iter f step start (unstables r step start)")(simp add: kildall_def iter_dom_properties iter_dom_properties2)


[STATEMENT]
lemma dom_kildall_stables: "stables r step (dom_kildall start)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stables r step (dom_kildall start)
[PROOF STEP]
using kildall_dom_properties
[PROOF STATE]
proof (prove)
using this:
kildall r f step start \<in> nlists n A \<and> stables r step (kildall r f step start) \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] kildall r f step start \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> kildall r f step start [\<sqsubseteq>\<^bsub>r\<^esub>] ts)

goal (1 subgoal):
 1. stables r step (dom_kildall start)
[PROOF STEP]
by(unfold dom_kildall_def nodes_semi_def) (simp add: r_def f_def step_def)


[STATEMENT]
lemma dom_kildall_entry: "dom_kildall start !0 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom_kildall start ! 0 = []
[PROOF STEP]
by (case_tac "iter f step start (unstables r step start)")
     (auto simp add:dom_kildall_def nodes_semi_def dom_iter_properties r_def f_def step_def kildall_def)


[STATEMENT]
lemma zero_dom_zero: "dom i 0 \<longleftrightarrow> i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom i 0 = (i = 0)
[PROOF STEP]
using start_def n_def nodes_def dom_kildall_entry
[PROOF STATE]
proof (prove)
using this:
start \<equiv> [] # replicate (length (g_V G) - 1) (rev [0..<n])
n \<equiv> length nodes
nodes \<equiv> g_V G
dom_kildall start ! 0 = []

goal (1 subgoal):
 1. local.dom i 0 = (i = 0)
[PROOF STEP]
by (simp add:dom_def)


[STATEMENT]
lemma sdom_dom_succs: "strict_dom i j \<Longrightarrow> j \<in> succs k \<Longrightarrow> dom i k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
assume sdom_i_j: "strict_dom i j" and k_j: "j \<in> succs k"
[PROOF STATE]
proof (state)
this:
strict_dom i j
j \<in> succs k

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
strict_dom i j
j \<in> succs k
[PROOF STEP]
have j: "j \<in> set (g_V G)"
        and k: "k \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
strict_dom i j
j \<in> succs k

goal (1 subgoal):
 1. j \<in> set (g_V G) &&& k \<in> set (g_V G)
[PROOF STEP]
using verts_set succ_in_verts
[PROOF STATE]
proof (prove)
using this:
strict_dom i j
j \<in> succs k
set (g_V G) = {0..<length (g_V G)}
?s \<in> succs ?n \<Longrightarrow> {?s, ?n} \<subseteq> set (g_V G)

goal (1 subgoal):
 1. j \<in> set (g_V G) &&& k \<in> set (g_V G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<in> set (g_V G)
k \<in> set (g_V G)

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<in> set (g_V G)
k \<in> set (g_V G)
[PROOF STEP]
have j_lt_n: "j < n" and k_lt_n: "k < n"
[PROOF STATE]
proof (prove)
using this:
j \<in> set (g_V G)
k \<in> set (g_V G)

goal (1 subgoal):
 1. j < n &&& k < n
[PROOF STEP]
using n_def nodes_def verts_set
[PROOF STATE]
proof (prove)
using this:
j \<in> set (g_V G)
k \<in> set (g_V G)
n \<equiv> length nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}

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

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
have fin_succs_k: "finite (succs k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (succs k)
[PROOF STEP]
using fin_succs k
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>set (g_V G). finite (succs v)
k \<in> set (g_V G)

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

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
with k_j
[PROOF STATE]
proof (chain)
picking this:
j \<in> succs k
finite (succs k)
[PROOF STEP]
have k_j2: "j \<in> set (rev (sorted_list_of_set(succs k)))"
[PROOF STATE]
proof (prove)
using this:
j \<in> succs k
finite (succs k)

goal (1 subgoal):
 1. j \<in> set (rev (sorted_list_of_set (succs k)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<in> set (rev (sorted_list_of_set (succs k)))

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
let ?ss0 = "start"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
let ?w0 = "unstables r step start"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
let ?res = "dom_kildall start"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
have dom_kil: "?res = kildall r f step ?ss0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom_kildall start = kildall r f step start
[PROOF STEP]
by (auto simp add:dom_kildall_def r_def f_def step_def nodes_semi_def)
[PROOF STATE]
proof (state)
this:
dom_kildall start = kildall r f step start

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
have sorted_unstables: "sorted ?w0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sorted_Less.sorted (unstables r step start)
[PROOF STEP]
by (auto simp add:unstables_def sorted_less_sorted_list_of_set)
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (unstables r step start)

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
have ss: "?res = fst (iter f step ?ss0 ?w0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom_kildall start = fst (iter f step start (unstables r step start))
[PROOF STEP]
by (auto simp add:dom_kildall_def kildall_def f_def step_def nodes_semi_def start_def r_def)
[PROOF STATE]
proof (state)
this:
dom_kildall start = fst (iter f step start (unstables r step start))

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dom_kildall start = fst (iter f step start (unstables r step start))
[PROOF STEP]
obtain ww where dom_iter: "iter f step ?ss0 ?w0 = (?res, ww)"
[PROOF STATE]
proof (prove)
using this:
dom_kildall start = fst (iter f step start (unstables r step start))

goal (1 subgoal):
 1. (\<And>ww. iter f step start (unstables r step start) = (dom_kildall start, ww) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "iter f step ?ss0 ?w0") auto
[PROOF STATE]
proof (state)
this:
iter f step start (unstables r step start) = (dom_kildall start, ww)

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
with iter_dom_properties
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
iter f step start (unstables r step start) = (dom_kildall start, ww)
[PROOF STEP]
have wf_res: "wf_dom (dom_kildall start) ww"
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
iter f step start (unstables r step start) = (dom_kildall start, ww)

goal (1 subgoal):
 1. wf_dom (dom_kildall start) ww
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_dom (dom_kildall start) ww

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
with sdom_i_j
[PROOF STATE]
proof (chain)
picking this:
strict_dom i j
wf_dom (dom_kildall start) ww
[PROOF STEP]
have i_dom_j: "i \<in> set (?res!j)"
[PROOF STATE]
proof (prove)
using this:
strict_dom i j
wf_dom (dom_kildall start) ww

goal (1 subgoal):
 1. i \<in> set (dom_kildall start ! j)
[PROOF STEP]
by (auto simp add:strict_dom_def start_def n_def nodes_def)
[PROOF STATE]
proof (state)
this:
i \<in> set (dom_kildall start ! j)

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
from wf_res
[PROOF STATE]
proof (chain)
picking this:
wf_dom (dom_kildall start) ww
[PROOF STEP]
have len_res: "length ?res = n"
[PROOF STATE]
proof (prove)
using this:
wf_dom (dom_kildall start) ww

goal (1 subgoal):
 1. length (dom_kildall start) = n
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
length (dom_kildall start) = n

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
show "dom i k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom i k
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> local.dom i k \<Longrightarrow> False
[PROOF STEP]
assume ass: "\<not> dom i k"
[PROOF STATE]
proof (state)
this:
\<not> local.dom i k

goal (1 subgoal):
 1. \<not> local.dom i k \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> local.dom i k
[PROOF STEP]
have i_neq_k: "i \<noteq> k"
[PROOF STATE]
proof (prove)
using this:
\<not> local.dom i k

goal (1 subgoal):
 1. i \<noteq> k
[PROOF STEP]
by (auto simp add:dom_refl)
[PROOF STATE]
proof (state)
this:
i \<noteq> k

goal (1 subgoal):
 1. \<not> local.dom i k \<Longrightarrow> False
[PROOF STEP]
with ass
[PROOF STATE]
proof (chain)
picking this:
\<not> local.dom i k
i \<noteq> k
[PROOF STEP]
have "(\<exists>res. ?res!k = res \<and> i \<notin> set res)"
[PROOF STATE]
proof (prove)
using this:
\<not> local.dom i k
i \<noteq> k

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res
[PROOF STEP]
using ass
[PROOF STATE]
proof (prove)
using this:
\<not> local.dom i k
i \<noteq> k
\<not> local.dom i k

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res
[PROOF STEP]
by (auto simp add:dom_def start_def nodes_def n_def)
[PROOF STATE]
proof (state)
this:
\<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res

goal (1 subgoal):
 1. \<not> local.dom i k \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res

goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
assume "\<exists>res. ?res ! k =  res \<and> i \<notin> set res"
[PROOF STATE]
proof (state)
this:
\<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res
[PROOF STEP]
obtain rs where k_dom: "?res ! k = rs" and i_notin_rs: "i \<notin> set rs"
[PROOF STATE]
proof (prove)
using this:
\<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res

goal (1 subgoal):
 1. (\<And>rs. \<lbrakk>dom_kildall start ! k = rs; i \<notin> set rs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom_kildall start ! k = rs
i \<notin> set rs

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
from iter_dom_properties dom_iter
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
iter f step start (unstables r step start) = (dom_kildall start, ww)
[PROOF STEP]
have "(\<forall>p < length ?res. stable r step ?res p)"
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
iter f step start (unstables r step start) = (dom_kildall start, ww)

goal (1 subgoal):
 1. \<forall>p<length (dom_kildall start). Typing_Framework_1.stable r step (dom_kildall start) p
[PROOF STEP]
by (auto simp add:stables_def)
[PROOF STATE]
proof (state)
this:
\<forall>p<length (dom_kildall start). Typing_Framework_1.stable r step (dom_kildall start) p

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
with k_lt_n
[PROOF STATE]
proof (chain)
picking this:
k < n
\<forall>p<length (dom_kildall start). Typing_Framework_1.stable r step (dom_kildall start) p
[PROOF STEP]
have "stable r step ?res k"
[PROOF STATE]
proof (prove)
using this:
k < n
\<forall>p<length (dom_kildall start). Typing_Framework_1.stable r step (dom_kildall start) p

goal (1 subgoal):
 1. Typing_Framework_1.stable r step (dom_kildall start) k
[PROOF STEP]
using len_res
[PROOF STATE]
proof (prove)
using this:
k < n
\<forall>p<length (dom_kildall start). Typing_Framework_1.stable r step (dom_kildall start) p
length (dom_kildall start) = n

goal (1 subgoal):
 1. Typing_Framework_1.stable r step (dom_kildall start) k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Typing_Framework_1.stable r step (dom_kildall start) k

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
with k_dom
[PROOF STATE]
proof (chain)
picking this:
dom_kildall start ! k = rs
Typing_Framework_1.stable r step (dom_kildall start) k
[PROOF STEP]
have aux: "\<forall>(q,\<tau>) \<in> set (map (\<lambda>pc. (pc, (k # rs))) (rev (sorted_list_of_set(succs k)))). \<tau> \<sqsubseteq>\<^sub>r ?res!q"
[PROOF STATE]
proof (prove)
using this:
dom_kildall start ! k = rs
Typing_Framework_1.stable r step (dom_kildall start) k

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (map (\<lambda>pc. (pc, k # rs)) (rev (sorted_list_of_set (succs k)))). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> dom_kildall start ! q
[PROOF STEP]
by (simp add:stable_def r_def step_def exec_def transf_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (map (\<lambda>pc. (pc, k # rs)) (rev (sorted_list_of_set (succs k)))). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> dom_kildall start ! q

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
with k_j2
[PROOF STATE]
proof (chain)
picking this:
j \<in> set (rev (sorted_list_of_set (succs k)))
\<forall>(q, \<tau>)\<in>set (map (\<lambda>pc. (pc, k # rs)) (rev (sorted_list_of_set (succs k)))). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> dom_kildall start ! q
[PROOF STEP]
have "(k # rs) \<sqsubseteq>\<^sub>r ?res!j"
[PROOF STATE]
proof (prove)
using this:
j \<in> set (rev (sorted_list_of_set (succs k)))
\<forall>(q, \<tau>)\<in>set (map (\<lambda>pc. (pc, k # rs)) (rev (sorted_list_of_set (succs k)))). \<tau> \<sqsubseteq>\<^bsub>r\<^esub> dom_kildall start ! q

goal (1 subgoal):
 1. k # rs \<sqsubseteq>\<^bsub>r\<^esub> dom_kildall start ! j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k # rs \<sqsubseteq>\<^bsub>r\<^esub> dom_kildall start ! j

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k # rs \<sqsubseteq>\<^bsub>r\<^esub> dom_kildall start ! j
[PROOF STEP]
have "set (?res!j) \<subseteq> set (k # rs) \<or> ?res!j = k#rs"
[PROOF STATE]
proof (prove)
using this:
k # rs \<sqsubseteq>\<^bsub>r\<^esub> dom_kildall start ! j

goal (1 subgoal):
 1. set (dom_kildall start ! j) \<subseteq> set (k # rs) \<or> dom_kildall start ! j = k # rs
[PROOF STEP]
by (auto simp add:lesssub_def lesub_def nodes_semi_def nodes_le_def r_def f_def)
[PROOF STATE]
proof (state)
this:
set (dom_kildall start ! j) \<subseteq> set (k # rs) \<or> dom_kildall start ! j = k # rs

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (dom_kildall start ! j) \<subseteq> set (k # rs) \<or> dom_kildall start ! j = k # rs
[PROOF STEP]
have "set (?res!j) \<subseteq> set (k # rs)"
[PROOF STATE]
proof (prove)
using this:
set (dom_kildall start ! j) \<subseteq> set (k # rs) \<or> dom_kildall start ! j = k # rs

goal (1 subgoal):
 1. set (dom_kildall start ! j) \<subseteq> set (k # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (dom_kildall start ! j) \<subseteq> set (k # rs)

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
with i_dom_j i_neq_k
[PROOF STATE]
proof (chain)
picking this:
i \<in> set (dom_kildall start ! j)
i \<noteq> k
set (dom_kildall start ! j) \<subseteq> set (k # rs)
[PROOF STEP]
have " i \<in> set rs"
[PROOF STATE]
proof (prove)
using this:
i \<in> set (dom_kildall start ! j)
i \<noteq> k
set (dom_kildall start ! j) \<subseteq> set (k # rs)

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

goal (1 subgoal):
 1. \<exists>res. dom_kildall start ! k = res \<and> i \<notin> set res \<Longrightarrow> False
[PROOF STEP]
with i_notin_rs
[PROOF STATE]
proof (chain)
picking this:
i \<notin> set rs
i \<in> set rs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
i \<notin> set rs
i \<in> set rs

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.dom i k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adom_succs: "dom i j \<Longrightarrow> i \<noteq> j \<Longrightarrow> j \<in> succs k \<Longrightarrow> dom i k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.dom i j; i \<noteq> j; j \<in> succs k\<rbrakk> \<Longrightarrow> local.dom i k
[PROOF STEP]
by (auto intro: dom_sdom sdom_dom_succs)


[STATEMENT]
lemma dom_kildall_is_strict: "j < length start \<Longrightarrow> dom_kildall start ! j = res \<Longrightarrow> j \<notin> set res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
assume j_dom: "dom_kildall start ! j = res" and j_lt: "j < length start"
[PROOF STATE]
proof (state)
this:
dom_kildall start ! j = res
j < length start

goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
from j_dom
[PROOF STATE]
proof (chain)
picking this:
dom_kildall start ! j = res
[PROOF STEP]
have iter_fst: "(fst (iter f step start (unstables r step start))) ! j = res"
[PROOF STATE]
proof (prove)
using this:
dom_kildall start ! j = res

goal (1 subgoal):
 1. fst (iter f step start (unstables r step start)) ! j = res
[PROOF STEP]
by (auto simp add:dom_kildall_def r_def f_def step_def start_def nodes_semi_def kildall_def)
[PROOF STATE]
proof (state)
this:
fst (iter f step start (unstables r step start)) ! j = res

goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (iter f step start (unstables r step start)) ! j = res
[PROOF STEP]
obtain ss w where iter: "iter f step start (unstables r step start) = (ss, w)"
[PROOF STATE]
proof (prove)
using this:
fst (iter f step start (unstables r step start)) ! j = res

goal (1 subgoal):
 1. (\<And>ss w. iter f step start (unstables r step start) = (ss, w) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
iter f step start (unstables r step start) = (ss, w)

goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
with iter_fst
[PROOF STATE]
proof (chain)
picking this:
fst (iter f step start (unstables r step start)) ! j = res
iter f step start (unstables r step start) = (ss, w)
[PROOF STEP]
have res: "ss!j = res"
[PROOF STATE]
proof (prove)
using this:
fst (iter f step start (unstables r step start)) ! j = res
iter f step start (unstables r step start) = (ss, w)

goal (1 subgoal):
 1. ss ! j = res
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ss ! j = res

goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
with dom_iter_properties2 iter
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (?ss, ?w) \<longrightarrow> (\<forall>p<n. ?ss ! p \<noteq> rev [0..<n])
iter f step start (unstables r step start) = (ss, w)
ss ! j = res
[PROOF STEP]
have res_neq_all: "res \<noteq> rev [0..<n]"
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss, ?w) \<longrightarrow> (\<forall>p<n. ?ss ! p \<noteq> rev [0..<n])
iter f step start (unstables r step start) = (ss, w)
ss ! j = res

goal (1 subgoal):
 1. res \<noteq> rev [0..<n]
[PROOF STEP]
using len_start_is_n  j_lt len_start_is_n
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss, ?w) \<longrightarrow> (\<forall>p<n. ?ss ! p \<noteq> rev [0..<n])
iter f step start (unstables r step start) = (ss, w)
ss ! j = res
length start = n
j < length start
length start = n

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

goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
with iter iter_dom_properties
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (ss, w)
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
res \<noteq> rev [0..<n]
[PROOF STEP]
have "\<forall>p < n. (ss!p) \<noteq> rev [0..< n] \<longrightarrow> (\<forall>x\<in>set ( (ss!p)). x < p)"
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (ss, w)
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> wf_dom ?ss' ?w' \<and> stables r step ?ss' \<and> start [\<sqsubseteq>\<^bsub>r\<^esub>] ?ss' \<and> (\<forall>ts\<in>nlists n A. start [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<and> stables r step ts \<longrightarrow> ?ss' [\<sqsubseteq>\<^bsub>r\<^esub>] ts)
res \<noteq> rev [0..<n]

goal (1 subgoal):
 1. \<forall>p<n. ss ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)
[PROOF STEP]
by (auto simp add:wf_dom_def)
[PROOF STATE]
proof (state)
this:
\<forall>p<n. ss ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)

goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
with j_lt len_start_is_n res res_neq_all
[PROOF STATE]
proof (chain)
picking this:
j < length start
length start = n
ss ! j = res
res \<noteq> rev [0..<n]
\<forall>p<n. ss ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)
[PROOF STEP]
have "(\<forall>x\<in>set res. x < j)"
[PROOF STATE]
proof (prove)
using this:
j < length start
length start = n
ss ! j = res
res \<noteq> rev [0..<n]
\<forall>p<n. ss ! p \<noteq> rev [0..<n] \<longrightarrow> (\<forall>x\<in>set (ss ! p). x < p)

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

goal (1 subgoal):
 1. \<lbrakk>j < length start; dom_kildall start ! j = res\<rbrakk> \<Longrightarrow> j \<notin> set res
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set res. x < j
[PROOF STEP]
show "j \<notin> set res"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set res. x < j

goal (1 subgoal):
 1. j \<notin> set res
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<notin> set res

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sdom_asyc: "strict_dom i j \<Longrightarrow> j \<in> set (g_V G) \<Longrightarrow> i \<noteq> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> i \<noteq> j
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> i \<noteq> j
[PROOF STEP]
assume sdom_i_j: "strict_dom i j" and "j \<in> set (g_V G)"
[PROOF STATE]
proof (state)
this:
strict_dom i j
j \<in> set (g_V G)

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> i \<noteq> j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
strict_dom i j
j \<in> set (g_V G)
[PROOF STEP]
have j_lt: "j < length start"
[PROOF STATE]
proof (prove)
using this:
strict_dom i j
j \<in> set (g_V G)

goal (1 subgoal):
 1. j < length start
[PROOF STEP]
using start_def n_def nodes_def verts_set
[PROOF STATE]
proof (prove)
using this:
strict_dom i j
j \<in> set (g_V G)
start \<equiv> [] # replicate (length (g_V G) - 1) (rev [0..<n])
n \<equiv> length nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}

goal (1 subgoal):
 1. j < length start
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < length start

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> i \<noteq> j
[PROOF STEP]
let ?start = " [] # (replicate (length (g_V G) - 1) ( (rev[0..<length(g_V G)])))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> i \<noteq> j
[PROOF STEP]
have eq_start: "?start = start"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start = start
[PROOF STEP]
using n_def nodes_def start_def
[PROOF STATE]
proof (prove)
using this:
n \<equiv> length nodes
nodes \<equiv> g_V G
start \<equiv> [] # replicate (length (g_V G) - 1) (rev [0..<n])

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

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> i \<noteq> j
[PROOF STEP]
from sdom_i_j
[PROOF STATE]
proof (chain)
picking this:
strict_dom i j
[PROOF STEP]
have i_in: "i \<in> set (dom_kildall ?start !j)"
[PROOF STATE]
proof (prove)
using this:
strict_dom i j

goal (1 subgoal):
 1. i \<in> set (dom_kildall start ! j)
[PROOF STEP]
by (auto simp add:strict_dom_def)
[PROOF STATE]
proof (state)
this:
i \<in> set (dom_kildall start ! j)

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> i \<noteq> j
[PROOF STEP]
from j_lt
[PROOF STATE]
proof (chain)
picking this:
j < length start
[PROOF STEP]
have j_nin: "j \<notin> set (dom_kildall ?start !j)"
[PROOF STATE]
proof (prove)
using this:
j < length start

goal (1 subgoal):
 1. j \<notin> set (dom_kildall start ! j)
[PROOF STEP]
using eq_start
[PROOF STATE]
proof (prove)
using this:
j < length start
start = start

goal (1 subgoal):
 1. j \<notin> set (dom_kildall start ! j)
[PROOF STEP]
by (simp add: dom_kildall_is_strict)
[PROOF STATE]
proof (state)
this:
j \<notin> set (dom_kildall start ! j)

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> i \<noteq> j
[PROOF STEP]
with i_in
[PROOF STATE]
proof (chain)
picking this:
i \<in> set (dom_kildall start ! j)
j \<notin> set (dom_kildall start ! j)
[PROOF STEP]
show "i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
i \<in> set (dom_kildall start ! j)
j \<notin> set (dom_kildall start ! j)

goal (1 subgoal):
 1. i \<noteq> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma propa_dom_invariant_complete:
  fixes i a b ss w
  assumes b_n_nil: "b \<noteq> [] "
      and propa: "propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w) "
      and wf_a_b: "wf_dom a b"
      and non_strict: "\<forall>i. i < n \<and>  k \<notin> set (a!i) \<longrightarrow> non_strict_dominate k i "
    shows "wf_dom ss w \<and> (\<forall>i. i < n \<and>  k \<notin> set ( ss ! i) \<longrightarrow> non_strict_dominate k i)"  (is "?PROP ?P")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b \<noteq> []
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)
wf_dom a b
\<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i

goal (1 subgoal):
 1. wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
let ?a_hdb = "a!hd b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
let ?qs = "step (hd b) (a!hd b)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
from wf_a_b b_n_nil propa
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
b \<noteq> []
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)
[PROOF STEP]
have wf_ss_w: "wf_dom ss w"
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)

goal (1 subgoal):
 1. wf_dom ss w
[PROOF STEP]
using propa_dom_invariant
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)
\<lbrakk>wf_dom ?ss ?w; ?w \<noteq> []; propa f (step (hd ?w) (?ss ! hd ?w)) ?ss (tl ?w) = (?ss', ?w')\<rbrakk> \<Longrightarrow> wf_dom ?ss' ?w'

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

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
from wf_a_b
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
[PROOF STEP]
have "\<forall>\<tau>\<in>set a. \<tau> \<in> A"
               and sorted_b: "sorted b"
               and len_a: "length a = n"
               and b_lt_n: "\<forall>x\<in>set b. x < n  "
[PROOF STATE]
proof (prove)
using this:
wf_dom a b

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

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<tau>\<in>set a. \<tau> \<in> A
Sorted_Less.sorted b
length a = n
\<forall>x\<in>set b. x < n
[PROOF STEP]
have set_a: "set a \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<tau>\<in>set a. \<tau> \<in> A
Sorted_Less.sorted b
length a = n
\<forall>x\<in>set b. x < n

goal (1 subgoal):
 1. set a \<subseteq> A
[PROOF STEP]
by (auto intro:nlistsI)
[PROOF STATE]
proof (state)
this:
set a \<subseteq> A

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
from sorted_b
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted b
[PROOF STEP]
have sorted_tl_b: "sorted (tl b)"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted b

goal (1 subgoal):
 1. Sorted_Less.sorted (tl b)
[PROOF STEP]
using b_n_nil
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted b
b \<noteq> []

goal (1 subgoal):
 1. Sorted_Less.sorted (tl b)
[PROOF STEP]
by (induct b) auto
[PROOF STATE]
proof (state)
this:
Sorted_Less.sorted (tl b)

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
from b_lt_n b_n_nil
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set b. x < n
b \<noteq> []
[PROOF STEP]
have hd_b_lt_n: "hd b < n"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set b. x < n
b \<noteq> []

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

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
with n_def nodes_def verts_set
[PROOF STATE]
proof (chain)
picking this:
n \<equiv> length nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}
hd b < n
[PROOF STEP]
have "hd b \<in> set (g_V G)"
[PROOF STATE]
proof (prove)
using this:
n \<equiv> length nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}
hd b < n

goal (1 subgoal):
 1. hd b \<in> set (g_V G)
[PROOF STEP]
using b_n_nil
[PROOF STATE]
proof (prove)
using this:
n \<equiv> length nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}
hd b < n
b \<noteq> []

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

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd b \<in> set (g_V G)
[PROOF STEP]
have fin_succ_hd_b: "finite (succs (hd b))"
[PROOF STATE]
proof (prove)
using this:
hd b \<in> set (g_V G)

goal (1 subgoal):
 1. finite (succs (hd b))
[PROOF STEP]
using fin_succs
[PROOF STATE]
proof (prove)
using this:
hd b \<in> set (g_V G)
\<forall>v\<in>set (g_V G). finite (succs v)

goal (1 subgoal):
 1. finite (succs (hd b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (succs (hd b))

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
from wf_a_b b_n_nil
[PROOF STATE]
proof (chain)
picking this:
wf_dom a b
b \<noteq> []
[PROOF STEP]
have sorted_hd_b_a: "sorted (rev (hd b # ?a_hdb))"
                       and step_pres_bounded: " \<forall>(q, \<tau>)\<in>set (step (hd b) ?a_hdb). q < length a \<and> \<tau> \<in> A"
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (hd b # a ! hd b)) &&& \<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A
[PROOF STEP]
using propa_dom_invariant_auxi
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
b \<noteq> []
\<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)

goal (1 subgoal):
 1. Sorted_Less.sorted (rev (hd b # a ! hd b)) &&& \<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:
Sorted_Less.sorted (rev (hd b # a ! hd b))
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
from hd_b_lt_n
[PROOF STATE]
proof (chain)
picking this:
hd b < n
[PROOF STEP]
have dist: "distinct (map fst ?qs)"
[PROOF STATE]
proof (prove)
using this:
hd b < n

goal (1 subgoal):
 1. distinct (map fst (step (hd b) (a ! hd b)))
[PROOF STEP]
using distinct_p
[PROOF STATE]
proof (prove)
using this:
hd b < n
?p < n \<longrightarrow> distinct (map fst (step ?p (?ss ! ?p)))

goal (1 subgoal):
 1. distinct (map fst (step (hd b) (a ! hd b)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (map fst (step (hd b) (a ! hd b)))

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
with set_a step_pres_bounded sorted_tl_b len_a
[PROOF STATE]
proof (chain)
picking this:
set a \<subseteq> A
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A
Sorted_Less.sorted (tl b)
length a = n
distinct (map fst (step (hd b) (a ! hd b)))
[PROOF STEP]
have "\<forall>(q, \<tau>) \<in> set ?qs. (fst(propa f ?qs a (tl b)))!q = \<tau> \<squnion>\<^bsub>f\<^esub>a!q"
[PROOF STATE]
proof (prove)
using this:
set a \<subseteq> A
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A
Sorted_Less.sorted (tl b)
length a = n
distinct (map fst (step (hd b) (a ! hd b)))

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). fst (propa f (step (hd b) (a ! hd b)) a (tl b)) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> a ! q
[PROOF STEP]
by (auto dest:propa_property1)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). fst (propa f (step (hd b) (a ! hd b)) a (tl b)) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> a ! q

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). fst (propa f (step (hd b) (a ! hd b)) a (tl b)) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> a ! q
[PROOF STEP]
have propa_ss1: "\<forall>(q, \<tau>) \<in> set ?qs. ss!q =  (hd b # ?a_hdb) \<squnion>\<^bsub>f\<^esub>a!q"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). fst (propa f (step (hd b) (a ! hd b)) a (tl b)) ! q = \<tau> \<squnion>\<^bsub>f\<^esub> a ! q

goal (1 subgoal):
 1. \<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). ss ! q = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! q
[PROOF STEP]
by (auto simp add:step_def exec_def transf_def)
[PROOF STATE]
proof (state)
this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). ss ! q = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! q

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
from step_pres_bounded sorted_tl_b set_a len_a dist
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A
Sorted_Less.sorted (tl b)
set a \<subseteq> A
length a = n
distinct (map fst (step (hd b) (a ! hd b)))
[PROOF STEP]
have  "\<And>q. q \<notin> set(map fst ?qs) \<Longrightarrow> q < length a \<Longrightarrow> (fst(propa f ?qs a (tl b)))!q = a!q"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). q < length a \<and> \<tau> \<in> A
Sorted_Less.sorted (tl b)
set a \<subseteq> A
length a = n
distinct (map fst (step (hd b) (a ! hd b)))

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<notin> set (map fst (step (hd b) (a ! hd b))); q < length a\<rbrakk> \<Longrightarrow> fst (propa f (step (hd b) (a ! hd b)) a (tl b)) ! q = a ! q
[PROOF STEP]
by (auto intro:propa_property2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<notin> set (map fst (step (hd b) (a ! hd b))); ?q < length a\<rbrakk> \<Longrightarrow> fst (propa f (step (hd b) (a ! hd b)) a (tl b)) ! ?q = a ! ?q

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
with propa
[PROOF STATE]
proof (chain)
picking this:
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)
\<lbrakk>?q \<notin> set (map fst (step (hd b) (a ! hd b))); ?q < length a\<rbrakk> \<Longrightarrow> fst (propa f (step (hd b) (a ! hd b)) a (tl b)) ! ?q = a ! ?q
[PROOF STEP]
have exec2: "\<And>q. q \<notin> set(map fst ?qs) \<Longrightarrow> q < length a \<Longrightarrow> ss!q = a!q"
[PROOF STATE]
proof (prove)
using this:
propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w)
\<lbrakk>?q \<notin> set (map fst (step (hd b) (a ! hd b))); ?q < length a\<rbrakk> \<Longrightarrow> fst (propa f (step (hd b) (a ! hd b)) a (tl b)) ! ?q = a ! ?q

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<notin> set (map fst (step (hd b) (a ! hd b))); q < length a\<rbrakk> \<Longrightarrow> ss ! q = a ! q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<notin> set (map fst (step (hd b) (a ! hd b))); ?q < length a\<rbrakk> \<Longrightarrow> ss ! ?q = a ! ?q

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
have "(\<forall>i. i < n \<and> k \<notin> set ( ss ! i) \<longrightarrow> non_strict_dominate k i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i
[PROOF STEP]
proof(intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n \<and> k \<notin> set (ss ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n \<and> k \<notin> set (ss ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
let ?a_i = "a!i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < n \<and> k \<notin> set (ss ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
assume "i < n \<and> k \<notin> set ( ss ! i) "
[PROOF STATE]
proof (state)
this:
i < n \<and> k \<notin> set (ss ! i)

goal (1 subgoal):
 1. \<And>i. i < n \<and> k \<notin> set (ss ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < n \<and> k \<notin> set (ss ! i)
[PROOF STEP]
have i_lt_n: "i < n" and k_nin_ss: "k \<notin> set (ss ! i) "
[PROOF STATE]
proof (prove)
using this:
i < n \<and> k \<notin> set (ss ! i)

goal (1 subgoal):
 1. i < n &&& k \<notin> set (ss ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < n
k \<notin> set (ss ! i)

goal (1 subgoal):
 1. \<And>i. i < n \<and> k \<notin> set (ss ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
from non_strict
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i
[PROOF STEP]
have g: "i < n \<and> a ! i =  ?a_i \<and> k \<notin> set ?a_i \<Longrightarrow> non_strict_dominate k i"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i

goal (1 subgoal):
 1. i < n \<and> a ! i = a ! i \<and> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < n \<and> a ! i = a ! i \<and> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i

goal (1 subgoal):
 1. \<And>i. i < n \<and> k \<notin> set (ss ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
have sorted_a_i: "sorted (rev ?a_i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sorted_Less.sorted (rev (a ! i))
[PROOF STEP]
using wf_a_b i_lt_n
[PROOF STATE]
proof (prove)
using this:
wf_dom a b
i < n

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

goal (1 subgoal):
 1. \<And>i. i < n \<and> k \<notin> set (ss ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
show "non_strict_dominate k i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
proof(cases "i \<in> (succs (hd b))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> succs (hd b) \<Longrightarrow> non_strict_dominate k i
 2. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<in> succs (hd b)

goal (2 subgoals):
 1. i \<in> succs (hd b) \<Longrightarrow> non_strict_dominate k i
 2. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
note i_succ_hdb = this
[PROOF STATE]
proof (state)
this:
i \<in> succs (hd b)

goal (2 subgoals):
 1. i \<in> succs (hd b) \<Longrightarrow> non_strict_dominate k i
 2. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with propa_ss1
[PROOF STATE]
proof (chain)
picking this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). ss ! q = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! q
i \<in> succs (hd b)
[PROOF STEP]
have ss_i: "ss!i =  (hd b # ?a_hdb) \<squnion>\<^bsub>f\<^esub> a!i"
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). ss ! q = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! q
i \<in> succs (hd b)

goal (1 subgoal):
 1. ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i
[PROOF STEP]
using fin_succ_hd_b
[PROOF STATE]
proof (prove)
using this:
\<forall>(q, \<tau>)\<in>set (step (hd b) (a ! hd b)). ss ! q = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! q
i \<in> succs (hd b)
finite (succs (hd b))

goal (1 subgoal):
 1. ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i

goal (2 subgoals):
 1. i \<in> succs (hd b) \<Longrightarrow> non_strict_dominate k i
 2. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i
[PROOF STEP]
have "ss!i =  (hd b # ?a_hdb ) \<squnion>\<^bsub>f\<^esub> ?a_i"
[PROOF STATE]
proof (prove)
using this:
ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i

goal (1 subgoal):
 1. ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i

goal (2 subgoals):
 1. i \<in> succs (hd b) \<Longrightarrow> non_strict_dominate k i
 2. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with sorted_hd_b_a sorted_a_i
[PROOF STATE]
proof (chain)
picking this:
Sorted_Less.sorted (rev (hd b # a ! hd b))
Sorted_Less.sorted (rev (a ! i))
ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i
[PROOF STEP]
have "set (ss!i) = set (hd b # ?a_hdb) \<inter> set ?a_i"
                                     and ss_i_merge: "ss!i =  ((inter_sorted_rev (hd b # ?a_hdb) ?a_i))"
[PROOF STATE]
proof (prove)
using this:
Sorted_Less.sorted (rev (hd b # a ! hd b))
Sorted_Less.sorted (rev (a ! i))
ss ! i = hd b # a ! hd b \<squnion>\<^bsub>f\<^esub> a ! i

goal (1 subgoal):
 1. set (ss ! i) = set (hd b # a ! hd b) \<inter> set (a ! i) &&& ss ! i = inter_sorted_rev (hd b # a ! hd b) (a ! i)
[PROOF STEP]
by (auto simp add:inter_sorted_correct f_def nodes_sup_def plussub_def)
[PROOF STATE]
proof (state)
this:
set (ss ! i) = set (hd b # a ! hd b) \<inter> set (a ! i)
ss ! i = inter_sorted_rev (hd b # a ! hd b) (a ! i)

goal (2 subgoals):
 1. i \<in> succs (hd b) \<Longrightarrow> non_strict_dominate k i
 2. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with k_nin_ss
[PROOF STATE]
proof (chain)
picking this:
k \<notin> set (ss ! i)
set (ss ! i) = set (hd b # a ! hd b) \<inter> set (a ! i)
ss ! i = inter_sorted_rev (hd b # a ! hd b) (a ! i)
[PROOF STEP]
have k_nin': "k \<notin> set (hd b # ?a_hdb) \<inter> set ?a_i"
[PROOF STATE]
proof (prove)
using this:
k \<notin> set (ss ! i)
set (ss ! i) = set (hd b # a ! hd b) \<inter> set (a ! i)
ss ! i = inter_sorted_rev (hd b # a ! hd b) (a ! i)

goal (1 subgoal):
 1. k \<notin> set (hd b # a ! hd b) \<inter> set (a ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<notin> set (hd b # a ! hd b) \<inter> set (a ! i)

goal (2 subgoals):
 1. i \<in> succs (hd b) \<Longrightarrow> non_strict_dominate k i
 2. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
proof(cases "k \<notin> set ?a_i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
 2. \<not> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k \<notin> set (a ! i)

goal (2 subgoals):
 1. k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
 2. \<not> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<notin> set (a ! i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<notin> set (a ! i)

goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
using i_lt_n g
[PROOF STATE]
proof (prove)
using this:
k \<notin> set (a ! i)
i < n
i < n \<and> a ! i = a ! i \<and> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i

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

goal (1 subgoal):
 1. \<not> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> k \<notin> set (a ! i)

goal (1 subgoal):
 1. \<not> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with k_nin'
[PROOF STATE]
proof (chain)
picking this:
k \<notin> set (hd b # a ! hd b) \<inter> set (a ! i)
\<not> k \<notin> set (a ! i)
[PROOF STEP]
have "k \<notin> set ?a_hdb" and k_neq_hdb: "k \<noteq> hd b"
[PROOF STATE]
proof (prove)
using this:
k \<notin> set (hd b # a ! hd b) \<inter> set (a ! i)
\<not> k \<notin> set (a ! i)

goal (1 subgoal):
 1. k \<notin> set (a ! hd b) &&& k \<noteq> hd b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<notin> set (a ! hd b)
k \<noteq> hd b

goal (1 subgoal):
 1. \<not> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with hd_b_lt_n non_strict
[PROOF STATE]
proof (chain)
picking this:
hd b < n
\<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i
k \<notin> set (a ! hd b)
k \<noteq> hd b
[PROOF STEP]
have n_k_hdb: "non_strict_dominate k (hd b)"
[PROOF STATE]
proof (prove)
using this:
hd b < n
\<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i
k \<notin> set (a ! hd b)
k \<noteq> hd b

goal (1 subgoal):
 1. non_strict_dominate k (hd b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
non_strict_dominate k (hd b)

goal (1 subgoal):
 1. \<not> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
from i_succ_hdb
[PROOF STATE]
proof (chain)
picking this:
i \<in> succs (hd b)
[PROOF STEP]
have "(hd b, i)\<in> g_E G"
[PROOF STATE]
proof (prove)
using this:
i \<in> succs (hd b)

goal (1 subgoal):
 1. (hd b, i) \<in> g_E G
[PROOF STEP]
by (auto simp add:succs_def)
[PROOF STATE]
proof (state)
this:
(hd b, i) \<in> g_E G

goal (1 subgoal):
 1. \<not> k \<notin> set (a ! i) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with n_k_hdb k_neq_hdb
[PROOF STATE]
proof (chain)
picking this:
non_strict_dominate k (hd b)
k \<noteq> hd b
(hd b, i) \<in> g_E G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
non_strict_dominate k (hd b)
k \<noteq> hd b
(hd b, i) \<in> g_E G

goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
using non_sdominate_succ
[PROOF STATE]
proof (prove)
using this:
non_strict_dominate k (hd b)
k \<noteq> hd b
(hd b, i) \<in> g_E G
\<lbrakk>(?i, ?j) \<in> g_E G; ?k \<noteq> ?i; non_strict_dominate ?k ?i\<rbrakk> \<Longrightarrow> non_strict_dominate ?k ?j

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
non_strict_dominate k i

goal (1 subgoal):
 1. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<notin> succs (hd b)

goal (1 subgoal):
 1. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with exec2
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?q \<notin> set (map fst (step (hd b) (a ! hd b))); ?q < length a\<rbrakk> \<Longrightarrow> ss ! ?q = a ! ?q
i \<notin> succs (hd b)
[PROOF STEP]
have "ss!i = a!i"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<notin> set (map fst (step (hd b) (a ! hd b))); ?q < length a\<rbrakk> \<Longrightarrow> ss ! ?q = a ! ?q
i \<notin> succs (hd b)

goal (1 subgoal):
 1. ss ! i = a ! i
[PROOF STEP]
using fin_succ_hd_b len_a i_lt_n
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<notin> set (map fst (step (hd b) (a ! hd b))); ?q < length a\<rbrakk> \<Longrightarrow> ss ! ?q = a ! ?q
i \<notin> succs (hd b)
finite (succs (hd b))
length a = n
i < n

goal (1 subgoal):
 1. ss ! i = a ! i
[PROOF STEP]
by (auto simp add:step_def exec_def)
[PROOF STATE]
proof (state)
this:
ss ! i = a ! i

goal (1 subgoal):
 1. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with k_nin_ss
[PROOF STATE]
proof (chain)
picking this:
k \<notin> set (ss ! i)
ss ! i = a ! i
[PROOF STEP]
have "k \<notin> set (a!i)"
[PROOF STATE]
proof (prove)
using this:
k \<notin> set (ss ! i)
ss ! i = a ! i

goal (1 subgoal):
 1. k \<notin> set (a ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<notin> set (a ! i)

goal (1 subgoal):
 1. i \<notin> succs (hd b) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with non_strict
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i
k \<notin> set (a ! i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i
k \<notin> set (a ! i)

goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
using i_lt_n
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i
k \<notin> set (a ! i)
i < n

goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
non_strict_dominate k i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
non_strict_dominate k i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> []; propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w); wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
with wf_ss_w
[PROOF STATE]
proof (chain)
picking this:
wf_dom ss w
\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i
[PROOF STEP]
show "?PROP ?P"
[PROOF STATE]
proof (prove)
using this:
wf_dom ss w
\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i

goal (1 subgoal):
 1. wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_dom ss w \<and> (\<forall>i. i < n \<and> k \<notin> set (ss ! i) \<longrightarrow> non_strict_dominate k i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma start_non_sdom: " i < n \<and> start!i =  res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<and> start ! i = res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i
[PROOF STEP]
proof(auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i < n; k \<notin> set (start ! i); res = start ! i\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
assume i_lt_n: "i < n" and k_nin: "k \<notin> set (start ! i)"
[PROOF STATE]
proof (state)
this:
i < n
k \<notin> set (start ! i)

goal (1 subgoal):
 1. \<lbrakk>i < n; k \<notin> set (start ! i); res = start ! i\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < n
k \<notin> set (start ! i)
[PROOF STEP]
have reach_i: "reachable i"
[PROOF STATE]
proof (prove)
using this:
i < n
k \<notin> set (start ! i)

goal (1 subgoal):
 1. reachable i
[PROOF STEP]
using n_def nodes_def verts_set len_verts_gt0 reachable
[PROOF STATE]
proof (prove)
using this:
i < n
k \<notin> set (start ! i)
n \<equiv> length nodes
nodes \<equiv> g_V G
set (g_V G) = {0..<length (g_V G)}
0 < length (g_V G)
\<forall>v\<in>set (g_V G). v \<in> (g_E G)\<^sup>* `` {0}

goal (1 subgoal):
 1. reachable i
[PROOF STEP]
by  (simp add:reachable_def)
[PROOF STATE]
proof (state)
this:
reachable i

goal (1 subgoal):
 1. \<lbrakk>i < n; k \<notin> set (start ! i); res = start ! i\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reachable i
[PROOF STEP]
obtain pa where pa_i: "path_entry (g_E G) pa i"
[PROOF STATE]
proof (prove)
using this:
reachable i

goal (1 subgoal):
 1. (\<And>pa. path_entry (g_E G) pa i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reachable_path_entry
[PROOF STATE]
proof (prove)
using this:
reachable i
reachable ?n \<Longrightarrow> \<exists>p. path_entry (g_E G) p ?n

goal (1 subgoal):
 1. (\<And>pa. path_entry (g_E G) pa i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_entry (g_E G) pa i

goal (1 subgoal):
 1. \<lbrakk>i < n; k \<notin> set (start ! i); res = start ! i\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
show "non_strict_dominate k i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
proof(cases "k \<in> set (g_V G)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<in> set (g_V G) \<Longrightarrow> non_strict_dominate k i
 2. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k \<in> set (g_V G)

goal (2 subgoals):
 1. k \<in> set (g_V G) \<Longrightarrow> non_strict_dominate k i
 2. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in> set (g_V G)
[PROOF STEP]
have "k < n"
[PROOF STATE]
proof (prove)
using this:
k \<in> set (g_V G)

goal (1 subgoal):
 1. k < n
[PROOF STEP]
using verts_set
[PROOF STATE]
proof (prove)
using this:
k \<in> set (g_V G)
set (g_V G) = {0..<length (g_V G)}

goal (1 subgoal):
 1. k < n
[PROOF STEP]
by (auto simp add:n_def nodes_def)
[PROOF STATE]
proof (state)
this:
k < n

goal (2 subgoals):
 1. k \<in> set (g_V G) \<Longrightarrow> non_strict_dominate k i
 2. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k < n
[PROOF STEP]
have k_in_verts: "k \<in> set (g_V G)" and k_in_verts': "k \<in> {0..<n}"
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. k \<in> set (g_V G) &&& k \<in> {0..<n}
[PROOF STEP]
using verts_set n_def nodes_def
[PROOF STATE]
proof (prove)
using this:
k < n
set (g_V G) = {0..<length (g_V G)}
n \<equiv> length nodes
nodes \<equiv> g_V G

goal (1 subgoal):
 1. k \<in> set (g_V G) &&& k \<in> {0..<n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> set (g_V G)
k \<in> {0..<n}

goal (2 subgoals):
 1. k \<in> set (g_V G) \<Longrightarrow> non_strict_dominate k i
 2. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
show "non_strict_dominate k i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
proof(cases "i = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<Longrightarrow> non_strict_dominate k i
 2. i \<noteq> 0 \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = 0

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> non_strict_dominate k i
 2. i \<noteq> 0 \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 0

goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
using any_sdominate_0 k_in_verts
[PROOF STATE]
proof (prove)
using this:
i = 0
?n \<in> set (g_V G) \<Longrightarrow> non_strict_dominate ?n 0
k \<in> set (g_V G)

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

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> 0
[PROOF STEP]
have "start!i = (rev [0..<n])"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0

goal (1 subgoal):
 1. start ! i = rev [0..<n]
[PROOF STEP]
using start_def i_lt_n n_def nodes_def
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0
start \<equiv> [] # replicate (length (g_V G) - 1) (rev [0..<n])
i < n
n \<equiv> length nodes
nodes \<equiv> g_V G

goal (1 subgoal):
 1. start ! i = rev [0..<n]
[PROOF STEP]
by (simp add:start_def)
[PROOF STATE]
proof (state)
this:
start ! i = rev [0..<n]

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with k_nin k_in_verts'
[PROOF STATE]
proof (chain)
picking this:
k \<notin> set (start ! i)
k \<in> {0..<n}
start ! i = rev [0..<n]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<notin> set (start ! i)
k \<in> {0..<n}
start ! i = rev [0..<n]

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
non_strict_dominate k i

goal (1 subgoal):
 1. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<notin> set (g_V G)

goal (1 subgoal):
 1. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
note k_nin_verts = this
[PROOF STATE]
proof (state)
this:
k \<notin> set (g_V G)

goal (1 subgoal):
 1. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
have "\<forall>pa. path_entry (g_E G) pa i \<longrightarrow> set pa \<subseteq> set (g_V G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>pa. path_entry (g_E G) pa i \<longrightarrow> set pa \<subseteq> set (g_V G)
[PROOF STEP]
using path_in_verts nodes_def
[PROOF STATE]
proof (prove)
using this:
path_entry (g_E G) ?l ?v \<Longrightarrow> set ?l \<subseteq> set (g_V G)
nodes \<equiv> g_V G

goal (1 subgoal):
 1. \<forall>pa. path_entry (g_E G) pa i \<longrightarrow> set pa \<subseteq> set (g_V G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>pa. path_entry (g_E G) pa i \<longrightarrow> set pa \<subseteq> set (g_V G)

goal (1 subgoal):
 1. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with k_nin_verts
[PROOF STATE]
proof (chain)
picking this:
k \<notin> set (g_V G)
\<forall>pa. path_entry (g_E G) pa i \<longrightarrow> set pa \<subseteq> set (g_V G)
[PROOF STEP]
have k_nin: "\<forall>pa. path_entry (g_E G) pa i \<longrightarrow> k \<notin> set pa"
[PROOF STATE]
proof (prove)
using this:
k \<notin> set (g_V G)
\<forall>pa. path_entry (g_E G) pa i \<longrightarrow> set pa \<subseteq> set (g_V G)

goal (1 subgoal):
 1. \<forall>pa. path_entry (g_E G) pa i \<longrightarrow> k \<notin> set pa
[PROOF STEP]
by (fastforce dest: contra_subsetD)
[PROOF STATE]
proof (state)
this:
\<forall>pa. path_entry (g_E G) pa i \<longrightarrow> k \<notin> set pa

goal (1 subgoal):
 1. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with pa_i
[PROOF STATE]
proof (chain)
picking this:
path_entry (g_E G) pa i
\<forall>pa. path_entry (g_E G) pa i \<longrightarrow> k \<notin> set pa
[PROOF STEP]
have "k \<notin> set pa"
[PROOF STATE]
proof (prove)
using this:
path_entry (g_E G) pa i
\<forall>pa. path_entry (g_E G) pa i \<longrightarrow> k \<notin> set pa

goal (1 subgoal):
 1. k \<notin> set pa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<notin> set pa

goal (1 subgoal):
 1. k \<notin> set (g_V G) \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with pa_i
[PROOF STATE]
proof (chain)
picking this:
path_entry (g_E G) pa i
k \<notin> set pa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path_entry (g_E G) pa i
k \<notin> set pa

goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
by (auto simp add: non_strict_dominate_def)
[PROOF STATE]
proof (state)
this:
non_strict_dominate k i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
non_strict_dominate k i

goal:
No subgoals!
[PROOF STEP]
qed