Theory More_Disjoint_Set_Forests

(* Title:      More on Disjoint-Set Forests
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

theory More_Disjoint_Set_Forests

imports Disjoint_Set_Forests

begin

section ‹More on Array Access and Disjoint-Set Forests›

text ‹
This section contains further results about directed acyclic graphs and relational array operations.
›

context stone_relation_algebra
begin

lemma update_square:
  assumes "point y"
    shows "x[yx[[x[[y]]]]]  x * x  x"
proof -
  have "x[yx[[x[[y]]]]] = (y  yT * x * x)  (-y  x)"
    by (simp add: conv_dist_comp)
  also have "...  (y  yT) * x * x  x"
    by (smt assms inf.eq_refl inf.sup_monoid.add_commute inf_le1 sup_mono vector_inf_comp)
  also have "...  x * x  x"
    by (smt (z3) assms comp_associative conv_dist_comp coreflexive_comp_top_inf inf.cobounded2 sup_left_isotone symmetric_top_closed)
  finally show ?thesis
    .
qed

lemma update_ub:
  "x[yz]  x  zT"
  by (meson dual_order.trans inf.cobounded2 le_supI sup.cobounded1 sup_ge2)

lemma update_square_ub:
  "x[y(x * x)T]  x  x * x"
  by (metis conv_involutive update_ub)

lemma update_same_sub:
  assumes "u  x = u  z"
      and "y  u"
      and "regular y"
    shows "x[yzT] = x"
  by (smt (z3) assms conv_involutive inf.sup_monoid.add_commute inf.sup_relative_same_increasing maddux_3_11_pp)

lemma update_point_get:
  "point y  x[yz[[y]]] = x[yzT]"
  by (metis conv_involutive get_put inf_commute update_inf_same)

lemma update_bot:
  "x[botz] = x"
  by simp

lemma update_top:
  "x[topz] = zT"
  by simp

lemma update_same:
  assumes "regular u"
    shows "(x[yz])[uz] = x[y  uz]"
proof -
  have "(x[yz])[uz] = (u  zT)  (-u  y  zT)  (-u  -y  x)"
    using inf.sup_monoid.add_assoc inf_sup_distrib1 sup_assoc by force
  also have "... = (u  zT)  (y  zT)  (-(u  y)  x)"
    by (metis assms inf_sup_distrib2 maddux_3_21_pp p_dist_sup)
  also have "... = x[y  uz]"
    using comp_inf.mult_right_dist_sup sup_commute by auto
  finally show ?thesis
    .
qed

lemma update_same_3:
  assumes "regular u"
      and "regular v"
    shows "((x[yz])[uz])[vz] = x[y  u  vz]"
  by (metis assms update_same)

lemma update_split:
  assumes "regular w"
    shows "x[yz] = (x[y - wz])[y  wz]"
  by (smt (z3) assms comp_inf.semiring.distrib_left inf.left_commute inf.sup_monoid.add_commute inf_import_p maddux_3_11_pp maddux_3_12 p_dist_inf sup_assoc)

lemma update_injective_swap:
  assumes "injective x"
      and "point y"
      and "injective z"
      and "vector z"
    shows "injective ((x[yx[[z]]])[zx[[y]]])"
proof -
  have 1: "(z  yT * x) * (z  yT * x)T  1"
    using assms(3) injective_inf_closed by auto
  have "(z  yT * x) * (-z  y  zT * x)T  (z  yT * x) * (yT  xT * z)"
    by (metis conv_dist_comp conv_involutive conv_order inf.boundedE inf.boundedI inf.cobounded1 inf.cobounded2 mult_right_isotone)
  also have "... = (z  zT * x) * (yT  xT * y)"
    by (smt (z3) assms(2,4) covector_inf_comp_3 inf.left_commute inf.sup_monoid.add_commute comp_associative conv_dist_comp conv_involutive)
  also have "... = (z  zT) * x * xT * (y  yT)"
    by (smt (z3) assms(2,4) comp_associative inf.sup_monoid.add_commute vector_covector vector_inf_comp)
  also have "...  x * xT"
    by (metis assms(2-4) comp_associative comp_right_one coreflexive_comp_top_inf inf.coboundedI2 mult_right_isotone vector_covector)
  also have "...  1"
    by (simp add: assms(1))
  finally have 2: "(z  yT * x) * (-z  y  zT * x)T  1"
    .
  have "(z  yT * x) * (-z  -y  x)T  yT * x * (-yT  xT)"
    by (smt comp_isotone conv_complement conv_dist_inf inf.cobounded2 inf.sup_monoid.add_assoc)
  also have "... = yT * x * xT  -yT"
    by (simp add: inf.commute assms(2) covector_comp_inf vector_conv_compl)
  also have "...  yT  -yT"
    by (metis assms(1) comp_associative comp_inf.mult_left_isotone comp_isotone comp_right_one mult_sub_right_one)
  finally have 3: "(z  yT * x) * (-z  -y  x)T  1"
    using pseudo_complement by fastforce
  have 4: "(-z  y  zT * x) * (z  yT * x)T  1"
    using 2 conv_dist_comp conv_order by force
  have 5: "(-z  y  zT * x) * (-z  y  zT * x)T  1"
    by (simp add: assms(2) inf_assoc inf_left_commute injective_inf_closed)
  have "(-z  y  zT * x) * (-z  -y  x)T  zT * x * (-zT  xT)"
    using comp_inf.mult_left_isotone comp_isotone conv_complement conv_dist_inf inf.cobounded1 inf.cobounded2 by auto
  also have "... = zT * x * xT  -zT"
    by (metis assms(4) covector_comp_inf inf.sup_monoid.add_commute vector_conv_compl)
  also have "...  zT  -zT"
    by (metis assms(1) comp_associative comp_inf.mult_left_isotone comp_isotone comp_right_one mult_sub_right_one)
  finally have 6: "(-z  y  zT * x) * (-z  -y  x)T  1"
    using pseudo_complement by fastforce
  have 7: "(-z  -y  x) * (z  yT * x)T  1"
    using 3 conv_dist_comp coreflexive_symmetric by fastforce
  have 8: "(-z  -y  x) * (-z  y  zT * x)T  1"
    using 6 conv_dist_comp coreflexive_symmetric by fastforce
  have 9: "(-z  -y  x) * (-z  -y  x)T  1"
    using assms(1) inf.sup_monoid.add_commute injective_inf_closed by auto
  have "(x[yx[[z]]])[zx[[y]]] = (z  yT * x)  (-z  y  zT * x)  (-z  -y  x)"
    by (simp add: comp_inf.comp_left_dist_sup conv_dist_comp inf_assoc sup_monoid.add_assoc)
  hence "((x[yx[[z]]])[zx[[y]]]) * ((x[yx[[z]]])[zx[[y]]])T = ((z  yT * x)  (-z  y  zT * x)  (-z  -y  x)) * ((z  yT * x)T  (-z  y  zT * x)T  (-z  -y  x)T)"
    by (simp add: conv_dist_sup)
  also have "... = (z  yT * x) * ((z  yT * x)T  (-z  y  zT * x)T  (-z  -y  x)T) 
                   (-z  y  zT * x) * ((z  yT * x)T  (-z  y  zT * x)T  (-z  -y  x)T) 
                   (-z  -y  x) * ((z  yT * x)T  (-z  y  zT * x)T  (-z  -y  x)T)"
    using mult_right_dist_sup by auto
  also have "... = (z  yT * x) * (z  yT * x)T  (z  yT * x) * (-z  y  zT * x)T  (z  yT * x) * (-z  -y  x)T 
                   (-z  y  zT * x) * (z  yT * x)T  (-z  y  zT * x) * (-z  y  zT * x)T  (-z  y  zT * x) * (-z  -y  x)T 
                   (-z  -y  x) * (z  yT * x)T  (-z  -y  x) * (-z  y  zT * x)T  (-z  -y  x) * (-z  -y  x)T"
    using mult_left_dist_sup sup.left_commute sup_commute by auto
  also have "...  1"
    using 1 2 3 4 5 6 7 8 9 by simp_all
  finally show ?thesis
    .
qed

lemma update_injective_swap_2:
  assumes "injective x"
    shows "injective ((x[yx[[bot]]])[botx[[y]]])"
  by (simp add: assms inf.sup_monoid.add_commute injective_inf_closed)

lemma update_univalent_swap:
  assumes "univalent x"
      and "injective y"
      and "vector y"
      and "injective z"
      and "vector z"
    shows "univalent ((x[yx[[z]]])[zx[[y]]])"
  by (simp add: assms read_injective update_univalent)

lemma update_mapping_swap:
  assumes "mapping x"
      and "point y"
      and "point z"
    shows "mapping ((x[yx[[z]]])[zx[[y]]])"
  by (simp add: assms bijective_regular read_injective read_surjective update_total update_univalent)

text ‹lemma mapping_inf_point_arc› has been moved to theory Relation_Algebras› in entry Stone_Relation_Algebras›

end

context stone_kleene_relation_algebra
begin

lemma omit_redundant_points_2:
  assumes "point p"
  shows "p  x = (p  1)  (p  x  -pT) * (x  -pT)"
proof -
  let ?p = "p  1"
  let ?np = "-p  1"
  have 1: "p  x  1 = p  1"
    by (metis inf.le_iff_sup inf.left_commute inf.sup_monoid.add_commute star.circ_reflexive)
  have 2: "p  1  -pT = bot"
    by (smt (z3) inf_bot_right inf_commute inf_left_commute one_inf_conv p_inf)
  have "p  x  -1 = p  x  -pT"
    by (metis assms antisymmetric_inf_diversity inf.cobounded1 inf.sup_relative_same_increasing vector_covector)
  also have "... = (p  1  -pT)  ((p  x) * (-p  x)  -pT)"
    by (simp add: assms omit_redundant_points comp_inf.semiring.distrib_right)
  also have "... = (p  x) * (-p  x)  -pT"
    using 2 by simp
  also have "... = ?p * x * (-p  x)  -pT"
    by (metis assms vector_export_comp_unit)
  also have "... = ?p * x * (?np * x)  -pT"
    by (metis assms vector_complement_closed vector_export_comp_unit)
  also have "... = ?p * x * (?np * x) * ?np"
    by (metis assms conv_complement covector_comp_inf inf.sup_monoid.add_commute mult_1_right one_inf_conv vector_conv_compl)
  also have "... = ?p * x * ?np * (x * ?np)"
    using star_slide mult_assoc by auto
  also have "... = (?p * x  -pT) * (x * ?np)"
    by (metis assms conv_complement covector_comp_inf inf.sup_monoid.add_commute mult_1_right one_inf_conv vector_conv_compl)
  also have "... = (?p * x  -pT) * (x  -pT)"
    by (metis assms conv_complement covector_comp_inf inf.sup_monoid.add_commute mult_1_right one_inf_conv vector_conv_compl)
  also have "... = (p  x  -pT) * (x  -pT)"
    by (metis assms vector_export_comp_unit)
  finally show ?thesis
    using 1 by (metis maddux_3_11_pp regular_one_closed)
qed

lemma omit_redundant_points_3:
  assumes "point p"
  shows "p  x = (p  1)  (p  (x  -pT)+)"
  by (simp add: assms inf_assoc vector_inf_comp omit_redundant_points_2)

lemma even_odd_root:
  assumes "acyclic (x - 1)"
      and "regular x"
      and "univalent x"
    shows "(x * x)T  xT * (x * x)T = (1  x) * ((x * x)T  xT * (x * x)T)"
proof -
  have 1: "univalent (x * x)"
    by (simp add: assms(3) univalent_mult_closed)
  have "x  1  top * (x  1)"
    by (simp add: top_left_mult_increasing)
  hence "x  -(top * (x  1))  x - 1"
    using assms(2) p_shunting_swap pp_dist_comp by auto
  hence "x * (x  -(top * (x  1)))  (x - 1) * (x - 1)"
    using mult_right_isotone reachable_without_loops by auto
  also have "...  -1"
    by (simp add: assms(1) star_plus)
  finally have "(x  -(top * (x  1)))T  -x"
    using schroeder_4_p by force
  hence "xT  x  (top * (x  1))T"
    by (smt (z3) assms(2) conv_complement conv_dist_inf p_shunting_swap regular_closed_inf regular_closed_top regular_mult_closed regular_one_closed)
  also have "... = (1  x) * top"
    by (metis conv_dist_comp conv_dist_inf inf_commute one_inf_conv symmetric_one_closed symmetric_top_closed)
  finally have 2: "(xT  x) * top  (1  x) * top"
    by (metis inf.orderE inf.orderI inf_commute inf_vector_comp)
  have "1  xT+  (xT  1 * x) * xT"
    by (metis conv_involutive conv_star_commute dedekind_2 inf_commute)
  also have "...  (xT  x) * top"
    by (simp add: mult_right_isotone)
  also have "...  (1  x) * top"
    using 2 by simp
  finally have 3: "1  xT+  (1  x) * top"
    .
  have "xT  (xT * xT)+ = 1 * xT  (xT * xT) * xT * xT"
    using star_plus mult_assoc by auto
  also have "... = (1  (xT * xT) * xT) * xT"
    using assms(3) injective_comp_right_dist_inf by force
  also have "...  (1  xT * xT) * xT"
    by (meson comp_inf.mult_right_isotone comp_isotone inf.eq_refl star.circ_square)
  also have "...  (1  x) * top * xT"
    using 3 by (simp add: mult_left_isotone star_plus)
  also have "...  (1  x) * top"
    by (simp add: comp_associative mult_right_isotone)
  finally have 4: "xT  (xT * xT)+  (1  x) * top"
    .
  have "xT  (xT * xT) = (xT  1)  (xT  (xT * xT)+)"
    by (metis inf_sup_distrib1 star_left_unfold_equal)
  also have "...  (1  x) * top"
    using 4 by (metis inf.sup_monoid.add_commute le_supI one_inf_conv top_right_mult_increasing)
  finally have 4: "xT  (xT * xT)  (1  x) * top"
    .
  have "xT  (x * x)  -1  xT  x  -1"
    by (simp add: inf.coboundedI2 inf.sup_monoid.add_commute star.circ_square)
  also have "... = (x - 1)  (x - 1)T"
    using conv_complement conv_dist_inf inf_assoc inf_left_commute reachable_without_loops symmetric_one_closed by auto
  also have "... = bot"
    using assms(1) acyclic_star_below_complement_1 by auto
  finally have 5: "xT  (x * x)  -1 = bot"
    by (simp add: le_bot)
  have "xT  (x * x) = (xT  (x * x)  1)  (xT  (x * x)  -1)"
    by (metis maddux_3_11_pp regular_one_closed)
  also have "... = xT  (x * x)  1"
    using 5 by simp
  also have "... = xT  1"
    by (metis calculation comp_inf.semiring.distrib_left inf.sup_monoid.add_commute star.circ_transitive_equal star_involutive star_left_unfold_equal sup_inf_absorb)
  finally have "(xT  (x * x))  (xT  (xT * xT))  (1  x) * top"
    using 4 inf.sup_monoid.add_commute one_inf_conv top_right_mult_increasing by auto
  hence "xT  ((x * x)  (x * x)T)  (1  x) * top"
    by (simp add: comp_inf.semiring.distrib_left conv_dist_comp)
  hence 6: "xT  (x * x)T * (x * x)  (1  x) * top"
    using 1 by (simp add: cancel_separate_eq sup_commute)
  have "(x * x)T  xT * (x * x)T  (xT  (x * x)T * (x * x)) * (x * x)T"
    by (metis conv_involutive conv_star_commute dedekind_2 inf_commute)
  also have "...  (1  x) * top * (x * x)T"
    using 6 by (simp add: mult_left_isotone)
  also have "... = (1  x) * top"
    by (simp add: comp_associative star.circ_left_top)
  finally have "(x * x)T  xT * (x * x)T = (x * x)T  xT * (x * x)T  (1  x) * top"
    using inf.order_iff by auto
  also have "... = (1  x) * ((x * x)T  xT * (x * x)T)"
    by (metis coreflexive_comp_top_inf inf.cobounded1 inf.sup_monoid.add_commute)
  finally show ?thesis
    .
qed

lemma update_square_plus:
  "point y  x[yx[[x[[y]]]]]  x+"
  by (meson update_square comp_isotone dual_order.trans le_supI order_refl star.circ_increasing star.circ_mult_increasing)

lemma update_square_ub_plus:
  "x[y(x * x)T]  x+"
  by (simp add: comp_isotone inf.coboundedI2 star.circ_increasing star.circ_mult_increasing)

lemma acyclic_square:
  assumes "acyclic (x - 1)"
    shows "x * x  1 = x  1"
proof (rule order.antisym)
  have "1  x * x = 1  ((x - 1) * x  (x  1) * x)"
    by (metis maddux_3_11_pp regular_one_closed semiring.distrib_right)
  also have "...  1  ((x - 1) * x  x)"
    by (metis inf.cobounded2 mult_1_left mult_left_isotone inf.sup_right_isotone semiring.add_left_mono)
  also have "... = 1  ((x - 1) * (x - 1)  (x - 1) * (x  1)  x)"
    by (metis maddux_3_11_pp mult_left_dist_sup regular_one_closed)
  also have "...  (1  (x - 1) * (x - 1))  (x - 1) * (x  1)  x"
    by (metis inf_le2 inf_sup_distrib1 semiring.add_left_mono sup_monoid.add_assoc)
  also have "...  (1  (x - 1)+)  (x - 1) * (x  1)  x"
    by (metis comp_isotone inf.eq_refl inf.sup_right_isotone star.circ_increasing sup_monoid.add_commute sup_right_isotone)
  also have "... = (x - 1) * (x  1)  x"
    by (metis assms inf.le_iff_sup inf.sup_monoid.add_commute inf_import_p inf_p regular_one_closed sup_inf_absorb sup_monoid.add_commute)
  also have "... = x"
    by (metis comp_isotone inf.cobounded1 inf_le2 mult_1_right sup.absorb2)
  finally show "x * x  1  x  1"
    by (simp add: inf.sup_monoid.add_commute)
  show "x  1  x * x  1"
    by (metis coreflexive_idempotent inf_le1 inf_le2 le_infI mult_isotone)
qed

lemma diagonal_update_square_aux:
  assumes "acyclic (x - 1)"
      and "point y"
    shows "1  y  yT * x * x = 1  y  x"
proof -
  have 1: "1  y  x  yT * x * x"
    by (metis comp_isotone coreflexive_idempotent inf.boundedE inf.cobounded1 inf.cobounded2 one_inf_conv)
  have "1  y  yT * x * x = 1  (y  yT) * x * x"
    by (simp add: assms(2) inf.sup_monoid.add_assoc vector_inf_comp)
  also have "... = 1  (y  1) * x * x"
    by (metis assms(2) inf.cobounded1 inf.sup_monoid.add_commute inf.sup_same_context one_inf_conv vector_covector)
  also have "...  1  x * x"
    by (metis comp_left_subdist_inf inf.sup_right_isotone le_infE mult_left_isotone mult_left_one)
  also have "...  x"
    using assms(1) acyclic_square inf.sup_monoid.add_commute by auto
  finally show ?thesis
    using 1 by (metis inf.absorb2 inf.left_commute inf.sup_monoid.add_commute)
qed

lemma diagonal_update_square:
  assumes "acyclic (x - 1)"
      and "point y"
    shows "(x[yx[[x[[y]]]]])  1 = x  1"
proof -
  let ?xy = "x[[y]]"
  let ?xxy = "x[[?xy]]"
  let ?xyxxy = "x[y?xxy]"
  have "?xyxxy  1 = ((y  yT * x * x)  (-y  x))  1"
    by (simp add: conv_dist_comp)
  also have "... = (y  yT * x * x  1)  (-y  x  1)"
    by (simp add: inf_sup_distrib2)
  also have "... = (y  x  1)  (-y  x  1)"
    using assms by (smt (verit, ccfv_threshold) diagonal_update_square_aux find_set_precondition_def inf_assoc inf_commute)
  also have "... = x  1"
    by (metis assms(2) bijective_regular comp_inf.mult_right_dist_sup inf.sup_monoid.add_commute maddux_3_11_pp)
  finally show ?thesis
    .
qed

lemma fc_update_square:
  assumes "mapping x"
      and "point y"
    shows "fc (x[yx[[x[[y]]]]]) = fc x"
proof (rule order.antisym)
  let ?xy = "x[[y]]"
  let ?xxy = "x[[?xy]]"
  let ?xyxxy = "x[y?xxy]"
  have 1: "y  yT * x * x  x * x"
    by (smt (z3) assms(2) inf.cobounded2 inf.sup_monoid.add_commute inf.sup_same_context mult_1_left one_inf_conv vector_covector vector_inf_comp)
  have 2: "?xyxxy = (y  yT * x * x)  (-y  x)"
    by (simp add: conv_dist_comp)
  also have "...  x * x  x"
    using 1 inf_le2 sup_mono by blast
  also have "...  x"
    by (simp add: star.circ_increasing star.circ_mult_upper_bound)
  finally show "fc ?xyxxy  fc x"
    by (metis comp_isotone conv_order conv_star_commute star_involutive star_isotone)
  have 3: "y  x  1  fc ?xyxxy"
    using inf.coboundedI1 inf.sup_monoid.add_commute reflexive_mult_closed star.circ_reflexive by auto
  have 4: "y - 1  -yT"
    using assms(2) p_shunting_swap regular_one_closed vector_covector by auto
  have "y  x  yT * x"
    by (simp add: assms(2) vector_restrict_comp_conv)
  also have "...  yT * x * x * xT"
    by (metis assms(1) comp_associative mult_1_right mult_right_isotone total_var)
  finally have "y  x  -1  y  -yT  yT * x * x * xT"
    using 4 by (smt (z3) inf.cobounded1 inf.coboundedI2 inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_greatest)
  also have "... = (y  yT * x * x) * xT  -yT"
    by (metis assms(2) inf.sup_monoid.add_assoc inf.sup_monoid.add_commute vector_inf_comp)
  also have "... = (y  yT * x * x) * (xT  -yT)"
    using assms(2) covector_comp_inf vector_conv_compl by auto
  also have "... = (y  yT * x * x) * (-y  x)T"
    by (simp add: conv_complement conv_dist_inf inf_commute)
  also have "...  ?xyxxy * (-y  x)T"
    using 2 by (simp add: comp_left_increasing_sup)
  also have "...  ?xyxxy * ?xyxxyT"
    by (simp add: conv_isotone mult_right_isotone)
  also have "...  fc ?xyxxy"
    using comp_isotone star.circ_increasing by blast
  finally have 5: "y  x  fc ?xyxxy"
    using 3 by (smt (z3) comp_inf.semiring.distrib_left inf.le_iff_sup maddux_3_11_pp regular_one_closed)
  have "x = (y  x)  (-y  x)"
    by (metis assms(2) bijective_regular inf.sup_monoid.add_commute maddux_3_11_pp)
  also have "...  fc ?xyxxy"
    using 5 dual_order.trans fc_increasing sup.cobounded2 sup_least by blast
  finally show "fc x  fc ?xyxxy"
    by (smt (z3) assms fc_equivalence fc_isotone fc_wcc read_injective star.circ_decompose_9 star_decompose_1 update_univalent)
qed

lemma acyclic_plus_loop:
  assumes "acyclic (x - 1)"
  shows "x+  1 = x  1"
proof -
  let ?r = "x  1"
  let ?i = "x - 1"
  have "x+  1 = (?i  ?r)+  1"
    by (metis maddux_3_11_pp regular_one_closed)
  also have "... = ((?i * ?r) * ?i+  (?i * ?r)+)  1"
    using plus_sup by auto
  also have "...  (?i+  (?i * ?r)+)  1"
    by (metis comp_associative dual_order.eq_iff maddux_3_11_pp reachable_without_loops regular_one_closed star.circ_plus_same star.circ_sup_9)
  also have "... = (?i * ?r)+  1"
    by (smt (z3) assms comp_inf.mult_right_dist_sup inf.absorb2 inf.sup_monoid.add_commute inf_le2 maddux_3_11_pp pseudo_complement regular_one_closed)
  also have "...  ?i * ?r  1"
    by (metis comp_associative dual_order.eq_iff maddux_3_11_pp reachable_without_loops regular_one_closed star.circ_sup_9 star_slide)
  also have "... = (?r  ?i+ * ?r)  1"
    using comp_associative star.circ_loop_fixpoint sup_commute by force
  also have "...  x  (?i+ * ?r  1)"
    by (metis comp_inf.mult_right_dist_sup inf.absorb1 inf.cobounded1 inf.cobounded2)
  also have "...  x  (-1 * ?r  1)"
    by (meson assms comp_inf.comp_isotone mult_left_isotone order.refl semiring.add_left_mono)
  also have "... = x"
    by (metis comp_inf.semiring.mult_not_zero comp_right_one inf.cobounded2 inf_sup_absorb mult_right_isotone pseudo_complement sup.idem sup_inf_distrib1)
  finally show ?thesis
    by (meson inf.sup_same_context inf_le1 order_trans star.circ_mult_increasing)
qed

lemma star_irreflexive_part_eq:
  "x - 1 = (x - 1)+ - 1"
  by (metis reachable_without_loops star_plus_without_loops)

lemma star_irreflexive_part:
  "x - 1  (x - 1)+"
  using star_irreflexive_part_eq by auto

lemma square_irreflexive_part:
  "x * x - 1  (x - 1)+"
proof -
  have "x * x = (x  1) * x  (x - 1) * x"
    by (metis maddux_3_11_pp mult_right_dist_sup regular_one_closed)
  also have "...  1 * x  (x - 1) * x"
    using comp_isotone inf.cobounded2 semiring.add_right_mono by blast
  also have "...  1  (x - 1)  (x - 1) * x"
    by (metis inf.cobounded2 maddux_3_11_pp mult_1_left regular_one_closed sup_left_isotone)
  also have "... = (x - 1) * (x  1)  1"
    by (simp add: mult_left_dist_sup sup_assoc sup_commute)
  finally have "x * x - 1  (x - 1) * (x  1)"
    using shunting_var_p by auto
  also have "... = (x - 1) * (x - 1)  (x - 1)"
    by (metis comp_right_one inf.sup_monoid.add_commute maddux_3_21_pp mult_left_dist_sup regular_one_closed sup_commute)
  also have "...  (x - 1)+"
    by (metis mult_left_isotone star.circ_increasing star.circ_mult_increasing star.circ_plus_same sup.bounded_iff)
  finally show ?thesis
    .
qed

lemma square_irreflexive_part_2:
  "x * x - 1  x - 1"
  using comp_inf.mult_left_isotone star.circ_increasing star.circ_mult_upper_bound by blast

lemma acyclic_update_square:
  assumes "acyclic (x - 1)"
  shows "acyclic ((x[y(x * x)T]) - 1)"
proof -
  have "((x[y(x * x)T]) - 1)+  ((x  x * x) - 1)+"
    by (metis comp_inf.mult_right_isotone comp_isotone inf.sup_monoid.add_commute star_isotone update_square_ub)
  also have "... = ((x - 1)  (x * x - 1))+"
    using comp_inf.semiring.distrib_right by auto
  also have "...  ((x - 1)+)+"
    by (smt (verit, del_insts) comp_isotone reachable_without_loops star.circ_mult_increasing star.circ_plus_same star.circ_right_slide star.circ_separate_5 star.circ_square star.circ_transitive_equal star.left_plus_circ sup.bounded_iff sup_ge1 square_irreflexive_part)
  also have "...  -1"
    using assms by (simp add: acyclic_plus)
  finally show ?thesis
    .
qed

lemma disjoint_set_forest_update_square:
  assumes "disjoint_set_forest x"
      and "vector y"
      and "regular y"
    shows "disjoint_set_forest (x[y(x * x)T])"
proof (intro conjI)
  show "univalent (x[y(x * x)T])"
    using assms update_univalent mapping_mult_closed univalent_conv_injective by blast
  show "total (x[y(x * x)T])"
    using assms update_total total_conv_surjective total_mult_closed by blast
  show "acyclic ((x[y(x * x)T]) - 1)"
    using acyclic_update_square assms(1) by blast
qed

lemma disjoint_set_forest_update_square_point:
  assumes "disjoint_set_forest x"
      and "point y"
    shows "disjoint_set_forest (x[y(x * x)T])"
  using assms disjoint_set_forest_update_square bijective_regular by blast

end

section ‹Verifying Further Operations on Disjoint-Set Forests›

text ‹
In this section we verify the init-sets, path-halving and path-splitting operations of disjoint-set forests.
›

class choose_point =
  fixes choose_point :: "'a  'a"

text ‹
Using the choose_point› operation we define a simple for-each-loop abstraction as syntactic sugar translated to a while-loop.
Regular vector h› describes the set of all elements that are yet to be processed.
It is made explicit so that the invariant can refer to it.
›

syntax
  "_Foreach" :: "idt  idt  'assn  'com  'com"  ("(1FOREACH _/ USING _/ INV {_} //DO _ /OD)" [0,0,0,0] 61)
translations "FOREACH x USING h INV { i } DO c OD" =>
  "h := CONST top;
   WHILE h  CONST bot
     INV { CONST regular h  CONST vector h  i }
     VAR { h }
      DO x := CONST choose_point h;
         c;
         h[x] := CONST bot
      OD"

class stone_kleene_relation_algebra_choose_point_finite_regular = stone_kleene_relation_algebra + finite_regular_p_algebra + choose_point +
  assumes choose_point_point: "vector x  x  bot  point (choose_point x)"
  assumes choose_point_decreasing: "choose_point x  --x"
begin

subclass stone_kleene_relation_algebra_tarski_finite_regular
proof unfold_locales
  fix x
  let ?p = "choose_point (x * top)"
  let ?q = "choose_point ((?p  x)T * top)"
  let ?y = "?p  ?qT"
  assume 1: "regular x" "x  bot"
  hence 2: "x * top  bot"
    using le_bot top_right_mult_increasing by auto
  hence 3: "point ?p"
    by (simp add: choose_point_point comp_associative)
  hence 4: "?p  bot"
    using 2 mult_right_zero by force
  have "?p  x  bot"
  proof
    assume "?p  x = bot"
    hence 5: "x  -?p"
      using p_antitone_iff pseudo_complement by auto
    have "?p  --(x * top)"
      by (simp add: choose_point_decreasing)
    also have "...  --(-?p * top)"
      using 5 by (simp add: comp_isotone pp_isotone)
    also have "... = -?p * top"
      using regular_mult_closed by auto
    also have "... = -?p"
      using 3 vector_complement_closed by auto
    finally have "?p = bot"
      using inf_absorb2 by fastforce
    thus False
      using 4 by auto
  qed
  hence "(?p  x)T * top  bot"
    by (metis comp_inf.semiring.mult_zero_left comp_right_one inf.sup_monoid.add_commute inf_top.left_neutral schroeder_1)
  hence "point ?q"
    using choose_point_point vector_top_closed mult_assoc by auto
  hence 6: "arc ?y"
    using 3 by (smt bijective_conv_mapping inf.sup_monoid.add_commute mapping_inf_point_arc)
  have "?q  --((?p  x)T * top)"
    by (simp add: choose_point_decreasing)
  hence "?y  ?p  --((?p  x)T * top)T"
    by (metis conv_complement conv_isotone inf.sup_right_isotone)
  also have "... = ?p  --(top * (?p  x))"
    by (simp add: conv_dist_comp)
  also have "... = ?p  top * (?p  x)"
    using 1 3 bijective_regular pp_dist_comp by auto
  also have "... = ?p  ?pT * x"
    using 3 by (metis comp_inf_vector conv_dist_comp inf.sup_monoid.add_commute inf_top_right symmetric_top_closed)
  also have "... = (?p  ?pT) * x"
    using 3 by (simp add: vector_inf_comp)
  also have "...  1 * x"
    using 3 point_antisymmetric mult_left_isotone by blast
  finally have "?y  x"
    by simp
  thus "top * x * top = top"
    using 6 by (smt (verit, ccfv_SIG) mult_assoc le_iff_sup mult_left_isotone semiring.distrib_left sup.orderE top.extremum)
qed

subsection ‹Init-Sets›

text ‹
A disjoint-set forest is initialised by applying make_set› to each node.
We prove that the resulting disjoint-set forest is the identity relation.
›

theorem init_sets:
  "VARS h p x
  [ True ]
  FOREACH x
    USING h
      INV { p - h = 1 - h }
       DO p := make_set p x
       OD
  [ p = 1  disjoint_set_forest p  h = bot ]"
proof vcg_tc_simp
  fix h p
  let ?x = "choose_point h"
  let ?m = "make_set p ?x"
  assume 1: "regular h  vector h  p - h = 1 - h  h  bot"
  show "vector (-?x  h) 
        ?m  (--?x  -h) = 1  (--?x  -h) 
        card { x . regular x  x  -?x  x  h } < h"
  proof (intro conjI)
    show "vector (-?x  h)"
      using 1 choose_point_point vector_complement_closed vector_inf_closed by blast
    have 2: "point ?x  regular ?x"
      using 1 bijective_regular choose_point_point by blast
    have 3: "-h  -?x"
      using choose_point_decreasing p_antitone_iff by auto
    have 4: "?x  ?m = ?x * ?xT  -?x  ?m = -?x  p"
      using 1 choose_point_point make_set_function make_set_postcondition_def by auto
    have "?m  (--?x  -h) = (?m  ?x)  (?m - h)"
      using 2 comp_inf.comp_left_dist_sup by auto
    also have "... = ?x * ?xT  (?m  -?x  -h)"
      using 3 4 by (smt (z3) inf_absorb2 inf_assoc inf_commute)
    also have "... = ?x * ?xT  (1 - h)"
      using 1 3 4 inf.absorb2 inf.sup_monoid.add_assoc inf_commute by auto
    also have "... = (1  ?x)  (1 - h)"
      using 2 by (metis inf.cobounded2 inf.sup_same_context one_inf_conv vector_covector)
    also have "... = 1  (--?x  -h)"
      using 2 comp_inf.semiring.distrib_left by auto
    finally show "?m  (--?x  -h) = 1  (--?x  -h)"
      .
    have 5: "¬ ?x  -?x"
      using 1 2 by (metis comp_commute_below_diversity conv_order inf.cobounded2 inf_absorb2 pseudo_complement strict_order_var top.extremum)
    have 6: "?x  h"
      using 1 by (metis choose_point_decreasing)
    show "card { x . regular x  x  -?x  x  h } < h"
      apply (rule psubset_card_mono)
      using finite_regular apply simp
      using 2 5 6 by auto
  qed
qed

end

subsection ‹Path Halving›

text ‹
Path halving is a variant of the path compression technique.
Similarly to path compression, we implement path halving independently of find-set, using a second while-loop which iterates over the same path to the root.
We prove that path halving preserves the equivalence-relational semantics of the disjoint-set forest and also preserves the roots of the component trees.
Additionally we prove the exact effect of path halving, which is to replace every other parent pointer with a pointer to the respective grandparent.
›

context stone_kleene_relation_algebra_tarski_finite_regular
begin

definition "path_halving_invariant p x y p0  
  find_set_precondition p x  point y  y  pT * x  y  (p0 * p0)T * x 
  p0[(p0 * p0)T * x - p0T * y(p0 * p0)T] = p 
  disjoint_set_forest p0"
definition "path_halving_postcondition p x y p0  
  disjoint_set_forest p  y = root p x  p  1 = p0  1  fc p = fc p0 
  p0[(p0 * p0)T * x(p0 * p0)T] = p"

lemma path_halving_invariant_aux_1:
  assumes "point x"
      and "point y"
      and "disjoint_set_forest p0"
  shows "p0  wcc (p0[(p0 * p0)T * x - p0T * y(p0 * p0)T])"
proof -
  let ?p2 = "p0 * p0"
  let ?p2t = "?p2T"
  let ?p2ts = "?p2t"
  let ?px = "?p2ts * x"
  let ?py = "-(p0T * y)"
  let ?pxy = "?px  ?py"
  let ?p = "p0[?pxy?p2t]"
  have 1: "regular ?pxy"
    using assms(1,3) bijective_regular find_set_precondition_def mapping_regular pp_dist_comp regular_closed_star regular_conv_closed path_halving_invariant_def by auto
  have 2: "vector x  vector ?px  vector ?py"
    using assms(1,2) find_set_precondition_def vector_complement_closed vector_mult_closed path_halving_invariant_def by auto
  have 3: "?pxy  p0  -?p2  -?pxT"
  proof -
    have 4: "injective x  univalent ?p2  regular p0"
      using assms(1,3) find_set_precondition_def mapping_regular univalent_mult_closed path_halving_invariant_def by auto
    have "?p2 * p0  1  p0+  1"
      using comp_inf.mult_left_isotone comp_isotone comp_right_one mult_sub_right_one star.circ_square star_slide by auto
    also have "...  p0"
      using acyclic_plus_loop assms(3) path_halving_invariant_def by auto
    finally have 5: "?p2 * p0  1  p0"
      .
    hence 6: "?p2ts * (1 - p0)  -p0"
      by (smt (verit, ccfv_SIG) conv_star_commute dual_order.trans inf.sup_monoid.add_assoc order.refl p_antitone_iff pseudo_complement schroeder_4_p schroeder_6_p)
    have "?p2t+ * p0  1 = ?p2ts * p0T * (p0T * p0)  1"
      by (metis conv_dist_comp star_plus mult_assoc)
    also have "...  ?p2ts * p0T  1"
      by (metis assms(3) comp_inf.mult_left_isotone comp_isotone comp_right_one mult_sub_right_one)
    also have "...  p0"
      using 5 by (metis conv_dist_comp conv_star_commute inf_commute one_inf_conv star_slide)
    finally have "?p2t+ * p0  -1  p0"
      by (metis regular_one_closed shunting_var_p sup_commute)
    hence 7: "?p2+ * (1 - p0)  -p0"
      by (smt (z3) conv_dist_comp conv_star_commute half_shunting inf.sup_monoid.add_assoc inf.sup_monoid.add_commute pseudo_complement schroeder_4_p schroeder_6_p star.circ_plus_same)
    have "(1  ?px) * top * (1  ?px  -p0) = ?px  top * (1  ?px  -p0)"
      using 2 by (metis inf_commute vector_inf_one_comp mult_assoc)
    also have "... = ?px  ?pxT * (1 - p0)"
      using 2 by (smt (verit, ccfv_threshold) covector_inf_comp_3 inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_top.left_neutral)
    also have "... = ?px  xT * ?p2 * (1 - p0)"
      by (simp add: conv_dist_comp conv_star_commute)
    also have "... = (?px  xT) * ?p2 * (1 - p0)"
      using 2 vector_inf_comp by auto
    also have "... = ?p2ts * (x * xT) * ?p2 * (1 - p0)"
      using 2 vector_covector mult_assoc by auto
    also have "...  ?p2ts * ?p2 * (1 - p0)"
      using 4 by (metis inf.order_lesseq_imp mult_left_isotone star.circ_mult_upper_bound star.circ_reflexive)
    also have "... = (?p2ts  ?p2) * (1 - p0)"
      using 4 by (simp add: cancel_separate_eq)
    also have "... = (?p2ts  ?p2+) * (1 - p0)"
      by (metis star.circ_plus_one star_plus_loops sup_assoc sup_commute)
    also have "...  -p0"
      using 6 7 by (simp add: mult_right_dist_sup)
    finally have "(1  ?px)T * p0 * (1  ?px  -p0)T  bot"
      by (smt (z3) inf.boundedI inf_p top.extremum triple_schroeder_p)
    hence 8: "(1  ?px) * p0 * (1  ?px  -p0) = bot"
      by (simp add: coreflexive_inf_closed coreflexive_symmetric le_bot)
    have "?px  p0  ?pxT = (1  ?px) * p0  ?pxT"
      using 2 inf_commute vector_inf_one_comp by fastforce
    also have "... = (1  ?px) * p0 * (1  ?px)"
      using 2 by (metis comp_inf_vector mult_1_right vector_conv_covector)
    also have "... = (1  ?px) * p0 * (1  ?px  p0)  (1  ?px) * p0 * (1  ?px  -p0)"
      using 4 by (metis maddux_3_11_pp mult_left_dist_sup)
    also have "... = (1  ?px) * p0 * (1  ?px  p0)"
      using 8 by simp
    also have "...  ?p2"
      by (metis comp_isotone coreflexive_comp_top_inf inf.cobounded1 inf.cobounded2)
    finally have "?px  p0  -?p2  -?pxT"
      using 4 p_shunting_swap regular_mult_closed by fastforce
    thus ?thesis
      by (meson comp_inf.mult_left_isotone dual_order.trans inf.cobounded1)
  qed
  have "p0  ?p2 * p0T"
    by (metis assms(3) comp_associative comp_isotone comp_right_one eq_refl total_var)
  hence "?pxy  p0  -?p2  ?p2 * p0T"
    by (metis inf.coboundedI1 inf.sup_monoid.add_commute)
  hence "?pxy  p0  -?p2  ?pxy  ?p2 * p0T  -?pxT"
    using 3 by (meson dual_order.trans inf.boundedI inf.cobounded1)
  also have "... = (?pxy  ?p2) * p0T  -?pxT"
    using 2 vector_inf_comp by auto
  also have "... = (?pxy  ?p2) * (-?px  p0)T"
    using 2 by (simp add: covector_comp_inf inf.sup_monoid.add_commute vector_conv_compl conv_complement conv_dist_inf)
  also have "...  ?p * (-?px  p0)T"
    using comp_left_increasing_sup by auto
  also have "...  ?p * ?pT"
    by (metis comp_inf.mult_right_isotone comp_isotone conv_isotone inf.eq_refl inf.sup_monoid.add_commute le_supI1 p_antitone_inf sup_commute)
  also have "...  wcc ?p"
    using star.circ_sub_dist_2 by auto
  finally have 9: "?pxy  p0  -?p2  wcc ?p"
    .
  have "p0 = (?pxy  p0)  (-?pxy  p0)"
    using 1 by (metis inf.sup_monoid.add_commute maddux_3_11_pp)
  also have "...  (?pxy  p0)  ?p"
    using sup_right_isotone by auto
  also have "... = (?pxy  p0  -?p2)  (?pxy  p0  ?p2)  ?p"
    by (smt (z3) assms(3) maddux_3_11_pp mapping_regular pp_dist_comp path_halving_invariant_def)
  also have "...  (?pxy  p0  -?p2)  (?pxy  ?p2)  ?p"
    by (meson comp_inf.comp_left_subdist_inf inf.boundedE semiring.add_left_mono semiring.add_right_mono)
  also have "... = (?pxy  p0  -?p2)  ?p"
    using sup_assoc by auto
  also have "...  wcc ?p  ?p"
    using 9 sup_left_isotone by blast
  also have "...  wcc ?p"
    by (simp add: star.circ_sub_dist_1)
  finally show ?thesis
    .
qed

lemma path_halving_invariant_aux:
  assumes "path_halving_invariant p x y p0"
  shows "p[[y]] = p0[[y]]"
    and "p[[p[[y]]]] = p0[[p0[[y]]]]"
    and "p[[p[[p[[y]]]]]] = p0[[p0[[p0[[y]]]]]]"
    and "p  1 = p0  1"
    and "fc p = fc p0"
proof -
  let ?p2 = "p0 * p0"
  let ?p2t = "?p2T"
  let ?p2ts = "?p2t"
  let ?px = "?p2ts * x"
  let ?py = "-(p0T * y)"
  let ?pxy = "?px  ?py"
  let ?p = "p0[?pxy?p2t]"
  have "?p[[y]] = p0[[y]]"
    apply (rule put_get_different_vector)
    using assms find_set_precondition_def vector_complement_closed vector_inf_closed vector_mult_closed path_halving_invariant_def apply force
    by (meson inf.cobounded2 order_lesseq_imp p_antitone_iff path_compression_1b)
  thus 1: "p[[y]] = p0[[y]]"
    using assms path_halving_invariant_def by auto
  have "?p[[p0[[y]]]] = p0[[p0[[y]]]]"
    apply (rule put_get_different_vector)
    using assms find_set_precondition_def vector_complement_closed vector_inf_closed vector_mult_closed path_halving_invariant_def apply force
    by (metis comp_isotone inf.boundedE inf.coboundedI2 inf.eq_refl p_antitone_iff selection_closed_id star.circ_increasing)
  thus 2: "p[[p[[y]]]] = p0[[p0[[y]]]]"
    using 1 assms path_halving_invariant_def by auto
  have "?p[[p0[[p0[[y]]]]]] = p0[[p0[[p0[[y]]]]]]"
    apply (rule put_get_different_vector)
    using assms find_set_precondition_def vector_complement_closed vector_inf_closed vector_mult_closed path_halving_invariant_def apply force
    by (metis comp_associative comp_isotone conv_dist_comp conv_involutive conv_order inf.coboundedI2 inf.le_iff_sup mult_left_isotone p_antitone_iff p_antitone_inf star.circ_increasing star.circ_transitive_equal)
  thus "p[[p[[p[[y]]]]]] = p0[[p0[[p0[[y]]]]]]"
    using 2 assms path_halving_invariant_def by auto
  have 3: "regular ?pxy"
    using assms bijective_regular find_set_precondition_def mapping_regular pp_dist_comp regular_closed_star regular_conv_closed path_halving_invariant_def by auto
  have "p  1 = ?p  1"
    using assms path_halving_invariant_def by auto
  also have "... = (?pxy  ?p2  1)  (-?pxy  p0  1)"
    using comp_inf.semiring.distrib_right conv_involutive by auto
  also have "... = (?pxy  p0  1)  (-?pxy  p0  1)"
    using assms acyclic_square path_halving_invariant_def inf.sup_monoid.add_assoc by auto
  also have "... = (?pxy  -?pxy)  p0  1"
    using inf_sup_distrib2 by auto
  also have "... = p0  1"
    using 3 by (metis inf.sup_monoid.add_commute inf_sup_distrib1 maddux_3_11_pp)
  finally show "p  1 = p0  1"
    .
  have "p  p0+"
    by (metis assms path_halving_invariant_def update_square_ub_plus)
  hence 4: "fc p  fc p0"
    using conv_plus_commute fc_isotone star.left_plus_circ by fastforce
  have "wcc p0  wcc ?p"
    by (meson assms wcc_below_wcc path_halving_invariant_aux_1 path_halving_invariant_def find_set_precondition_def)
  hence "fc p0  fc ?p"
    using assms find_set_precondition_def path_halving_invariant_def fc_wcc by auto
  thus "fc p = fc p0"
    using 4 assms path_halving_invariant_def by auto
qed

lemma path_halving_1:
  "find_set_precondition p0 x  path_halving_invariant p0 x x p0"
proof -
  assume 1: "find_set_precondition p0 x"
  show "path_halving_invariant p0 x x p0"
  proof (unfold path_halving_invariant_def, intro conjI)
    show "find_set_precondition p0 x"
      using 1 by simp
    show "vector x" "injective x" "surjective x"
      using 1 find_set_precondition_def by auto
    show "x  p0T * x"
      by (simp add: path_compression_1b)
    show "x  (p0 * p0)T * x"
      by (simp add: path_compression_1b)
    have "(p0 * p0)T * x  p0T * x"
      by (simp add: conv_dist_comp mult_left_isotone star.circ_square)
    thus "p0[(p0 * p0)T * x - p0T * x(p0 * p0)T] = p0"
      by (smt (z3) inf.le_iff_sup inf_commute maddux_3_11_pp p_antitone_inf pseudo_complement)
    show "univalent p0" "total p0" "acyclic (p0 - 1)"
      using 1 find_set_precondition_def by auto
  qed
qed

lemma path_halving_2:
  "path_halving_invariant p x y p0  y  p[[y]]  path_halving_invariant (p[yp[[p[[y]]]]]) x ((p[yp[[p[[y]]]]])[[y]]) p0  ((p[yp[[p[[y]]]]])T * ((p[yp[[p[[y]]]]])[[y]])) < (pT * y)"
proof -
  let ?py = "p[[y]]"
  let ?ppy = "p[[?py]]"
  let ?pyppy = "p[y?ppy]"
  let ?p2 = "p0 * p0"
  let ?p2t = "?p2T"
  let ?p2ts = "?p2t"
  let ?px = "?p2ts * x"
  let ?py2 = "-(p0T * y)"
  let ?pxy = "?px  ?py2"
  let ?p = "p0[?pxy?p2t]"
  let ?pty = "p0T * y"
  let ?pt2y = "p0T * p0T * y"
  let ?pt2sy = "p0T * p0T * p0T * y"
  assume 1: "path_halving_invariant p x y p0  y  ?py"
  have 2: "point ?pty  point ?pt2y"
    using 1 by (smt (verit) comp_associative read_injective read_surjective path_halving_invariant_def)
  show "path_halving_invariant ?pyppy x (?pyppy[[y]]) p0  (?pyppyT * (?pyppy[[y]])) < (pT * y)"
  proof
    show "path_halving_invariant ?pyppy x (?pyppy[[y]]) p0"
    proof (unfold path_halving_invariant_def, intro conjI)
      show 3: "find_set_precondition ?pyppy x"
      proof (unfold find_set_precondition_def, intro conjI)
        show "univalent ?pyppy"
          using 1 find_set_precondition_def read_injective update_univalent path_halving_invariant_def by auto
        show "total ?pyppy"
          using 1 bijective_regular find_set_precondition_def read_surjective update_total path_halving_invariant_def by force
        show "acyclic (?pyppy - 1)"
          apply (rule update_acyclic_3)
          using 1 find_set_precondition_def path_halving_invariant_def apply blast
          using 1 2 comp_associative path_halving_invariant_aux(2) apply force
          using 1 path_halving_invariant_def apply blast
          by (metis inf.order_lesseq_imp mult_isotone star.circ_increasing star.circ_square mult_assoc)
        show "vector x" "injective x" "surjective x"
          using 1 find_set_precondition_def path_halving_invariant_def by auto
      qed
      show "vector (?pyppy[[y]])"
        using 1 comp_associative path_halving_invariant_def by auto
      show "injective (?pyppy[[y]])"
        using 1 3 read_injective path_halving_invariant_def find_set_precondition_def by auto
      show "surjective (?pyppy[[y]])"
        using 1 3 read_surjective path_halving_invariant_def find_set_precondition_def by auto
      show "?pyppy[[y]]  ?pyppyT * x"
      proof -
        have "y = (y  pT) * x"
          using 1 le_iff_inf vector_inf_comp path_halving_invariant_def by auto
        also have "... = ((y  1)  (y  (pT  -yT)+)) * x"
          using 1 omit_redundant_points_3 path_halving_invariant_def by auto
        also have "...  (1  (y  (pT  -yT)+)) * x"
          using 1 sup_inf_distrib2 vector_inf_comp path_halving_invariant_def by auto
        also have "...  (1  (pT  -yT)+) * x"
          by (simp add: inf.coboundedI2 mult_left_isotone)
        also have "... = (p  -y)T * x"
          by (simp add: conv_complement conv_dist_inf star_left_unfold_equal)
        also have "...  ?pyppyT * x"
          by (simp add: conv_isotone inf.sup_monoid.add_commute mult_left_isotone star_isotone)
        finally show ?thesis
          by (metis mult_isotone star.circ_increasing star.circ_transitive_equal mult_assoc)
      qed
      show "?pyppy[[y]]  ?px"
      proof -
        have "?pyppy[[y]] = p[[?py]]"
          using 1 put_get vector_mult_closed path_halving_invariant_def by force
        also have "... = p0[[p0[[y]]]]"
          using 1 path_halving_invariant_aux(2) by blast
        also have "... = ?p2t * y"
          by (simp add: conv_dist_comp mult_assoc)
        also have "...  ?p2t * ?px"
          using 1 path_halving_invariant_def comp_associative mult_right_isotone by force
        also have "...  ?px"
          by (metis comp_associative mult_left_isotone star.left_plus_below_circ)
        finally show ?thesis
          .
      qed
      show "p0[?px - p0T * (?pyppy[[y]])?p2t] = ?pyppy"
      proof -
        have "?px  ?pty = ?px  p0T * ?px  ?pty"
          using 1 inf.absorb2 inf.sup_monoid.add_assoc mult_right_isotone path_halving_invariant_def by force
        also have "... = (?p2ts  p0T * ?p2ts) * x  ?pty"
          using 3 comp_associative find_set_precondition_def injective_comp_right_dist_inf by auto
        also have "... = (1  p0) * (?p2ts  p0T * ?p2ts) * x  ?pty"
          using 1 even_odd_root mapping_regular path_halving_invariant_def by auto
        also have "...  (1  p0) * top  ?pty"
          by (metis comp_associative comp_inf.mult_left_isotone comp_inf.star.circ_sub_dist_2 comp_left_subdist_inf dual_order.trans mult_right_isotone)
        also have 4: "... = (1  p0T) * ?pty"
          using coreflexive_comp_top_inf one_inf_conv by auto
        also have "...  ?pt2y"
          by (simp add: mult_assoc mult_left_isotone)
        finally have 5: "?px  ?pty  ?pt2y"
          .
        have 6: "p[?px  -?pt2sy  ?pty?p2t] = p"
        proof (cases "?pty  ?px  -?pt2sy")
          case True
          hence "?pty  ?pt2y"
            using 5 conv_dist_comp inf.absorb2 by auto
          hence 7: "?pty = ?pt2y"
            using 2 epm_3 by fastforce
          have "p[?px  -?pt2sy  ?pty?p2t] = p[?pty?p2t]"
            using True inf.absorb2 by auto
          also have "... = p[?pty?p2[[?pty]]]"
            using 2 update_point_get by auto
          also have "... = p[?ptyp0T * p0T * p0T * y]"
            using comp_associative conv_dist_comp by auto
          also have "... = p[?pty?pt2y]"
            using 7 mult_assoc by simp
          also have "... = p[?ptyp[[?pty]]]"
            using 1 path_halving_invariant_aux(1,2) mult_assoc by force
          also have "... = p"
            using 2 get_put by auto
          finally show ?thesis
            .
        next
          case False
          have "mapping ?p2"
            using 1 mapping_mult_closed path_halving_invariant_def by blast
          hence 8: "regular (?px  -?pt2sy)"
            using 1 bijective_regular find_set_precondition_def mapping_regular pp_dist_comp regular_closed_star regular_conv_closed path_halving_invariant_def by auto
          have "vector (?px  -?pt2sy)"
            using 1 find_set_precondition_def vector_complement_closed vector_inf_closed vector_mult_closed path_halving_invariant_def by force
          hence "?pty  -(?px  -?pt2sy)"
            using 2 8 point_in_vector_or_complement False by blast
          hence "?px  -?pt2sy  ?pty = bot"
            by (simp add: p_antitone_iff pseudo_complement)
          thus ?thesis
            by simp
        qed
        have 9: "p[?px  -?pt2sy  y?p2t] = ?pyppy"
        proof (cases "y  -?pt2sy")
          case True
          hence "p[?px  -?pt2sy  y?p2t] = p[y?p2t]"
            using 1 inf.absorb2 path_halving_invariant_def by auto
          also have "... = ?pyppy"
            using 1 by (metis comp_associative conv_dist_comp path_halving_invariant_aux(2) path_halving_invariant_def update_point_get)
          finally show ?thesis
            .
        next
          case False
          have "vector (-?pt2sy)"
            using 1 vector_complement_closed vector_mult_closed path_halving_invariant_def by blast
          hence 10: "y  ?pt2sy"
            using 1 by (smt (verit, del_insts) False bijective_regular point_in_vector_or_complement regular_closed_star regular_mult_closed total_conv_surjective univalent_conv_injective path_halving_invariant_def)
          hence "?px  -?pt2sy  y = bot"
            by (simp add: inf.coboundedI2 p_antitone pseudo_complement)
          hence 11: "p[?px  -?pt2sy  y?p2t] = p"
            by simp
          have "y  p0T+ * y"
            using 10 by (metis mult_left_isotone order_lesseq_imp star.circ_plus_same star.left_plus_below_circ)
          hence 12: "y = root p0 y"
            using 1 loop_root_2 path_halving_invariant_def by blast
          have "?pyppy = p[yp0[[p0[[y]]]]]"
            using 1 path_halving_invariant_aux(2) by force
          also have "... = p[yp0[[y]]]"
            using 1 12 by (metis root_successor_loop path_halving_invariant_def)
          also have "... = p[y?py]"
            using 1 path_halving_invariant_aux(1) by force
          also have "... = p"
            using 1 get_put path_halving_invariant_def by blast
          finally show ?thesis
            using 11 by simp
        qed
        have 13: "-?pt2sy = -(p0T * y)  (-?pt2sy  ?pty)  (-?pt2sy  y)"
        proof (rule order.antisym)
          have 14: "regular (p0T * y)  regular ?pt2sy"
            using 1 by (metis order.antisym conv_complement conv_dist_comp conv_involutive conv_star_commute forest_components_increasing mapping_regular pp_dist_star regular_mult_closed top.extremum path_halving_invariant_def)
          have "p0T = p0T * p0T * p0T  p0T  1"
            using star.circ_back_loop_fixpoint star.circ_plus_same star_left_unfold_equal sup_commute by auto
          hence "p0T * y  ?pt2sy  ?pty  y"
            by (metis inf.eq_refl mult_1_left mult_right_dist_sup)
          also have "... = ?pt2sy  (-?pt2sy  ?pty)  y"
            using 14 by (metis maddux_3_21_pp)
          also have "... = ?pt2sy  (-?pt2sy  ?pty)  (-?pt2sy  y)"
            using 14 by (smt (z3) maddux_3_21_pp sup.left_commute sup_assoc)
          hence "p0T * y  -?pt2sy  (-?pt2sy  ?pty)  (-?pt2sy  y)"
            using calculation half_shunting sup_assoc sup_commute by auto
          thus "-?pt2sy  -(p0T * y)  (-?pt2sy  ?pty)  (-?pt2sy  y)"
            using 14 by (smt (z3) inf.sup_monoid.add_commute shunting_var_p sup.left_commute sup_commute)
          have "-(p0T * y)  -?pt2sy"
            by (meson mult_left_isotone order.trans p_antitone star.right_plus_below_circ)
          thus "-(p0T * y)  (-?pt2sy  ?pty)  (-?pt2sy  y)  -?pt2sy"
            by simp
        qed
        have "regular ?px" "regular ?pty" "regular y"
          using 1 bijective_regular find_set_precondition_def mapping_regular pp_dist_comp regular_closed_star regular_conv_closed path_halving_invariant_def by auto
        hence 15: "regular (?px  -?pt2sy  ?pty)" "regular (?px  -?pt2sy  y)"
          by auto
        have "p0[?px - p0T * (?pyppy[[y]])?p2t] = p0[?px - p0T * (p[[?py]])?p2t]"
          using 1 put_get vector_mult_closed path_halving_invariant_def by auto
        also have "... = p0[?px - ?pt2sy?p2t]"
          using 1 comp_associative path_halving_invariant_aux(2) by force
        also have "... = p0[?pxy  (?px  -?pt2sy  ?pty)  (?px  -?pt2sy  y)?p2t]"
          using 13 by (metis comp_inf.semiring.distrib_left inf.sup_monoid.add_assoc)
        also have "... = (?p[?px  -?pt2sy  ?pty?p2t])[?px  -?pt2sy  y?p2t]"
          using 15 by (smt (z3) update_same_3 comp_inf.semiring.mult_not_zero inf.sup_monoid.add_assoc inf.sup_monoid.add_commute)
        also have "... = (p[?px  -?pt2sy  ?pty?p2t])[?px  -?pt2sy  y?p2t]"
          using 1 path_halving_invariant_def by auto
        also have "... = p[?px  -?pt2sy  y?p2t]"
          using 6 by simp
        also have "... = ?pyppy"
          using 9 by auto
        finally show ?thesis
          .
      qed
      show "univalent p0" "total p0" "acyclic (p0 - 1)