# 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

text ‹Theorem 6.4›

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

text ‹Theorem 2.13›

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

text ‹Theorem 6.7›

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

text ‹Theorem 2.14›

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)

text ‹Theorem 2.15›

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

text ‹Theorem 2.11›

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

text ‹Theorem 2.12›

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

text ‹Theorem 2.6›

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)

text ‹Theorem 2.7›

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)

text ‹Theorem 2.8›

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]]])"

text ‹Theorem 2.9›

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]]])"

text ‹Theorem 2.10›

lemma update_mapping_swap:
assumes "mapping x"
and "point y"
and "point z"
shows "mapping ((x[yx[[z]]])[zx[[y]]])"

text ‹Theorem 2.16 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

text ‹Theorem 5.3›

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)

text ‹Theorem 6.1›

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"
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)

text ‹Theorem 6.2›

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"
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"
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"
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

text ‹Theorem 6.5›

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

text ‹Theorem 6.6›

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"
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)"
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

text ‹Theorem 6.2›

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)

text ‹Theorem 6.3›

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

text ‹Theorem 6.3›

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

text ‹Theorem 6.8›

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

text ‹Theorem 6.9›

lemma disjoint_set_forest_update_square:
assumes
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
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
path_compression_precondition p x y  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
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)"
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"
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:
show "path_halving_invariant p0 x x p0"
proof (unfold path_halving_invariant_def, intro conjI)
show
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