theory Ribbons_Soundness imports 
  Ribbons_Graphical 
  "~~/src/HOL/Library/Permutation"
  "~~/src/HOL/Library/Quotient_List"
begin

text {* We prove that the proof rules defined in ribbons_graphical.thy are sound with respect to the rules of separation logic defined in ribbons_basic.thy, under the assumption that variables-as-resource is in use (which means that the Frame rule has no side-condition). The script is very long, and not intended for reading! The soundness theorem is stated at the end. *}

subsection {* Proof chains *}

text {* To enable the proof of soundness, we introduce proof chains. An (a,c) proof chain is a sequence of alternating a's and c's, beginning and ending with an a. Usually "a" represents an assertion or an interface, and "c" represents a command or a command-node. *}
datatype ('a,'c) chain = 
  cNil "'a"
| cCons "'a" "'c" "('a,'c) chain"

text {* Project first interface *}
fun
  pre :: "('a,'c) chain \<Rightarrow> 'a"
where
  "pre (cNil P) = P"
| "pre (cCons P x \<Pi>) = P"

text {* Project final interface *}
fun 
  post :: "('a,'c) chain \<Rightarrow> 'a"
where
  "post (cNil P) = P"
| "post (cCons P x \<Pi>) = post \<Pi>"

text {* Project list of commands *}
fun
  comlist :: "('a,'c) chain \<Rightarrow> 'c list"
where
  "comlist (cNil _) = []"
| "comlist (cCons _ x \<Pi>) = x # (comlist \<Pi>)" 

text {* Extract nth triple from a non-empty chain. *}
fun
  nthtriple :: "('a,'c) chain \<Rightarrow> nat \<Rightarrow> ('a * 'c * 'a)"
where
  "nthtriple (cCons P x \<Pi>) 0 = (P, x, pre \<Pi>)"
| "nthtriple (cCons P x \<Pi>) (Suc n) = nthtriple \<Pi> n"

text {* Length of a chain *}
fun
  chainlen :: "('a,'c) chain \<Rightarrow> nat"
where
  "chainlen (cNil _) = 0"
| "chainlen (cCons _ _ \<Pi>) = 1 + (chainlen \<Pi>)"

text {* The list of middle components of \<Pi>'s triples is the list of \<Pi>'s commands *}
lemma snds_of_triples_form_comlist:
  fixes \<Pi>
  shows "\<And>i. i < chainlen \<Pi> \<Longrightarrow> 
  snd3 (nthtriple \<Pi> i) = (comlist \<Pi>)!i"
proof (induct \<Pi>)
  case cNil thus ?case by auto
next
  case (cCons p c \<Pi>)
  thus ?case
  proof (induct i) (* actually just a case-split *)
    case 0 thus ?case by (auto simp add: snd3_def)
  next
    case (Suc i)
    hence "i < chainlen \<Pi>" by auto
    from Suc.prems(1)[OF this] have "snd3 (nthtriple \<Pi> i) = comlist \<Pi> ! i" by auto
    thus "snd3 (nthtriple (cCons p c \<Pi>) (Suc i)) = comlist (cCons p c \<Pi>) ! Suc i" by auto
  qed
qed

text {* Map one function over all the interfaces, and another over all the commands. *}
fun
  chainmap :: "('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> ('a,'c) chain \<Rightarrow> ('b,'d) chain"
where
  "chainmap f g (cNil P) = cNil (f P)"
| "chainmap f g (cCons P x \<Pi>) = cCons (f P) (g x) (chainmap f g \<Pi>)"

text {* Mapping over a chain preserves its length *}
lemma chainmap_preserves_length: 
  "chainlen (chainmap f g \<Pi>) = chainlen \<Pi>"
by (induct \<Pi>, auto)

text {* Extend a chain on its right-hand side. *}
fun
  cSnoc :: "('a,'c) chain \<Rightarrow> 'c \<Rightarrow> 'a \<Rightarrow> ('a,'c) chain"
where
  "cSnoc (cNil P) y Q = cCons P y (cNil Q)"
| "cSnoc (cCons P x \<Pi>) y Q = cCons P x (cSnoc \<Pi> y Q)"

lemma len_snoc:
  fixes \<Pi> x P
  shows "chainlen (cSnoc \<Pi> x P) = 1 + (chainlen \<Pi>)"
by (induct \<Pi>, auto)

lemma pre_snoc: 
  "pre (cSnoc \<Pi> x P) = pre \<Pi>" by (induct \<Pi>, auto)

lemma comlist_snoc:
  "comlist (cSnoc \<Pi> x p) = comlist \<Pi> @ [x]"
by (induct \<Pi>, auto)

text {* Like set-difference, but for lists *}
definition listdiff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  "listdiff X Y \<equiv> [x \<leftarrow> X . x \<notin> set Y]"

lemma listdiff_nil_right: 
  "listdiff X [] = X"
  by (unfold listdiff_def, auto)

lemma listdiff_is_fold_rem:
  fixes X Y
  shows "listdiff X Y = foldr removeAll Y X" 
proof (induct Y)
  case Nil
  show ?case unfolding listdiff_def by auto
next
  case (Cons y Y)
  have "foldr removeAll (y # Y) X
    = removeAll y (foldr removeAll Y X)" by auto
  also have "... = removeAll y (listdiff X Y)"
    unfolding Cons.hyps by auto
  also have "... = removeAll y [x \<leftarrow> X . x \<notin> set Y]"
    unfolding listdiff_def by auto
  also have "... = filter (op \<noteq> y) [x \<leftarrow> X . x \<notin> set Y]"
    unfolding removeAll_filter_not_eq by auto
  also have "... = [x\<leftarrow>X . x \<notin> set Y \<and> y \<noteq> x]"
    unfolding filter_filter by auto
  also have "... = [x\<leftarrow>X . \<not> (x \<in> set Y \<or> x = y)]" 
    unfolding eq_commute by auto
  also have "... = [x\<leftarrow>X . \<not> (x \<in> insert y (set Y))]" 
    unfolding insert_iff disj_commute by auto
  also have "... = [x\<leftarrow>X . x \<notin> set (y # Y)]"
    unfolding set.simps by auto
  also have "... = listdiff X (y # Y)"
    unfolding listdiff_def by auto
  finally show ?case by auto
qed

text {* Markers to indicate whether we're at the "top" or the "bottom" of a node; i.e., whether it hasn't (top) or has (bottom) been processed. *}
datatype topbot = Top | Bot

text {* A proofstate is a list of "currently initial" nodes, each marked as processed or not. The list is not ordered. Hence we could have used the theory of Finite Multisets here. *}

quotient_type proofstate = "(node * topbot) list" / "perm"
proof (intro equivpI)
  show "reflp perm" by (metis perm_refl reflpI)
next
  show "symp perm" by (metis perm_sym sympI)
next
  show "transp perm" by (metis perm.trans transpI)
qed

text {* \<alpha> converts a particular list to its equivalence class. \<gamma> converts an equivalence class to a particular list (in that class). *}
abbreviation \<alpha> where "\<alpha> \<equiv> abs_proofstate"
abbreviation \<gamma> where "\<gamma> \<equiv> rep_proofstate"

lemma conc_abs:
  "\<gamma> (\<alpha> X) <~~> X"
by (metis Quotient_proofstate perm_refl rep_abs_rsp_left)

lemma abs_conc:
  "\<alpha> (\<gamma> X) = X"
by (metis Quotient_def Quotient_proofstate)

lemma abs_equiv:
  "X <~~> Y \<Longrightarrow> \<alpha> X = \<alpha> Y"
by (metis Quotient_proofstate Quotient_rel)

type_synonym rawchain = "(proofstate, node + edge) chain"
type_synonym cookedchain = "(interface, assnode + comnode) chain"

text {* mk \<Pi> \<pi> converts the node+edge list \<pi> into a rawchain by interspersing the appropriate proofstates. The first argument \<Pi> is the part of the chain that has already been converted. *}
definition
  mk :: "[rawchain, (node + edge) list] \<Rightarrow> rawchain"
where
  "mk \<Pi> \<pi> \<equiv> foldl (\<lambda>\<Pi>. sum_case 
  (\<lambda>v. cSnoc \<Pi> (Inl v) (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) 
    [(v,Top)]) @ [(v,Bot)]))) 
  (\<lambda>e. cSnoc \<Pi> (Inr e) (\<alpha> ((listdiff (\<gamma> (post \<Pi>))
    [(v,Bot) . v \<leftarrow> fst3 e]) @ [(v,Top) . v \<leftarrow> thd3 e])))) \<Pi> \<pi>"

lemma mk_preserves_length:
  fixes \<pi>
  shows "\<And>\<Pi>. chainlen (mk \<Pi> \<pi>) = chainlen \<Pi> + length \<pi>"
proof (induct \<pi>)
  case Nil
  show ?case by (unfold mk_def, auto)
next
  case (Cons x \<pi>)
  hence "\<And>\<Pi>. chainlen (mk \<Pi> \<pi>) = chainlen \<Pi> + length \<pi>"
    by auto
  show ?case
  proof (cases x)
    case (Inl v)
    let ?lhs = "chainlen (mk \<Pi> (x # \<pi>))"
    have "?lhs = chainlen (mk \<Pi> ((Inl v) # \<pi>))"
      using Inl by auto
    also have "... = chainlen (mk 
      (cSnoc \<Pi> (Inl v) (\<alpha> (listdiff (\<gamma> (post \<Pi>)) [(v, Top)] 
      @ [(v, Bot)]))) \<pi>)" unfolding mk_def by auto
    also have "... = chainlen (cSnoc \<Pi> (Inl v) (\<alpha> (listdiff (\<gamma> 
      (post \<Pi>)) [(v, Top)] @ [(v, Bot)]))) + length \<pi>" 
      using Cons.hyps by auto
    also have "... = 1 + chainlen \<Pi> + length \<pi>" 
      using len_snoc by auto
    also have "... = chainlen \<Pi> + length (x # \<pi>)" by auto
    finally show ?thesis by auto
  next
    case (Inr e)
    let ?lhs = "chainlen (mk \<Pi> (x # \<pi>))"
    have "?lhs = chainlen (mk \<Pi> ((Inr e) # \<pi>))"
      using Inr by auto
    also have "... = chainlen (mk 
      (cSnoc \<Pi> (Inr e) (\<alpha> (listdiff (\<gamma> (post \<Pi>)) 
      [(v, Bot) . v \<leftarrow> fst3 e] @ [(v, Top) . v \<leftarrow> thd3 e]))) \<pi>)"
      unfolding mk_def by auto
    also have "... = chainlen (cSnoc \<Pi> (Inr e) (\<alpha> (listdiff (\<gamma> 
      (post \<Pi>)) [(v, Bot) . v \<leftarrow> fst3 e] @ [(v, Top) . v \<leftarrow> thd3 e])))
      + length \<pi>" 
      using Cons.hyps by auto
    also have "... = 1 + chainlen \<Pi> + length \<pi>" 
      using len_snoc by auto
    also have "... = chainlen \<Pi> + length (x # \<pi>)" by auto
    finally show ?thesis by auto
  qed
qed
 
text {* mk distributes over cCons *}
lemma mk_ccons:
  fixes \<pi> \<Pi>
  shows "mk (cCons \<sigma> x \<Pi>) \<pi> = cCons \<sigma> x (mk \<Pi> \<pi>)"
proof (induct \<pi> arbitrary: \<Pi>)
  case Nil
  thus ?case unfolding mk_def by auto
next
  case (Cons y \<tau>)
  let ?f = "\<lambda>\<Pi>. sum_case 
  (\<lambda>v. cSnoc \<Pi> (Inl v) (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) 
    [(v,Top)]) @ [(v,Bot)]))) 
  (\<lambda>e. cSnoc \<Pi> (Inr e) (\<alpha> ((listdiff (\<gamma> (post \<Pi>))
    [(v,Bot) . v \<leftarrow> fst3 e]) @ [(v,Top) . v \<leftarrow> thd3 e])))"
  show ?case 
  proof (cases y)
    case (Inl v)
    hence sleik: "y = Inl v" by auto
    let ?lhs = "mk (cCons \<sigma> x \<Pi>) ((Inl v) # \<tau>)"
    have "?lhs = foldl ?f (cCons \<sigma> x \<Pi>) ((Inl v) # \<tau>)"
      unfolding mk_def by auto
    also have "... = foldl ?f (?f (cCons \<sigma> x \<Pi>) (Inl v)) \<tau>" 
      by (unfold foldl.simps(2), auto)
    also have "... = foldl ?f (cSnoc (cCons \<sigma> x \<Pi>) (Inl v) 
      (\<alpha> ((listdiff (\<gamma> (post (cCons \<sigma> x \<Pi>))) [(v,Top)]) 
      @ [(v,Bot)]))) \<tau>" 
      by auto
    also have "... = foldl ?f (cCons \<sigma> x (cSnoc \<Pi> (Inl v) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)])))) \<tau>"
      by auto
    also have "... = mk (cCons \<sigma> x (cSnoc \<Pi> (Inl v) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)])))) \<tau>" 
      unfolding mk_def by auto
    also have "... = cCons \<sigma> x (mk (cSnoc \<Pi> (Inl v) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)]))) \<tau>)" 
      using Cons.hyps by auto
    also have "... = cCons \<sigma> x (mk \<Pi> ((Inl v) # \<tau>))"
      unfolding mk_def by auto
    finally show ?thesis using sleik by auto
  next
    case (Inr e)
    hence sleik: "y = Inr e" by auto
    let ?lhs = "mk (cCons \<sigma> x \<Pi>) ((Inr e) # \<tau>)"
    have "?lhs = foldl ?f (cCons \<sigma> x \<Pi>) ((Inr e) # \<tau>)"
      unfolding mk_def by auto
    also have "... = foldl ?f (?f (cCons \<sigma> x \<Pi>) (Inr e)) \<tau>" 
      by (unfold foldl.simps(2), auto)
    also have "... = foldl ?f (cSnoc (cCons \<sigma> x \<Pi>) (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post (cCons \<sigma> x \<Pi>))) [(v,Bot) . v \<leftarrow> fst3 e]) 
      @ [(v,Top) . v \<leftarrow> thd3 e]))) \<tau>" 
      by auto
    also have "... = foldl ?f (cCons \<sigma> x (cSnoc \<Pi> (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot) . v \<leftarrow> fst3 e]) 
      @ [(v,Top) . v \<leftarrow> thd3 e])))) \<tau>"
      by auto
    also have "... = mk (cCons \<sigma> x (cSnoc \<Pi> (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot) . v \<leftarrow> fst3 e]) 
      @ [(v,Top) . v \<leftarrow> thd3 e])))) \<tau>" 
      unfolding mk_def by auto
    also have "... = cCons \<sigma> x (mk (cSnoc \<Pi> (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot) . v \<leftarrow> fst3 e]) 
      @ [(v,Top) . v \<leftarrow> thd3 e]))) \<tau>)" 
      using Cons.hyps by auto
    also have "... = cCons \<sigma> x (mk \<Pi> ((Inr e) # \<tau>))"
      unfolding mk_def by auto
    finally show ?thesis using sleik by auto
  qed
qed

text {* mk preserves \<pi> as its list of commands *}
lemma mk_comlist:
  fixes \<Pi> \<pi>
  shows "comlist (mk \<Pi> \<pi>) = (comlist \<Pi>) @ \<pi>"
proof (induct \<pi> arbitrary: \<Pi>)
  case Nil thus ?case unfolding mk_def by auto
next
  case (Cons x \<pi>)
  hence "\<And>\<Pi>. comlist (mk \<Pi> \<pi>) = comlist \<Pi> @ \<pi>" by auto
  let ?f = "\<lambda>\<Pi>. sum_case 
    (\<lambda>v. cSnoc \<Pi> (Inl v) (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)]))) 
    (\<lambda>e. cSnoc \<Pi> (Inr e) 
    (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot) . v \<leftarrow> fst3 e]) 
    @ [(v,Top) . v \<leftarrow> thd3 e])))"
  show ?case
  proof (induct x)
    case (Inl v)
    let ?lhs = "comlist (mk \<Pi> (Inl v # \<pi>))"
    let ?rhs = "comlist \<Pi> @ (Inl v) # \<pi>"
   
    have "?lhs = comlist (foldl ?f (?f \<Pi> (Inl v)) \<pi>)" 
      unfolding mk_def by auto
    hence "?lhs = comlist (foldl ?f (?f \<Pi> (Inl v)) \<pi>)" 
      by auto
    hence "?lhs = comlist (foldl ?f (cSnoc \<Pi> (Inl v) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)]))) \<pi>)"
      by auto
    hence "?lhs = comlist (mk (cSnoc \<Pi> (Inl v) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)]))) \<pi>)" 
      unfolding mk_def by auto
    hence "?lhs = comlist (cSnoc \<Pi> (Inl v) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)]))) @ \<pi>"
      using Cons.hyps by auto
    hence "?lhs = (comlist \<Pi> @ [Inl v]) @ \<pi>" 
      using comlist_snoc by auto
    thus "?lhs = ?rhs" by auto
  next
    case (Inr e)

    let ?lhs = "comlist (mk \<Pi> (Inr e # \<pi>))"
    let ?rhs = "comlist \<Pi> @ (Inr e) # \<pi>"
    
    have "?lhs = comlist (foldl ?f (?f \<Pi> (Inr e)) \<pi>)" 
      unfolding mk_def by auto
    hence "?lhs = comlist (foldl ?f (?f \<Pi> (Inr e)) \<pi>)" 
      by auto
    hence "?lhs = comlist (foldl ?f (cSnoc \<Pi> (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot). v\<leftarrow>fst3 e]) @ [(v,Top). v\<leftarrow>thd3 e]))) \<pi>)"
      by auto
    hence "?lhs = comlist (mk (cSnoc \<Pi> (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot). v\<leftarrow>fst3 e]) @ [(v,Top). v\<leftarrow>thd3 e]))) \<pi>)" 
      unfolding mk_def by auto
    hence "?lhs = comlist (cSnoc \<Pi> (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot). v\<leftarrow>fst3 e]) @ [(v,Top). v\<leftarrow>thd3 e]))) @ \<pi>"
      using Cons.hyps by auto
    hence "?lhs = (comlist \<Pi> @ [Inr e]) @ \<pi>" 
      using comlist_snoc by auto
    thus "?lhs = ?rhs" by auto
  qed
qed

lemma pre_mk:
  fixes \<Pi> \<pi>
  shows "pre (mk \<Pi> \<pi>) = pre \<Pi>"
proof (induct \<pi> arbitrary: \<Pi>)
  case Nil
  thus ?case by (unfold mk_def, auto)
next
  case (Cons x \<pi>')
  hence "\<And>\<Pi>. pre (mk \<Pi> \<pi>') = pre \<Pi>" by auto
  let ?f = "\<lambda>\<Pi>. sum_case 
    (\<lambda>v. cSnoc \<Pi> (Inl v) (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)]))) 
    (\<lambda>e. cSnoc \<Pi> (Inr e) 
    (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot) . v \<leftarrow> fst3 e]) 
    @ [(v,Top) . v \<leftarrow> thd3 e])))"
  have "pre (mk \<Pi> (x # \<pi>')) = pre (foldl ?f \<Pi> (x # \<pi>'))" 
    unfolding mk_def by auto
  also have "... = pre (foldl ?f (?f \<Pi> x) \<pi>')"
    unfolding foldl.simps(2) by auto
  also have "... = pre (mk (?f \<Pi> x) \<pi>')"
    unfolding mk_def by auto
  also have "... = pre (?f \<Pi> x)"
    unfolding Cons.hyps by auto
  also have "... = pre \<Pi>"
  proof (cases x)
    case (Inl v)
    hence "pre (?f \<Pi> x) = pre (?f \<Pi> (Inl v))" by auto
    also have "... = pre (cSnoc \<Pi> (Inl v) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) @ [(v,Bot)])))" 
      by auto
    also have "... = pre \<Pi>" unfolding pre_snoc by auto
    finally show ?thesis by auto
  next
    case (Inr e)
    hence "pre (?f \<Pi> x) = pre (?f \<Pi> (Inr e))" by auto
    also have "... = pre (cSnoc \<Pi> (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot) . v \<leftarrow> fst3 e]) 
      @ [(v,Top) . v \<leftarrow> thd3 e])))" 
      by auto
    also have "... = pre \<Pi>" unfolding pre_snoc by auto
    finally show ?thesis by auto
  qed
  finally show ?case by auto
qed

text {* Converts a "raw" chain, which talks about nodes and edges, into a "cooked" chain, which talks about interfaces and command-/assertion-nodes. *}
fun 
  cook :: "[diagram, rawchain] \<Rightarrow> cookedchain"
where 
  "cook (Graph V \<Lambda> E) \<Pi> = chainmap 
  ((foldl (op \<otimes>) Emp_int) \<circ> 
  (map (\<lambda>(v,z). topbot_case top_ass bot_ass z (\<Lambda> v))) \<circ> \<gamma>) 
  (sum_case (Inl \<circ> \<Lambda>) (Inr \<circ> snd3)) \<Pi>"

text {* The S argument is the subset of initial nodes that have already been processed, and shouldn't be included in the linear extensions. *}
fun lins2 :: "[node list, diagram] \<Rightarrow> ((node + edge) list) set"
where
"lins2 S (Graph V \<Lambda> E) = {\<pi> . (distinct \<pi>) \<and> (set \<pi> = ((Inl ` (set V - set S)) \<union> (Inr ` (set E)))) \<and> (\<forall>i j v e. i < length \<pi> \<and> j < length \<pi> \<and> \<pi>!i = Inl v \<and> \<pi>!j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i<j) \<and> (\<forall>j k w e. j < length \<pi> \<and> k < length \<pi> \<and> \<pi>!j = Inr e \<and> \<pi>!k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j<k) }"

text {* When S is empty, the two definitions coincide. *}
lemma lins_is_lins2_with_empty_S:
  fixes V \<Lambda> E
  shows "lins (Graph V \<Lambda> E) = lins2 [] (Graph V \<Lambda> E)"
proof (intro set_eqI iffI)
  fix \<pi>
  assume "\<pi> \<in> lins (Graph V \<Lambda> E)"
  hence "distinct \<pi> \<and>
    set \<pi> = Inl ` set V \<union> Inr ` set E \<and>
    (\<forall>i j v e. i < length \<pi> \<and> j < length \<pi> \<and> \<pi> ! i = Inl v 
    \<and> \<pi> ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j) \<and>
    (\<forall>j k w e. j < length \<pi> \<and> k < length \<pi> \<and> \<pi> ! j = Inr e 
    \<and> \<pi> ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k)" 
  apply (unfold lins.simps) 
  apply (erule CollectE, assumption)
  done
  hence "distinct \<pi> \<and>
    set \<pi> = Inl ` (set V - set []) \<union> Inr ` set E \<and>
    (\<forall>i j v e. i < length \<pi> \<and> j < length \<pi> \<and> \<pi> ! i = Inl v 
    \<and> \<pi> ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j) \<and>
    (\<forall>j k w e. j < length \<pi> \<and> k < length \<pi> \<and> \<pi> ! j = Inr e 
    \<and> \<pi> ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k)"
    apply (elim conjE)
    apply (intro conjI)
    apply assumption
    apply simp
    apply assumption+ 
    done
  thus "\<pi> \<in> lins2 [] (Graph V \<Lambda> E)"
    apply (unfold lins2.simps) 
    apply (intro CollectI, assumption) 
    done
next
  fix \<pi>
  assume "\<pi> \<in> lins2 [] (Graph V \<Lambda> E)"
  hence "distinct \<pi> \<and>
    set \<pi> = Inl ` (set V - set []) \<union> Inr ` set E \<and>
    (\<forall>i j v e. i < length \<pi> \<and> j < length \<pi> \<and> \<pi> ! i = Inl v
    \<and> \<pi> ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j) \<and>
    (\<forall>j k w e. j < length \<pi> \<and> k < length \<pi> \<and> \<pi> ! j = Inr e 
    \<and> \<pi> ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k)"
    apply (unfold lins2.simps) 
    apply (erule CollectE, assumption) 
    done
  hence "distinct \<pi> \<and>
    set \<pi> = Inl ` (set V) \<union> Inr ` set E \<and>
    (\<forall>i j v e. i < length \<pi> \<and> j < length \<pi> \<and> \<pi> ! i = Inl v 
    \<and> \<pi> ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j) \<and>
    (\<forall>j k w e. j < length \<pi> \<and> k < length \<pi> \<and> \<pi> ! j = Inr e 
    \<and> \<pi> ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k)"
    apply (elim conjE)
    apply (intro conjI)
    apply assumption
    apply simp
    apply assumption+ 
    done
  thus "\<pi> \<in> lins (Graph V \<Lambda> E)"
    apply (unfold lins.simps) apply (intro CollectI, assumption) done
qed

text {* The set of raw chains of a diagram *}
definition rawchains :: "diagram \<Rightarrow> rawchain set"
where "rawchains G \<equiv> {mk (cNil 
  (\<alpha> [(v,Top). v \<leftarrow> initials G])) \<pi> 
  | \<pi> . \<pi> \<in> lins G}"

text {* The set of raw chains of a diagram, where S is the set of initial nodes that should not be included in the chains. *}
definition rawchains2 :: "[node list, diagram] \<Rightarrow> rawchain set"
where "rawchains2 S G \<equiv> { mk (cNil 
  (\<alpha> ([(v,Top). v \<leftarrow> initials G, v \<notin> set S] @ [(v,Bot). v \<leftarrow> S]))) \<pi> 
  | \<pi> . \<pi> \<in> lins2 S G }"

text {* When S is empty, the two definitions coincide. *}
lemma rawchains_is_rawchains2_with_empty_S:
  fixes V \<Lambda> E
  shows "rawchains (Graph V \<Lambda> E) = rawchains2 [] (Graph V \<Lambda> E)"
proof (intro set_eqI iffI)
  fix \<Pi>
  assume "\<Pi> \<in> rawchains (Graph V \<Lambda> E)"
  then obtain \<pi> where 
    zgico: "\<Pi> = mk (cNil (\<alpha> [(v,Top). v \<leftarrow> 
    initials (Graph V \<Lambda> E)])) \<pi>" and
    "\<pi> \<in> lins (Graph V \<Lambda> E)" by (unfold rawchains_def, auto)
  with lins_is_lins2_with_empty_S[of V \<Lambda> E] have
    "\<pi> \<in> lins2 [] (Graph V \<Lambda> E)" 
    by metis
  with zgico show "\<Pi> \<in> rawchains2 [] (Graph V \<Lambda> E)" 
    unfolding rawchains2_def
  proof (intro CollectI exI[of _ \<pi>] conjI)
    assume "\<Pi> = mk (cNil (\<alpha> [(v,Top). v \<leftarrow> initials
      (Graph V \<Lambda> E)])) \<pi>"
    thus "\<Pi> = mk
      (cNil (\<alpha> ([(v,Top). v \<leftarrow> initials (Graph V \<Lambda> E), v \<notin> set []] 
      @ [(v,Bot). v \<leftarrow> []]))) \<pi>" by auto
  qed (assumption)
next
  fix \<Pi>
  assume "\<Pi> \<in> rawchains2 [] (Graph V \<Lambda> E)"
  then obtain \<pi> where
    zgico: "\<Pi> = mk (cNil (\<alpha> ([(v,Top). v \<leftarrow> initials 
    (Graph V \<Lambda> E), v \<notin> set []] @ [(v,Bot). v \<leftarrow> []]))) \<pi>" and
    "\<pi> \<in> lins2 [] (Graph V \<Lambda> E)" unfolding rawchains2_def by auto
  with lins_is_lins2_with_empty_S[of V \<Lambda> E] have
    "\<pi> \<in> lins (Graph V \<Lambda> E)" 
    by metis
  with zgico show "\<Pi> \<in> rawchains (Graph V \<Lambda> E)" 
    unfolding rawchains_def
  proof (intro CollectI exI[of _ \<pi>] conjI)
    assume "\<Pi> = mk
      (cNil (\<alpha> ([(v,Top). v \<leftarrow> initials (Graph V \<Lambda> E), v \<notin> set []] 
      @ [(v,Bot). v \<leftarrow> []]))) \<pi>"
    thus "\<Pi> = mk (cNil 
      (\<alpha> [(v,Top). v \<leftarrow> initials (Graph V \<Lambda> E)])) \<pi>"
      by auto
  qed (assumption)
qed

text {* A rawchain is well-formed if for each triple {P} (Inl v) {Q}, P is of the form [(v,Top)] @ F, and Q is of the form [(v,Bot)] @ F, and for each triple {P} (Inr (vs,_,ws)) {Q}, P is of the form [(v,Bot). v\<leftarrow>vs] @ F, and Q is of the form [(v,Top), v \<leftarrow> ws] @ F. *}

definition
  wf_rawchain :: "rawchain \<Rightarrow> bool"
where
  "wf_rawchain \<Pi> \<equiv> \<forall>i < chainlen \<Pi>. \<exists>\<sigma>'. (\<exists>v. nthtriple \<Pi> i =
  (\<alpha> ([(v,Top)] @ \<sigma>'), Inl v, \<alpha> ([(v,Bot)] @ \<sigma>')))
  \<or> (\<exists>e. nthtriple \<Pi> i = 
  (\<alpha> ([(v,Bot). v\<leftarrow>fst3 e] @ \<sigma>'), Inr e, \<alpha> ([(v,Top). v\<leftarrow>thd3 e] @ \<sigma>')))"

text {* The nil chain is well-formed. *}
lemma wf_rawchain_cnil: 
  "wf_rawchain (cNil (\<alpha> \<sigma>))"
by (unfold wf_rawchain_def, auto)

lemma wf_rawchain_ccons_inl: 
  fixes \<sigma> v \<sigma>' \<Pi>
  assumes "\<sigma> <~~> [(v,Top)] @ \<sigma>'"
  assumes "\<gamma> (pre \<Pi>) <~~> [(v,Bot)] @ \<sigma>'"
  assumes "wf_rawchain \<Pi>"
  shows "wf_rawchain (cCons (\<alpha> \<sigma>) (Inl v) \<Pi>)"
proof (unfold wf_rawchain_def, intro allI impI)
  fix i
  assume vzoyp: "i < chainlen (cCons (\<alpha> \<sigma>) (Inl v) \<Pi>)"
  from assms(1) assms(2) have 
    guhla: "\<sigma> <~~> (v, Top) # \<sigma>'" "\<gamma> (pre \<Pi>) <~~> (v, Bot) # \<sigma>'"
    by auto
  from assms(3)
  have xautg: "\<And>i. i < chainlen \<Pi> \<Longrightarrow>
    \<exists>\<sigma>'. (\<exists>v. nthtriple \<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))) \<or>
    (\<exists>e. nthtriple \<Pi> i =
    (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>')))"
    unfolding wf_rawchain_def by auto
  show "\<exists>\<sigma>'. (\<exists>va. nthtriple (cCons (\<alpha> \<sigma>) (Inl v) \<Pi>) i =
    (\<alpha> ([(va, Top)] @ \<sigma>'), Inl va, \<alpha> ([(va, Bot)] @ \<sigma>'))) \<or>
    (\<exists>e. nthtriple (cCons (\<alpha> \<sigma>) (Inl v) \<Pi>) i =
    (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>')))"
  proof (cases i)
    case 0
    show ?thesis
      apply (unfold 0) 
      apply (intro exI disjI1)
      apply (unfold nthtriple.simps(1))
      apply (intro tripleI)
      apply (unfold fst3_def snd3_def thd3_def)
      apply (simp_all)
      apply (rule abs_equiv[OF guhla(1)])
    proof -
      from abs_equiv[OF guhla(2)]
      have "\<alpha> (\<gamma> (pre \<Pi>)) = \<alpha> ((v, Bot) # \<sigma>')"
        by auto
      with abs_conc[of "pre \<Pi>"] show "pre \<Pi> = \<alpha> ((v, Bot) # \<sigma>')" by auto
    qed
  next
    case (Suc i')
    with vzoyp have "i' < chainlen \<Pi>" by auto
    show ?thesis
      apply (unfold Suc)
      apply (unfold nthtriple.simps(2))
      apply (rule xautg[OF `i' < chainlen \<Pi>`])
      done
  qed
qed

lemma wf_rawchain_ccons_inr: 
  fixes \<sigma> e \<sigma>' \<Pi>
  assumes "\<sigma> <~~> [(v,Bot) . v \<leftarrow> fst3 e] @ \<sigma>'"
  assumes "\<gamma> (pre \<Pi>) <~~> [(v,Top) . v \<leftarrow> thd3 e] @ \<sigma>'"
  assumes "wf_rawchain \<Pi>"
  shows "wf_rawchain (cCons (\<alpha> \<sigma>) (Inr e) \<Pi>)"
proof (unfold wf_rawchain_def, intro allI impI)
  fix i
  assume vzoyp: "i < chainlen (cCons (\<alpha> \<sigma>) (Inr e) \<Pi>)"
  from assms(1) assms(2) have 
    guhla: "\<sigma> <~~> [(v, Bot). v\<leftarrow>fst e] @ \<sigma>'" "\<gamma> (pre \<Pi>) <~~> [(v, Top). v\<leftarrow> snd (snd e)] @ \<sigma>'"
    unfolding fst3_def thd3_def by auto
  from assms(3)
  have xautg: "\<And>i. i < chainlen \<Pi> \<Longrightarrow>
    \<exists>\<sigma>'. (\<exists>v. nthtriple \<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))) \<or>
    (\<exists>e. nthtriple \<Pi> i =
    (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>')))"
    unfolding wf_rawchain_def by auto
  show "\<exists>\<sigma>'. (\<exists>va. nthtriple (cCons (\<alpha> \<sigma>) (Inr e) \<Pi>) i =
    (\<alpha> ([(va, Top)] @ \<sigma>'), Inl va, \<alpha> ([(va, Bot)] @ \<sigma>'))) \<or>
    (\<exists>ea. nthtriple (cCons (\<alpha> \<sigma>) (Inr e) \<Pi>) i =
    (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 ea) @ \<sigma>'), Inr ea, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 ea) @ \<sigma>')))"
  proof (cases i)
    case 0
    show ?thesis
      apply (unfold 0) 
      apply (intro exI disjI2)
      apply (unfold nthtriple.simps(1))
      apply (intro tripleI)
      apply (unfold fst3_def snd3_def thd3_def)
      apply (simp_all)
      thm abs_equiv [OF guhla(1)]
      apply (rule abs_equiv[OF guhla(1)])
    proof -
      from abs_equiv[OF guhla(2)]
      have "\<alpha> (\<gamma> (pre \<Pi>)) = \<alpha> ([(v, Top). v\<leftarrow> snd (snd e)] @ \<sigma>')"
        by auto
      with abs_conc[of "pre \<Pi>"] show "pre \<Pi> = \<alpha> ([(v, Top). v\<leftarrow> snd (snd e)] @ \<sigma>')" by auto
    qed
  next
    case (Suc i')
    with vzoyp have "i' < chainlen \<Pi>" by auto
    show ?thesis
      apply (unfold Suc)
      apply (unfold nthtriple.simps(2))
      apply (rule xautg[OF `i' < chainlen \<Pi>`])
      done
  qed
qed


lemma list_subseteq:
  fixes X
  shows "\<And>Y. \<lbrakk> distinct X ; set X \<subseteq> set Y \<rbrakk> \<Longrightarrow> length X \<le> length Y"
proof (induct X)
  case (Cons x X)
  from Cons.prems(1) have zeiaq: "distinct X" and gpzjd: "x \<notin> set X"
    by auto
  from Cons.prems(2) have "set X \<subseteq> set Y" and gnvih: "x \<in> set Y" 
    by auto
  from this(1) have nfvso: "set X - {x} \<subseteq> set Y - {x}" by auto
  from nfvso gpzjd have "set X \<subseteq> set Y - {x}" by auto
  moreover from nfvso gnvih have "set Y - {x} \<subseteq> set (remove1 x Y)" 
    by auto
  ultimately have "set X \<subseteq> set (remove1 x Y)" by auto
  from Cons.hyps[OF zeiaq this] have
    "length X \<le> length (remove1 x Y)" by auto
  hence "1 + length X \<le> 1 + length (remove1 x Y)" by auto
  hence fuwjo: "length (x#X) \<le> 1 + length (remove1 x Y)" by auto
  from gnvih have "length (remove1 x Y) = length Y - 1"
    using length_remove1[of x Y] by auto
  with fuwjo have fnowt: "length (x#X) \<le> 1 + (length Y - 1)" by auto
  from gnvih have "length Y \<noteq> 0" by auto
  with fnowt show "length (x#X) \<le> length Y" by arith
qed (auto)

lemma length_listdiff:
  fixes X Y
  assumes "distinct X"
  shows "\<lbrakk>distinct Y; set Y \<subseteq> set X \<rbrakk> \<Longrightarrow>
  length (listdiff X Y) = length X - length Y"
proof (induct Y)
  case Nil
  thus ?case unfolding listdiff_def by auto
next
  case (Cons y Y)
  from assms have "distinct (listdiff X Y)" 
    unfolding listdiff_def by auto
  from distinct_remove1_removeAll[OF this] have
    ptcbz: "remove1 y (listdiff X Y) = removeAll y (listdiff X Y)"
    by auto
  from Cons.prems have 
    "distinct Y" "set Y \<subseteq> set X" "y \<notin> set Y" by auto
  from Cons.hyps[OF this(1) this(2)] have 
    olttc: "length (listdiff X Y) = length X - length Y" 
    by auto
  from Cons.prems(2) have "y \<in> set X" by auto
  with `y \<notin> set Y` have 
    jgvgk: "y \<in> set (listdiff X Y)" 
    unfolding listdiff_def by auto
  have "length (listdiff X (y # Y))
    = length (foldr removeAll (y # Y) X)" 
    unfolding listdiff_is_fold_rem by auto
  also have "... = length (removeAll y (foldr removeAll Y X))" 
    by auto
  also have "... = length (removeAll y (listdiff X Y))" 
    unfolding listdiff_is_fold_rem by auto
  also have "... = length (remove1 y (listdiff X Y))" 
    using ptcbz by auto
  also have "... = length (listdiff X Y) - 1"
    unfolding length_remove1 using jgvgk  by auto
  also have "... = length X - length Y - 1" using olttc by auto
  also have "... = length X - length (y#Y)" by auto
  finally have "length (listdiff X (y # Y)) 
    = length X - length (y # Y)" by auto
  thus ?case by auto
qed

lemma diff_then_append:
  fixes X Y
  assumes "distinct X"
  shows "\<lbrakk> set Y \<subseteq> set X ; distinct Y \<rbrakk> \<Longrightarrow> X <~~> Y @ (listdiff X Y)"
proof (induct Y)
  case Nil
  show "X <~~> [] @ listdiff X []" unfolding listdiff_def by auto
next
  case (Cons y Y)
  from Cons.prems have 
    "y \<notin> set Y" and "distinct Y" and "y \<in> set X" and "set Y \<subseteq> set X"
    by (metis distinct.simps(2), 
      metis Cons(3) distinct.simps(2), 
      metis Cons(2) ListMem_iff elem subsetD, auto)
  from Cons.hyps [OF this(4) this(2)] have 
    "Y @ listdiff X Y <~~> X" using perm_sym by auto
  have "distinct (listdiff X Y)" using assms unfolding listdiff_def by auto
  let ?rhs = "(y # Y) @ listdiff X (y # Y)"
  have "?rhs = y # Y @ foldr removeAll (y#Y) X" 
    unfolding listdiff_is_fold_rem by auto
  also have "... = y # Y @ (removeAll y (foldr removeAll Y X))" by auto
  also have "... = y # Y @ (removeAll y (listdiff X Y))" 
    unfolding listdiff_is_fold_rem by auto
  also have "... = y # Y @ (remove1 y (listdiff X Y))"
    unfolding distinct_remove1_removeAll[OF `distinct (listdiff X Y)`] 
    by auto
  also have "... = y # (remove1 y (Y @ (listdiff X Y)))" 
    unfolding remove1_append using `y \<notin> set Y` by auto
  also have "... <~~> y # (remove1 y X)"
    by (intro perm.Cons perm_remove_perm, rule `Y @ listdiff X Y <~~> X`)
  finally have "?rhs <~~> y # (remove1 y X)" by auto
  moreover have "y # (remove1 y X) <~~> X" using `y \<in> set X` 
    by (metis perm_remove perm_sym)
  ultimately have "?rhs <~~> X" by auto
  thus ?case using perm_sym by auto
qed

lemma map_fst_pair:
  fixes a x
  shows "map fst (map (\<lambda>v. (v, a)) x) = x" 
by (induct x, auto)

lemma distinct_initials:
  fixes V \<Lambda> E
  assumes "wf_dia (Graph V \<Lambda> E)"
  shows "distinct (initials (Graph V \<Lambda> E))"
proof -
  from wf_dia_inv[OF assms] have "distinct V" by auto
  thus ?thesis unfolding initials.simps by auto
qed

lemma distinct_terminals:
  fixes V \<Lambda> E
  assumes "wf_dia (Graph V \<Lambda> E)"
  shows "distinct (terminals (Graph V \<Lambda> E))"
proof -
  from wf_dia_inv[OF assms] have "distinct V" by auto
  thus ?thesis unfolding terminals.simps by auto
qed

lemma map_filter_is_concat_map:
  fixes P X f
  shows "map f (filter P X) 
  = concat (map (\<lambda>x. if P x then [f x] else []) X)" 
  (is "?lhs = ?rhs") 
proof -
  have "?lhs = map f (concat (map (\<lambda>x. if P x then [x] else []) X))" 
    by (induct X, auto)
  also have "... = concat (map (map f) 
    (map (\<lambda>x. if P x then [x] else []) X))" 
    unfolding map_concat by auto
  also have "... = concat (map ((map f) \<circ> 
    (\<lambda>x. if P x then [x] else [])) X)"
    unfolding map_map by auto
  also have "... = concat (map 
    (\<lambda>x. (map f) (if P x then [x] else [])) X)" 
    unfolding comp_def by auto
  also have "... = concat (map 
    (\<lambda>x. if P x then (map f) [x] else (map f) []) X)" 
    unfolding if_distrib by auto
  also have "... = ?rhs" 
    unfolding map.simps by auto
  finally show ?thesis 
    by auto
qed

text {* If two lists have the same sets of elements, and neither has any duplicates, then they are permutations of each other. *}
lemma permI [intro]:
  fixes X Y
  assumes "set X = set Y" and "distinct X" and "distinct Y"
  shows "X <~~> Y"
proof -
  have "X = remdups X" 
    using distinct_remdups_id[OF assms(2), symmetric] by auto
  also have "...  <~~> remdups Y"
    using eq_set_perm_remdups[OF assms(1)] by auto
  also have "... = Y"
    using distinct_remdups_id[OF assms(3)] by auto
  finally show ?thesis by auto
qed

lemma if_and:
  fixes p q a b
  shows "(if p \<and> q then a else b) 
  = (if p then if q then a else b else b)" 
  by auto  

lemma set_listdiff: 
  fixes X Y
  shows "set (listdiff X Y) = set X - set Y"
  by (induct X, unfold listdiff_def, auto)

lemma listdiff_perm: 
  fixes X Y Z
  assumes "X <~~> Y"
  assumes "distinct X" "distinct Y"
  shows "listdiff X Z <~~> listdiff Y Z" 
proof -
  from assms(1) have "set X = set Y" using perm_set_eq by auto
  hence "set (listdiff X Z) = set (listdiff Y Z)" 
    using set_listdiff by metis
  moreover from assms(2) assms(3) have 
    "distinct (listdiff X Z)" "distinct (listdiff Y Z)"
    unfolding listdiff_def by auto
  ultimately show "listdiff X Z <~~> listdiff Y Z" 
    by (intro permI, auto)
qed

lemma inj_imp_inj_on: 
  fixes f X
  assumes "inj f"
  shows "inj_on f X" 
  by (metis subset_UNIV subset_inj_on assms)


lemma map_perm:
  fixes f X Y
  assumes "X <~~> Y"
  shows "map f X <~~> map f Y"
using assms
by (induct rule:perm.induct, auto)


lemma listdiff_append:
  fixes X Y Z
  shows "listdiff (X @ Y) Z = (listdiff X Z) @ (listdiff Y Z)" 
  unfolding listdiff_def
  by auto

lemma listdiff_id: 
  fixes X Y
  assumes "set X \<inter> set Y = {}"
  shows "listdiff X Y = X"
  unfolding listdiff_def
  using assms 
  by (induct X, auto)

lemma bigunion_subset: 
  "\<And>X Y S. X \<subseteq> Y \<Longrightarrow> (\<Union>x\<in>X. S) \<subseteq> (\<Union>x\<in>Y. S)"
  by auto

lemma all_but_one: 
  fixes P a X
  assumes "a \<in> X"
  shows "(P a \<and> (\<forall>x\<in>X. x\<noteq>a \<longrightarrow> P x)) = (\<forall>x\<in>X. P x)"
  by (metis assms)

lemma map_listdiff_inj:
  fixes f X Y
  assumes "inj f"
  shows "map f (listdiff X Y) = listdiff (map f X) (map f Y)"
unfolding listdiff_is_fold_rem
by (induct Y, auto simp add: map_removeAll_inj[OF assms])


lemma wf_chains2:
  fixes k 
  shows "\<And>S V \<Lambda> E \<Pi>. \<lbrakk> distinct S ; 
  set S \<subseteq> set (initials (Graph V \<Lambda> E)) ; 
  wf_dia (Graph V \<Lambda> E) ; \<Pi> \<in> rawchains2 S (Graph V \<Lambda> E) ; 
  length V + length E = k + length S \<rbrakk> 
  \<Longrightarrow> wf_rawchain \<Pi> \<and> 
  \<gamma> (post \<Pi>) <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]"
proof (induct k)
  case 0
  let ?\<sigma>1 = "[(v,Top). v \<leftarrow> initials (Graph V \<Lambda> E), v \<notin> set S]"
  let ?\<sigma>2 = "[(v,Bot). v \<leftarrow> S]"
  let ?\<sigma> = "?\<sigma>1 @ ?\<sigma>2"
  have tklgv: "distinct ?\<sigma>"
  proof -  
    let ?\<sigma>1 = "[(v,Top). v \<leftarrow> initials (Graph V \<Lambda> E), v \<notin> set S]"
    let ?\<sigma>2 = "[(v,Bot). v \<leftarrow> S]"
    have "distinct ?\<sigma>1"
      apply (unfold map_filter_is_concat_map [symmetric])
      apply (unfold distinct_map)
      apply (intro conjI)
      apply (intro distinct_filter)
      apply (rule distinct_initials[OF "0.prems"(3)])
      apply (unfold inj_on_def, simp)
      done
    moreover have "distinct ?\<sigma>2" 
      apply (unfold distinct_map)
      apply (intro conjI)
      apply (rule "0.prems"(1))
      apply (unfold inj_on_def, simp)
      done
    ultimately show ?thesis
      unfolding distinct_append
      by auto
  qed
  from wf_dia_inv [OF "0.prems"(3)] have 
    iecss:  "set (initials (Graph V \<Lambda> E)) \<subseteq> set V" and 
    nsckf: "distinct V" by auto
  from iecss and "0.prems"(2)
  have hfgey: "set S \<subseteq> set V" by auto
  from list_subseteq[OF "0.prems"(1) this] have
    dwcgc: "length S \<le> length V"  by auto
  from "0.prems"(5) have
    xglfj: "length V + length E = length S" by auto
  with dwcgc have pqshe: "length E = 0" by arith
  with xglfj have "length V = length S" by auto
  with distinct_card[OF nsckf] and distinct_card[OF "0.prems"(1)] 
  have rophe: "card (set V) = card (set S)" by auto
  have hpjzb: "set V = set S" 
  proof (rule ccontr)
    assume "set V \<noteq> set S"
    with hfgey have "finite (set V)" "set S \<subset> set V" by auto
    from psubset_card_mono[OF this] have 
      "card (set S) < card (set V)" by auto
    with rophe show False by auto
  qed
  with iecss and "0.prems"(2) have 
    dakuy: "set S = set (initials (Graph V \<Lambda> E))" and
    iuqxi: "set (initials (Graph V \<Lambda> E)) = set V" by auto
  from pqshe have wsegy: "set E = {}" by auto  
  hence hkimj: "E = []" by auto
  have xfbme: "?\<sigma>1 = []" using dakuy by auto
  from no_edges_imp_all_nodes_terminal and 
    no_edges_imp_all_nodes_initial and hkimj have 
    hjaws: "terminals (Graph V \<Lambda> E) = initials (Graph V \<Lambda> E)" by auto
  from hjaws dakuy have
    qoeqk: "set S = set (terminals (Graph V \<Lambda> E))" by auto
  hence socgi:
    "set ?\<sigma>2 = set [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]" by auto
  have "?\<sigma>2 <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]"
    apply (intro permI)
    apply (rule socgi)
    apply (metis "0.prems"(1) distinct_zipI1 map_fst_pair zip_map_fst_snd)
    apply (metis (no_types) `length V = length S` append_Nil card_distinct distinct_card hjaws hkimj length_map no_edges_imp_all_nodes_initial socgi tklgv xfbme)
    done
  hence 
    hislv: "?\<sigma> <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]"
    by (metis append_Nil xfbme)
  hence "set (map fst ?\<sigma>2) = set (terminals (Graph V \<Lambda> E))" 
    by (metis qoeqk map_fst_pair)
  from eq_set_perm_remdups[OF this]
  have
    cpzwf: "remdups (map fst ?\<sigma>2) 
    <~~> remdups (terminals (Graph V \<Lambda> E))" 
    by auto
  have "fst \<circ> (\<lambda>v. (v,Bot)) = id" by auto
  hence "map fst ?\<sigma>2 = S" by (metis map.id map_map map_fst_pair)
  with "0.prems"(1) have
    xecbe: "distinct (map fst ?\<sigma>2)" by auto
  hence uismw: "distinct (map fst ?\<sigma>)"
    using xfbme by (metis append_Nil)
  from distinct_remdups_id[OF xecbe] and
    distinct_remdups_id[OF distinct_terminals[OF "0.prems"(3)]] and
    cpzwf have
    arvry: "map fst ?\<sigma>2 <~~> terminals (Graph V \<Lambda> E)"
    by metis
  have eyzmp: "map fst ?\<sigma> <~~> terminals (Graph V \<Lambda> E)"
    using xfbme arvry by (metis append_Nil)
  from "0.prems"(4) obtain \<pi> where 
    mkaec: "\<Pi> = mk (cNil (\<alpha> ?\<sigma>)) \<pi>" and 
    "\<pi> \<in> lins2 S (Graph V \<Lambda> E)" 
    unfolding rawchains2_def by auto
  from this(2)
  have "distinct \<pi>"
    "set \<pi> = Inl ` (set V - set S) \<union> Inr ` set E"
    "\<forall>i j v e. i < length \<pi> \<and> j < length \<pi> \<and> \<pi> ! i = Inl v 
    \<and> \<pi> ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j"
    "\<forall>j k w e. j < length \<pi> \<and> k < length \<pi> \<and> \<pi> ! j = Inr e 
    \<and> \<pi> ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k"
    apply (unfold lins2.simps) 
    apply (elim CollectE conjE, assumption+)+ 
    done
  from this(2) and hpjzb and wsegy have
    "set \<pi> = {}" by auto
  hence "\<pi> = []" by auto
  with mkaec have 
    smliq: "\<Pi> = cNil (\<alpha> ?\<sigma>)"
    unfolding mk_def by auto
  hence vqpgq: "wf_rawchain \<Pi>" using wf_rawchain_cnil by auto
  from smliq have
    hhfar: "post \<Pi> = (\<alpha> ?\<sigma>)" by auto

  hence "\<gamma> (post \<Pi>) = \<gamma> (\<alpha> ?\<sigma>)" by auto
  also have "... <~~> ?\<sigma>" using conc_abs[of "?\<sigma>"] by auto
  finally have 
    ifega: "\<gamma> (post \<Pi>) <~~> ?\<sigma>" by auto
  with hislv have 
    "\<gamma> (post \<Pi>) <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]" by auto
  with vqpgq show ?case by auto
next
  case (Suc k)
  let ?\<sigma> = "[(v,Top). v \<leftarrow> initials (Graph V \<Lambda> E), v \<notin> set S] 
    @ [(v,Bot). v \<leftarrow> S]"
  have tklgv: "distinct ?\<sigma>"
  proof -  
    let ?\<sigma>1 = "[(v,Top). v \<leftarrow> initials (Graph V \<Lambda> E), v \<notin> set S]"
    let ?\<sigma>2 = "[(v,Bot). v \<leftarrow> S]"
    have "distinct ?\<sigma>1"
      apply (unfold map_filter_is_concat_map [symmetric])
      apply (unfold distinct_map)
      apply (intro conjI)
      apply (intro distinct_filter)
      apply (rule distinct_initials[OF Suc.prems(3)])
      apply (unfold inj_on_def, simp)
      done
    moreover have "distinct ?\<sigma>2" 
      apply (unfold distinct_map)
      apply (intro conjI)
      apply (rule Suc.prems(1))
      apply (unfold inj_on_def, simp)
      done
    ultimately show ?thesis
      unfolding distinct_append
      by auto
  qed
  from Suc.prems(4) obtain \<pi> where
    mkaec: "\<Pi> = mk (cNil (\<alpha> ?\<sigma>)) \<pi>" and 
    "\<pi> \<in> lins2 S (Graph V \<Lambda> E)" 
    unfolding rawchains2_def by auto
  from this(2)
  have 
    ujyes: "distinct \<pi>" and
    aqxbk: "set \<pi> = Inl ` (set V - set S) \<union> Inr ` set E" and
    myqpt: "\<forall>i j v e. i < length \<pi> \<and> j < length \<pi> \<and> \<pi> ! i = Inl v 
    \<and> \<pi> ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j" and
    zjtlg: "\<forall>j k w e. j < length \<pi> \<and> k < length \<pi> \<and> \<pi> ! j = Inr e 
    \<and> \<pi> ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k"
    apply (unfold lins2.simps) 
    apply (elim CollectE conjE, assumption+)+ 
    done

  from wf_dia_inv [OF Suc.prems(3)]
    have 
      jupgv: "set (initials (Graph V \<Lambda> E)) \<subseteq> set V" and 
      nsckf: "distinct V" and 
      xfrmj: "acyclicity E" and 
      fivyp: "linearity E" and
      joven: "\<And>e. e \<in> set E \<Longrightarrow> distinct (fst3 e) 
      \<and> set (fst3 e) \<subseteq> set V" and 
      tbdcm: "\<And>e. e \<in> set E \<Longrightarrow> distinct (thd3 e) 
      \<and> set (thd3 e) \<subseteq> set V" 
      by auto      
    from this(1) and Suc.prems(2)
    have hfgey: "set S \<subseteq> set V" by auto

  show "wf_rawchain \<Pi> \<and> \<gamma> (post \<Pi>)
    <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]"
  proof (cases "\<pi>")
    case Nil
    hence "set \<pi> = {}" by auto
    hence "Inl ` (set V - set S) \<union> Inr ` set E = {}" 
      using aqxbk by auto
    hence "Inl ` (set V - set S) = {}" and "Inr ` set E = {}"
      by auto
    hence "(set V - set S) = {}" and "set E = {}" by auto
    hence "set V \<subseteq> set S" and ruaau: "E = []" by auto
    with hfgey have "set V = set S" by auto
    hence "card (set V) = card (set S)" by auto
    with distinct_card[OF nsckf] and distinct_card[OF Suc.prems(1)] 
      and ruaau have
      "length V = length S" and "length E = 0" by auto
    with Suc.prems(5) have "Suc k = 0" by auto
    hence False by auto
    thus ?thesis by auto
  next
    case (Cons x \<pi>')
    hence yketi: "\<pi> = x # \<pi>'" by auto
    let ?f = "\<lambda>\<Pi>. sum_case 
      (\<lambda>v. cSnoc \<Pi> (Inl v) (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Top)]) 
      @ [(v,Bot)]))) 
      (\<lambda>e. cSnoc \<Pi> (Inr e) 
      (\<alpha> ((listdiff (\<gamma> (post \<Pi>)) [(v,Bot) . v \<leftarrow> fst3 e]) @ 
      [(v,Top) . v \<leftarrow> thd3 e])))"
    from yketi mkaec have
      "\<Pi> = foldl ?f (cNil (\<alpha> ?\<sigma>)) (x # \<pi>')" 
      unfolding mk_def by auto
    hence ulrqd: "\<Pi> = foldl ?f (?f (cNil (\<alpha> ?\<sigma>)) x) \<pi>'"
      by (unfold foldl.simps(2), auto)
    show ?thesis
    proof (cases x)
      case (Inl v)
      hence hnqdb: "x = Inl v" by auto
      with ulrqd have 
        "\<Pi> = foldl ?f (?f (cNil (\<alpha> ?\<sigma>)) (Inl v)) \<pi>'" by auto
      hence "\<Pi> = foldl ?f 
        (cSnoc (cNil (\<alpha> ?\<sigma>)) (Inl v) (\<alpha> ((listdiff 
        (\<gamma> (post (cNil (\<alpha> ?\<sigma>)))) [(v,Top)]) @ [(v,Bot)]))) \<pi>'"
        by simp
      hence "\<Pi> = foldl ?f
        (cCons (\<alpha> ?\<sigma>) (Inl v) (cNil (\<alpha> ((listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Top)]) 
        @ [(v,Bot)])))) \<pi>'" 
        by auto
      hence "\<Pi> = mk (cCons (\<alpha> ?\<sigma>) (Inl v) 
        (cNil (\<alpha> ((listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Top)]) @ [(v,Bot)])))) \<pi>'" 
        unfolding mk_def by auto
      hence lmkbq: "\<Pi> = cCons (\<alpha> ?\<sigma>) (Inl v) (mk 
        (cNil (\<alpha> ((listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Top)]) @ [(v,Bot)]))) \<pi>')" 
        (is "_ = cCons _ _ ?\<Pi>'") 
        using mk_ccons by auto
      from yketi hnqdb have "(Inl v) \<in> set \<pi>" by auto
      with aqxbk have "v \<in> set V - set S" by auto
      hence cygbs: "v \<in> set V" and kaucq: "v \<notin> set S" by auto
      from kaucq and Suc.prems(1) have 
        cuztr: "distinct (v#S)" by auto 
      have bjmwl: "v \<in> set (initials (Graph V \<Lambda> E))" 
      proof (rule ccontr)
        assume "v \<notin> set (initials (Graph V \<Lambda> E))"
        hence "v \<notin> set [v\<leftarrow>V . v \<notin> set (concat (map thd3 E))]" by auto
        with cygbs have "v \<in> set (concat (map thd3 E))" by auto
        then obtain e where "e \<in> set E" and sscmh: "v \<in> set (thd3 e)"
          by auto
        from aqxbk this(1) have "Inr e \<in> set \<pi>" by auto
        then obtain j where "\<pi>!j = Inr e" and "j < length \<pi>" 
          unfolding in_set_conv_nth by auto
        moreover from yketi hnqdb have "\<pi>!0 = Inl v" and "0 < length \<pi>"
          by auto
        ultimately have "j < 0" using zjtlg sscmh by metis
        thus False by auto
      qed       
      with Suc.prems(2) have 
        fthcv: "set (v#S) \<subseteq> set (initials (Graph V \<Lambda> E))" 
        by auto
      have "((listdiff 
        (\<gamma> (\<alpha> ([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
        @ [(w,Bot). w \<leftarrow> S]))) [(v, Top)]) @ [(v, Bot)]) 
        <~~> ([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set (v#S)] 
        @ [(w,Bot). w \<leftarrow> (v#S)])" (is "?lhs <~~> ?rhs") 
      proof -
        have wargt: "inj (\<lambda>w. (w, Top))"
          by (metis (no_types) Pair_inject injI)
        have kblbw: "\<And>X y. listdiff X [y] = removeAll y X" 
          unfolding listdiff_is_fold_rem by auto
        have pudxd: "(v,Top) \<notin> set (map (\<lambda>w. (w, Bot)) S)" 
          by auto
        have "?rhs = concat 
          (map (\<lambda>w. if w \<noteq> v \<and> w \<notin> set S then [(w, Top)] else []) 
          (initials (Graph V \<Lambda> E))) 
          @ map (\<lambda>w. (w, Bot)) (v#S)" by auto
        also have "... = map (\<lambda>w. (w, Top)) 
          (filter (\<lambda>w. w \<noteq> v \<and> w \<notin> set S) (initials (Graph V \<Lambda> E))) 
          @ map (\<lambda>w. (w, Bot)) (v#S)" 
          unfolding map_filter_is_concat_map by auto
        also have "... = map (\<lambda>w. (w, Top)) (filter (op \<noteq> v) 
          (filter (\<lambda>w. w \<notin> set S) (initials (Graph V \<Lambda> E))))
          @ map (\<lambda>w. (w, Bot)) (v#S)" 
          unfolding filter_filter conj_commute neq_commute by auto
        also have "... = map (\<lambda>w. (w, Top)) 
          (removeAll v [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S]) 
          @ map (\<lambda>w. (w, Bot)) (v#S)"
          unfolding removeAll_filter_not_eq by auto
        also have "... = removeAll (v, Top) 
          (map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S]) 
          @ map (\<lambda>w. (w, Bot)) (v#S)"
          unfolding map_removeAll_inj[OF wargt] by auto
        also have "... = removeAll (v, Top) 
          (map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S]) 
          @ [(v,Bot)] @ map (\<lambda>w. (w, Bot)) S" by auto
        also have "... <~~> removeAll (v, Top) 
          (map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S]) 
          @ map (\<lambda>w. (w, Bot)) S @ [(v,Bot)]" 
          by (metis perm_append1 perm_append_swap)
        also have "... = removeAll (v, Top) 
          (map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S]) 
          @ removeAll (v, Top) (map (\<lambda>w. (w, Bot)) S) @ [(v, Bot)]"
          unfolding removeAll_id[OF pudxd] by auto
        also have "... = removeAll (v, Top) 
          ((map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S]) 
          @ (map (\<lambda>w. (w, Bot)) S)) @ [(v, Bot)]"
          by auto
        also have "... = (listdiff 
          ((map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S]) 
          @ (map (\<lambda>w. (w, Bot)) S)) [(v,Top)]) @ [(v, Bot)]" 
          unfolding kblbw by auto
        finally have "?rhs <~~> (listdiff 
          ((([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
          @ [(w,Bot). w \<leftarrow> S]))) [(v, Top)]) @ [(v, Bot)]" 
          unfolding map_filter_is_concat_map by auto
        moreover
        have "(listdiff 
          ((([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
          @ [(w,Bot). w \<leftarrow> S]))) [(v, Top)]) @ [(v, Bot)] <~~> ?lhs" 
        proof (intro perm_append2 listdiff_perm)
          show "([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
          @ [(w,Bot). w \<leftarrow> S]) <~~> 
            \<gamma> (\<alpha> ([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
          @ [(w,Bot). w \<leftarrow> S]))" 
            using perm_sym[OF conc_abs[of 
              "[(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
              @ [(w,Bot). w \<leftarrow> S]"]] by auto
        next
          show "distinct ([(w,Top). 
            w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
          @ [(w,Bot). w \<leftarrow> S])" by (metis tklgv)
        next
          show "distinct (\<gamma> (\<alpha> ([(w,Top). 
            w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
          @ [(w,Bot). w \<leftarrow> S])))" 
            by (metis (no_types) conc_abs listdiff_def 
              map_filter_is_concat_map maps_def 
              perm_distinct_iff tklgv)
        qed
        ultimately have "?rhs <~~> ?lhs" by (rule perm.trans)
        thus ?thesis by (rule perm_sym)
      qed
      hence jtgmn: "\<alpha> ((listdiff 
        (\<gamma> (\<alpha> ([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
        @ [(w,Bot). w \<leftarrow> S]))) [(v, Top)]) @ [(v, Bot)]) 
        = \<alpha> ([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set (v#S)] 
        @ [(w,Bot). w \<leftarrow> (v#S)])" using abs_equiv by auto
      have jvlal: "?\<Pi>' \<in> rawchains2 (v#S) (Graph V \<Lambda> E)"
        unfolding rawchains2_def unfolding jtgmn
      proof (intro CollectI exI[of _ \<pi>'] conjI, simp,
          unfold lins2.simps(1), intro CollectI conjI)
        from ujyes yketi show "distinct \<pi>'" by auto
      next
        show "set \<pi>' = Inl ` (set V - set (v#S)) \<union> Inr ` set E" 
          (is "?lhs = ?rhs") 
        proof -
          have "?rhs = Inl ` (set V - set S - {v}) \<union> Inr ` set E" 
            by auto
          also have "... = set \<pi> - {Inl v}" using aqxbk by auto
          also have "... = set (removeAll (Inl v) \<pi>)" 
            unfolding set_removeAll by auto
          also have "... = set (remove1 (Inl v) \<pi>)"
            using distinct_remove1_removeAll[OF ujyes] by auto
          also have "... = set (remove1 (Inl v) ((Inl v)#\<pi>'))" 
            using yketi hnqdb by auto
          also have "... = ?lhs" by auto
          finally show ?thesis by auto
        qed
      next
        show "\<forall>i j v e. i < length \<pi>' \<and> j < length \<pi>' \<and> \<pi>' ! i = Inl v 
          \<and> \<pi>' ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j" 
        proof (intro allI impI, (erule conjE)+)
          fix i j v e
          assume "i < length \<pi>'" and "j < length \<pi>'" 
            and "\<pi>' ! i = Inl v" and "\<pi>' ! j = Inr e"
          hence "i+1 < length \<pi>" "j+1 < length \<pi>"
            "\<pi>!(i+1) = Inl v" "\<pi>!(j+1) = Inr e" 
            using yketi by auto
          moreover
          assume "v \<in> set (fst3 e)"
          ultimately have "i+1 < j+1" using myqpt by metis          
          thus "i < j" by auto
        qed
      next
        show "\<forall>j k w e. j < length \<pi>' \<and> k < length \<pi>' \<and> \<pi>' ! j = Inr e 
          \<and> \<pi>' ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k"
        proof (intro allI impI, (erule conjE)+)
          fix j k w e
          assume "j < length \<pi>'" and "k < length \<pi>'" 
            and "\<pi>' ! j = Inr e" and "\<pi>' ! k = Inl w"
          hence "j+1 < length \<pi>" "k+1 < length \<pi>" "\<pi>!(j+1) = Inr e"
            "\<pi>!(k+1) = Inl w" 
            using yketi by auto
          moreover
          assume "w \<in> set (thd3 e)"
          ultimately have "j+1 < k+1" using zjtlg by metis          
          thus "j < k" by auto
        qed
      qed
      from Suc.prems(5) 
      have favzl: "length V + length E = k + length (v#S)" by auto
      from Suc.hyps[OF cuztr fthcv Suc.prems(3) jvlal favzl] have
        mapkz: "wf_rawchain ?\<Pi>'" and 
        uzlwq: "\<gamma> (post ?\<Pi>') <~~> 
        [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]" 
        by auto
      let ?\<sigma>' = "remove1 (v,Top) ?\<sigma>"
      from bjmwl and kaucq have "(v,Top) \<in> set ?\<sigma>" by auto
      from perm_remove[OF this]
      have ppefa: "?\<sigma> <~~> [(v, Top)] @ ?\<sigma>'" by auto
      from tklgv have zuuso: "distinct (\<gamma> (\<alpha> ?\<sigma>))" 
        by (metis (no_types) conc_abs perm_distinct_iff)
      have vpcvj: "pre ?\<Pi>' 
        = \<alpha> ((listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Top)]) @ [(v,Bot)])" 
        using pre_mk by auto
      have "listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Top)] 
        = removeAll (v,Top) (\<gamma> (\<alpha> ?\<sigma>))"
        using listdiff_is_fold_rem[of "(\<gamma> (\<alpha> ?\<sigma>))" "[(v,Top)]"] by auto
      also have "... = remove1 (v,Top) (\<gamma> (\<alpha> ?\<sigma>))" 
        using distinct_remove1_removeAll[OF zuuso] by auto
      also have "... <~~> remove1 (v,Top) ?\<sigma>"
        by (rule perm_remove_perm, rule conc_abs)
      finally have "listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Top)] <~~> ?\<sigma>'" 
        by auto
      hence "listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Top)] @ [(v,Bot)] 
        <~~> ?\<sigma>' @ [(v,Bot)]" by auto
      from abs_equiv[OF this] have 
        "\<alpha> (listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Top)] @ [(v,Bot)]) 
        = \<alpha> (?\<sigma>' @ [(v,Bot)])" by auto
      with vpcvj have "pre ?\<Pi>' = \<alpha> (?\<sigma>' @ [(v,Bot)])" by auto
      hence "\<gamma> (pre ?\<Pi>') <~~> ?\<sigma>' @ [(v,Bot)]" 
        using conc_abs by auto
      moreover have "?\<sigma>' @ [(v,Bot)] <~~> [(v, Bot)] @ ?\<sigma>'" 
        by (metis perm_append_swap)
      ultimately have otqat: "\<gamma> (pre ?\<Pi>') <~~>  [(v, Bot)] @ ?\<sigma>'" 
        by (rule perm.trans)
      from wf_rawchain_ccons_inl[OF ppefa otqat mapkz] lmkbq
      have "wf_rawchain \<Pi>" by auto 
      moreover
      from lmkbq have "post \<Pi> = post ?\<Pi>'" by auto
      with uzlwq have 
        "\<gamma> (post \<Pi>) <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]"
        by auto
      ultimately show ?thesis by auto
    next
      case (Inr e)
      hence hnqdb: "x = Inr e" by auto
      with ulrqd have 
        "\<Pi> = foldl ?f (?f (cNil (\<alpha> ?\<sigma>)) (Inr e)) \<pi>'" by auto
      hence "\<Pi> = foldl ?f 
        (cSnoc (cNil (\<alpha> ?\<sigma>)) (Inr e) (\<alpha> ((listdiff 
        (\<gamma> (post (cNil (\<alpha> ?\<sigma>)))) [(v,Bot). v \<leftarrow> fst3 e]) 
        @ [(v,Top). v \<leftarrow> thd3 e]))) \<pi>'"
        by simp
      hence "\<Pi> = foldl ?f
        (cCons (\<alpha> ?\<sigma>) (Inr e) (cNil (\<alpha> ((listdiff (\<gamma> (\<alpha> ?\<sigma>)) 
        [(v,Bot). v\<leftarrow>fst3 e]) 
        @ [(v,Top). v \<leftarrow> thd3 e])))) \<pi>'" 
        by auto
      hence "\<Pi> = mk (cCons (\<alpha> ?\<sigma>) (Inr e) 
        (cNil (\<alpha> ((listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Bot). v\<leftarrow>fst3 e]) 
        @ [(v,Top). v\<leftarrow>thd3 e])))) \<pi>'" 
        unfolding mk_def by auto
      hence lmkbq: "\<Pi> = cCons (\<alpha> ?\<sigma>) (Inr e) (mk 
        (cNil (\<alpha> ((listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Bot). v\<leftarrow>fst3 e]) 
        @ [(v,Top). v\<leftarrow>thd3 e]))) \<pi>')" 
        (is "_ = cCons _ _ ?\<Pi>'") 
        using mk_ccons by auto

      from yketi hnqdb have "(Inr e) \<in> set \<pi>" by auto
      with aqxbk have "e \<in> set E" by auto
      with joven [OF this] tbdcm[OF this] have
        rodmt: "set (fst3 e) \<subseteq> set V" and
        bjcek: "distinct (fst3 e)" and
        ptyhv: "set (thd3 e) \<subseteq> set V" and
        nyneq: "distinct (thd3 e)" by auto
      
      
      let ?\<sigma>' = "listdiff ?\<sigma> [(v,Bot). v\<leftarrow>fst3 e]"

      have bjmwl: "set (fst3 e) \<subseteq> set S" 
      proof (intro subsetI)
        fix v
        assume nloqn: "v \<in> set (fst3 e)"
        with rodmt have xhrjc: "v \<in> set V" by auto
        show "v \<in> set S"
        proof (rule ccontr)
          assume "v \<notin> set S"
          with xhrjc have "v \<in> set V - set S" by auto
          with aqxbk have "Inl v \<in> set \<pi>" by auto
          then obtain i where "\<pi>!i = Inl v" and "i < length \<pi>" 
            unfolding in_set_conv_nth by auto
          moreover from yketi hnqdb have 
            "\<pi>!0 = Inr e" and "0 < length \<pi>"
            by auto
          ultimately have "i<0" using nloqn myqpt by metis
          thus False by auto
        qed
      qed  

      let ?V' = "listdiff V (fst3 e)"
      let ?E' = "listdiff E [e]"
      let ?S' = "listdiff S (fst3 e)"

      from Suc.prems(1) have
        cuztr: "distinct (?S')" 
        unfolding listdiff_def by auto
      
      have fthcv: "set (?S') \<subseteq> set (initials (Graph ?V' \<Lambda> ?E'))" 
      proof (intro subsetI)
        fix v
        assume "v \<in> set (listdiff S (fst3 e))"
        hence "v \<in> set S - set (fst3 e)" 
          by (unfold set_listdiff, auto)
        hence 
          biyvo: "v \<in> set S" and
          mpyux: "v \<notin> set (fst3 e)" by auto
        from biyvo have "v \<in> set (initials (Graph V \<Lambda> E))" 
          using Suc.prems(2) by auto
        hence "v \<in> set V" and dnwmt: "v \<notin> set (concat (map thd3 E))" 
          by auto
        from this(1) and mpyux have "v \<in> set V - set (fst3 e)" by auto
        hence sdrkm: "v \<in> set (listdiff V (fst3 e))"
          by (unfold set_listdiff, auto)
        have uyyio: "v \<notin> set (concat (map thd3 (listdiff E [e])))" 
        proof (rule ccontr)
          assume "\<not> v \<notin> set (concat (map thd3 (listdiff E [e])))"
          hence "v \<in> set (concat (map thd3 (listdiff E [e])))" by auto
          then obtain f where "f \<in> set (listdiff E [e])" 
            and gopfu: "v \<in> set (thd3 f)" by auto
          from this(1) have "f \<in> set E" and "f\<noteq>e"
            by (unfold set_listdiff, auto)
          with gopfu have "v \<in> set (concat (map thd3 E))" by auto
          with dnwmt show False by auto
        qed
        from sdrkm uyyio show 
          "v \<in> set (initials (Graph (listdiff V (fst3 e)) \<Lambda> 
          (listdiff E [e])))"
          by auto
      qed

      from fivyp have 
        brrov: "distinct E" and
        rwiiv: "\<And>e f.\<lbrakk> e\<in>set E; f\<in>set E; e \<noteq> f \<rbrakk> \<Longrightarrow> 
        set (fst3 e) \<inter> set (fst3 f) = {} 
        \<and> set (thd3 e) \<inter> set (thd3 f) = {}"
        unfolding linearity_def by auto

      have shifk: "wf_dia (Graph ?V' \<Lambda> ?E')" 
      proof (intro wf_dia)
        show "distinct (listdiff V (fst3 e))" 
          unfolding listdiff_def using nsckf by auto
      next
        show "acyclicity (listdiff E [e])"
          using xfrmj
          unfolding acyclicity_def listdiff_def
        proof (elim acyclic_subset)
          have "set [x\<leftarrow>E . x \<notin> set [e]] \<subseteq> set E" by auto
          from bigunion_subset[OF this]
          show "(\<Union>e\<in>set [x\<leftarrow>E . x \<notin> set [e]]. 
            \<Union>v\<in>set (fst3 e). \<Union>w\<in>set (thd3 e). {(v, w)})
            \<subseteq> (\<Union>e\<in>set E. 
            \<Union>v\<in>set (fst3 e). \<Union>w\<in>set (thd3 e). {(v, w)})" by auto
        qed
      next
        show "linearity (listdiff E [e])"
          by (unfold linearity_def, intro conjI, 
            unfold listdiff_def, simp add: brrov, 
            intro ballI impI conjI, (simp add: rwiiv)+)        
      next
        fix f
        assume "f \<in> set (listdiff E [e])"
        hence "f \<in> set E" and "f \<noteq> e" unfolding listdiff_def by auto 
        from joven[OF this(1)] have "set (fst3 f) \<subseteq> set V" and
          bqbem: "distinct (fst3 f)" by auto
        moreover have "set (fst3 f) \<inter> set (fst3 e) = {}" 
          using rwiiv[OF `f \<in> set E` `e \<in> set E` `f \<noteq> e`] by auto
        ultimately have "set (fst3 f) \<subseteq> (set V - set (fst3 e))" by auto
        also have "... = (set (listdiff V (fst3 e)))" 
          unfolding listdiff_def by auto
        finally have "(set (fst3 f)) \<subseteq> (set (listdiff V (fst3 e)))" 
          by auto
        thus "distinct (fst3 f) \<and>
          (set (fst3 f)) \<subseteq> (set (listdiff V (fst3 e)))" using bqbem 
          by auto
      next
        fix f
        assume "f \<in> set (listdiff E [e])"
        hence "f \<in> set E" and "f \<noteq> e" unfolding listdiff_def by auto 
        from tbdcm[OF this(1)] have "set (thd3 f) \<subseteq> set V" and 
          nxvti: "distinct (thd3 f)" by auto
        moreover have "set (thd3 f) \<inter> set (fst3 e) = {}" 
        proof (rule ccontr)
          assume "set (thd3 f) \<inter> set (fst3 e) \<noteq> {}"
          then obtain w where "w \<in> set (thd3 f)" and 
            lghfv: "w \<in> set (fst3 e)" by auto
          from this(1) have "w \<notin> set (initials (Graph V \<Lambda> E))" 
            using `f \<in> set E` by auto
          moreover 
          from bjmwl lghfv Suc.prems(2) have 
            "w \<in> set (initials (Graph V \<Lambda> E))" by auto
          ultimately show False by auto
        qed
        ultimately have "set (thd3 f) \<subseteq> (set V - set (fst3 e))" by auto
        also have "... = (set (listdiff V (fst3 e)))" 
          unfolding listdiff_def by auto
        finally have "(set (thd3 f)) \<subseteq> (set (listdiff V (fst3 e)))"
          by auto
        thus "distinct (thd3 f) \<and>
          (set (thd3 f)) \<subseteq> (set (listdiff V (fst3 e)))" 
          using nxvti by auto
      qed

      have "((listdiff 
        (\<gamma> (\<alpha> ([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
        @ [(w,Bot). w \<leftarrow> S]))) [(v, Bot). v\<leftarrow>fst3 e]) 
        @ [(v, Top). v\<leftarrow>thd3 e]) 
        <~~> ([(w,Top). w \<leftarrow> initials (Graph ?V' \<Lambda> ?E'), w \<notin> set ?S'] 
        @ [(w,Bot). w \<leftarrow> ?S'])" (is "?lhs <~~> ?rhs") 
      
      proof -
        have wargt: "\<And>a. inj (\<lambda>w. (w, a))"
          by (metis (no_types) Pair_inject injI)

        have ohruf:
          "set (map (\<lambda>w. (w, Top)) 
          (filter (\<lambda>w. w \<notin> set S \<or> w \<in> set (fst3 e))
          (initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e]))))) 
          \<inter> set (map (\<lambda>w. (w, Bot)) (fst3 e)) = {}" by auto

        have jxzvk: "set (map (\<lambda>v. (v, Top)) (thd3 e)) 
          \<inter> set (map (\<lambda>v. (v, Bot)) (fst3 e)) = {}" by auto

        have "?rhs = map (\<lambda>w. (w, Top)) 
          (filter (\<lambda>w. w \<notin> set (listdiff S (fst3 e))) 
          (initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])))) 
          @ map (\<lambda>w. (w, Bot)) (listdiff S (fst3 e))" 
          unfolding map_filter_is_concat_map by auto
        also have "... = map (\<lambda>w. (w, Top)) 
          (filter (\<lambda>w. w \<notin> (set S - set (fst3 e)))
          (initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])))) 
          @ map (\<lambda>w. (w, Bot)) (listdiff S (fst3 e))" 
          unfolding listdiff_def by auto
        also have "... = map (\<lambda>w. (w, Top)) 
          (filter (\<lambda>w. w \<notin> set S \<or> w \<in> set (fst3 e))
          (initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])))) 
          @ map (\<lambda>w. (w, Bot)) (listdiff S (fst3 e))" 
          by auto
        also have "... = map (\<lambda>w. (w, Top)) 
          (filter (\<lambda>w. w \<notin> set S \<or> w \<in> set (fst3 e))
          (initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])))) 
          @ listdiff (map (\<lambda>w. (w, Bot)) S) (map (\<lambda>w. (w, Bot)) (fst3 e))" 
          using map_listdiff_inj[OF wargt[of "Bot"]] by auto
        also have "... = listdiff (map (\<lambda>w. (w, Top)) 
          (filter (\<lambda>w. w \<notin> set S \<or> w \<in> set (fst3 e))
          (initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e]))))) 
          (map (\<lambda>w. (w, Bot)) (fst3 e)) 
          @ listdiff (map (\<lambda>w. (w, Bot)) S) (map (\<lambda>w. (w, Bot)) (fst3 e))"
          unfolding listdiff_id[OF ohruf] by auto
        also have "... = listdiff ((map (\<lambda>w. (w, Top)) 
          (filter (\<lambda>w. w \<notin> set S \<or> w \<in> set (fst3 e))
          (initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e]))))) 
          @ (map (\<lambda>w. (w, Bot)) S)) (map (\<lambda>w. (w, Bot)) (fst3 e))" 
          unfolding listdiff_append by auto

        also have "... <~~> listdiff (((map (\<lambda>w. (w,Top)) 
          (filter (\<lambda>w. w\<notin>set S) (initials (Graph V \<Lambda> E)))) 
          @ map (\<lambda>w. (w, Bot)) S) @
          (map (\<lambda>v. (v, Top)) (thd3 e))) (map (\<lambda>v. (v, Bot)) (fst3 e))" 
        proof (intro listdiff_perm)
          have "map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])) 
            . w \<notin> set S \<or> w \<in> set (fst3 e)] @ map (\<lambda>w. (w, Bot)) S 
            <~~> (map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S] 
            @ map (\<lambda>v. (v, Top)) (thd3 e)) @ map (\<lambda>w. (w, Bot)) S"
          proof (intro perm_append2)
            have "map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])) .
              w \<notin> set S \<or> w \<in> set (fst3 e)] <~~> map (\<lambda>w. (w, Top)) ([w\<leftarrow>initials (Graph V \<Lambda> E) .
              w \<notin> set S] @ (thd3 e))" 
            proof (intro map_perm)
              let ?lhs = "[w\<leftarrow>initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])) .
                w \<notin> set S \<or> w \<in> set (fst3 e)]"
              let ?rhs = "[w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S] @ thd3 e"
              
              have "?lhs = [w\<leftarrow>listdiff V (fst3 e) . 
                (\<forall>f\<in>set (listdiff E [e]). w \<notin> set (thd3 f)) 
                \<and> (w \<in> set S \<longrightarrow> w \<in> set (fst3 e))]" by auto
              also have "... = [w\<leftarrow>V . w \<notin> set (fst3 e) 
                \<and> (\<forall>f. f \<in> set E \<and> f \<noteq> e \<longrightarrow> w \<notin> set (thd3 f)) 
                \<and> (w \<in> set S \<longrightarrow> w \<in> set (fst3 e))]"
                unfolding listdiff_def by auto
              also have "... <~~> [w\<leftarrow>V . (\<forall>a\<in>set E. w \<notin> set (thd3 a)) \<and> w \<notin> set S] @ thd3 e" 
              proof (intro permI)
                show "set [w\<leftarrow>V . w \<notin> set (fst3 e) \<and> (\<forall>f. f \<in> set E \<and> f \<noteq> e 
                  \<longrightarrow> w \<notin> set (thd3 f)) \<and> (w \<in> set S \<longrightarrow> w \<in> set (fst3 e))] 
                  = set ([w\<leftarrow>V . (\<forall>a\<in>set E. w \<notin> set (thd3 a)) \<and> w \<notin> set S] @ thd3 e)" 
                  unfolding set_append set_filter
                proof (auto)
                  fix v
                  assume "v \<notin> set S" and "v \<in> set (fst3 e)"
                  thus "False" using `set (fst3 e) \<subseteq> set S` by auto
                next
                  fix v
                  assume "v \<in> set (thd3 e)"
                  thus "v \<in> set V" by (metis ptyhv subsetD)
                next
                  fix v
                  assume "v \<in> set (thd3 e)" "v \<in> set (fst3 e)"
                  with `e \<in> set E` have
                    "(v,v) \<in> (\<Union>e\<in>set E. \<Union>v\<in>set (fst3 e). \<Union>w\<in>set (thd3 e). {(v, w)})" 
                    by auto
                  hence "(v,v) \<in> (\<Union>e\<in>set E. \<Union>v\<in>set (fst3 e). \<Union>w\<in>set (thd3 e). {(v, w)})^+"
                    by auto
                  with xfrmj show "False" unfolding acyclicity_def acyclic_def by auto
                next
                  fix v vs c ws
                  assume "v \<in> set (thd3 e)" and "(vs, c, ws) \<in> set E" 
                    and "(vs, c, ws) \<noteq> e" and "v \<in> set (thd3 (vs, c, ws))"
                  thus "False" by (metis (no_types) Collect_conj_eq Collect_def
                    Int_absorb Int_def `e \<in> set E` `v \<in> set (thd3 (vs, c, ws))`
                    `v \<in> set (thd3 e)` bot_empty_eq bot_fun_def emptyE inf1I rwiiv)
                next
                  fix v
                  assume uewqy: "v \<in> set (thd3 e)" 
                  assume "v \<in> set S"
                  hence "v \<in> set (initials (Graph V \<Lambda> E))" 
                    by (metis Suc.prems(2) subsetD)
                  hence "\<forall>a\<in>set E. v \<notin> set (thd3 a)" by auto
                  with uewqy `e \<in> set E` have False by auto
                  thus "v \<in> set (fst3 e)" by auto
                qed
              next
                show "distinct [w\<leftarrow>V . w \<notin> set (fst3 e) \<and> (\<forall>f. f \<in> set E \<and> f \<noteq> e \<longrightarrow> w \<notin> set (thd3 f)) 
                  \<and> (w \<in> set S \<longrightarrow> w \<in> set (fst3 e))]" using `distinct V` by auto
              next
                show "distinct ([w\<leftarrow>V . (\<forall>a\<in>set E. w \<notin> set (thd3 a)) \<and> w \<notin> set S] @ thd3 e)"
                  apply (unfold distinct_append, intro conjI, auto simp add: `distinct V`)
                  apply (metis nyneq)
                proof -
                  fix w
                  assume "w \<in> set (thd3 e)" and "\<forall>a\<in>set E. w \<notin> set (thd3 a)" 
                  with `e \<in> set E` show "False" by auto
                qed
              qed
              also have "... = ?rhs" by auto
              finally show "?lhs <~~> ?rhs" by auto
            qed
          moreover
            have "map (\<lambda>w. (w, Top)) ([w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S] @ (thd3 e))
              <~~> map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S] 
              @ map (\<lambda>v. (v, Top)) (thd3 e)" by auto
           ultimately show "map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph (listdiff V (fst3 e)) 
             \<Lambda> (listdiff E [e])) . w \<notin> set S \<or> w \<in> set (fst3 e)] 
             <~~> map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S] 
             @ map (\<lambda>v. (v, Top)) (thd3 e)" by auto
          qed           
          moreover have "(map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S] 
            @ map (\<lambda>v. (v, Top)) (thd3 e)) @ map (\<lambda>w. (w, Bot)) S 
            <~~> (map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S] 
            @ map (\<lambda>w. (w, Bot)) S) @ map (\<lambda>v. (v, Top)) (thd3 e)" 
            by (metis append_assoc perm_append1 perm_append_swap)
          ultimately show "map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph 
            (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])) . w \<notin> set S \<or> w \<in> set (fst3 e)] 
            @ map (\<lambda>w. (w, Bot)) S <~~> (map (\<lambda>w. (w, Top)) 
            [w\<leftarrow>initials (Graph V \<Lambda> E) . w \<notin> set S] @ map (\<lambda>w. (w, Bot)) S) 
            @ map (\<lambda>v. (v, Top)) (thd3 e)" by auto
        next
          have 
            vqyuv: "distinct (initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])))" 
            by (unfold initials.simps, intro distinct_filter, unfold listdiff_def, 
              intro distinct_filter, rule `distinct V`)
          show "distinct (map (\<lambda>w. (w, Top)) 
            [w\<leftarrow>initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])) .
            w \<notin> set S \<or> w \<in> set (fst3 e)] @ map (\<lambda>w. (w, Bot)) S)" 
          proof (unfold distinct_append, intro conjI)
            show "distinct (map (\<lambda>w. (w, Top)) 
              [w\<leftarrow>initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])) 
              . w \<notin> set S \<or> w \<in> set (fst3 e)])"
            proof (unfold distinct_map, intro conjI)
              show "distinct [w\<leftarrow>initials (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])) 
                . w \<notin> set S \<or> w \<in> set (fst3 e)]" 
                using vqyuv by (metis (no_types) distinct_filter)
            next
              show "inj_on (\<lambda>w. (w, Top)) (set [w\<leftarrow>initials 
                (Graph (listdiff V (fst3 e)) \<Lambda> (listdiff E [e])) 
                . w \<notin> set S \<or> w \<in> set (fst3 e)])" 
                using inj_imp_inj_on[OF wargt[of "Top"]] by auto 
            qed
          next
            show "distinct (map (\<lambda>w. (w, Bot)) S)" 
              by (metis Suc(2) distinct_zipI1 map_fst_pair zip_map_fst_snd)
          qed (auto)
        next
          show "distinct ((map (\<lambda>w. (w, Top)) [w\<leftarrow>initials (Graph V \<Lambda> E) .
            w \<notin> set S] @ map (\<lambda>w. (w, Bot)) S) @ map (\<lambda>v. (v, Top)) (thd3 e))" 
          proof (unfold distinct_append, intro conjI, auto)
            show "distinct (map (\<lambda>w. (w, Top)) [x\<leftarrow>V . (\<forall>a\<in>set E. x \<notin> set (thd3 a)) \<and> x \<notin> set S])"
            proof (unfold distinct_map, intro conjI)
              show "distinct [x\<leftarrow>V . (\<forall>a\<in>set E. x \<notin> set (thd3 a)) \<and> x \<notin> set S]"
                by (auto simp add: `distinct V`)
            next
              show "inj_on (\<lambda>w. (w, Top)) (set [x\<leftarrow>V . 
                (\<forall>a\<in>set E. x \<notin> set (thd3 a)) \<and> x \<notin> set S])" 
                using inj_imp_inj_on[OF wargt[of "Top"]] by auto 
            qed
          next
            show "distinct (map (\<lambda>w. (w, Bot)) S)"
              by (unfold distinct_map, intro conjI, rule `distinct S`, 
                rule inj_imp_inj_on[OF wargt[of "Bot"]])
          next
            show "distinct (map (\<lambda>v. (v, Top)) (thd3 e))"
              by (unfold distinct_map, intro conjI, rule `distinct (thd3 e)`,
                rule inj_imp_inj_on[OF wargt[of "Top"]])
          next
            fix w
            assume "w \<in> set (thd3 e)" and "\<forall>a\<in>set E. w \<notin> set (thd3 a)" 
            with `e \<in> set E` show "False" by auto
          qed
        qed

        also have "... = listdiff ((map (\<lambda>w. (w,Top)) 
          (filter (\<lambda>w. w\<notin>set S) (initials (Graph V \<Lambda> E)))) 
          @ map (\<lambda>w. (w, Bot)) S) (map (\<lambda>v. (v, Bot)) (fst3 e)) @
          listdiff (map (\<lambda>v. (v, Top)) (thd3 e)) (map (\<lambda>v. (v, Bot)) (fst3 e))" 
          unfolding listdiff_append by auto
        also have "... = listdiff ((map (\<lambda>w. (w,Top)) 
          (filter (\<lambda>w. w\<notin>set S) (initials (Graph V \<Lambda> E)))) 
          @ map (\<lambda>w. (w, Bot)) S) (map (\<lambda>v. (v, Bot)) (fst3 e)) @
          map (\<lambda>v. (v, Top)) (thd3 e)" 
          unfolding listdiff_id[OF jxzvk] by auto
        also have "... = listdiff
          (concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else []) (initials (Graph V \<Lambda> E))) @
          map (\<lambda>w. (w, Bot)) S)
          (map (\<lambda>v. (v, Bot)) (fst3 e)) @
          map (\<lambda>v. (v, Top)) (thd3 e)"
          unfolding map_filter_is_concat_map by auto
        finally have "?rhs <~~> listdiff
          (concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else []) (initials (Graph V \<Lambda> E))) @
          map (\<lambda>w. (w, Bot)) S)
          (map (\<lambda>v. (v, Bot)) (fst3 e)) @
          map (\<lambda>v. (v, Top)) (thd3 e)" by auto
        moreover 
        have "listdiff
          (concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else []) (initials (Graph V \<Lambda> E))) @
          map (\<lambda>w. (w, Bot)) S)
          (map (\<lambda>v. (v, Bot)) (fst3 e)) @
          map (\<lambda>v. (v, Top)) (thd3 e) <~~> ?lhs"
        proof (intro perm_append2 listdiff_perm)
          have "concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else []) 
            (initials (Graph V \<Lambda> E))) @ map (\<lambda>w. (w, Bot)) S = 
            (map (\<lambda>x. (x, Top)) [x\<leftarrow>initials (Graph V \<Lambda> E) . x \<notin> set S]) 
            @ map (\<lambda>w. (w, Bot)) S" 
            unfolding map_filter_is_concat_map by auto
          moreover have "(map (\<lambda>x. (x, Top)) [x\<leftarrow>initials (Graph V \<Lambda> E) . x \<notin> set S]) 
            @ map (\<lambda>w. (w, Bot)) S <~~> \<gamma> (\<alpha> ((map (\<lambda>x. (x, Top)) [x\<leftarrow>initials (Graph V \<Lambda> E) . x \<notin> set S]) 
            @ map (\<lambda>w. (w, Bot)) S))" 
            by (rule perm_sym[OF conc_abs]) 
          moreover have "\<gamma> (\<alpha> ((map (\<lambda>x. (x, Top)) [x\<leftarrow>initials (Graph V \<Lambda> E) . x \<notin> set S]) 
            @ map (\<lambda>w. (w, Bot)) S)) = \<gamma> (\<alpha> (concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else []) 
            (initials (Graph V \<Lambda> E))) @ map (\<lambda>w. (w, Bot)) S))"
            unfolding map_filter_is_concat_map by auto
          ultimately
          show "concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else []) (initials (Graph V \<Lambda> E))) @
            map (\<lambda>w. (w, Bot))
            S <~~> \<gamma> (\<alpha> (concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else []) (initials (Graph V \<Lambda> E))) @
            map (\<lambda>w. (w, Bot)) S))" by auto
        next
          show "distinct (concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else [])
            (initials (Graph V \<Lambda> E))) @ map (\<lambda>w. (w, Bot)) S)" by (metis tklgv)
        next
          show "distinct (\<gamma> (\<alpha> (concat (map (\<lambda>w. if w \<notin> set S then [(w, Top)] else [])
            (initials (Graph V \<Lambda> E))) @ map (\<lambda>w. (w, Bot)) S)))" 
            by (metis (no_types) conc_abs listdiff_def 
              map_filter_is_concat_map maps_def perm_distinct_iff
              tklgv)
        qed
        ultimately have "?rhs <~~> ?lhs" by auto
        thus ?thesis by (rule perm_sym)
      qed

      hence jtgmn: "\<alpha> ((listdiff 
        (\<gamma> (\<alpha> ([(w,Top). w \<leftarrow> initials (Graph V \<Lambda> E), w \<notin> set S] 
        @ [(w,Bot). w \<leftarrow> S]))) [(v, Bot). v\<leftarrow>fst3 e]) 
        @ [(v, Top). v\<leftarrow>thd3 e]) 
        = \<alpha> ([(w,Top). w \<leftarrow> initials (Graph ?V' \<Lambda> ?E'), w \<notin> set ?S'] 
        @ [(w,Bot). w \<leftarrow> ?S'])" using abs_equiv by auto




      have jvlal: "?\<Pi>' \<in> rawchains2 (?S') (Graph ?V' \<Lambda> ?E')"
        unfolding rawchains2_def unfolding jtgmn
      proof (intro CollectI exI[of _ \<pi>'] conjI, simp,
          unfold lins2.simps(1), intro CollectI conjI)
        from ujyes yketi show "distinct \<pi>'" by auto
      next
        show "set \<pi>' = Inl ` (set ?V' - set ?S') \<union> Inr ` set ?E'" 
          (is "?lhs = ?rhs") 
        proof -
          have "?rhs = Inl ` (set V - set (fst3 e) 
            - (set S - set (fst3 e))) \<union> Inr ` set ?E'"
            by (metis set_listdiff)
          also have "... = Inl ` (set V - set (fst3 e) 
            - (set S - set (fst3 e))) \<union> Inr ` ((set E) - {e})"
            by (unfold set_listdiff, auto)
          also have "... = Inl ` (set V - set S) \<union> Inr ` (set E) - {Inr e}"
            using hfgey bjmwl by auto 
          also have "... = set \<pi> - {Inr e}" using aqxbk by auto
          also have "... = set (removeAll (Inr e) \<pi>)" 
            unfolding set_removeAll by auto
          also have "... = set (remove1 (Inr e) \<pi>)"
            using distinct_remove1_removeAll[OF ujyes] by auto
          also have "... = set (remove1 (Inr e) ((Inr e)#\<pi>'))" 
            using yketi hnqdb by auto
          also have "... = ?lhs" by auto
          finally show ?thesis by auto
        qed
      next
        show "\<forall>i j v e. i < length \<pi>' \<and> j < length \<pi>' \<and> \<pi>' ! i = Inl v 
          \<and> \<pi>' ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j" 
        proof (intro allI impI, (erule conjE)+)
          fix i j v e
          assume "i < length \<pi>'" and "j < length \<pi>'" 
            and "\<pi>' ! i = Inl v" and "\<pi>' ! j = Inr e"
          hence "i+1 < length \<pi>" "j+1 < length \<pi>"
            "\<pi>!(i+1) = Inl v" "\<pi>!(j+1) = Inr e" 
            using yketi by auto
          moreover
          assume "v \<in> set (fst3 e)"
          ultimately have "i+1 < j+1" using myqpt by metis          
          thus "i < j" by auto
        qed
      next
        show "\<forall>j k w e. j < length \<pi>' \<and> k < length \<pi>' \<and> \<pi>' ! j = Inr e 
          \<and> \<pi>' ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k"
        proof (intro allI impI, (erule conjE)+)
          fix j k w e
          assume "j < length \<pi>'" and "k < length \<pi>'" 
            and "\<pi>' ! j = Inr e" and "\<pi>' ! k = Inl w"
          hence "j+1 < length \<pi>" "k+1 < length \<pi>" "\<pi>!(j+1) = Inr e"
            "\<pi>!(k+1) = Inl w" 
            using yketi by auto
          moreover
          assume "w \<in> set (thd3 e)"
          ultimately have "j+1 < k+1" using zjtlg by metis          
          thus "j < k" by auto
        qed
      qed

      from `e \<in> set E` have 
        bnrxu: "distinct [e]" "set [e] \<subseteq> set E" by auto
     
      have favzl: "length ?V' + length ?E' = k + length ?S'"
        (is "?lhs = ?rhs")
      proof -
        have "?lhs = length V - length (fst3 e) + length E 
          - length [e]" 
          using length_listdiff[OF `distinct V` bjcek rodmt]
          using length_listdiff[OF `distinct E` bnrxu] 
          by (metis add_diff_assoc2 bnrxu(2) distinct_singleton 
            list_subseteq nat_add_commute)
        also have "... = length V - length (fst3 e) + length E - 1" 
          by auto
        also have "... = k + length S - length (fst3 e)" 
          using Suc.prems(5) and list_subseteq[OF bjcek rodmt] by arith
        also have "... = k + length (listdiff S (fst3 e))" 
          using length_listdiff[OF `distinct S` bjcek bjmwl] 
          by (metis bjcek bjmwl diff_add_assoc list_subseteq)
        finally show "?lhs = ?rhs" by auto
      qed
      have cwzgj: "terminals (Graph V \<Lambda> E) 
        = terminals (Graph ?V' \<Lambda> ?E')"
      proof (unfold terminals.simps, auto)
        let ?lhs = "[v\<leftarrow>V . \<forall>a\<in>set E. v \<notin> set (fst3 a)]"
        let ?rhs = "[v\<leftarrow>listdiff V (fst3 e) . \<forall>f\<in>set (listdiff E [e]).
          v \<notin> set (fst3 f)]"
        have "?rhs = [v\<leftarrow>[v\<leftarrow>V . v \<notin> set (fst3 e)] . 
          \<forall>f\<in>set [f\<leftarrow>E . f \<notin> set [e]]. v \<notin> set (fst3 f)]" 
          unfolding listdiff_def by auto
        also have "... = [x\<leftarrow>V . x \<notin> set (fst3 e) \<and> 
          (\<forall>f\<in>set [f\<leftarrow>E . f \<notin> set [e]]. x \<notin> set (fst3 f))]" 
          unfolding filter_filter by auto
        also have "... = [x\<leftarrow>V . x \<notin> set (fst3 e) \<and> 
          (\<forall>f. f \<in> set [f\<leftarrow>E . f\<noteq>e] \<longrightarrow> x \<notin> set (fst3 f))]"
          by auto
        also have "... = [x\<leftarrow>V . x \<notin> set (fst3 e) \<and> 
          (\<forall>f. f \<in> set E \<and> f\<noteq>e \<longrightarrow> x \<notin> set (fst3 f))]"
          by auto
        also have "... = [x\<leftarrow>V . x \<notin> set (fst3 e) \<and> 
          (\<forall>f. f \<in> set E \<longrightarrow> f\<noteq>e \<longrightarrow> x \<notin> set (fst3 f))]"
          unfolding imp_conjL by auto
        also have "... = [x\<leftarrow>V . x \<notin> set (fst3 e) \<and> 
          (\<forall>f \<in> set E. f\<noteq>e \<longrightarrow> x \<notin> set (fst3 f))]"
          by metis
        also have "... = ?lhs"
        proof (intro filter_cong, simp)
          fix x
          assume "x \<in> set V"
          show "(x \<notin> set (fst3 e) \<and> 
            (\<forall>f\<in>set E. f \<noteq> e \<longrightarrow> x \<notin> set (fst3 f))) 
            = (\<forall>f\<in>set E. x \<notin> set (fst3 f))"
            using all_but_one[OF `e \<in> set E`, 
              of "\<lambda>e. x \<notin> set (fst3 e)"] by auto
        qed
        finally show "?lhs = ?rhs" by auto
      qed

      from Suc.hyps[OF cuztr fthcv shifk jvlal favzl] have
        mapkz: "wf_rawchain ?\<Pi>'" and 
        "\<gamma> (post ?\<Pi>') <~~> [(v,Bot). v \<leftarrow> terminals (Graph ?V' \<Lambda> ?E')]" 
        by auto
      from this(2) and cwzgj have 
        uzlwq: "\<gamma> (post ?\<Pi>') 
        <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]"
        by auto
 
      have ppefa: "?\<sigma> <~~> [(v, Bot). v\<leftarrow>fst3 e] @ ?\<sigma>'"
        apply (intro diff_then_append, rule tklgv)
        defer
        apply (unfold distinct_map, intro conjI bjcek)
        apply (metis (no_types) Pair_eq inj_on_def)
      proof (intro subsetI, auto)
        fix v
        assume "v \<in> set (fst3 e)"
        hence "v \<in> set S" by (metis bjmwl subsetD)
        moreover assume "(v, Bot) \<notin> (\<lambda>v. (v, Bot)) ` set S"
        ultimately show "False" by (metis imageI) 
      qed 

      from tklgv have zuuso: "distinct (\<gamma> (\<alpha> ?\<sigma>))" 
        by (metis (no_types) conc_abs perm_distinct_iff)
      have vpcvj: "pre ?\<Pi>' = \<alpha> ((listdiff (\<gamma> (\<alpha> ?\<sigma>)) 
        [(v,Bot). v\<leftarrow>fst3 e]) @ [(v,Top). v\<leftarrow>thd3 e])" 
        using pre_mk by auto
      
      have ejtrd: "\<And>X Y. \<lbrakk> distinct X ; X <~~> Y \<rbrakk> \<Longrightarrow> distinct Y" 
        using perm_distinct_iff by auto

      have "listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Bot). v \<leftarrow> fst3 e] 
        <~~> listdiff ?\<sigma> [(v,Bot). v \<leftarrow> fst3 e]" 
        apply (intro listdiff_perm conc_abs, rule ejtrd)
        prefer 2
        apply (rule perm_sym[OF conc_abs])
        apply (metis tklgv)+
        done
      
      hence "listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Bot). v \<leftarrow> fst3 e] 
        @ [(v,Top). v \<leftarrow> thd3 e] <~~> ?\<sigma>' @ [(v,Top). v \<leftarrow> thd3 e]"
        by auto
      from abs_equiv[OF this] have 
        "\<alpha> (listdiff (\<gamma> (\<alpha> ?\<sigma>)) [(v,Bot). v \<leftarrow> fst3 e] 
        @ [(v,Top). v \<leftarrow> thd3 e]) = \<alpha> (?\<sigma>' @ [(v,Top). v \<leftarrow> thd3 e])"
        by auto
      with vpcvj have "pre ?\<Pi>' = \<alpha> (?\<sigma>' @ [(v,Top). v \<leftarrow> thd3 e])" 
        by auto
      hence "\<gamma> (pre ?\<Pi>') <~~> ?\<sigma>' @ [(v,Top). v \<leftarrow> thd3 e]" 
        using conc_abs by auto
      moreover have "?\<sigma>' @ [(v,Top). v \<leftarrow> thd3 e] 
        <~~> [(v,Top). v \<leftarrow> thd3 e] @ ?\<sigma>'" 
        by (metis perm_append_swap)
      ultimately have otqat: "\<gamma> (pre ?\<Pi>') <~~>  
        [(v,Top). v \<leftarrow> thd3 e] @ ?\<sigma>'" 
        by (rule perm.trans)
      
      from wf_rawchain_ccons_inr[OF ppefa otqat mapkz] lmkbq
      have "wf_rawchain \<Pi>" by auto 
      moreover
      from lmkbq have "post \<Pi> = post ?\<Pi>'" by auto
      with uzlwq have 
        "\<gamma> (post \<Pi>) <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]" 
        by auto
      ultimately show ?thesis by auto
    qed
  qed
qed


corollary wf_chains:  
  fixes V \<Lambda> E \<Pi>
  assumes "wf_dia (Graph V \<Lambda> E)"
  assumes "\<Pi> \<in> rawchains (Graph V \<Lambda> E)"
  shows "wf_rawchain \<Pi> 
  \<and> \<gamma> (post \<Pi>) <~~> [(v,Bot). v \<leftarrow> terminals (Graph V \<Lambda> E)]"
proof (intro wf_chains2) 
  show "distinct []" by auto
next
  show "set [] \<subseteq> set (initials (Graph V \<Lambda> E))" by auto
next
  show "wf_dia (Graph V \<Lambda> E)" using assms(1) by auto
next
  show "\<Pi> \<in> rawchains2 [] (Graph V \<Lambda> E)" 
    using assms(2) and rawchains_is_rawchains2_with_empty_S by auto
next
  show "length V + length E = length V + length E + length []" by auto
qed

lemma nth_suc:   
  fixes X i
  shows "Suc i < length X \<Longrightarrow> X ! Suc i = tl X ! i"
  by (induct X, auto)

lemma pre_chainmap:
  fixes f g \<Pi>
  shows "pre (chainmap f g \<Pi>) = f (pre \<Pi>)"
  by (induct \<Pi>, auto)

lemma post_chainmap:
  fixes f g \<Pi>
  shows "post (chainmap f g \<Pi>) = f (post \<Pi>)"
  by (induct \<Pi>, auto)

lemma ass_fold_hcomp:
  fixes Ps
  shows "ass (foldl (op \<otimes>) Emp_int Ps) = foldl (op \<ast>) Emp (map ass Ps)"
proof -
  have "\<And>Q. ass (foldl (op \<otimes>) Q Ps) = foldl (op \<ast>) (ass Q) (map ass Ps)"
  proof (induct Ps)
    case Nil
    show ?case by auto
  next
    case (Cons P Ps)
    hence "\<And>Q. ass (foldl op \<otimes> Q Ps) 
      = foldl op \<ast> (ass Q) (map ass Ps)" by auto
    let ?lhs = "ass (foldl op \<otimes> Q (P # Ps))"
    let ?rhs = "foldl op \<ast> (ass Q) (map ass (P # Ps))"
    have "?lhs = ass (foldl op \<otimes> (Q \<otimes> P) Ps)" by auto
    also have "... = foldl op \<ast> (ass (Q \<otimes> P)) (map ass Ps)"
      using Cons.hyps by auto
    also have "... = foldl op \<ast> (ass Q \<ast> ass P) (map ass Ps)" 
      by auto
    also have "... = foldl op \<ast> (ass Q) ((ass P) # (map ass Ps))" 
      by auto
    also have "... = ?rhs" by auto
    finally show ?case by auto
  qed
  thus ?thesis by auto
qed

lemma ass_perm: 
  fixes ps Qs
  assumes "ps <~~> qs"
  shows "foldl (op \<ast>) Emp ps = foldl (op \<ast>) Emp qs" 
using assms
proof (induct rule:perm.induct)
  case swap
  thus ?case by (metis emp_star foldl_Cons star_comm)
next
  case Cons
  thus ?case by (metis (no_types) foldl_Cons 
    foldl_fun_comm star_assoc star_comm)
qed (auto)

lemma ass_foldl_foldr:
  fixes Ps
  shows "ass (foldl (op \<otimes>) Emp_int Ps) 
  = ass (foldr (op \<otimes>) Ps Emp_int)"
proof -
  have "\<And>Q R. ass (R \<otimes> (foldr (op \<otimes>) Ps Q)) 
  = ass ((foldl (op \<otimes>) R Ps) \<otimes> Q)"
  proof (induct Ps) 
    case Nil thus ?case by auto
  next
    case (Cons P Ps) thus ?case 
      by (metis equiv_int_sound foldl_Cons foldr.simps(2) hcomp_assoc)
  qed
  from this[of Emp_int Emp_int] show ?thesis 
    using emp_star star_emp by auto
qed

lemma ass_perm_int:
  fixes Ps Qs
  assumes "Ps <~~> Qs"
  shows "ass (foldr (op \<otimes>) Ps Emp_int) 
  = ass (foldr (op \<otimes>) Qs Emp_int)"
  by (metis ass_fold_hcomp ass_foldl_foldr ass_perm assms map_perm)

lemma nthtriple_chainmap: 
  fixes f g \<Pi>
  shows "\<And>i. i < chainlen \<Pi> \<Longrightarrow> nthtriple (chainmap f g \<Pi>) i = 
  (\<lambda>(\<sigma>1,x,\<sigma>2). (f \<sigma>1, g x, f \<sigma>2)) (nthtriple \<Pi> i)"
proof (induct \<Pi>)
  case (cNil P)
  thus ?case by auto
next
  case (cCons P c \<Pi>)
  thus ?case by (induct i, auto simp add: pre_chainmap)
qed


lemma seq_fold: 
  fixes cs
  shows "\<And>\<Pi>. \<lbrakk> length cs = chainlen \<Pi> ; 
  \<forall>i < chainlen \<Pi>. prov_triple 
  (ass (fst3 (nthtriple \<Pi> i)), cs ! i, ass (thd3 (nthtriple \<Pi> i))) \<rbrakk>
  \<Longrightarrow> prov_triple (ass (pre \<Pi>), foldr (op ;;) cs Skip, ass (post \<Pi>))"
proof (induct cs)
  case Nil
  hence "chainlen \<Pi> = 0" by auto
  then obtain p where "\<Pi> = cNil p" by (cases \<Pi>, auto)
  show ?case unfolding `\<Pi> = cNil p` by (auto simp add: prov_triple.skip)
next
  case (Cons c cs)
  from Cons.prems(1) have "length (c # cs) = chainlen \<Pi>" by assumption
  from Cons.prems(2) have ozniy: "\<And>i. i<chainlen \<Pi> \<Longrightarrow> prov_triple (ass (fst3 (nthtriple \<Pi> i)), (c # cs) ! i, ass (thd3 (nthtriple \<Pi> i)))" by auto

  from Cons.prems(1) obtain p x \<Pi>' where hnsvs: "\<Pi> = cCons p x \<Pi>'" 
    by (metis chain.exhaust chainlen.simps(1) impossible_Cons le0)

  with Cons.prems(1) have "length cs = chainlen \<Pi>'" by auto
  from Cons.hyps[OF this] have 
    tnlzn: "\<forall>i<chainlen \<Pi>'. 
    prov_triple (ass (fst3 (nthtriple \<Pi>' i)), cs ! i, ass (thd3 (nthtriple \<Pi>' i))) 
    \<Longrightarrow> prov_triple (ass (pre \<Pi>'), foldr op ;; cs Skip, ass (post \<Pi>'))" by auto

  from Cons.prems(1) have "0 < chainlen \<Pi>" by auto
  from ozniy[OF this] have zyaiu: "prov_triple (ass p, c, ass (pre \<Pi>'))"
    unfolding hnsvs by (auto, unfold fst3_simp thd3_simp)
  
  from hnsvs have uqmba: "post \<Pi>' = post \<Pi>" by auto

  have lkgap: "prov_triple (ass (pre \<Pi>), c, ass (pre \<Pi>'))" using zyaiu hnsvs by auto
  have pehot: "prov_triple (ass (pre \<Pi>'), foldr op ;; cs Skip, ass (post \<Pi>))" 
  proof (fold uqmba, intro tnlzn, intro allI impI)
    fix i
    assume "i < chainlen \<Pi>'"
    hence "i+1 < chainlen \<Pi>" using hnsvs by auto
    from ozniy[OF this] show "prov_triple (ass (fst3 (nthtriple \<Pi>' i)),
      cs ! i, ass (thd3 (nthtriple \<Pi>' i)))" by (unfold hnsvs, auto)
  qed
  from prov_triple.seq[OF lkgap pehot] show ?case by auto
qed
  
lemma foldr_hcomp:
  fixes Ps Q
  shows "ass (foldr op \<otimes> Ps Q) = ass ((foldr op \<otimes> Ps Emp_int) \<otimes> Q)"
proof (induct Ps)
  case Nil
  show ?case by (auto simp add: emp_star)
next
  case (Cons P Ps)
  hence "ass (foldr op \<otimes> Ps Q) = ass (foldr op \<otimes> Ps Emp_int \<otimes> Q)"
    by metis
  show "ass (foldr op \<otimes> (P # Ps) Q) =
    ass (foldr op \<otimes> (P # Ps) Emp_int \<otimes> Q)"
    apply auto 
    apply (unfold Cons.hyps)  
    apply (auto simp add: star_assoc) 
    done
qed
 

lemma var_soundness_helper:
  assumes no_var_interference: "\<And>c. wr_com c = {}"
  shows "(prov_dia G P Q \<longrightarrow> (P = top_dia G \<and> Q = bot_dia G \<and> 
  (\<forall>c \<in> coms_dia G. prov_triple (ass P, c, ass Q)))) 
  \<and> (prov_com C P Q \<longrightarrow> (\<forall>c \<in> coms_com C. prov_triple (ass P, c, ass Q)))
  \<and> (prov_ass A \<longrightarrow> (\<forall>c \<in> coms_ass A. prov_triple (ass (top_ass A), c, ass (bot_ass A))))"
proof (induct rule: prov_dia_prov_com_prov_ass.induct)
  case (Skip p)
  thus ?case 
  proof (intro ballI)
    fix c 
    assume "c \<in> coms_ass (Rib p)"
    hence "coms_ass (Rib p) c" by (metis mem_def)
    from coms_skip_inv[OF this] have "c = Skip" by auto
    moreover have "ass (top_ass (Rib p)) = p" by auto
    moreover have "ass (bot_ass (Rib p)) = p" by auto
    ultimately show "prov_triple (ass (top_ass (Rib p)), c, ass (bot_ass (Rib p)))" 
      using prov_triple.skip by auto
  qed
next
  case (Exists G P Q x)
  thus ?case
  proof (intro ballI)
    fix c
    assume "c \<in> coms_ass (Exists_dia x G)"
    hence ldqxz: "coms_ass (Exists_dia x G) c" by (metis mem_def)
    assume wflao: "P = top_dia G \<and> Q = bot_dia G \<and> (\<forall>c\<in>coms_dia G. prov_triple (ass P, c, ass Q))" 
    have "c \<in> coms_dia G" using coms_exists_inv[OF ldqxz] by (metis mem_def)
    with wflao have fsree: "prov_triple (ass P, c, ass Q)" by auto
    have "ass (top_ass (Exists_dia x G)) = Exists x (ass P)" using wflao by auto
    moreover
    have "ass (bot_ass (Exists_dia x G)) = Exists x (ass Q)" using wflao by auto
    moreover
    have "prov_triple (Exists x (ass P), c, Exists x (ass Q))" 
      by (rule prov_triple.exists, rule fsree)
    ultimately
    show "prov_triple (ass (top_ass (Exists_dia x G)), c, ass (bot_ass (Exists_dia x G)))"
      by auto
  qed
next
  case (Basic P c Q)
  thus ?case
  proof (intro ballI)
    fix ca
    assume lxkin: "prov_triple (ass P, c, ass Q)"
    assume "ca \<in> coms_com (Com c)"
    hence "coms_com (Com c) ca" by (metis mem_def)
    from coms_basic_inv [OF this] have "ca = c" by auto
    with lxkin show "prov_triple (ass P, ca, ass Q)" by auto
  qed
next
  case (Choice G P Q H)
  thus ?case
    apply (intro ballI) 
    apply (elim conjE)
  proof -
    fix c
    assume ydhfk: "\<forall>c\<in>coms_dia G. prov_triple (ass P, c, ass Q)"
    assume bbzsd: "\<forall>c\<in>coms_dia H. prov_triple (ass P, c, ass Q)"
    assume "c \<in> coms_com (Choose_dia G H)"
    hence "coms_com (Choose_dia G H) c" by (metis mem_def)
    from coms_choice_inv[OF this] obtain c1 c2 where 
      pehfc: "c = Choose c1 c2" and
      "coms_dia G c1" and "coms_dia H c2" by auto
    hence "c1 \<in> coms_dia G" and "c2 \<in> coms_dia H" 
      by (metis mem_def)+
    with ydhfk bbzsd have 
      "prov_triple (ass P, c1, ass Q)" 
      "prov_triple (ass P, c2, ass Q)" by auto
    from prov_triple.choose[OF this] and pehfc show
      "prov_triple (ass P, c, ass Q)"
      by auto
  qed
next
  case (Loop G P)
  thus ?case
    apply (intro ballI) 
    apply (elim conjE) 
  proof -
    fix c
    assume gchsd: "\<forall>c\<in>coms_dia G. prov_triple (ass P, c, ass P)"
    assume "c \<in> coms_com (Loop_dia G)"
    hence "coms_com (Loop_dia G) c" by (metis mem_def)
    from coms_loop_inv[OF this] obtain c1 where
      vxvnb: "c = Loop c1" and "coms_dia G c1" by auto
    hence "c1 \<in> coms_dia G" by (metis mem_def)
    with gchsd have "prov_triple (ass P, c1, ass P)" by auto
    from prov_triple.loop[OF this] and vxvnb show
      "prov_triple (ass P, c, ass P)"
      by auto
  qed
next
  case (Main V \<Lambda> E)
  thus ?case
    apply (intro conjI, simp, simp) 
    apply (intro ballI) 
  proof -
    let ?G = "Graph V \<Lambda> E"
    fix c
    assume sexqd: "\<And>v. v \<in> set V \<Longrightarrow> \<forall>c\<in>coms_ass (\<Lambda> v). 
      prov_triple (ass (top_ass (\<Lambda> v)), c, ass (bot_ass (\<Lambda> v)))"
    assume aprie: "\<And>e. e \<in> set E \<Longrightarrow> \<forall>c\<in>coms_com (snd3 e). prov_triple 
      (ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))), c,
      ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))))"
    assume quitc: "wf_dia ?G"
    assume "c \<in> coms_dia (Graph V \<Lambda> E)"
    hence "coms_dia (Graph V \<Lambda> E) c" by (metis mem_def)
    from coms_main_inv[OF this] 
     obtain \<pi> cs where "\<pi> \<in> lins (Graph V \<Lambda> E) 
       \<and> length cs = length \<pi> 
       \<and> (\<forall>i<length \<pi>. (\<exists>v. \<pi> ! i = Inl v) 
       \<longrightarrow> coms_ass (\<Lambda> (Sum_Type.Projl (\<pi> ! i))) (cs ! i)) 
       \<and> (\<forall>i<length \<pi>. (\<exists>e. \<pi> ! i = Inr e) 
       \<longrightarrow> coms_com (snd3 (Sum_Type.Projr (\<pi> ! i))) (cs ! i)) \<and>
       c = foldr op ;; cs Skip" by auto
     hence 
       ovuqv: "\<pi> \<in> lins (Graph V \<Lambda> E)" and 
       ipvoy: "length cs = length \<pi>" and 
       "\<forall>i<length \<pi>. (\<exists>v. \<pi> ! i = Inl v) 
       \<longrightarrow> coms_ass (\<Lambda> (Sum_Type.Projl (\<pi> ! i))) (cs ! i)" and 
       "\<forall>i<length \<pi>. (\<exists>e. \<pi> ! i = Inr e) 
       \<longrightarrow> coms_com (snd3 (Sum_Type.Projr (\<pi> ! i))) (cs ! i)" and 
       zkhmj: "c = foldr op ;; cs Skip" 
       by (metis)+
     from this(3) this(4) have 
       yqvfp: "\<And>i v. \<lbrakk> i < length \<pi> ; \<pi>!i = Inl v \<rbrakk> \<Longrightarrow>
       coms_ass (\<Lambda> (Sum_Type.Projl (\<pi> ! i))) (cs ! i)" and 
       dnhoi: "\<And>i e. \<lbrakk> i < length \<pi> ; \<pi>!i = Inr e \<rbrakk> \<Longrightarrow>
       coms_com (snd3 (Sum_Type.Projr (\<pi> ! i))) (cs ! i)" by auto
     
     from ovuqv have 
       pwlee: "distinct \<pi>" and 
       eagbg: "set \<pi> = Inl ` set V \<union> Inr ` set E" and
       "\<forall>i j v e. i < length \<pi> \<and> j < length \<pi> \<and> \<pi> ! i = Inl v 
       \<and> \<pi> ! j = Inr e \<and> v \<in> set (fst3 e) \<longrightarrow> i < j" and
       "\<forall>j k w e. j < length \<pi> \<and> k < length \<pi> \<and> \<pi> ! j = Inr e 
       \<and> \<pi> ! k = Inl w \<and> w \<in> set (thd3 e) \<longrightarrow> j < k" 
       apply (unfold lins.simps) 
       apply (elim CollectE conjE, assumption)+
       done
     
     from this(3) this(4) have 
       qfgbz: "\<And>i j v e. \<lbrakk> i < length \<pi> ; j < length \<pi> ; \<pi> ! i = Inl v 
       ; \<pi> ! j = Inr e ; v \<in> set (fst3 e) \<rbrakk> \<Longrightarrow> i < j" and
       zyzev: "\<And>j k w e. \<lbrakk> j < length \<pi> ; k < length \<pi> ; \<pi> ! j = Inr e 
       ; \<pi> ! k = Inl w ; w \<in> set (thd3 e) \<rbrakk> \<Longrightarrow> j < k" 
       by metis+     
     let ?\<Pi> = "mk (cNil (\<alpha> [(v, Top) . v \<leftarrow> initials ?G])) \<pi>"
     
     have nuksb: "?\<Pi> \<in> rawchains ?G" by (unfold rawchains_def, intro CollectI, metis ovuqv)
     have distinct_perm: "\<And>X Y. \<lbrakk> distinct X ; X <~~> Y \<rbrakk> \<Longrightarrow> distinct Y" 
       by (metis perm_distinct_iff)

     from pre_mk have 
       "pre ?\<Pi> = \<alpha> [(v, Top) . v \<leftarrow> initials ?G]" by auto
     hence "map fst (\<gamma> (pre ?\<Pi>)) 
       = map fst (\<gamma> (\<alpha> [(v, Top) . v \<leftarrow> initials ?G]))" by auto
     also have "... <~~> map fst [(v, Top) . v \<leftarrow> initials ?G]" 
       by (intro map_perm, rule conc_abs)
     also have "... = initials ?G" by (metis map_fst_pair)
     finally have "map fst (\<gamma> (pre ?\<Pi>)) <~~> initials ?G" by auto
     
     from wf_chains [OF quitc nuksb] have 
       mdajx: "wf_rawchain ?\<Pi>" and 
       lisdi: "\<gamma> (post ?\<Pi>) <~~> [(v,Bot). v \<leftarrow> terminals ?G]" by auto

     have rxqbt: "\<lbrakk> \<And>i. i < chainlen ?\<Pi>
       \<Longrightarrow> prov_triple ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
       (nthtriple (cook ?G ?\<Pi>) i)) \<rbrakk> 
       \<Longrightarrow> prov_triple (ass (pre (cook ?G ?\<Pi>)), c, 
       ass (post (cook ?G ?\<Pi>)))"
     proof -
       assume mboea: "\<And>i. i < chainlen ?\<Pi>
         \<Longrightarrow> prov_triple ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
         (nthtriple (cook ?G ?\<Pi>) i))"
       from ipvoy have "length cs = length \<pi>" by auto
       moreover
       from mk_preserves_length have 
         "length \<pi> = chainlen ?\<Pi>" by auto
       moreover
       from chainmap_preserves_length have 
         ywrwb: "chainlen (cook ?G ?\<Pi>) = chainlen ?\<Pi>" unfolding cook.simps by auto
       ultimately have zoejd: "length cs = chainlen (cook ?G ?\<Pi>)" by auto
       have vuzmq: "\<forall>i < chainlen (cook ?G ?\<Pi>). 
         prov_triple (ass (fst3 (nthtriple (cook ?G ?\<Pi>) i)), 
         cs ! i, ass (thd3 (nthtriple (cook ?G ?\<Pi>) i)))"
       proof(intro allI impI)
         fix i
         assume "i < chainlen (cook ?G ?\<Pi>)"
         hence "i < chainlen ?\<Pi>" using ywrwb by auto
         hence "prov_triple ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
       (nthtriple (cook ?G ?\<Pi>) i))" using mboea by auto
         moreover
         have "prov_triple ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
       (nthtriple (cook ?G ?\<Pi>) i)) = prov_triple (ass (fst3 (nthtriple (cook ?G ?\<Pi>) i)), 
         cs ! i, ass (thd3 (nthtriple (cook ?G ?\<Pi>) i)))" 
           apply (intro arg_cong[of _ _ "prov_triple"], intro tripleI)
           apply (unfold fst3_comp fst3_simp, simp)
           apply (unfold snd3_comp snd3_simp, simp)
           apply (unfold thd3_comp thd3_simp, simp)
           done
         ultimately show "prov_triple (ass (fst3 (nthtriple (cook ?G ?\<Pi>) i)), 
         cs ! i, ass (thd3 (nthtriple (cook ?G ?\<Pi>) i)))" by auto
       qed
       from seq_fold[OF zoejd vuzmq] and zkhmj
       show "prov_triple (ass (pre (cook ?G ?\<Pi>)), c, 
         ass (post (cook ?G ?\<Pi>)))" by auto
     qed

     have "prov_triple (ass (pre (cook ?G ?\<Pi>)), c,
       ass (post (cook ?G ?\<Pi>)))" 
     proof (intro rxqbt)
       fix i
       assume iyuyo: "i < chainlen ?\<Pi>"
       also have "... = length \<pi>" 
         unfolding mk_preserves_length by auto
       finally have aktjb: "i < length \<pi>" by auto
       show "prov_triple ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) (nthtriple (cook ?G ?\<Pi>) i))" 
       proof (cases "\<pi>!i")
         case (Inl v)
         from wf_rawchain_def mdajx iyuyo obtain \<sigma>' where
           mzkbx: "(\<exists>v. nthtriple ?\<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))) \<or>
           (\<exists>e. nthtriple ?\<Pi> i =
           (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>')))"
           by metis
         have zyxtr: "snd3 (nthtriple ?\<Pi> i) = Inl v"
         proof -
           from snds_of_triples_form_comlist[OF iyuyo]
           have "snd3 (nthtriple ?\<Pi> i) = \<pi>!i" 
             unfolding mk_comlist by auto
           thus ?thesis using Inl by auto
         qed
         have "\<not> (\<exists>e. nthtriple ?\<Pi> i =
           (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>')))"
         proof (intro notI)
           assume "\<exists>e. nthtriple ?\<Pi> i = (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e,
             \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>'))"
           then obtain e where "nthtriple ?\<Pi> i = (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, 
             \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>'))" by auto
           hence "snd3 (nthtriple ?\<Pi> i) = snd3 (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, 
             \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>'))" by auto
           hence "Inl v = Inr e" using zyxtr unfolding snd3_def by auto
           thus False by auto
         qed
         with mzkbx have "\<exists>v. nthtriple ?\<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))" by auto
         then obtain v' where 
           wvjxe: "nthtriple ?\<Pi> i = (\<alpha> ([(v', Top)] @ \<sigma>'), Inl v', \<alpha> ([(v', Bot)] @ \<sigma>'))" 
           by auto
         hence "snd3 (nthtriple ?\<Pi> i) = Inl v'" unfolding snd3_def by auto
         with zyxtr have "v = v'" by auto
         with wvjxe have rraei: "nthtriple ?\<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))" by auto
         
         let ?f = "ass ((foldl op \<otimes> Emp_int \<circ> map 
           (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) \<circ> \<gamma>) (\<alpha> \<sigma>'))"
         
         from Inl and yqvfp[OF aktjb Inl] have
           "coms_ass (\<Lambda> v) (cs ! i)" by auto
         hence 
           nrmyv: "(cs ! i) \<in> coms_ass (\<Lambda> v)" by (metis mem_def)
         from Inl aktjb have "Inl v \<in> set \<pi>" by (metis nth_mem)
         with eagbg have "v \<in> set V" by auto
         from sexqd[OF this] nrmyv have
           "prov_triple (ass (top_ass (\<Lambda> v)), cs!i, 
           ass (bot_ass (\<Lambda> v)))" by auto
         hence
           "prov_triple (ass (top_ass (\<Lambda> v)) \<ast> ?f, cs!i, 
           ass (bot_ass (\<Lambda> v)) \<ast> ?f)" 
           using prov_triple.frame and no_var_interference 
           by auto
         moreover
         have "((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
           (nthtriple (cook ?G ?\<Pi>) i)) = 
           (ass (top_ass (\<Lambda> v)) \<ast> ?f, cs!i, 
           ass (bot_ass (\<Lambda> v)) \<ast> ?f)" 
         proof (intro tripleI)
           have "fst3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i))
             = ass (fst3 (nthtriple (cook ?G ?\<Pi>) i))"
             unfolding split_def fst3_def by auto
           also have "... = ass (foldl op \<otimes> Emp_int 
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) 
             (\<gamma> (fst3 (nthtriple ?\<Pi> i)))))"
              unfolding cook.simps nthtriple_chainmap[OF iyuyo]
                fst3_comp by auto
           also have "... = ass (foldl op \<otimes> Emp_int
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> ((v, Top) # \<sigma>')))))" 
             unfolding rraei fst3_def by auto
           also have "... = ass (foldr op \<otimes> 
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> ((v, Top) # \<sigma>')))) Emp_int)"
             using ass_foldl_foldr by auto
           also have "... = ass (((foldr (op \<otimes>) (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) 
             ((v,Top) # \<gamma> (\<alpha> \<sigma>'))) Emp_int)))" 
             apply (intro ass_perm_int map_perm)
             apply (metis Quotient_proofstate perm.Cons perm_refl
               rep_abs_rsp rep_abs_rsp_left)
             done
           also have "... = ass (((foldr (op \<otimes>) (top_ass (\<Lambda> v) # map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))) Emp_int)))" by auto
           also have "... = ass (top_ass (\<Lambda> v) \<otimes> 
             ((foldr (op \<otimes>) (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))) Emp_int)))" by auto
           also have "... = ass (top_ass (\<Lambda> v) \<otimes> 
             ((foldl (op \<otimes>) Emp_int (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))))))" 
             using ass_foldl_foldr by auto
           also have "... = ass (top_ass (\<Lambda> v)) \<ast> ?f" by auto
           finally have "fst3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i)) 
             = ass (top_ass (\<Lambda> v)) \<ast> ?f" by auto
           thus "fst3 ((\<lambda>(P, _, Q). (ass P, cs ! i, ass Q))
             (nthtriple (cook ?G ?\<Pi>) i)) =
             fst3 (ass (top_ass (\<Lambda> v)) \<ast> ?f, cs ! i, 
             ass (bot_ass (\<Lambda> v)) \<ast> ?f)" unfolding fst3_def by auto
         next
           have cojiq: "\<And>X Y. snd3 ((\<lambda>(P,_,Q). (ass P, Y, ass Q)) X) 
             = Y" unfolding snd3_def by auto
           have "snd3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i)) 
             = cs!i" unfolding cojiq by auto
           thus "snd3 ((\<lambda>(P, _, Q). (ass P, cs ! i, ass Q))
             (nthtriple (cook ?G ?\<Pi>) i)) =
             snd3 (ass (top_ass (\<Lambda> v)) \<ast> ?f, cs ! i, 
             ass (bot_ass (\<Lambda> v)) \<ast> ?f)" unfolding snd3_def by auto
         next
           have "thd3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i))
             = ass (thd3 (nthtriple (cook ?G ?\<Pi>) i))"
             unfolding split_def thd3_def by auto
           also have "... = ass (foldl op \<otimes> Emp_int 
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) 
             (\<gamma> (thd3 (nthtriple ?\<Pi> i)))))"
              unfolding cook.simps nthtriple_chainmap[OF iyuyo]
                thd3_comp by auto
           also have "... = ass (foldl op \<otimes> Emp_int
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> ((v, Bot) # \<sigma>')))))" 
             unfolding rraei thd3_def by auto
           also have "... = ass (foldr op \<otimes> 
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> ((v, Bot) # \<sigma>')))) Emp_int)"
             using ass_foldl_foldr by auto
           also have "... = ass (((foldr (op \<otimes>) (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) 
             ((v,Bot) # \<gamma> (\<alpha> \<sigma>'))) Emp_int)))" 
             apply (intro ass_perm_int map_perm)
             apply (metis Quotient_proofstate perm.Cons perm_refl
               rep_abs_rsp rep_abs_rsp_left)
             done
           also have "... = ass (((foldr (op \<otimes>) (bot_ass (\<Lambda> v) # map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))) Emp_int)))" by auto
           also have "... = ass (bot_ass (\<Lambda> v) \<otimes> 
             ((foldr (op \<otimes>) (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))) Emp_int)))" by auto
           also have "... = ass (bot_ass (\<Lambda> v) \<otimes> 
             ((foldl (op \<otimes>) Emp_int (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))))))" 
             using ass_foldl_foldr by auto
           also have "... = ass (bot_ass (\<Lambda> v)) \<ast> ?f" by auto
           finally have "thd3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i)) 
             = ass (bot_ass (\<Lambda> v)) \<ast> ?f" by auto
           thus "thd3 ((\<lambda>(P, _, Q). (ass P, cs ! i, ass Q))
             (nthtriple (cook ?G ?\<Pi>) i)) =
             thd3 (ass (top_ass (\<Lambda> v)) \<ast> ?f, cs ! i, 
             ass (bot_ass (\<Lambda> v)) \<ast> ?f)" unfolding thd3_def by auto
         qed
         ultimately  
         show ?thesis by auto
       next
         case (Inr e)
         from wf_rawchain_def mdajx iyuyo obtain \<sigma>' where
           mzkbx: "(\<exists>v. nthtriple ?\<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))) \<or>
           (\<exists>e. nthtriple ?\<Pi> i =
           (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>')))"
           by metis
         have zyxtr: "snd3 (nthtriple ?\<Pi> i) = Inr e"
         proof -
           from snds_of_triples_form_comlist[OF iyuyo]
           have "snd3 (nthtriple ?\<Pi> i) = \<pi>!i" 
             unfolding mk_comlist by auto
           thus ?thesis using Inr by auto
         qed
         have "\<not> (\<exists>v. nthtriple ?\<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>')))"
         proof (intro notI)
           assume "\<exists>v. nthtriple ?\<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))"
           then obtain v where "nthtriple ?\<Pi> i = (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))" by auto
           hence "snd3 (nthtriple ?\<Pi> i) = snd3 (\<alpha> ([(v, Top)] @ \<sigma>'), Inl v, \<alpha> ([(v, Bot)] @ \<sigma>'))" by auto
           hence "Inl e = Inr v" using zyxtr unfolding snd3_def by auto
           thus False by auto
         qed
         with mzkbx have "\<exists>e. nthtriple ?\<Pi> i =
           (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>'))" by auto
         then obtain e' where 
           wvjxe: "nthtriple ?\<Pi> i =
           (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e') @ \<sigma>'), Inr e', \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e') @ \<sigma>'))" 
           by auto
         hence "snd3 (nthtriple ?\<Pi> i) = Inr e'" unfolding snd3_def by auto
         with zyxtr have "e = e'" by auto
         with wvjxe have rraei: "nthtriple ?\<Pi> i = (\<alpha> (map (\<lambda>v. (v, Bot)) (fst3 e) @ \<sigma>'), Inr e, \<alpha> (map (\<lambda>v. (v, Top)) (thd3 e) @ \<sigma>'))" by auto
         
         let ?f = "ass ((foldl op \<otimes> Emp_int \<circ> map 
           (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) \<circ> \<gamma>) (\<alpha> \<sigma>'))"
         
         from Inr and dnhoi[OF aktjb Inr] have
           "coms_com (snd3 e) (cs ! i)" by auto
         hence 
           nrmyv: "(cs ! i) \<in> coms_com (snd3 e)" by (metis mem_def)
         from Inr aktjb have "Inr e \<in> set \<pi>" by (metis nth_mem)
         with eagbg have "e \<in> set E" by auto
         from aprie[OF this] nrmyv have
           "prov_triple (ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))), 
           cs ! i, ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))))" by auto
         hence
           "prov_triple (ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))) \<ast> ?f, 
           cs!i, ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))) \<ast> ?f)" 
           using prov_triple.frame and no_var_interference 
           by auto
         moreover
         have kqrdm: "map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
           (map (\<lambda>v. (v, Bot)) (fst3 e)) 
           = map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e)" by auto
         have jrlxz: "map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
           (map (\<lambda>v. (v, Top)) (thd3 e)) 
           = map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e)" by auto
         
         have "((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
           (nthtriple (cook ?G ?\<Pi>) i)) = 
           (ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))) \<ast> ?f, cs!i, 
           ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))) \<ast> ?f)" 
         proof (intro tripleI)
           have "fst3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i))
             = ass (fst3 (nthtriple (cook ?G ?\<Pi>) i))"
             unfolding split_def fst3_def by auto
           also have "... = ass (foldl op \<otimes> Emp_int 
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) 
             (\<gamma> (fst3 (nthtriple ?\<Pi> i)))))"
              unfolding cook.simps nthtriple_chainmap[OF iyuyo]
                fst3_comp by auto
           also have "... = ass (foldl op \<otimes> Emp_int
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> ([(v, Bot). v \<leftarrow> fst3 e] @ \<sigma>')))))" 
             unfolding rraei fst3_def by auto
           also have "... = ass (foldr op \<otimes> 
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> ([(v, Bot). v \<leftarrow> fst3 e] @ \<sigma>')))) Emp_int)"
             using ass_foldl_foldr by auto
           also have "... = ass (((foldr (op \<otimes>) (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) 
             ([(v, Bot). v \<leftarrow> fst3 e] @ \<gamma> (\<alpha> \<sigma>'))) Emp_int)))" 
             apply (intro ass_perm_int map_perm)
             apply (metis Quotient_proofstate perm_append1 perm_refl
               rep_abs_rsp rep_abs_rsp_left)
             done
           also have "... = ass (foldr op \<otimes>
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (map (\<lambda>v. (v, Bot)) (fst3 e)) @
             map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> \<sigma>')))
             Emp_int)" unfolding map_append by auto
           also have "... = ass (((foldr (op \<otimes>) ((map (\<lambda>v. bot_ass 
             (\<Lambda> v)) (fst3 e)) @ map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))) Emp_int)))" unfolding kqrdm by auto
           also have "... = ass (foldr op \<otimes> (map (\<lambda>v. bot_ass (\<Lambda> v))
             (fst3 e)) ((foldr (op \<otimes>) (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))) Emp_int)))" by auto
           also have "... = ass ((foldr op \<otimes> (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e)) Emp_int) \<otimes>
         (foldr op \<otimes>
          (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
            (\<gamma> (\<alpha> \<sigma>')))
          Emp_int))" unfolding foldr_hcomp by auto
           also have "... = ass ((foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))) \<otimes> 
             ((foldl (op \<otimes>) Emp_int (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))))))" 
             using ass_foldl_foldr by auto
           also have "... = ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))) \<ast> ?f" by auto
           finally have "fst3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i)) 
             = ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))) \<ast> ?f" by auto
           thus "fst3 ((\<lambda>(P, _, Q). (ass P, cs ! i, ass Q))
             (nthtriple (cook ?G ?\<Pi>) i)) =
             fst3 (ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))) \<ast> ?f, cs ! i, 
             ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))) \<ast> ?f)" unfolding fst3_def by auto
         next
           have cojiq: "\<And>X Y. snd3 ((\<lambda>(P,_,Q). (ass P, Y, ass Q)) X) 
             = Y" unfolding snd3_def by auto
           have "snd3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i)) 
             = cs!i" unfolding cojiq by auto
           thus "snd3 ((\<lambda>(P, _, Q). (ass P, cs ! i, ass Q))
             (nthtriple (cook ?G ?\<Pi>) i)) =
             snd3 (ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))) \<ast> ?f, cs ! i, 
             ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))) \<ast> ?f)" unfolding snd3_def by auto
         next
           have "thd3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i))
             = ass (thd3 (nthtriple (cook ?G ?\<Pi>) i))"
             unfolding split_def thd3_def by auto
           also have "... = ass (foldl op \<otimes> Emp_int 
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) 
             (\<gamma> (thd3 (nthtriple ?\<Pi> i)))))"
              unfolding cook.simps nthtriple_chainmap[OF iyuyo]
                thd3_comp by auto
           also have "... = ass (foldl op \<otimes> Emp_int
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> ([(v, Top). v \<leftarrow> thd3 e] @ \<sigma>')))))" 
             unfolding rraei thd3_def by auto
           also have "... = ass (foldr op \<otimes> 
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> ([(v, Top). v \<leftarrow> thd3 e] @ \<sigma>')))) Emp_int)"
             using ass_foldl_foldr by auto
           also have "... = ass (((foldr (op \<otimes>) (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) 
             ([(v, Top). v \<leftarrow> thd3 e] @ \<gamma> (\<alpha> \<sigma>'))) Emp_int)))" 
             apply (intro ass_perm_int map_perm)
             apply (metis Quotient_proofstate perm_append1 perm_refl
               rep_abs_rsp rep_abs_rsp_left)
             done
           also have "... = ass (foldr op \<otimes>
             (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (map (\<lambda>v. (v, Top)) (thd3 e)) @
             map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
             (\<gamma> (\<alpha> \<sigma>')))
             Emp_int)" unfolding map_append by auto
           also have "... = ass (((foldr (op \<otimes>) ((map (\<lambda>v. top_ass 
             (\<Lambda> v)) (thd3 e)) @ map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))) Emp_int)))" unfolding jrlxz by auto
           also have "... = ass (foldr op \<otimes> (map (\<lambda>v. top_ass (\<Lambda> v))
             (thd3 e)) ((foldr (op \<otimes>) (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))) Emp_int)))" by auto
           also have "... = ass ((foldr op \<otimes> (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e)) Emp_int) \<otimes>
         (foldr op \<otimes>
          (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
            (\<gamma> (\<alpha> \<sigma>')))
          Emp_int))" unfolding foldr_hcomp by auto
           also have "... = ass ((foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))) \<otimes> 
             ((foldl (op \<otimes>) Emp_int (map 
             (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v)) ( \<gamma> 
             (\<alpha> \<sigma>'))))))" 
             using ass_foldl_foldr by auto
           also have "... = ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))) \<ast> ?f" by auto
           finally have "thd3 ((\<lambda>(P,_,Q). (ass P, cs!i, ass Q)) 
             (nthtriple (cook ?G ?\<Pi>) i)) 
             = ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))) \<ast> ?f" by auto
           thus "thd3 ((\<lambda>(P, _, Q). (ass P, cs ! i, ass Q))
             (nthtriple (cook ?G ?\<Pi>) i)) =
             thd3 (ass (foldl op \<otimes> Emp_int (map (\<lambda>v. bot_ass (\<Lambda> v)) (fst3 e))) \<ast> ?f, cs ! i, 
             ass (foldl op \<otimes> Emp_int (map (\<lambda>v. top_ass (\<Lambda> v)) (thd3 e))) \<ast> ?f)" unfolding thd3_def by auto
         qed
         ultimately  
         show ?thesis by auto
       qed
     qed

     moreover

     have "ass (top_dia ?G) = ass (pre (cook ?G ?\<Pi>))"
     proof -
       let ?lhs = "ass (top_dia ?G)"
       let ?rhs = "ass (pre (cook ?G ?\<Pi>))"
       have "?lhs = ass (foldl op \<otimes> Emp_int
         (map (\<lambda>v. top_ass (\<Lambda> v)) (initials ?G)))" by auto
       also have "... = foldl op \<ast> Emp (map ass 
         (map (\<lambda>v. top_ass (\<Lambda> v)) (initials ?G)))"
         using ass_fold_hcomp by auto
       also have "... = foldl op \<ast> Emp 
         (map (\<lambda>v. ass (top_ass (\<Lambda> v))) (initials ?G))" 
         unfolding map_map comp_def by auto 
       also have "... = foldl op \<ast> Emp
         (map (\<lambda>(v,z). ass (top_ass (\<Lambda> v))) 
         [(v,Top) . v \<leftarrow> initials ?G])" 
         unfolding map_map comp_def by auto
       also have "... = foldl op \<ast> Emp
         (map (\<lambda>(v, z). ass (topbot_case top_ass bot_ass z (\<Lambda> v)))
         [(v,Top) . v \<leftarrow> initials ?G])" 
         unfolding map_map comp_def by auto
       also have "... = foldl op \<ast> Emp (
         (map (\<lambda>(v, z). ass (topbot_case top_ass bot_ass z (\<Lambda> v)))
         (\<gamma> (pre ?\<Pi>))))" 
         by (intro ass_perm map_perm, 
           metis conc_abs perm_sym pre.simps(1) pre_mk)     
       also have "... = foldl op \<ast> Emp (map ass (
         (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
         (\<gamma> (pre ?\<Pi>)))))" unfolding map_map comp_def split_def by auto
       also have "... = ass (foldl op \<otimes> Emp_int
         (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
         (\<gamma> (pre ?\<Pi>))))" using ass_fold_hcomp by auto
       also have "... = ?rhs"
         by (auto simp add: pre_chainmap)
       finally show "?lhs = ?rhs" by auto 
     qed

     moreover

     have "ass (bot_dia ?G) = ass (post (cook ?G ?\<Pi>))"
     proof -
       let ?lhs = "ass (bot_dia ?G)"
       let ?rhs = "ass (post (cook ?G ?\<Pi>))"
       have "?lhs = ass (foldl op \<otimes> Emp_int
         (map (\<lambda>v. bot_ass (\<Lambda> v)) (terminals ?G)))" by auto
       also have "... = foldl op \<ast> Emp (map ass 
         (map (\<lambda>v. bot_ass (\<Lambda> v)) (terminals ?G)))"
         using ass_fold_hcomp by auto
       also have "... = foldl op \<ast> Emp 
         (map (\<lambda>v. ass (bot_ass (\<Lambda> v))) (terminals ?G))" 
         unfolding map_map comp_def by auto 
       also have "... = foldl op \<ast> Emp
         (map (\<lambda>(v,z). ass (bot_ass (\<Lambda> v))) 
         [(v,Bot) . v \<leftarrow> terminals ?G])" 
         unfolding map_map comp_def by auto
       also have "... = foldl op \<ast> Emp
         (map (\<lambda>(v, z). ass (topbot_case top_ass bot_ass z (\<Lambda> v)))
         [(v,Bot) . v \<leftarrow> terminals ?G])" 
         unfolding map_map comp_def by auto
       also have "... = foldl op \<ast> Emp (
         (map (\<lambda>(v, z). ass (topbot_case top_ass bot_ass z (\<Lambda> v)))
         (\<gamma> (post ?\<Pi>))))" 
         apply (intro ass_perm map_perm) 
         apply (metis perm_sym lisdi) 
         done
       also have "... = foldl op \<ast> Emp (map ass (
         (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
         (\<gamma> (post ?\<Pi>)))))" unfolding map_map comp_def split_def by auto
       also have "... = ass (foldl op \<otimes> Emp_int
         (map (\<lambda>(v, z). topbot_case top_ass bot_ass z (\<Lambda> v))
         (\<gamma> (post ?\<Pi>))))" using ass_fold_hcomp by auto
       also have "... = ?rhs"
         by (auto simp add: post_chainmap)
       finally show "?lhs = ?rhs" by auto 
     qed
     ultimately
     show "prov_triple (ass (top_dia ?G), c, ass (bot_dia ?G))"
       by auto
   qed
 qed
      
theorem var_soundness:
  assumes "\<And>c. wr_com c = {}"
  assumes "prov_dia G P Q"
  shows "\<forall>c \<in> coms_dia G. prov_triple (ass P, c, ass Q)"
using var_soundness_helper[OF assms(1)] and assms(2) by auto  

end