Theory Kleene_Relation_Algebras

(* Title:      Kleene Relation Algebras
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Kleene Relation Algebras›

text ‹
This theory combines Kleene algebras with Stone relation algebras.
Relation algebras with transitive closure have been studied by \<^cite>‹"Ng1984"›.
The weakening to Stone relation algebras allows us to talk about reachability in weighted graphs, for example.

Many results in this theory are used in the correctness proof of Prim's minimum spanning tree algorithm.
In particular, they are concerned with the exchange property, preservation of parts of the invariant and with establishing parts of the postcondition.
›

theory Kleene_Relation_Algebras

imports Stone_Relation_Algebras.Relation_Algebras Kleene_Algebras

begin

text ‹
We first note that bounded distributive lattices can be expanded to Kleene algebras by reusing some of the operations.
›

sublocale bounded_distrib_lattice < comp_inf: bounded_kleene_algebra where star = "λx . top" and one = top and times = inf
  apply unfold_locales
  apply (simp add: inf.assoc)
  apply simp
  apply simp
  apply (simp add: le_infI2)
  apply (simp add: inf_sup_distrib2)
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply (simp add: inf_sup_distrib1)
  apply simp
  apply simp
  by (simp add: inf_assoc)

text ‹
We add the Kleene star operation to each of bounded distributive allegories, pseudocomplemented distributive allegories and Stone relation algebras.
We start with single-object bounded distributive allegories.
›

class bounded_distrib_kleene_allegory = bounded_distrib_allegory + kleene_algebra
begin

subclass bounded_kleene_algebra ..

lemma conv_star_conv:
  "x⇧^⋆ ≤ x⇧^T⇧^⋆⇧^T"
proof -
  have "x⇧^T⇧^⋆ * x⇧^T ≤ x⇧^T⇧^⋆"
    by (simp add: star.right_plus_below_circ)
  hence 1: "x * x⇧^T⇧^⋆⇧^T ≤ x⇧^T⇧^⋆⇧^T"
    using conv_dist_comp conv_isotone by fastforce
  have "1 ≤ x⇧^T⇧^⋆⇧^T"
    by (simp add: reflexive_conv_closed star.circ_reflexive)
  hence "1 ⊔ x * x⇧^T⇧^⋆⇧^T ≤ x⇧^T⇧^⋆⇧^T"
    using 1 by simp
  thus ?thesis
    using star_left_induct by fastforce
qed

text ‹
It follows that star and converse commute.
›

lemma conv_star_commute:
  "x⇧^⋆⇧^T = x⇧^T⇧^⋆"
proof (rule order.antisym)
  show "x⇧^⋆⇧^T ≤ x⇧^T⇧^⋆"
    using conv_star_conv conv_isotone by fastforce
next
  show "x⇧^T⇧^⋆ ≤ x⇧^⋆⇧^T"
    by (metis conv_star_conv conv_involutive)
qed

lemma conv_plus_commute:
  "x⇧⁺⇧^T = x⇧^T⇧⁺"
  by (simp add: conv_dist_comp conv_star_commute star_plus)

text ‹Lemma ‹reflexive_inf_star› was contributed by Nicolas Robinson-O'Brien.›

lemma reflexive_inf_star:
  assumes "reflexive y"
    shows "y ⊓ x⇧^⋆ = 1 ⊔ (y ⊓ x⇧⁺)"
  by (simp add: assms star_left_unfold_equal sup.absorb2 sup_inf_distrib1)

text ‹
The following results are variants of a separation lemma of Kleene algebras.
›

lemma cancel_separate_2:
  assumes "x * y ≤ 1"
    shows "((w ⊓ x) ⊔ (z ⊓ y))⇧^⋆ = (z ⊓ y)⇧^⋆ * (w ⊓ x)⇧^⋆"
proof -
  have "(w ⊓ x) * (z ⊓ y) ≤ 1"
    by (meson assms comp_isotone order.trans inf.cobounded2)
  thus ?thesis
    using cancel_separate_1 sup_commute by simp
qed

lemma cancel_separate_3:
  assumes "x * y ≤ 1"
    shows "(w ⊓ x)⇧^⋆ * (z ⊓ y)⇧^⋆ = (w ⊓ x)⇧^⋆ ⊔ (z ⊓ y)⇧^⋆"
proof -
  have "(w ⊓ x) * (z ⊓ y) ≤ 1"
    by (meson assms comp_isotone order.trans inf.cobounded2)
  thus ?thesis
    by (simp add: cancel_separate_eq)
qed

lemma cancel_separate_4:
  assumes "z * y ≤ 1"
      and "w ≤ y ⊔ z"
      and "x ≤ y ⊔ z"
    shows "w⇧^⋆ * x⇧^⋆ = (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆) * (x ⊓ z)⇧^⋆"
proof -
  have "w⇧^⋆ * x⇧^⋆ = ((w ⊓ y) ⊔ (w ⊓ z))⇧^⋆ * ((x ⊓ y) ⊔ (x ⊓ z))⇧^⋆"
    by (metis assms(2,3) inf.orderE inf_sup_distrib1)
  also have "... = (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ * (x ⊓ y)⇧^⋆) * (x ⊓ z)⇧^⋆"
    by (metis assms(1) cancel_separate_2 sup_commute mult_assoc)
  finally show ?thesis
    by (simp add: assms(1) cancel_separate_3)
qed

lemma cancel_separate_5:
  assumes "w * z⇧^T ≤ 1"
    shows "w ⊓ x * (y ⊓ z) ≤ y"
proof -
  have "w ⊓ x * (y ⊓ z) ≤ (x ⊓ w * (y ⊓ z)⇧^T) * (y ⊓ z)"
    by (metis dedekind_2 inf_commute)
  also have "... ≤ w * z⇧^T * (y ⊓ z)"
    by (simp add: conv_dist_inf inf.coboundedI2 mult_left_isotone mult_right_isotone)
  also have "... ≤ y ⊓ z"
    by (metis assms mult_1_left mult_left_isotone)
  finally show ?thesis
    by simp
qed

lemma cancel_separate_6:
  assumes "z * y ≤ 1"
      and "w ≤ y ⊔ z"
      and "x ≤ y ⊔ z"
      and "v * z⇧^T ≤ 1"
      and "v ⊓ y⇧^⋆ = bot"
    shows "v ⊓ w⇧^⋆ * x⇧^⋆ ≤ x ⊔ w"
proof -
  have "v ⊓ (w ⊓ y)⇧^⋆ * (x ⊓ y)⇧^⋆ ≤ v ⊓ y⇧^⋆ * (x ⊓ y)⇧^⋆"
    using comp_inf.mult_right_isotone mult_left_isotone star_isotone by simp
  also have "... ≤ v ⊓ y⇧^⋆"
    by (simp add: inf.coboundedI2 star.circ_increasing star.circ_mult_upper_bound star_right_induct_mult)
  finally have 1: "v ⊓ (w ⊓ y)⇧^⋆ * (x ⊓ y)⇧^⋆ = bot"
    using assms(5) le_bot by simp
  have "v ⊓ w⇧^⋆ * x⇧^⋆ = v ⊓ (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆) * (x ⊓ z)⇧^⋆"
    using assms(1-3) cancel_separate_4 by simp
  also have "... = (v ⊓ (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆) * (x ⊓ z)⇧^⋆ * (x ⊓ z)) ⊔ (v ⊓ (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆))"
    by (metis inf_sup_distrib1 star.circ_back_loop_fixpoint)
  also have "... ≤ x ⊔ (v ⊓ (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆))"
    using assms(4) cancel_separate_5 semiring.add_right_mono by simp
  also have "... = x ⊔ (v ⊓ (w ⊓ y)⇧^⋆ * (w ⊓ z)⇧^⋆)"
    using 1 by (simp add: inf_sup_distrib1 mult_left_dist_sup sup_monoid.add_assoc)
  also have "... = x ⊔ (v ⊓ (w ⊓ y)⇧^⋆ * (w ⊓ z)⇧^⋆ * (w ⊓ z)) ⊔ (v ⊓ (w ⊓ y)⇧^⋆)"
    by (metis comp_inf.semiring.distrib_left star.circ_back_loop_fixpoint sup_assoc)
  also have "... ≤ x ⊔ w ⊔ (v ⊓ (w ⊓ y)⇧^⋆)"
    using assms(4) cancel_separate_5 sup_left_isotone sup_right_isotone by simp
  also have "... ≤ x ⊔ w ⊔ (v ⊓ y⇧^⋆)"
    using comp_inf.mult_right_isotone star_isotone sup_right_isotone by simp
  finally show ?thesis
    using assms(5) le_bot by simp
qed

text ‹
We show several results about the interaction of vectors and the Kleene star.
›

lemma vector_star_1:
  assumes "vector x"
    shows "x⇧^T * (x * x⇧^T)⇧^⋆ ≤ x⇧^T"
proof -
  have "x⇧^T * (x * x⇧^T)⇧^⋆ = (x⇧^T * x)⇧^⋆ * x⇧^T"
    by (simp add: star_slide)
  also have "... ≤ top * x⇧^T"
    by (simp add: mult_left_isotone)
  also have "... = x⇧^T"
    using assms vector_conv_covector by auto
  finally show ?thesis
    .
qed

lemma vector_star_2:
  "vector x ⟹ x⇧^T * (x * x⇧^T)⇧^⋆ ≤ x⇧^T * bot⇧^⋆"
  by (simp add: star_absorb vector_star_1)

lemma vector_vector_star:
  "vector v ⟹ (v * v⇧^T)⇧^⋆ = 1 ⊔ v * v⇧^T"
  by (simp add: transitive_star vv_transitive)

lemma equivalence_star_closed:
  "equivalence x ⟹ equivalence (x⇧^⋆)"
  by (simp add: conv_star_commute star.circ_reflexive star.circ_transitive_equal)

lemma equivalence_plus_closed:
  "equivalence x ⟹ equivalence (x⇧⁺)"
  by (simp add: conv_star_commute star.circ_reflexive star.circ_sup_one_left_unfold star.circ_transitive_equal)

text ‹
The following equivalence relation characterises the component trees of a forest.
This is a special case of undirected reachability in a directed graph.
›

abbreviation "forest_components f ≡ f⇧^T⇧^⋆ * f⇧^⋆"

lemma forest_components_equivalence:
  "injective x ⟹ equivalence (forest_components x)"
  apply (intro conjI)
  apply (simp add: reflexive_mult_closed star.circ_reflexive)
  apply (metis cancel_separate_1 order.eq_iff star.circ_transitive_equal)
  by (simp add: conv_dist_comp conv_star_commute)

lemma forest_components_increasing:
  "x ≤ forest_components x"
  by (metis order.trans mult_left_isotone mult_left_one star.circ_increasing star.circ_reflexive)

lemma forest_components_isotone:
  "x ≤ y ⟹ forest_components x ≤ forest_components y"
  by (simp add: comp_isotone conv_isotone star_isotone)

lemma forest_components_idempotent:
  "injective x ⟹ forest_components (forest_components x) = forest_components x"
  by (metis forest_components_equivalence cancel_separate_1 star.circ_transitive_equal star_involutive)

lemma forest_components_star:
  "injective x ⟹ (forest_components x)⇧^⋆ = forest_components x"
  using forest_components_equivalence forest_components_idempotent star.circ_transitive_equal by simp

text ‹
The following lemma shows that the nodes reachable in the graph can be reached by only using edges between reachable nodes.
›

lemma reachable_restrict:
  assumes "vector r"
    shows "r⇧^T * g⇧^⋆ = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆"
proof -
  have 1: "r⇧^T ≤ r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆"
    using mult_right_isotone mult_1_right star.circ_reflexive by fastforce
  have 2: "covector (r⇧^T * g⇧^⋆)"
    using assms covector_mult_closed vector_conv_covector by auto
  have "r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * g ≤ r⇧^T * g⇧^⋆ * g"
    by (simp add: mult_left_isotone mult_right_isotone star_isotone)
  also have "... ≤ r⇧^T * g⇧^⋆"
    by (simp add: mult_assoc mult_right_isotone star.left_plus_below_circ star_plus)
  finally have "r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * g = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * g ⊓ r⇧^T * g⇧^⋆"
    by (simp add: le_iff_inf)
  also have "... = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * (g ⊓ r⇧^T * g⇧^⋆)"
    using assms covector_comp_inf covector_mult_closed vector_conv_covector by auto
  also have "... = (r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ ⊓ r⇧^T * g⇧^⋆) * (g ⊓ r⇧^T * g⇧^⋆)"
    by (simp add: inf.absorb2 inf_commute mult_right_isotone star_isotone)
  also have "... = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * (g ⊓ r⇧^T * g⇧^⋆ ⊓ (r⇧^T * g⇧^⋆)⇧^T)"
    using 2 by (metis comp_inf_vector_1)
  also have "... = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * ((r⇧^T * g⇧^⋆)⇧^T ⊓ r⇧^T * g⇧^⋆ ⊓ g)"
    using inf_commute inf_assoc by simp
  also have "... = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)"
    using 2 by (metis covector_conv_vector inf_top.right_neutral vector_inf_comp)
  also have "... ≤ r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆"
    by (simp add: mult_assoc mult_right_isotone star.left_plus_below_circ star_plus)
  finally have "r⇧^T * g⇧^⋆ ≤ r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆"
    using 1 star_right_induct by auto
  thus ?thesis
    by (simp add: order.eq_iff mult_right_isotone star_isotone)
qed

lemma kruskal_acyclic_inv_1:
  assumes "injective f"
      and "e * forest_components f * e = bot"
    shows "(f ⊓ top * e * f⇧^T⇧^⋆)⇧^T * f⇧^⋆ * e = bot"
proof -
  let ?q = "top * e * f⇧^T⇧^⋆"
  let ?F = "forest_components f"
  have "(f ⊓ ?q)⇧^T * f⇧^⋆ * e = ?q⇧^T ⊓ f⇧^T * f⇧^⋆ * e"
    by (metis (mono_tags) comp_associative conv_dist_inf covector_conv_vector inf_vector_comp vector_top_closed)
  also have "... ≤ ?q⇧^T ⊓ ?F * e"
    using comp_inf.mult_right_isotone mult_left_isotone star.circ_increasing by simp
  also have "... = f⇧^⋆ * e⇧^T * top ⊓ ?F * e"
    by (simp add: conv_dist_comp conv_star_commute mult_assoc)
  also have "... ≤ ?F * e⇧^T * top ⊓ ?F * e"
    by (metis conv_dist_comp conv_star_commute conv_top inf.sup_left_isotone star.circ_right_top star_outer_increasing mult_assoc)
  also have "... = ?F * (e⇧^T * top ⊓ ?F * e)"
    by (metis assms(1) forest_components_equivalence equivalence_comp_dist_inf mult_assoc)
  also have "... = (?F ⊓ top * e) * ?F * e"
    by (simp add: comp_associative comp_inf_vector_1 conv_dist_comp inf_vector_comp)
  also have "... ≤ top * e * ?F * e"
    by (simp add: mult_left_isotone)
  also have "... = bot"
    using assms(2) mult_assoc by simp
  finally show ?thesis
    by (simp add: bot_unique)
qed

lemma kruskal_forest_components_inf_1:
  assumes "f ≤ w ⊔ w⇧^T"
      and "injective w"
      and "f ≤ forest_components g"
    shows "f * forest_components (forest_components g ⊓ w) ≤ forest_components (forest_components g ⊓ w)"
proof -
  let ?f = "forest_components g"
  let ?w = "forest_components (?f ⊓ w)"
  have "f * ?w = (f ⊓ (w ⊔ w⇧^T)) * ?w"
    by (simp add: assms(1) inf.absorb1)
  also have "... = (f ⊓ w) * ?w ⊔ (f ⊓ w⇧^T) * ?w"
    by (simp add: inf_sup_distrib1 semiring.distrib_right)
  also have "... ≤ (?f ⊓ w) * ?w ⊔ (f ⊓ w⇧^T) * ?w"
    using assms(3) inf.sup_left_isotone mult_left_isotone sup_left_isotone by simp
  also have "... ≤ (?f ⊓ w) * ?w ⊔ (?f ⊓ w⇧^T) * ?w"
    using assms(3) inf.sup_left_isotone mult_left_isotone sup_right_isotone by simp
  also have "... = (?f ⊓ w) * ?w ⊔ (?f ⊓ w)⇧^T * ?w"
    by (simp add: conv_dist_comp conv_dist_inf conv_star_commute)
  also have "... ≤ (?f ⊓ w) * ?w ⊔ ?w"
    by (metis star.circ_loop_fixpoint sup_ge1 sup_right_isotone)
  also have "... = ?w ⊔ (?f ⊓ w) * (?f ⊓ w)⇧^⋆ ⊔ (?f ⊓ w) * (?f ⊓ w)⇧^T⇧⁺ * (?f ⊓ w)⇧^⋆"
    by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint sup_commute sup_assoc)
  also have "... ≤ ?w ⊔ (?f ⊓ w)⇧^⋆ ⊔ (?f ⊓ w) * (?f ⊓ w)⇧^T⇧⁺ * (?f ⊓ w)⇧^⋆"
    using star.left_plus_below_circ sup_left_isotone sup_right_isotone by auto
  also have "... = ?w ⊔ (?f ⊓ w) * (?f ⊓ w)⇧^T⇧⁺ * (?f ⊓ w)⇧^⋆"
    by (metis star.circ_loop_fixpoint sup.right_idem)
  also have "... ≤ ?w ⊔ w * w⇧^T * ?w"
    using comp_associative conv_dist_inf mult_isotone sup_right_isotone by simp
  also have "... = ?w"
    by (metis assms(2) coreflexive_comp_top_inf inf.cobounded2 sup.orderE)
  finally show ?thesis
    by simp
qed

lemma kruskal_forest_components_inf:
  assumes "f ≤ w ⊔ w⇧^T"
      and "injective w"
    shows "forest_components f ≤ forest_components (forest_components f ⊓ w)"
proof -
  let ?f = "forest_components f"
  let ?w = "forest_components (?f ⊓ w)"
  have 1: "1 ≤ ?w"
    by (simp add: reflexive_mult_closed star.circ_reflexive)
  have "f * ?w ≤ ?w"
    using assms forest_components_increasing kruskal_forest_components_inf_1 by simp
  hence 2: "f⇧^⋆ ≤ ?w"
    using 1 star_left_induct by fastforce
  have "f⇧^T * ?w ≤ ?w"
    apply (rule kruskal_forest_components_inf_1)
    apply (metis assms(1) conv_dist_sup conv_involutive conv_isotone sup_commute)
    apply (simp add: assms(2))
    by (metis le_supI2 star.circ_back_loop_fixpoint star.circ_increasing)
  thus "?f ≤ ?w"
    using 2 star_left_induct by simp
qed

end

text ‹
We next add the Kleene star to single-object pseudocomplemented distributive allegories.
›

class pd_kleene_allegory = pd_allegory + bounded_distrib_kleene_allegory
begin

text ‹
The following definitions and results concern acyclic graphs and forests.
›

abbreviation acyclic :: "'a ⇒ bool" where "acyclic x ≡ x⇧⁺ ≤ -1"

abbreviation forest :: "'a ⇒ bool" where "forest x ≡ injective x ∧ acyclic x"

lemma forest_bot:
  "forest bot"
  by simp

lemma acyclic_down_closed:
  "x ≤ y ⟹ acyclic y ⟹ acyclic x"
  using comp_isotone star_isotone by fastforce

lemma forest_down_closed:
  "x ≤ y ⟹ forest y ⟹ forest x"
  using conv_isotone mult_isotone star_isotone by fastforce

lemma acyclic_star_below_complement:
  "acyclic w ⟷ w⇧^T⇧^⋆ ≤ -w"
  by (simp add: conv_star_commute schroeder_4_p)

lemma acyclic_star_below_complement_1:
  "acyclic w ⟷ w⇧^⋆ ⊓ w⇧^T = bot"
  using pseudo_complement schroeder_5_p by force

lemma acyclic_star_inf_conv:
  assumes "acyclic w"
  shows "w⇧^⋆ ⊓ w⇧^T⇧^⋆ = 1"
proof -
  have "w⇧⁺ ⊓ w⇧^T⇧^⋆ ≤ (w ⊓ w⇧^T⇧^⋆) * w⇧^⋆"
    by (metis conv_star_commute dedekind_2 star.circ_transitive_equal)
  also have "... = bot"
    by (metis assms conv_star_commute p_antitone_iff pseudo_complement schroeder_4_p semiring.mult_not_zero star.circ_circ_mult star_involutive star_one)
  finally have "w⇧^⋆ ⊓ w⇧^T⇧^⋆ ≤ 1"
    by (metis order.eq_iff le_bot mult_left_zero star.circ_plus_one star.circ_zero star_left_unfold_equal sup_inf_distrib1)
  thus ?thesis
    by (simp add: order.antisym star.circ_reflexive)
qed

lemma acyclic_asymmetric:
  "acyclic w ⟹ asymmetric w"
  by (simp add: dual_order.trans pseudo_complement schroeder_5_p star.circ_increasing)

lemma forest_separate:
  assumes "forest x"
    shows "x⇧^⋆ * x⇧^T⇧^⋆ ⊓ x⇧^T * x ≤ 1"
proof -
  have "x⇧^⋆ * 1 ≤ -x⇧^T"
    using assms schroeder_5_p by force
  hence 1: "x⇧^⋆ ⊓ x⇧^T = bot"
    by (simp add: pseudo_complement)
  have "x⇧^⋆ ⊓ x⇧^T * x = (1 ⊔ x⇧^⋆ * x) ⊓ x⇧^T * x"
    using star.circ_right_unfold_1 by simp
  also have "... = (1 ⊓ x⇧^T * x) ⊔ (x⇧^⋆ * x ⊓ x⇧^T * x)"
    by (simp add: inf_sup_distrib2)
  also have "... ≤ 1 ⊔ (x⇧^⋆ * x ⊓ x⇧^T * x)"
    using sup_left_isotone by simp
  also have "... = 1 ⊔ (x⇧^⋆ ⊓ x⇧^T) * x"
    by (simp add: assms injective_comp_right_dist_inf)
  also have "... = 1"
    using 1 by simp
  finally have 2: "x⇧^⋆ ⊓ x⇧^T * x ≤ 1"
    .
  hence 3: "x⇧^T⇧^⋆ ⊓ x⇧^T * x ≤ 1"
    by (metis (mono_tags, lifting) conv_star_commute conv_dist_comp conv_dist_inf conv_involutive coreflexive_symmetric)
  have "x⇧^⋆ * x⇧^T⇧^⋆ ⊓ x⇧^T * x ≤ (x⇧^⋆ ⊔ x⇧^T⇧^⋆) ⊓ x⇧^T * x"
    using assms cancel_separate inf.sup_left_isotone by simp
  also have "... ≤ 1"
    using 2 3 by (simp add: inf_sup_distrib2)
  finally show ?thesis
    .
qed

text ‹
The following definition captures the components of undirected weighted graphs.
›

abbreviation "components g ≡ (--g)⇧^⋆"

lemma components_equivalence:
  "symmetric x ⟹ equivalence (components x)"
  by (simp add: conv_star_commute conv_complement star.circ_reflexive star.circ_transitive_equal)

lemma components_increasing:
  "x ≤ components x"
  using order_trans pp_increasing star.circ_increasing by blast

lemma components_isotone:
  "x ≤ y ⟹ components x ≤ components y"
  by (simp add: pp_isotone star_isotone)

lemma cut_reachable:
  assumes "v⇧^T = r⇧^T * t⇧^⋆"
      and "t ≤ g"
    shows "v * -v⇧^T ⊓ g ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆)"
proof -
  have "v * -v⇧^T ⊓ g ≤ v * top ⊓ g"
    using inf.sup_left_isotone mult_right_isotone top_greatest by blast
  also have "... = (r⇧^T * t⇧^⋆)⇧^T * top ⊓ g"
    by (metis assms(1) conv_involutive)
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * top ⊓ g"
    using assms(2) conv_isotone inf.sup_left_isotone mult_left_isotone mult_right_isotone star_isotone by auto
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * ((r⇧^T * g⇧^⋆) * g)"
    by (metis conv_involutive dedekind_1 inf_top.left_neutral)
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆)"
    by (simp add: mult_assoc mult_right_isotone star.left_plus_below_circ star_plus)
  finally show ?thesis
    .
qed

text ‹
The following lemma shows that the predecessors of visited nodes in the minimum spanning tree extending the current tree have all been visited.
›

lemma predecessors_reachable:
  assumes "vector r"
      and "injective r"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "forest w"
      and "t ≤ w"
      and "w ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g"
      and "r⇧^T * g⇧^⋆ ≤ r⇧^T * w⇧^⋆"
    shows "w * v ≤ v"
proof -
  have "w * r ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) * r"
    using assms(6) mult_left_isotone by auto
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * top"
    by (simp add: mult_assoc mult_right_isotone)
  also have "... = (r⇧^T * g⇧^⋆)⇧^T"
    by (simp add: assms(1) comp_associative conv_dist_comp)
  also have "... ≤ (r⇧^T * w⇧^⋆)⇧^T"
    by (simp add: assms(7) conv_isotone)
  also have "... = w⇧^T⇧^⋆ * r"
    by (simp add: conv_dist_comp conv_star_commute)
  also have "... ≤ -w * r"
    using assms(4) by (simp add: mult_left_isotone acyclic_star_below_complement)
  also have "... ≤ -(w * r)"
    by (simp add: assms(2) comp_injective_below_complement)
  finally have 1: "w * r = bot"
    by (simp add: le_iff_inf)
  have "v = t⇧^T⇧^⋆ * r"
    by (metis assms(3) conv_dist_comp conv_involutive conv_star_commute)
  also have "... = t⇧^T * v ⊔ r"
    by (simp add: calculation star.circ_loop_fixpoint)
  also have "... ≤ w⇧^T * v ⊔ r"
    using assms(5) comp_isotone conv_isotone semiring.add_right_mono by auto
  finally have "w * v ≤ w * w⇧^T * v ⊔ w * r"
    by (simp add: comp_left_dist_sup mult_assoc mult_right_isotone)
  also have "... = w * w⇧^T * v"
    using 1 by simp
  also have "... ≤ v"
    using assms(4) by (simp add: star_left_induct_mult_iff star_sub_one)
  finally show ?thesis
    .
qed

subsection ‹Prim's Algorithm›

text ‹
The following results are used for proving the correctness of Prim's minimum spanning tree algorithm.
›

subsubsection ‹Preservation of Invariant›

text ‹
We first treat the preservation of the invariant.
The following lemma shows that the while-loop preserves that ‹v› represents the nodes of the constructed tree.
The remaining lemmas in this section show that ‹t› is a spanning tree.
The exchange property is treated in the following two sections.
›

lemma reachable_inv:
  assumes "vector v"
      and "e ≤ v * -v⇧^T"
      and "e * t = bot"
      and "v⇧^T = r⇧^T * t⇧^⋆"
    shows "(v ⊔ e⇧^T * top)⇧^T = r⇧^T * (t ⊔ e)⇧^⋆"
proof -
  have 1: "v⇧^T ≤ r⇧^T * (t ⊔ e)⇧^⋆"
    by (simp add: assms(4) mult_right_isotone star.circ_sub_dist)
  have 2: "(e⇧^T * top)⇧^T = top * e"
    by (simp add: conv_dist_comp)
  also have "... = top * (v * -v⇧^T ⊓ e)"
    by (simp add: assms(2) inf_absorb2)
  also have "... ≤ top * (v * top ⊓ e)"
    using inf.sup_left_isotone mult_right_isotone top_greatest by blast
  also have "... = top * v⇧^T * e"
    by (simp add: comp_inf_vector inf.sup_monoid.add_commute)
  also have "... = v⇧^T * e"
    using assms(1) vector_conv_covector by auto
  also have "... ≤ r⇧^T * (t ⊔ e)⇧^⋆ * e"
    using 1 by (simp add: mult_left_isotone)
  also have "... ≤ r⇧^T * (t ⊔ e)⇧^⋆ * (t ⊔ e)"
    by (simp add: mult_right_isotone)
  also have "... ≤ r⇧^T * (t ⊔ e)⇧^⋆"
    by (simp add: comp_associative mult_right_isotone star.right_plus_below_circ)
  finally have 3: "(v ⊔ e⇧^T * top)⇧^T ≤ r⇧^T * (t ⊔ e)⇧^⋆"
    using 1 by (simp add: conv_dist_sup)
  have "r⇧^T ≤ r⇧^T * t⇧^⋆"
    using sup.bounded_iff star.circ_back_loop_prefixpoint by blast
  also have "... ≤ (v ⊔ e⇧^T * top)⇧^T"
    by (metis assms(4) conv_isotone sup_ge1)
  finally have 4: "r⇧^T ≤ (v ⊔ e⇧^T * top)⇧^T"
    .
  have "(v ⊔ e⇧^T * top)⇧^T * (t ⊔ e) = (v ⊔ e⇧^T * top)⇧^T * t ⊔ (v ⊔ e⇧^T * top)⇧^T * e"
    by (simp add: mult_left_dist_sup)
  also have "... ≤ (v ⊔ e⇧^T * top)⇧^T * t ⊔ top * e"
    using comp_isotone semiring.add_left_mono by auto
  also have "... = v⇧^T * t ⊔ top * e * t ⊔ top * e"
    using 2 by (simp add: conv_dist_sup mult_right_dist_sup)
  also have "... = v⇧^T * t ⊔ top * e"
    by (simp add: assms(3) comp_associative)
  also have "... ≤ r⇧^T * t⇧^⋆ ⊔ top * e"
    by (metis assms(4) star.circ_back_loop_fixpoint sup_ge1 sup_left_isotone)
  also have "... = v⇧^T ⊔ top * e"
    by (simp add: assms(4))
  finally have 5: "(v ⊔ e⇧^T * top)⇧^T * (t ⊔ e) ≤ (v ⊔ e⇧^T * top)⇧^T"
    using 2 by (simp add: conv_dist_sup)
  have "r⇧^T * (t ⊔ e)⇧^⋆ ≤ (v ⊔ e⇧^T * top)⇧^T * (t ⊔ e)⇧^⋆"
    using 4 by (simp add: mult_left_isotone)
  also have "... ≤ (v ⊔ e⇧^T * top)⇧^T"
    using 5 by (simp add: star_right_induct_mult)
  finally show ?thesis
    using 3 by (simp add: order.eq_iff)
qed

text ‹
The next result is used to show that the while-loop preserves acyclicity of the constructed tree.
›

lemma acyclic_inv:
  assumes "acyclic t"
      and "vector v"
      and "e ≤ v * -v⇧^T"
      and "t ≤ v * v⇧^T"
    shows "acyclic (t ⊔ e)"
proof -
  have "t⇧⁺ * e ≤ t⇧⁺ * v * -v⇧^T"
    by (simp add: assms(3) comp_associative mult_right_isotone)
  also have "... ≤ v * v⇧^T * t⇧^⋆ * v * -v⇧^T"
    by (simp add: assms(4) mult_left_isotone)
  also have "... ≤ v * top * -v⇧^T"
    by (metis mult_assoc mult_left_isotone mult_right_isotone top_greatest)
  also have "... = v * -v⇧^T"
    by (simp add: assms(2))
  also have "... ≤ -1"
    by (simp add: pp_increasing schroeder_3_p)
  finally have 1: "t⇧⁺ * e ≤ -1"
    .
  have 2: "e * t⇧^⋆ = e"
    using assms(2-4) et(1) star_absorb by blast
  have "e⇧^⋆ = 1 ⊔ e ⊔ e * e * e⇧^⋆"
    by (metis star.circ_loop_fixpoint star_square_2 sup_commute)
  also have "... = 1 ⊔ e"
    using assms(2,3) ee comp_left_zero bot_least sup_absorb1 by simp
  finally have 3: "e⇧^⋆ = 1 ⊔ e"
    .
  have "e ≤ v * -v⇧^T"
    by (simp add: assms(3))
  also have "... ≤ -1"
    by (simp add: pp_increasing schroeder_3_p)
  finally have 4: "t⇧⁺ * e ⊔ e ≤ -1"
    using 1 by simp
  have "(t ⊔ e)⇧⁺ = (t ⊔ e) * t⇧^⋆ * (e * t⇧^⋆)⇧^⋆"
    using star_sup_1 mult_assoc by simp
  also have "... = (t ⊔ e) * t⇧^⋆ * (1 ⊔ e)"
    using 2 3 by simp
  also have "... = t⇧⁺ * (1 ⊔ e) ⊔ e * t⇧^⋆ * (1 ⊔ e)"
    by (simp add: comp_right_dist_sup)
  also have "... = t⇧⁺ * (1 ⊔ e) ⊔ e * (1 ⊔ e)"
    using 2 by simp
  also have "... = t⇧⁺ * (1 ⊔ e) ⊔ e"
    using 3 by (metis star_absorb assms(2,3) ee)
  also have "... = t⇧⁺ ⊔ t⇧⁺ * e ⊔ e"
    by (simp add: mult_left_dist_sup)
  also have "... ≤ -1"
    using 4 by (metis assms(1) sup.absorb1 sup.orderI sup_assoc)
  finally show ?thesis
    .
qed

text ‹
The following lemma shows that the extended tree is in the component reachable from the root.
›

lemma mst_subgraph_inv_2:
  assumes "regular (v * v⇧^T)"
      and "t ≤ v * v⇧^T ⊓ --g"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "e ≤ v * -v⇧^T ⊓ --g"
      and "vector v"
      and "regular ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T)"
    shows "t ⊔ e ≤ (r⇧^T * (--((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g))⇧^⋆)⇧^T * (r⇧^T * (--((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g))⇧^⋆)"
proof -
  let ?v = "v ⊔ e⇧^T * top"
  let ?G = "?v * ?v⇧^T ⊓ g"
  let ?c = "r⇧^T * (--?G)⇧^⋆"
  have "v⇧^T ≤ r⇧^T * (--(v * v⇧^T ⊓ g))⇧^⋆"
    using assms(1-3) inf_pp_commute mult_right_isotone star_isotone by auto
  also have "... ≤ ?c"
    using comp_inf.mult_right_isotone comp_isotone conv_isotone inf.commute mult_right_isotone pp_isotone star_isotone sup.cobounded1 by presburger
  finally have 2: "v⇧^T ≤ ?c ∧ v ≤ ?c⇧^T"
    by (metis conv_isotone conv_involutive)
  have "t ≤ v * v⇧^T"
    using assms(2) by auto
  hence 3: "t ≤ ?c⇧^T * ?c"
    using 2 order_trans mult_isotone by blast
  have "e ≤ v * top ⊓ --g"
    by (metis assms(4,5) inf.bounded_iff inf.sup_left_divisibility mult_right_isotone top.extremum)
  hence "e ≤ v * top ⊓ top * e ⊓ --g"
    by (simp add: top_left_mult_increasing inf.boundedI)
  hence "e ≤ v * top * e ⊓ --g"
    by (metis comp_inf_covector inf.absorb2 mult_assoc top.extremum)
  hence "t ⊔ e ≤ (v * v⇧^T ⊓ --g) ⊔ (v * top * e ⊓ --g)"
    using assms(2) sup_mono by blast
  also have "... = v * ?v⇧^T ⊓ --g"
    by (simp add: inf_sup_distrib2 mult_assoc mult_left_dist_sup conv_dist_comp conv_dist_sup)
  also have "... ≤ --?G"
    using assms(6) comp_left_increasing_sup inf.sup_left_isotone pp_dist_inf by auto
  finally have 4: "t ⊔ e ≤ --?G"
    .
  have "e ≤ e * e⇧^T * e"
    by (simp add: ex231c)
  also have "... ≤ v * -v⇧^T * -v * v⇧^T * e"
    by (metis assms(4) mult_left_isotone conv_isotone conv_dist_comp mult_assoc mult_isotone conv_involutive conv_complement inf.boundedE)
  also have "... ≤ v * top * v⇧^T * e"
    by (metis mult_assoc mult_left_isotone mult_right_isotone top.extremum)
  also have "... = v * r⇧^T * t⇧^⋆ * e"
    using assms(3,5) by (simp add: mult_assoc)
  also have "... ≤ v * r⇧^T * (t ⊔ e)⇧^⋆"
    by (simp add: comp_associative mult_right_isotone star.circ_mult_upper_bound star.circ_sub_dist_1 star_isotone sup_commute)
  also have "... ≤ v * ?c"
    using 4 by (simp add: mult_assoc mult_right_isotone star_isotone)
  also have "... ≤ ?c⇧^T * ?c"
    using 2 by (simp add: mult_left_isotone)
  finally show ?thesis
    using 3 by simp
qed

lemma span_inv:
  assumes "e ≤ v * -v⇧^T"
      and "vector v"
      and "arc e"
      and "t ≤ (v * v⇧^T) ⊓ g"
      and "g⇧^T = g"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "injective r"
      and "r⇧^T ≤ v⇧^T"
      and "r⇧^T * ((v * v⇧^T) ⊓ g)⇧^⋆ ≤ r⇧^T * t⇧^⋆"
    shows "r⇧^T * (((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T) ⊓ g)⇧^⋆ ≤ r⇧^T * (t ⊔ e)⇧^⋆"
proof -
  let ?d = "(v * v⇧^T) ⊓ g"
  have 1: "(v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T = v * v⇧^T ⊔ v * v⇧^T * e ⊔ e⇧^T * v * v⇧^T ⊔ e⇧^T * e"
    using assms(1-3) ve_dist by simp
  have "t⇧^T ≤ ?d⇧^T"
    using assms(4) conv_isotone by simp
  also have "... = (v * v⇧^T) ⊓ g⇧^T"
    by (simp add: conv_dist_comp conv_dist_inf)
  also have "... = ?d"
    by (simp add: assms(5))
  finally have 2: "t⇧^T ≤ ?d"
    .
  have "v * v⇧^T = (r⇧^T * t⇧^⋆)⇧^T * (r⇧^T * t⇧^⋆)"
    by (metis assms(6) conv_involutive)
  also have "... = t⇧^T⇧^⋆ * (r * r⇧^T) * t⇧^⋆"
    by (simp add: comp_associative conv_dist_comp conv_star_commute)
  also have "... ≤ t⇧^T⇧^⋆ * 1 * t⇧^⋆"
    by (simp add: assms(7) mult_left_isotone star_right_induct_mult_iff star_sub_one)
  also have "... = t⇧^T⇧^⋆ * t⇧^⋆"
    by simp
  also have "... ≤ ?d⇧^⋆ * t⇧^⋆"
    using 2 by (simp add: comp_left_isotone star.circ_isotone)
  also have "... ≤ ?d⇧^⋆ * ?d⇧^⋆"
    using assms(4) mult_right_isotone star_isotone by simp
  also have 3: "... = ?d⇧^⋆"
    by (simp add: star.circ_transitive_equal)
  finally have 4: "v * v⇧^T ≤ ?d⇧^⋆"
    .
  have 5: "r⇧^T * ?d⇧^⋆ * (v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆"
    by (simp add: comp_associative mult_right_isotone star.circ_plus_same star.left_plus_below_circ)
  have "r⇧^T * ?d⇧^⋆ * (v * v⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * v * v⇧^T * e"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * ?d⇧^⋆ * e"
    using 3 4 by (metis comp_associative comp_isotone eq_refl)
  finally have 6: "r⇧^T * ?d⇧^⋆ * (v * v⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e"
    .
  have 7: "∀x . r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * x = bot"
  proof
    fix x
    have "r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * x ≤ r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * top"
      by (simp add: mult_right_isotone)
    also have "... = r⇧^T * e⇧^T * top ⊔ r⇧^T * v * v⇧^T * e⇧^T * top"
      by (simp add: comp_associative mult_left_dist_sup mult_right_dist_sup)
    also have "... = r⇧^T * e⇧^T * top"
      by (metis assms(1,2) mult_assoc mult_right_dist_sup mult_right_zero sup_bot_right vTeT)
    also have "... ≤ v⇧^T * e⇧^T * top"
      by (simp add: assms(8) comp_isotone)
    also have "... = bot"
      using vTeT assms(1,2) by simp
    finally show "r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * x = bot"
      by (simp add: le_bot)
  qed
  have "r⇧^T * ?d⇧^⋆ * (e⇧^T * v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e⇧^T * v * v⇧^T"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * v * v⇧^T"
    by (metis assms(2) star.circ_isotone vector_vector_star inf_le1 comp_associative comp_right_isotone comp_left_isotone)
  also have "... = bot"
    using 7 by simp
  finally have 8: "r⇧^T * ?d⇧^⋆ * (e⇧^T * v * v⇧^T ⊓ g) = bot"
    by (simp add: le_bot)
  have "r⇧^T * ?d⇧^⋆ * (e⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e⇧^T * e"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * e"
    by (metis assms(2) star.circ_isotone vector_vector_star inf_le1 comp_associative comp_right_isotone comp_left_isotone)
  also have "... = bot"
    using 7 by simp
  finally have 9: "r⇧^T * ?d⇧^⋆ * (e⇧^T * e ⊓ g) = bot"
    by (simp add: le_bot)
  have "r⇧^T * ?d⇧^⋆ * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) = r⇧^T * ?d⇧^⋆ * ((v * v⇧^T ⊔ v * v⇧^T * e ⊔ e⇧^T * v * v⇧^T ⊔ e⇧^T * e) ⊓ g)"
    using 1 by simp
  also have "... = r⇧^T * ?d⇧^⋆ * ((v * v⇧^T ⊓ g) ⊔ (v * v⇧^T * e ⊓ g) ⊔ (e⇧^T * v * v⇧^T ⊓ g) ⊔ (e⇧^T * e ⊓ g))"
    by (simp add: inf_sup_distrib2)
  also have "... = r⇧^T * ?d⇧^⋆ * (v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * (v * v⇧^T * e ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * (e⇧^T * v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * (e⇧^T * e ⊓ g)"
    by (simp add: comp_left_dist_sup)
  also have "... = r⇧^T * ?d⇧^⋆ * (v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * (v * v⇧^T * e ⊓ g)"
    using 8 9 by simp
  also have "... ≤ r⇧^T * ?d⇧^⋆ ⊔ r⇧^T * ?d⇧^⋆ * e"
    using 5 6 sup.mono by simp
  also have "... = r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by (simp add: mult_left_dist_sup)
  finally have 10: "r⇧^T * ?d⇧^⋆ * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by simp
  have "r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e * v * v⇧^T"
    by (simp add: comp_associative comp_right_isotone)
  also have "... = bot"
    by (metis assms(1,2) comp_associative comp_right_zero ev comp_left_zero)
  finally have 11: "r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T ⊓ g) = bot"
    by (simp add: le_bot)
  have "r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e * v * v⇧^T * e"
    by (simp add: comp_associative comp_right_isotone)
  also have "... = bot"
    by (metis assms(1,2) comp_associative comp_right_zero ev comp_left_zero)
  finally have 12: "r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T * e ⊓ g) = bot"
    by (simp add: le_bot)
  have "r⇧^T * ?d⇧^⋆ * e * (e⇧^T * v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e * e⇧^T * v * v⇧^T"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * ?d⇧^⋆ * 1 * v * v⇧^T"
    by (metis assms(3) arc_injective comp_associative comp_left_isotone comp_right_isotone)
  also have "... = r⇧^T * ?d⇧^⋆ * v * v⇧^T"
    by simp
  also have "... ≤ r⇧^T * ?d⇧^⋆ * ?d⇧^⋆"
    using 4 by (simp add: mult_right_isotone mult_assoc)
  also have "... = r⇧^T * ?d⇧^⋆"
    by (simp add: star.circ_transitive_equal comp_associative)
  finally have 13: "r⇧^T * ?d⇧^⋆ * e * (e⇧^T * v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆"
    .
  have "r⇧^T * ?d⇧^⋆ * e * (e⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e * e⇧^T * e"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * ?d⇧^⋆ * 1 * e"
    by (metis assms(3) arc_injective comp_associative comp_left_isotone comp_right_isotone)
  also have "... = r⇧^T * ?d⇧^⋆ * e"
    by simp
  finally have 14: "r⇧^T * ?d⇧^⋆ * e * (e⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e"
    .
  have "r⇧^T * ?d⇧^⋆ * e * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) = r⇧^T * ?d⇧^⋆ * e * ((v * v⇧^T ⊔ v * v⇧^T * e ⊔ e⇧^T * v * v⇧^T ⊔ e⇧^T * e) ⊓ g)"
    using 1 by simp
  also have "... = r⇧^T * ?d⇧^⋆ * e * ((v * v⇧^T ⊓ g) ⊔ (v * v⇧^T * e ⊓ g) ⊔ (e⇧^T * v * v⇧^T ⊓ g) ⊔ (e⇧^T * e ⊓ g))"
    by (simp add: inf_sup_distrib2)
  also have "... = r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T * e ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * (e⇧^T * v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * (e⇧^T * e ⊓ g)"
    by (simp add: comp_left_dist_sup)
  also have "... = r⇧^T * ?d⇧^⋆ * e * (e⇧^T * v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * (e⇧^T * e ⊓ g)"
    using 11 12 by simp
  also have "... ≤ r⇧^T * ?d⇧^⋆ ⊔ r⇧^T * ?d⇧^⋆ * e"
    using 13 14 sup_mono by simp
  also have "... = r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by (simp add: mult_left_dist_sup)
  finally have 15: "r⇧^T * ?d⇧^⋆ * e * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by simp
  have "r⇧^T ≤ r⇧^T * ?d⇧^⋆"
    using mult_right_isotone star.circ_reflexive by fastforce
  also have "... ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by (simp add: semiring.distrib_left)
  finally have 16: "r⇧^T ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    .
  have "r⇧^T * ?d⇧^⋆ * (1 ⊔ e) * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) = r⇧^T * ?d⇧^⋆ * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g)"
    by (simp add: semiring.distrib_left semiring.distrib_right)
  also have "... ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    using 10 15 le_supI by simp
  finally have "r⇧^T * ?d⇧^⋆ * (1 ⊔ e) * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    .
  hence "r⇧^T ⊔ r⇧^T * ?d⇧^⋆ * (1 ⊔ e) * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    using 16 sup_least by simp
  hence "r⇧^T * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g)⇧^⋆ ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by (simp add: star_right_induct)
  also have "... ≤ r⇧^T * t⇧^⋆ * (1 ⊔ e)"
    by (simp add: assms(9) mult_left_isotone)
  also have "... ≤ r⇧^T * (t ⊔ e)⇧^⋆"
    by (simp add: star_one_sup_below)
  finally show ?thesis
    .
qed

subsubsection ‹Exchange gives Spanning Trees›

text ‹
The following abbreviations are used in the spanning tree application using Prim's algorithm to construct the new tree for the exchange property.
It is obtained by replacing an edge with one that has minimal weight and reversing the path connecting these edges.
Here, w represents a weighted graph, v represents a set of nodes and e represents an edge.
›

abbreviation prim_E :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where "prim_E w v e ≡ w ⊓ --v * -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
abbreviation prim_P :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where "prim_P w v e ≡ w ⊓ -v * -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
abbreviation prim_EP :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where "prim_EP w v e ≡ w ⊓ -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
abbreviation prim_W :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where "prim_W w v e ≡ (w ⊓ -(prim_EP w v e)) ⊔ (prim_P w v e)⇧^T ⊔ e"

text ‹
The lemmas in this section are used to show that the relation after exchange represents a spanning tree.
The results in the next section are used to show that it is a minimum spanning tree.
›

lemma exchange_injective_3:
  assumes "e ≤ v * -v⇧^T"
      and "vector v"
    shows "(w ⊓ -(prim_EP w v e)) * e⇧^T = bot"
proof -
  have 1: "top * e ≤ -v⇧^T"
    by (simp add: assms schroeder_4_p vTeT)
  have "top * e ≤ top * e * w⇧^T⇧^⋆"
    using sup_right_divisibility star.circ_back_loop_fixpoint by blast
  hence "top * e ≤ -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
    using 1 by simp
  hence "top * e ≤ -(w ⊓ -prim_EP w v e)"
    by (metis inf.assoc inf_import_p le_infI2 p_antitone p_antitone_iff)
  hence "(w ⊓ -(prim_EP w v e)) * e⇧^T ≤ bot"
    using p_top schroeder_4_p by blast
  thus ?thesis
    using le_bot by simp
qed

lemma exchange_injective_6:
  assumes "arc e"
      and "forest w"
    shows "(prim_P w v e)⇧^T * e⇧^T = bot"
proof -
  have "e⇧^T * top * e ≤ --1"
    by (simp add: assms(1) p_antitone p_antitone_iff point_injective)
  hence 1: "e * -1 * e⇧^T ≤ bot"
    by (metis conv_involutive p_top triple_schroeder_p)
  have "(prim_P w v e)⇧^T * e⇧^T ≤ (w ⊓ top * e * w⇧^T⇧^⋆)⇧^T * e⇧^T"
    using comp_inf.mult_left_isotone conv_dist_inf mult_left_isotone by simp
  also have "... = (w⇧^T ⊓ w⇧^T⇧^⋆⇧^T * e⇧^T * top) * e⇧^T"
    by (simp add: comp_associative conv_dist_comp conv_dist_inf)
  also have "... = w⇧^⋆ * e⇧^T * top ⊓ w⇧^T * e⇧^T"
    by (simp add: conv_star_commute inf_vector_comp)
  also have "... ≤ (w⇧^T ⊓ w⇧^⋆ * e⇧^T * top * e) * (e⇧^T ⊓ w⇧⁺ * e⇧^T * top)"
    by (metis dedekind mult_assoc conv_involutive inf_commute)
  also have "... ≤ (w⇧^⋆ * e⇧^T * top * e) * (w⇧⁺ * e⇧^T * top)"
    by (simp add: mult_isotone)
  also have "... ≤ (top * e) * (w⇧⁺ * e⇧^T * top)"
    by (simp add: mult_left_isotone)
  also have "... = top * e * w⇧⁺ * e⇧^T * top"
    using mult_assoc by simp
  also have "... ≤ top * e * -1 * e⇧^T * top"
    using assms(2) mult_left_isotone mult_right_isotone by simp
  also have "... ≤ bot"
    using 1 by (metis le_bot semiring.mult_not_zero mult_assoc)
  finally show ?thesis
    using le_bot by simp
qed

text ‹
The graph after exchanging is injective.
›

lemma exchange_injective:
  assumes "arc e"
      and "e ≤ v * -v⇧^T"
      and "forest w"
      and "vector v"
    shows "injective (prim_W w v e)"
proof -
  have 1: "(w ⊓ -(prim_EP w v e)) * (w ⊓ -(prim_EP w v e))⇧^T ≤ 1"
  proof -
    have "(w ⊓ -(prim_EP w v e)) * (w ⊓ -(prim_EP w v e))⇧^T ≤ w * w⇧^T"
      by (simp add: comp_isotone conv_isotone)
    also have "... ≤ 1"
      by (simp add: assms(3))
    finally show ?thesis
      .
  qed
  have 2: "(w ⊓ -(prim_EP w v e)) * (prim_P w v e)⇧^T⇧^T ≤ 1"
  proof -
    have "top * (prim_P w v e)⇧^T = top * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^T⇧^⋆⇧^T * e⇧^T * top)"
      by (simp add: comp_associative conv_complement conv_dist_comp conv_dist_inf)
    also have "... = top * e * w⇧^T⇧^⋆ * (w⇧^T ⊓ -v * -v⇧^T)"
      by (metis comp_inf_vector conv_dist_comp conv_involutive inf_top_left mult_assoc)
    also have "... ≤ top * e * w⇧^T⇧^⋆ * (w⇧^T ⊓ top * -v⇧^T)"
      using comp_inf.mult_right_isotone mult_left_isotone mult_right_isotone by simp
    also have "... = top * e * w⇧^T⇧^⋆ * w⇧^T ⊓ -v⇧^T"
      by (metis assms(4) comp_inf_covector vector_conv_compl)
    also have "... ≤ -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
      by (simp add: comp_associative comp_isotone inf.coboundedI1 star.circ_plus_same star.left_plus_below_circ)
    finally have "top * (prim_P w v e)⇧^T ≤ -(w ⊓ -prim_EP w v e)"
      by (metis inf.assoc inf_import_p le_infI2 p_antitone p_antitone_iff)
    hence "(w ⊓ -(prim_EP w v e)) * (prim_P w v e)⇧^T⇧^T ≤ bot"
      using p_top schroeder_4_p by blast
    thus ?thesis
      by (simp add: bot_unique)
  qed
  have 3: "(w ⊓ -(prim_EP w v e)) * e⇧^T ≤ 1"
    by (metis assms(2,4) exchange_injective_3 bot_least)
  have 4: "(prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧^T ≤ 1"
    using 2 conv_dist_comp coreflexive_symmetric by fastforce
  have 5: "(prim_P w v e)⇧^T * (prim_P w v e)⇧^T⇧^T ≤ 1"
  proof -
    have "(prim_P w v e)⇧^T * (prim_P w v e)⇧^T⇧^T ≤ (top * e * w⇧^T⇧^⋆)⇧^T * (top * e * w⇧^T⇧^⋆)"
      by (simp add: conv_dist_inf mult_isotone)
    also have "... = w⇧^⋆ * e⇧^T * top * top * e * w⇧^T⇧^⋆"
      using conv_star_commute conv_dist_comp conv_involutive conv_top mult_assoc by presburger
    also have "... = w⇧^⋆ * e⇧^T * top * e * w⇧^T⇧^⋆"
      by (simp add: comp_associative)
    also have "... ≤ w⇧^⋆ * 1 * w⇧^T⇧^⋆"
      by (metis comp_left_isotone comp_right_isotone mult_assoc assms(1) point_injective)
    finally have "(prim_P w v e)⇧^T * (prim_P w v e)⇧^T⇧^T ≤ w⇧^⋆ * w⇧^T⇧^⋆ ⊓ w⇧^T * w"
      by (simp add: conv_isotone inf.left_commute inf.sup_monoid.add_commute mult_isotone)
    also have "... ≤ 1"
      by (simp add: assms(3) forest_separate)
    finally show ?thesis
      .
  qed
  have 6: "(prim_P w v e)⇧^T * e⇧^T ≤ 1"
    using assms exchange_injective_6 bot_least by simp
  have 7: "e * (w ⊓ -(prim_EP w v e))⇧^T ≤ 1"
    using 3 by (metis conv_dist_comp conv_involutive coreflexive_symmetric)
  have 8: "e * (prim_P w v e)⇧^T⇧^T ≤ 1"
    using 6 conv_dist_comp coreflexive_symmetric by fastforce
  have 9: "e * e⇧^T ≤ 1"
    by (simp add: assms(1) arc_injective)
  have "(prim_W w v e) * (prim_W w v e)⇧^T = (w ⊓ -(prim_EP w v e)) * (w ⊓ -(prim_EP w v e))⇧^T ⊔ (w ⊓ -(prim_EP w v e)) * (prim_P w v e)⇧^T⇧^T ⊔ (w ⊓ -(prim_EP w v e)) * e⇧^T ⊔ (prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧^T ⊔ (prim_P w v e)⇧^T * (prim_P w v e)⇧^T⇧^T ⊔ (prim_P w v e)⇧^T * e⇧^T  ⊔ e * (w ⊓ -(prim_EP w v e))⇧^T ⊔ e * (prim_P w v e)⇧^T⇧^T ⊔ e * e⇧^T"
    using comp_left_dist_sup comp_right_dist_sup conv_dist_sup sup.assoc by simp
  also have "... ≤ 1"
    using 1 2 3 4 5 6 7 8 9 by simp
  finally show ?thesis
    .
qed

lemma pv:
  assumes "vector v"
    shows "(prim_P w v e)⇧^T * v = bot"
proof -
  have "(prim_P w v e)⇧^T * v ≤ (-v * -v⇧^T)⇧^T * v"
    by (meson conv_isotone inf_le1 inf_le2 mult_left_isotone order_trans)
  also have "... = -v * -v⇧^T * v"
    by (simp add: conv_complement conv_dist_comp)
  also have "... = bot"
    by (simp add: assms covector_vector_comp mult_assoc)
  finally show ?thesis
    by (simp add: order.antisym)
qed

lemma vector_pred_inv:
  assumes "arc e"
      and "e ≤ v * -v⇧^T"
      and "forest w"
      and "vector v"
      and "w * v ≤ v"
    shows "(prim_W w v e) * (v ⊔ e⇧^T * top) ≤ v ⊔ e⇧^T * top"
proof -
  have "(prim_W w v e) * e⇧^T * top = (w ⊓ -(prim_EP w v e)) * e⇧^T * top ⊔ (prim_P w v e)⇧^T * e⇧^T * top ⊔ e * e⇧^T * top"
    by (simp add: mult_right_dist_sup)
  also have "... = e * e⇧^T * top"
   using assms exchange_injective_3 exchange_injective_6 comp_left_zero by simp
  also have "... ≤ v * -v⇧^T * e⇧^T * top"
    by (simp add: assms(2) comp_isotone)
  also have "... ≤ v * top"
    by (simp add: comp_associative mult_right_isotone)
  also have "... = v"
    by (simp add: assms(4))
  finally have 1: "(prim_W w v e) * e⇧^T * top ≤ v"
    .
  have "(prim_W w v e) * v = (w ⊓ -(prim_EP w v e)) * v ⊔ (prim_P w v e)⇧^T * v ⊔ e * v"
    by (simp add: mult_right_dist_sup)
  also have "... = (w ⊓ -(prim_EP w v e)) * v"
    by (metis assms(2,4) pv ev sup_bot_right)
  also have "... ≤ w * v"
    by (simp add: mult_left_isotone)
  finally have 2: "(prim_W w v e) * v ≤ v"
    using assms(5) order_trans by blast
  have "(prim_W w v e) * (v ⊔ e⇧^T * top) = (prim_W w v e) * v ⊔ (prim_W w v e) * e⇧^T * top"
    by (simp add: semiring.distrib_left mult_assoc)
  also have "... ≤ v"
    using 1 2 by simp
  also have "... ≤ v ⊔ e⇧^T * top"
    by simp
  finally show ?thesis
    .
qed

text ‹
The graph after exchanging is acyclic.
›

lemma exchange_acyclic:
  assumes "vector v"
      and "e ≤ v * -v⇧^T"
      and "w * v ≤ v"
      and "acyclic w"
    shows "acyclic (prim_W w v e)"
proof -
  have 1: "(prim_P w v e)⇧^T * e = bot"
  proof -
    have "(prim_P w v e)⇧^T * e ≤ (-v * -v⇧^T)⇧^T * e"
      by (meson conv_order dual_order.trans inf.cobounded1 inf.cobounded2 mult_left_isotone)
    also have "... = -v * -v⇧^T * e"
      by (simp add: conv_complement conv_dist_comp)
    also have "... ≤ -v * -v⇧^T * v * -v⇧^T"
      by (simp add: assms(2) comp_associative mult_right_isotone)
    also have "... = bot"
      by (simp add: assms(1) covector_vector_comp mult_assoc)
    finally show ?thesis
      by (simp add: bot_unique)
  qed
  have 2: "e * e = bot"
    using assms(1,2) ee by auto
  have 3: "(w ⊓ -(prim_EP w v e)) * (prim_P w v e)⇧^T = bot"
  proof -
    have "top * (prim_P w v e) ≤ top * (-v * -v⇧^T ⊓ top * e * w⇧^T⇧^⋆)"
      using comp_inf.mult_semi_associative mult_right_isotone by auto
    also have "... ≤ top * -v * -v⇧^T ⊓ top * top * e * w⇧^T⇧^⋆"
      by (simp add: comp_inf_covector mult_assoc)
    also have "... ≤ top * -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
      using mult_left_isotone top.extremum inf_mono by presburger
    also have "... = -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
      by (simp add: assms(1) vector_conv_compl)
    finally have "top * (prim_P w v e) ≤ -(w ⊓ -prim_EP w v e)"
      by (metis inf.assoc inf_import_p le_infI2 p_antitone p_antitone_iff)
    hence "(w ⊓ -(prim_EP w v e)) * (prim_P w v e)⇧^T ≤ bot"
      using p_top schroeder_4_p by blast
    thus ?thesis
      using bot_unique by blast
  qed
  hence 4: "(w ⊓ -(prim_EP w v e)) * (prim_P w v e)⇧^T⇧^⋆ = w ⊓ -(prim_EP w v e)"
    using star_absorb by blast
  hence 5: "(w ⊓ -(prim_EP w v e))⇧⁺ * (prim_P w v e)⇧^T⇧^⋆ = (w ⊓ -(prim_EP w v e))⇧⁺"
    by (metis star_plus mult_assoc)
  hence 6: "(w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ = (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧^⋆"
    by (metis star.circ_loop_fixpoint mult_assoc)
  have 7: "(w ⊓ -(prim_EP w v e))⇧⁺ * e ≤ v * top"
  proof -
    have "e ≤ v * top"
      using assms(2) dual_order.trans mult_right_isotone top_greatest by blast
    hence 8: "e ⊔ w * v * top ≤ v * top"
      by (simp add: assms(1,3) comp_associative)
    have "(w ⊓ -(prim_EP w v e))⇧⁺ * e ≤ w⇧⁺ * e"
      by (simp add: comp_isotone star_isotone)
    also have "... ≤ w⇧^⋆ * e"
      by (simp add: mult_left_isotone star.left_plus_below_circ)
    also have "... ≤ v * top"
      using 8 by (simp add: comp_associative star_left_induct)
    finally show ?thesis
      .
  qed
  have 9: "(prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧⁺ * e = bot"
  proof -
    have "(prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧⁺ * e ≤ (prim_P w v e)⇧^T * v * top"
      using 7 by (simp add: mult_assoc mult_right_isotone)
    also have "... = bot"
      by (simp add: assms(1) pv)
    finally show ?thesis
      using bot_unique by blast
  qed
  have 10: "e * (w ⊓ -(prim_EP w v e))⇧⁺ * e = bot"
  proof -
    have "e * (w ⊓ -(prim_EP w v e))⇧⁺ * e ≤ e * v * top"
      using 7 by (simp add: mult_assoc mult_right_isotone)
    also have "... ≤ v * -v⇧^T * v * top"
      by (simp add: assms(2) mult_left_isotone)
    also have "... = bot"
      by (simp add: assms(1) covector_vector_comp mult_assoc)
    finally show ?thesis
      using bot_unique by blast
  qed
  have 11: "e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ v * -v⇧^T"
  proof -
    have 12: "-v⇧^T * w ≤ -v⇧^T"
      by (metis assms(3) conv_complement order_lesseq_imp pp_increasing schroeder_6_p)
    have "v * -v⇧^T * (w ⊓ -(prim_EP w v e)) ≤ v * -v⇧^T * w"
      by (simp add: comp_isotone star_isotone)
    also have "... ≤ v * -v⇧^T"
      using 12 by (simp add: comp_isotone comp_associative)
    finally have 13: "v * -v⇧^T * (w ⊓ -(prim_EP w v e)) ≤ v * -v⇧^T"
      .
    have 14: "(prim_P w v e)⇧^T ≤ -v * -v⇧^T"
      by (metis conv_complement conv_dist_comp conv_involutive conv_order inf_le1 inf_le2 order_trans)
    have "e * (prim_P w v e)⇧^T⇧^⋆ ≤ v * -v⇧^T * (prim_P w v e)⇧^T⇧^⋆"
      by (simp add: assms(2) mult_left_isotone)
    also have "... = v * -v⇧^T ⊔ v * -v⇧^T * (prim_P w v e)⇧^T⇧⁺"
      by (metis mult_assoc star.circ_back_loop_fixpoint star_plus sup_commute)
    also have "... = v * -v⇧^T ⊔ v * -v⇧^T * (prim_P w v e)⇧^T⇧^⋆ * (prim_P w v e)⇧^T"
      by (simp add: mult_assoc star_plus)
    also have "... ≤ v * -v⇧^T ⊔ v * -v⇧^T * (prim_P w v e)⇧^T⇧^⋆ * -v * -v⇧^T"
      using 14 mult_assoc mult_right_isotone sup_right_isotone by simp
    also have "... ≤ v * -v⇧^T ⊔ v * top * -v⇧^T"
      by (metis top_greatest mult_right_isotone mult_left_isotone mult_assoc sup_right_isotone)
    also have "... = v * -v⇧^T"
      by (simp add: assms(1))
    finally have "e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ v * -v⇧^T * (w ⊓ -(prim_EP w v e))⇧^⋆"
      by (simp add: mult_left_isotone)
    also have "... ≤ v * -v⇧^T"
      using 13 by (simp add: star_right_induct_mult)
    finally show ?thesis
      .
  qed
  have 15: "(w ⊓ -(prim_EP w v e))⇧⁺ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ -1"
  proof -
    have "(w ⊓ -(prim_EP w v e))⇧⁺ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ = (w ⊓ -(prim_EP w v e))⇧⁺ * (w ⊓ -(prim_EP w v e))⇧^⋆"
      using 5 by simp
    also have "... = (w ⊓ -(prim_EP w v e))⇧⁺"
      by (simp add: mult_assoc star.circ_transitive_equal)
    also have "... ≤ w⇧⁺"
      by (simp add: comp_isotone star_isotone)
    finally show ?thesis
      using assms(4) by simp
  qed
  have 16: "(prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ -1"
  proof -
    have "(w ⊓ -(prim_EP w v e))⇧⁺ * (prim_P w v e)⇧^T⇧⁺ ≤ (w ⊓ -(prim_EP w v e))⇧⁺ * (prim_P w v e)⇧^T⇧^⋆"
      by (simp add: mult_right_isotone star.left_plus_below_circ)
    also have "... = (w ⊓ -(prim_EP w v e))⇧⁺"
      using 5 by simp
    also have "... ≤ w⇧⁺"
      by (simp add: comp_isotone star_isotone)
    finally have "(w ⊓ -(prim_EP w v e))⇧⁺ * (prim_P w v e)⇧^T⇧⁺ ≤ -1"
      using assms(4) by simp
    hence 17: "(prim_P w v e)⇧^T⇧⁺ * (w ⊓ -(prim_EP w v e))⇧⁺ ≤ -1"
      by (simp add: comp_commute_below_diversity)
    have "(prim_P w v e)⇧^T⇧⁺ ≤ w⇧^T⇧⁺"
      by (simp add: comp_isotone conv_dist_inf inf.left_commute inf.sup_monoid.add_commute star_isotone)
    also have "... = w⇧⁺⇧^T"
      by (simp add: conv_dist_comp conv_star_commute star_plus)
    also have "... ≤ -1"
      using assms(4) conv_complement conv_isotone by force
    finally have 18: "(prim_P w v e)⇧^T⇧⁺ ≤ -1"
      .
    have "(prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ = (prim_P w v e)⇧^T * ((w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧^⋆) * (w ⊓ -(prim_EP w v e))⇧^⋆"
      using 6 by (simp add: comp_associative)
    also have "... = (prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧⁺ * (w ⊓ -(prim_EP w v e))⇧^⋆ ⊔ (prim_P w v e)⇧^T⇧⁺ * (w ⊓ -(prim_EP w v e))⇧^⋆"
      by (simp add: mult_left_dist_sup mult_right_dist_sup)
    also have "... = (prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧⁺ * (w ⊓ -(prim_EP w v e))⇧^⋆"
      by (simp add: mult_assoc star.circ_transitive_equal)
    also have "... = (prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧⁺ * (1 ⊔ (w ⊓ -(prim_EP w v e))⇧⁺)"
      using star_left_unfold_equal by simp
    also have "... = (prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧⁺ * (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧⁺"
      by (simp add: mult_left_dist_sup sup.left_commute sup_commute)
    also have "... = ((prim_P w v e)⇧^T ⊔ (prim_P w v e)⇧^T⇧⁺) * (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧⁺"
      by (simp add: mult_right_dist_sup)
    also have "... = (prim_P w v e)⇧^T⇧⁺ * (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧⁺"
      using star.circ_mult_increasing by (simp add: le_iff_sup)
    also have "... ≤ -1"
      using 17 18 by simp
    finally show ?thesis
      .
  qed
  have 19: "e * (w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ -1"
  proof -
    have "e * (w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ = e * ((w ⊓ -(prim_EP w v e))⇧⁺ ⊔ (prim_P w v e)⇧^T⇧^⋆) * (w ⊓ -(prim_EP w v e))⇧^⋆"
      using 6 by (simp add: mult_assoc)
    also have "... = e * (w ⊓ -(prim_EP w v e))⇧⁺ * (w ⊓ -(prim_EP w v e))⇧^⋆ ⊔ e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆"
      by (simp add: mult_left_dist_sup mult_right_dist_sup)
    also have "... = e * (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆"
      by (simp add: mult_assoc star.circ_transitive_equal)
    also have "... ≤ e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧⁺ ⊔ e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆"
      by (metis mult_right_sub_dist_sup_right semiring.add_right_mono star.circ_back_loop_fixpoint)
    also have "... ≤ e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆"
      using mult_right_isotone star.left_plus_below_circ by auto
    also have "... ≤ v * -v⇧^T"
      using 11 by simp
    also have "... ≤ -1"
      by (simp add: pp_increasing schroeder_3_p)
    finally show ?thesis
      .
  qed
  have 20: "(prim_W w v e) * (w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ -1"
    using 15 16 19 by (simp add: comp_right_dist_sup)
  have 21: "(w ⊓ -(prim_EP w v e))⇧⁺ * e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ -1"
  proof -
    have "(w ⊓ -(prim_EP w v e)) * v * -v⇧^T ≤ w * v * -v⇧^T"
      by (simp add: comp_isotone star_isotone)
    also have "... ≤ v * -v⇧^T"
      by (simp add: assms(3) mult_left_isotone)
    finally have 22: "(w ⊓ -(prim_EP w v e)) * v * -v⇧^T ≤ v * -v⇧^T"
      .
    have "(w ⊓ -(prim_EP w v e))⇧⁺ * e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ (w ⊓ -(prim_EP w v e))⇧⁺ * v * -v⇧^T"
      using 11 by (simp add: mult_right_isotone mult_assoc)
    also have "... ≤ (w ⊓ -(prim_EP w v e))⇧^⋆ * v * -v⇧^T"
      using mult_left_isotone star.left_plus_below_circ by blast
    also have "... ≤ v * -v⇧^T"
      using 22 by (simp add: star_left_induct_mult mult_assoc)
    also have "... ≤ -1"
      by (simp add: pp_increasing schroeder_3_p)
    finally show ?thesis
      .
  qed
  have 23: "(prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧^⋆ * e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ -1"
  proof -
    have "(prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧^⋆ * e = (prim_P w v e)⇧^T * e ⊔ (prim_P w v e)⇧^T * (w ⊓ -(prim_EP w v e))⇧⁺ * e"
      using comp_left_dist_sup mult_assoc star.circ_loop_fixpoint sup_commute by auto
    also have "... = bot"
      using 1 9 by simp
    finally show ?thesis
      by simp
  qed
  have 24: "e * (w ⊓ -(prim_EP w v e))⇧^⋆ * e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ -1"
  proof -
    have "e * (w ⊓ -(prim_EP w v e))⇧^⋆ * e = e * e ⊔ e * (w ⊓ -(prim_EP w v e))⇧⁺ * e"
      using comp_left_dist_sup mult_assoc star.circ_loop_fixpoint sup_commute by auto
    also have "... = bot"
      using 2 10 by simp
    finally show ?thesis
      by simp
  qed
  have 25: "(prim_W w v e) * (w ⊓ -(prim_EP w v e))⇧^⋆ * e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ≤ -1"
    using 21 23 24 by (simp add: comp_right_dist_sup)
  have "(prim_W w v e)⇧^⋆ = ((prim_P w v e)⇧^T ⊔ e)⇧^⋆ * ((w ⊓ -(prim_EP w v e)) * ((prim_P w v e)⇧^T ⊔ e)⇧^⋆)⇧^⋆"
    by (metis star_sup_1 sup.left_commute sup_commute)
  also have "... = ((prim_P w v e)⇧^T⇧^⋆ ⊔ e * (prim_P w v e)⇧^T⇧^⋆) * ((w ⊓ -(prim_EP w v e)) * ((prim_P w v e)⇧^T⇧^⋆ ⊔ e * (prim_P w v e)⇧^T⇧^⋆))⇧^⋆"
    using 1 2 star_separate by auto
  also have "... = ((prim_P w v e)⇧^T⇧^⋆ ⊔ e * (prim_P w v e)⇧^T⇧^⋆) * ((w ⊓ -(prim_EP w v e)) * (1 ⊔ e * (prim_P w v e)⇧^T⇧^⋆))⇧^⋆"
    using 4 mult_left_dist_sup by auto
  also have "... = (w ⊓ -(prim_EP w v e))⇧^⋆ * ((prim_P w v e)⇧^T⇧^⋆ ⊔ e * (prim_P w v e)⇧^T⇧^⋆) * (w ⊓ -(prim_EP w v e))⇧^⋆"
    using 3 9 10 star_separate_2 by blast
  also have "... = (w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ⊔ (w ⊓ -(prim_EP w v e))⇧^⋆ * e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆"
    by (simp add: semiring.distrib_left semiring.distrib_right mult_assoc)
  finally have "(prim_W w v e)⇧⁺ = (prim_W w v e) * ((w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ⊔ (w ⊓ -(prim_EP w v e))⇧^⋆ * e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆)"
    by simp
  also have "... = (prim_W w v e) * (w ⊓ -(prim_EP w v e))⇧^⋆ * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆ ⊔ (prim_W w v e) * (w ⊓ -(prim_EP w v e))⇧^⋆ * e * (prim_P w v e)⇧^T⇧^⋆ * (w ⊓ -(prim_EP w v e))⇧^⋆"
    by (simp add: comp_left_dist_sup comp_associative)
  also have "... ≤ -1"
    using 20 25 by simp
  finally show ?thesis
    .
qed

text ‹
The following lemma shows that an edge across the cut between visited nodes and unvisited nodes does not leave the component of visited nodes.
›

lemma mst_subgraph_inv:
  assumes "e ≤ v * -v⇧^T ⊓ g"
      and "t ≤ g"
      and "v⇧^T = r⇧^T * t⇧^⋆"
    shows "e ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g"
proof -
  have "e ≤ v * -v⇧^T ⊓ g"
    by (rule assms(1))
  also have "... ≤ v * (-v⇧^T ⊓ v⇧^T * g) ⊓ g"
    by (simp add: dedekind_1)
  also have "... ≤ v * v⇧^T * g ⊓ g"
    by (simp add: comp_associative comp_right_isotone inf_commute le_infI2)
  also have "... = v * (r⇧^T * t⇧^⋆) * g ⊓ g"
    by (simp add: assms(3))
  also have "... = (r⇧^T * t⇧^⋆)⇧^T * (r⇧^T * t⇧^⋆) * g ⊓ g"
    by (metis assms(3) conv_involutive)
  also have "... ≤ (r⇧^T * t⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) * g ⊓ g"
    using assms(2) comp_inf.mult_left_isotone comp_isotone star_isotone by auto
  also have "... ≤ (r⇧^T * t⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g"
    using inf.sup_right_isotone inf_commute mult_assoc mult_right_isotone star.left_plus_below_circ star_plus by presburger
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g"
    using assms(2) comp_inf.mult_left_isotone conv_dist_comp conv_isotone mult_left_isotone star_isotone by auto
  finally show ?thesis
    .
qed

text ‹
The following lemmas show that the tree after exchanging contains the currently constructed and tree and its extension by the chosen edge.
›

lemma mst_extends_old_tree:
  assumes "t ≤ w"
      and "t ≤ v * v⇧^T"
      and "vector v"
    shows "t ≤ prim_W w v e"
proof -
  have "t ⊓ prim_EP w v e ≤ t ⊓ -v⇧^T"
    by (simp add: inf.coboundedI2 inf.sup_monoid.add_assoc)
  also have "... ≤ v * v⇧^T ⊓ -v⇧^T"
    by (simp add: assms(2) inf.coboundedI1)
  also have "... ≤ bot"
    by (simp add: assms(3) covector_vector_comp eq_refl schroeder_2)
  finally have "t ≤ -(prim_EP w v e)"
    using le_bot pseudo_complement by blast
  hence "t ≤ w ⊓ -(prim_EP w v e)"
    using assms(1) by simp
  thus ?thesis
    using le_supI1 by blast
qed

lemma mst_extends_new_tree:
  "t ≤ w ⟹ t ≤ v * v⇧^T ⟹ vector v ⟹ t ⊔ e ≤ prim_W w v e"
  using mst_extends_old_tree by auto

text ‹Lemmas ‹forests_bot_1›, ‹forests_bot_2›, ‹forests_bot_3› and ‹fc_comp_eq_fc› were contributed by Nicolas Robinson-O'Brien.›

lemma forests_bot_1:
  assumes "equivalence e"
      and "forest f"
    shows "(-e ⊓ f) * (e ⊓ f)⇧^T = bot"
proof -
  have "f * f⇧^T ≤ e"
    using assms dual_order.trans by blast
  hence "f * (e ⊓ f)⇧^T ≤ e"
    by (metis conv_dist_inf inf.boundedE inf.cobounded2 inf.orderE mult_right_isotone)
  hence "-e ⊓ f * (e ⊓ f)⇧^T = bot"
    by (simp add: p_antitone pseudo_complement)
  thus ?thesis
    by (metis assms(1) comp_isotone conv_dist_inf equivalence_comp_right_complement inf.boundedI inf.cobounded1 inf.cobounded2 le_bot)
qed

lemma forests_bot_2:
  assumes "equivalence e"
      and "forest f"
    shows "(-e ⊓ f⇧^T) * x ⊓ (e ⊓ f⇧^T) * y = bot"
proof -
  have "(-e ⊓ f) * (e ⊓ f⇧^T) = bot"
    using assms forests_bot_1 conv_dist_inf by simp
  thus ?thesis
    by (smt assms(1) comp_associative comp_inf.semiring.mult_not_zero conv_complement conv_dist_comp conv_dist_inf conv_involutive dedekind_1 inf.cobounded2 inf.sup_monoid.add_commute le_bot mult_right_zero p_antitone_iff pseudo_complement semiring.mult_not_zero symmetric_top_closed top.extremum)
qed

lemma forests_bot_3:
  assumes "equivalence e"
      and "forest f"
    shows "x * (-e ⊓ f) ⊓ y * (e ⊓ f) = bot"
proof -
  have "(e ⊓ f) * (-e ⊓ f⇧^T) = bot"
    using assms forests_bot_1 conv_dist_inf conv_complement by (smt conv_dist_comp conv_involutive conv_order coreflexive_bot_closed coreflexive_symmetric)
  hence "y * (e ⊓ f) * (-e ⊓ f⇧^T) = bot"
    by (simp add: comp_associative)
  hence 1: "x ⊓ y * (e ⊓ f) * (-e ⊓ f⇧^T) = bot"
    using comp_inf.semiring.mult_not_zero by blast
  hence "(x ⊓ y * (e ⊓ f) * (-e ⊓ f⇧^T)) * (-e ⊓ f) = bot"
    using semiring.mult_not_zero by blast
  hence "x * (-e ⊓ f⇧^T)⇧^T ⊓ y * (e ⊓ f) = bot"
    using 1 dedekind_2 inf_commute schroeder_2 by auto
  thus ?thesis
    by (simp add: assms(1) conv_complement conv_dist_inf)
qed

lemma acyclic_plus:
  "acyclic x ⟹ acyclic (x⇧⁺)"
  by (simp add: star.circ_transitive_equal star.left_plus_circ mult_assoc)

end

text ‹
We finally add the Kleene star to Stone relation algebras.
Kleene star and the relational operations are reasonably independent.
The only additional axiom we need in the generalisation to Stone-Kleene relation algebras is that star distributes over double complement.
›

class stone_kleene_relation_algebra = stone_relation_algebra + pd_kleene_allegory +
  assumes pp_dist_star: "--(x⇧^⋆) = (--x)⇧^⋆"
begin

lemma reachable_without_loops:
  "x⇧^⋆ = (x ⊓ -1)⇧^⋆"
proof (rule order.antisym)
  have "x * (x ⊓ -1)⇧^⋆ = (x ⊓ 1) * (x ⊓ -1)⇧^⋆ ⊔ (x ⊓ -1) * (x ⊓ -1)⇧^⋆"
    by (metis maddux_3_11_pp mult_right_dist_sup regular_one_closed)
  also have "... ≤ (x ⊓ -1)⇧^⋆"
    by (metis inf.cobounded2 le_supI mult_left_isotone star.circ_circ_mult star.left_plus_below_circ star_involutive star_one)
  finally show "x⇧^⋆ ≤ (x ⊓ -1)⇧^⋆"
    by (metis inf.cobounded2 maddux_3_11_pp regular_one_closed star.circ_circ_mult star.circ_sup_2 star_involutive star_sub_one)
next
  show "(x ⊓ -1)⇧^⋆ ≤ x⇧^⋆"
    by (simp add: star_isotone)
qed

lemma plus_reachable_without_loops:
  "x⇧⁺ = (x ⊓ -1)⇧⁺ ⊔ (x ⊓ 1)"
  by (metis comp_associative maddux_3_11_pp regular_one_closed star.circ_back_loop_fixpoint star.circ_loop_fixpoint sup_assoc reachable_without_loops)

lemma star_plus_without_loops:
  "x⇧^⋆ ⊓ -1 = x⇧⁺ ⊓ -1"
  by (metis maddux_3_13 star_left_unfold_equal)

lemma regular_closed_star:
  "regular x ⟹ regular (x⇧^⋆)"
  by (simp add: pp_dist_star)

lemma components_idempotent:
  "components (components x) = components x"
  using pp_dist_star star_involutive by auto

lemma fc_comp_eq_fc:
  "-forest_components (--f) = -forest_components f"
  by (metis conv_complement p_comp_pp p_pp_comp pp_dist_star)

text ‹
The following lemma shows that the nodes reachable in the tree after exchange contain the nodes reachable in the tree before exchange.
›

lemma mst_reachable_inv:
  assumes "regular (prim_EP w v e)"
      and "vector r"
      and "e ≤ v * -v⇧^T"
      and "vector v"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "t ≤ w"
      and "t ≤ v * v⇧^T"
      and "w * v ≤ v"
    shows "r⇧^T * w⇧^⋆ ≤ r⇧^T * (prim_W w v e)⇧^⋆"
proof -
  have 1: "r⇧^T ≤ r⇧^T * (prim_W w v e)⇧^⋆"
    using sup.bounded_iff star.circ_back_loop_prefixpoint by blast
  have "top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ * w⇧^T ⊓ -v⇧^T = top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ * (w⇧^T ⊓ -v⇧^T)"
    by (simp add: assms(4) covector_comp_inf vector_conv_compl)
  also have "... ≤ top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆"
    by (simp add: comp_isotone mult_assoc star.circ_plus_same star.left_plus_below_circ)
  finally have 2: "top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ * w⇧^T ≤ top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ ⊔ --v⇧^T"
    by (simp add: shunting_var_p)
  have 3: "--v⇧^T * w⇧^T ≤ top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ ⊔ --v⇧^T"
    by (metis assms(8) conv_dist_comp conv_order mult_assoc order.trans pp_comp_semi_commute pp_isotone sup.coboundedI1 sup_commute)
  have 4: "top * e ≤ top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ ⊔ --v⇧^T"
    using sup_right_divisibility star.circ_back_loop_fixpoint le_supI1 by blast
  have "(top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ ⊔ --v⇧^T) * w⇧^T = top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ * w⇧^T ⊔ --v⇧^T * w⇧^T"
    by (simp add: comp_right_dist_sup)
  also have "... ≤ top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ ⊔ --v⇧^T"
    using 2 3 by simp
  finally have "top * e ⊔ (top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ ⊔ --v⇧^T) * w⇧^T ≤ top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ ⊔ --v⇧^T"
    using 4 by simp
  hence 5: "top * e * w⇧^T⇧^⋆ ≤ top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆ ⊔ --v⇧^T"
    by (simp add: star_right_induct)
  have 6: "top * e ≤ top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆"
    using sup_right_divisibility star.circ_back_loop_fixpoint by blast
  have "(top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆)⇧^T ≤ (top * e * w⇧^T⇧^⋆)⇧^T"
    by (simp add: star_isotone mult_right_isotone conv_isotone inf_assoc)
  also have "... = w⇧^⋆ * e⇧^T * top"
    by (simp add: conv_dist_comp conv_star_commute mult_assoc)
  finally have 7: "(top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆)⇧^T ≤ w⇧^⋆ * e⇧^T * top"
    .
  have "(top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆)⇧^T ≤ (top * e * (-v * -v⇧^T)⇧^⋆)⇧^T"
    by (simp add: conv_isotone inf_commute mult_right_isotone star_isotone le_infI2)
  also have "... ≤ (top * v * -v⇧^T * (-v * -v⇧^T)⇧^⋆)⇧^T"
    by (metis assms(3) conv_isotone mult_left_isotone mult_right_isotone mult_assoc)
  also have "... = (top * v * (-v⇧^T * -v)⇧^⋆ * -v⇧^T)⇧^T"
    by (simp add: mult_assoc star_slide)
  also have "... ≤ (top * -v⇧^T)⇧^T"
    using conv_order mult_left_isotone by auto
  also have "... = -v"
    by (simp add: assms(4) conv_complement vector_conv_compl)
  finally have 8: "(top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆)⇧^T ≤ w⇧^⋆ * e⇧^T * top ⊓ -v"
    using 7 by simp
  have "covector (top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆)"
    by (simp add: covector_mult_closed)
  hence "top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆ * (w⇧^T ⊓ -v⇧^T) = top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆ * (w⇧^T ⊓ -v⇧^T ⊓ (top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆)⇧^T)"
    by (metis comp_inf_vector_1 inf.idem)
  also have "... ≤ top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆ * (w⇧^T ⊓ -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top ⊓ -v)"
    using 8 mult_right_isotone inf.sup_right_isotone inf_assoc by simp
  also have "... = top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆ * (w⇧^T ⊓ (-v ⊓ -v⇧^T) ⊓ w⇧^⋆ * e⇧^T * top)"
    using inf_assoc inf_commute by (simp add: inf_assoc)
  also have "... = top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆ * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)"
    using assms(4) conv_complement vector_complement_closed vector_covector by fastforce
  also have "... ≤ top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆"
    by (simp add: comp_associative comp_isotone star.circ_plus_same star.left_plus_below_circ)
  finally have 9: "top * e ⊔ top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆ * (w⇧^T ⊓ -v⇧^T) ≤ top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆"
    using 6 by simp
  have "prim_EP w v e ≤ -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
    using inf.sup_left_isotone by auto
  also have "... ≤ top * e * (w⇧^T ⊓ -v⇧^T)⇧^⋆"
    using 5 by (metis inf_commute shunting_var_p)
  also have "... ≤ top * e * (w⇧^T ⊓ -v * -v⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^⋆"
    using 9 by (simp add: star_right_induct)
  finally have 10: "prim_EP w v e ≤ top * e * (prim_P w v e)⇧^T⇧^⋆"
    by (simp add: conv_complement conv_dist_comp conv_dist_inf conv_star_commute mult_assoc)
  have "top * e = top * (v * -v⇧^T ⊓ e)"
    by (simp add: assms(3) inf.absorb2)
  also have "... ≤ top * (v * top ⊓ e)"
    using inf.sup_right_isotone inf_commute mult_right_isotone top_greatest by presburger
  also have "... = (top ⊓ (v * top)⇧^T) * e"
    using assms(4) covector_inf_comp_3 by presburger
  also have "... = top * v⇧^T * e"
    by (simp add: conv_dist_comp)
  also have "... = top * r⇧^T * t⇧^⋆ * e"
    by (simp add: assms(5) comp_associative)
  also have "... ≤ top * r⇧^T * (prim_W w v e)⇧^⋆ * e"
    by (metis assms(4,6,7) mst_extends_old_tree star_isotone mult_left_isotone mult_right_isotone)
  finally have 11: "top * e ≤ top * r⇧^T * (prim_W w v e)⇧^⋆ * e"
    .
  have "r⇧^T * (prim_W w v e)⇧^⋆ * (prim_EP w v e) ≤ r⇧^T * (prim_W w v e)⇧^⋆ * (top * e * (prim_P w v e)⇧^T⇧^⋆)"
    using 10 mult_right_isotone by blast
  also have "... = r⇧^T * (prim_W w v e)⇧^⋆ * top * e * (prim_P w v e)⇧^T⇧^⋆"
    by (simp add: mult_assoc)
  also have "... ≤ top * e * (prim_P w v e)⇧^T⇧^⋆"
    by (metis comp_associative comp_inf_covector inf.idem inf.sup_right_divisibility)
  also have "... ≤ top * r⇧^T * (prim_W w v e)⇧^⋆ * e * (prim_P w v e)⇧^T⇧^⋆"
    using 11 by (simp add: mult_left_isotone)
  also have "... = r⇧^T * (prim_W w v e)⇧^⋆ * e * (prim_P w v e)⇧^T⇧^⋆"
    using assms(2) vector_conv_covector by auto
  also have "... ≤ r⇧^T * (prim_W w v e)⇧^⋆ * (prim_W w v e) * (prim_P w v e)⇧^T⇧^⋆"
    by (simp add: mult_left_isotone mult_right_isotone)
  also have "... ≤ r⇧^T * (prim_W w v e)⇧^⋆ * (prim_W w v e) * (prim_W w v e)⇧^⋆"
    by (meson dual_order.trans mult_right_isotone star_isotone sup_ge1 sup_ge2)
  also have "... ≤ r⇧^T * (prim_W w v e)⇧^⋆"
    by (metis mult_assoc mult_right_isotone star.circ_transitive_equal star.left_plus_below_circ)
  finally have 12: "r⇧^T * (prim_W w v e)⇧^⋆ * (prim_EP w v e) ≤ r⇧^T * (prim_W w v e)⇧^⋆"
    .
  have "r⇧^T * (prim_W w v e)⇧^⋆ * w ≤ r⇧^T * (prim_W w v e)⇧^⋆ * (w ⊔ prim_EP w v e)"
    by (simp add: inf_assoc)
  also have "... = r⇧^T * (prim_W w v e)⇧^⋆ * ((w ⊔ prim_EP w v e) ⊓ (-(prim_EP w v e) ⊔ prim_EP w v e))"
    by (metis assms(1) inf_top_right stone)
  also have "... = r⇧^T * (prim_W w v e)⇧^⋆ * ((w ⊓ -(prim_EP w v e)) ⊔ prim_EP w v e)"
    by (simp add: sup_inf_distrib2)
  also have "... = r⇧^T * (prim_W w v e)⇧^⋆ * (w ⊓ -(prim_EP w v e)) ⊔ r⇧^T * (prim_W w v e)⇧^⋆ * (prim_EP w v e)"
    by (simp add: comp_left_dist_sup)
  also have "... ≤ r⇧^T * (prim_W w v e)⇧^⋆ * (prim_W w v e) ⊔ r⇧^T * (prim_W w v e)⇧^⋆ * (prim_EP w v e)"
    using mult_right_isotone sup_left_isotone by auto
  also have "... ≤ r⇧^T * (prim_W w v e)⇧^⋆ ⊔ r⇧^T * (prim_W w v e)⇧^⋆ * (prim_EP w v e)"
    using mult_assoc mult_right_isotone star.circ_plus_same star.left_plus_below_circ sup_left_isotone by auto
  also have "... = r⇧^T * (prim_W w v e)⇧^⋆"
    using 12 sup.absorb1 by blast
  finally have "r⇧^T ⊔ r⇧^T * (prim_W w v e)⇧^⋆ * w ≤ r⇧^T * (prim_W w v e)⇧^⋆"
    using 1 by simp
  thus ?thesis
    by (simp add: star_right_induct)
qed

text ‹
Some of the following lemmas already hold in pseudocomplemented distributive Kleene allegories.
›

subsubsection ‹Exchange gives Minimum Spanning Trees›

text ‹
The lemmas in this section are used to show that the after exchange we obtain a minimum spanning tree.
The following lemmas show various interactions between the three constituents of the tree after exchange.
›

lemma epm_1:
  "vector v ⟹ prim_E w v e ⊔ prim_P w v e = prim_EP w v e"
  by (metis inf_commute inf_sup_distrib1 mult_assoc mult_right_dist_sup regular_closed_p regular_complement_top vector_conv_compl)

lemma epm_2:
  assumes "regular (prim_EP w v e)"
      and "vector v"
    shows "(w ⊓ -(prim_EP w v e)) ⊔ prim_P w v e ⊔ prim_E w v e = w"
proof -
  have "(w ⊓ -(prim_EP w v e)) ⊔ prim_P w v e ⊔ prim_E w v e = (w ⊓ -(prim_EP w v e)) ⊔ prim_EP w v e"
    using epm_1 sup_assoc sup_commute assms(2) by (simp add: inf_sup_distrib1)
  also have "... = w ⊔ prim_EP w v e"
    by (metis assms(1) inf_top.right_neutral regular_complement_top sup_inf_distrib2)
  also have "... = w"
    by (simp add: sup_inf_distrib1)
  finally show ?thesis
    .
qed

lemma epm_4:
  assumes "e ≤ w"
      and "injective w"
      and "w * v ≤ v"
      and "e ≤ v * -v⇧^T"
    shows "top * e * w⇧^T⇧⁺ ≤ top * v⇧^T"
proof -
  have "w⇧^⋆ * v ≤ v"
    by (simp add: assms(3) star_left_induct_mult)
  hence 1: "v⇧^T * w⇧^T⇧^⋆ ≤ v⇧^T"
    using conv_star_commute conv_dist_comp conv_isotone by fastforce
  have "e * w⇧^T ≤ w * w⇧^T ⊓ e * w⇧^T"
    by (simp add: assms(1) mult_left_isotone)
  also have "... ≤ 1 ⊓ e * w⇧^T"
    using assms(2) inf.sup_left_isotone by auto
  also have "... = 1 ⊓ w * e⇧^T"
    using calculation conv_dist_comp conv_involutive coreflexive_symmetric by fastforce
  also have "... ≤ w * e⇧^T"
    by simp
  also have "... ≤ w * -v * v⇧^T"
    by (metis assms(4) conv_complement conv_dist_comp conv_involutive conv_order mult_assoc mult_right_isotone)
  also have "... ≤ top * v⇧^T"
    by (simp add: mult_left_isotone)
  finally have "top * e * w⇧^T⇧⁺ ≤ top * v⇧^T * w⇧^T⇧^⋆"
    by (metis order.antisym comp_associative comp_isotone dense_top_closed mult_left_isotone transitive_top_closed)
  also have "... ≤ top * v⇧^T"
    using 1 by (simp add: mult_assoc mult_right_isotone)
  finally show ?thesis
    .
qed

lemma epm_5:
  assumes "e ≤ w"
      and "injective w"
      and "w * v ≤ v"
      and "e ≤ v * -v⇧^T"
      and "vector v"
    shows "prim_P w v e = bot"
proof -
  have 1: "e = w ⊓ top * e"
    by (simp add: assms(1,2) epm_3)
  have 2: "top * e * w⇧^T⇧⁺ ≤ top * v⇧^T"
    by (simp add: assms(1-4) epm_4)
  have 3: "-v * -v⇧^T ⊓ top * v⇧^T = bot"
    by (simp add: assms(5) comp_associative covector_vector_comp inf.sup_monoid.add_commute schroeder_2)
  have "prim_P w v e = (w ⊓ -v * -v⇧^T ⊓ top * e) ⊔ (w ⊓ -v * -v⇧^T ⊓ top * e * w⇧^T⇧⁺)"
    by (metis inf_sup_distrib1 mult_assoc star.circ_back_loop_fixpoint star_plus sup_commute)
  also have "... ≤ (e ⊓ -v * -v⇧^T) ⊔ (w ⊓ -v * -v⇧^T ⊓ top * e * w⇧^T⇧⁺)"
    using 1 by (metis comp_inf.mult_semi_associative inf.sup_monoid.add_commute semiring.add_right_mono)
  also have "... ≤ (e ⊓ -v * -v⇧^T) ⊔ (w ⊓ -v * -v⇧^T ⊓ top * v⇧^T)"
    using 2 by (metis sup_right_isotone inf.sup_right_isotone)
  also have "... ≤ (e ⊓ -v * -v⇧^T) ⊔ (-v * -v⇧^T ⊓ top * v⇧^T)"
    using inf.assoc le_infI2 by auto
  also have "... ≤ v * -v⇧^T ⊓ -v * -v⇧^T"
    using 3 assms(4) inf.sup_left_isotone by auto
  also have "... ≤ v * top ⊓ -v * top"
    using inf.sup_mono mult_right_isotone top_greatest by blast
  also have "... = bot"
    using assms(5) inf_compl_bot vector_complement_closed by auto
  finally show ?thesis
    by (simp add: le_iff_inf)
qed

lemma epm_6:
  assumes "e ≤ w"
      and "injective w"
      and "w * v ≤ v"
      and "e ≤ v * -v⇧^T"
      and "vector v"
    shows "prim_E w v e = e"
proof -
  have 1: "e ≤ --v * -v⇧^T"
    using assms(4) mult_isotone order_lesseq_imp pp_increasing by blast
  have 2: "top * e * w⇧^T⇧⁺ ≤ top * v⇧^T"
    by (simp add: assms(1-4) epm_4)
  have 3: "e = w ⊓ top * e"
    by (simp add: assms(1,2) epm_3)
  hence "e ≤ top * e * w⇧^T⇧^⋆"
    by (metis le_infI2 star.circ_back_loop_fixpoint sup.commute sup_ge1)
  hence 4: "e ≤ prim_E w v e"
    using 1 by (simp add: assms(1))
  have 5: "--v * -v⇧^T ⊓ top * v⇧^T = bot"
    by (simp add: assms(5) comp_associative covector_vector_comp inf.sup_monoid.add_commute schroeder_2)
  have "prim_E w v e = (w ⊓ --v * -v⇧^T ⊓ top * e) ⊔ (w ⊓ --v * -v⇧^T ⊓ top * e * w⇧^T⇧⁺)"
    by (metis inf_sup_distrib1 mult_assoc star.circ_back_loop_fixpoint star_plus sup_commute)
  also have "... ≤ (e ⊓ --v * -v⇧^T) ⊔ (w ⊓ --v * -v⇧^T ⊓ top * e * w⇧^T⇧⁺)"
    using 3 by (metis comp_inf.mult_semi_associative inf.sup_monoid.add_commute semiring.add_right_mono)
  also have "... ≤ (e ⊓ --v * -v⇧^T) ⊔ (w ⊓ --v * -v⇧^T ⊓ top * v⇧^T)"
    using 2 by (metis sup_right_isotone inf.sup_right_isotone)
  also have "... ≤ (e ⊓ --v * -v⇧^T) ⊔ (--v * -v⇧^T ⊓ top * v⇧^T)"
    using inf.assoc le_infI2 by auto
  also have "... ≤ e"
    by (simp add: "5")
  finally show ?thesis
    using 4 by (simp add: order.antisym)
qed

lemma epm_7:
  "regular (prim_EP w v e) ⟹ e ≤ w ⟹ injective w ⟹ w * v ≤ v ⟹ e ≤ v * -v⇧^T ⟹ vector v ⟹ prim_W w v e = w"
  by (metis conv_bot epm_2 epm_5 epm_6)

lemma epm_8:
  assumes "acyclic w"
    shows "(w ⊓ -(prim_EP w v e)) ⊓ (prim_P w v e)⇧^T = bot"
proof -
  have "(w ⊓ -(prim_EP w v e)) ⊓ (prim_P w v e)⇧^T ≤ w ⊓ w⇧^T"
    by (meson conv_isotone inf_le1 inf_mono order_trans)
  thus ?thesis
    by (metis assms acyclic_asymmetric inf.commute le_bot)
qed

lemma epm_9:
  assumes "e ≤ v * -v⇧^T"
      and "vector v"
    shows "(w ⊓ -(prim_EP w v e)) ⊓ e = bot"
proof -
  have 1: "e ≤ -v⇧^T"
    by (metis assms complement_conv_sub vector_conv_covector ev p_antitone_iff p_bot)
  have "(w ⊓ -(prim_EP w v e)) ⊓ e = (w ⊓ --v⇧^T ⊓ e) ⊔ (w ⊓ -(top * e * w⇧^T⇧^⋆) ⊓ e)"
    by (simp add: inf_commute inf_sup_distrib1)
  also have "... ≤ (--v⇧^T ⊓ e) ⊔ (-(top * e * w⇧^T⇧^⋆) ⊓ e)"
    using comp_inf.mult_left_isotone inf.cobounded2 semiring.add_mono by blast
  also have "... = -(top * e * w⇧^T⇧^⋆) ⊓ e"
    using 1 by (metis inf.sup_relative_same_increasing inf_commute inf_sup_distrib1 maddux_3_13 regular_closed_p)
  also have "... = bot"
    by (metis inf.sup_relative_same_increasing inf_bot_right inf_commute inf_p mult_left_isotone star_outer_increasing top_greatest)
  finally show ?thesis
    by (simp add: le_iff_inf)
qed

lemma epm_10:
  assumes "e ≤ v * -v⇧^T"
      and "vector v"
    shows "(prim_P w v e)⇧^T ⊓ e = bot"
proof -
  have "(prim_P w v e)⇧^T ≤ -v * -v⇧^T"
    by (simp add: conv_complement conv_dist_comp conv_dist_inf inf.absorb_iff1 inf.left_commute inf_commute)
  hence "(prim_P w v e)⇧^T ⊓ e ≤ -v * -v⇧^T ⊓ v * -v⇧^T"
    using assms(1) inf_mono by blast
  also have "... ≤ -v * top ⊓ v * top"
    using inf.sup_mono mult_right_isotone top_greatest by blast
  also have "... = bot"
    using assms(2) inf_compl_bot vector_complement_closed by auto
  finally show ?thesis
    by (simp add: le_iff_inf)
qed

lemma epm_11:
  assumes "vector v"
    shows "(w ⊓ -(prim_EP w v e)) ⊓ prim_P w v e = bot"
proof -
  have "prim_P w v e ≤ prim_EP w v e"
    by (metis assms comp_isotone inf.sup_left_isotone inf.sup_right_isotone order.refl top_greatest vector_conv_compl)
  thus ?thesis
    using inf_le2 order_trans p_antitone pseudo_complement by blast
qed

lemma epm_12:
  assumes "vector v"
    shows "(w ⊓ -(prim_EP w v e)) ⊓ prim_E w v e = bot"
proof -
  have "prim_E w v e ≤ prim_EP w v e"
    by (metis assms comp_isotone inf.sup_left_isotone inf.sup_right_isotone order.refl top_greatest vector_conv_compl)
  thus ?thesis
    using inf_le2 order_trans p_antitone pseudo_complement by blast
qed

lemma epm_13:
  assumes "vector v"
    shows "prim_P w v e ⊓ prim_E w v e = bot"
proof -
  have "prim_P w v e ⊓ prim_E w v e ≤ -v * -v⇧^T ⊓ --v * -v⇧^T"
    by (meson dual_order.trans inf.cobounded1 inf.sup_mono inf_le2)
  also have "... ≤ -v * top ⊓ --v * top"
    using inf.sup_mono mult_right_isotone top_greatest by blast
  also have "... = bot"
    using assms inf_compl_bot vector_complement_closed by auto
  finally show ?thesis
    by (simp add: le_iff_inf)
qed

text ‹
The following lemmas show that the relation characterising the edge across the cut is an arc.
›

lemma arc_edge_1:
  assumes "e ≤ v * -v⇧^T ⊓ g"
      and "vector v"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "t ≤ g"
      and "r⇧^T * g⇧^⋆ ≤ r⇧^T * w⇧^⋆"
    shows "top * e ≤ v⇧^T * w⇧^⋆"
proof -
  have "top * e ≤ top * (v * -v⇧^T ⊓ g)"
    using assms(1) mult_right_isotone by auto
  also have "... ≤ top * (v * top ⊓ g)"
    using inf.sup_right_isotone inf_commute mult_right_isotone top_greatest by presburger
  also have "... = v⇧^T * g"
    by (metis assms(2) covector_inf_comp_3 inf_top.left_neutral)
  also have "... = r⇧^T * t⇧^⋆ * g"
    by (simp add: assms(3))
  also have "... ≤ r⇧^T * g⇧^⋆ * g"
    by (simp add: assms(4) mult_left_isotone mult_right_isotone star_isotone)
  also have "... ≤ r⇧^T * g⇧^⋆"
    by (simp add: mult_assoc mult_right_isotone star.right_plus_below_circ)
  also have "... ≤ r⇧^T * w⇧^⋆"
    by (simp add: assms(5))
  also have "... ≤ v⇧^T * w⇧^⋆"
    by (metis assms(3) mult_left_isotone mult_right_isotone mult_1_right star.circ_reflexive)
  finally show ?thesis
    .
qed

lemma arc_edge_2:
  assumes "e ≤ v * -v⇧^T ⊓ g"
      and "vector v"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "t ≤ g"
      and "r⇧^T * g⇧^⋆ ≤ r⇧^T * w⇧^⋆"
      and "w * v ≤ v"
      and "injective w"
    shows "top * e * w⇧^T⇧^⋆ ≤ v⇧^T * w⇧^⋆"
proof -
  have 1: "top * e ≤ v⇧^T * w⇧^⋆"
    using assms(1-5) arc_edge_1 by blast
  have "v⇧^T * w⇧^⋆ * w⇧^T = v⇧^T * w⇧^T ⊔ v⇧^T * w⇧⁺ * w⇧^T"
    by (metis mult_assoc mult_left_dist_sup star.circ_loop_fixpoint sup_commute)
  also have "... ≤ v⇧^T ⊔ v⇧^T * w⇧⁺ * w⇧^T"
    by (metis assms(6) conv_dist_comp conv_isotone sup_left_isotone)
  also have "... = v⇧^T ⊔ v⇧^T * w⇧^⋆ * (w * w⇧^T)"
    by (metis mult_assoc star_plus)
  also have "... ≤ v⇧^T ⊔ v⇧^T * w⇧^⋆"
    by (metis assms(7) mult_right_isotone mult_1_right sup_right_isotone)
  also have "... = v⇧^T * w⇧^⋆"
    by (metis star.circ_back_loop_fixpoint sup_absorb2 sup_ge2)
  finally show ?thesis
    using 1 star_right_induct by auto
qed

lemma arc_edge_3:
  assumes "e ≤ v * -v⇧^T ⊓ g"
      and "vector v"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "t ≤ g"
      and "r⇧^T * g⇧^⋆ ≤ r⇧^T * w⇧^⋆"
      and "w * v ≤ v"
      and "injective w"
      and "prim_E w v e = bot"
    shows "e = bot"
proof -
  have "bot = prim_E w v e"
    by (simp add: assms(8))
  also have "... = w ⊓ --v * top ⊓ top * -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
    by (metis assms(2) comp_inf_covector inf.assoc inf_top.left_neutral vector_conv_compl)
  also have "... = w ⊓ top * e * w⇧^T⇧^⋆ ⊓ -v⇧^T ⊓ --v"
    using assms(2) inf.assoc inf.commute vector_conv_compl vector_complement_closed by (simp add: inf_assoc)
  finally have 1: "w ⊓ top * e * w⇧^T⇧^⋆ ⊓ -v⇧^T ≤ -v"
    using shunting_1_pp by force
  have "w⇧^⋆ * e⇧^T * top = (top * e * w⇧^T⇧^⋆)⇧^T"
    by (simp add: conv_star_commute comp_associative conv_dist_comp)
  also have "... ≤ (v⇧^T * w⇧^⋆)⇧^T"
    using assms(1-7) arc_edge_2 by (simp add: conv_isotone)
  also have "... = w⇧^T⇧^⋆ * v"
    by (simp add: conv_star_commute conv_dist_comp)
  finally have 2: "w⇧^⋆ * e⇧^T * top ≤ w⇧^T⇧^⋆ * v"
    .
  have "(w⇧^T ⊓ w⇧^⋆ * e⇧^T * top)⇧^T * -v = (w ⊓ top * e * w⇧^T⇧^⋆) * -v"
    by (simp add: conv_dist_comp conv_dist_inf conv_star_commute mult_assoc)
  also have "... = (w ⊓ top * e * w⇧^T⇧^⋆ ⊓ -v⇧^T) * top"
    by (metis assms(2) conv_complement covector_inf_comp_3 inf_top.right_neutral vector_complement_closed)
  also have "... ≤ -v * top"
    using 1 by (simp add: comp_isotone)
  also have "... = -v"
    using assms(2) vector_complement_closed by auto
  finally have "(w⇧^T ⊓ w⇧^⋆ * e⇧^T * top) * --v ≤ --v"
    using p_antitone_iff schroeder_3_p by auto
  hence "w⇧^⋆ * e⇧^T * top ⊓ w⇧^T * --v ≤ --v"
    by (simp add: inf_vector_comp)
  hence 3: "w⇧^T * --v ≤ --v ⊔ -(w⇧^⋆ * e⇧^T * top)"
    by (simp add: inf.commute shunting_p)
  have "w⇧^T * -(w⇧^⋆ * e⇧^T * top) ≤ -(w⇧^⋆ * e⇧^T * top)"
    by (metis mult_assoc p_antitone p_antitone_iff schroeder_3_p star.circ_loop_fixpoint sup_commute sup_right_divisibility)
  also have "... ≤ --v ⊔ -(w⇧^⋆ * e⇧^T * top)"
    by simp
  finally have "w⇧^T * (--v ⊔ -(w⇧^⋆ * e⇧^T * top)) ≤ --v ⊔ -(w⇧^⋆ * e⇧^T * top)"
    using 3 by (simp add: mult_left_dist_sup)
  hence "w⇧^T⇧^⋆ * (--v ⊔ -(w⇧^⋆ * e⇧^T * top)) ≤ --v ⊔ -(w⇧^⋆ * e⇧^T * top)"
    using star_left_induct_mult_iff by blast
  hence "w⇧^T⇧^⋆ * --v ≤ --v ⊔ -(w⇧^⋆ * e⇧^T * top)"
    by (simp add: semiring.distrib_left)
  hence "w⇧^⋆ * e⇧^T * top ⊓ w⇧^T⇧^⋆ * --v ≤ --v"
    by (simp add: inf_commute shunting_p)
  hence "w⇧^⋆ * e⇧^T * top ≤ --v"
    using 2 by (metis inf.absorb1 p_antitone_iff p_comp_pp vector_export_comp)
  hence 4: "e⇧^T * top ≤ --v"
    by (metis mult_assoc star.circ_loop_fixpoint sup.bounded_iff)
  have "e⇧^T * top ≤ (v * -v⇧^T)⇧^T * top"
    using assms(1) comp_isotone conv_isotone by auto
  also have "... ≤ -v * top"
    by (simp add: conv_complement conv_dist_comp mult_assoc mult_right_isotone)
  also have "... = -v"
    using assms(2) vector_complement_closed by auto
  finally have "e⇧^T * top ≤ bot"
    using 4 shunting_1_pp by auto
  hence "e⇧^T = bot"
    using order.antisym bot_least top_right_mult_increasing by blast
  thus ?thesis
    using conv_bot by fastforce
qed

lemma arc_edge_4:
  assumes "e ≤ v * -v⇧^T ⊓ g"
      and "vector v"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "t ≤ g"
      and "r⇧^T * g⇧^⋆ ≤ r⇧^T * w⇧^⋆"
      and "arc e"
    shows "top * prim_E w v e * top = top"
proof -
  have "--v⇧^T * w = (--v⇧^T * w ⊓ -v⇧^T) ⊔ (--v⇧^T * w ⊓ --v⇧^T)"
    by (simp add: maddux_3_11_pp)
  also have "... ≤ (--v⇧^T * w ⊓ -v⇧^T) ⊔ --v⇧^T"
    using sup_right_isotone by auto
  also have "... = --v⇧^T * (w ⊓ -v⇧^T) ⊔ --v⇧^T"
    using assms(2) covector_comp_inf covector_complement_closed vector_conv_covector by auto
  also have "... ≤ --v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆ ⊔ --v⇧^T"
    by (metis star.circ_back_loop_fixpoint sup.cobounded2 sup_left_isotone)
  finally have 1: "--v⇧^T * w ≤ --v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆ ⊔ --v⇧^T"
    .
  have "--v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆ * w ≤ --v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆ ⊔ --v⇧^T"
    by (simp add: le_supI1 mult_assoc mult_right_isotone star.circ_plus_same star.left_plus_below_circ)
  hence 2: "(--v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆ ⊔ --v⇧^T) * w ≤ --v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆ ⊔ --v⇧^T"
    using 1 by (simp add: inf.orderE mult_right_dist_sup)
  have "v⇧^T ≤ --v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆ ⊔ --v⇧^T"
    by (simp add: pp_increasing sup.coboundedI2)
  hence "v⇧^T * w⇧^⋆ ≤ --v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆ ⊔ --v⇧^T"
    using 2 by (simp add: star_right_induct)
  hence 3: "-v⇧^T ⊓ v⇧^T * w⇧^⋆ ≤ --v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆"
    by (metis inf_commute shunting_var_p)
  have "top * e = top * e ⊓ v⇧^T * w⇧^⋆"
    by (meson assms(1-5) arc_edge_1 inf.orderE)
  also have "... ≤ top * v * -v⇧^T ⊓ v⇧^T * w⇧^⋆"
    using assms(1) inf.sup_left_isotone mult_assoc mult_right_isotone by auto
  also have "... ≤ top * -v⇧^T ⊓ v⇧^T * w⇧^⋆"
    using inf.sup_left_isotone mult_left_isotone top_greatest by blast
  also have "... = -v⇧^T ⊓ v⇧^T * w⇧^⋆"
    by (simp add: assms(2) vector_conv_compl)
  also have "... ≤ --v⇧^T * (w ⊓ -v⇧^T) * w⇧^⋆"
    using 3 by simp
  also have "... = (top ⊓ (--v)⇧^T) * (w ⊓ -v⇧^T) * w⇧^⋆"
    by (simp add: conv_complement)
  also have "... = top * (w ⊓ --v ⊓ -v⇧^T) * w⇧^⋆"
    using assms(2) covector_inf_comp_3 inf_assoc inf_left_commute vector_complement_closed by presburger
  also have "... = top * (w ⊓ --v * -v⇧^T) * w⇧^⋆"
    by (metis assms(2) vector_complement_closed conv_complement inf_assoc vector_covector)
  finally have "top * (e⇧^T * top)⇧^T ≤ top * (w ⊓ --v * -v⇧^T) * w⇧^⋆"
    by (metis conv_dist_comp conv_involutive conv_top mult_assoc top_mult_top)
  hence "top ≤ top * (w ⊓ --v * -v⇧^T) * w⇧^⋆ * (e⇧^T * top)"
    using assms(6) shunt_bijective by blast
  also have "... = top * (w ⊓ --v * -v⇧^T) * (top * e * w⇧^⋆⇧^T)⇧^T"
    by (simp add: conv_dist_comp mult_assoc)
  also have "... = top * (w ⊓ --v * -v⇧^T ⊓ top * e * w⇧^⋆⇧^T) * top"
    by (simp add: comp_inf_vector_1 mult_assoc)
  finally show ?thesis
    by (simp add: conv_star_commute top_le)
qed

lemma arc_edge_5:
  assumes "vector v"
      and "w * v ≤ v"
      and "injective w"
      and "arc e"
    shows "(prim_E w v e)⇧^T * top * prim_E w v e ≤ 1"
proof -
  have 1: "e⇧^T * top * e ≤ 1"
    by (simp add: assms(4) point_injective)
  have "prim_E w v e ≤ --v * top"
    by (simp add: inf_commute le_infI2 mult_right_isotone)
  hence 2: "prim_E w v e ≤ --v"
    by (simp add: assms(1) vector_complement_closed)
  have 3: "w * --v ≤ --v"
    by (simp add: assms(2) p_antitone p_antitone_iff)
  have "w ⊓ top * prim_E w v e ≤ w * (prim_E w v e)⇧^T * prim_E w v e"
    by (metis dedekind_2 inf.commute inf_top.left_neutral)
  also have "... ≤ w * w⇧^T * prim_E w v e"
    by (simp add: conv_isotone le_infI1 mult_left_isotone mult_right_isotone)
  also have "... ≤ prim_E w v e"
    by (metis assms(3) mult_left_isotone mult_left_one)
  finally have 4: "w ⊓ top * prim_E w v e ≤ prim_E w v e"
    .
  have "w⇧⁺ ⊓ top * prim_E w v e = w⇧^⋆ * (w ⊓ top * prim_E w v e)"
    by (simp add: comp_inf_covector star_plus)
  also have "... ≤ w⇧^⋆ * prim_E w v e"
    using 4 by (simp add: mult_right_isotone)
  also have "... ≤ --v"
    using 2 3 star_left_induct sup.bounded_iff by blast
  finally have 5: "w⇧⁺ ⊓ top * prim_E w v e ⊓ -v = bot"
    using shunting_1_pp by blast
  hence 6: "w⇧⁺⇧^T ⊓ (prim_E w v e)⇧^T * top ⊓ -v⇧^T = bot"
    using conv_complement conv_dist_comp conv_dist_inf conv_top conv_bot by force
  have "(prim_E w v e)⇧^T * top * prim_E w v e ≤ (top * e * w⇧^T⇧^⋆)⇧^T * top * (top * e * w⇧^T⇧^⋆)"
    by (simp add: conv_isotone mult_isotone)
  also have "... = w⇧^⋆ * e⇧^T * top * e * w⇧^T⇧^⋆"
    by (metis conv_star_commute conv_dist_comp conv_involutive conv_top mult_assoc top_mult_top)
  also have "... ≤ w⇧^⋆ * w⇧^T⇧^⋆"
    using 1 by (metis mult_assoc mult_1_right mult_right_isotone mult_left_isotone)
  also have "... = w⇧^⋆ ⊔ w⇧^T⇧^⋆"
    by (metis assms(3) cancel_separate order.eq_iff star.circ_sup_sub_sup_one_1 star.circ_plus_one star_involutive)
  also have "... = w⇧⁺ ⊔ w⇧^T⇧⁺ ⊔ 1"
    by (metis star.circ_plus_one star_left_unfold_equal sup.assoc sup.commute)
  finally have 7: "(prim_E w v e)⇧^T * top * prim_E w v e ≤ w⇧⁺ ⊔ w⇧^T⇧⁺ ⊔ 1"
    .
  have "prim_E w v e ≤ --v * -v⇧^T"
    by (simp add: le_infI1)
  also have "... ≤ top * -v⇧^T"
    by (simp add: mult_left_isotone)
  also have "... = -v⇧^T"
    by (simp add: assms(1) vector_conv_compl)
  finally have 8: "prim_E w v e ≤ -v⇧^T"
    .
  hence 9: "(prim_E w v e)⇧^T ≤ -v"
    by (metis conv_complement conv_involutive conv_isotone)
  have "(prim_E w v e)⇧^T * top * prim_E w v e = (w⇧⁺ ⊔ w⇧^T⇧⁺ ⊔ 1) ⊓ (prim_E w v e)⇧^T * top * prim_E w v e"
    using 7 by (simp add: inf.absorb_iff2)
  also have "... = (1 ⊓ (prim_E w v e)⇧^T * top * prim_E w v e) ⊔ (w⇧⁺ ⊓ (prim_E w v e)⇧^T * top * prim_E w v e) ⊔ (w⇧^T⇧⁺ ⊓ (prim_E w v e)⇧^T * top * prim_E w v e)"
    using comp_inf.mult_right_dist_sup sup_assoc sup_commute by auto
  also have "... ≤ 1 ⊔ (w⇧⁺ ⊓ (prim_E w v e)⇧^T * top * prim_E w v e) ⊔ (w⇧^T⇧⁺ ⊓ (prim_E w v e)⇧^T * top * prim_E w v e)"
    using inf_le1 sup_left_isotone by blast
  also have "... ≤ 1 ⊔ (w⇧⁺ ⊓ (prim_E w v e)⇧^T * top * prim_E w v e) ⊔ (w⇧^T⇧⁺ ⊓ (prim_E w v e)⇧^T * top * -v⇧^T)"
    using 8 inf.sup_right_isotone mult_right_isotone sup_right_isotone by blast
  also have "... ≤ 1 ⊔ (w⇧⁺ ⊓ -v * top * prim_E w v e) ⊔ (w⇧^T⇧⁺ ⊓ (prim_E w v e)⇧^T * top * -v⇧^T)"
    using 9 by (metis inf.sup_right_isotone mult_left_isotone sup.commute sup_right_isotone)
  also have "... = 1 ⊔ (w⇧⁺ ⊓ -v * top ⊓ top * prim_E w v e) ⊔ (w⇧^T⇧⁺ ⊓ (prim_E w v e)⇧^T * top ⊓ top * -v⇧^T)"
    by (metis (no_types) vector_export_comp inf_top_right inf_assoc)
  also have "... = 1 ⊔ (w⇧⁺ ⊓ -v ⊓ top * prim_E w v e) ⊔ (w⇧^T⇧⁺ ⊓ (prim_E w v e)⇧^T * top ⊓ -v⇧^T)"
    using assms(1) vector_complement_closed vector_conv_compl by auto
  also have "... = 1"
    using 5 6 by (simp add: conv_star_commute conv_dist_comp inf.commute inf_assoc star.circ_plus_same)
  finally show ?thesis
    .
qed

lemma arc_edge_6:
  assumes "vector v"
      and "w * v ≤ v"
      and "injective w"
      and "arc e"
    shows "prim_E w v e * top * (prim_E w v e)⇧^T ≤ 1"
proof -
  have "prim_E w v e * 1 * (prim_E w v e)⇧^T ≤ w * w⇧^T"
    using comp_isotone conv_order inf.coboundedI1 mult_one_associative by auto
  also have "... ≤ 1"
    by (simp add: assms(3))
  finally have 1: "prim_E w v e * 1 * (prim_E w v e)⇧^T ≤ 1"
    .
  have "(prim_E w v e)⇧^T * top * prim_E w v e ≤ 1"
    by (simp add: assms arc_edge_5)
  also have "... ≤ --1"
    by (simp add: pp_increasing)
  finally have 2: "prim_E w v e * -1 * (prim_E w v e)⇧^T ≤ bot"
    by (metis conv_involutive regular_closed_bot regular_dense_top triple_schroeder_p)
  have "prim_E w v e * top * (prim_E w v e)⇧^T = prim_E w v e * 1 * (prim_E w v e)⇧^T ⊔ prim_E w v e * -1 * (prim_E w v e)⇧^T"
    by (metis mult_left_dist_sup mult_right_dist_sup regular_complement_top regular_one_closed)
  also have "... ≤ 1"
    using 1 2 by (simp add: bot_unique)
  finally show ?thesis
    .
qed

lemma arc_edge:
  assumes "e ≤ v * -v⇧^T ⊓ g"
      and "vector v"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "t ≤ g"
      and "r⇧^T * g⇧^⋆ ≤ r⇧^T * w⇧^⋆"
      and "w * v ≤ v"
      and "injective w"
      and "arc e"
    shows "arc (prim_E w v e)"
proof (intro conjI)
  have "prim_E w v e * top * (prim_E w v e)⇧^T ≤ 1"
    using assms(2,6-8) arc_edge_6 by simp
  thus "injective (prim_E w v e * top)"
    by (metis conv_dist_comp conv_top mult_assoc top_mult_top)
next
  show "surjective (prim_E w v e * top)"
    using assms(1-5,8) arc_edge_4 mult_assoc by simp
next
  have "(prim_E w v e)⇧^T * top * prim_E w v e ≤ 1"
    using assms(2,6-8) arc_edge_5 by simp
  thus "injective ((prim_E w v e)⇧^T * top)"
    by (metis conv_dist_comp conv_involutive conv_top mult_assoc top_mult_top)
next
  have "top * prim_E w v e * top = top"
    using assms(1-5,8) arc_edge_4 by simp
  thus "surjective ((prim_E w v e)⇧^T * top)"
    by (metis mult_assoc conv_dist_comp conv_top)
qed

subsubsection ‹Invariant implies Postcondition›

text ‹
The lemmas in this section are used to show that the invariant implies the postcondition at the end of the algorithm.
The following lemma shows that the nodes reachable in the graph are the same as those reachable in the constructed tree.
›

lemma span_post:
  assumes "regular v"
      and "vector v"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "v * -v⇧^T ⊓ g = bot"
      and "t ≤ v * v⇧^T ⊓ g"
      and "r⇧^T * (v * v⇧^T ⊓ g)⇧^⋆ ≤ r⇧^T * t⇧^⋆"
    shows "v⇧^T = r⇧^T * g⇧^⋆"
proof -
  let ?vv = "v * v⇧^T ⊓ g"
  have 1: "r⇧^T ≤ v⇧^T"
    using assms(3) mult_right_isotone mult_1_right star.circ_reflexive by fastforce
  have "v * top ⊓ g = (v * v⇧^T ⊔ v * -v⇧^T) ⊓ g"
    by (metis assms(1) conv_complement mult_left_dist_sup regular_complement_top)
  also have "... = ?vv ⊔ (v * -v⇧^T ⊓ g)"
    by (simp add: inf_sup_distrib2)
  also have "... = ?vv"
    by (simp add: assms(4))
  finally have 2: "v * top ⊓ g = ?vv"
    by simp
  have "r⇧^T * ?vv⇧^⋆ ≤ v⇧^T * ?vv⇧^⋆"
    using 1 by (simp add: comp_left_isotone)
  also have "... ≤ v⇧^T * (v * v⇧^T)⇧^⋆"
    by (simp add: comp_right_isotone star.circ_isotone)
  also have "... ≤ v⇧^T"
    by (simp add: assms(2) vector_star_1)
  finally have "r⇧^T * ?vv⇧^⋆ ≤ v⇧^T"
    by simp
  hence "r⇧^T * ?vv⇧^⋆ * g = (r⇧^T * ?vv⇧^⋆ ⊓ v⇧^T) * g"
    by (simp add: inf.absorb1)
  also have "... = r⇧^T * ?vv⇧^⋆ * (v * top ⊓ g)"
    by (simp add: assms(2) covector_inf_comp_3)
  also have "... = r⇧^T * ?vv⇧^⋆ * ?vv"
    using 2 by simp
  also have "... ≤ r⇧^T * ?vv⇧^⋆"
    by (simp add: comp_associative comp_right_isotone star.left_plus_below_circ star_plus)
  finally have "r⇧^T ⊔ r⇧^T * ?vv⇧^⋆ * g ≤ r⇧^T * ?vv⇧^⋆"
    using star.circ_back_loop_prefixpoint by auto
  hence "r⇧^T * g⇧^⋆ ≤ r⇧^T * ?vv⇧^⋆"
    using star_right_induct by blast
  hence "r⇧^T * g⇧^⋆ = r⇧^T * ?vv⇧^⋆"
    by (simp add: order.antisym mult_right_isotone star_isotone)
  also have "... = r⇧^T * t⇧^⋆"
    using assms(5,6) order.antisym mult_right_isotone star_isotone by auto
  also have "... = v⇧^T"
    by (simp add: assms(3))
  finally show ?thesis
    by simp
qed

text ‹
The following lemma shows that the minimum spanning tree extending a tree is the same as the tree at the end of the algorithm.
›

lemma mst_post:
  assumes "vector r"
      and "injective r"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "forest w"
      and "t ≤ w"
      and "w ≤ v * v⇧^T"
    shows "w = t"
proof -
  have 1: "vector v"
    using assms(1,3) covector_mult_closed vector_conv_covector by auto
  have "w * v ≤ v * v⇧^T * v"
    by (simp add: assms(6) mult_left_isotone)
  also have "... ≤ v"
    using 1 by (metis mult_assoc mult_right_isotone top_greatest)
  finally have 2: "w * v ≤ v"
    .
  have 3: "r ≤ v"
    by (metis assms(3) conv_order mult_right_isotone mult_1_right star.circ_reflexive)
  have 4: "v ⊓ -r = t⇧^T⇧^⋆ * r ⊓ -r"
    by (metis assms(3) conv_dist_comp conv_involutive conv_star_commute)
  also have "... = (r ⊔ t⇧^T⇧⁺ * r) ⊓ -r"
    using mult_assoc star.circ_loop_fixpoint sup_commute by auto
  also have "... ≤ t⇧^T⇧⁺ * r"
    by (simp add: shunting)
  also have "... ≤ t⇧^T * top"
    by (simp add: comp_isotone mult_assoc)
  finally have "1 ⊓ (v ⊓ -r) * (v ⊓ -r)⇧^T ≤ 1 ⊓ t⇧^T * top * (t⇧^T * top)⇧^T"
    using conv_order inf.sup_right_isotone mult_isotone by auto
  also have "... = 1 ⊓ t⇧^T * top * t"
    by (metis conv_dist_comp conv_involutive conv_top mult_assoc top_mult_top)
  also have "... ≤ t⇧^T * (top * t ⊓ t * 1)"
    by (metis conv_involutive dedekind_1 inf.commute mult_assoc)
  also have "... ≤ t⇧^T * t"
    by (simp add: mult_right_isotone)
  finally have 5: "1 ⊓ (v ⊓ -r) * (v ⊓ -r)⇧^T ≤ t⇧^T * t"
    .
  have "w * w⇧⁺ ≤ -1"
    by (metis assms(4) mult_right_isotone order_trans star.circ_increasing star.left_plus_circ)
  hence 6: "w⇧^T⇧⁺ ≤ -w"
    by (metis conv_star_commute mult_assoc mult_1_left triple_schroeder_p)
  have "w * r ⊓ w⇧^T⇧⁺ * r = (w ⊓ w⇧^T⇧⁺) * r"
    using assms(2) by (simp add: injective_comp_right_dist_inf)
  also have "... = bot"
    using 6 p_antitone pseudo_complement_pp semiring.mult_not_zero by blast
  finally have 7: "w * r ⊓ w⇧^T⇧⁺ * r = bot"
    .
  have "-1 * r ≤ -r"
    using assms(2) dual_order.trans pp_increasing schroeder_4_p by blast
  hence "-1 * r * top ≤ -r"
    by (simp add: assms(1) comp_associative)
  hence 8: "r⇧^T * -1 * r ≤ bot"
    by (simp add: mult_assoc schroeder_6_p)
  have "r⇧^T * w * r ≤ r⇧^T * w⇧⁺ * r"
    by (simp add: mult_left_isotone mult_right_isotone star.circ_mult_increasing)
  also have "... ≤ r⇧^T * -1 * r"
    by (simp add: assms(4) comp_isotone)
  finally have "r⇧^T * w * r ≤ bot"
    using 8 by simp
  hence "w * r * top ≤ -r"
    by (simp add: mult_assoc schroeder_6_p)
  hence "w * r ≤ -r"
    by (simp add: assms(1) comp_associative)
  hence "w * r ≤ -r ⊓ w * v"
    using 3 by (simp add: mult_right_isotone)
  also have "... ≤ -r ⊓ v"
    using 2 by (simp add: le_infI2)
  also have "... = -r ⊓ t⇧^T⇧^⋆ * r"
    using 4 by (simp add: inf_commute)
  also have "... ≤ -r ⊓ w⇧^T⇧^⋆ * r"
    using assms(5) comp_inf.mult_right_isotone conv_isotone mult_left_isotone star_isotone by auto
  also have "... = -r ⊓ (r ⊔ w⇧^T⇧⁺ * r)"
    using mult_assoc star.circ_loop_fixpoint sup_commute by auto
  also have "... ≤ w⇧^T⇧⁺ * r"
    using inf.commute maddux_3_13 by auto
  finally have "w * r = bot"
    using 7 by (simp add: le_iff_inf)
  hence "w = w ⊓ top * -r⇧^T"
    by (metis complement_conv_sub conv_dist_comp conv_involutive conv_bot inf.assoc inf.orderE regular_closed_bot regular_dense_top top_left_mult_increasing)
  also have "... = w ⊓ v * v⇧^T ⊓ top * -r⇧^T"
    by (simp add: assms(6) inf_absorb1)
  also have "... ≤ w ⊓ top * v⇧^T ⊓ top * -r⇧^T"
    using comp_inf.mult_left_isotone comp_inf.mult_right_isotone mult_left_isotone by auto
  also have "... = w ⊓ top * (v⇧^T ⊓ -r⇧^T)"
    using 1 assms(1) covector_inf_closed inf_assoc vector_conv_compl vector_conv_covector by auto
  also have "... = w * (1 ⊓ (v ⊓ -r) * top)"
    by (simp add: comp_inf_vector conv_complement conv_dist_inf)
  also have "... = w * (1 ⊓ (v ⊓ -r) * (v ⊓ -r)⇧^T)"
    by (metis conv_top dedekind_eq inf_commute inf_top_left mult_1_left mult_1_right)
  also have "... ≤ w * t⇧^T * t"
    using 5 by (simp add: comp_isotone mult_assoc)
  also have "... ≤ w * w⇧^T * t"
    by (simp add: assms(5) comp_isotone conv_isotone)
  also have "... ≤ t"
    using assms(4) mult_left_isotone mult_1_left by fastforce
  finally show ?thesis
    by (simp add: assms(5) order.antisym)
qed

subsection ‹Kruskal's Algorithm›

text ‹
The following results are used for proving the correctness of Kruskal's minimum spanning tree algorithm.
›

subsubsection ‹Preservation of Invariant›

text ‹
We first treat the preservation of the invariant.
The following lemmas show conditions necessary for preserving that ‹f› is a forest.
›

lemma kruskal_injective_inv_2:
  assumes "arc e"
      and "acyclic f"
    shows "top * e * f⇧^T⇧^⋆ * f⇧^T ≤ -e"
proof -
  have "f ≤ -f⇧^T⇧^⋆"
    using assms(2) acyclic_star_below_complement p_antitone_iff by simp
  hence "e * f ≤ top * e * -f⇧^T⇧^⋆"
    by (simp add: comp_isotone top_left_mult_increasing)
  also have "... = -(top * e * f⇧^T⇧^⋆)"
    by (metis assms(1) comp_mapping_complement conv_dist_comp conv_involutive conv_top)
  finally show ?thesis
    using schroeder_4_p by simp
qed

lemma kruskal_injective_inv_3:
  assumes "arc e"
      and "forest f"
    shows "(top * e * f⇧^T⇧^⋆)⇧^T * (top * e * f⇧^T⇧^⋆) ⊓ f⇧^T * f ≤ 1"
proof -
  have "(top * e * f⇧^T⇧^⋆)⇧^T * (top * e * f⇧^T⇧^⋆) = f⇧^⋆ * e⇧^T * top * e * f⇧^T⇧^⋆"
    by (metis conv_dist_comp conv_involutive conv_star_commute conv_top vector_top_closed mult_assoc)
  also have "... ≤ f⇧^⋆ * f⇧^T⇧^⋆"
    by (metis assms(1) arc_expanded mult_left_isotone mult_right_isotone mult_1_left mult_assoc)
  finally have "(top * e * f⇧^T⇧^⋆)⇧^T * (top * e * f⇧^T⇧^⋆) ⊓ f⇧^T * f ≤ f⇧^⋆ * f⇧^T⇧^⋆ ⊓ f⇧^T * f"
    using inf.sup_left_isotone by simp
  also have "... ≤ 1"
    using assms(2) forest_separate by simp
  finally show ?thesis
    by simp
qed

lemma kruskal_acyclic_inv:
  assumes "acyclic f"
      and "covector q"
      and "(f ⊓ q)⇧^T * f⇧^⋆ * e = bot"
      and "e * f⇧^⋆ * e = bot"
      and "f⇧^T⇧^⋆ * f⇧^⋆ ≤ -e"
    shows "acyclic ((f ⊓ -q) ⊔ (f ⊓ q)⇧^T ⊔ e)"
proof -
  have "(f ⊓ -q) * (f ⊓ q)⇧^T = (f ⊓ -q) * (f⇧^T ⊓ q⇧^T)"
    by (simp add: conv_dist_inf)
  hence 1: "(f ⊓ -q) * (f ⊓ q)⇧^T = bot"
    by (metis assms(2) comp_inf.semiring.mult_zero_right comp_inf_vector_1 conv_bot covector_bot_closed inf.sup_monoid.add_assoc p_inf)
  hence 2: "(f ⊓ -q)⇧^⋆ * (f ⊓ q)⇧^T = (f ⊓ q)⇧^T"
    using mult_right_zero star_absorb star_simulation_right_equal by fastforce
  hence 3: "((f ⊓ -q) ⊔ (f ⊓ q)⇧^T)⇧⁺ = (f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ q)⇧^T⇧⁺"
    by (simp add: plus_sup)
  have 4: "((f ⊓ -q) ⊔ (f ⊓ q)⇧^T)⇧^⋆ = (f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧^⋆"
    using 2 by (simp add: star.circ_sup_9)
  have "(f ⊓ q)⇧^T * (f ⊓ -q)⇧^⋆ * e ≤ (f ⊓ q)⇧^T * f⇧^⋆ * e"
    by (simp add: mult_left_isotone mult_right_isotone star_isotone)
  hence "(f ⊓ q)⇧^T * (f ⊓ -q)⇧^⋆ * e = bot"
    using assms(3) le_bot by simp
  hence 5: "(f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧^⋆ * e = (f ⊓ -q)⇧^⋆ * e"
    by (metis comp_associative conv_bot conv_dist_comp conv_involutive conv_star_commute star_absorb)
  have "e * (f ⊓ -q)⇧^⋆ * e ≤ e * f⇧^⋆ * e"
    by (simp add: mult_left_isotone mult_right_isotone star_isotone)
  hence "e * (f ⊓ -q)⇧^⋆ * e = bot"
    using assms(4) le_bot by simp
  hence 6: "((f ⊓ -q)⇧^⋆ * e)⇧⁺ = (f ⊓ -q)⇧^⋆ * e"
    by (simp add: comp_associative star_absorb)
  have "f⇧^T⇧^⋆ * 1 * f⇧^T⇧^⋆ * f⇧^⋆ ≤ -e"
    by (simp add: assms(5) star.circ_transitive_equal)
  hence 7: "f⇧^⋆ * e * f⇧^T⇧^⋆ * f⇧^⋆ ≤ -1"
    by (metis comp_right_one conv_involutive conv_one conv_star_commute triple_schroeder_p)
  have "(f ⊓ -q)⇧⁺ * (f ⊓ q)⇧^T⇧⁺ ≤ -1"
    using 1 2 by (metis forest_bot mult_left_zero mult_assoc)
  hence 8: "(f ⊓ q)⇧^T⇧⁺ * (f ⊓ -q)⇧⁺ ≤ -1"
    using comp_commute_below_diversity by simp
  have 9: "f⇧^T⇧⁺ ≤ -1"
    using assms(1) acyclic_star_below_complement schroeder_5_p by force
  have "((f ⊓ -q) ⊔ (f ⊓ q)⇧^T ⊔ e)⇧⁺ = (((f ⊓ -q) ⊔ (f ⊓ q)⇧^T)⇧^⋆ * e)⇧^⋆ * ((f ⊓ -q) ⊔ (f ⊓ q)⇧^T)⇧⁺ ⊔ (((f ⊓ -q) ⊔ (f ⊓ q)⇧^T)⇧^⋆ * e)⇧⁺"
    by (simp add: plus_sup)
  also have "... = ((f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧^⋆ * e)⇧^⋆ * ((f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ q)⇧^T⇧⁺) ⊔ ((f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧^⋆ * e)⇧⁺"
    using 3 4 by simp
  also have "... = ((f ⊓ -q)⇧^⋆ * e)⇧^⋆ * ((f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ q)⇧^T⇧⁺) ⊔ ((f ⊓ -q)⇧^⋆ * e)⇧⁺"
    using 5 by simp
  also have "... = ((f ⊓ -q)⇧^⋆ * e ⊔ 1) * ((f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ q)⇧^T⇧⁺) ⊔ (f ⊓ -q)⇧^⋆ * e"
    using 6 by (metis star_left_unfold_equal sup_monoid.add_commute)
  also have "... = (f ⊓ -q)⇧^⋆ * e ⊔ (f ⊓ -q)⇧^⋆ * e * (f ⊓ q)⇧^T⇧⁺ ⊔ (f ⊓ -q)⇧^⋆ * e * (f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ q)⇧^T⇧⁺"
    using comp_associative mult_left_dist_sup mult_right_dist_sup sup_assoc sup_commute by simp
  also have "... = (f ⊓ -q)⇧^⋆ * e * (f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧^⋆ ⊔ (f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ q)⇧^T⇧⁺"
    by (metis star.circ_back_loop_fixpoint star_plus sup_monoid.add_commute mult_assoc)
  also have "... ≤ f⇧^⋆ * e * f⇧^T⇧^⋆ * (f ⊓ -q)⇧^⋆ ⊔ (f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ q)⇧^T⇧⁺"
    using mult_left_isotone mult_right_isotone star_isotone sup_left_isotone conv_isotone order_trans inf_le1 by meson
  also have "... ≤ f⇧^⋆ * e * f⇧^T⇧^⋆ * f⇧^⋆ ⊔ (f ⊓ q)⇧^T⇧^⋆ * (f ⊓ -q)⇧⁺ ⊔ f⇧^T⇧⁺"
    using mult_left_isotone mult_right_isotone star_isotone sup_left_isotone sup_right_isotone conv_isotone order_trans inf_le1 by meson
  also have "... = f⇧^⋆ * e * f⇧^T⇧^⋆ * f⇧^⋆ ⊔ (f ⊓ q)⇧^T⇧⁺ * (f ⊓ -q)⇧⁺ ⊔ (f ⊓ -q)⇧⁺ ⊔ f⇧^T⇧⁺"
    by (simp add: star.circ_loop_fixpoint sup_monoid.add_assoc mult_assoc)
  also have "... ≤ f⇧^⋆ * e * f⇧^T⇧^⋆ * f⇧^⋆ ⊔ (f ⊓ q)⇧^T⇧⁺ * (f ⊓ -q)⇧⁺ ⊔ f⇧⁺ ⊔ f⇧^T⇧⁺"
    using mult_left_isotone mult_right_isotone star_isotone sup_left_isotone sup_right_isotone order_trans inf_le1 by meson
  also have "... ≤ -1"
    using 7 8 9 assms(1) by simp
  finally show ?thesis
    by simp
qed

lemma kruskal_exchange_acyclic_inv_1:
  assumes "acyclic f"
      and "covector q"
    shows "acyclic ((f ⊓ -q) ⊔ (f ⊓ q)⇧^T)"
  using kruskal_acyclic_inv[where e=bot] by (simp add: assms)

lemma kruskal_exchange_acyclic_inv_2:
  assumes "acyclic w"
      and "injective w"
      and "d ≤ w"
      and "bijective (d⇧^T * top)"
      and "bijective (e * top)"
      and "d ≤ top * e⇧^T * w⇧^T⇧^⋆"
      and "w * e⇧^T * top = bot"
    shows "acyclic ((w ⊓ -d) ⊔ e)"
proof -
  let ?v = "w ⊓ -d"
  let ?w = "?v ⊔ e"
  have "d⇧^T * top ≤ w⇧^⋆ * e * top"
    by (metis assms(6) comp_associative comp_inf.star.circ_decompose_9 comp_inf.star_star_absorb comp_isotone conv_dist_comp conv_involutive conv_order conv_star_commute conv_top inf.cobounded1 vector_top_closed)
  hence 1: "e * top ≤ w⇧^T⇧^⋆ * d⇧^T * top"
    by (metis assms(4,5) bijective_reverse comp_associative conv_star_commute)
  have 2: "?v * d⇧^T * top = bot"
    by (simp add: assms(2,3) kruskal_exchange_acyclic_inv_3)
  have "?v * w⇧^T⇧⁺ * d⇧^T * top ≤ w * w⇧^T⇧⁺ * d⇧^T * top"
    by (simp add: mult_left_isotone)
  also have "... ≤ w⇧^T⇧^⋆ * d⇧^T * top"
    by (metis assms(2) mult_left_isotone mult_1_left mult_assoc)
  finally have "?v * w⇧^T⇧^⋆ * d⇧^T * top ≤ w⇧^T⇧^⋆ * d⇧^T * top"
    using 2 by (metis bot_least comp_associative mult_right_dist_sup star.circ_back_loop_fixpoint star.circ_plus_same sup_least)
  hence 3: "?v⇧^⋆ * e * top ≤ w⇧^T⇧^⋆ * d⇧^T * top"
    using 1 by (simp add: comp_associative star_left_induct sup_least)
  have "d * e⇧^T ≤ bot"
    by (metis assms(3,7) conv_bot conv_dist_comp conv_involutive conv_top order.trans inf.absorb2 inf.cobounded2 inf_commute le_bot p_antitone_iff p_top schroeder_4_p top_left_mult_increasing)
  hence 4: "e⇧^T * top ≤ -(d⇧^T * top)"
    by (metis (no_types) comp_associative inf.cobounded2 le_bot p_antitone_iff schroeder_3_p semiring.mult_zero_left)
  have "?v⇧^T * -(d⇧^T * top) ≤ -(d⇧^T * top)"
    using schroeder_3_p mult_assoc 2 by simp
  hence "?v⇧^T⇧^⋆ * e⇧^T * top ≤ -(d⇧^T * top)"
    using 4 by (simp add: comp_associative star_left_induct sup_least)
  hence 5: "d⇧^T * top ≤ -(?v⇧^T⇧^⋆ * e⇧^T * top)"
    by (simp add: p_antitone_iff)
  have "w * ?v⇧^T⇧^⋆ * e⇧^T * top = w * e⇧^T * top ⊔ w * ?v⇧^T⇧⁺ * e⇧^T * top"
    by (metis star_left_unfold_equal mult_right_dist_sup mult_left_dist_sup mult_1_right mult_assoc)
  also have "... = w * ?v⇧^T⇧⁺ * e⇧^T * top"
    using assms(7) by simp
  also have "... ≤ w * w⇧^T * ?v⇧^T⇧^⋆ * e⇧^T * top"
    by (simp add: comp_associative conv_isotone mult_left_isotone mult_right_isotone)
  also have "... ≤ ?v⇧^T⇧^⋆ * e⇧^T * top"
    by (metis assms(2) mult_1_left mult_left_isotone)
  finally have "w * ?v⇧^T⇧^⋆ * e⇧^T * top ≤ --(?v⇧^T⇧^⋆ * e⇧^T * top)"
    by (simp add: p_antitone p_antitone_iff)
  hence "w⇧^T * -(?v⇧^T⇧^⋆ * e⇧^T * top) ≤ -(?v⇧^T⇧^⋆ * e⇧^T * top)"
    using comp_associative schroeder_3_p by simp
  hence 6: "w⇧^T⇧^⋆ * d⇧^T * top ≤ -(?v⇧^T⇧^⋆ * e⇧^T * top)"
    using 5 by (simp add: comp_associative star_left_induct sup_least)
  have "e * ?v⇧^⋆ * e ≤ e * ?v⇧^⋆ * e * top"
    by (simp add: top_right_mult_increasing)
  also have "... ≤ e * w⇧^T⇧^⋆ * d⇧^T * top"
    using 3 by (simp add: comp_associative mult_right_isotone)
  also have "... ≤ e * -(?v⇧^T⇧^⋆ * e⇧^T * top)"
    using 6 by (simp add: comp_associative mult_right_isotone)
  also have "... ≤ bot"
    by (metis conv_complement_sub_leq conv_dist_comp conv_involutive conv_star_commute le_bot mult_right_sub_dist_sup_right p_bot regular_closed_bot star.circ_back_loop_fixpoint)
  finally have 7: "e * ?v⇧^⋆ * e = bot"
    by (simp add: order.antisym)
  hence "?v⇧^⋆ * e ≤ -1"
    by (metis bot_least comp_associative comp_commute_below_diversity ex231d order_lesseq_imp semiring.mult_zero_left star.circ_left_top)
  hence 8: "?v⇧^⋆ * e * ?v⇧^⋆ ≤ -1"
    by (metis comp_associative comp_commute_below_diversity star.circ_transitive_equal)
  have "1 ⊓ ?w⇧⁺ = 1 ⊓ ?w * ?v⇧^⋆ * (e * ?v⇧^⋆)⇧^⋆"
    by (simp add: star_sup_1 mult_assoc)
  also have "... = 1 ⊓ ?w * ?v⇧^⋆ * (e * ?v⇧^⋆ ⊔ 1)"
    using 7 by (metis star.circ_mult_1 star_absorb sup_monoid.add_commute mult_assoc)
  also have "... = 1 ⊓ (?v⇧⁺ * e * ?v⇧^⋆ ⊔ ?v⇧⁺ ⊔ e * ?v⇧^⋆ * e * ?v⇧^⋆ ⊔ e * ?v⇧^⋆)"
    by (simp add: comp_associative mult_left_dist_sup mult_right_dist_sup sup_assoc sup_commute sup_left_commute)
  also have "... = 1 ⊓ (?v⇧⁺ * e * ?v⇧^⋆ ⊔ ?v⇧⁺ ⊔ e * ?v⇧^⋆)"
    using 7 by simp
  also have "... = 1 ⊓ (?v⇧^⋆ * e * ?v⇧^⋆ ⊔ ?v⇧⁺)"
    by (metis (mono_tags, opaque_lifting) comp_associative star.circ_loop_fixpoint sup_assoc sup_commute)
  also have "... ≤ 1 ⊓ (?v⇧^⋆ * e * ?v⇧^⋆ ⊔ w⇧⁺)"
    using comp_inf.mult_right_isotone comp_isotone semiring.add_right_mono star_isotone sup_commute by simp
  also have "... = (1 ⊓ ?v⇧^⋆ * e * ?v⇧^⋆) ⊔ (1 ⊓ w⇧⁺)"
    by (simp add: inf_sup_distrib1)
  also have "... = 1 ⊓ ?v⇧^⋆ * e * ?v⇧^⋆"
    by (metis assms(1) inf_commute pseudo_complement sup_bot_right)
  also have "... = bot"
    using 8 p_antitone_iff pseudo_complement by simp
  finally show ?thesis
    using le_bot p_antitone_iff pseudo_complement by auto
qed

subsubsection ‹Exchange gives Spanning Trees›

text ‹
The lemmas in this section are used to show that the relation after exchange represents a spanning tree.
›

lemma inf_star_import:
  assumes "x ≤ z"
      and "univalent z"
      and "reflexive y"
      and "regular z"
    shows "x⇧^⋆ * y ⊓ z⇧^⋆ ≤ x⇧^⋆ * (y ⊓ z⇧^⋆)"
proof -
  have 1: "y ≤ x⇧^⋆ * (y ⊓ z⇧^⋆) ⊔ -z⇧^⋆"
    by (metis assms(4) pp_dist_star shunting_var_p star.circ_loop_fixpoint sup.cobounded2)
  have "x * -z⇧^⋆ ⊓ z⇧⁺ ≤ x * (-z⇧^⋆ ⊓ x⇧^T * z⇧⁺)"
    by (simp add: dedekind_1)
  also have "... ≤ x * (-z⇧^⋆ ⊓ z⇧^T * z⇧⁺)"
    using assms(1) comp_inf.mult_right_isotone conv_isotone mult_left_isotone mult_right_isotone by simp
  also have "... ≤ x * (-z⇧^⋆ ⊓ 1 * z⇧^⋆)"
    by (metis assms(2) comp_associative comp_inf.mult_right_isotone mult_left_isotone mult_right_isotone)
  finally have 2: "x * -z⇧^⋆ ⊓ z⇧⁺ = bot"
    by (simp add: order.antisym)
  have "x * -z⇧^⋆ ⊓ z⇧^⋆ = (x * -z⇧^⋆ ⊓ z⇧⁺) ⊔ (x * -z⇧^⋆ ⊓ 1)"
    by (metis comp_inf.semiring.distrib_left star_left_unfold_equal sup_commute)
  also have "... ≤ x⇧^⋆ * (y ⊓ z⇧^⋆)"
    using 2 by (simp add: assms(3) inf.coboundedI2 reflexive_mult_closed star.circ_reflexive)
  finally have "x * -z⇧^⋆ ≤ x⇧^⋆ * (y ⊓ z⇧^⋆) ⊔ -z⇧^⋆"
    by (metis assms(4) pp_dist_star shunting_var_p)
  hence "x * (x⇧^⋆ * (y ⊓ z⇧^⋆) ⊔ -z⇧^⋆) ≤ x⇧^⋆ * (y ⊓ z⇧^⋆) ⊔ -z⇧^⋆"
    by (metis le_supE le_supI mult_left_dist_sup star.circ_loop_fixpoint sup.cobounded1)
  hence "x⇧^⋆ * y ≤ x⇧^⋆ * (y ⊓ z⇧^⋆) ⊔ -z⇧^⋆"
    using 1 by (simp add: star_left_induct)
  hence "x⇧^⋆ * y ⊓ --z⇧^⋆ ≤ x⇧^⋆ * (y ⊓ z⇧^⋆)"
    using shunting_var_p by simp
  thus ?thesis
    using order.trans inf.sup_right_isotone pp_increasing by blast
qed

lemma kruskal_exchange_forest_components_inv:
  assumes "injective ((w ⊓ -d) ⊔ e)"
      and "regular d"
      and "e * top * e = e"
      and "d ≤ top * e⇧^T * w⇧^T⇧^⋆"
      and "w * e⇧^T * top = bot"
      and "injective w"
      and "d ≤ w"
      and "d ≤ (w ⊓ -d)⇧^T⇧^⋆ * e⇧^T * top"
    shows "forest_components w ≤ forest_components ((w ⊓ -d) ⊔ e)"
proof -
  let ?v = "w ⊓ -d"
  let ?w = "?v ⊔ e"
  let ?f = "forest_components ?w"
  have 1: "?v * d⇧^T * top = bot"
    by (simp add: assms(6,7) kruskal_exchange_acyclic_inv_3)
  have 2: "d * e⇧^T ≤ bot"
    by (metis assms(5,7) conv_bot conv_dist_comp conv_involutive conv_top order.trans inf.absorb2 inf.cobounded2 inf_commute le_bot p_antitone_iff p_top schroeder_4_p top_left_mult_increasing)
  have "w⇧^⋆ * e⇧^T * top = e⇧^T * top"
    by (metis assms(5) conv_bot conv_dist_comp conv_involutive conv_star_commute star.circ_top star_absorb)
  hence "w⇧^⋆ * e⇧^T * top ≤ -(d⇧^T * top)"
    using 2 by (metis (no_types) comp_associative inf.cobounded2 le_bot p_antitone_iff schroeder_3_p semiring.mult_zero_left)
  hence 3: "e⇧^T * top ≤ -(w⇧^T⇧^⋆ * d⇧^T * top)"
    by (metis conv_star_commute p_antitone_iff schroeder_3_p mult_assoc)
  have "?v * w⇧^T⇧^⋆ * d⇧^T * top = ?v * d⇧^T * top ⊔ ?v * w⇧^T⇧⁺ * d⇧^T * top"
    by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint sup_commute)
  also have "... ≤ w * w⇧^T⇧⁺ * d⇧^T * top"
    using 1 by (simp add: mult_left_isotone)
  also have "... ≤ w⇧^T⇧^⋆ * d⇧^T * top"
    by (metis assms(6) mult_assoc mult_1_left mult_left_isotone)
  finally have "?v * w⇧^T⇧^⋆ * d⇧^T * top ≤ --(w⇧^T⇧^⋆ * d⇧^T * top)"
    using p_antitone p_antitone_iff by auto
  hence 4: "?v⇧^T * -(w⇧^T⇧^⋆ * d⇧^T * top) ≤ -(w⇧^T⇧^⋆ * d⇧^T * top)"
    using comp_associative schroeder_3_p by simp
  have 5: "injective ?v"
    using assms(1) conv_dist_sup mult_left_dist_sup mult_right_dist_sup by simp
  have "?v * ?v⇧^T⇧^⋆ * e⇧^T * top = ?v * e⇧^T * top ⊔ ?v * ?v⇧^T⇧⁺ * e⇧^T * top"
    by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint sup_commute)
  also have "... ≤ w * e⇧^T * top ⊔ ?v * ?v⇧^T⇧⁺ * e⇧^T * top"
    using mult_left_isotone sup_left_isotone by simp
  also have "... ≤ w * e⇧^T * top ⊔ ?v⇧^T⇧^⋆ * e⇧^T * top"
    using 5 by (metis mult_assoc mult_1_left mult_left_isotone sup_right_isotone)
  finally have "?v * ?v⇧^T⇧^⋆ * e⇧^T * top ≤ ?v⇧^T⇧^⋆ * e⇧^T * top"
    by (simp add: assms(5))
  hence "?v⇧^⋆ * d * top ≤ ?v⇧^T⇧^⋆ * e⇧^T * top"
    by (metis assms(8) star_left_induct sup_least comp_associative mult_right_sub_dist_sup_right sup.orderE vector_top_closed)
  also have "... ≤ -(w⇧^T⇧^⋆ * d⇧^T * top)"
    using 3 4 by (simp add: comp_associative star_left_induct)
  also have "... ≤ -(d⇧^T * top)"
    by (metis p_antitone star.circ_left_top star_outer_increasing mult_assoc)
  finally have 6: "?v⇧^⋆ * d * top ≤ -(d⇧^T * top)"
    by simp
  have "d⇧^T * top ≤ w⇧^⋆ * e * top"
    by (metis assms(4) comp_associative comp_inf.star.circ_sup_2 comp_isotone conv_dist_comp conv_involutive conv_order conv_star_commute conv_top vector_top_closed)
  also have "... ≤ (?v ⊔ d)⇧^⋆ * e * top"
    by (metis assms(2) comp_inf.semiring.distrib_left maddux_3_11_pp mult_left_isotone star_isotone sup.cobounded2 sup_commute sup_inf_distrib1)
  also have "... = ?v⇧^⋆ * (d * ?v⇧^⋆)⇧^⋆ * e * top"
    by (simp add: star_sup_1)
  also have "... = ?v⇧^⋆ * e * top ⊔ ?v⇧^⋆ * d * ?v⇧^⋆ * (d * ?v⇧^⋆)⇧^⋆ * e * top"
    by (metis semiring.distrib_right star.circ_unfold_sum star_decompose_1 star_decompose_3 mult_assoc)
  also have "... ≤ ?v⇧^⋆ * e * top ⊔ ?v⇧^⋆ * d * top"
    by (metis comp_associative comp_isotone le_supI mult_left_dist_sup mult_right_dist_sup mult_right_isotone star.circ_decompose_5 star_decompose_3 sup.cobounded1 sup_commute top.extremum)
  finally have "d⇧^T * top ≤ ?v⇧^⋆ * e * top ⊔ (d⇧^T * top ⊓ ?v⇧^⋆ * d * top)"
    using sup_inf_distrib2 sup_monoid.add_commute by simp
  hence "d⇧^T * top ≤ ?v⇧^⋆ * e * top"
    using 6 by (metis inf_commute pseudo_complement sup_monoid.add_0_right)
  hence 7: "d ≤ top * e⇧^T * ?v⇧^T⇧^⋆"
    by (metis comp_associative conv_dist_comp conv_involutive conv_isotone conv_star_commute conv_top order.trans top_right_mult_increasing)
  have 8: "?v ≤ ?f"
    using forest_components_increasing le_supE by blast
  have "d ≤ ?v⇧^T⇧^⋆ * e⇧^T * top ⊓ top * e⇧^T * ?v⇧^T⇧^⋆"
    using 7 assms(8) by simp
  also have "... = ?v⇧^T⇧^⋆ * e⇧^T * top * e⇧^T * ?v⇧^T⇧^⋆"
    by (metis inf_top_right vector_inf_comp vector_top_closed mult_assoc)
  also have "... = ?v⇧^T⇧^⋆ * e⇧^T * ?v⇧^T⇧^⋆"
    by (metis assms(3) comp_associative conv_dist_comp conv_top)
  also have "... ≤ ?v⇧^T⇧^⋆ * e⇧^T * ?f"
    using 8 by (metis assms(1) forest_components_equivalence cancel_separate_1 conv_dist_comp conv_order mult_left_isotone star_involutive star_isotone)
  also have "... ≤ ?v⇧^T⇧^⋆ * ?f * ?f"
    by (metis assms(1) forest_components_equivalence forest_components_increasing conv_isotone le_supE mult_left_isotone mult_right_isotone)
  also have "... ≤ ?f * ?f * ?f"
    by (metis comp_associative comp_isotone conv_dist_sup star.circ_loop_fixpoint star_isotone sup.cobounded1 sup.cobounded2)
  also have "... = ?f"
    by (simp add: assms(1) forest_components_equivalence preorder_idempotent)
  finally have "w ≤ ?f"
    using 8 by (metis assms(2) shunting_var_p sup.orderE)
  thus ?thesis
    using assms(1) forest_components_idempotent forest_components_isotone by fastforce
qed

lemma kruskal_spanning_inv:
  assumes "injective ((f ⊓ -q) ⊔ (f ⊓ q)⇧^T ⊔ e)"
      and "regular q"
      and "regular e"
      and "(-h ⊓ --g)⇧^⋆ ≤ forest_components f"
    shows "components (-(h ⊓ -e ⊓ -e⇧^T) ⊓ g) ≤ forest_components ((f ⊓ -q) ⊔ (f ⊓ q)⇧^T ⊔ e)"
proof -
  let ?f = "(f ⊓ -q) ⊔ (f ⊓ q)⇧^T ⊔ e"
  let ?h = "h ⊓ -e ⊓ -e⇧^T"
  let ?F = "forest_components f"
  let ?FF = "forest_components ?f"
  have 1: "equivalence ?FF"
    using assms(1) forest_components_equivalence by simp
  hence 2: "?f * ?FF ≤ ?FF"
    using order.trans forest_components_increasing mult_left_isotone by blast
  have 3: "?f⇧^T * ?FF ≤ ?FF"
    using 1 by (metis forest_components_increasing mult_left_isotone conv_isotone preorder_idempotent)
  have "(f ⊓ q) * ?FF ≤ ?f⇧^T * ?FF"
    using conv_dist_sup conv_involutive sup_assoc sup_left_commute mult_left_isotone by simp
  hence 4: "(f ⊓ q) * ?FF ≤ ?FF"
    using 3 order.trans by blast
  have "(f ⊓ -q) * ?FF ≤ ?f * ?FF"
    using le_supI1 mult_left_isotone by simp
  hence "(f ⊓ -q) * ?FF ≤ ?FF"
    using 2 order.trans by blast
  hence "((f ⊓ q) ⊔ (f ⊓ -q)) * ?FF ≤ ?FF"
    using 4 mult_right_dist_sup by simp
  hence "f * ?FF ≤ ?FF"
    by (metis assms(2) maddux_3_11_pp)
  hence 5: "f⇧^⋆ * ?FF ≤ ?FF"
    using star_left_induct_mult_iff by simp
  have "(f ⊓ -q)⇧^T * ?FF ≤ ?f⇧^T * ?FF"
    by (meson conv_isotone order.trans mult_left_isotone sup.cobounded1)
  hence 6: "(f ⊓ -q)⇧^T * ?FF ≤ ?FF"
    using 3 order.trans by blast
  have "(f ⊓ q)⇧^T * ?FF ≤ ?f * ?FF"
    by (simp add: mult_left_isotone sup.left_commute sup_assoc)
  hence "(f ⊓ q)⇧^T * ?FF ≤ ?FF"
    using 2 order.trans by blast
  hence "((f ⊓ -q)⇧^T ⊔ (f ⊓ q)⇧^T) * ?FF ≤ ?FF"
    using 6 mult_right_dist_sup by simp
  hence "f⇧^T * ?FF ≤ ?FF"
    by (metis assms(2) conv_dist_sup maddux_3_11_pp)
  hence 7: "?F * ?FF ≤ ?FF"
    using 5 star_left_induct mult_assoc by simp
  have 8: "e * ?FF ≤ ?FF"
    using 2 by (simp add: mult_right_dist_sup mult_left_isotone)
  have "e⇧^T * ?FF ≤ ?f⇧^T * ?FF"
    by (simp add: mult_left_isotone conv_isotone)
  also have "... ≤ ?FF * ?FF"
    using 1 by (metis forest_components_increasing mult_left_isotone conv_isotone)
  finally have "e⇧^T * ?FF ≤ ?FF"
    using 1 preorder_idempotent by auto
  hence 9: "(?F ⊔ e ⊔ e⇧^T) * ?FF ≤ ?FF"
    using 7 8 mult_right_dist_sup by simp
  have "components (-?h ⊓ g) ≤ ((-h ⊓ --g) ⊔ e ⊔ e⇧^T)⇧^⋆"
    by (metis assms(3) comp_inf.mult_left_sub_dist_sup_left conv_complement p_dist_inf pp_dist_inf regular_closed_p star_isotone sup_inf_distrib2 sup_monoid.add_assoc)
  also have "... ≤ ((-h ⊓ --g)⇧^⋆ ⊔ e ⊔ e⇧^T)⇧^⋆"
    using star.circ_increasing star_isotone sup_left_isotone by simp
  also have "... ≤ (?F ⊔ e ⊔ e⇧^T)⇧^⋆"
    using assms(4) sup_left_isotone star_isotone by simp
  also have "... ≤ ?FF"
    using 1 9 star_left_induct by force
  finally show ?thesis
    by simp
qed

lemma kruskal_exchange_spanning_inv_1:
  assumes "injective ((w ⊓ -q) ⊔ (w ⊓ q)⇧^T)"
      and "regular (w ⊓ q)"
      and "components g ≤ forest_components w"
    shows "components g ≤ forest_components ((w ⊓ -q) ⊔ (w ⊓ q)⇧^T)"
proof -
  let ?p = "w ⊓ q"
  let ?w = "(w ⊓ -q) ⊔ ?p⇧^T"
  have 1: "w ⊓ -?p ≤ forest_components ?w"
    by (metis forest_components_increasing inf_import_p le_supE)
  have "w ⊓ ?p ≤ ?w⇧^T"
    by (simp add: conv_dist_sup)
  also have "... ≤ forest_components ?w"
    by (metis assms(1) conv_isotone forest_components_equivalence forest_components_increasing)
  finally have "w ⊓ (?p ⊔ -?p) ≤ forest_components ?w"
    using 1 inf_sup_distrib1 by simp
  hence "w ≤ forest_components ?w"
    by (metis assms(2) inf_top_right stone)
  hence 2: "w⇧^⋆ ≤ forest_components ?w"
    using assms(1) star_isotone forest_components_star by force
  hence 3: "w⇧^T⇧^⋆ ≤ forest_components ?w"
    using assms(1) conv_isotone conv_star_commute forest_components_equivalence by force
  have "components g ≤ forest_components w"
    using assms(3) by simp
  also have "... ≤ forest_components ?w * forest_components ?w"
    using 2 3 mult_isotone by simp
  also have "... = forest_components ?w"
    using assms(1) forest_components_equivalence preorder_idempotent by simp
  finally show ?thesis
    by simp
qed

lemma kruskal_exchange_spanning_inv_2:
  assumes "injective w"
      and "w⇧^⋆ * e⇧^T = e⇧^T"
      and "f ⊔ f⇧^T ≤ (w ⊓ -d ⊓ -d⇧^T) ⊔ (w⇧^T ⊓ -d ⊓ -d⇧^T)"
      and "d ≤ forest_components f * e⇧^T * top"
    shows "d ≤ (w ⊓ -d)⇧^T⇧^⋆ * e⇧^T * top"
proof -
  have 1: "(w ⊓ -d ⊓ -d⇧^T) * (w⇧^T ⊓ -d ⊓ -d⇧^T) ≤ 1"
    using assms(1) comp_isotone order.trans inf.cobounded1 by blast
  have "d ≤ forest_components f * e⇧^T * top"
    using assms(4) by simp
  also have "... ≤ (f ⊔ f⇧^T)⇧^⋆ * (f ⊔ f⇧^T)⇧^⋆ * e⇧^T * top"
    by (simp add: comp_isotone star_isotone)
  also have "... = (f ⊔ f⇧^T)⇧^⋆ * e⇧^T * top"
    by (simp add: star.circ_transitive_equal)
  also have "... ≤ ((w ⊓ -d ⊓ -d⇧^T) ⊔ (w⇧^T ⊓ -d ⊓ -d⇧^T))⇧^⋆ * e⇧^T * top"
    using assms(3) by (simp add: comp_isotone star_isotone)
  also have "... = (w⇧^T ⊓ -d ⊓ -d⇧^T)⇧^⋆ * (w ⊓ -d ⊓ -d⇧^T)⇧^⋆ * e⇧^T * top"
    using 1 cancel_separate_1 by simp
  also have "... ≤ (w⇧^T ⊓ -d ⊓ -d⇧^T)⇧^⋆ * w⇧^⋆ * e⇧^T * top"
    by (simp add: inf_assoc mult_left_isotone mult_right_isotone star_isotone)
  also have "... = (w⇧^T ⊓ -d ⊓ -d⇧^T)⇧^⋆ * e⇧^T * top"
    using assms(2) mult_assoc by simp
  also have "... ≤ (w⇧^T ⊓ -d⇧^T)⇧^⋆ * e⇧^T * top"
    using mult_left_isotone conv_isotone star_isotone comp_inf.mult_right_isotone inf.cobounded2 inf.left_commute inf.sup_monoid.add_commute by presburger
  also have "... = (w ⊓ -d)⇧^T⇧^⋆ * e⇧^T * top"
    using conv_complement conv_dist_inf by presburger
  finally show ?thesis
    by simp
qed

lemma kruskal_spanning_inv_1:
  assumes "e ≤ F"
      and "regular e"
      and "components (-h ⊓ g) ≤ F"
      and "equivalence F"
    shows "components (-(h ⊓ -e ⊓ -e⇧^T) ⊓ g) ≤ F"
proof -
  have 1: "F * F ≤ F"
    using assms(4) by simp
  hence 2: "e * F ≤ F"
    using assms(1) mult_left_isotone order_lesseq_imp by blast
  have "e⇧^T * F ≤ F"
    by (metis assms(1,4) conv_isotone mult_left_isotone preorder_idempotent)
  hence 3: "(F ⊔ e ⊔ e⇧^T) * F ≤ F"
    using 1 2 mult_right_dist_sup by simp
  have "components (-(h ⊓ -e ⊓ -e⇧^T) ⊓ g) ≤ ((-h ⊓ --g) ⊔ e ⊔ e⇧^T)⇧^⋆"
    by (metis assms(2) comp_inf.mult_left_sub_dist_sup_left conv_complement p_dist_inf pp_dist_inf regular_closed_p star_isotone sup_inf_distrib2 sup_monoid.add_assoc)
  also have "... ≤ ((-h ⊓ --g)⇧^⋆ ⊔ e ⊔ e⇧^T)⇧^⋆"
    using sup_left_isotone star.circ_increasing star_isotone by simp
  also have "... ≤ (F ⊔ e ⊔ e⇧^T)⇧^⋆"
    using assms(3) sup_left_isotone star_isotone by simp
  also have "... ≤ F"
    using 3 assms(4) star_left_induct by force
  finally show ?thesis
    by simp
qed

lemma kruskal_reroot_edge:
  assumes "injective (e⇧^T * top)"
      and "acyclic w"
    shows "((w ⊓ -(top * e * w⇧^T⇧^⋆)) ⊔ (w ⊓ top * e * w⇧^T⇧^⋆)⇧^T) * e⇧^T = bot"
proof -
  let ?q = "top * e * w⇧^T⇧^⋆"
  let ?p = "w ⊓ ?q"
  let ?w = "(w ⊓ -?q) ⊔ ?p⇧^T"
  have "(w ⊓ -?q) * e⇧^T * top = w * (e⇧^T * top ⊓ -?q⇧^T)"
    by (metis comp_associative comp_inf_vector_1 conv_complement covector_complement_closed vector_top_closed)
  also have "... = w * (e⇧^T * top ⊓ -(w⇧^⋆ * e⇧^T * top))"
    by (simp add: conv_dist_comp conv_star_commute mult_assoc)
  also have "... = bot"
    by (metis comp_associative comp_inf.semiring.mult_not_zero inf.sup_relative_same_increasing inf_p mult_right_zero star.circ_loop_fixpoint sup_commute sup_left_divisibility)
  finally have 1: "(w ⊓ -?q) * e⇧^T * top = bot"
    by simp
  have "?p⇧^T * e⇧^T * top = (w⇧^T ⊓ w⇧^⋆ * e⇧^T * top) * e⇧^T * top"
    by (simp add: conv_dist_comp conv_star_commute mult_assoc conv_dist_inf)
  also have "... = w⇧^⋆ * e⇧^T * top ⊓ w⇧^T * e⇧^T * top"
    by (simp add: inf_vector_comp vector_export_comp)
  also have "... = (w⇧^⋆ ⊓ w⇧^T) * e⇧^T * top"
    using assms(1) injective_comp_right_dist_inf mult_assoc by simp
  also have "... = bot"
    using assms(2) acyclic_star_below_complement_1 semiring.mult_not_zero by blast
  finally have "?w * e⇧^T * top = bot"
    using 1 mult_right_dist_sup by simp
  thus ?thesis
    by (metis star.circ_top star_absorb)
qed

subsubsection ‹Exchange gives Minimum Spanning Trees›

text ‹
The lemmas in this section are used to show that the after exchange we obtain a minimum spanning tree.
The following lemmas show that the relation characterising the edge across the cut is an arc.
›

lemma kruskal_edge_arc:
  assumes "equivalence F"
      and "forest w"
      and "arc e"
      and "regular F"
      and "F ≤ forest_components (F ⊓ w)"
      and "regular w"
      and "w * e⇧^T = bot"
      and "e * F * e = bot"
      and "e⇧^T ≤ w⇧^⋆"
    shows "arc (w ⊓ top * e⇧^T * w⇧^T⇧^⋆ ⊓ F * e⇧^T * top ⊓ top * e * -F)"
proof (unfold arc_expanded, intro conjI)
  let ?E = "top * e⇧^T * w⇧^T⇧^⋆"
  let ?F = "F * e⇧^T * top"
  let ?G = "top * e * -F"
  let ?FF = "F * e⇧^T * e * F"
  let ?GG = "-F * e⇧^T * e * -F"
  let ?w = "forest_components (F ⊓ w)"
  have "F ⊓ w⇧^T⇧^⋆ ≤ forest_components (F ⊓ w) ⊓ w⇧^T⇧^⋆"
    by (simp add: assms(5) inf.coboundedI1)
  also have "... ≤ (F ⊓ w)⇧^T⇧^⋆ * ((F ⊓ w)⇧^⋆ ⊓ w⇧^T⇧^⋆)"
    apply (rule inf_star_import)
    apply (simp add: conv_isotone)
    apply (simp add: assms(2))
    apply (simp add: star.circ_reflexive)
    by (metis assms(6) conv_complement)
  also have "... ≤ (F ⊓ w)⇧^T⇧^⋆ * (w⇧^⋆ ⊓ w⇧^T⇧^⋆)"
    using comp_inf.mult_left_isotone mult_right_isotone star_isotone by simp
  also have "... = (F ⊓ w)⇧^T⇧^⋆"
    by (simp add: assms(2) acyclic_star_inf_conv)
  finally have "w * (F ⊓ w⇧^T⇧^⋆) * e⇧^T * e ≤ w * (F ⊓ w)⇧^T⇧^⋆ * e⇧^T * e"
    by (simp add: mult_left_isotone mult_right_isotone)
  also have "... = w * e⇧^T * e ⊔ w * (F ⊓ w)⇧^T⇧⁺ * e⇧^T * e"
    by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint sup_commute)
  also have "... = w * (F ⊓ w)⇧^T⇧⁺ * e⇧^T * e"
    by (simp add: assms(7))
  also have "... ≤ w * (F ⊓ w)⇧^T⇧⁺"
    by (metis assms(3) arc_univalent mult_assoc mult_1_right mult_right_isotone)
  also have "... ≤ w * w⇧^T * (F ⊓ w)⇧^T⇧^⋆"
    by (simp add: comp_associative conv_isotone mult_left_isotone mult_right_isotone)
  also have "... ≤ (F ⊓ w)⇧^T⇧^⋆"
    using assms(2) coreflexive_comp_top_inf inf.sup_right_divisibility by auto
  also have "... ≤ F⇧^T⇧^⋆"
    by (simp add: conv_dist_inf star_isotone)
  finally have 1: "w * (F ⊓ w⇧^T⇧^⋆) * e⇧^T * e ≤ F"
    by (metis assms(1) order.antisym mult_1_left mult_left_isotone star.circ_plus_same star.circ_reflexive star.left_plus_below_circ star_left_induct_mult_iff)
  have "F * e⇧^T * e ≤ forest_components (F ⊓ w) * e⇧^T * e"
    by (simp add: assms(5) mult_left_isotone)
  also have "... ≤ forest_components w * e⇧^T * e"
    by (simp add: comp_isotone conv_dist_inf star_isotone)
  also have "... = w⇧^T⇧^⋆ * e⇧^T * e"
    by (metis (no_types) assms(7) comp_associative conv_bot conv_dist_comp conv_involutive conv_star_commute star_absorb)
  also have "... ≤ w⇧^T⇧^⋆"
    by (metis assms(3) arc_univalent mult_assoc mult_1_right mult_right_isotone)
  finally have 2: "F * e⇧^T * e ≤ w⇧^T⇧^⋆"
    by simp
  have "w * F * e⇧^T * e ≤ w * F * e⇧^T * e * e⇧^T * e"
    using comp_associative ex231c mult_right_isotone by simp
  also have "... = w * (F * e⇧^T * e ⊓ w⇧^T⇧^⋆) * e⇧^T * e"
    using 2 by (simp add: comp_associative inf.absorb1)
  also have "... ≤ w * (F ⊓ w⇧^T⇧^⋆) * e⇧^T * e"
    by (metis assms(3) arc_univalent mult_assoc mult_1_right mult_right_isotone mult_left_isotone inf.sup_left_isotone)
  also have "... ≤ F"
    using 1 by simp
  finally have 3: "w * F * e⇧^T * e ≤ F"
    by simp
  hence "e⇧^T * e * F * w⇧^T ≤ F"
    by (metis assms(1) conv_dist_comp conv_dist_inf conv_involutive inf.absorb_iff1 mult_assoc)
  hence "e⇧^T * e * F * w⇧^T ≤ e⇧^T * top ⊓ F"
    by (simp add: comp_associative mult_right_isotone)
  also have "... ≤ e⇧^T * e * F"
    by (metis conv_involutive dedekind_1 inf_top_left mult_assoc)
  finally have 4: "e⇧^T * e * F * w⇧^T ≤ e⇧^T * e * F"
    by simp
  have "(top * e)⇧^T * (?F ⊓ w⇧^T⇧^⋆) = e⇧^T * top * e * F * w⇧^T⇧^⋆"
    by (metis assms(1) comp_inf.star.circ_decompose_9 comp_inf.star_star_absorb conv_dist_comp conv_involutive conv_top covector_inf_comp_3 vector_top_closed mult_assoc)
  also have "... = e⇧^T * e * F * w⇧^T⇧^⋆"
    by (simp add: assms(3) arc_top_edge)
  also have "... ≤ e⇧^T * e * F"
    using 4 star_right_induct_mult by simp
  also have "... ≤ F"
    by (metis assms(3) arc_injective conv_involutive mult_1_left mult_left_isotone)
  finally have 5: "(top * e)⇧^T * (?F ⊓ w⇧^T⇧^⋆) ≤ F"
    by simp
  have "(?F ⊓ w) * w⇧^T⇧⁺ = ?F ⊓ w * w⇧^T⇧⁺"
    by (simp add: vector_export_comp)
  also have "... ≤ ?F ⊓ w⇧^T⇧^⋆"
    by (metis assms(2) comp_associative inf.sup_right_isotone mult_left_isotone star.circ_transitive_equal star_left_unfold_equal sup.absorb_iff2 sup_monoid.add_assoc)
  also have 6: "... ≤ top * e * F"
    using 5 by (metis assms(3) shunt_mapping conv_dist_comp conv_involutive conv_top)
  finally have 7: "(?F ⊓ w) * w⇧^T⇧⁺ ≤ top * e * F"
    by simp
  have "e⇧^T * top * e ≤ 1"
    by (simp add: assms(3) point_injective)
  also have "... ≤ F"
    by (simp add: assms(1))
  finally have 8: "e * -F * e⇧^T ≤ bot"
    by (metis p_antitone p_antitone_iff p_bot regular_closed_bot schroeder_3_p schroeder_4_p mult_assoc)
  have "?FF ⊓ w * (w⇧^T⇧⁺ ⊓ ?GG) * w⇧^T ≤ ?F ⊓ w * (w⇧^T⇧⁺ ⊓ ?GG) * w⇧^T"
    using comp_inf.mult_left_isotone mult_isotone mult_assoc by simp
  also have "... ≤ ?F ⊓ w * (w⇧^T⇧⁺ ⊓ ?G) * w⇧^T"
    by (metis assms(3) arc_top_edge comp_inf.star.circ_decompose_9 comp_inf_covector inf.sup_right_isotone inf_le2 mult_left_isotone mult_right_isotone vector_top_closed mult_assoc)
  also have "... = (?F ⊓ w) * (w⇧^T⇧⁺ ⊓ ?G) * w⇧^T"
    by (simp add: vector_export_comp)
  also have "... = (?F ⊓ w) * w⇧^T⇧⁺ * (?G⇧^T ⊓ w⇧^T)"
    by (simp add: covector_comp_inf covector_comp_inf_1 covector_mult_closed)
  also have "... ≤ top * e * F * (?G⇧^T ⊓ w⇧^T)"
    using 7 mult_left_isotone by simp
  also have "... ≤ top * e * F * ?G⇧^T"
    by (simp add: mult_right_isotone)
  also have "... = top * e * -F * e⇧^T * top"
    by (metis assms(1) conv_complement conv_dist_comp conv_top equivalence_comp_left_complement mult_assoc)
  finally have 9: "?FF ⊓ w * (w⇧^T⇧⁺ ⊓ ?GG) * w⇧^T = bot"
    using 8 by (metis comp_associative covector_bot_closed le_bot vector_bot_closed)
  hence 10: "?FF ⊓ w * (w⇧⁺ ⊓ ?GG) * w⇧^T = bot"
    using assms(1) comp_associative conv_bot conv_complement conv_dist_comp conv_dist_inf conv_star_commute star.circ_plus_same by fastforce
  have "(w ⊓ ?E ⊓ ?F ⊓ ?G) * top * (w ⊓ ?E ⊓ ?F ⊓ ?G)⇧^T = (?F ⊓ (w ⊓ ?E ⊓ ?G)) * top * ((w ⊓ ?E ⊓ ?G)⇧^T ⊓ ?F⇧^T)"
    by (simp add: conv_dist_inf inf_commute inf_left_commute)
  also have "... = (?F ⊓ (w ⊓ ?E ⊓ ?G)) * top * (w ⊓ ?E ⊓ ?G)⇧^T ⊓ ?F⇧^T"
    using covector_comp_inf vector_conv_covector vector_mult_closed vector_top_closed by simp
  also have "... = ?F ⊓ (w ⊓ ?E ⊓ ?G) * top * (w ⊓ ?E ⊓ ?G)⇧^T ⊓ ?F⇧^T"
    by (simp add: vector_export_comp)
  also have "... = ?F ⊓ top * e * F ⊓ (w ⊓ ?E ⊓ ?G) * top * (w ⊓ ?E ⊓ ?G)⇧^T"
    by (simp add: assms(1) conv_dist_comp inf_assoc inf_commute mult_assoc)
  also have "... = ?F * e * F ⊓ (w ⊓ ?E ⊓ ?G) * top * (w ⊓ ?E ⊓ ?G)⇧^T"
    by (metis comp_associative comp_inf_covector inf_top.left_neutral)
  also have "... = ?FF ⊓ (w ⊓ ?E ⊓ ?G) * (top * (w ⊓ ?E ⊓ ?G)⇧^T)"
    using assms(3) arc_top_edge comp_associative by simp
  also have "... = ?FF ⊓ (w ⊓ ?E ⊓ ?G) * (top * (?G⇧^T ⊓ (?E⇧^T ⊓ w⇧^T)))"
    by (simp add: conv_dist_inf inf_assoc inf_commute inf_left_commute)
  also have "... = ?FF ⊓ (w ⊓ ?E ⊓ ?G) * (?G * (?E⇧^T ⊓ w⇧^T))"
    by (metis covector_comp_inf_1 covector_top_closed covector_mult_closed inf_top_left)
  also have "... = ?FF ⊓ (w ⊓ ?E ⊓ ?G) * (?G ⊓ ?E) * w⇧^T"
    by (metis covector_comp_inf_1 covector_top_closed mult_assoc)
  also have "... = ?FF ⊓ (w ⊓ ?E) * (?G⇧^T ⊓ ?G ⊓ ?E) * w⇧^T"
    by (metis covector_comp_inf_1 covector_mult_closed inf.sup_monoid.add_assoc vector_top_closed)
  also have "... = ?FF ⊓ w * (?E⇧^T ⊓ ?G⇧^T ⊓ ?G ⊓ ?E) * w⇧^T"
    by (metis covector_comp_inf_1 covector_mult_closed inf.sup_monoid.add_assoc vector_top_closed)
  also have "... = ?FF ⊓ w * (?E⇧^T ⊓ ?E ⊓ (?G⇧^T ⊓ ?G)) * w⇧^T"
    by (simp add: inf_commute inf_left_commute)
  also have "... = ?FF ⊓ w * (?E⇧^T ⊓ ?E ⊓ (-F * e⇧^T * top ⊓ ?G)) * w⇧^T"
    by (simp add: assms(1) conv_complement conv_dist_comp mult_assoc)
  also have "... = ?FF ⊓ w * (?E⇧^T ⊓ ?E ⊓ (-F * e⇧^T * ?G)) * w⇧^T"
    by (metis comp_associative comp_inf_covector inf_top.left_neutral)
  also have "... = ?FF ⊓ w * (?E⇧^T ⊓ ?E ⊓ ?GG) * w⇧^T"
    by (metis assms(3) arc_top_edge comp_associative)
  also have "... = ?FF ⊓ w * (w⇧^⋆ * e * top ⊓ ?E ⊓ ?GG) * w⇧^T"
    by (simp add: comp_associative conv_dist_comp conv_star_commute)
  also have "... = ?FF ⊓ w * (w⇧^⋆ * e * ?E ⊓ ?GG) * w⇧^T"
    by (metis comp_associative comp_inf_covector inf_top.left_neutral)
  also have "... ≤ ?FF ⊓ w * (w⇧^⋆ * w⇧^T⇧^⋆ ⊓ ?GG) * w⇧^T"
    by (metis assms(3) mult_assoc mult_1_right mult_left_isotone mult_right_isotone inf.sup_left_isotone inf.sup_right_isotone arc_expanded)
  also have "... = ?FF ⊓ w * ((w⇧⁺ ⊔ 1 ⊔ w⇧^T⇧^⋆) ⊓ ?GG) * w⇧^T"
    by (simp add: assms(2) cancel_separate_eq star_left_unfold_equal sup_monoid.add_commute)
  also have "... = ?FF ⊓ w * ((w⇧⁺ ⊔ 1 ⊔ w⇧^T⇧⁺) ⊓ ?GG) * w⇧^T"
    using star.circ_plus_one star_left_unfold_equal sup_assoc by presburger
  also have "... = (?FF ⊓ w * (w⇧⁺ ⊓ ?GG) * w⇧^T) ⊔ (?FF ⊓ w * (1 ⊓ ?GG) * w⇧^T) ⊔ (?FF ⊓ w * (w⇧^T⇧⁺ ⊓ ?GG) * w⇧^T)"
    by (simp add: inf_sup_distrib1 inf_sup_distrib2 semiring.distrib_left semiring.distrib_right)
  also have "... ≤ w * (1 ⊓ ?GG) * w⇧^T"
    using 9 10 by simp
  also have "... ≤ w * w⇧^T"
    by (metis inf.cobounded1 mult_1_right mult_left_isotone mult_right_isotone)
  also have "... ≤ 1"
    by (simp add: assms(2))
  finally show "(w ⊓ ?E ⊓ ?F ⊓ ?G) * top * (w ⊓ ?E ⊓ ?F ⊓ ?G)⇧^T ≤ 1"
    by simp
  have "w⇧^T⇧⁺ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w ≤ w⇧^T⇧⁺ ⊓ ?G ⊓ w⇧^T * F * e⇧^T * e * F * w"
    using top_greatest inf.sup_left_isotone inf.sup_right_isotone mult_left_isotone by simp
  also have "... ≤ w⇧^T⇧⁺ ⊓ ?G ⊓ w⇧^T * ?F"
    using comp_associative inf.sup_right_isotone mult_right_isotone top.extremum by presburger
  also have "... = w⇧^T * (w⇧^T⇧^⋆ ⊓ ?F) ⊓ ?G"
    using assms(2) inf_assoc inf_commute inf_left_commute univalent_comp_left_dist_inf by simp
  also have "... ≤ w⇧^T * (top * e * F) ⊓ ?G"
    using 6 by (metis inf.sup_monoid.add_commute inf.sup_right_isotone mult_right_isotone)
  also have "... ≤ top * e * F ⊓ ?G"
    by (metis comp_associative comp_inf_covector mult_left_isotone top.extremum)
  also have "... = bot"
    by (metis assms(3) conv_dist_comp conv_involutive conv_top inf_p mult_right_zero univalent_comp_left_dist_inf)
  finally have 11: "w⇧^T⇧⁺ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w = bot"
    by (simp add: order.antisym)
  hence 12: "w⇧⁺ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w = bot"
    using assms(1) comp_associative conv_bot conv_complement conv_dist_comp conv_dist_inf conv_star_commute star.circ_plus_same by fastforce
  have "(w ⊓ ?E ⊓ ?F ⊓ ?G)⇧^T * top * (w ⊓ ?E ⊓ ?F ⊓ ?G) = ((w ⊓ ?E ⊓ ?G)⇧^T ⊓ ?F⇧^T) * top * (?F ⊓ (w ⊓ ?E ⊓ ?G))"
    by (simp add: conv_dist_inf inf_commute inf_left_commute)
  also have "... = (w ⊓ ?E ⊓ ?G)⇧^T * ?F * (?F ⊓ (w ⊓ ?E ⊓ ?G))"
    by (simp add: covector_inf_comp_3 vector_mult_closed)
  also have "... = (w ⊓ ?E ⊓ ?G)⇧^T * (?F ⊓ ?F⇧^T) * (w ⊓ ?E ⊓ ?G)"
    using covector_comp_inf covector_inf_comp_3 vector_conv_covector vector_mult_closed by simp
  also have "... = (w ⊓ ?E ⊓ ?G)⇧^T * (?F ⊓ ?F⇧^T) * (w ⊓ ?E) ⊓ ?G"
    by (simp add: comp_associative comp_inf_covector)
  also have "... = (w ⊓ ?E ⊓ ?G)⇧^T * (?F ⊓ ?F⇧^T) * w ⊓ ?E ⊓ ?G"
    by (simp add: comp_associative comp_inf_covector)
  also have "... = (?G⇧^T ⊓ (?E⇧^T ⊓ w⇧^T)) * (?F ⊓ ?F⇧^T) * w ⊓ ?E ⊓ ?G"
    by (simp add: conv_dist_inf inf.left_commute inf.sup_monoid.add_commute)
  also have "... = ?G⇧^T ⊓ (?E⇧^T ⊓ w⇧^T) * (?F ⊓ ?F⇧^T) * w ⊓ ?E ⊓ ?G"
    by (metis (no_types) comp_associative conv_dist_comp conv_top vector_export_comp)
  also have "... = ?G⇧^T ⊓ ?E⇧^T ⊓ w⇧^T * (?F ⊓ ?F⇧^T) * w ⊓ ?E ⊓ ?G"
    by (metis (no_types) comp_associative inf_assoc conv_dist_comp conv_top vector_export_comp)
  also have "... = ?E⇧^T ⊓ ?E ⊓ (?G⇧^T ⊓ ?G) ⊓ w⇧^T * (?F ⊓ ?F⇧^T) * w"
    by (simp add: inf_assoc inf.left_commute inf.sup_monoid.add_commute)
  also have "... = w⇧^⋆ * e * top ⊓ ?E ⊓ (?G⇧^T ⊓ ?G) ⊓ w⇧^T * (?F ⊓ ?F⇧^T) * w"
    by (simp add: comp_associative conv_dist_comp conv_star_commute)
  also have "... = w⇧^⋆ * e * ?E ⊓ (?G⇧^T ⊓ ?G) ⊓ w⇧^T * (?F ⊓ ?F⇧^T) * w"
    by (metis comp_associative comp_inf_covector inf_top.left_neutral)
  also have "... ≤ w⇧^⋆ * w⇧^T⇧^⋆ ⊓ (?G⇧^T ⊓ ?G) ⊓ w⇧^T * (?F ⊓ ?F⇧^T) * w"
    by (metis assms(3) mult_assoc mult_1_right mult_left_isotone mult_right_isotone inf.sup_left_isotone arc_expanded)
  also have "... = w⇧^⋆ * w⇧^T⇧^⋆ ⊓ (-F * e⇧^T * top ⊓ ?G) ⊓ w⇧^T * (?F ⊓ ?F⇧^T) * w"
    by (simp add: assms(1) conv_complement conv_dist_comp mult_assoc)
  also have "... = w⇧^⋆ * w⇧^T⇧^⋆ ⊓ -F * e⇧^T * ?G ⊓ w⇧^T * (?F ⊓ ?F⇧^T) * w"
    by (metis comp_associative comp_inf_covector inf_top.left_neutral)
  also have "... = w⇧^⋆ * w⇧^T⇧^⋆ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * (?F ⊓ ?F⇧^T) * w"
    by (metis assms(3) arc_top_edge mult_assoc)
  also have "... = w⇧^⋆ * w⇧^T⇧^⋆ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * (?F ⊓ top * e * F) * w"
    by (simp add: assms(1) conv_dist_comp mult_assoc)
  also have "... = w⇧^⋆ * w⇧^T⇧^⋆ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * (?F * e * F) * w"
    by (metis comp_associative comp_inf_covector inf_top.left_neutral)
  also have "... = w⇧^⋆ * w⇧^T⇧^⋆ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w"
    by (metis assms(3) arc_top_edge mult_assoc)
  also have "... = (w⇧⁺ ⊔ 1 ⊔ w⇧^T⇧^⋆) ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w"
    by (simp add: assms(2) cancel_separate_eq star_left_unfold_equal sup_monoid.add_commute)
  also have "... = (w⇧⁺ ⊔ 1 ⊔ w⇧^T⇧⁺) ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w"
    using star.circ_plus_one star_left_unfold_equal sup_assoc by presburger
  also have "... = (w⇧⁺ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w) ⊔ (1 ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w) ⊔ (w⇧^T⇧⁺ ⊓ -F * e⇧^T * e * -F ⊓ w⇧^T * F * e⇧^T * e * F * w)"
    by (simp add: inf_sup_distrib2)
  also have "... ≤ 1"
    using 11 12 by (simp add: inf.coboundedI1)
  finally show "(w ⊓ ?E ⊓ ?F ⊓ ?G)⇧^T * top * (w ⊓ ?E ⊓ ?F ⊓ ?G) ≤ 1"
    by simp
  have "(w ⊓ -F) * (F ⊓ w⇧^T) ≤ w * w⇧^T ⊓ -F * F"
    by (simp add: mult_isotone)
  also have "... ≤ 1 ⊓ -F"
    using assms(1,2) comp_inf.comp_isotone equivalence_comp_right_complement by auto
  also have "... = bot"
    using assms(1) bot_unique pp_isotone pseudo_complement_pp by blast
  finally have 13: "(w ⊓ -F) * (F ⊓ w⇧^T) = bot"
    by (simp add: order.antisym)
  have "w ⊓ ?G ≤ F * (w ⊓ ?G)"
    by (metis assms(1) mult_1_left mult_right_dist_sup sup.absorb_iff2)
  also have "... ≤ F * (w ⊓ ?G) * w⇧^⋆"
    by (metis eq_refl le_supE star.circ_back_loop_fixpoint)
  finally have 14: "w ⊓ ?G ≤ F * (w ⊓ ?G) * w⇧^⋆"
    by simp
  have "w ⊓ top * e * F ≤ w * (e * F)⇧^T * e * F"
    by (metis (no_types) comp_inf.star_slide dedekind_2 inf_left_commute inf_top_right mult_assoc)
  also have "... ≤ F"
    using 3 assms(1) by (metis comp_associative conv_dist_comp mult_left_isotone preorder_idempotent)
  finally have "w ⊓ -F ≤ -(top * e * F)"
    using order.trans p_shunting_swap pp_increasing by blast
  also have "... = ?G"
    by (metis assms(3) comp_mapping_complement conv_dist_comp conv_involutive conv_top)
  finally have "(w ⊓ -F) * F * (w ⊓ ?G) = (w ⊓ -F ⊓ ?G) * F * (w ⊓ ?G)"
    by (simp add: inf.absorb1)
  also have "... ≤ (w ⊓ -F ⊓ ?G) * F * w"
    by (simp add: comp_isotone)
  also have "... ≤ (w ⊓ -F ⊓ ?G) * forest_components (F ⊓ w) * w"
    by (simp add: assms(5) mult_left_isotone mult_right_isotone)
  also have "... ≤ (w ⊓ -F ⊓ ?G) * (F ⊓ w)⇧^T⇧^⋆ * w⇧^⋆ * w"
    by (simp add: mult_left_isotone mult_right_isotone star_isotone mult_assoc)
  also have "... ≤ (w ⊓ -F ⊓ ?G) * (F ⊓ w)⇧^T⇧^⋆ * w⇧^⋆"
    by (simp add: comp_associative mult_right_isotone star.circ_plus_same star.left_plus_below_circ)
  also have "... = (w ⊓ -F ⊓ ?G) * w⇧^⋆ ⊔ (w ⊓ -F ⊓ ?G) * (F ⊓ w)⇧^T⇧⁺ * w⇧^⋆"
    by (metis comp_associative inf.sup_monoid.add_assoc mult_left_dist_sup star.circ_loop_fixpoint sup_commute)
  also have "... ≤ (w ⊓ -F ⊓ ?G) * w⇧^⋆ ⊔ (w ⊓ -F ⊓ ?G) * (F ⊓ w)⇧^T * top"
    by (metis mult_assoc top_greatest mult_right_isotone sup_right_isotone)
  also have "... ≤ (w ⊓ -F ⊓ ?G) * w⇧^⋆ ⊔ (w ⊓ -F) * (F ⊓ w)⇧^T * top"
    using inf.cobounded1 mult_left_isotone sup_right_isotone by blast
  also have "... ≤ (w ⊓ ?G) * w⇧^⋆ ⊔ (w ⊓ -F) * (F ⊓ w)⇧^T * top"
    using inf.sup_monoid.add_assoc inf.sup_right_isotone mult_left_isotone sup_commute sup_right_isotone by simp
  also have "... = (w ⊓ ?G) * w⇧^⋆ ⊔ (w ⊓ -F) * (F ⊓ w⇧^T) * top"
    by (simp add: assms(1) conv_dist_inf)
  also have "... ≤ 1 * (w ⊓ ?G) * w⇧^⋆"
    using 13 by simp
  also have "... ≤ F * (w ⊓ ?G) * w⇧^⋆"
    using assms(1) mult_left_isotone by blast
  finally have 15: "(w ⊓ -F) * F * (w ⊓ ?G) ≤ F * (w ⊓ ?G) * w⇧^⋆"
    by simp
  have "(w ⊓ F) * F * (w ⊓ ?G) ≤ F * F * (w ⊓ ?G)"
    by (simp add: mult_left_isotone)
  also have "... = F * (w ⊓ ?G)"
    by (simp add: assms(1) preorder_idempotent)
  also have "... ≤ F * (w ⊓ ?G) * w⇧^⋆"
    by (metis eq_refl le_supE star.circ_back_loop_fixpoint)
  finally have "(w ⊓ F) * F * (w ⊓ ?G) ≤ F * (w ⊓ ?G) * w⇧^⋆"
    by simp
  hence "((w ⊓ F) ⊔ (w ⊓ -F)) * F * (w ⊓ ?G) ≤ F * (w ⊓ ?G) * w⇧^⋆"
    using 15 by (simp add: semiring.distrib_right)
  hence "w * F * (w ⊓ ?G) ≤ F * (w ⊓ ?G) * w⇧^⋆"
    by (metis assms(4) maddux_3_11_pp)
  hence "w * F * (w ⊓ ?G) * w⇧^⋆ ≤ F * (w ⊓ ?G) * w⇧^⋆"
    by (metis (full_types) comp_associative mult_left_isotone star.circ_transitive_equal)
  hence "w⇧^⋆ * (w ⊓ ?G) ≤ F * (w ⊓ ?G) * w⇧^⋆"
    using 14 by (simp add: mult_assoc star_left_induct)
  hence 16: "w⇧⁺ ⊓ ?G ≤ F * (w ⊓ ?G) * w⇧^⋆"
    by (simp add: covector_comp_inf covector_mult_closed star.circ_plus_same)
  have 17: "e⇧^T * top * e⇧^T ≤ -F"
    using assms(8) le_bot triple_schroeder_p by simp
  hence "(top * e)⇧^T * e⇧^T ≤ -F"
    by (simp add: conv_dist_comp)
  hence 18: "e⇧^T ≤ ?G"
    by (metis assms(3) shunt_mapping conv_dist_comp conv_involutive conv_top)
  have "e⇧^T ≤ -F"
    using 17 by (simp add: assms(3) arc_top_arc)
  also have "... ≤ -1"
    by (simp add: assms(1) p_antitone)
  finally have "e⇧^T ≤ w⇧^⋆ ⊓ -1"
    using assms(9) by simp
  also have "... ≤ w⇧⁺"
    using shunting_var_p star_left_unfold_equal sup_commute by simp
  finally have "e⇧^T ≤ w⇧⁺ ⊓ ?G"
    using 18 by simp
  hence "e⇧^T ≤ F * (w ⊓ ?G) * w⇧^⋆"
    using 16 order_trans by blast
  also have "... = (F * w ⊓ ?G) * w⇧^⋆"
    by (simp add: comp_associative comp_inf_covector)
  finally have "e⇧^T * top * e⇧^T ≤ (F * w ⊓ ?G) * w⇧^⋆"
    by (simp add: assms(3) arc_top_arc)
  hence "e⇧^T * top * (e * top)⇧^T ≤ (F * w ⊓ ?G) * w⇧^⋆"
    by (metis conv_dist_comp conv_top vector_top_closed mult_assoc)
  hence "e⇧^T * top ≤ (F * w ⊓ ?G) * w⇧^⋆ * e * top"
    by (metis assms(3) shunt_bijective mult_assoc)
  hence "(top * e)⇧^T * top ≤ (F * w ⊓ ?G) * w⇧^⋆ * e * top"
    by (simp add: conv_dist_comp mult_assoc)
  hence "top ≤ top * e * (F * w ⊓ ?G) * w⇧^⋆ * e * top"
    by (metis assms(3) shunt_mapping conv_dist_comp conv_involutive conv_top mult_assoc)
  also have "... = top * e * F * w * (w⇧^⋆ * e * top ⊓ ?G⇧^T)"
    by (metis comp_associative comp_inf_vector_1)
  also have "... = top * (w ⊓ (top * e * F)⇧^T) * (w⇧^⋆ * e * top ⊓ ?G⇧^T)"
    by (metis comp_inf_vector_1 inf_top.left_neutral)
  also have "... = top * (w ⊓ ?F) * (w⇧^⋆ * e * top ⊓ ?G⇧^T)"
    by (simp add: assms(1) conv_dist_comp mult_assoc)
  also have "... = top * (w ⊓ ?F) * (?E⇧^T ⊓ ?G⇧^T)"
    by (simp add: comp_associative conv_dist_comp conv_star_commute)
  also have "... = top * (w ⊓ ?F ⊓ ?G) * ?E⇧^T"
    by (simp add: comp_associative comp_inf_vector_1)
  also have "... = top * (w ⊓ ?F ⊓ ?G ⊓ ?E) * top"
    using comp_inf_vector_1 mult_assoc by simp
  finally show "top * (w ⊓ ?E ⊓ ?F ⊓ ?G) * top = top"
    by (simp add: inf_commute inf_left_commute top_le)
qed

lemma kruskal_edge_arc_1:
  assumes "e ≤ --h"
      and "h ≤ g"
      and "symmetric g"
      and "components g ≤ forest_components w"
      and "w * e⇧^T = bot"
    shows "e⇧^T ≤ w⇧^⋆"
proof -
  have "w⇧^T * top ≤ -(e⇧^T * top)"
    using assms(5) schroeder_3_p vector_bot_closed mult_assoc by fastforce
  hence 1: "w⇧^T * top ⊓ e⇧^T * top = bot"
    using pseudo_complement by simp
  have "e⇧^T ≤ e⇧^T * top ⊓ --h⇧^T"
    using assms(1) conv_complement conv_isotone top_right_mult_increasing by fastforce
  also have "... ≤ e⇧^T * top ⊓ --g"
    by (metis assms(2,3) inf.sup_right_isotone pp_isotone conv_isotone)
  also have "... ≤ e⇧^T * top ⊓ components g"
    using inf.sup_right_isotone star.circ_increasing by simp
  also have "... ≤ e⇧^T * top ⊓ forest_components w"
    using assms(4) comp_inf.mult_right_isotone by simp
  also have "... = (e⇧^T * top ⊓ w⇧^T⇧^⋆) * w⇧^⋆"
    by (simp add: inf_assoc vector_export_comp)
  also have "... = (e⇧^T * top ⊓ 1) * w⇧^⋆ ⊔ (e⇧^T * top ⊓ w⇧^T⇧⁺) * w⇧^⋆"
    by (metis inf_sup_distrib1 semiring.distrib_right star_left_unfold_equal)
  also have "... ≤ w⇧^⋆ ⊔ (e⇧^T * top ⊓ w⇧^T⇧⁺) * w⇧^⋆"
    by (metis inf_le2 mult_1_left mult_left_isotone sup_left_isotone)
  also have "... ≤ w⇧^⋆ ⊔ (e⇧^T * top ⊓ w⇧^T) * top"
    using comp_associative comp_inf.mult_right_isotone sup_right_isotone mult_right_isotone top.extremum vector_export_comp by presburger
  also have "... = w⇧^⋆"
    using 1 inf.sup_monoid.add_commute inf_vector_comp by simp
  finally show ?thesis
    by simp
qed

lemma kruskal_edge_between_components_1:
  assumes "equivalence F"
      and "mapping (top * e)"
    shows "F ≤ -(w ⊓ top * e⇧^T * w⇧^T⇧^⋆ ⊓ F * e⇧^T * top ⊓ top * e * -F)"
proof -
  let ?d = "w ⊓ top * e⇧^T * w⇧^T⇧^⋆ ⊓ F * e⇧^T * top ⊓ top * e * -F"
  have "?d ⊓ F ≤ F * e⇧^T * top ⊓ F"
    by (meson inf_le1 inf_le2 le_infI order_trans)
  also have "... ≤ (F * e⇧^T * top)⇧^T * F"
    by (simp add: mult_assoc vector_restrict_comp_conv)
  also have "... = top * e * F * F"
    by (simp add: assms(1) comp_associative conv_dist_comp conv_star_commute)
  also have "... = top * e * F"
    using assms(1) preorder_idempotent mult_assoc by fastforce
  finally have "?d ⊓ F ≤ top * e * F ⊓ top * e * -F"
    by (simp add: le_infI1)
  also have "... = top * e * F ⊓ -(top * e * F)"
    using assms(2) conv_dist_comp total_conv_surjective comp_mapping_complement by simp
  finally show ?thesis
    by (metis inf_p le_bot p_antitone_iff pseudo_complement)
qed

lemma kruskal_edge_between_components_2:
  assumes "forest_components f ≤ -d"
      and "injective f"
      and "f ⊔ f⇧^T ≤ w ⊔ w⇧^T"
    shows "f ⊔ f⇧^T ≤ (w ⊓ -d ⊓ -d⇧^T) ⊔ (w⇧^T ⊓ -d ⊓ -d⇧^T)"
proof -
  let ?F = "forest_components f"
  have "?F⇧^T ≤ -d⇧^T"
    using assms(1) conv_complement conv_order by fastforce
  hence 1: "?F ≤ -d⇧^T"
    by (simp add: conv_dist_comp conv_star_commute)
  have "equivalence ?F"
    using assms(2) forest_components_equivalence by simp
  hence "f ⊔ f⇧^T ≤ ?F"
    by (metis conv_dist_inf forest_components_increasing inf.absorb_iff2 sup.boundedI)
  also have "... ≤ -d ⊓ -d⇧^T"
    using 1 assms(1) by simp
  finally have "f ⊔ f⇧^T ≤ -d ⊓ -d⇧^T"
    by simp
  thus ?thesis
    by (metis assms(3) inf_sup_distrib2 le_inf_iff)
qed

end

subsection ‹Related Structures›

text ‹
Stone algebras can be expanded to Stone-Kleene relation algebras by reusing some operations.
›

sublocale stone_algebra < comp_inf: stone_kleene_relation_algebra where star = "λx . top" and one = top and times = inf and conv = id
  apply unfold_locales
  by simp

text ‹
Every bounded linear order can be expanded to a Stone algebra, which can be expanded to a Stone relation algebra, which can be expanded to a Stone-Kleene relation algebra.
›

class linorder_stone_kleene_relation_algebra_expansion = linorder_stone_relation_algebra_expansion + star +
  assumes star_def [simp]: "x⇧^⋆ = top"
begin

subclass kleene_algebra
  apply unfold_locales
  apply simp
  apply (simp add: min.coboundedI1 min.commute)
  by (simp add: min.coboundedI1)

subclass stone_kleene_relation_algebra
  apply unfold_locales
  by simp

end

text ‹
A Kleene relation algebra is based on a relation algebra.
›

class kleene_relation_algebra = relation_algebra + stone_kleene_relation_algebra
begin

text ‹See 🌐‹https://arxiv.org/abs/2310.08946› for the following results ‹scc_1›-‹scc_4›.›

lemma scc_1:
  assumes "1 ⊓ y ≤ z"
      and "x⇧^T * y ≤ y"
      and "y * z⇧^T ≤ y"
      and "(x ⊓ y) * z ≤ z"
    shows "x⇧^⋆ ⊓ y ≤ z"
proof -
  have "x * (-y ⊔ z) ⊓ y = x * z ⊓ y"
  proof (rule order.antisym)
    have "x * (-y ⊔ z) ⊓ y ≤ x * ((-y ⊔ z) ⊓ x⇧^T * y)"
      by (simp add: dedekind_1)
    also have "... ≤ x * ((-y ⊔ z) ⊓ y)"
      by (simp add: assms(2) le_infI2 mult_right_isotone)
    also have "... ≤ x * z"
      by (simp add: inf.sup_monoid.add_commute mult_right_isotone)
    finally show "x * (-y ⊔ z) ⊓ y ≤ x * z ⊓ y"
      by simp
    show "x * z ⊓ y ≤ x * (-y ⊔ z) ⊓ y"
      by (simp add: inf_commute le_infI2 mult_right_isotone)
  qed
  also have "... ≤ (x ⊓ y * z⇧^T) * z"
    by (simp add: dedekind_2)
  also have "... ≤ (x ⊓ y) * z"
    by (simp add: assms(3) le_infI2 mult_left_isotone)
  also have "... ≤ z"
    by (simp add: assms(4))
  finally have 1: "x * (-y ⊔ z) ⊓ y ≤ z"
    .
  have "(1 ⊔ x * (-y ⊔ z)) ⊓ y = (1 ⊓ y) ⊔ (x * (-y ⊔ z) ⊓ y)"
    by (simp add: comp_inf.mult_right_dist_sup)
  also have "... ≤ z"
    using 1 by (simp add: assms(1))
  finally have "1 ⊔ x * (-y ⊔ z) ≤ -y ⊔ z"
    using shunt1 by blast
  hence "x⇧^⋆ ≤ -y ⊔ z"
    using star_left_induct by fastforce
  thus ?thesis
    by (simp add: shunt1)
qed

lemma scc_2:
  assumes "x⇧^T * y ≤ y"
      and "y * (x ⊓ y)⇧^⋆⇧^T ≤ y"
    shows "x⇧^⋆ ⊓ y ≤ (x ⊓ y)⇧^⋆"
proof -
  have 1: "1 ⊓ y ≤ (x ⊓ y)⇧^⋆"
    by (simp add: inf.coboundedI1 star.circ_reflexive)
  have "(x ⊓ y) * (x ⊓ y)⇧^⋆ ≤ (x ⊓ y)⇧^⋆"
    by (simp add: star.left_plus_below_circ)
  thus ?thesis
    using 1 assms scc_1 by blast
qed

lemma scc_3:
  "x⇧^⋆ ⊓ x⇧^T⇧^⋆ ≤ (x ⊓ x⇧^T⇧^⋆)⇧^⋆"
proof -
  have 1: "x⇧^T * x⇧^T⇧^⋆ ≤ x⇧^T⇧^⋆"
    by (simp add: star.left_plus_below_circ)
  have "x⇧^T⇧^⋆ * (x ⊓ x⇧^T⇧^⋆)⇧^⋆⇧^T ≤ x⇧^T⇧^⋆ * x⇧^⋆⇧^T"
    by (simp add: star_isotone conv_isotone mult_right_isotone)
  also have "... = x⇧^T⇧^⋆ * x⇧^T⇧^⋆"
    by (simp add: conv_star_commute)
  finally have "x⇧^T⇧^⋆ * (x ⊓ x⇧^T⇧^⋆)⇧^⋆⇧^T ≤ x⇧^T⇧^⋆"
    by (simp add: star.circ_transitive_equal)
  thus ?thesis
    using 1 scc_2 by auto
qed

lemma scc_4:
  "x⇧^⋆ ⊓ x⇧^T⇧^⋆ = (x ⊓ x⇧^T⇧^⋆)⇧^⋆"
proof (rule order.antisym)
  show "x⇧^⋆ ⊓ x⇧^T⇧^⋆ ≤ (x ⊓ x⇧^T⇧^⋆)⇧^⋆"
    by (simp add: scc_3)
  have 1: "(x ⊓ x⇧^T⇧^⋆)⇧^⋆ ≤ x⇧^⋆"
    by (simp add: star_isotone)
  have "(x ⊓ x⇧^T⇧^⋆)⇧^⋆ ≤ x⇧^T⇧^⋆⇧^⋆"
    by (simp add: star_isotone)
  also have "... = x⇧^T⇧^⋆"
    using star_involutive by auto
  finally show "(x ⊓ x⇧^T⇧^⋆)⇧^⋆ ≤ x⇧^⋆ ⊓ x⇧^T⇧^⋆"
    using 1 by simp
qed

end

class stone_kleene_relation_algebra_tarski = stone_kleene_relation_algebra + stone_relation_algebra_tarski

class kleene_relation_algebra_tarski = kleene_relation_algebra + stone_kleene_relation_algebra_tarski
begin

subclass relation_algebra_tarski ..

end

class stone_kleene_relation_algebra_consistent = stone_kleene_relation_algebra + stone_relation_algebra_consistent
begin

lemma acyclic_reachable_different:
  assumes "acyclic p" "bijective y" "x ≤ p⇧⁺ * y"
  shows "x ≠ y"
proof (rule ccontr)
  assume 1: "¬ x ≠ y"
  have "x * y⇧^T ≤ p⇧⁺"
    using assms(2,3) shunt_bijective by blast
  also have "... ≤ -1"
    by (simp add: assms(1))
  finally show False
    using 1 by (metis assms(2) dual_order.antisym le_supI2 mult_1_left order_char_1 point_not_bot schroeder_4_p semiring.mult_not_zero)
qed

end

class kleene_relation_algebra_consistent = kleene_relation_algebra + stone_kleene_relation_algebra_consistent
begin

subclass relation_algebra_consistent ..

end

class stone_kleene_relation_algebra_tarski_consistent = stone_kleene_relation_algebra + stone_relation_algebra_tarski_consistent
begin

subclass stone_kleene_relation_algebra_tarski ..

subclass stone_kleene_relation_algebra_consistent ..

end

class kleene_relation_algebra_tarski_consistent = kleene_relation_algebra + stone_kleene_relation_algebra_tarski_consistent
begin

subclass relation_algebra_tarski_consistent ..

end

class linorder_stone_kleene_relation_algebra_tarski_consistent_expansion = linorder_stone_kleene_relation_algebra_expansion + non_trivial_bounded_order
begin

subclass stone_kleene_relation_algebra_tarski_consistent
  apply unfold_locales
  by (simp_all add: bot_not_top)

end

end