Theory Irreducible

(*  Title:    Irreducible.thy
    Author:   Max Wagner
*)

section ‹Minimality under Irreducible Control Flow›

txt ‹Braun~et~al.~\<^cite>‹"braun13cc"› provide an extension to the original construction algorithm to ensure
minimality according to Cytron's definition even in the case of irreducible control flow. This extension
establishes the property of being \emph{redundant-scc-free}, i.e.\ the resulting graph $G$ contains no
subsets inducing a strongly connected subgraph $G'$ via \pf s such that $G'$ has less than two
$\phi$ arguments in $G\setminus G'$. In this section we will show that a graph with this property is Cytron-minimal.

Our formalization follows the proof sketch given in \<^cite>‹"braun13cc"›.
We first provide a formal proof of Lemma 1 from \<^cite>‹"braun13cc"› which states that every redundant set of \pf s contains at least one redundant SCC.
A redundant set of \pf s is a set $P$ of \pf s with $P \cup \{v\} \supseteq A$, where $A$ is the union over all \pf s arguments contained in $P$.
I.e.\ $P$ references at most one SSA value ($v$) outside $P$.
A redundant SCC is a redundant set that is strongly connected according to the \emph{is-argument} relation.

Next, we show that a CFG in SSA form without redundant sets of \pf s is Cytron-minimal.

Finally putting those results together, we conclude that the extension to Braun~et~al.'s algorithm always produces minimal SSA form.
›

theory Irreducible
  imports Formal_SSA.Minimality
begin

context CFG_SSA_Transformed
begin


subsection ‹Proof of Lemma 1 from Braun~et~al.›

txt ‹To preserve readability, we won't distinguish between graph nodes and the \pf s contained inside such a node.›

txt ‹The graph induced by the $\phi$ network contained in the vertex set @{term P}. Note that the edges
of this graph are not necessarily a subset of the edges of the input graph.›
definition "induced_phi_graph g P ≡ {(φ,φ'). phiArg g φ φ'} ∩ P × P"

txt ‹For the purposes of this section, we define a "redundant set" as a nonempty set of \pf s with
at most one $\phi$ argument outside itself. A redundant SCC is defined analogously. Note that since
any uses of values in a redundant set can be replaced by uses of its singular argument (without
modifying program semantics), the name is adequate.›
definition "redundant_set g P ≡ P ≠ {} ∧ P ⊆ dom (phi g) ∧ (∃v' ∈ allVars g. ∀φ ∈ P. ∀φ'. phiArg g φ φ' ⟶ φ' ∈ P ∪ {v'})"
definition "redundant_scc g P scc ≡ redundant_set g scc ∧ is_scc (induced_phi_graph g P) scc"

txt ‹We prove an important lemma via condensation graphs of $\phi$ networks, so the relevant definitions are introduced here.›
definition "condensation_nodes g P ≡ scc_of (induced_phi_graph g P) ` P"
definition "condensation_edges g P ≡ ((λ(x,y). (scc_of (induced_phi_graph g P) x, scc_of (induced_phi_graph g P) y)) ` (induced_phi_graph g P)) - Id"


txt ‹For a finite @{term P}, the condensation graph induced by @{term P} is finite and acyclic.›

lemma condensation_finite: "finite (condensation_edges g P)"
txt ‹The set of edges of the condensation graph, spanning at most all $\phi$ nodes and their arguments (both of which are finite sets), is finite itself.›
proof -
  let ?phiEdges="{(a,b). phiArg g a b}"
  have "finite ?phiEdges"
  proof -
    let ?phiDomRan="(dom (phi g) × ⋃ (set ` (ran (phi g))))"
    from phi_finite
    have "finite ?phiDomRan" by (simp add: imageE phi_finite map_dom_ran_finite)
    have "?phiEdges ⊆ ?phiDomRan"
     apply (rule subst[of "∀a ∈ ?phiEdges. a ∈ ?phiDomRan"])
      apply (simp_all add: subset_eq[symmetric] phiArg_def)
     by (auto simp: ran_def)
    with ‹finite ?phiDomRan›
    show "finite ?phiEdges" by (rule Finite_Set.rev_finite_subset)
  qed
  hence "⋀f. finite (f ` (?phiEdges ∩ (P × P)))" by auto
  thus "finite (condensation_edges g P)" unfolding condensation_edges_def induced_phi_graph_def by auto
qed


txt ‹auxiliary lemmas for acyclicity›

lemma condensation_nodes_edges: "(condensation_edges g P) ⊆ (condensation_nodes g P × condensation_nodes g P)"
unfolding condensation_edges_def condensation_nodes_def induced_phi_graph_def
by auto


lemma condensation_edge_impl_path:
assumes "(a, b) ∈ (condensation_edges g P)"
assumes "(φ⇩a ∈ a)"
assumes "(φ⇩b ∈ b)"
shows "(φ⇩a, φ⇩b) ∈ (induced_phi_graph g P)⇧*"
unfolding condensation_edges_def
proof -
  from assms(1)
  obtain x y where x_y_props:
    "(x, y) ∈ (induced_phi_graph g P)"
    "a = scc_of (induced_phi_graph g P) x"
    "b = scc_of (induced_phi_graph g P) y"
   unfolding condensation_edges_def by auto
  hence "x ∈ a" "y ∈ b" by auto

  txt ‹All that's left is to combine these paths.›
  with assms(2) x_y_props(2)
  have "(φ⇩a, x) ∈ (induced_phi_graph g P)⇧*" by (meson is_scc_connected scc_of_is_scc)
  moreover with assms(3) x_y_props(3) ‹y ∈ b›
  have "(y, φ⇩b) ∈ (induced_phi_graph g P)⇧*" by (meson is_scc_connected scc_of_is_scc)
  ultimately
  show "(φ⇩a, φ⇩b) ∈ (induced_phi_graph g P)⇧*" using x_y_props(1)  by auto
qed


lemma path_in_condensation_impl_path:
assumes "(a, b) ∈ (condensation_edges g P)⇧+"
assumes "(φ⇩a ∈ a)"
assumes "(φ⇩b ∈ b)"
shows "(φ⇩a, φ⇩b) ∈ (induced_phi_graph g P)⇧*"
using assms
proof (induction arbitrary: φ⇩b rule:trancl_induct)
  fix y z φ⇩b
  assume "(y, z) ∈ condensation_edges g P"

  hence "is_scc (induced_phi_graph g P) y" unfolding condensation_edges_def by auto
  hence "∃φ⇩y. φ⇩y ∈ y" using scc_non_empty' by auto
  then obtain φ⇩y where φ⇩y_in_y: "φ⇩y ∈ y" by auto

  assume φ⇩b_elem: "φ⇩b ∈ z"
  assume "⋀φ⇩b. φ⇩a ∈ a ⟹ φ⇩b ∈ y ⟹ (φ⇩a, φ⇩b) ∈ (induced_phi_graph g P)⇧*"
  with assms(2) φ⇩y_in_y
  have φ⇩a_to_φ⇩y: "(φ⇩a, φ⇩y) ∈ (induced_phi_graph g P)⇧*" using condensation_edge_impl_path by auto

  from φ⇩b_elem φ⇩y_in_y ‹(y, z) ∈ condensation_edges g P›
  have "(φ⇩y, φ⇩b) ∈ (induced_phi_graph g P)⇧*" using condensation_edge_impl_path by auto
  with φ⇩a_to_φ⇩y
  show "(φ⇩a, φ⇩b) ∈ (induced_phi_graph g P)⇧*"  by auto
qed (auto intro:condensation_edge_impl_path)


lemma condensation_acyclic: "acyclic (condensation_edges g P)"
proof (rule acyclicI, rule allI, rule ccontr, simp)
  fix x
  txt ‹Assume there is a cycle in the condensation graph.›
  assume cyclic: "(x, x) ∈ (condensation_edges g P)⇧+"
  have nonrefl: "(x, x) ∉ (condensation_edges g P)" unfolding condensation_edges_def by auto
  txt ‹Then there must be a second SCC ‹b› on this path.›
  from this cyclic
  obtain b where b_on_path: "(x, b) ∈ (condensation_edges g P)" "(b, x) ∈ (condensation_edges g P)⇧+"
   by (meson converse_tranclE)

  hence "x ∈ (condensation_nodes g P)" "b ∈ (condensation_nodes g P)" using condensation_nodes_edges by auto
  hence nodes_are_scc: "is_scc (induced_phi_graph g P) x" "is_scc (induced_phi_graph g P) b"
    using scc_of_is_scc unfolding induced_phi_graph_def condensation_nodes_def by auto

  txt ‹However, the existence of this path means all nodes in @{term b} and @{term x} are mutually reachable.›
  have "∃φ⇩x. φ⇩x ∈ x" "∃φ⇩b. φ⇩b ∈ b" using nodes_are_scc scc_non_empty' ex_in_conv by auto
  then obtain φ⇩x φ⇩b where φxb_elem: "φ⇩x ∈ x" "φ⇩b ∈ b" by metis
  with nodes_are_scc(1) b_on_path path_in_condensation_impl_path condensation_edge_impl_path φxb_elem(2)
  have "φ⇩b ∈ x"
   by - (rule is_scc_closed)
  txt ‹This however means @{term x} and @{term b} must be the same SCC, which is a contradiction to the nonreflexivity of @{theory_text condensation_edges}.›
  with nodes_are_scc φxb_elem
  have "x = b" using is_scc_unique[of "induced_phi_graph g P"] by simp
  hence "(x, x) ∈ (condensation_edges g P)" using b_on_path by simp
  with nonrefl
  show "False" by simp
qed


txt ‹Since the condensation graph of a set is acyclic and finite, it must have a leaf.›
lemma Ex_condensation_leaf:
assumes "P ≠ {}"
shows "∃leaf. leaf ∈ (condensation_nodes g P) ∧ (∀ scc.(leaf, scc) ∉ condensation_edges g P)"
proof -
  from assms obtain x where "x ∈ condensation_nodes g P" unfolding condensation_nodes_def by auto
  show ?thesis
  proof (rule wfE_min)
    from condensation_finite condensation_acyclic
    show "wf ((condensation_edges g P)¯)" by (rule finite_acyclic_wf_converse)
  next
    fix leaf
    assume leaf_node: "leaf ∈ condensation_nodes g P"
    moreover
    assume leaf_is_leaf: "scc ∉ condensation_nodes g P" if "(scc, leaf) ∈ (condensation_edges g P)¯" for scc
    ultimately
    have "leaf ∈ condensation_nodes g P ∧ (∀scc. (leaf, scc) ∉ condensation_edges g P)" using condensation_nodes_edges by blast
    thus "∃leaf. leaf ∈ condensation_nodes g P ∧ (∀scc. (leaf, scc) ∉ condensation_edges g P)" by blast
  qed fact
qed


lemma scc_in_P:
assumes "scc ∈ condensation_nodes g P"
shows "scc ⊆ P"
proof -
  have "scc ⊆ P" if y_props: "scc = scc_of (induced_phi_graph g P) n" "n ∈ P" for n
  proof -
    from y_props
    show "scc ⊆ P"
    proof (clarsimp simp:y_props(1); case_tac "n = x")
      fix x
      assume different: "n ≠ x"
      assume "x ∈ scc_of (induced_phi_graph g P) n"
      hence "(n, x) ∈ (induced_phi_graph g P)⇧*" by (metis is_scc_connected scc_of_is_scc node_in_scc_of_node)
      with different
      have "(n, x) ∈ (induced_phi_graph g P)⇧+" by (metis rtranclD)
      then obtain z where step: "(z, x) ∈ (induced_phi_graph g P)" by (meson tranclE)
      from step
      show "x ∈ P" unfolding induced_phi_graph_def by auto
    qed simp
  qed
  from this assms(1) have "x ∈ P" if x_node: "x ∈ scc" for x
   apply -
   apply (rule imageE[of scc "scc_of (induced_phi_graph g P)"])
    using condensation_nodes_def x_node by blast+
  thus ?thesis by clarify
qed


lemma redundant_scc_phis:
assumes "redundant_set g P" "scc ∈ condensation_nodes g P" "x ∈ scc"
shows "phi g x ≠ None"
using assms by (meson domIff redundant_set_def scc_in_P subsetCE)


txt ‹The following lemma will be important for the main proof of this section.
If @{term P} is redundant, a leaf in the condensation graph induced by P corresponds to a strongly connected set
with at most one argument, thus a redundant strongly connected set exists.›

txt ‹Lemma 1. Every redundant set contains a redundant SCC.›

lemma 1:
assumes "redundant_set g P"
shows "∃scc ⊆ P. redundant_scc g P scc"
proof -
  from assms Ex_condensation_leaf[of P g]
  obtain leaf where leaf_props: "leaf ∈ (condensation_nodes g P)" "∀scc. (leaf, scc) ∉ condensation_edges g P"
   unfolding redundant_set_def by auto
  hence "is_scc (induced_phi_graph g P) leaf" unfolding condensation_nodes_def by auto
  moreover
  hence "leaf ≠ {}" by (rule scc_non_empty')
  moreover
  have "leaf ⊆ dom (phi g)"
    apply (subst subset_eq, rule ballI)
    using redundant_scc_phis leaf_props(1) assms(1) by auto
  moreover
  from assms
  obtain pred where pred_props: "pred ∈ allVars g" "∀φ∈P. ∀φ'. phiArg g φ φ' ⟶ φ' ∈ P ∪ {pred}" unfolding redundant_set_def by auto
  {
    txt ‹Any argument of a \pf\ in the leaf SCC which is \emph{not} in the leaf SCC itself must be the unique argument of P›
    fix φ φ'

    consider (in_P) "φ' ∉ leaf ∧ φ' ∈ P" | (neither) "φ' ∉ leaf ∧ φ' ∉ P ∪ {pred}" | "φ' ∉ leaf ∧ φ' ∈ {pred}" | "φ' ∈ leaf" by auto
    hence "φ' ∈ leaf ∪ {pred}" if "φ ∈ leaf" and "phiArg g φ φ'"
    proof cases
      case in_P ― ‹In this case @{term leaf} wasn't really a leaf, a contradiction›
      moreover
      from in_P that leaf_props(1) scc_in_P[of leaf g P]
      have "(φ, φ') ∈ induced_phi_graph g P" unfolding induced_phi_graph_def by auto
      ultimately
      have "(leaf, scc_of (induced_phi_graph g P) φ') ∈ condensation_edges g P" unfolding condensation_edges_def
       using leaf_props(1) that ‹is_scc (induced_phi_graph g P) leaf›
       apply -
       apply clarsimp
       apply (rule conjI)
        prefer 2
        apply auto[1]
       unfolding condensation_nodes_def
       by (metis (no_types, lifting) is_scc_unique node_in_scc_of_node pair_imageI scc_of_is_scc)
      with leaf_props(2)
      show ?thesis by auto
    next
      case neither ― ‹In which case @{term P} itself wasn't redundant, a contradiction›
      with that leaf_props pred_props
      have "¬redundant_set g P" unfolding redundant_set_def
        by (meson rev_subsetD scc_in_P)
      with assms
      show ?thesis by auto
    qed auto ― ‹the other cases are trivial›
  }
  with pred_props(1)
  have "∃v'∈allVars g. ∀φ∈leaf. ∀φ'. phiArg g φ φ' ⟶ φ' ∈ leaf ∪ {v'}"  by auto
  ultimately
  have "redundant_scc g P leaf" unfolding redundant_scc_def redundant_set_def by auto
  thus ?thesis using leaf_props(1) scc_in_P by meson
qed

subsection ‹Proof of Minimality›

txt ‹We inductively define the reachable-set of a \pf\ as all \pf s reachable from a given node via an
unbroken chain of $\phi$ argument edges to unnecessary \pf s.›

inductive_set reachable :: "'g ⇒ 'val ⇒ 'val set"
  for g :: "'g" and φ :: "'val"
  where refl: "unnecessaryPhi g φ ⟹ φ ∈ reachable g φ"
  | step: "φ' ∈ reachable g φ ⟹ phiArg g φ' φ'' ⟹ unnecessaryPhi g φ'' ⟹ φ'' ∈ reachable g φ"


lemma reachable_props:
  assumes "φ' ∈ reachable g φ"
  shows "(phiArg g)⇧*⇧* φ φ'" and "unnecessaryPhi g φ'"
  using assms
  by (induction φ' rule: reachable.induct) auto


txt ‹We call the transitive arguments of a \pf\ not in its reachable-set the "true arguments" of this \pf.›
definition [simp]: "trueArgs g φ ≡ {φ'. φ' ∉ reachable g φ} ∩ {φ'. ∃φ'' ∈ reachable g φ. phiArg g φ'' φ'}"


lemma preds_finite: "finite (trueArgs g φ)"
proof (rule ccontr)
  assume "infinite (trueArgs g φ)"
  hence a: "infinite {φ'. ∃φ'' ∈ reachable g φ. phiArg g φ'' φ'}" by auto
  have phiarg_set: "{φ'. ∃φ. phiArg g φ φ'} = ⋃ (set `{b. ∃a. phi g a = Some b})" unfolding phiArg_def by auto
  txt ‹If the true arguments of a \pf\ are infinite in number, there must be an infinite number of \pf s\ldots›
  have "infinite {φ'. ∃φ. phiArg g φ φ'}"
    by (rule infinite_super[of "{φ'. ∃φ'' ∈ reachable g φ. phiArg g φ'' φ'}"])  (auto simp: a)
  with phiarg_set
  have "infinite (ran (phi g))" unfolding ran_def phiArg_def by clarsimp
  txt ‹Which cannot be.›
  thus False by (simp add:phi_finite map_dom_ran_finite)
qed


txt ‹Any unnecessary $\phi$ with less than 2 true arguments induces with @{term "reachable g φ"} a redundant set itself.›

lemma few_preds_redundant:
assumes "card (trueArgs g φ) < 2" "unnecessaryPhi g φ"
shows "redundant_set g (reachable g φ)"
unfolding redundant_set_def
proof (intro conjI)
  from assms
  show "reachable g φ ≠ {}"
    using empty_iff reachable.intros(1) by auto
next
  from assms(2)
  show "reachable g φ ⊆ dom (phi g)"
    by (metis domIff reachable.cases subsetI unnecessaryPhi_def)
next
  from assms(1)
  consider (single) "card (trueArgs g φ) = 1" | (empty) "card (trueArgs g φ) = 0" by force
  thus "∃pred∈allVars g. ∀φ'∈reachable g φ. ∀φ''. phiArg g φ' φ'' ⟶ φ'' ∈ reachable g φ ∪ {pred}"
  proof cases
    case single
    then obtain pred where pred_prop: "trueArgs g φ = {pred}" using card_eq_1_singleton by blast
    hence "pred ∈ allVars g" by (auto intro: Int_Collect phiArg_in_allVars)
    moreover
    from pred_prop
    have "∀φ'∈reachable g φ. ∀φ''. phiArg g φ' φ'' ⟶ φ'' ∈ reachable g φ ∪ {pred}" by auto
    ultimately
    show ?thesis by auto
  next
    case empty
    from allDefs_in_allVars[of _ g "defNode g φ"] assms
    have phi_var: "φ ∈ allVars g" unfolding unnecessaryPhi_def phiDefs_def allDefs_def defNode_def phi_def trueArgs_def
      by (clarsimp simp: domIff phis_in_αn)
    from empty assms(1)
    have no_preds: "trueArgs g φ = {}"  by (subst card_0_eq[OF preds_finite, symmetric]) auto
    show ?thesis
    proof (rule bexI, rule ballI, rule allI, rule impI)
      fix φ' φ''
      assume phis_props: "φ' ∈ reachable g φ" "phiArg g φ' φ''"
      with no_preds
      have "φ'' ∈ reachable g φ"
      unfolding trueArgs_def
      proof -
        from phis_props
        have "φ'' ∈ {φ'. ∃φ''∈reachable g φ. phiArg g φ'' φ'}" by auto
        with phis_props no_preds
        show "φ'' ∈ reachable g φ" unfolding trueArgs_def by auto
      qed
      thus "φ'' ∈ reachable g φ ∪ {φ}" by simp
    qed (auto simp: phi_var)
  qed
qed


lemma phiArg_trancl_same_var:
assumes "(phiArg g)⇧+⇧+ φ n"
shows "var g φ = var g n"
using assms
apply (induction rule: tranclp_induct)
  apply (rule phiArg_same_var[symmetric])
  apply simp
 using phiArg_same_var by auto


txt ‹The following path extension lemma will be used a number of times in the inner induction of the
main proof. Basically, the idea is to extend a path ending in a $\phi$ argument to the corresponding \pf\ 
while preserving disjointness to a second path.›

lemma phiArg_disjoint_paths_extend:
assumes "var g r = V" and "var g s = V" and "r ∈ allVars g" and "s ∈ allVars g"
and "V ∈ oldDefs g n" and "V ∈ oldDefs g m"
and "g ⊢ n-ns→defNode g r" and "g ⊢ m-ms→defNode g s"
and "set ns ∩ set ms = {}"
and "phiArg g φ⇩r r"
obtains ns'
where "g ⊢ n-ns@ns'→defNode g φ⇩r"
and "set (butlast (ns@ns')) ∩ set ms = {}"
proof (cases "r = φ⇩r")
  case (True)
  txt ‹If the node to extend the path to is already the endpoint, the lemma is trivial.›
  with assms(7,8,9) in_set_butlastD
  have "g ⊢ n-ns@[]→defNode g φ⇩r" "set (butlast (ns@[])) ∩ set ms = {}"
    by simp_all fastforce
  with that show ?thesis .
next
  case False
  txt ‹It suffices to obtain any path from r to @{term φ⇩r}.
     However, since we'll need the corresponding predecessor of @{term φ⇩r} later, we must do this as follows:›
  from assms(10)
  have "φ⇩r ∈ allVars g" unfolding phiArg_def
    by (metis allDefs_in_allVars phiDefs_in_allDefs phi_def phi_phiDefs phis_in_αn)
  with assms(10)
  obtain rs' pred⇩φ⇩r where rs'_props: "g ⊢ defNode g r-rs'→ pred⇩φ⇩r" "old.EntryPath g rs'" "r ∈ phiUses g pred⇩φ⇩r" "pred⇩φ⇩r ∈ set (old.predecessors g (defNode g φ⇩r))"
   by (rule phiArg_path_ex')

  define rs where "rs = rs'@[defNode g φ⇩r]"
  from rs'_props(2,1) old.EntryPath_distinct old.path2_hd
  have rs'_loopfree: "defNode g r ∉ set (tl rs')"  by (simp add: Misc.distinct_hd_tl)

  from False assms have "defNode g φ⇩r ≠ defNode g r"
   apply -
   apply (rule phiArg_distinct_nodes)
     apply (auto intro:phiArg_in_allVars)[2]
   unfolding phiArg_def by (metis allDefs_in_allVars phiDefs_in_allDefs phi_def phi_phiDefs phis_in_αn)

  from rs'_props
  have rs_props: "g ⊢ defNode g r-rs→ defNode g φ⇩r" "length rs > 1" "defNode g r ∉ set (tl rs)"
     apply (subgoal_tac "defNode g r = hd rs'")
      prefer 2 using rs'_props(1)
     apply (rule old.path2_hd)
     using old.path2_snoc old.path2_def rs'_props(1) rs_def rs'_loopfree ‹defNode g φ⇩r ≠ defNode g r› by auto

  show thesis
  proof (cases "set (butlast rs) ∩ set ms = {}")
    case inter_empty: True
    txt ‹If the intersection of these is empty, @{term "tl rs"} is already the extension we're looking for›
    show thesis
    proof (rule that)
      show "set (butlast (ns @ tl rs)) ∩ set ms = {}"
      proof (rule ccontr, simp only: ex_in_conv[symmetric])
        assume "∃x. x ∈ set (butlast (ns @ tl rs)) ∩ set ms"
        then obtain x where x_props: "x ∈ set (butlast (ns @ tl rs))" "x ∈ set ms" by auto
        with rs_props(2)
        consider (in_ns) "x ∈ set ns" | (in_rs) "x ∈ set (butlast (tl rs))" by (metis Un_iff butlast_append in_set_butlastD set_append)
        thus False
         apply (cases)
          using x_props(2) assms(9)
          apply (simp add: disjoint_elem)
         by (metis x_props(2) inter_empty in_set_tlD List.butlast_tl disjoint_iff_not_equal)
      qed
    qed (auto intro:assms(7) rs_props(1) old.path2_app)
  next
    case inter_ex: False
    txt ‹If the intersection is nonempty, there must be a first point of intersection @{term i}.›
    from inter_ex assms(7,8) rs_props
    obtain i ri where ri_props: "g ⊢ defNode g r-ri→i" "i ∈ set ms" "∀n ∈ set (butlast ri). n ∉ set ms" "prefix ri rs"
     apply -
     apply (rule old.path2_split_first_prop[of g "defNode g r" rs "defNode g φ⇩r", where P="λm. m ∈ set ms"])
       apply blast
      apply (metis disjoint_iff_not_equal in_set_butlastD)
     by blast
    with assms(8) old.path2_prefix_ex
    obtain ms' where ms'_props: "g ⊢ m -ms'→ i" "prefix ms' ms" "i ∉ set (butlast ms')" by blast

    txt ‹We proceed by case distinction:
      ▪ if @{prop "i = defNode g φ⇩r"}, the path @{term ri} is already the path extension we're looking for
      ▪ Otherwise, the fact that @{term i} is on the path from $\phi$ argument to the $\phi$ itself leads to a contradiction.
        However, we still need to distinguish the cases of whether @{prop "m = i"}›
    consider (ri_is_valid) "i = defNode g φ⇩r" | (m_i_same) "i ≠ defNode g φ⇩r" "m = i" | (m_i_differ) "i ≠ defNode g φ⇩r" "m ≠ i" by auto

    thus thesis
    proof (cases)
      case ri_is_valid
      txt ‹@{term ri} is a valid path extension.›
      with assms(7) ri_props(1)
      have "g ⊢ n -ns@(tl ri)→ defNode g φ⇩r" by auto

      moreover
      have "set (butlast (ns@(tl ri))) ∩ set ms = {}"
      proof (rule ccontr)
        assume contr: "set (butlast (ns @ tl ri)) ∩ set ms ≠ {}"
        from this
        obtain x where x_props: "x ∈ set (butlast (ns @ tl ri))" "x ∈ set ms" by auto
        with assms(9) have "x ∉ set ns" by auto
        with x_props ‹g ⊢ n-ns @ tl ri→defNode g φ⇩r› ‹defNode g φ⇩r ≠ defNode g r› assms(7)
        have "x ∈ set (butlast (tl ri))"
         by (metis Un_iff append_Nil2 butlast_append old.path2_last set_append)
        with x_props(2) ri_props(3)
        show "False" by (metis FormalSSA_Misc.in_set_tlD List.butlast_tl)
      qed
      ultimately
      show thesis by (rule that)
    next
      case m_i_same
      txt ‹If @{prop "m = i"}, we have, with @{term m}, a variable definition on the path from a \pf\ to its argument.
          This constitutes a contradiction to the conventional property.›
      note rs'_props(1) rs'_loopfree
      moreover have "r ∈ allDefs g (defNode g r)" by (simp add: assms(3))
      moreover from rs'_props(3) have "r ∈ allUses g pred⇩φ⇩r" unfolding allUses_def by simp

      moreover
      from rs_props(1) m_i_same rs_def ri_props(1,2,4) ‹defNode g φ⇩r ≠ defNode g r› assms(7,9)
      have "m ∈ set (tl rs')"
       by (metis disjoint_elem hd_append in_hd_or_tl_conv in_prefix list.sel(1) old.path2_hd old.path2_last old.path2_last_in_ns prefix_snoc)

      moreover
      from assms(6) obtain def⇩m where "def⇩m ∈ allDefs g m" "var g def⇩m = V" unfolding oldDefs_def using defs_in_allDefs by blast

      ultimately
      have "var g def⇩m ≠ var g r" by - (rule conventional, simp_all)
      with ‹var g def⇩m = V› assms(1)
      have "False" by simp
      thus ?thesis by simp

    next
      case m_i_differ
      txt ‹If @{prop "m ≠ i"}, @{term i} constitutes a proper path convergence point.›
      have "old.pathsConverge g m ms' n (ns @ tl ri) i"
      proof (rule old.pathsConvergeI)
        show "1 < length ms'" using m_i_differ ms'_props old.path2_nontriv by blast
      next
        show "1 < length (ns @ tl ri)"
        using ri_props old.path2_nontriv assms(9) by (metis assms(7) disjoint_elem old.path2_app old.path2_hd_in_ns)
      next
        show "set (butlast ms') ∩ set (butlast (ns @ tl ri)) = {}"
        proof (rule ccontr)
          assume "set (butlast ms') ∩ set (butlast (ns @ tl ri)) ≠ {}"
          then obtain i' where i'_props: "i' ∈ set (butlast ms')" "i' ∈ set (butlast (ns @ tl ri))" by auto
          with ms'_props(2)
          have i'_not_in_ms: "i' ∈ set (butlast ms)" by (metis in_set_butlast_appendI prefixE)

          with assms(9)
          show False
          proof (cases "i' ∉ set ns")
            case True
            with i'_props(2)
            have "i' ∈ set (butlast (tl ri))"
             by (metis Un_iff butlast_append in_set_butlastD set_append)
            hence "i' ∈ set (butlast ri)" by (simp add:in_set_tlD List.butlast_tl)
            with i'_not_in_ms ri_props(3)
            show False by (auto dest:in_set_butlastD)
          qed (meson disjoint_elem in_set_butlastD)
        qed
      qed (auto intro: assms(7) ri_props(1) old.path2_app ms'_props(1))

      txt ‹At this intersection of paths we can find a \pf.›
      from this assms(6,5)
      have "necessaryPhi g V i" by (rule necessaryPhiI)

      txt ‹Before we can conclude that there is indeed a $\phi$ at @{term i}, we have to prove a couple of technicalities\ldots›
      moreover
      from m_i_differ ri_props(1,4) rs_def old.path2_last prefix_snoc
      have ri_rs'_prefix: "prefix ri rs'" by fastforce
      then obtain rs'_rest where rs'_rest_prop: "rs' = ri@rs'_rest" using prefixE by auto
      from old.path2_last[OF ri_props(1)] last_snoc[of _ i] obtain tmp where "ri = tmp@[i]"
       apply (subgoal_tac "ri ≠ []")
        prefer 2
        using ri_props(1) apply (simp add: old.path2_not_Nil)
       apply (rule_tac that)
       using append_butlast_last_id[symmetric] by auto 
      with rs'_rest_prop have rs'_rest_def: "rs' = tmp@i#rs'_rest" by auto
      with rs'_props(1) have "g ⊢ i -i#rs'_rest→ pred⇩φ⇩r"
       by (simp add:old.path2_split)
      moreover
      note ‹var g r = V› [simp]
      from rs'_props(3)
      have "r ∈ allUses g pred⇩φ⇩r" unfolding allUses_def by simp

      moreover
      from ‹defNode g r ∉ set (tl rs')› rs'_rest_def
      have "defNode g r ∉ set rs'_rest" by auto
      with ‹g ⊢ i -i#rs'_rest→ pred⇩φ⇩r›
      have "⋀x. x ∈ set rs'_rest ⟹ r ∉ allDefs g x"
       by (metis defNode_eq list.distinct(1) list.sel(3) list.set_cases old.path2_cases old.path2_in_αn)

      moreover
      from assms(7,9) ‹g ⊢ i -i#rs'_rest→ pred⇩φ⇩r› ri_props(2)
      have "r ∉ defs g i"
       by (metis defNode_eq defs_in_allDefs disjoint_elem old.path2_hd_in_αn old.path2_last_in_ns)
      ultimately

      txt ‹The convergence property gives us that there is a $\phi$ in the last node fulfilling @{theory_text necessaryPhi}
          on a path to a use of @{term r} without a definition of @{term r}.
          Thus @{term i} bears a \pf\ for the value of @{term r}.›

      have "∃y. phis g (i, r) = Some y"
       by (rule convergence_prop [where g=g and n=i and v=r and ns="i#rs'_rest", simplified])
      moreover

      from ‹g ⊢ n-ns→defNode g r› have "defNode g r ∈ set ns" by auto
      with ‹set ns ∩ set ms = {}› ‹i ∈ set ms› have "i ≠ defNode g r" by auto
      moreover

      from ms'_props(1) have "i ∈ set (αn g)" by auto
      moreover

      have "defNode g r ∈ set (αn g)" by (simp add: assms(3))

      txt ‹However, we now have two definitions of @{term r}: one in @{term i}, and one in @{term "defNode g r"}, which we know to be distinct.
          This is a contradiction to the @{theory_text allDefs_disjoint}-property.›
      ultimately have False
        using allDefs_disjoint [where g=g and n=i and m="defNode g r"]
        unfolding allDefs_def phiDefs_def
        apply clarsimp
        apply (erule_tac c=r in equalityCE)
        using phi_def phis_phi by auto
      thus ?thesis by simp
    qed
  qed
qed


lemma reachable_same_var:
assumes "φ' ∈ reachable g φ"
shows "var g φ = var g φ'"
using assms by (metis Nitpick.rtranclp_unfold phiArg_trancl_same_var reachable_props(1))


lemma φ_node_no_defs:
assumes "unnecessaryPhi g φ" "φ ∈ allVars g" "var g φ ∈ oldDefs g n"
shows "defNode g φ ≠ n"
using assms simpleDefs_phiDefs_var_disjoint defNode(1) not_None_eq phi_phiDefs
  unfolding unnecessaryPhi_def by auto


lemma defNode_differ_aux:
assumes "φ⇩s ∈ reachable g φ" "φ ∈ allVars g" "s ∈ allVars g" "φ⇩s ≠ s" "var g φ = var g s"
shows "defNode g φ⇩s ≠ defNode g s" unfolding reachable_def
proof (rule ccontr)
  assume "¬ defNode g φ⇩s ≠ defNode g s"
  hence eq: "defNode g φ⇩s = defNode g s" by simp
  from assms(1)
  have vars_eq: "var g φ = var g φ⇩s"
    apply -
    apply (cases "φ = φ⇩s")
    apply simp
    apply (rule phiArg_trancl_same_var)
    apply (drule reachable_props)
    unfolding reachable_def by (meson IntD1 mem_Collect_eq rtranclpD)
  have φ⇩s_in_allVars: "φ⇩s ∈ allVars g" unfolding reachable_def
  proof (cases "φ = φ⇩s")
    case False
    with assms(1)
    obtain φ' where "phiArg g φ' φ⇩s"  by (metis rtranclp.cases reachable_props(1))
    thus "φ⇩s ∈ allVars g" by (rule phiArg_in_allVars)
  next
    case eq: True
    with assms(2)
    show "φ⇩s ∈ allVars g" by (subst eq[symmetric])
  qed

  from eq φ⇩s_in_allVars assms(3,4)
  have "var g φ⇩s ≠ var g s" by - (rule defNode_var_disjoint)
  with vars_eq assms(5)
  show False by auto
qed


txt ‹Theorem 1. A graph which does not contain any redundant set is minimal according to Cytron et al.'s definition of minimality.›

theorem no_redundant_set_minimal:
assumes no_redundant_set: "¬(∃P. redundant_set g P)"
shows "cytronMinimal g"
proof (rule ccontr)
  assume "¬cytronMinimal g"
  txt ‹Assume the graph is not Cytron-minimal. Thus there is a \pf\ which does not sit at the
      convergence point of multiple liveness intervals.›
  then obtain φ where φ_props: "unnecessaryPhi g φ" "φ ∈ allVars g" "φ ∈ reachable g φ"
  using cytronMinimal_def unnecessaryPhi_def reachable_def unnecessaryPhi_def reachable.intros by auto

  txt ‹We consider the reachable-set of @{term φ}. If @{term φ} has less than two true arguments, we
     know it to be a redundant set, a contradiction. Otherwise, we know there to be at least two
     paths from different definitions leading into the reachable-set of @{term φ}.›

  consider (nontrivial) "card (trueArgs g φ) ≥ 2" | (trivial) "card (trueArgs g φ) < 2" using linorder_not_le by auto
  thus False
  proof cases
    case trivial
    txt ‹If there are less than 2 true arguments of this set, the set is trivially redundant (see @{theory_text few_preds_redundant}).›
    from this φ_props(1)
    have "redundant_set g (reachable g φ)" by (rule few_preds_redundant)
    with no_redundant_set
    show False by simp
  next
    case nontrivial
    txt ‹If there are two or more necessary arguments, there must be disjoint paths from Defs to two of these \pf s.›
    then obtain r s φ⇩r φ⇩s where assign_nodes_props:
      "r ≠ s" "φ⇩r ∈ reachable g φ" "φ⇩s ∈ reachable g φ"
      "¬ unnecessaryPhi g r" "¬ unnecessaryPhi g s"
      "r ∈ {n. (phiArg g)⇧*⇧* φ n}" "s ∈ {n. (phiArg g)⇧*⇧* φ n}"
      "phiArg g φ⇩r r" "phiArg g φ⇩s s"
     apply simp
     apply (rule set_take_two[OF nontrivial])
     apply simp
     by (meson reachable.intros(2) reachable_props(1) rtranclp_tranclp_tranclp tranclp.r_into_trancl tranclp_into_rtranclp)
    moreover from assign_nodes_props
    have φ_r_s_uneq: "φ ≠ r" "φ ≠ s" using φ_props by auto
    moreover
    from assign_nodes_props this
    have r_s_in_tranclp: "(phiArg g)⇧+⇧+ φ r" "(phiArg g)⇧+⇧+ φ s"
      by (meson mem_Collect_eq rtranclpD) (meson assign_nodes_props(7) φ_r_s_uneq(2) mem_Collect_eq rtranclpD)
    from this
    obtain V where V_props: "var g r = V" "var g s = V" "var g φ = V" by (metis phiArg_trancl_same_var)
    moreover
    from r_s_in_tranclp
    have r_s_allVars: "r ∈ allVars g" "s ∈ allVars g" by (metis phiArg_in_allVars tranclp.cases)+
    moreover
    from V_props defNode_var_disjoint r_s_allVars assign_nodes_props(1)
    have r_s_defNode_distinct: "defNode g r ≠ defNode g s" by auto
    ultimately
    obtain n ns m ms where r_s_path_props: "V ∈ oldDefs g n" "g ⊢ n-ns→defNode g r" "V ∈ oldDefs g m" "g ⊢ m-ms→defNode g s"
      "set ns ∩ set ms = {}" by (auto intro: ununnecessaryPhis_disjoint_paths[of g r s])

    have n_m_distinct: "n ≠ m"
    proof (rule ccontr)
      assume n_m: "¬ n ≠ m"
      with r_s_path_props(2) old.path2_hd_in_ns
      have "n ∈ set ns" by blast
      moreover
      from n_m r_s_path_props(4) old.path2_hd_in_ns
      have "n ∈ set ms" by blast
      ultimately
      show False using r_s_path_props(5) by auto
    qed

    txt ‹These paths can be extended into paths reaching \pf s in our set.›

    from V_props r_s_allVars r_s_path_props assign_nodes_props
    obtain rs where rs_props: "g ⊢ n -ns@rs→ defNode g φ⇩r" "set (butlast (ns@rs)) ∩ set ms = {}"
    using phiArg_disjoint_paths_extend by blast

    txt ‹(In fact, we can prove that @{prop "set (ns@rs) ∩ set ms = {}"}, which we need for the next path extension.)›
    have "defNode g φ⇩r ∉ set ms"
    proof (rule ccontr)
      assume φ⇩r_in_ms: "¬ defNode g φ⇩r ∉ set ms"
      from this r_s_path_props(4)
      obtain ms' where ms'_props: "g ⊢ m -ms'→ defNode g φ⇩r" "prefix ms' ms" by -(rule old.path2_prefix_ex[of g m ms "defNode g s" "defNode g φ⇩r"], auto)

      have "old.pathsConverge g n (ns@rs) m ms' (defNode g φ⇩r)"
      proof (rule old.pathsConvergeI)
        show "set (butlast (ns @ rs)) ∩ set (butlast ms') = {}"
        proof (rule ccontr)
          assume "set (butlast (ns @ rs)) ∩ set (butlast ms') ≠ {}"
          then obtain c where c_props: "c ∈ set (butlast (ns@rs))" "c ∈ set (butlast ms')" by auto
          from this(2) ms'_props(2)
          have "c ∈ set ms" by (simp add: in_prefix in_set_butlastD)
          with c_props(1) rs_props(2)
          show False by auto
        qed
      next
        have m_n_φ⇩r_differ: "n ≠ defNode g φ⇩r" "m ≠ defNode g φ⇩r"
          using assign_nodes_props(2,3,4,5) V_props r_s_path_props φ⇩r_in_ms
          apply fastforce
         using V_props(1) φ⇩r_in_ms assign_nodes_props(8) old.path2_in_αn phiArg_def phiArg_same_var r_s_path_props(3,4) simpleDefs_phiDefs_var_disjoint
         by auto
        with ms'_props(1)
        show "1 < length ms'" using old.path2_nontriv by simp
        from m_n_φ⇩r_differ rs_props(1)
        show "1 < length (ns@rs)" using old.path2_nontriv by blast
      qed (auto intro: rs_props set_mono_prefix ms'_props)
      with V_props r_s_path_props
      have "necessaryPhi' g φ⇩r" unfolding necessaryPhi_def using assign_nodes_props(8) phiArg_same_var by auto
      with reachable_props(2)[OF assign_nodes_props(2)]
      show False unfolding unnecessaryPhi_def by simp
    qed

    with rs_props
    have aux: "set ms ∩ set (ns @ rs) = {}"
      by (metis disjoint_iff_not_equal not_in_butlast old.path2_last)

    have φ⇩r_V: "var g φ⇩r = V"
      using V_props(1) assign_nodes_props(8) phiArg_same_var by auto

    have φ⇩r_allVars: "φ⇩r ∈ allVars g"
      by (meson phiArg_def assign_nodes_props(8) allDefs_in_allVars old.path2_tl_in_αn phiDefs_in_allDefs phi_phiDefs rs_props)

    from V_props(2) φ⇩r_V r_s_allVars(2) φ⇩r_allVars r_s_path_props(3) r_s_path_props(1)
             r_s_path_props(4) rs_props(1) aux assign_nodes_props(9)
    obtain ss where ss_props: "g ⊢ m -ms@ss→ defNode g φ⇩s" "set (butlast (ms@ss)) ∩ set (butlast (ns@rs)) = {}"
     by (rule phiArg_disjoint_paths_extend) (metis disjoint_iff_not_equal in_set_butlastD)

    define p⇩m where "p⇩m = ms@ss"
    define p⇩n where "p⇩n = ns@rs"

    have ind_props: "g ⊢ m -p⇩m→ defNode g φ⇩s" "g ⊢ n -p⇩n→ defNode g φ⇩r" "set (butlast p⇩m) ∩ set (butlast p⇩n) = {}"
    using rs_props(1) ss_props p⇩m_def p⇩n_def by auto

    txt ‹The following case will occur twice in the induction, with swapped identifiers, so we're proving it outside.
    Basically, if the paths @{term p⇩m} and @{term p⇩n} intersect, the first such intersection point must be a \pf\ in @{term "reachable g φ"},
    yielding the path convergence we seek.›

    have path_crossing_yields_convergence:
      "∃φ⇩z ∈ reachable g φ. ∃ns ms. old.pathsConverge g n ns m ms (defNode g φ⇩z)"
      if "φ⇩r ∈ reachable g φ" and "φ⇩s ∈ reachable g φ" and "g ⊢ n -p⇩n→ defNode g φ⇩r"
        and "g ⊢ m -p⇩m→ defNode g φ⇩s" and "set (butlast p⇩m) ∩ set (butlast p⇩n) = {}"
        and "set p⇩m ∩ set p⇩n ≠ {}"
      for φ⇩r φ⇩s p⇩m p⇩n
    proof -
      from that(6) split_list_first_propE
      obtain p⇩m1 n⇩z p⇩m2 where n⇩z_props: "n⇩z ∈ set p⇩n" "p⇩m = p⇩m1 @ n⇩z # p⇩m2" "∀n ∈ set p⇩m1. n ∉ set p⇩n"
         by (auto intro: split_list_first_propE)

      with that(3,4)
      obtain p⇩n' where p⇩n'_props: "g ⊢ n-p⇩n'→n⇩z" "g ⊢ m-p⇩m1@[n⇩z]→n⇩z" "prefix p⇩n' p⇩n" "n⇩z ∉ set (butlast p⇩n')"
          by (meson old.path2_prefix_ex old.path2_split(1))

      from V_props(3) reachable_same_var[OF that(1)] reachable_same_var[OF that(2)]
      have phis_V: "var g φ⇩r = V" "var g φ⇩s = V" by simp_all
      from reachable_props(1) that(1,2) φ_props(2) phiArg_in_allVars
      have phis_allVars: "φ⇩r ∈ allVars g" "φ⇩s ∈ allVars g" by (metis rtranclp.cases)+

      txt ‹Various inequalities for proving paths aren't trivial.›
      have "n ≠ defNode g φ⇩r" "m ≠ defNode g φ⇩r"
       using φ_node_no_defs phis_V(1) phis_allVars(1) r_s_path_props(1,3) reachable_props(2) that(1) by blast+

      from φ_node_no_defs reachable_props(2) that(2) r_s_path_props(1,3) phis_V(2) that phis_allVars
      have "m ≠ defNode g φ⇩s" "n ≠ defNode g φ⇩s" by blast+

      txt ‹With this scenario, since @{prop "set (butlast p⇩n) ∩ set (butlast p⇩m) = {}"}, one of the paths @{term p⇩n} and
      @{term p⇩m} must end somewhere within the other, however this means the \pf\ in that node must either be @{term φ} or @{term φ⇩r}›

      from assms n⇩z_props
      consider (p⇩n_ends_in_p⇩m) "n⇩z = defNode g φ⇩s" | (p⇩m_ends_in_p⇩n) "n⇩z = defNode g φ⇩r"
      proof (cases "n⇩z = last p⇩n")
        case True
        with ‹g ⊢ n -p⇩n→ defNode g φ⇩r›
        have "n⇩z = defNode g φ⇩r" using old.path2_last by auto
        with that(2) show ?thesis.
      next
        case False
        from n⇩z_props(2)
        have "n⇩z ∈ set p⇩m" by simp
        with False n⇩z_props(1) ‹set (butlast p⇩m) ∩ set (butlast p⇩n) = {}› ‹g ⊢ m -p⇩m→ defNode g φ⇩s›
        have "n⇩z = defNode g φ⇩s" by (metis disjoint_elem not_in_butlast old.path2_last)
        with that(1) show ?thesis.
      qed

      thus "∃φ⇩z ∈ reachable g φ. ∃ns ms. old.pathsConverge g n ns m ms (defNode g φ⇩z)"
      proof (cases)
        case p⇩n_ends_in_p⇩m
        have "old.pathsConverge g n p⇩n' m p⇩m (defNode g φ⇩s)"
        proof (rule old.pathsConvergeI)
          from p⇩n_ends_in_p⇩m p⇩n'_props(1) show "g ⊢ n-p⇩n'→defNode g φ⇩s" by simp
          from ‹n ≠ defNode g φ⇩s› p⇩n_ends_in_p⇩m p⇩n'_props(1) old.path2_nontriv show "1 < length p⇩n'" by auto
          from that(4) show "g ⊢ m -p⇩m→ defNode g φ⇩s".
          with ‹m ≠ defNode g φ⇩s› old.path2_nontriv show "1 < length p⇩m" by simp
          from that p⇩n'_props(3) show "set (butlast p⇩n') ∩ set (butlast p⇩m) = {}"
           by (meson butlast_prefix disjointI disjoint_elem in_prefix)
        qed
        with that(1,2,3) show ?thesis by (auto intro:reachable.intros(2))
      next
        case p⇩m_ends_in_p⇩n
        have "old.pathsConverge g n p⇩n' m (p⇩m1@[n⇩z]) (defNode g φ⇩r)"
        proof (rule old.pathsConvergeI)
          from p⇩m_ends_in_p⇩n  p⇩n'_props(1,2) show "g ⊢ n-p⇩n'→defNode g φ⇩r" "g ⊢ m-p⇩m1 @ [n⇩z]→defNode g φ⇩r" by simp_all
          with ‹n ≠ defNode g φ⇩r› ‹m ≠ defNode g φ⇩r› show "1 < length p⇩n'" "1 < length (p⇩m1 @ [n⇩z])"
           using old.path2_nontriv[of g m "p⇩m1 @ [n⇩z]"] old.path2_nontriv[of g n] by simp_all
          from n⇩z_props p⇩n'_props(3) show "set (butlast p⇩n') ∩ set (butlast (p⇩m1 @ [n⇩z])) = {}"
           using butlast_snoc disjointI in_prefix in_set_butlastD by fastforce
        qed
        with that(1) show ?thesis by (auto intro:reachable.intros)
      qed
    qed


    txt ‹Since the reachable-set was built starting at a single $\phi$, these paths must at some
         point converge \emph{within} @{term "reachable g φ"}.›
    from assign_nodes_props(3,2) ind_props V_props(3) φ⇩r_V φ⇩r_allVars
    have "∃φ⇩z ∈ reachable g φ. ∃ns ms. old.pathsConverge g n ns m ms (defNode g φ⇩z)"
    proof (induction arbitrary: p⇩m p⇩n rule: reachable.induct)
      case refl
      txt ‹In the induction basis, we know that @{prop "φ = φ⇩s"}, and a path to @{term φ⇩r} must be obtained
          -- for this we need a second induction.›
      from refl.prems refl.hyps show ?case
      proof (induction arbitrary: p⇩m p⇩n rule: reachable.induct)
        case refl
        txt ‹The first case, in which ‹φ⇩r = φ⇩s = φ›, is trivial -- ‹φ› suffices.›
        have "old.pathsConverge g n p⇩n m p⇩m (defNode g φ)"
        proof (rule old.pathsConvergeI)
          show "1 < length p⇩n" "1 < length p⇩m"
            using refl V_props simpleDefs_phiDefs_var_disjoint unfolding unnecessaryPhi_def
            by (metis domD domIff old.path2_hd_in_αn old.path2_nontriv phi_phiDefs r_s_path_props(1) r_s_path_props(3))+
          show "g ⊢ n-p⇩n→defNode g φ" "g ⊢ m-p⇩m→defNode g φ" "set (butlast p⇩n) ∩ set (butlast p⇩m) = {}"
          using refl by auto
        qed
        with ‹φ ∈ reachable g φ› show ?case by auto
      next
        case (step φ' φ⇩r)
        txt ‹In this case we have that @{prop "φ = φ⇩s"} and need to acquire a path going to @{term φ⇩r},
            however with the aux.\ lemma we have, we still need that @{term p⇩n} and @{term p⇩m} are disjoint.›
        thus ?case
        proof (cases "set p⇩n ∩ set p⇩m = {}")
          case paths_cross: False
          with step reachable.intros
          show ?thesis using path_crossing_yields_convergence[of φ⇩r φ p⇩n p⇩m] by (metis disjointI disjoint_elem)
        next
          case True
          txt ‹If the paths are intersection-free, we can apply our path extension lemma to obtain the path needed.›
          from step(9,8,10) ‹φ ∈ allVars g› r_s_path_props(1,3) step(6,5) True step(2)
          obtain ns where "g ⊢ n -p⇩n@ns→ defNode g φ'" "set (butlast (p⇩n@ns)) ∩ set p⇩m = {}" by (rule phiArg_disjoint_paths_extend)

          from this(2) have "set (butlast p⇩m) ∩ set (butlast (p⇩n @ ns)) = {}"
            using in_set_butlastD by fastforce
          moreover
          from phiArg_same_var step.hyps(2) step.prems(5) have "var g φ' = V"
            by auto
          moreover
          have "φ' ∈ allVars g"
            by (metis φ_props(2) phiArg_in_allVars reachable.cases step.hyps(1))
          ultimately
          show "∃φ⇩z∈reachable g φ. ∃ns ms. old.pathsConverge g n ns m ms (defNode g φ⇩z)"
            using step.prems(1) φ_props V_props ‹g ⊢ n -p⇩n@ns→ defNode g φ'›
            by -(rule step.IH; blast)
        qed
      qed
    next
      case (step φ' φ⇩s)
      txt ‹With the induction basis handled, we can finally move on to the induction proper.›

      show ?thesis
      proof (cases "set p⇩m ∩ set p⇩n = {}")
        case True
        have φ⇩s_V: "var g φ⇩s = V" using step(1,2,3,9) reachable_same_var by (simp add: phiArg_same_var)
        from step(2) have φ⇩s_allVars: "φ⇩s ∈ allVars g" by (rule phiArg_in_allVars)

        obtain p⇩m' where tmp: "g ⊢ m -p⇩m@p⇩m'→ defNode g φ'" "set (butlast (p⇩m@p⇩m')) ∩ set (butlast p⇩n) = {}"
         by (rule phiArg_disjoint_paths_extend[of g φ⇩s V  φ⇩r m n p⇩m p⇩n φ'])
            (metis φ⇩s_V φ⇩s_allVars step r_s_path_props(1,3) True disjoint_iff_not_equal in_set_butlastD)+

        from step(5) this(1) step(7) this(2) step(9) step(10) step(11)
        show ?thesis by (rule step.IH[of "p⇩m@p⇩m'" p⇩n])
      next
        case paths_cross: False
        with step reachable.intros
        show ?thesis using path_crossing_yields_convergence[of φ⇩r φ⇩s p⇩n p⇩m] by blast
      qed
    qed

    then obtain φ⇩z ns ms where "φ⇩z ∈ reachable g φ" and "old.pathsConverge g n ns m ms (defNode g φ⇩z)"
      by blast
    moreover
    with reachable_props have "var g φ⇩z = V" by (metis V_props(3) phiArg_trancl_same_var rtranclpD)
    ultimately have "necessaryPhi' g φ⇩z " using r_s_path_props
      unfolding necessaryPhi_def by blast
    moreover with ‹φ⇩z ∈ reachable g φ› have "unnecessaryPhi g φ⇩z" by -(rule reachable_props)
    ultimately show False unfolding unnecessaryPhi_def by blast
  qed
qed

txt ‹Together with lemma 1, we thus have that a CFG without redundant SCCs is cytron-minimal, proving that the
     property established by Braun et al.'s algorithm suffices.›
corollary no_redundant_SCC_minimal:
assumes "¬(∃P scc. redundant_scc g P scc)"
shows "cytronMinimal g"
using assms 1 no_redundant_set_minimal by blast


txt ‹Finally, to conclude, we'll show that the above theorem is indeed a stronger assertion about a graph
     than the lack of trivial \pf s. Intuitively, this is because a set containing only a
     trivial \pf\ is a redundant set.›

corollary
assumes "¬(∃P. redundant_set g P)"
shows "¬redundant g"
proof -
  have "redundant g ⟹ ∃P. redundant_set g P"
  proof -
    assume "redundant g"
    then obtain φ where "phi g φ ≠ None" "trivial g φ"
     unfolding redundant_def redundant_set_def dom_def phiArg_def trivial_def isTrivialPhi_def
     by (clarsimp split: option.splits) fastforce
    hence "redundant_set g {φ}"
     unfolding redundant_set_def dom_def phiArg_def trivial_def isTrivialPhi_def
     by auto
    thus ?thesis by auto
  qed
  with assms show ?thesis by auto
qed


end

end