Theory Dom_Kildall_Property

(* Author: Nan Jiang *)


section ‹Properties of the kildall's algorithm on the semilattice ›

theory Dom_Kildall_Property
imports Dom_Kildall "Jinja.Listn" "Jinja.Kildall_1"
begin

lemma sorted_list_len_lt: "x ⊂ y ⟹ finite y ⟹ length (sorted_list_of_set x) < length (sorted_list_of_set y)" 
proof-
  let ?x = "sorted_list_of_set x"
  let ?y = "sorted_list_of_set y" 
  assume x_y: "x ⊂ y" and fin_y: "finite y" 
  then have card_x_y: "card x < card y" and fin_x: "finite x" 
    by (auto simp add:psubset_card_mono finite_subset)
  with fin_y have "length ?x = card x" and "length ?y = card y" by auto
  with card_x_y show ?thesis by auto
qed

lemma wf_sorted_list: 
  "wf ((λ(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)"
  apply (unfold finite_psubset_def)
  apply (rule wf_measure [THEN wf_subset])
  apply (simp add: measure_def inv_image_def image_def)
  by (auto intro: sorted_list_len_lt)

lemma sorted_list_psub: 
  "sorted w ⟶
   w ≠ [] ⟶
   (sorted_list_of_set (set (tl w)), w) ∈ (λ(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A ⊂ B ∧ finite B}"
proof(intro strip, simp add:image_iff)
  assume sorted_w: "sorted w" and w_n_nil: "w ≠ []" 
  let ?a = "set (tl w)" 
  let ?b = "set w" 

  from sorted_w have sorted_tl_w: "sorted (tl w)" and dist: "distinct w" by (induct w) (auto simp add: sorted_wrt_append )  
  with w_n_nil  have a_psub_b: "?a ⊂ ?b" by (induct w)auto
  from sorted_w sorted_tl_w have "w = sorted_list_of_set ?b" and "tl w = sorted_list_of_set (set (tl w))" 
    by (auto simp add: sorted_less_set_eq)
  with a_psub_b show "∃a b. a ⊂ b ∧ finite b ∧ sorted_list_of_set (set (tl w)) = sorted_list_of_set a ∧ w = sorted_list_of_set b"
    by auto  
qed

locale dom_sl = cfg_doms +
  fixes A and r and f and step and start and n 
  defines "A  ≡ ((rev ∘ sorted_list_of_set) ` (Pow (set (nodes))))" 
  defines "r  ≡ nodes_le"
  defines "f  ≡ nodes_sup"
  defines "n  ≡ (size nodes)"
  defines "step ≡ exec" 
  defines "start ≡ ([] # (replicate (length (g_V G) - 1) ( (rev[0..<n]))))::state_dom list "

begin 

lemma is_semi: "semilat(A,r,f)" 
  by(insert nodes_semi_is_semilat) (auto simp add:nodes_semi_def A_def r_def f_def)

―‹used by acc\_le\_listI›
lemma Cons_less_Conss [simp]:
  "x#xs [⊏⇩r] y#ys = (x ⊏⇩r y ∧ xs [⊑⇘r⇙] ys ∨ x = y ∧ xs [⊏⇩r] ys)"
  apply (unfold lesssub_def)
  apply auto
  apply (unfold lesssub_def lesub_def r_def)
  apply (simp only: nodes_le_refl)
  done

lemma acc_le_listI [intro!]:
  "acc r ⟹ acc (Listn.le r) "
  apply (unfold acc_def)
  apply (subgoal_tac "Wellfounded.wf(UN n. {(ys,xs).  size xs = n ∧ size ys = n ∧ xs <_(Listn.le r) ys})")
   apply (erule wf_subset)
   apply (blast intro: lesssub_lengthD)
  apply (rule wf_UN)
   prefer 2
   apply (rename_tac m n)
   apply (case_tac "m=n")
    apply simp
   apply (fast intro!: equals0I dest: not_sym)
  apply (rename_tac n)
  apply (induct_tac n)
   apply (simp add: lesssub_def cong: conj_cong)
  apply (rename_tac k)
  apply (simp add: wf_eq_minimal)
  apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
  apply clarify
  apply (rename_tac M m)
  apply (case_tac "∃x xs. size xs = k ∧ x#xs ∈ M")
   prefer 2
   apply (erule thin_rl)
   apply (erule thin_rl)
   apply blast
  apply (erule_tac x = "{a. ∃xs. size xs = k ∧ a#xs:M}" in allE)
  apply (erule impE)
   apply blast
  apply (thin_tac "∃x xs. P x xs" for P)
  apply clarify
  apply (rename_tac maxA xs)
  apply (erule_tac x = "{ys. size ys = size xs ∧ maxA#ys ∈ M}" in allE)
  apply (erule impE)
   apply blast
  apply clarify
  apply (thin_tac "m ∈ M")
  apply (thin_tac "maxA#xs ∈ M")
  apply (rule bexI)
   prefer 2
   apply assumption
  apply clarify
  apply simp
  apply blast
  done

lemma wf_listn: "wf {(y,x). x ⊏⇘Listn.le r⇙ y}" 
  by(insert acc_nodes_le acc_le_listI r_def)  (simp add:acc_def)

lemma wf_listn': "wf {(y,x). x [⊏⇩r] y}" 
  by (rule wf_listn)

lemma wf_listn_termination_rel: 
  "wf ({(y,x). x ⊏⇘Listn.le r⇙ y}  <*lex*> (λ(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)"
  by (insert wf_listn wf_sorted_list)  (fastforce dest:wf_lex_prod)

lemma inA_is_sorted: "xs ∈ A ⟹ sorted (rev xs)" 
  by (auto simp add:A_def sorted_less_sorted_list_of_set)

lemma list_nA_lt_refl: "xs ∈ nlists n A ⟶ xs [⊑⇘r⇙] xs"
proof
  assume "xs ∈ nlists n A"
  then have "set xs ⊆ A" by (rule nlistsE_set)
  then have "∀i<length xs. xs!i ∈ A" by auto
  then have "∀i<length xs. sorted (rev (xs!i))" by (simp add:inA_is_sorted)
  then show "xs [⊑⇘r⇙] xs" by(unfold Listn.le_def lesub_def) 
     (auto simp add:list_all2_conv_all_nth Listn.le_def r_def nodes_le_def) 
qed

lemma nil_inA: "[] ∈ A"
  apply (unfold A_def)
  apply (subgoal_tac "{} ∈ Pow (set nodes)")
  apply (subgoal_tac "[] = (λx. rev (sorted_list_of_set x)) {}")
    apply (fastforce intro:rev_image_eqI)
  by auto

lemma upt_n_in_pow_nodes: "{0..<n} ∈ Pow (set nodes)" 
  by(auto simp add:n_def nodes_def verts_set)

lemma rev_all_inA: "rev [0..<n] ∈ A"
proof(unfold A_def,simp)
  let ?f = "λx. rev (sorted_list_of_set x)" 
  have "rev [0..<n] =?f {0..<n}" by auto
  with upt_n_in_pow_nodes show "rev [0..<n] ∈ ?f ` Pow (set nodes)" 
    by (fastforce intro: image_eqI)
qed

lemma len_start_is_n: "length start = n" 
  by (insert len_verts_gt0) (auto simp add:start_def n_def nodes_def dest:Suc_pred)

lemma len_start_is_len_verts: "length start = length (g_V G)" 
  using len_verts_gt0 by (simp add:start_def)

lemma start_len_gt_0: "length start > 0" 
  by (insert len_verts_gt0) (simp add:start_def) 

lemma start_subset_A: "set start ⊆ A" 
  by(auto simp add:nil_inA rev_all_inA start_def)

lemma start_in_A : "start ∈ (nlists n A)" 
  by (insert start_subset_A len_start_is_n)(fastforce intro:nlistsI)

lemma sorted_start_nth: "i < n ⟹ sorted (rev (start!i))" 
  apply(subgoal_tac "start!i ∈ A")    
  apply (fastforce dest:inA_is_sorted)
  by (auto simp add:start_subset_A  len_start_is_n)

lemma start_nth0_empty: "start!0 = []"
  by (simp add:start_def)

lemma start_nth_lt0_all: "∀p∈{1..< length start}. start!p = (rev [0..<n])" 
  by (auto simp add:start_def)
                                                          
lemma in_nodes_lt_n: "x ∈ set (g_V G) ⟹ x < n" 
  by (simp add:n_def nodes_def verts_set)

lemma start_nth0_unstable_auxi: "¬ [0] ⊑⇘r⇙ (rev [0..<n])"  
  by (insert len_verts_gt1 verts_ge_Suc0)
  (auto simp add:r_def lesssub_def lesub_def nodes_le_def n_def nodes_def)
                                                          
lemma start_nth0_unstable: "¬ stable r step start 0" 
proof(rule notI,auto simp add: start_nth0_empty stable_def step_def exec_def transf_def) 
  assume ass: "∀x∈set (sorted_list_of_set (succs 0)). [0] ⊑⇘r⇙ start ! x"
  from succ_of_entry0 obtain s where "s ∈ succs 0" and "s ≠ 0 ∧ s ∈ set (g_V G)" using head_is_vert 
    by (auto simp add:succs_def)
  then have "s ∈ set (sorted_list_of_set (succs 0))" 
        and "start!s = (rev [0..<n])" using fin_succs verts_set len_verts_gt0 by (auto simp add:start_def)
  then show False using ass start_nth0_unstable_auxi by auto
qed

lemma start_nth_unstable: 
  assumes "p ∈ {1 ..< length (g_V G)} "
      and "succs p ≠ {}"
    shows "¬ stable r step start p" 
proof (rule notI, unfold stable_def)  
  let ?step_p = "step p (start ! p)"
  let ?rev_all = "rev[0..<length(g_V G)]"
  assume sta: "∀(q, τ)∈set ?step_p. τ ⊑⇘r⇙ start ! q"  

  from assms(1) have n_sorted: "¬ sorted (rev (p # ?rev_all))"    
                 and p:"p ∈ set (g_V G)" and "start!p = ?rev_all" using verts_set by (auto simp add:n_def nodes_def start_def sorted_wrt_append)  
  with sta have step_p: "∀(q, τ)∈set ?step_p. sorted (rev (p # ?rev_all)) ∨ (p # ?rev_all = start!q)" 
    by (auto simp add:step_def exec_def transf_def lesssub_def lesub_def r_def nodes_le_def)
  
  from assms(2) fin_succs p obtain a b where a_b: "(a, b) ∈ set ?step_p" by (auto simp add:step_def exec_def transf_def)
  with step_p have "sorted (rev (p # ?rev_all)) ∨ (p # ?rev_all = start!a)" by auto
  with n_sorted have eq_p_cons: "(p # ?rev_all = start!a)" by auto
 
  from p have "∀(q, τ)∈set ?step_p. q < n" using succ_in_G fin_succs verts_set n_def nodes_def by (auto simp add:step_def exec_def)
  with a_b have "a < n" using len_start_is_n by auto
  then have "sorted (rev (start!a))" using sorted_start_nth by auto
  with eq_p_cons n_sorted show False  by auto

qed

lemma start_unstable_cond: 
  assumes "succs p ≠ {} "
      and "p < length (g_V G)"
    shows "¬ stable r step start p"  
  using assms start_nth0_unstable start_nth_unstable 
  by(cases "p = 0")  auto

lemma unstable_start: "unstables r step start = sorted_list_of_set ({p. succs p ≠ {} ∧ p < length start})"
  using len_start_is_len_verts start_unstable_cond
  by (subgoal_tac "{p. p < length start ∧ ¬ stable r step start p} = {p. succs p ≠ {} ∧ p < length start}")
     (auto simp add: unstables_def stable_def step_def exec_def)

end

declare sorted_list_of_set_insert_remove[simp del]

context dom_sl
begin 

lemma (in dom_sl) decomp_propa: "⋀ss w. 
   (∀(q,t)∈set qs. q < size ss ∧ t ∈ A ) ⟹ 
   sorted w ⟹ 
   set ss ⊆ A ⟹ 
   propa f qs ss w = (merges f qs ss, (sorted_list_of_set ({q. ∃t.(q,t)∈set qs ∧ t ⊔⇘f⇙ (ss!q) ≠ ss!q} ∪ set w)))"
(*<*)
  apply (induct qs)
   apply (fastforce intro:sorted_less_set_eq)
  apply (simp (no_asm))
  apply clarify 
 apply (subst sorted_insort_remove1)
  apply simp
  apply (simp add: sorted_less_sorted_list_of_set Semilat.closed_f[OF Semilat.intro, OF is_semi])
  apply (rule conjI)   
   apply (blast intro: arg_cong)
  apply(simp add: nth_list_update)
  by (auto intro: arg_cong)

lemma distinct_pair_filter_n: "distinct (map fst xs) ⟹ a ∉ set (map fst xs) ⟹ (map snd (filter (λ(x,y). x = a) xs)) = []"
  by (induct xs) (auto simp add: distinct_map_filter image_def)

lemma map_fst: "map fst (map (λpc. (pc, x)) xs) =  xs" 
  by (induct xs) auto

lemma distinct_p: "p < n ⟶ distinct (map fst (step p (ss!p)))" 
proof-
  let ?qs = "step p (ss!p)" 
  have "map fst ?qs = (rev (sorted_list_of_set(succs p)))" 
    using map_fst[of _ "(rev (sorted_list_of_set(succs p)))"] by (auto simp add:step_def exec_def)
  then show ?thesis by auto
qed

lemma distinct_pair_filter: "distinct (map fst xs) ⟹ (a,b)∈ set xs ⟹ map snd (filter (λx. fst x = a) xs) = [b]"
  apply (induct xs)
   apply simp
  apply (auto simp add: distinct_map_filter image_def)
proof-
  {
    fix xs
    assume "∀x∈set xs. a ≠ fst x " and " distinct (map fst xs)"
    then show "filter (λx. fst x = a) xs = []" by (induct xs)  auto
  }
qed

lemma split_comp_eq_pair: "(λx. fst x = a) = (λ(x,y). x = a)"
  by (rule split_comp_eq)

lemma distinct_pair_filter': "distinct (map fst xs) ⟹ (a,b)∈ set xs ⟹ (map snd (filter (λ(x,y). x = a) xs)) = [b]"
  using distinct_pair_filter by (simp only: split_comp_eq_pair)

lemma merges_property1: 
  fixes ss w qs
  assumes step_bounded_pres: "∀(q, τ) ∈ set qs. q < size ss ∧ τ ∈ A"
      and subset_ss_A:       "set ss ⊆ A "
      and len_ss_n:          "length ss = n "
      and dist:              "distinct (map fst qs) "
    shows "∀(q, τ) ∈ set qs. merges f qs ss!q = τ ⊔⇘f⇙ss!q" 
proof
  fix x
  assume "x ∈ set qs"
  from dist have τ: "∀(q, τ) ∈ set qs. (map snd (filter (λ(x,y). x = q) qs)) = [τ]" using distinct_pair_filter' by fastforce  
  from len_ss_n subset_ss_A have "ss ∈ nlists n A" by (rule nlistsI)
  with step_bounded_pres have merge_nth: "∀(q, τ) ∈ set qs. (merges f qs ss)!q = map snd [(p',t') ← qs. p'=q] ⨆⇘f⇙ ss!q" 
    by (fastforce intro:Semilat.nth_merges[OF Semilat.intro, OF is_semi]) ― ‹use lemma:  listE_length›
  with τ have "∀(q, τ) ∈ set qs. (merges f qs ss)!q = [τ]⨆⇘f⇙ ss!q" by fastforce
  then show "case x of (q, τ) ⇒ merges f qs ss ! q = τ ⊔⇘f⇙ ss ! q" using ‹x ∈ set qs› by auto  
qed

lemma propa_property1: 
  fixes ss w qs
  assumes step_bounded_pres: "∀(q, τ) ∈ set qs. q < size ss ∧ τ ∈ A  "
      and sorted_w:          "sorted (w ::nat list)"
      and subset_ss_A:       "set ss ⊆ A "
      and len_ss_n:          "length ss = n "
      and dist:              "distinct (map fst qs) "
    shows "∀(q, τ) ∈ set qs. (fst(propa f qs ss w))!q = τ ⊔⇘f⇙ss!q" 
  using assms
  apply (subgoal_tac "fst (propa f qs ss w) = merges f qs ss")
   apply(simp add: merges_property1) 
  by (auto dest:decomp_propa)

lemma merges_property2: 
  fixes ss w qs q
  assumes step_bounded_pres: "∀(q, τ) ∈ set qs. q < size ss ∧ τ ∈ A"
      and subset_ss_A:       "set ss ⊆ A"
      and len_ss_n:          "length ss = n "
      and dist:              "distinct (map fst qs) "
      and q_nin:             "q ∉ set(map fst qs) "
      and q_lt_len_ss:       "q < length ss "
    shows "(merges f qs ss)!q = ss!q" 
proof- 
  from len_ss_n subset_ss_A have "ss ∈ nlists n A" by (rule nlistsI)
  with step_bounded_pres q_lt_len_ss have merge_nth: "(merges f qs ss)!q = map snd [(p',t') ← qs. p'=q] ⨆⇘f⇙ ss!q" 
    by (fastforce intro:Semilat.nth_merges[OF Semilat.intro, OF is_semi])
  from dist have "q ∉ set(map fst qs) ⟹ (map snd (filter (λ(x,y). x = q) qs)) = []" using distinct_pair_filter_n by fastforce
  with merge_nth q_nin have "(merges f qs ss)!q = []⨆⇘f⇙ ss!q" by fastforce
  then show "(merges f qs ss)!q =  ss ! q" by auto  
qed

lemma propa_property2: 
  fixes ss w qs q
  assumes step_bounded_pres: "∀(q, τ) ∈ set qs. q < size ss ∧ τ ∈ A"
      and sorted_w:          "sorted (w ::nat list)"
      and subset_ss_A:       "set ss ⊆ A"
      and len_ss_n:          "length ss = n "
      and dist:              "distinct (map fst qs) "
      and q_nin:             "q ∉ set(map fst qs) "
      and q_lt_len_ss:       "q < length ss "
    shows "(fst(propa f qs ss w))!q = ss!q" 
  using assms
  apply (subgoal_tac "fst (propa f qs ss w) = merges f qs ss")
   apply(simp add: merges_property2) 
  by (auto dest:decomp_propa)

lemma merges_incr_lemma_dom:
 "∀xs. xs ∈ nlists n A ⟶ distinct (map fst ps) ⟶ (∀(p,x)∈set ps. p<size xs ∧ x ∈ A) ⟶ xs [⊑⇘r⇙] merges f ps xs"
proof(intro strip)
  fix xs
  assume xs_inA: "xs ∈ nlists n A " 
     and step_bounded_pres: "∀(p, x)∈set ps. p < length xs ∧ x ∈ A"
     and dist: "distinct (map fst ps)" 
  then have len_xs_n: "length xs = n" and subset_xs_inA: "set xs ⊆ A" by (auto simp add:nlistsE_length)
  with step_bounded_pres dist have merge1: "∀(q, τ) ∈ set ps. (merges f ps xs)!q = τ ⊔⇘f⇙xs!q" 
    using merges_property1 by auto

  from step_bounded_pres dist len_xs_n subset_xs_inA  
  have merge2: "⋀q. q ∉ set(map fst ps) ⟶ q < length xs ⟶ (merges f ps xs)!q = xs!q" using merges_property2 by auto
  
  have len_eq: "length xs = length (merges f ps xs)" by simp

  have "∀i<length xs. xs!i ⊑⇘r⇙ (merges f ps xs)!i" 
  proof(intro strip)
    fix i
    assume i_lt_len_xs: "i < length xs" 
    with xs_inA have xs_i_inA: "xs!i ∈ A" by auto

    show " xs ! i ⊑⇘r⇙ (merges f ps xs) ! i "
    proof(cases "i ∈ set (map fst ps)")
      case True
      then  obtain s' where s': "(i, s') ∈ set ps" by auto
      with merge1 have merge1': "(merges f ps xs)!i = s' ⊔⇘f⇙ xs ! i" by auto
      from s' step_bounded_pres have "s' ∈ A" by auto      
      with xs_i_inA merge1' show ?thesis  by (auto intro: Semilat.ub2[OF Semilat.intro, OF is_semi])
    next
      case False note i_nin = this
      with i_lt_len_xs merge2  have "(merges f ps xs)!i = xs!i" by auto
      with xs_i_inA show ?thesis by (auto simp add:Semilat.refl_r[OF Semilat.intro, OF is_semi])
    qed
  qed
  then have "∀i<length xs. xs!i ⊑⇘r⇙ (merges f ps xs)!i" by auto
  then have "∀i<length xs. lesub (xs!i) r  ((merges f ps xs)!i)" by (auto simp add:lesssub_def lesub_def)
  then have  "∀i<length xs. (λx y. lesub x r y) (xs!i)((merges f ps xs)!i)" by simp
  then have nth_lt: "⋀i. i <length xs ⟹  (λx y. lesub x r y) (xs!i)((merges f ps xs)!i)" by simp 
  with len_eq show "xs [⊑⇘r⇙] merges f ps xs" 
    by (auto simp only:list_all2_conv_all_nth Listn.le_def lesssub_def lesub_def) 
qed
   
lemma merges_incr_dom:
 "⟦ xs ∈ nlists n A; distinct (map fst ps); ∀(p,x)∈set ps. p<size xs ∧ x ∈ A ⟧ ⟹ xs [⊑⇘r⇙] merges f ps xs"
  by (simp add: merges_incr_lemma_dom)

lemma merges_same_conv_dom [rule_format]:
 "(∀xs. xs ∈ nlists n A ⟶ distinct (map fst ps) ⟶
        (∀(p,x)∈set ps. p<size xs ∧ x∈A) ⟶ 
        (merges f ps xs = xs) = (∀(p,x)∈set ps. x ⊑⇘r⇙ xs!p))"
  apply (induct_tac ps)
   apply (simp)
  apply clarsimp
  apply (rename_tac p x ps xs)
  apply (rule iffI)
   apply (rule context_conjI)
    apply (subgoal_tac "xs[p := x ⊔⇘f⇙ xs!p] [⊑⇘r⇙] xs")
     apply (fastforce dest!: le_listD 
            simp add: nth_list_update Semilat.plus_le_conv[OF Semilat.intro,OF is_semi] 
                      Semilat.ub1[OF Semilat.intro,OF is_semi] 
                      Semilat.ub2[OF Semilat.intro,OF is_semi]
Semilat.lub[OF Semilat.intro,OF is_semi] 
 )
    apply (erule subst, rule merges_incr_dom)
      apply (blast intro!: nlistsE_set intro: closedD nlistsE_length [THEN nth_in]
                            Semilat.closed_f[OF Semilat.intro, OF is_semi])
     apply clarify
  apply(intro strip)
  apply auto
   apply (erule allE)
   apply (erule impE)
    apply assumption
   apply (drule bspec)
    apply assumption
   apply (simp add: Semilat.le_iff_plus_unchanged [OF Semilat.intro, OF is_semi, THEN iffD1] list_update_same_conv [THEN iffD2])
   apply blast
  apply (simp add: Semilat.le_iff_plus_unchanged[OF Semilat.intro, OF is_semi, THEN iffD1] list_update_same_conv [THEN iffD2])
  done
(*>*)

lemma  (in Semilat)list_update_le_listI [rule_format]:
  "set xs ⊆ A ⟶ set ys ⊆ A ⟶ xs [⊑⇩r] ys ⟶ p < size xs ⟶  
   x ⊑⇩r ys!p ⟶ x∈A ⟶ 
   xs[p := x ⊔⇩f xs!p] [⊑⇩r] ys"
(*<*)
  apply (insert semilat)
  apply (simp only: Listn.le_def lesub_def semilat_def)
  apply (simp add: list_all2_conv_all_nth nth_list_update)
  done

lemma (in Semilat) merges_pres_le_ub:
  assumes "set ts ⊆ A"  
          "set ss ⊆ A"
          "∀(p,t)∈set ps. t ⊑⇘r⇙ ts!p ∧ t ∈ A ∧ p < size ts"  
          "ss [⊑⇘r⇙] ts"
  shows "merges f ps ss [⊑⇘r⇙] ts"
(*<*)
proof -
  { fix t ts ps
    have
    "⋀qs. ⟦set ts ⊆ A; ∀(p,t)∈set ps. t ⊑⇘r⇙ ts!p ∧ t ∈ A ∧ p< size ts ⟧ ⟹
          set qs ⊆ set ps ⟶ (∀ss. set ss ⊆ A ⟶ ss [⊑⇘r⇙] ts ⟶ merges f qs ss [⊑⇘r⇙] ts)"
    apply (induct_tac qs)
     apply simp
    apply (simp (no_asm_simp))
    apply clarify
    apply simp
    apply (erule allE, erule impE, erule_tac [2] mp)
       apply (drule bspec, assumption)
     apply (simp add: closedD  Semilat.closed_f)
    apply (drule bspec, assumption)
      apply (simp ) 
      apply(rule list_update_le_listI)
            apply auto
done 
  } note this [dest]  
  from assms show ?thesis by blast
qed
(*>*)

lemma termination_lemma: 
shows "⟦ss ∈ nlists n A; distinct (map fst qs); ∀(q,t)∈set qs. q<n ∧ t∈A; sorted w; w ≠ [] ⟧ ⟹ 
        ss [⊏⇩r] merges f qs ss ∨ 
        merges f qs ss = ss ∧ 
       (sorted_list_of_set ({q. ∃t. (q,t)∈set qs ∧ t ⊔⇘f⇙ ss!q ≠ ss!q} ∪ set (tl w)),w) ∈
       (λx. case x of (x, y) ⇒ (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A ⊂ B ∧ finite B}"
  apply(insert is_semi)
  apply (unfold lesssub_def)
  apply (simp (no_asm_simp) add: merges_incr_dom)
  apply (rule impI)
  apply (rule merges_same_conv_dom [THEN iffD1, elim_format]) 
      apply assumption+
    defer
    apply (rule sym, assumption)
   defer apply simp
  apply (subgoal_tac "∀q t. ¬((q, t) ∈ set qs ∧ t ⊔⇘f⇙ ss ! q ≠ ss ! q)")
   defer
   apply clarsimp
   apply (drule bspec, assumption) 
   apply (drule bspec, assumption)
   apply clarsimp      
  apply(subgoal_tac "{q. ∃t. (q, t) ∈ set qs ∧ t ⊔⇘f⇙ ss ! q ≠ ss ! q} ∪ set (tl w) = set (tl w)")
   apply (auto simp add: sorted_list_psub)
  done

lemma bounded_exec: "bounded step n"
  apply (insert is_semi,unfold semilat_def bounded_def step_def exec_def transf_def )
  by (auto simp add: n_def nodes_def verts_set fin_succs' succ_range)

lemma bounded_exec':
  fixes ss w a b
  assumes w_n_nil: " w ≠ [] "
       and step_hdw: " (a, b) ∈ set (step (hd w) (ss ! hd w)) "      
       and w_lt_n:"∀p∈set w. p < n "
      shows" a < n"
  using assms 
proof-
  from w_lt_n have "hd w < n" using w_n_nil by auto
  with bounded_exec have "( ∀τ. ∀(q,τ') ∈ set (step (hd w) τ). q<n)" by (auto simp add:bounded_def)
  with step_hdw show "a < n" by auto
qed

definition "wf_dom ss w ≡ 
    (∀τ∈set ss. τ ∈ A) ∧ 
    (∀p < n. sorted (rev ( (ss!p))) ∧
             (ss!p ≠ rev [0..< n] ⟶ (∀x∈set ( (ss!p)). x < p)) ∧
             (ss!p = rev [0..<n] ⟶  (∃x∈ set w. (x,p)∈ g_E G ∧ x < p)) ∧
             (p ∉ set w ⟶ stable r step ss p)) ∧              
    sorted w ∧ length ss = n ∧ (∀x∈set w. x < n) "

lemma wf_dom_w: 
  assumes "wf_dom ss w"
  shows "sorted w" 
  using assms
  by (auto simp add:wf_dom_def)

lemma wf_dom_w2: 
  assumes "wf_dom ss w"
  shows "(∀x∈set w. x < n)" 
  using assms
  by (auto simp add:wf_dom_def)

lemma wf_dom_len_eq: 
  assumes "wf_dom ss w"
  shows "(length ss = n)" 
  using assms
  by (auto simp add:wf_dom_def)


lemma  wf_dom_inA: 
  assumes "wf_dom ss w"
  shows "ss ∈ nlists n A" 
  using assms by (auto simp add:wf_dom_def intro: nlistsI)

lemma wf_dom_le: 
  assumes wf_ss_w: "wf_dom ss w"
  shows "ss [⊑⇘r⇙] ss" 
  using assms 
proof-
  from wf_ss_w have  "∀i<length ss. ss!i ∈ A" by (auto simp add:wf_dom_def)
  then have  "∀i<length ss. sorted (rev (ss!i))" by (auto simp add:A_def sorted_less_sorted_list_of_set)
  then show ?thesis 
    by (auto simp add:Listn.le_def lesssub_def lesub_def r_def nodes_le_def intro:list_all2_all_nthI)
qed

lemma pres_transf:  
  "∀ss∈A. p < n ⟶ (∀x<length ss. p > ss!x) ⟶ transf p ss ∈ A" 
proof(intro strip, unfold transf_def)
  fix ss  
  assume  p_lt_n: "p < n" and p_gt:  "∀x<length ss. ss!x < p" and τ_in_A: "ss ∈ A" 
  then have "set ss ⊆ set nodes" by (unfold A_def) (rule inpow_subset_nodes)
  with p_lt_n have p_τ_in: "set (p # ss) ⊆ set nodes" by (auto simp add:n_def nodes_def verts_set)
  from τ_in_A have sorted_τ: "sorted (rev ss)" by (simp add:inA_is_sorted)
  with p_gt have "sorted (rev (p # ss))" using Cons_sorted_less_nth by auto
  with p_τ_in show "(p # ss) ∈ A" by (unfold A_def) (fastforce intro: subset_nodes_inpow) 
qed

lemma pres_exec: 
  assumes "(q,τ) ∈ set (step p (ss!p))"
      and "∀n ∈ set (ss!p). p > n"
      and "ss!p ∈ A"
      and "p < n" 
    shows "τ ∈ A "
  using assms
 by (auto simp add:step_def exec_def pres_transf)

lemma wf_hd_neq_all: 
  assumes wf_ss_w: "wf_dom ss w " 
      and w_n_nil: "w ≠ [] " 
    shows " ss!(hd w) ≠ rev [0..<n]" 
proof(rule ccontr)
  assume "¬ ss ! hd w ≠  (rev [0..<n])" note x = this
  from wf_ss_w have "∀x∈ set w. x < n" and "sorted w" by (auto simp add:wf_dom_def)
  then have "hd w < n" and y:"∀x ∈ set w. x ≥ hd w" using w_n_nil by (induct w) (auto simp add:sorted_wrt_append)
  with wf_ss_w x have  "(∃x∈ set w. (x,hd w)∈ g_E G ∧ x < hd w)" by (auto simp add:wf_dom_def)  
  with y show False by auto
qed

lemma pres_wf_exec: 
  fixes ss w a b
  assumes wf_ss_w: "wf_dom ss w "
      and w_n_nil: "w ≠ [] "
    shows "∀(q,τ) ∈ set (step (hd w) (ss!(hd w))). τ ∈ A "
  using assms
proof(intro strip, auto)
  fix a b
  assume a_b: "(a, b) ∈ set (step (hd w) (ss ! hd w))"
  from wf_ss_w have sorted_w: "sorted w" and hd_w_lt_n: "hd w < n"  
    and ss_hdw_inA: "ss!hd w ∈ A" using w_n_nil by (auto simp add:wf_dom_def)
  from assms have ss_hd_w_neq_all: "ss!hd w ≠ (rev [0..<n])" by (rule wf_hd_neq_all)  
  with wf_ss_w hd_w_lt_n have "∀x∈set (ss!hd w). hd w > x" by (auto simp add:wf_dom_def)
  with ss_hdw_inA hd_w_lt_n a_b show "b ∈ A"  using pres_exec by auto
qed

lemma propa_dom_invariant_auxi: 
  assumes wf_a_b: "wf_dom a b" and b_n_nil: "b ≠ [] " 
    shows "a!hd b ≠ rev [0..<n] ∧
           sorted (rev (hd b # (a!hd b))) ∧
           set (hd b # (a!hd b)) ⊆ set nodes ∧
           hd b # (a!hd b) ∈ A ∧
           (∀(q, τ)∈set (step (hd b) (a!hd b)). q < length a ∧ τ ∈ A)" 
  using assms
proof-
  from assms have "a!hd b ∈ (rev ∘ sorted_list_of_set) ` (Pow (set nodes))"
              and  sorted_hdb: "sorted (rev (a!hd b))" 
              and hd_b_lt_n: "hd b < n" 
              and sorted_b: "sorted b" 
              and len_eq: "length a = n" by (auto simp add:A_def wf_dom_def) 
  then have as_subset_nodes: "set (a!hd b) ⊆ set nodes" by (auto simp add:inpow_subset_nodes)
  with n_def verts_set assms nodes_def have hdb_cons_subset_nodes: "set (hd b # (a!hd b)) ⊆ set nodes" by (auto simp add:wf_dom_def)
  then have hdb_subset_n: "set (hd b # (a!hd b)) ⊆ {0..<n}" using nodes_def verts_set n_def by auto

  from wf_a_b b_n_nil have a_hd_b_neq_all: "a!hd b ≠ (rev [0..<n])" using wf_hd_neq_all by auto
  with wf_a_b hd_b_lt_n sorted_hdb have sorted_hd_b_cons: "sorted (rev (hd b # (a!hd b)))" 
    by (fastforce simp add: wf_dom_def dest: Cons_sorted_less)

  from hdb_cons_subset_nodes have  "set ((hd b # (a!hd b))) ∈ Pow (set (g_V G))" by (auto simp add:nodes_def)
  then have pow1: "set ((hd b # (a!hd b))) ⊆ set nodes" by (auto simp add:nodes_def)
  from hdb_cons_subset_nodes sorted_hd_b_cons have "hd b # (a!hd b) ∈ (rev ∘ sorted_list_of_set) ` (Pow (set nodes))"
    by (fastforce intro: subset_nodes_inpow)
  then have hd_b_cons_in_A: "(hd b # (a!hd b)) ∈ A" by (unfold A_def ) (auto simp add:nodes_def)  

  have "(∀p<n. ∀τ. ∀(q,τ') ∈ set (step p τ). q<n)" 
    using bounded_exec by (auto simp add:bounded_def)
  with hd_b_lt_n have bounded: "∀(q,τ') ∈ set (step (hd b) (a!hd b)). q<n" by auto
  from wf_a_b b_n_nil have pres: "∀(q, τ)∈set(step (hd b) (a!hd b)). τ ∈ A" by (rule pres_wf_exec)
  with bounded pres have step_pres_bounded: "∀(q, τ)∈set (step (hd b) (a!hd b)). q < length a ∧ τ ∈ A " using  len_eq by auto
  with a_hd_b_neq_all sorted_hd_b_cons hdb_cons_subset_nodes hd_b_cons_in_A  show ?thesis by auto
qed

lemma propa_dom_invariant_aux:
  fixes a b ss w
assumes propa: "propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w) "    
    and b_n_nil: "b ≠ [] " 
    and a_in_A: "∀τ∈set a. τ ∈ A"   
    and ass: "∀p<n.
          sorted (rev ( (a ! p))) ∧
          (a!p ≠ rev [0..<n] ⟶ (∀x∈set (a!p). x < p)) ∧
          (a!p = rev [0..<n] ⟶ (∃x∈set b. (x,p)∈ g_E G ∧ x < p)) ∧
          (p ∉ set b ⟶ stable r step a p)"
    and sorted_b: "sorted b  "
    and len_eq:  "length a = n  "
    and b_lt_n: "∀x∈set b. x < n  "
  shows "(∀τ∈set ss. τ ∈ A) ∧
         (∀p<n.
           sorted (rev ( (ss ! p))) ∧
           (ss!p ≠ rev [0..<n] ⟶ (∀x∈set (ss!p). x < p)) ∧
           (ss!p = rev [0..<n] ⟶ (∃x∈ set w. (x,p)∈ g_E G ∧ x < p)) ∧
           (p ∉ set w ⟶ stable r step ss p)) ∧
         sorted w ∧ length ss = n ∧ (∀x∈set w. x <n)"
  using assms 
proof-
  let ?a_hdb = "a!hd b"
  let ?ss_hdw = "ss!hd w"
  let ?ss_hdb = "ss!hd b" 

  let ?a_hdw = "a!hd w" 

  let ?qs_a = "step (hd b) ?a_hdb" 
  let ?qs_ss = "step (hd w) ?ss_hdw" 
  let ?qs_ss_hdb = "step (hd b) ?ss_hdb" 

  let ?q_a_wl = "{q. ∃t.(q,t)∈set ?qs_a ∧ t ⊔⇘f⇙ (a!q) ≠ a!q}"
  let ?q_ss_wl = "{q. ∃t.(q,t)∈set ?qs_ss ∧ t ⊔⇘f⇙ (ss!q) ≠ ss!q}" 

  from a_in_A len_eq have a_in_list_nA: "a ∈ nlists n A" by (auto intro: nlistsI)
  from a_in_A have "∀p< length a. a!p ∈ A" by (auto simp add:A_def)
  then have a_p_subset: "∀p< length a. set (a!p) ⊆ set nodes" by (auto simp add:inpow_subset_nodes A_def)

  from a_in_A ass sorted_b len_eq b_lt_n  b_n_nil have wf_a_b: "wf_dom a b" by (auto simp add:wf_dom_def)
  with b_n_nil have a_hd_b_neq_all: "?a_hdb ≠ rev [0..<n]" 
                and sorted_hd_b_cons: "sorted (rev (hd b # ?a_hdb))"
                and hd_b_cons_in_nodes: "set (hd b # ?a_hdb) ⊆ set nodes" 
                and hd_b_cons_in_A: "hd b # ?a_hdb ∈ A"
                and step_pres_bounded: "(∀(q, τ)∈set (step (hd b) ?a_hdb). q < length a ∧ τ ∈ A)" 
    using propa_dom_invariant_auxi
    by auto
  then have hdb_subset_n: "set (hd b # ?a_hdb) ⊆ {0..<n}" using nodes_def verts_set n_def by auto
  
  from b_lt_n b_n_nil have hd_b_lt_n: "hd b < n" 
                       and tl_b_lt_n: "∀x∈ set (tl b). x < n" 
    by (induct b)(auto simp add:wf_dom_def)
  then have dist: "distinct (map fst ?qs_a)" using distinct_p  by auto   

  from b_lt_n len_eq sorted_b have sorted_tl_b: "sorted (tl b)" by (induct b) auto 

  from b_lt_n verts n_def nodes_def verts_set have b_in_verts: "∀x∈set b. x ∈ set (g_V G)" by auto
  then have hd_b_in_verts: "hd b ∈ set (g_V G)" using b_n_nil by auto
  then  have fin_succ_hd_b: "finite (succs (hd b))" using fin_succs  by auto    

  have fin_q1: "finite {q. ∃t.(q,t)∈set ?qs_a}" 
   and fin_q2: "finite ?q_a_wl" by (auto simp add:step_def exec_def image_def)
  then have fin: "finite (?q_a_wl ∪ set (tl b))" by auto 
  
  from a_in_A have set_a: "set a ⊆ A" by auto
  with step_pres_bounded sorted_tl_b len_eq dist
  have "∀(q, τ) ∈ set ?qs_a. (fst(propa f ?qs_a a (tl b)))!q = τ ⊔⇘f⇙a!q" by (auto dest:propa_property1)
  with propa have propa_ss1: "∀(q, τ) ∈ set ?qs_a. ss!q = τ ⊔⇘f⇙a!q" by simp  
  then have propa_ss1': "∀(q, τ) ∈ set ?qs_a. ss!q =  (hd b # ?a_hdb) ⊔⇘f⇙a!q" by (auto simp add:step_def exec_def transf_def)
  then have succ_self_eq: "∀(q, τ) ∈ set ?qs_a. q = hd b ⟶ ss!q = a!q"    
    by(auto simp add: f_def nodes_sup_def plussub_def inter_sorted_cons[OF sorted_hd_b_cons])    

  have step_hd_b: "∀(q,τ)∈set ?qs_a. τ = (hd b # ?a_hdb)"
    by(auto simp add:step_def exec_def transf_def) 

  from step_pres_bounded sorted_tl_b set_a len_eq dist 
  have  "⋀q. q ∉ set(map fst ?qs_a) ⟹ q < length a ⟹ (fst(propa f ?qs_a a (tl b)))!q = a!q" 
    by (auto intro:propa_property2)
  with propa have exec2: "⋀q. q ∉ set(map fst ?qs_a) ⟹ q < length a ⟹ ss!q = a!q" by auto
  then have ss_hd_b_eq_a: "ss!hd b = a!hd b" using hd_b_lt_n len_eq  fin_succ_hd_b succ_self_eq
    by (auto simp add:step_def exec_def)  
  then have hdb_nin_w: "hd b ∉ ?q_a_wl" using fin_succ_hd_b propa_ss1 by (auto simp add:step_def exec_def)

  from step_pres_bounded sorted_tl_b set_a 
  have "snd (propa f ?qs_a a (tl b)) = (sorted_list_of_set (?q_a_wl ∪ set (tl b)))" 
    by (fastforce dest:decomp_propa)
  with propa have ww: "w = sorted_list_of_set (?q_a_wl ∪ set (tl b))" by simp  
  then have sorted_w:"sorted w" by (simp add:sorted_less_sorted_list_of_set)
  from ww have set_ww: "set w =?q_a_wl ∪ set (tl b)" using fin by auto
  with step_pres_bounded tl_b_lt_n ww fin len_eq have w_lt_n: "(∀x∈set w. x < n)" using len_eq by auto
  then have w_set': "∀x∈set w. x ∈ {0..<n}" using verts_set len_eq  by auto
  then have w_set: "set w ⊆ {0..<n}" by auto

  from sorted_b have hd_b_nin_tl_b: "hd b ∉ set (tl b) " by (induct b) (auto simp add:sorted_wrt_append)
  with hdb_nin_w ww have "hd b ∉ set w" using fin by auto 

  from step_pres_bounded sorted_tl_b set_a propa have ss_merge: "ss = merges f ?qs_a a" by (auto dest: decomp_propa)
  from step_pres_bounded a_in_list_nA have "∀(q, τ)∈set (step (hd b) (a ! hd b)). q < n ∧ τ ∈ A" using len_eq by simp
  with a_in_list_nA have "merges f ?qs_a a  ∈ nlists n A"  
    by (rule Semilat.merges_preserves_type[OF Semilat.intro, OF is_semi])
  with ss_merge have ss_in_A: "ss ∈ nlists n A" by simp
  then have len_ss_n: "length ss = n"  using  len_eq by simp
  with len_eq  have len_ss_n: "length ss = n" by auto

  from ss_in_A have set_ss: "set ss ⊆ A " by (rule nlistsE_set)
  then have ss_inA:  "∀τ∈set ss. τ ∈ A" by auto
  then have ss_p_subset: "∀p< length ss.  set (ss!p) ⊆ set nodes" by (auto simp add:inpow_subset_nodes A_def)

  from w_lt_n len_ss_n have bounded_a: "⋀a b.  w ≠ [] ⟹ (a, b) ∈ set ?qs_ss ⟹ a < length ss" 
    by (auto simp add:bounded_exec') 

  have sorted_a_hdw_n: "w ≠ [] ⟶ sorted (rev ?a_hdw)" 
    using wf_a_b len_eq w_set' by (auto simp add:wf_dom_def)

  have sorted_ss_hdw_n: "w ≠ [] ⟶ sorted (rev ?ss_hdw)" 
    using ss_in_A inA_is_sorted w_lt_n by auto

  have "w ≠ [] ⟶ (hd w # ?ss_hdw) ∈ A"
  proof
    assume w_n_nil: "w ≠ []" 
    with w_lt_n have hd_w_lt_n: "hd w < n" by auto   
    with a_in_A have a_hdw_inA: "?a_hdw ∈ A" using len_eq by auto 
    then have a_hdw_in_nodes: "set ?a_hdw ⊆ set nodes" by (unfold A_def )(rule inpow_subset_nodes)

    from hd_w_lt_n have hdw_in_nodes: "hd w ∈ set nodes" using verts_set by (simp add:n_def nodes_def) 
    from sorted_a_hdw_n w_n_nil have sorted_a_hdw: "sorted (rev ?a_hdw)" by auto

    show "(hd w # ?ss_hdw) ∈ A"
    proof(cases "hd w ∈ succs (hd b)")
      case True
      then obtain s where s: "(hd w, s) ∈ set ?qs_a" using fin_succ_hd_b  by (auto simp add:step_def exec_def)
      with step_hd_b have "s = (hd b # ?a_hdb)" by auto
      with s propa_ss1 have ss_hd_w: "?ss_hdw = (hd b # ?a_hdb) ⊔⇘f⇙ ?a_hdw"  by auto
      with hd_b_cons_in_A a_hdw_inA have "?ss_hdw ∈ A" by (simp add: Semilat.closed_f[OF Semilat.intro, OF is_semi])   
      then have ss_hdw_in_nodes: "set ?ss_hdw ⊆ set nodes" 
        by (auto simp add:inpow_subset_nodes A_def)       
      with hdw_in_nodes have hdw_cons_ss_in_nodes: "set (hd w # ?ss_hdw) ⊆ set nodes" by auto

      then have in_pow: "set (hd w # ?ss_hdw) ∈ Pow (set (g_V G))" by (auto simp add:nodes_def)
          
      from sorted_a_hdw ss_hd_w sorted_hd_b_cons
      have "sorted (rev ?ss_hdw)" and "set ?ss_hdw = set (hd b # ?a_hdb) ∩ set ?a_hdw" 
        by (auto simp add:f_def plussub_def nodes_sup_def inter_sorted_correct)
      then have sorted_ss_hdw: "sorted (rev ?ss_hdw)" 
            and ss_hdw_subset_a_hdb_cons: "set ?ss_hdw ⊆ set (hd b # ?a_hdb)" 
            and ss_hdw_subset_a_hdw: "set ?ss_hdw ⊆ set ?a_hdw" by auto         

      from  sorted_hd_b_cons have "∀x∈ set (hd b # ?a_hdb). x ≤ hd b" using b_n_nil 
        by (induct b) (auto simp add:sorted_wrt_append)
      with ss_hdw_subset_a_hdb_cons
      have ss_hdw_lt_hdb: "∀x∈set ?ss_hdw. x ≤ hd b" using sorted_hd_b_cons by auto                   
      
      have sorted_rev_hdw: "sorted (rev (hd w # ?ss_hdw))" 
      proof(cases "?a_hdw = rev [0..<n]")
        case True
        with wf_a_b have "∃x∈ set b. (x,hd w)∈ g_E G ∧ x < hd w" using hd_w_lt_n by (auto simp add:wf_dom_def)
        then obtain prev_hd_w where prev_hd_w_in_b: "prev_hd_w ∈ set b" 
                                and prev_hd_w: "(prev_hd_w, hd w)∈ g_E G"
                                and prev_hd_w_lt: "prev_hd_w < hd w" by auto


        show ?thesis
        proof(cases "prev_hd_w = hd b")
          case True
          with prev_hd_w_lt have "hd b < hd w" by auto
          with ss_hdw_lt_hdb  have "∀x∈set ?ss_hdw. hd w > x" by auto
          with sorted_ss_hdw show ?thesis by (auto simp add:sorted_wrt_append)
        next
          case False
          with prev_hd_w_in_b have "prev_hd_w ∈ set (tl b)" by (induct b) auto
          with ww have prev_hd_w_nin_w: "prev_hd_w ∈ set w" using fin by auto
          from sorted_w have "∀x∈ set w. x ≥ hd w" by(induct w) (auto simp add:sorted_wrt_append sorted_less_sorted_list_of_set) 
          with prev_hd_w_lt have "prev_hd_w ∉ set w" by auto
          with prev_hd_w_nin_w show ?thesis by auto
        qed

      next
        case False
        with wf_a_b have "(∀x∈set ?a_hdw. x < hd w)" using hd_w_lt_n by (auto simp add:wf_dom_def)
        with ss_hdw_subset_a_hdw
        have "(∀x∈set ?ss_hdw. x < hd w)" by auto
        with sorted_ss_hdw show ?thesis by (auto simp add:sorted_wrt_append)
      qed
      with hdw_cons_ss_in_nodes show "hd w # ?ss_hdw ∈ A" using A_def by (fastforce dest:subset_nodes_inpow)

    next
      case False note hd_w_nin_succ_hdb = this
      then have "hd w ∉ set (map fst ?qs_a)" using fin_succ_hd_b by (auto simp add:step_def exec_def)
      with exec2 have ss_hd_w_eq_a: "?ss_hdw = ?a_hdw"  using hd_w_lt_n len_ss_n len_eq  by auto
      with a_hdw_in_nodes  sorted_a_hdw have ss_hdw_in_nodes: "set ?ss_hdw ⊆ set nodes" 
                                         and sorted_ss_hdw: "sorted (rev ?ss_hdw)" by auto
      with hdw_in_nodes have hdw_cons_in_nodes: "set (hd w # ?ss_hdw) ⊆ set nodes" by (auto) 

      from hd_w_nin_succ_hdb ww have hd_w_non: "hd w ∉{q. ∃t. (q, t) ∈ set ?qs_a ∧ t ⊔⇘f⇙ a ! q ≠ a ! q}"
        using fin_succ_hd_b by (auto simp add:step_def exec_def )

      from set_ww hd_w_non have hd_w_in_tl_b: "hd w ∈ set (tl b)" using sorted_tl_b ‹w ≠ []› by auto      
        
      have sorted_rev_hdw: "sorted (rev (hd w # ?ss_hdw))"
      proof(cases "?a_hdw = rev [0..<n]")
        case True
        with wf_a_b have "∃x∈ set b. (x,hd w)∈ g_E G ∧ x < hd w" using hd_w_lt_n by (auto simp add:wf_dom_def)
        then obtain prev_hd_w where prev_hd_w_in_b: "prev_hd_w ∈ set b" 
                                and prev_hd_w:      "(prev_hd_w, hd w)∈ g_E G" 
                                and prev_hd_w_lt:   "prev_hd_w < hd w"  by auto
        from ww have "sorted w" by(simp add:sorted_less_sorted_list_of_set)
        then have "∀x∈ set w. x ≥ hd w" using w_n_nil by (induct w) (auto simp add:sorted_wrt_append)
        with prev_hd_w_lt have prev_hd_w_nin_w: "prev_hd_w ∉ set w" using w_n_nil by auto 
        with set_ww have "prev_hd_w ∉ set (tl b)" by auto
        with prev_hd_w_in_b have "prev_hd_w = hd b" using sorted_b by (induct b) auto
        with prev_hd_w have "(hd b, hd w) ∈ g_E G" by auto 
        with hd_w_nin_succ_hdb show ?thesis by (auto simp add:succs_def)
      next
        case False
        with wf_a_b have a_hdw_lt: "(∀x∈set ?a_hdw. x < hd w)" 
                     and "sorted (rev ?a_hdw)" using hd_w_lt_n by (auto simp add:wf_dom_def)
        with ss_hd_w_eq_a have "sorted (rev ?ss_hdw)" by simp
        from ss_hd_w_eq_a  have "?a_hdw =  ?ss_hdw" by auto
        with a_hdw_lt have "∀x∈set ?ss_hdw. x < hd w" by auto
        with sorted_ss_hdw show ?thesis by (auto simp add:sorted_wrt_append)
      qed 
      with hdw_cons_in_nodes show " (hd w # ss ! hd w) ∈ A" by (unfold A_def) (rule subset_nodes_inpow)
    qed
  qed   
  then have pres_ss: "⋀q τ. w ≠ [] ⟹ (q, τ) ∈ set (step (hd w) ?ss_hdw) ⟹ τ ∈ A" 
    by (auto simp add:step_def exec_def transf_def)
 
  have hd_b_ss_sta: "stable r step ss (hd b)" 
  proof(unfold stable_def, clarsimp)
    fix q τ
    assume "(q, τ) ∈ set ?qs_ss_hdb "
    then have "q ∈ succs (hd b)" and  "τ = transf (hd b) ?ss_hdb" using hd_b_lt_n fin_succ_hd_b
      by (auto simp add:step_def exec_def)
    then have τ:"τ =  (hd b # ?a_hdb)" using ss_hd_b_eq_a by (auto simp add:transf_def)  
    from ‹q ∈ succs (hd b)› hd_b_lt_n have "q∈ set (g_V G)" using succ_in_G by auto
    then have "q < n" using verts_set by (auto simp add:n_def nodes_def)
    with wf_a_b have a_q_inA: "a!q ∈ A"  by (auto simp add:wf_dom_def)
    from wf_a_b a_hd_b_neq_all hd_b_lt_n have "∀x∈ set ( (a!hd b)). x < hd b" by (auto simp add:wf_dom_def)
    with sorted_hd_b_cons have "sorted (rev (hd b # ?a_hdb))"  by (auto simp add:sorted_wrt_append)
    from propa_ss1 ‹(q, τ) ∈ set (step (hd b) (ss ! hd b))›
    have "ss!q = τ ⊔⇘f⇙ a ! q" using ‹ss!hd b = a!hd b› by auto
    with τ have "ss!q =  (hd b # ?a_hdb) ⊔⇘f⇙ a ! q" by simp
    with hd_b_cons_in_A a_q_inA have " (hd b # ?a_hdb)⊑⇘r⇙ ss!q " 
      by (auto simp add: Semilat.ub1[OF Semilat.intro, OF is_semi])
    with τ show "τ ⊑⇘r⇙ ss ! q" by auto
  qed

  have wf_dom_2: "∀p<n.
        sorted (rev (ss ! p)) ∧
        (ss ! p ≠ rev [0..<n] ⟶ (∀x∈set ( (ss ! p)). x < p)) ∧
        (ss ! p = rev [0..<n] ⟶ (∃x∈ set w. (x,p)∈ g_E G ∧ x < p)) ∧
        (p ∉ set w ⟶ stable r step ss p)"
  proof (intro strip)
    fix p
    let ?a_p = "a!p"
    let ?ss_p = "ss!p"

    assume p_lt_n: "p < n" 
    with wf_a_b have a_p_inA: "?a_p ∈ A" 
                 and sorted_a_p: "sorted (rev ?a_p)" 
                 and sta_a_p: "p ∉ set b ⟶ stable r step a p" by (auto simp add:wf_dom_def)

    from p_lt_n have "p ∈ set (g_V G)" using verts_set n_def nodes_def by auto
    then have fin_succ_p: "finite (succs p)" using fin_succs by auto

    from set_a p_lt_n have a_p_inA: "?a_p ∈ A" using ‹length a = n› by (auto simp add:A_def)
    then have "set ?a_p ⊆ set nodes" using inpow_subset_nodes by (auto simp add:A_def)
    with p_lt_n have set_p_a_p: "set (p#?a_p) ⊆ set nodes" using n_def nodes_def verts_set  by auto

    from p_lt_n len_eq have p_lt_len_a:  "p < length a" by auto
    with ss_inA  have ss_p_in_A: "ss!p ∈ A"  using len_eq len_ss_n by auto
    with p_lt_n have sorted_ss_p: "sorted (rev ?ss_p)" by (auto simp add:A_def sorted_less_sorted_list_of_set)

    have len_ss_eq_a: "length ss = length a" using  len_eq len_ss_n by auto

    have p_nin_w_eq: "p ∉ set w ⟷ (p ∉ set b ∨ p = hd b) ∧ (∀s. (p, s) ∈ set ?qs_a ⟶ s ⊔⇘f⇙ ?a_p = ?a_p)"
    proof
      assume "p ∉ set w" 
      with set_ww have p_nin1: "p ∉ {q. ∃t. (q, t) ∈ set ?qs_a∧ t ⊔⇘f⇙ a ! q ≠ a ! q}" 
                   and p_nin2: "p ∉ set (tl b)" by auto
      from p_nin1 have p_nin: "(∀s. (p, s) ∈ set ?qs_a ⟶ s ⊔⇘f⇙ ?a_p = ?a_p)" by auto
      from p_nin2 have  "p ∉ set b ∨ p = hd b" by (induct b) auto
      with p_nin show "(p ∉ set b ∨ p = hd b) ∧ (∀s. (p, s) ∈ set  ?qs_a ⟶ s ⊔⇘f⇙ ?a_p = ?a_p)" by auto
    next
      assume "(p ∉ set b ∨ p = hd b) ∧ (∀s. (p, s) ∈ set ?qs_a ⟶ s ⊔⇘f⇙ ?a_p = ?a_p)"
      then have p1: "p ∉ set b ∨ p = hd b" 
            and p2: "∀s. (p, s) ∈ set ?qs_a ⟶ s ⊔⇘f⇙ a ! p = ?a_p" by auto
      from p1 have "p ∉ set (tl b)" 
      proof
        assume "p ∉ set b" 
        then show ?thesis by(induct b) auto
      next
        assume "p = hd b" 
        with sorted_b show ?thesis by (induct b) (auto simp add:sorted_wrt_append)
      qed
      with p2 set_ww show "p ∉ set w" using set_ww by auto
    qed

    have stable_ss_p: "p ∉ set w ⟶ w ≠ Nil ⟶ stable r step ss p"
    proof (clarsimp simp add: stable_def split_paired_all)
      fix q τ
      assume p_nin_w: "p ∉ set w" and w_n_nil: "w ≠ Nil" and step_ss_p: "(q, τ) ∈ set (step p ?ss_p) "
      from p_nin_w have p_cond: "(p ∉ set b ∨ p = hd b) ∧ 
                                 (∀s. (p, s) ∈ set ?qs_a ⟶  (hd b # ?a_hdb) ⊔⇘f⇙ ?a_p = ?a_p)"
        using p_nin_w_eq  by (auto simp add:transf_def step_def exec_def)
      then have p_cond1: "(p ∉ set b ∨ p = hd b)"
            and p_cond2: "(∀s. (p, s) ∈ set ?qs_a ⟶  (hd b # ?a_hdb) ⊔⇘f⇙ ?a_p = ?a_p)"by auto

      from bounded_a pres_ss w_n_nil have " ∀(q, t)∈set ?qs_ss. q < length ss ∧ t ∈ A" by auto
      then have "∀(q, t)∈set (step (hd w) (ss ! hd w)). q < length ss ∧ (transf (hd w) (ss!hd w)) ∈ A" 
        by (auto simp add:step_def exec_def)         
      
      have ss_a_p_eq: "?ss_p = ?a_p"
      proof(cases "p ∈ succs (hd b)")
        case True note p_in_succ_hd_b = this 
        from ‹p ∈ succs (hd b)› propa_ss1' have ss_p: "?ss_p =  (hd b # ?a_hdb) ⊔⇘f⇙ ?a_p" using fin_succ_hd_b
          by (auto simp add:step_def exec_def)
        from p_in_succ_hd_b p_cond2 have " (hd b # ?a_hdb) ⊔⇘f⇙ ?a_p= ?a_p" using fin_succ_hd_b
          by (auto simp add:step_def exec_def)
        with ss_p show ?thesis by auto
      next
        case False
        then have "p ∉ {q. ∃t. (q, t) ∈ set ?qs_a}" using fin fin_succ_hd_b  by (auto simp add:step_def exec_def)
        then have "p ∉ set ( map fst ?qs_a)" by auto
        with p_lt_n show ?thesis using exec2 len_eq  by auto
      qed
      
      have "(∀(q, τ)∈set (step p ?ss_p). transf p ?ss_p ⊑⇘r⇙ ss ! q) "      
      proof(intro strip, clarsimp)
        fix succ_p z
        let ?a_succ_p = "a!succ_p"
        let ?ss_succ_p = "ss!succ_p"         

        assume "(succ_p, z)  ∈ set (step p ?ss_p)"
        then have succ_p: "succ_p ∈ succs p" using p_lt_n fin_succ_p by (auto simp add:step_def exec_def)
        with p_lt_n have succ_p_lt_n: "succ_p < n" using succ_in_verts  n_def nodes_def verts_set by auto
        with wf_a_b have a_succ_p_inA: "?a_succ_p ∈ A"  by (auto simp add:wf_dom_def)
        from succ_p_lt_n ss_in_A have ss_succ_p_inA: "?ss_succ_p ∈ A" by auto 

        have p_nin_b_ssp: "p ∉ set b ⟹ transf p ?ss_p ∈ A ∧ transf p ?ss_p ⊑⇩r ?a_succ_p"
        proof-
          assume "p ∉ set b"
          with sta_a_p have "(∀(q,τ) ∈ set (step p ?a_p). τ ⊑⇩r a!q)" by (simp add:stable_def)
          with succ_p have transf_p_succp':"transf p ?a_p ⊑⇩r ?a_succ_p" using fin_succ_p 
            by (auto simp add:stable_def step_def exec_def)
          with ss_a_p_eq have transf_lt_p: "transf p ?ss_p ⊑⇩r ?a_succ_p" by auto
          from transf_p_succp' have "(p# ?a_p) ⊑⇩r ?a_succ_p" by (auto simp add:transf_def)
          then have "sorted (rev (p#?a_p)) ∨ (p#?a_p = ?a_succ_p)" 
            by (auto simp add:step_def exec_def transf_def r_def lesssub_def lesub_def nodes_le_def)
          with set_p_a_p a_succ_p_inA
          have "(p#?a_p) ∈ (rev ∘ sorted_list_of_set) ` (Pow (set nodes))" using subset_nodes_inpow by (auto simp add:A_def)
          then have "transf p ?a_p ∈ A" using transf_def by (auto simp add:A_def transf_def)
          then show ?thesis using ss_a_p_eq transf_lt_p by auto
        qed
              
        show "transf p ?ss_p ⊑⇘r⇙ ?ss_succ_p"
        proof(cases "p ∈ succs (hd b)")
          case True note p_in_succ_hd_b = this   
          with p_cond have " (hd b # ?a_hdb) ⊔⇘f⇙ ?a_p =?a_p" using fin_succ_hd_b
            by (auto simp add:step_def exec_def)
          from p_in_succ_hd_b propa_ss1' have ss_p: "?ss_p = (hd b # ?a_hdb) ⊔⇘f⇙ ?a_p" using fin_succ_hd_b
            by (auto simp add:step_def exec_def)
          then have transf_p2: "transf p ?ss_p = (p # (inter_sorted_rev (hd b # ?a_hdb) ?a_p))" 
            by (auto simp add:f_def plussub_def nodes_sup_def transf_def )
          then show ?thesis 
          proof(cases "succ_p ∈ succs (hd b)")
            case True note succ_p_is_succ_hdb = this
            with propa_ss1 have ss_succ_p: "?ss_succ_p = (hd b # ?a_hdb) ⊔⇘f⇙ ?a_succ_p" using fin_succ_hd_b
              by (auto simp add:step_def exec_def transf_def)
            with a_succ_p_inA hd_b_cons_in_A  have succ_p1: "(hd b # ?a_hdb) ⊑⇘r⇙?ss_succ_p" 
                                               and succ_p2: "?a_succ_p⊑⇘r⇙ ?ss_succ_p "
              by (auto simp add:Semilat.ub1[OF Semilat.intro, OF is_semi]
                                Semilat.ub2[OF Semilat.intro, OF is_semi])           
            show ?thesis 
            proof(cases "p ∈ set b")
              case True note p_in_set_b = this
              then have p_eq_hdb: "p = hd b" using p_cond by auto
              with succ_p have succ_p_is_succ_hdb: "succ_p ∈ succs (hd b)" by auto
              from ss_a_p_eq p_eq_hdb have "(hd b # ?ss_hdb) = hd b # ?a_hdb" by auto
              with succ_p1 have "hd b # ss ! hd b ⊑⇘r⇙ ss ! succ_p" by auto
              with p_eq_hdb show ?thesis by (auto simp add:transf_def)             
            next 
              case False
              then have "transf p ?ss_p ∈ A" and "transf p ?ss_p ⊑⇩r ?a_succ_p" using p_nin_b_ssp by auto                       
              with succ_p2 a_succ_p_inA ss_succ_p_inA  
              show ?thesis by (auto intro: order_trans Semilat.orderI[OF Semilat.intro, OF is_semi])
            qed
          next
            case False note succ_p_n_succ_hdb = this
            with exec2 have ss_succ_p_eq_a: "?ss_succ_p = ?a_succ_p" using fin_succ_hd_b succ_p_lt_n  len_eq 
              by (auto simp add:step_def exec_def)
            show ?thesis 
            proof(cases "p ∈ set b")
              case True
              with p_cond have p_eq_hdb: "p = hd b" by auto
              with succ_p have succ_p_is_succ_hdb: "succ_p ∈ succs (hd b)" by auto
              with succ_p_n_succ_hdb show ?thesis by auto
            next 
              case False
              with sta_a_p have "∀(q,τ) ∈ set (step p ?a_p). τ ⊑⇩r a!q" by (simp add:stable_def)
              with succ_p fin_succ_p have "transf p ?a_p ⊑⇩r ?a_succ_p" 
                by (auto simp add:step_def exec_def)
              with ss_succ_p_eq_a ss_a_p_eq show ?thesis by auto
            qed
          qed
        next
          case False note p_nin_succ_hd_b = this  
          from p_nin_succ_hd_b p_cond have "p ∉ set b ∨ p = hd b" by auto
          then show ?thesis 
          proof
            assume "p ∉ set b"
            then have transf_ss_p_inA: "transf p ?ss_p ∈ A" and transf_lt_p: "transf p ?ss_p ⊑⇩r ?a_succ_p" using p_nin_b_ssp by auto  
            show "transf p ?ss_p ⊑⇘r⇙ ?ss_succ_p"
            proof(cases "succ_p ∈ succs (hd b)")
              case True
              with succ_p_lt_n propa_ss1' len_eq  fin_succ_hd_b have "?ss_succ_p = (hd b # ?a_hdb) ⊔⇘f⇙ ?a_succ_p" 
                by (auto simp add:step_def exec_def)
              with a_succ_p_inA hd_b_cons_in_A have "?a_succ_p ⊑⇩r ?ss_succ_p" 
                by (auto simp add:Semilat.ub2[OF Semilat.intro, OF is_semi])            
              with transf_lt_p transf_ss_p_inA a_succ_p_inA ss_succ_p_inA  
              show ?thesis by (auto intro: order_trans  Semilat.orderI[OF Semilat.intro, OF is_semi])              
            next
              case False
              with succ_p_lt_n exec2 len_eq  fin_succ_hd_b have "?ss_succ_p = ?a_succ_p" 
                by (auto simp add:step_def exec_def)
              with transf_lt_p show ?thesis by auto
              qed
          next
            assume "p = hd b" 
            with hd_b_ss_sta have "(∀(q,τ) ∈ set (step p ?ss_p). τ ⊑⇩r ss!q)" by (simp add:stable_def)
            with succ_p ‹p = hd b›
            show "transf p ?ss_p ⊑⇘r⇙ ?ss_succ_p" using fin_succ_hd_b
              by (auto simp add:stable_def step_def exec_def transf_def)
          qed
        qed          
      qed
      with step_ss_p show "τ ⊑⇘r⇙ ss ! q" by (auto simp add:step_def exec_def)
    qed

    show "sorted (rev ?ss_p) ∧ 
          (?ss_p ≠ rev [0..<n] ⟶ (∀x∈set?ss_p. x < p)) ∧
          (?ss_p = rev [0..<n] ⟶ (∃x∈ set w. (x,p)∈ g_E G ∧ x < p)) ∧
          (p ∉ set w ⟶ stable r step ss p)"  
    proof(cases "w ≠ []")
      case True note w_n_nil = this
      show ?thesis
      proof (cases "p ∈ set( map fst (?qs_a))")
        case True
        with propa_ss1 have ss_p: "?ss_p = (hd b # ?a_hdb) ⊔⇘f⇙ ?a_p" by (simp add:step_def exec_def transf_def)
        with sorted_hd_b_cons sorted_a_p
        have ss_p_lt_hdb: "set ?ss_p ⊆ set (hd b # ?a_hdb)" 
         and ss_p_lt: "set ?ss_p ⊆ set ?a_p" 
         and ss_p_inter: "set ?ss_p = set (hd b # ?a_hdb) ∩ set ?a_p"         
          by (auto simp add:f_def plussub_def nodes_sup_def inter_sorted_correct)
  
        from sorted_hd_b_cons sorted_a_p
        have "inter_sorted_rev (hd b # ?a_hdb) ?a_p = rev (sorted_list_of_set (set (hd b # ?a_hdb) ∩ set ?a_p))" 
          by (rule inter_sorted_correct_col)
        with ss_p have ss_p2: "?ss_p = (rev (sorted_list_of_set (set (hd b # ?a_hdb) ∩ set ?a_p)))" 
          by (auto simp add:f_def plussub_def nodes_sup_def)

        show ?thesis
        proof(cases "?a_p ≠ (rev [0..<n])")
          case True note a_p_neq_all = this
          then have seta_p_neq_all: "set ?a_p ≠ {0..<n}" using sorted_a_p  by (auto intro: sorted_less_rev_set_unique)
          from a_p_neq_all wf_a_b p_lt_n have a_lt_p: "(∀x∈set ?a_p. x < p)" using n_def len_eq  by (auto simp add:wf_dom_def)  
          with ss_p_lt have "∀x∈set ?ss_p. x < p" by auto
          then have  ss_lt_p: "?ss_p ≠ rev [0..<n] ⟶ (∀x∈set ?ss_p. x < p)" by auto
          have "set ?ss_p ≠ {0..<n}" 
          proof(rule ccontr)
            assume "¬ set ?ss_p ≠ {0..<n}"            
            with ss_p_lt have cc:  "{0..<n} ⊆ set ?a_p" by auto
            from a_in_A p_lt_len_a have " ?a_p ∈ ((rev ∘ sorted_list_of_set) ` (Pow (set nodes)))" by (auto simp add: A_def)           
            then have ass_set_in_nodes: "set ?a_p ⊆ set nodes" by (rule inpow_subset_nodes)
            then have "set ?a_p ⊆ {0..<n}" by (auto simp add:nodes_def n_def verts_set) 
            with cc have "set ?a_p = {0..<n}"  by auto
            with seta_p_neq_all show False by auto 
          qed
          then have ss_p_not_all: "?ss_p ≠ rev [0..<n]" using  sorted_ss_p by (auto intro: sorted_less_rev_set_unique)
          then have "?ss_p = rev [0..<n] ⟶  (∃x∈set w. (x,p)∈ g_E G ∧ x < p)" by auto
          with sorted_ss_p ss_lt_p stable_ss_p w_n_nil show ?thesis by fastforce
        next
          case False 
          then have a_p_all: "?a_p =  (rev [0..<n])"  by auto
          with wf_a_b p_lt_n   have ex_lt_p: " (∃x∈ set b. (x,p)∈ g_E G ∧ x < p)" by (auto simp add:wf_dom_def)
  
          have "hd b ∈ set b" using b_n_nil by auto                  
  
          from a_p_all have "set ?a_p = {0..<n}" by auto
          with ss_p_inter have "set ?ss_p ⊆ {0..<n}" by auto
          with ss_p2 hdb_subset_n ‹set ?a_p  = {0..<n}› have "(set (hd b # ?a_hdb) ∩ set ?a_p) = set (hd b # ?a_hdb)" by auto
  
          with ss_p2 have ss_p3: "?ss_p =  (rev (sorted_list_of_set (set (hd b # ?a_hdb))))" by auto
          from sorted_hd_b_cons have "sorted_list_of_set (set (hd b # ?a_hdb)) = rev (hd b # ?a_hdb)" by (fastforce dest: sorted_less_rev_set_eq)
          with ss_p3 have ss_p_4: "?ss_p = (hd b # ?a_hdb)" by auto          
           
          
          have "(?ss_p ≠ rev [0..<n] ⟶ (∀x∈set ?ss_p. x < p)) ∧
                (?ss_p = rev [0..<n] ⟶  (∃x∈ set w. (x,p)∈ g_E G ∧ x < p)) ∧
                (p ∉ set w ⟶ stable r step ss p)"
          proof(cases "?ss_p ≠  (rev [0..<n])")
            case True note ss_p_n_all = this
            with ss_p_4 show ?thesis
            proof(cases "hd b < p")
              case True
              with ss_p_4 sorted_hd_b_cons have ss_p_lt_p: "∀x∈set ( (ss ! p)). x < p" by (auto simp add:sorted_wrt_append)
              with ss_p_4 ss_p_n_all stable_ss_p ‹w ≠ []› show ?thesis by auto
            next
              case False note hd_b_ge_p = this
              from ex_lt_p obtain x where "x∈ set b " and " (x,p)∈ g_E G " and "x < p"by auto
              from ‹x ∈ set b› ‹x < p› hd_b_ge_p have "tl b ≠ []" by (induct b) auto
              with  hd_b_ge_p sorted_b have temp_t: "∀x∈ set (tl b). x ≥ p" by (induct b) auto
              with ‹¬hd b < p› have "x ∈ set (tl b)" using ‹(x,p)∈ g_E G › ‹x ∈ set b› ‹x < p› by (induct b) auto              
              with ‹x < p› temp_t have False by auto
              then  show ?thesis by auto
            qed
          next
            case False
            then have "?ss_p =  (rev [0..<n])" by auto 
            with ss_p_4 have hd_b_as1: "(hd b # ?a_hdb) = rev [0..<n]" by auto
            then have "hd (hd b # ?a_hdb) = hd (rev [0..<n])" by auto
            then have hd_b: "hd b = hd (rev [0..<n])" by auto
            have "n > 0 "using n_def nodes_def len_verts_gt0 by auto
            then have last_hd: "last [0..<n] = hd (rev [0..<n])" apply (induct n)  by auto            
            have "last[0..<n] = n - 1" using ‹n> 0› by auto
            then have "hd (rev [0..<n]) = n - 1" using last_hd by auto
            with hd_b  have hd_b_n_minus1: "hd b = n - 1" by auto
  
            show ?thesis
            proof(cases "hd b < p")
              case True
              with hd_b_n_minus1 p_lt_n  show ?thesis by arith    
            next
              case False
              from ex_lt_p obtain x where x: "x∈set b ∧ (x, p) ∈ g_E G ∧ x < p" by auto
              then have "x∈set b " and " (x, p) ∈ g_E G " and " x < p"by auto
              from x ‹¬hd b <p› have x_n_hd_b: "x ≠ hd b" by auto
              with  ‹x∈set b › have "tl b ≠ []" by (induct b) auto
              with ‹x∈set b › x_n_hd_b have "x ∈ set (tl b)"  by (induct b) auto
              with ww have "x ∈ set w" using fin by auto
              then show ?thesis using ‹ss!p =  (rev [0..<n])› ‹(x, p) ∈ g_E G› ‹x<p› stable_ss_p ‹w ≠ []› by auto
            qed
          qed
          then show ?thesis using sorted_ss_p by auto
        qed

      next
        case False note p_not_in_succ = this
        with exec2 p_lt_n len_eq have ss_a_p_eq: "ss!p = a!p" by auto
        with ass p_lt_n  wf_a_b
        have cond1: "(?ss_p ≠ rev [0..<n] ⟶ (∀x∈set ?ss_p. x < p))" 
          by (auto simp add:wf_dom_def)
  
        show ?thesis
        proof(cases "?a_p ≠  (rev [0..<n])")
          case True
  
          with wf_a_b have "(∀x∈set ?a_p. x < p)" using p_lt_n  len_eq  by (auto simp add:wf_dom_def)
          with ss_a_p_eq have "(∀x∈set ?ss_p. x < p)" by auto
          with cond1 sorted_ss_p show ?thesis using p_lt_n  len_eq stable_ss_p w_n_nil by auto
        next 
          case False
          then have "?a_p =  (rev [0..<n])" by auto
          from ss_a_p_eq ass p_lt_n  wf_a_b 
          have "?ss_p = rev [0..<n] ⟶  (∃x∈ set b. (x,p)∈ g_E G ∧ x < p)" by (auto simp add:wf_dom_def)
          with ss_a_p_eq ‹a!p =  (rev [0..<n])› have hd_b_lt_p: " (∃x∈ set b. (x,p)∈ g_E G ∧ x < p)" using len_eq  by auto
          then obtain x where "x∈ set b " and " (x,p) ∈  g_E G" and " x < p" by auto
            
                
          from fin_succ_hd_b ‹(x,p) ∈  g_E G› p_not_in_succ have "x ≠ hd b " by (auto simp add:step_def exec_def succs_def)
          with ‹x∈ set b› have "x ∈ set (tl b)" using b_n_nil by (induct b)  auto
  
          with ww have "x ∈ set w" using fin by auto
          with ‹(x,p) ∈  g_E G› and ‹ x < p› have "(∃x∈ set w. (x,p)∈ g_E G ∧ x < p)" by auto
          with cond1 sorted_ss_p show ?thesis using stable_ss_p w_n_nil by auto  
        qed
      qed
    next
      case False
      then have w_n_nil: "w =[]" by auto 
      with set_ww have "tl b = []" and succ_hd_b_eq: "∀(q, t) ∈ set ?qs_a.  t ⊔⇘f⇙ a ! q = a ! q" by auto
      
      from  succ_hd_b_eq propa have "∀p<n. ss!p = a!p"
      proof (intro strip)
        fix p
        assume ass_eq: " ∀(q, t)∈set ?qs_a. t ⊔⇘f⇙ a ! q = a ! q "
           and " propa f ?qs_a a (tl b) = (ss, w) " and p_lt_n: " p < n "
        show "ss ! p = a ! p"
        proof(cases "p ∈ succs (hd b)")
          case True
          with fin_succ_hd_b propa_ss1 have ss_p_eq: "ss!p = transf (hd b) (a!hd b)   ⊔⇘f⇙ a ! p"
            by (auto simp add:step_def exec_def)
          with ass_eq ‹p ∈ succs (hd b)› fin_succ_hd_b have "transf (hd b) (a!hd b) ⊔⇘f⇙ a ! p = a ! p" 
            by (auto simp add:step_def exec_def)
          with ss_p_eq show ?thesis by auto
        next
          case False
          with fin_succ_hd_b exec2 p_lt_n n_def len_eq nodes_def  show ?thesis
            by (auto simp add:step_def exec_def)
        qed
      qed
      then have "∀p< length ss. ss!p = a!p" using ‹length ss = n› by auto
      then have ss_eq_a: "ss = a" using n_def len_eq nodes_def ‹length ss = n› by (auto simp add:list_eq_iff_nth_eq)
      
      with wf_a_b p_lt_n have 
                              t3: "(?ss_p ≠ rev [0..<n] ⟶ (∀x∈set ?ss_p. x < p))" and 
                              t4:  "(?ss_p = rev [0..<n] ⟶ (∃x∈set b. (x, p) ∈ g_E G ∧ x < p))" and 
                              sta_temp: "(p ∉ set b ⟶  stable r step ss p)"  by (auto simp add:wf_dom_def)

      from  ‹tl b = []›  ‹b ≠ []›   have "p ∉ set b ⟷ p ≠ hd b " by (induct b) auto
      with sta_temp have "p ≠ hd b ⟶ stable r step ss p" by auto
      with hd_b_ss_sta have "stable r step ss p" by auto
      then have sta_temp': "p ∉ set w ⟶  stable r step ss p" using w_n_nil by auto

      have "?ss_p ≠ (rev [0..<n])" 
      proof(rule ccontr)
        assume "¬?ss_p ≠  (rev [0..<n])"
        then have ss_p_all: "?ss_p =  (rev [0..<n])" by simp
        with ‹ss = a› have "a!p =  (rev [0..<n])" by auto
        from ‹?ss_p =  (rev [0..<n])›
        have " ?ss_p = rev [0..<n]" by auto
        with  t4 have "(∃x∈set b. (x, p) ∈ g_E G ∧ x < p)" by auto
        then obtain x where x: "x ∈ set b ∧ (x, p) ∈ g_E G ∧ x < p" by auto 
        with ‹tl b = []›  ‹b ≠ []› have "x =hd b"  by (induct b) auto
        with x have " (hd b, p) ∈ g_E G" and hdb_lt_p: "hd b < p" by auto
        then have "p ∈ succs (hd b)" by (simp add:succs_def)
        with succ_hd_b_eq have transf_hd_b_ap: "transf (hd b) (a!hd b)  ⊔⇘f⇙ a ! p = a ! p"  using fin_succ_hd_b 
          by (auto simp add:step_def exec_def)

        have a_p_neq_all: "?a_p ≠ (rev [0..<n])" 
        proof(rule ccontr)
          assume "¬ ?a_p ≠  (rev [0..<n])" 
          then have a_p_all: "?a_p =  (rev [0..<n])" by auto
          then have "transf (hd b) ?a_hdb ⊔⇘f⇙ ?a_p =  (hd b # ?a_hdb)  ⊔⇘f⇙  (rev [0..<n])" 
            by (auto simp add:transf_def)
          then have "transf (hd b) ?a_hdb  ⊔⇘f⇙?a_p =  ( (inter_sorted_rev (hd b # ?a_hdb) (rev [0..<n])))" 
            by (auto simp add:f_def plussub_def nodes_sup_def )
          with transf_hd_b_ap a_p_all have "inter_sorted_rev (hd b # ?a_hdb) (rev [0..<n]) = 
                                              (rev [0..<n])"by auto
          then have tx: "inter_sorted_rev (hd b # ?a_hdb) (rev [0..<n]) = (rev [0..<n])" by auto
          from sorted_hd_b_cons have "set (inter_sorted_rev (hd b # ?a_hdb) (rev [0..<n])) ⊆
                                    set (hd b # ?a_hdb)" by (auto simp add: inter_sorted_correct)
          with tx have "set (rev [0..<n]) ⊆ set (hd b #  ?a_hdb)" by auto
          then have ty: "{0..<n} ⊆ set (hd b # ?a_hdb)"  by auto
         
          from hdb_subset_n ty have "{0..<n} = set (hd b # ?a_hdb)" by auto

          with sorted_hd_b_cons have tz: "hd b # ?a_hdb = rev [0..<n]" by (auto simp add:sorted_less_rev_set_unique)

          from n_def nodes_def len_verts_gt0 verts have "n > 0" by auto
          with tz have tzz: "hd b = n - 1" by (induct n)  auto
          from p_lt_n tzz hdb_lt_p show False by auto
        qed
        with  ss_p_all ss_eq_a show False  by auto
      qed
      with sta_temp' sorted_ss_p t3 show ?thesis by auto
    qed
  qed

  from ss_inA wf_dom_2 sorted_w len_ss_n w_lt_n show ?thesis by auto
qed

lemma propa_dom_invariant_aux':
  fixes a b ss w
assumes propa: "propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w) "    
    and b_n_nil: "b ≠ [] " 
    and a_in_A: "∀τ∈set a. τ ∈ A  "   
    and ass: "∀p<length ss0.
          sorted (rev ( (a ! p))) ∧
          (a ! p ≠ rev [0..<length ss0] ⟶ (∀x∈set ( (a ! p)). x < p)) ∧
          (a ! p = rev [0..<length ss0] ⟶  (∃x∈ set b. (x,p)∈ g_E G ∧ x < p)) ∧
          (p ∉ set b ⟶ stable r step a p)"
    and sorted_b: "sorted b  "
    and n_len: "n = length ss0  "
    and len_eq:  "length a = length ss0  "
    and b_lt_n: "∀x∈set b. x < length ss0  "
  shows "(∀τ∈set ss. τ ∈ A) ∧
         (∀p<length ss0.
           sorted (rev ( (ss ! p))) ∧
           (ss ! p ≠ rev [0..<length ss0] ⟶ (∀x∈set (ss ! p). x < p)) ∧
           (ss ! p = rev [0..<length ss0] ⟶  (∃x∈ set w. (x,p)∈ g_E G ∧ x < p)) ∧
           (p ∉ set w ⟶ stable r step ss p)) ∧
         sorted w ∧ length ss = length ss0 ∧ (∀x∈set w. x < length ss0) " 
  using assms 
  by (auto dest: propa_dom_invariant_aux)


lemma propa_dom_invariant: 
  assumes wf_ss_w: "wf_dom ss w "
      and w_n_nil: "w ≠ []"
      and propa: "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w') "
    shows "wf_dom ss' w'" 
  using assms 
proof-
  from wf_ss_w have ass:
    "(∀p< n. sorted (rev (ss!p)) ∧
             (ss!p ≠ rev [0..< n] ⟶ (∀x∈set (ss!p). x < p)) ∧
             (ss!p = rev [0..< n] ⟶  (∃x∈ set w. (x,p)∈ g_E G ∧ x < p)) ∧
             (p ∉ set w ⟶ stable r step ss p)) "
  and sorted_b: "sorted w"
  and a_in_A: "∀τ∈set ss. τ ∈ A" 
  and len_eq: "length ss = n"
  and b_lt_n: "(∀x∈set w. x < n)"  by (auto simp add:wf_dom_def)
  from propa w_n_nil a_in_A ass sorted_b len_eq b_lt_n 
  show ?thesis by (unfold wf_dom_def) (rule propa_dom_invariant_aux)
qed


lemma step_dom_mono_aux: 
  fixes τ p τ' a b
  assumes sorted: "sorted (rev (transf p  τ)) "
      and a_b_step: "(a, b) ∈ set (step p  τ) " 
      and "τ ∈ A " and " p < n " and " τ ⊑⇘r⇙ τ'" 
    shows "∃τ''. (a, τ'') ∈ set (step p τ') ∧ b ⊑⇘r⇙ τ''"
proof-  
  have step1: "step p τ = map (λpc. (pc, (transf  p τ))) (rev (sorted_list_of_set(succs p)))" by (simp add:step_def exec_def)
  from a_b_step have "set (step p τ) ≠ {}" by auto
  with step1 have succ_p_n_nil: "(rev (sorted_list_of_set(succs p))) ≠ []" by auto

  from ‹p<n› have "p ∈ set (g_V G)" using n_def nodes_def verts_set len_verts_gt0 by auto
  then have fin: "finite (succs p)" using fin_succs by auto
  with step1  have "∀(x,y)∈ set (step p τ). x ∈ succs p" 
               and step2: "∀(x,y)∈ set (step p τ). y = transf p τ" by (auto simp add:step_def exec_def)
  with a_b_step have "a ∈ succs p" by auto
  then have "succs p ≠ {}" by auto
  from step2 a_b_step have b:  "b = transf p τ" by auto

  have step2: "step p τ' = map (λpc. (pc, (transf  p τ'))) (rev (sorted_list_of_set(succs p)))" by (simp add:step_def exec_def)
  with fin have g1: "∀(x,y)∈ set (step p τ'). x ∈ succs p" 
                and g2: "∀(x,y)∈ set (step p τ'). y = transf p τ'" by (auto simp add:step_def exec_def)
  with ‹a ∈ succs p› have "∃t. (a,t)∈ set (step p τ')" using fin by (auto simp add:step_def exec_def)
  then obtain t where ex: "(a,t)∈ set (step p τ')" by auto 
  with g2 have t: "t = transf p τ'" by auto

  from‹ τ ⊑⇘r⇙ τ'› have g: "sorted (rev τ) ∧ sorted (rev τ')∧ set τ' ⊆ set τ ∨ τ = τ'"
    by (auto simp add:r_def lesssub_def lesub_def nodes_le_def)
  then have subset_p: "set (p#τ') ⊆ set (p# τ)" and "set  τ' ⊆ set τ" by auto
  from sorted have "∀x∈ set τ. x < p" and "sorted (rev τ')" using g by (auto simp add:sorted_wrt_append transf_def)
  with ‹set τ' ⊆ set τ› have "∀x∈ set τ'. x < p" by auto
  with ‹sorted (rev τ')› have "sorted (rev (p#τ'))" by (auto simp add:sorted_wrt_append)
  with sorted b t subset_p

  have "b ⊑⇘r⇙ t" by (auto simp add:r_def lesssub_def lesub_def nodes_le_def transf_def)
  with ex show ?thesis by auto
qed

lemma step_dom_mono: 
"(∀τ p τ'. τ ∈ A ∧ p<n ∧ τ ⊑⇩r τ' ⟶ 
           sorted (rev (transf p τ)) ⟶ 
           set (step p τ) {⊑⇘r⇙} set (step p τ'))"
  apply(unfold mono_def lesubstep_type_def)
  by(auto simp add:step_dom_mono_aux n_def nodes_def transf_def)


lemma propa_termination: 
  fixes a b
  assumes wf_a_b: "wf_dom a b" 
      and b_n_nil: "b ≠ [] "
    shows "(propa f (step (hd b) (a ! hd b)) a (tl b), a, b) ∈
           {(ss', ss). ss [⊏⇘r⇙] ss'} <*lex*> 
           (λx. case x of (x, y) ⇒ (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset"
proof-
  let ?qs = "(step (hd b) (a ! hd b))"
  from wf_a_b have "∀x∈set b. x < n" and n_len: "length a = n"  and sorted_b: "sorted b" 
               and set_a: "set a ⊆ A" by (auto simp add:wf_dom_def)
  then have sorted_tl_b: "sorted (tl b)" and hd_b_lt_n: "hd b < n" using b_n_nil by (induct b) (auto simp add:sorted_wrt_append)
  from set_a have a_inA: "a ∈ nlists n A" using n_len by (auto intro: nlistsI)

  from hd_b_lt_n have dist: "distinct (map fst ?qs)" using distinct_p  by auto   

  from wf_a_b b_n_nil have step_pres_bounded: "∀(q, τ)∈set ?qs. q < n ∧ τ ∈ A"
    using propa_dom_invariant_auxi n_len by fastforce  
  with sorted_tl_b set_a n_len
  have propa: "propa f ?qs a (tl b) = (merges f ?qs a, (sorted_list_of_set ({q. ∃t.(q,t)∈set ?qs ∧ t ⊔⇘f⇙ (a!q) ≠ a!q} ∪ set(tl b))))" 
    by (auto dest: decomp_propa)
  
  from a_inA step_pres_bounded sorted_b b_n_nil  dist
  have "((merges f ?qs a, (sorted_list_of_set ({q. ∃t.(q,t)∈set ?qs ∧ t ⊔⇘f⇙ (a!q) ≠ a!q} ∪ set(tl b)))),(a,b)) ∈
        {(ss', ss). ss [⊏⇘r⇙] ss'} <*lex*> (λx. case x of (x, y) ⇒ (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset"
    by (auto simp add: finite_psubset_def dest: termination_lemma)      
  with propa show ?thesis by auto
qed   

lemma iter_dom_invariant: 
  assumes "wf_dom ss0 w0"
    shows "iter f step ss0 w0 = (ss',w') ⟶ wf_dom ss' w'" 
  using assms
  apply (unfold iter_def)
  apply(rule_tac  
      P = "(λ(ss, w). wf_dom ss w )" and
      r = "{(ss',ss). ss [⊏⇩r] ss'} <*lex*> (λ(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset" 
      in while_rule) 
  ― ‹Invariant holds initially:›
      apply (clarsimp)

  ― ‹Invariant is preserved:›
     apply(simp add: wf_dom_def)
     apply clarsimp  
     apply(rule propa_dom_invariant_aux')
            apply assumption+
  ― ‹Postcondition holds upon termination:›
    apply clarsimp 

  ― ‹Well-foundedness of the termination relation:›
   apply (simp add: wf_listn_termination_rel) 

  ― ‹Loop decreases along termination relation:›
   apply clarsimp
   apply (fastforce intro:propa_termination)
  done

lemma propa_dom_invariant_aux2: 
  fixes ss w ssa wa
  assumes wf_dom_ss0_w0: "wf_dom ss0 w0"
      and w_n_nil: "w ≠ [] "     
      and propa: "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa) "
      and wf_ss_w: "wf_dom ss w "
      and ss0_lt_ss: "ss0 [⊑⇘r⇙] ss"
      and sta: " ∀ts∈nlists n A. ss0 [⊑⇘r⇙] ts ∧ (∀p<n. stable r step ts p) ⟶ ss [⊑⇘r⇙] ts"    
    shows "ss0 [⊑⇘r⇙] ssa ∧ 
           (∀ts∈nlists n A. ss0 [⊑⇘r⇙] ts ∧ (∀p<n. stable r step ts p) ⟶ ssa [⊑⇘r⇙] ts)"
  using assms
proof-
  let ?ss_hdw = "ss!hd w"
  from wf_dom_ss0_w0 have len_ss0: "length ss0 = n" and "∀x∈ set ss0. x ∈ A" by (auto simp add:wf_dom_def)
  then have ss0_inA:  "ss0 ∈ nlists n A"  and set_ss0: "set ss0 ⊆ A"by (auto intro:nlistsI)
  then have ss0_nth_inA: "∀i<length ss0. ss0!i ∈ A" by auto
  then have ss0_p_subset: "∀p< length ss0. set (ss0!p) ⊆ set nodes" by (auto simp add:inpow_subset_nodes A_def)

  from len_ss0 n_def nodes_def len_verts_gt0 have "0 < length ss0" by auto

  from ss0_lt_ss have "list_all2 (λx y. x ⊑⇩r y) ss0 ss" 
    by (auto simp add:lesssub_def lesub_def list_all2_def Listn.le_def)
  then have lt1: "∀p<length ss0. ss0 !p ⊑⇘r⇙ ss!p" by (auto simp add: list_all2_conv_all_nth) 

  from wf_ss_w have  "∀τ∈set ss. τ ∈ A" 
                and ass1: "∀p<n. sorted (rev ( (ss ! p))) ∧
                                (ss!p ≠ rev [0..<n] ⟶ (∀x∈set (ss ! p). x < p)) ∧
                                (ss!p = rev [0..<n] ⟶  (∃x∈ set w. (x,p)∈ g_E G ∧ x < p)) ∧
                                (p ∉ set w ⟶ stable r step ss p)" 
                and sorted_w: "sorted w" 
                and len_ss: "length ss = n" 
                and w_lt_n: "∀x∈set w. x < n  "by (auto simp add:wf_dom_def)
  then have ss_inA: "ss ∈ nlists n A" and set_ss: "set ss ⊆ A" by (auto intro:nlistsI)
  then have ss_nth_inA: "∀i<length ss. ss!i ∈ A"  by auto
  then have ss_p_subset: "∀p< length ss. set (ss!p) ⊆ set nodes" by (auto simp add:inpow_subset_nodes A_def)
  then have ss_hdw_nodes: "set ?ss_hdw ⊆ set nodes" using w_lt_n w_n_nil len_ss by auto

  let ?qs = "step (hd w) ?ss_hdw"
  from w_lt_n have hd_w_lt_n: "hd w < n" using w_n_nil by auto
  then  have dist: "distinct (map fst ?qs)" using distinct_p by auto

  from ss_nth_inA have ss_hdw_inA: "?ss_hdw ∈ A" using w_lt_n w_n_nil len_ss by auto
  from ass1 have sorted_ss_hdw: "sorted (rev ?ss_hdw)" using w_lt_n w_n_nil  by auto
  
  then have "∀q∈succs (hd w). q ∈ set (g_V G)" by (auto simp add:succ_in_G)
  then have hd_w_suc_lt_n: "∀q∈succs (hd w). q < n" using n_def verts_set nodes_def by auto

  have hdw_in_nodes:"hd w ∈ set (g_V G)" using verts_set n_def nodes_def w_lt_n w_n_nil by auto
  then have fin_succ_hd_w: "finite (succs (hd w))" using fin_succs by auto

  from sorted_w have sorted_tl_w': "sorted (tl w)" using w_n_nil by (induct w) auto
  from wf_ss_w w_n_nil have ss_hd_w_neq_all: "?ss_hdw ≠ (rev [0..<n])" 
                        and sorted_hd_w_ss: "sorted (rev (hd w # ?ss_hdw))"
                        and hdb_subset_nodes: "set (hd w # ?ss_hdw) ⊆ set nodes"
                        and hd_w_ss_in_A: " (hd w # ?ss_hdw) ∈ A" 
                        and step_pres_bounded: " ∀(q, τ)∈set (step (hd w) ?ss_hdw). q < length ss ∧ τ ∈ A" 
    using propa_dom_invariant_auxi by auto
  from ss_hd_w_neq_all have ss_lt_hd_w: "∀x∈set ?ss_hdw. x < hd w" using hd_w_lt_n wf_ss_w by (auto simp add:wf_dom_def)

  from wf_ss_w w_n_nil propa have wf_ssa_wa: "wf_dom ssa wa" using propa_dom_invariant by auto
  then have sorted_ssa_p: "∀p<n. sorted (rev (ssa!p))" 
        and len_ssa: "length ssa = n" 
        and "∀x∈ set ssa. x ∈ A" 
        and sorted_wa: "sorted wa" 
        and len_ssa: "length ssa = n" 
        and wa_lt_n: "∀x∈ set wa. x < n" 
    by (auto simp add:wf_dom_def)
  then have ssa_inA: "ssa∈ nlists n A" and set_ssa: "set ssa ⊆ A"by (auto intro:nlistsI)
  then have ssa_nth_inA: "∀i<length ssa. ssa!i ∈ A" by auto
  then have ssa_p_subset: "∀p< length ssa. set (ssa!p) ⊆ set nodes" by (auto simp add:inpow_subset_nodes A_def)

  from len_ss0 len_ssa have len_ss0_ssa: "length ss0 = length ssa" by simp
  from len_ss0 len_ss  have len_ss0_ss:  "length ss0 = length ss" by simp  
  have "∀(q, τ)∈set ?qs. τ = transf (hd w) (ss!(hd w))" by (simp add:step_def exec_def)
  then have transf_ss_hd_w: "∀(q, τ)∈set ?qs. τ =  (hd w # ?ss_hdw)" 
    by (simp add:transf_def) 
  from set_ss step_pres_bounded sorted_tl_w' len_ss dist have "∀(q, τ) ∈ set ?qs. (fst(propa f ?qs ss (tl w)))!q = τ ⊔⇘f⇙ss!q" 
    by (auto dest:propa_property1)
  with propa have propa_ss: "∀(q, τ) ∈ set ?qs. ssa!q = τ ⊔⇘f⇙ss!q" by simp  
  with transf_ss_hd_w have propa_ss1:  "∀(q, τ) ∈ set ?qs. ssa!q =  (hd w # ?ss_hdw) ⊔⇘f⇙ss!q" by auto

  from ss_nth_inA step_pres_bounded have "∀(q, τ) ∈ set ?qs. ss!q ∈ A" using hd_w_suc_lt_n fin_succ_hd_w
    by (auto simp add:step_def exec_def)
  from hd_w_ss_in_A this propa_ss1 have ss_lt_ssa_q: "∀(q, τ) ∈ set ?qs. ss!q ⊑⇘r⇙ ssa!q" 
    by (fastforce dest:Semilat.ub2[OF Semilat.intro, OF is_semi])
  
  from step_pres_bounded sorted_tl_w' set_ss len_ss dist
  have  "⋀q. q ∉ set(map fst ?qs) ⟹ q < length ss ⟹ (fst(propa f ?qs ss (tl w)))!q = ss!q"     
    by (auto intro:propa_property2)
  with propa have exec2: "⋀q. q ∉ set(map fst ?qs) ⟹ q < length ss ⟹ ssa!q = ss!q" by auto
 
  have tran_ss_ssa: "∀p<length ss. ss!p ⊑⇘r⇙ ssa!p" 
  proof(intro strip)
    fix p 
    assume "p < length ss" 
    with ssa_nth_inA have ssa_p_inA: "ssa!p ∈ A" using ‹length ssa = n› ‹length ss = n› by auto
    from ss_nth_inA have ss_p_inA: "ss!p ∈ A" using  ‹length ss = n› ‹p < length ss› by auto
    
    show " ss ! p ⊑⇘r⇙ ssa ! p" 
    proof(cases "p ∈ succs (hd w)")
      case True
      then show "ss!p ⊑⇘r⇙  ssa!p" using ss_lt_ssa_q using fin_succ_hd_w by (auto simp add:step_def exec_def)
     next
       case False
       then have "p ∉ set (map fst ?qs)" using fin_succ_hd_w by (auto simp add:step_def exec_def)
       then show ?thesis using exec2 ‹p < length ss› using ssa_p_inA ss_p_inA 
         by(auto simp add:step_def exec_def intro: Semilat.orderI[OF Semilat.intro, OF is_semi])
    qed
  qed
  then have "∀p<length ss0. ss ! p ⊑⇘r⇙ ssa ! p" using len_ss0_ss by auto
  with lt1  have "∀p<length ss0. ss0!p ⊑⇘r⇙ ssa!p" using ss0_nth_inA ssa_nth_inA  ss_nth_inA  using len_ss0_ss len_ss0_ssa 
    by (auto intro: order_trans Semilat.orderI[OF Semilat.intro, OF is_semi])
  with len_ss0_ssa
  have g1: "ss0 [⊑⇘r⇙] ssa" by (auto simp only:Listn.le_def lesssub_def lesub_def intro:list_all2_all_nthI)

  have "(∀ts∈nlists n A. ss0 [⊑⇘r⇙] ts ∧ (∀p<n. stable r step ts p) ⟶ ssa [⊑⇘r⇙] ts)" 
  proof(intro strip)
    fix ts     
    assume ts_inA: "ts ∈ nlists n A" and ass: "ss0 [⊑⇘r⇙] ts ∧ (∀p<n. stable r step ts p)" 
    let ?ts_hdw = "ts!(hd w)" 

    from ts_inA sta ass have ss_ts: "ss [⊑⇘r⇙] ts" and sta_ts: "(∀p<n. stable r step ts p)" by auto 
    then have len_ss_ts: "length ss = length ts" and 
              ss_ts_hdw: "?ss_hdw ⊑⇘r⇙ ?ts_hdw "using le_listD len_ss hd_w_lt_n by auto 
    then have "sorted (rev (?ts_hdw)) ∧ set ?ts_hdw ⊆ set ?ss_hdw ∨ ?ss_hdw =?ts_hdw "
      by (auto simp add:r_def lesssub_def lesub_def  nodes_le_def)
    then have sorted_ts_hdw: "sorted (rev (?ts_hdw))" 
          and ts_ss_subset: "set ?ts_hdw ⊆ set ?ss_hdw" using sorted_ss_hdw
      by (auto simp add:r_def lesssub_def lesub_def  nodes_le_def)
    then have "∀x∈ set ?ts_hdw. x < hd w" using ss_lt_hd_w by auto
    with sorted_ts_hdw have sorted_hd_w_ts: "sorted (rev (hd w # ?ts_hdw))" 
      by (auto simp add:sorted_wrt_append)
    with sorted_hd_w_ss ts_ss_subset 
    have "(hd w # ?ss_hdw) ⊑⇘r⇙ (hd w # ?ts_hdw)" 
      by (auto simp add:transf_def lesssub_def lesub_def r_def  nodes_le_def)  
    then have transf_ss_ts: "transf (hd w) ?ss_hdw ⊑⇘r⇙ transf (hd w) ?ts_hdw" by (auto simp add:transf_def)

    from sta_ts hd_w_lt_n have sta_ts_hdw: "stable r step ts (hd w)" by auto

    from ss_hdw_nodes ts_ss_subset have "set ?ts_hdw ⊆ set nodes" by auto
    with hd_w_lt_n have hdw_ts_subset_nodes: "set (hd w # ?ts_hdw) ⊆ set nodes" using nodes_def n_def verts_set by auto
    with sorted_hd_w_ts have "(hd w # ?ts_hdw) ∈ ( (rev ∘ sorted_list_of_set) ` (Pow (set nodes)))"
      by (fastforce intro: subset_nodes_inpow)
    then have transf_ts_inA: "(hd w #?ts_hdw) ∈ A" by (simp add:A_def)
    then have sorted_hdw_ts_hdw:  "sorted (rev (hd w # ?ts_hdw))" by (rule inA_is_sorted)   

    have "∀p<length ssa. ssa!p ⊑⇘r⇙ ts!p" 
    proof(intro strip)
      fix p 
      assume p_lt_len_ssa: "p < length ssa"
      then have "p < length ss" and "p < n" using len_ssa len_ss by auto
      with ss_ts have ss_ts_p: "ss!p ⊑⇘r⇙ ts!p " using le_listD by auto  

      show "ssa ! p ⊑⇘r⇙ ts ! p" 
      proof(cases "p ∈ succs (hd w)")
        case True note p_in_succs_hdw = this
        then have "ss!p ⊑⇘r⇙ ssa!p" using ss_lt_ssa_q using fin_succ_hd_w by (auto simp add:step_def exec_def)

        from p_in_succs_hdw have ssa_p: "ssa!p = transf (hd w) (ss!hd w) ⊔⇘f⇙ss!p" using propa_ss fin_succ_hd_w 
          by (auto simp add:step_def exec_def)        

        from sta_ts_hdw have transf_hdw_ts_hdw: "transf (hd w) (ts!hd w) ⊑⇘r⇙ ts!p" using p_in_succs_hdw fin_succ_hd_w
          by (auto simp add:step_def exec_def stable_def)
        then have ts_p_subset: "(hd w # ?ts_hdw) ⊑⇘r⇙ ts!p" by (auto simp add:transf_def)
        then have "(sorted (rev (ts!p)) ∧ set (ts!p)⊆ set (hd w # ?ts_hdw)∧ sorted (rev (hd w # ?ts_hdw))) ∨ 
                   hd w # ?ts_hdw = ts!p"
          by (auto simp add:r_def lesssub_def lesub_def nodes_le_def)
        then have "sorted (rev (ts!p)) ∧ set (ts!p)⊆ set (hd w # ?ts_hdw)"
        proof
          assume "sorted (rev (ts ! p)) ∧ set (ts ! p) ⊆ set (hd w # ts ! hd w) ∧ sorted (rev (hd w # ts ! hd w))" 
          then show ?thesis by auto
        next
          assume " hd w # ts ! hd w = ts ! p"
          with sorted_hdw_ts_hdw show ?thesis by auto
        qed

        then have sorted_ts_p: "sorted (rev (ts!p))" 
              and ts_as_subset: "set (ts!p)⊆ set (hd w # ?ts_hdw)"
          by auto
        with hdw_ts_subset_nodes have "set (ts!p) ⊆ set nodes" by auto
        with sorted_ts_p have "(ts!p) ∈ ( (rev ∘ sorted_list_of_set) ` (Pow (set nodes)))" 
          by (fastforce intro: subset_nodes_inpow)
        then have ts_p_inA: "ts!p ∈ A" by (simp add:A_def)

        from sorted_hdw_ts_hdw have "∀x∈ set ?ts_hdw. x < hd w" by (auto simp add:sorted_wrt_append)
        with ‹hd w < n› have "∀x∈ set ?ts_hdw. x < n" by auto
        then have "set(hd w # ?ts_hdw) ⊆ set nodes"using ‹hd w < n› n_def verts_set nodes_def  by auto
        with sorted_hdw_ts_hdw have "hd w # ?ts_hdw  ∈ ( (rev ∘ sorted_list_of_set) ` (Pow (set nodes)))" 
          by (fastforce intro: subset_nodes_inpow)
        then have "(hd w # ?ts_hdw) ∈ A" by (auto simp add:A_def)
        then have trans_hdw_ts_inA: "transf (hd w) (ts!hd w) ∈ A"  by (auto simp add:transf_def)

        have transf_hdw_ss_inA: "transf (hd w) ?ss_hdw ∈ A" using hd_w_ss_in_A  by (auto simp add:transf_def)
        have ss_p_inA: "ss!p ∈ A" using ‹p<length ss› ss_inA by auto
        from transf_ss_ts  transf_hdw_ts_hdw transf_hdw_ss_inA trans_hdw_ts_inA  ts_p_inA  have "transf (hd w) ?ss_hdw ⊑⇘r⇙ ts ! p" 
         by (auto intro: order_trans  Semilat.orderI[OF Semilat.intro, OF is_semi])          
        with ‹ss!p ⊑⇘r⇙ ts ! p› trans_hdw_ts_inA ss_p_inA transf_hdw_ss_inA ssa_p ts_p_inA
        show "ssa ! p ⊑⇘r⇙ ts ! p" by (auto intro: Semilat.lub[OF Semilat.intro, OF is_semi])
      next
        case False
        then have "p ∉ set (map fst ?qs)" using fin_succ_hd_w by (auto simp add:step_def exec_def)
        then have "ssa!p = ss!p"using exec2 p_lt_len_ssa len_ss len_ssa
          by(auto simp add:step_def exec_def)    
        with ss_ts_p show ?thesis by auto
      qed
    qed
    with ‹length ss = length ts› len_ss len_ssa
    show "ssa [⊑⇘r⇙] ts" by (auto simp only:Listn.le_def lesssub_def lesub_def intro:list_all2_all_nthI)
  qed
  with g1 show ?thesis by auto
qed

lemma in_list_nA_refl: "ss ∈ nlists n A  ⟹  ss [⊑⇘r⇙] ss"
  apply (unfold Listn.le_def lesssub_def lesub_def)
proof-
  assume "ss ∈ nlists n A"
  then have "set ss ⊆ A" and "length ss = n" by auto
  then have "∀i<n. ss!i ∈ A" by auto
  then have "∀i<length ss. ss!i ⊑⇘r⇙ ss!i" 
    by (auto simp add:r_def lesssub_def lesub_def nodes_le_def ) 
  then show " list_all2 r ss ss" by (auto simp add:lesssub_def lesub_def intro: list_all2_all_nthI)
qed

lemma iter_dom: 
 assumes "wf_dom ss0 w0"
 shows "iter f step ss0 w0 = (ss',w') ⟶ 
        wf_dom ss' w' ∧ 
        stables r step ss' ∧ 
        ss0 [⊑⇩r] ss' ∧
        (∀ts∈nlists n A. ss0 [⊑⇩r] ts ∧ stables r step ts ⟶ ss' [⊑⇩r] ts)"
  using assms
  apply (unfold iter_def stables_def)
  apply (rule_tac P = "λ(ss,w). wf_dom ss w ∧ ss0 [⊑⇩r] ss ∧ (∀ts∈nlists n A. ss0 [⊑⇩r] ts ∧ stables r step ts ⟶ ss [⊑⇩r] ts)" 
              and r =  "{(ss',ss). ss [⊏⇩r] ss'} <*lex*> (λ(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset"  
         in while_rule)

  ― ‹Invariant holds initially:›
      apply(fastforce simp add: wf_dom_def intro:wf_dom_le)
  
  ― ‹Invariant is preserved:›
     apply clarsimp
     apply (rule conjI)
      apply(fastforce dest:propa_dom_invariant)
     apply(simp add:stables_def)
     apply (rule propa_dom_invariant_aux2)
          apply assumption+

  ― ‹Postcondition holds upon termination:›
    apply(clarsimp simp add: stables_def split_paired_all)
    apply(subgoal_tac "length ss0 = n")
     apply(simp add:wf_dom_def)+

  ― ‹Well-foundedness of the termination relation:›
   apply clarsimp 
   apply(simp add:wf_listn_termination_rel)

  ― ‹Loop decreases along termination relation:›
  apply clarsimp
  apply (fastforce intro:propa_termination) 
  done   

lemma wf_start: "wf_dom start (unstables r step start)" 
proof-
  let ?w0 = "unstables r step start" 
  have sorted_w: "sorted ?w0" using unstables_def  by (simp add:sorted_less_sorted_list_of_set)
  have w0_lt_n: "∀x∈set ?w0. x < n" using unstables_def len_start_is_n by auto 
 
  have neq_all: "∀p < n. start!p ≠ rev [0..< n] ⟶ (∀x∈set (start!p). x < p) " 
  proof(intro strip)
    fix p x
    assume p_lt_n: "p < n" and p_neq_all: "start ! p ≠ rev [0..< n]" and x_in: "x ∈ set (start ! p)"
    then have "p = 0" using start_nth_lt0_all len_start_is_n by auto
    with start_nth0_empty show "x < p" using x_in by auto
  qed
 
  have eq_all:"(∀p < n. start!p = rev [0..< n] ⟶ (∃x∈ set ?w0. (x,p)∈ g_E G ∧ x < p))"
  proof(intro strip)
    fix p
    assume p_lt_n: "p < n" and p_eq_all: "start ! p = rev [0..< n]" 
    from ‹p < n› have "p = 0 ∨ p > 0 ∧ p < length start" using len_start_is_n by auto
    with p_eq_all have "p > 0" and p_lt_len_start: "p < length start" using start_nth0_empty n_def nodes_def len_verts_gt0 by auto
    then have "p ∈ set (g_V G) - {0}" using len_start_is_n n_def nodes_def verts_set by auto 
    with dfst obtain prev where "(prev, p) ∈ g_E G" and "prev < p" by auto
    then have "succs prev ≠ {}" and "prev < length start" using p_lt_len_start by (auto simp add:succs_def)  
    with unstable_start  have "prev ∈ set ?w0" by auto
    with ‹(prev, p) ∈ g_E G› ‹prev < p›
    show "∃x∈set (unstables r step start). (x, p) ∈ g_E G ∧ x < p"  by auto     
  qed

  have "∀p<n. (p ∉ set (unstables r step start)⟶ stable r step start p)"
    by (unfold unstables_def) (simp add:n_def start_def nodes_def)
  with sorted_start_nth neq_all eq_all start_subset_A sorted_w len_start_is_n w0_lt_n show ?thesis by (auto simp only:wf_dom_def) 
qed

lemma iter_dom_properties:
 "iter f step start (unstables r step start) = (ss',w') ⟶ 
  wf_dom ss' w' ∧ 
  stables r step ss' ∧ 
  start [⊑⇩r] ss' ∧
  (∀ts∈nlists n A. start [⊑⇩r] ts ∧ stables r step ts ⟶ ss' [⊑⇩r] ts)"
  using iter_dom[OF wf_start] by auto

lemma iter_dom_properties2:
 "iter f step start (unstables r step start) = (ss',w') ⟶ ss' ∈ nlists n A"
  using iter_dom_properties by (auto simp only:wf_dom_def nlists_def)

lemma iter_dom_termination: 
  "iter f step start (unstables r step start) = (ss,w) ⟶ 
   w ≠ [] ⟶
   propa f (step (hd w) (ss!(hd w))) ss (tl w) = (ss, tl w)"
proof (intro strip)
  assume iter: "iter f step start (unstables r step start) = (ss, w)" and w_n_nil: "w ≠ []"
  with iter_dom_properties 
  have stas: "stables r step ss" 
   and wf_ss_w: "wf_dom ss w" 
   and start_le_ss: "start [⊑⇩r] ss" by auto
  from stas have sta_p: "(∀p < size ss. stable r step ss p)"by (auto simp add:stables_def)

  from wf_ss_w have n_w_sta:  "∀p<n. p ∉set w ⟶  stable r step ss p" 
                      and len_eq: "length ss = n" 
                      and w_lt_n: "∀x∈ set w. x < n" 
                      and ss_inA: "∀x∈set ss. x ∈  A" 
                      and sorted_w: "sorted w "  by (auto simp add:wf_dom_def)
  from w_lt_n have hd_w_lt_n: "hd w < n" using w_n_nil by auto 
  then have hd_w_in_verts: "hd w ∈ set (g_V G)" using n_def nodes_def verts_set by auto
  then have fin_succ_hd_w: "finite (succs (hd w))" using fin_succs hd_w_in_verts by auto  

  let ?ss_hdw = "ss!hd w"
  let ?qs = "step (hd w) ?ss_hdw"  

  from hd_w_lt_n have dist: "distinct (map fst ?qs)" using distinct_p by auto

  from wf_ss_w w_n_nil have hdw_ss_subset_nodes: "set (hd w # ?ss_hdw) ⊆ set nodes"
                        and sorted_hd_w_ss: "sorted (rev (hd w # ?ss_hdw))" 
                        and hd_w_ss_in_A: " ((hd w # ?ss_hdw)) ∈ A"
                        and step_pres_bounded: "∀(q, τ)∈set ?qs. q < length ss ∧ τ ∈ A"
    using propa_dom_invariant_auxi by auto  

  let ?res = "propa f (step (hd w) (ss!(hd w))) ss (tl w) "
  have "propa f (step (hd w) (ss!(hd w))) ss (tl w) = ?res" by simp
  then obtain ss' w' where propa: "propa f (step (hd w) (ss!(hd w))) ss (tl w) = (ss', w')" by (cases ?res) auto

  from sorted_w have sorted_tl_b: "sorted (tl w)" by (induct w) auto
  from ss_inA have set_a: "set ss ⊆ A" by auto
  with step_pres_bounded sorted_tl_b len_eq dist have "∀(q, τ) ∈ set ?qs. (fst(propa f ?qs ss (tl w)))!q = τ ⊔⇘f⇙ss!q" 
    by (auto dest:propa_property1)
  with propa have propa_ss1:  "∀(q, τ) ∈ set ?qs. ss'!q =  (hd w # ?ss_hdw) ⊔⇘f⇙ss!q" by (simp add:step_def exec_def transf_def)

  from step_pres_bounded sorted_tl_b set_a  len_eq dist
  have  "⋀q. q ∉ set(map fst ?qs) ⟹ q < length ss ⟹ (fst(propa f ?qs ss (tl w)))!q = ss!q" 
    by (auto intro:propa_property2)
  with propa have g2: "⋀q. q ∉ set(map fst ?qs) ⟹ q < length ss ⟹ ss'!q = ss!q" by auto

  from sorted_w have sorted_tl_w: "sorted (tl w)" by (induct w)  auto
  with step_pres_bounded set_a 
  have fst_propa: "fst (propa f ?qs ss (tl w)) = (merges f ?qs ss)"   
   and snd_propa: "snd (propa f ?qs ss (tl w)) = (sorted_list_of_set ({q. ∃t.(q,t)∈set ?qs ∧ t ⊔⇘f⇙ (ss!q) ≠ ss!q} ∪ set (tl w)))"
    using decomp_propa by auto
  with propa have len_ss_eq_ss': "length ss' = length ss" using length_merges by auto

  have ss_ss'_eq:  "∀i<n. (fst (propa f ?qs ss (tl w)))!i = ss!i"
  proof(intro strip)
    fix i 
    assume "i < n" 
    then have i_lt_len_ss: "i < length ss" using ‹length ss = n› by auto
    show "fst (propa f ?qs ss (tl w)) ! i = ss ! i "
    proof(cases "i ∈ set(map fst ?qs)")
      case True
      assume ass1: "i ∈ set (map fst ?qs)" 
      with propa_ss1 have ss': "ss'!i = (hd w # ?ss_hdw) ⊔⇘f⇙ss!i" by (auto simp add: step_def exec_def)    
      from ass1 have "i ∈ set (g_V G)" using succ_in_G fin_succ_hd_w by (auto simp add:step_def exec_def)
      then have q_lt_len_ss: "i < length ss" using len_eq by (auto simp add:n_def nodes_def verts_set)      
      from hd_w_lt_n len_eq stas have "stable r step ss (hd w)" by (auto simp add:stables_def)
      with ass1 have "(hd w # ?ss_hdw) ⊑⇩r ss!i" by (auto simp add:stables_def stable_def step_def exec_def transf_def)
      then have "set (ss!i) ⊆ set (hd w # ?ss_hdw) ∨ (hd w # ?ss_hdw) = ss!i" by (auto simp add:lesssub_def lesub_def r_def nodes_le_def)
      then have set_ss_q_subst_hdw_ss: "set (ss!i) ⊆ set (hd w # ?ss_hdw)" by (rule disjE)(auto simp add:lesssub_def lesub_def r_def nodes_le_def)
      then have ss_q: "set (ss!i) ∩ set (hd w # ?ss_hdw) = set (ss!i)" by auto
      from wf_ss_w q_lt_len_ss have sorted_ss_q: "sorted (rev (ss!i))" by (simp add:wf_dom_def)
      with sorted_hd_w_ss have ss_q': "set (ss'!i) = set (ss!i) ∩ set (hd w # ?ss_hdw)" 
                           and sorrted_ss_q': "sorted (rev (ss'!i))" using ss'
        by (auto simp add:plussub_def f_def nodes_sup_def inter_sorted_correct) 
      with ss_q sorted_ss_q sorrted_ss_q' show ?thesis using sorted_less_rev_set_unique propa by auto   
    next
      case False note i_nin = this
      from step_pres_bounded sorted_tl_b set_a len_eq dist propa i_lt_len_ss i_nin 
      show ?thesis by (fastforce dest:propa_property2)
    qed
  qed
  with len_ss_eq_ss' have eq_ss: "ss' = ss" using len_eq propa by (auto simp add:list_eq_iff_nth_eq)
  then have qs_empty: "(({q. ∃t.(q,t)∈set ?qs ∧ t ⊔⇘f⇙ (ss!q) ≠ ss!q} ∪ set (tl w))) =  (set (tl w))" 
   using propa_ss1 propa transf_def step_def exec_def by fastforce
  with snd_propa have "snd (propa f ?qs ss (tl w)) = sorted_list_of_set (set (tl w))" using sorted_w by auto
  with sorted_tl_w have "snd (propa f ?qs ss (tl w)) = tl w" by (fastforce dest:sorted_less_set_eq)
  with propa have "w' = tl w" by simp
  with eq_ss show "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)" using propa by auto
qed
  
lemma dom_iter_properties: 
  "iter f step start (unstables r step start) = (ss, w) ⟶ 
   ss!0 = [] ∧ 
   (∀p<n. p ≠ 0 ⟶ ss!p ≠ (rev [0..<n]))"
proof(intro strip)
  assume iter: "iter f step start (unstables r step start) = (ss, w)"
  with iter_dom_properties iter_dom_properties2
  have "wf_dom ss w" 
   and stas: "stables r step ss" 
   and start_le_ss: "start [⊑⇩r] ss" 
   and ss_inA: "ss ∈ nlists n A" by auto
  then have len_ss_n: "length ss = n" by (auto simp only:nlists_def)

  from start_le_ss have "start!0 ⊑⇩r ss!0" using start_len_gt_0
    by (unfold Listn.le_def lesssub_def lesub_def) (auto simp add:lesssub_def lesub_def intro:list_all2_nthD)
  then have ss_0th: "ss!0 = []" by (auto simp add:r_def nodes_le_def lesssub_def lesub_def start_def)
 
  have "(∀p<n. p ≠ 0 ⟶ ss ! p ≠  (rev [0..<n]))"  
  proof(intro strip, rule ccontr)
    fix p
    assume p_lt_n: "p < n" and p_neq_0: "p≠0" and ss_p_eq_all: "¬ ss ! p ≠ rev [0..<n]"
    with stas len_ss_n  have step_sta: "∀(q,τ) ∈ set (step p (ss!p)). τ ⊑⇩r ss!q" by (simp add: stables_def stable_def)
    from p_lt_n len_start_is_n verts_set have p_is_vert: "p ∈ set (g_V G)" by (auto simp add:n_def nodes_def)
    then have step_p: "∀(q,τ) ∈ set (step p (ss!p)). q ∈ succs p" using fin_succs by (auto simp add:step_def exec_def)

    from p_is_vert p_neq_0 dfst obtain prev where "(prev, p) ∈ g_E G" and prev_lt_p: "prev < p" by auto
    then have prev_lt_n: "prev < n" 
         and prev_p: "p ∈ succs prev" 
         and "prev ∈ set (g_V G)" using p_lt_n tail_is_vert by (auto simp add:succs_def)     
    then have fin_suc_prev : "finite (succs prev)" using fin_succs by auto

    let ?prev_τ = "ss!prev"    

    from prev_lt_n stas ‹length ss = n› have "stable r step ss prev" by (auto simp add:stables_def)
    then have "∀(q,τ) ∈ set (step prev ?prev_τ). (prev # ?prev_τ) ⊑⇩r ss!q"
      by (auto simp add: stable_def transf_def step_def exec_def)
    with prev_p have "(prev # ?prev_τ) ⊑⇘r⇙ ss ! p" using fin_suc_prev by (auto simp add: stable_def transf_def step_def exec_def)
    with ss_p_eq_all have "sorted (rev (prev # ?prev_τ)) ∧ {0..<n} ⊆ set (prev # ?prev_τ) ∨ (prev # ss ! prev) =  (rev [0..<n])"
      by (auto simp add:r_def lesssub_def lesub_def nodes_le_def)
    then have "sorted (rev (prev # ?prev_τ)) ∧ {0..<n} ⊆ set (prev # ?prev_τ)" by(rule disjE)  auto
    then have sorted_rev: "sorted (rev (prev # ?prev_τ))" 
          and pres_subset: "{0..<n} ⊆ set (prev # ?prev_τ)" by auto    
    then have prev_set: "∀x∈ set ?prev_τ. x < prev" by (induct ?prev_τ) (auto simp add:sorted_wrt_append)
    
    from p_lt_n prev_lt_p have "prev < n - 1" using n_def nodes_def len_verts_gt0 by auto
    with prev_set have prev_lt_n: "∀x∈set(prev # ?prev_τ). x < n - 1" by auto
    from pres_subset have "n - 1 ∈ set (prev # ?prev_τ)" using n_def nodes_def len_verts_gt0 by fastforce
    with prev_lt_n show False by auto
  qed

  with ss_0th show " ss ! 0 = [] ∧ (∀p<n. p ≠ 0 ⟶ ss ! p ≠ rev [0..<n])" by auto
qed

lemma dom_iter_properties2: 
  "iter f step start (unstables r step start) = (ss,w) ⟶ (∀p<n.  ss!p ≠ (rev [0..<n]))"
proof(intro strip)
  fix p 
  assume iter: "iter f step start (unstables r step start) = (ss, w)" and p: "p < n"
  show "ss ! p ≠ (rev [0..<n])"
  proof(cases "p = 0")
    case True  
    with iter have "ss!p = []" by  (auto simp add:dom_iter_properties)
    then show ?thesis using n_def nodes_def len_verts_gt0 by auto
  next
    case False
    with iter p show ?thesis by (auto simp add:dom_iter_properties)
  qed
qed

lemma kildall_dom_properties:
  "kildall r f step start ∈ nlists n A ∧ 
   stables r step (kildall r f step start) ∧ 
   start [⊑⇩r] (kildall r f step start) ∧
   (∀ts∈nlists n A. start [⊑⇩r] ts ∧ stables r step ts ⟶ (kildall r f step start) [⊑⇩r] ts)"  (is "PROP ?P")
  by (case_tac "iter f step start (unstables r step start)")(simp add: kildall_def iter_dom_properties iter_dom_properties2)

lemma dom_kildall_stables: "stables r step (dom_kildall start)" 
  using kildall_dom_properties 
  by(unfold dom_kildall_def nodes_semi_def) (simp add: r_def f_def step_def)

lemma dom_kildall_entry: "dom_kildall start !0 = []" 
  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)

lemma zero_dom_zero: "dom i 0 ⟷ i = 0"
  using start_def n_def nodes_def dom_kildall_entry  by (simp add:dom_def)

(*lemma sadom_succs:  "strict_dom i j ⟹ j ∈ succs k ⟹ strict_dom i k"*)

lemma sdom_dom_succs: "strict_dom i j ⟹ j ∈ succs k ⟹ dom i k"
proof - 
  assume sdom_i_j: "strict_dom i j" and k_j: "j ∈ succs k" 
  then have j: "j ∈ set (g_V G)" 
        and k: "k ∈ set (g_V G)"  using verts_set succ_in_verts by auto
  then have j_lt_n: "j < n" and k_lt_n: "k < n"  using n_def nodes_def verts_set by auto

  have fin_succs_k: "finite (succs k)" using fin_succs k by auto
  with k_j have k_j2: "j ∈ set (rev (sorted_list_of_set(succs k)))" by auto

  let ?ss0 = "start"
  let ?w0 = "unstables r step start"
  let ?res = "dom_kildall start"

  have dom_kil: "?res = kildall r f step ?ss0" 
    by (auto simp add:dom_kildall_def r_def f_def step_def nodes_semi_def)

  have sorted_unstables: "sorted ?w0" by (auto simp add:unstables_def sorted_less_sorted_list_of_set)
  have ss: "?res = fst (iter f step ?ss0 ?w0)" by (auto simp add:dom_kildall_def kildall_def f_def step_def nodes_semi_def start_def r_def)
  then obtain ww where dom_iter: "iter f step ?ss0 ?w0 = (?res, ww)" by (cases "iter f step ?ss0 ?w0") auto  
  with iter_dom_properties have wf_res: "wf_dom (dom_kildall start) ww" by auto  
  with sdom_i_j have i_dom_j: "i ∈ set (?res!j)" by (auto simp add:strict_dom_def start_def n_def nodes_def)

  from wf_res have len_res: "length ?res = n" by (auto simp add:wf_dom_def)

  show "dom i k" 
  proof(rule ccontr)
    assume ass: "¬ dom i k" 
    then have i_neq_k: "i ≠ k" by (auto simp add:dom_refl)
    with ass have "(∃res. ?res!k = res ∧ i ∉ set res)" using ass by (auto simp add:dom_def start_def nodes_def n_def)
    then show False
    proof -
      assume "∃res. ?res ! k =  res ∧ i ∉ set res"
      then obtain rs where k_dom: "?res ! k = rs" and i_notin_rs: "i ∉ set rs" by auto     

      from iter_dom_properties dom_iter have "(∀p < length ?res. stable r step ?res p)" by (auto simp add:stables_def)
      with k_lt_n have "stable r step ?res k" using len_res by auto      
      with k_dom have aux: "∀(q,τ) ∈ set (map (λpc. (pc, (k # rs))) (rev (sorted_list_of_set(succs k)))). τ ⊑⇩r ?res!q"
        by (simp add:stable_def r_def step_def exec_def transf_def)      
      with k_j2 have "(k # rs) ⊑⇩r ?res!j" by auto
      then have "set (?res!j) ⊆ set (k # rs) ∨ ?res!j = k#rs" 
        by (auto simp add:lesssub_def lesub_def nodes_semi_def nodes_le_def r_def f_def)
      then have "set (?res!j) ⊆ set (k # rs)" by auto        
      with i_dom_j i_neq_k have " i ∈ set rs" by auto
      with i_notin_rs show False by auto
    qed
  qed
qed

lemma adom_succs: "dom i j ⟹ i ≠ j ⟹ j ∈ succs k ⟹ dom i k"
  by (auto intro: dom_sdom sdom_dom_succs)

lemma dom_kildall_is_strict: "j < length start ⟹ dom_kildall start ! j = res ⟹ j ∉ set res" 
proof -
  assume j_dom: "dom_kildall start ! j = res" and j_lt: "j < length start" 
  from j_dom have iter_fst: "(fst (iter f step start (unstables r step start))) ! j = res" 
    by (auto simp add:dom_kildall_def r_def f_def step_def start_def nodes_semi_def kildall_def)
  then obtain ss w where iter: "iter f step start (unstables r step start) = (ss, w)" by fastforce
  with iter_fst have res: "ss!j = res" by auto
  with dom_iter_properties2 iter have res_neq_all: "res ≠ rev [0..<n]" using len_start_is_n  j_lt len_start_is_n by auto

  with iter iter_dom_properties have "∀p < n. (ss!p) ≠ rev [0..< n] ⟶ (∀x∈set ( (ss!p)). x < p)" by (auto simp add:wf_dom_def)  
  with j_lt len_start_is_n res res_neq_all have "(∀x∈set res. x < j)" by (auto simp add:wf_dom_def) 
  then show "j ∉ set res" by auto
qed

lemma sdom_asyc: "strict_dom i j ⟹ j ∈ set (g_V G) ⟹ i ≠ j"
proof-
  assume sdom_i_j: "strict_dom i j" and "j ∈ set (g_V G)" 
  then have j_lt: "j < length start" using start_def n_def nodes_def verts_set by auto
  let ?start = " [] # (replicate (length (g_V G) - 1) ( (rev[0..<length(g_V G)])))"
  have eq_start: "?start = start" using n_def nodes_def start_def by simp  
  from sdom_i_j have i_in: "i ∈ set (dom_kildall ?start !j)" by (auto simp add:strict_dom_def)
  from j_lt have j_nin: "j ∉ set (dom_kildall ?start !j)" using eq_start by (simp add: dom_kildall_is_strict)
  with i_in  show "i ≠ j" by auto
qed


lemma propa_dom_invariant_complete:
  fixes i a b ss w 
  assumes b_n_nil: "b ≠ [] "
      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: "∀i. i < n ∧  k ∉ set (a!i) ⟶ non_strict_dominate k i "
    shows "wf_dom ss w ∧ (∀i. i < n ∧  k ∉ set ( ss ! i) ⟶ non_strict_dominate k i)"  (is "?PROP ?P")
  using assms
proof-  
  let ?a_hdb = "a!hd b" 
  let ?qs = "step (hd b) (a!hd b)"
  from wf_a_b b_n_nil propa have wf_ss_w: "wf_dom ss w" using propa_dom_invariant by auto
  
  from wf_a_b have "∀τ∈set a. τ ∈ A" 
               and sorted_b: "sorted b" 
               and len_a: "length a = n" 
               and b_lt_n: "∀x∈set b. x < n  "by (auto simp add:wf_dom_def)
  then have set_a: "set a ⊆ A" by (auto intro:nlistsI)
  from sorted_b have sorted_tl_b: "sorted (tl b)" using b_n_nil by (induct b) auto
  from b_lt_n b_n_nil have hd_b_lt_n: "hd b < n" by auto
  with n_def nodes_def verts_set have "hd b ∈ set (g_V G)" using b_n_nil  by auto
  then have fin_succ_hd_b: "finite (succs (hd b))" using fin_succs by auto 

  from wf_a_b b_n_nil have sorted_hd_b_a: "sorted (rev (hd b # ?a_hdb))"
                       and step_pres_bounded: " ∀(q, τ)∈set (step (hd b) ?a_hdb). q < length a ∧ τ ∈ A" 
    using propa_dom_invariant_auxi by auto 

  from hd_b_lt_n have dist: "distinct (map fst ?qs)" using distinct_p by auto
  with set_a step_pres_bounded sorted_tl_b len_a have "∀(q, τ) ∈ set ?qs. (fst(propa f ?qs a (tl b)))!q = τ ⊔⇘f⇙a!q" 
    by (auto dest:propa_property1)
  with propa have propa_ss1: "∀(q, τ) ∈ set ?qs. ss!q =  (hd b # ?a_hdb) ⊔⇘f⇙a!q" by (auto simp add:step_def exec_def transf_def)
  
  from step_pres_bounded sorted_tl_b set_a len_a dist
  have  "⋀q. q ∉ set(map fst ?qs) ⟹ q < length a ⟹ (fst(propa f ?qs a (tl b)))!q = a!q" 
    by (auto intro:propa_property2)
  with propa have exec2: "⋀q. q ∉ set(map fst ?qs) ⟹ q < length a ⟹ ss!q = a!q" by auto
 
  have "(∀i. i < n ∧ k ∉ set ( ss ! i) ⟶ non_strict_dominate k i)" 
  proof(intro strip)
    fix i
    let ?a_i = "a!i" 
    assume "i < n ∧ k ∉ set ( ss ! i) "
    then have i_lt_n: "i < n" and k_nin_ss: "k ∉ set (ss ! i) " by auto
    from non_strict have g: "i < n ∧ a ! i =  ?a_i ∧ k ∉ set ?a_i ⟹ non_strict_dominate k i" by auto 
    have sorted_a_i: "sorted (rev ?a_i)" using wf_a_b i_lt_n by (auto simp add:_wf_dom_def)

    show "non_strict_dominate k i" 
    proof(cases "i ∈ (succs (hd b))")
      case True note i_succ_hdb = this
      with propa_ss1 have ss_i: "ss!i =  (hd b # ?a_hdb) ⊔⇘f⇙ a!i" using fin_succ_hd_b by (auto simp add:step_def exec_def)
      then have "ss!i =  (hd b # ?a_hdb ) ⊔⇘f⇙ ?a_i" by auto
      with sorted_hd_b_a sorted_a_i have "set (ss!i) = set (hd b # ?a_hdb) ∩ set ?a_i" 
                                     and ss_i_merge: "ss!i =  ((inter_sorted_rev (hd b # ?a_hdb) ?a_i))" 
        by (auto simp add:inter_sorted_correct f_def nodes_sup_def plussub_def)
      with k_nin_ss have k_nin': "k ∉ set (hd b # ?a_hdb) ∩ set ?a_i" by auto

      show ?thesis 
      proof(cases "k ∉ set ?a_i")
        case True
        then show ?thesis using i_lt_n g by auto
      next 
        case False
        with k_nin' have "k ∉ set ?a_hdb" and k_neq_hdb: "k ≠ hd b" by auto   
        with hd_b_lt_n non_strict have n_k_hdb: "non_strict_dominate k (hd b)" by auto
        from i_succ_hdb have "(hd b, i)∈ g_E G" by (auto simp add:succs_def)        
        with n_k_hdb k_neq_hdb show ?thesis using non_sdominate_succ by auto
      qed      
    next
      case False      
      with exec2 have "ss!i = a!i" using fin_succ_hd_b len_a i_lt_n by (auto simp add:step_def exec_def)
      with k_nin_ss have "k ∉ set (a!i)" by auto
      with non_strict show ?thesis using i_lt_n by fastforce
    qed
  qed

  with wf_ss_w show "?PROP ?P" by auto
qed

lemma start_non_sdom: " i < n ∧ start!i =  res ∧ k ∉ set res ⟶ non_strict_dominate k i" 
proof(auto)
  assume i_lt_n: "i < n" and k_nin: "k ∉ set (start ! i)"
  then have reach_i: "reachable i" using n_def nodes_def verts_set len_verts_gt0 reachable by  (simp add:reachable_def)
  then obtain pa where pa_i: "path_entry (g_E G) pa i" using reachable_path_entry by auto

  show "non_strict_dominate k i"
  proof(cases "k ∈ set (g_V G)")
    case True
    then have "k < n" using verts_set by (auto simp add:n_def nodes_def)
    then have k_in_verts: "k ∈ set (g_V G)" and k_in_verts': "k ∈ {0..<n}" using verts_set n_def nodes_def by auto

    show "non_strict_dominate k i"
    proof(cases "i = 0")
      case True then show ?thesis using any_sdominate_0 k_in_verts by auto
    next
      case False
      then have "start!i = (rev [0..<n])" using start_def i_lt_n n_def nodes_def by (simp add:start_def)
      with k_nin k_in_verts' show ?thesis by auto
    qed
  next
    case False note k_nin_verts = this
    have "∀pa. path_entry (g_E G) pa i ⟶ set pa ⊆ set (g_V G)" using path_in_verts nodes_def by auto
    with k_nin_verts have k_nin: "∀pa. path_entry (g_E G) pa i ⟶ k ∉ set pa" 
      by (fastforce dest: contra_subsetD) 
    with pa_i have "k ∉ set pa" by auto
    with pa_i show ?thesis by (auto simp add: non_strict_dominate_def) 
  qed
qed

lemma iter_dom_invariant_complete:
    shows "⋀res.  iter f step start (unstables r step start) = (ss',w') ⟶ i < n ∧ ss'!i =  res ∧ k ∉ set res ⟶ non_strict_dominate k i" 
  apply (unfold iter_def)  
  apply(rule_tac  
      P = "(λ(ss, w). wf_dom ss w ∧ (∀i. (∃rs. i < n ∧ ss!i =  rs ∧ k ∉ set rs) ⟶ non_strict_dominate k i))" and
      r = "{(ss',ss). ss [⊏⇩r] ss'} <*lex*> (λ(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset" 
      in while_rule) 
  ― ‹Invariant holds initially:›
      apply clarsimp
      apply (fastforce simp add:start_non_sdom wf_start)

  ― ‹Invariant is preserved:›
     apply (fastforce dest:propa_dom_invariant_complete)

  ― ‹Postcondition holds upon termination:›
    apply clarsimp    

  ― ‹Well-foundedness of the termination relation:›
   apply (simp add:wf_listn_termination_rel)

  ― ‹Loop decreases along termination relation:›
  apply clarsimp 
  apply (fastforce dest:propa_termination)
 
  done

end

end