Theory Paths

(* Title:      Relational Characterisation of Paths
   Author:     Walter Guttmann, Peter Hoefner
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
               Peter Hoefner <peter at hoefner-online.de>
*)

section ‹Relational Characterisation of Paths›

text ‹
This theory provides the relation-algebraic characterisations of paths, as defined in Sections 3--5 of cite‹"BerghammerFurusawaGuttmannHoefner2020"›.
›

theory Paths

imports More_Relation_Algebra

begin

context relation_algebra_tarski
begin

lemma path_concat_aux_0:
  assumes "is_vector v"
      and "v ≠ 0"
      and "w;vT ≤ x"
      and "v;z ≤ y"
    shows "w;1;z ≤ x;y"
proof -
  from tarski assms(1,2) have "1 = 1;vT;v;1"
    by (metis conv_contrav conv_one eq_refl inf_absorb1 inf_top_left is_vector_def ra_2)
  hence "w;1;z = w;1;vT;v;1;z"
    by (simp add: mult_isor mult_isol mult_assoc)
  also from assms(1) have "... = w;vT;v;z"
    by (metis is_vector_def comp_assoc conv_contrav conv_one)
  also from assms(3) have "... ≤ x;v;z"
    by (simp add: mult_isor)
  also from assms(4) have "... ≤ x;y"
    by (simp add: mult_isol mult_assoc)
  finally show ?thesis .
qed

end (* context relation_algebra_tarski *)

subsection ‹Consequences without the Tarski rule›

context relation_algebra_rtc
begin

text ‹Definitions for path classifications›

abbreviation connected
  where "connected x ≡ x;1;x ≤ x⋆ + xT⋆"

abbreviation many_strongly_connected
  where "many_strongly_connected x ≡ x⋆ = xT⋆"

abbreviation one_strongly_connected
  where "one_strongly_connected x ≡ xT;1;xT ≤ x⋆"

definition path
  where "path x ≡ connected x ∧ is_p_fun x ∧ is_inj x"

abbreviation cycle
  where "cycle x ≡ path x ∧ many_strongly_connected x"

abbreviation start_points
  where "start_points x ≡ x;1 ⋅ -(xT;1)"

abbreviation end_points
  where "end_points x ≡ xT;1 ⋅ -(x;1)"

abbreviation no_start_points
  where "no_start_points x ≡ x;1 ≤ xT;1"

abbreviation no_end_points
  where "no_end_points x ≡ xT;1 ≤ x;1"

abbreviation no_start_end_points
  where "no_start_end_points x ≡ x;1 = xT;1"

abbreviation has_start_points
  where "has_start_points x ≡ 1 = -(1;x);x;1"

abbreviation has_end_points
  where "has_end_points x ≡ 1 = 1;x;-(x;1)"

abbreviation has_start_end_points
  where "has_start_end_points x ≡ 1 = -(1;x);x;1 ⋅ 1;x;-(x;1)"

abbreviation backward_terminating
  where "backward_terminating x ≡ x ≤ -(1;x);x;1"

abbreviation forward_terminating
  where "forward_terminating x ≡ x ≤ 1;x;-(x;1)"

abbreviation terminating
  where "terminating x ≡ x ≤ -(1;x);x;1 ⋅ 1;x;-(x;1)"

abbreviation backward_finite
  where "backward_finite x ≡ x ≤ xT⋆ + -(1;x);x;1"

abbreviation forward_finite
  where "forward_finite x ≡ x ≤ xT⋆ + 1;x;-(x;1)"

abbreviation finite
  where "finite x ≡ x ≤ xT⋆ + (-(1;x);x;1 ⋅ 1;x;-(x;1))"

abbreviation no_start_points_path
  where "no_start_points_path x ≡ path x ∧ no_start_points x"

abbreviation no_end_points_path
  where "no_end_points_path x ≡ path x ∧ no_end_points x"

abbreviation no_start_end_points_path
  where "no_start_end_points_path x ≡ path x ∧ no_start_end_points x"

abbreviation has_start_points_path
  where "has_start_points_path x ≡ path x ∧ has_start_points x"

abbreviation has_end_points_path
  where "has_end_points_path x ≡ path x ∧ has_end_points x"

abbreviation has_start_end_points_path
  where "has_start_end_points_path x ≡ path x ∧ has_start_end_points x"

abbreviation backward_terminating_path
  where "backward_terminating_path x ≡ path x ∧ backward_terminating x"

abbreviation forward_terminating_path
  where "forward_terminating_path x ≡ path x ∧ forward_terminating x"

abbreviation terminating_path
  where "terminating_path x ≡ path x ∧ terminating x"

abbreviation backward_finite_path
  where "backward_finite_path x ≡ path x ∧ backward_finite x"

abbreviation forward_finite_path
  where "forward_finite_path x ≡ path x ∧ forward_finite x"

abbreviation finite_path
  where "finite_path x ≡ path x ∧ finite x"

text ‹General properties›

lemma reachability_from_z_in_y:
  assumes "x ≤ y⋆;z"
      and "x ⋅ z = 0"
    shows "x ≤ y+;z"
by (metis assms conway.dagger_unfoldl_distr galois_1 galois_aux inf.orderE)

lemma reachable_imp:
  assumes "point p"
      and "point q"
      and "p⋆;q ≤ pT⋆;p"
    shows "p ≤ p⋆;q"
by (metis assms conway.dagger_unfoldr_distr le_supE point_swap star_conv)

text ‹Basic equivalences›

lemma no_start_end_points_iff:
  "no_start_end_points x ⟷ no_start_points x ∧ no_end_points x"
by fastforce

lemma has_start_end_points_iff:
  "has_start_end_points x ⟷ has_start_points x ∧ has_end_points x"
by (metis inf_eq_top_iff)

lemma terminating_iff:
  "terminating x ⟷ backward_terminating x ∧ forward_terminating x"
by simp

lemma finite_iff:
  "finite x ⟷ backward_finite x ∧ forward_finite x"
by (simp add: sup_inf_distrib1 inf.boundedI)

lemma no_start_end_points_path_iff:
  "no_start_end_points_path x ⟷ no_start_points_path x ∧ no_end_points_path x"
by fastforce

lemma has_start_end_points_path_iff:
  "has_start_end_points_path x ⟷ has_start_points_path x ∧ has_end_points_path x"
using has_start_end_points_iff by blast

lemma terminating_path_iff:
  "terminating_path x ⟷ backward_terminating_path x ∧ forward_terminating_path x"
by fastforce

lemma finite_path_iff:
  "finite_path x ⟷ backward_finite_path x ∧ forward_finite_path x"
using finite_iff by fastforce

text ‹Closure under converse›

lemma connected_conv:
  "connected x ⟷ connected (xT)"
by (metis comp_assoc conv_add conv_contrav conv_iso conv_one star_conv)

lemma conv_many_strongly_connected:
  "many_strongly_connected x ⟷ many_strongly_connected (xT)"
by fastforce

lemma conv_one_strongly_connected:
  "one_strongly_connected x ⟷ one_strongly_connected (xT)"
by (metis comp_assoc conv_contrav conv_iso conv_one star_conv)

lemma conv_path:
  "path x ⟷ path (xT)"
using connected_conv inj_p_fun path_def by fastforce

lemma conv_cycle:
  "cycle x ⟷ cycle (xT)"
using conv_path by fastforce

lemma conv_no_start_points:
  "no_start_points x ⟷ no_end_points (xT)"
by simp

lemma conv_no_start_end_points:
  "no_start_end_points x ⟷ no_start_end_points (xT)"
by fastforce

lemma conv_has_start_points:
  "has_start_points x ⟷ has_end_points (xT)"
by (metis comp_assoc conv_compl conv_contrav conv_invol conv_one)

lemma conv_has_start_end_points:
  "has_start_end_points x ⟷ has_start_end_points (xT)"
by (metis comp_assoc conv_compl conv_contrav conv_invol conv_one inf_eq_top_iff)

lemma conv_backward_terminating:
  "backward_terminating x ⟷ forward_terminating (xT)"
by (metis comp_assoc conv_compl conv_contrav conv_iso conv_one)

lemma conv_terminating:
  "terminating x ⟷ terminating (xT)"
  apply (rule iffI)
 apply (metis conv_compl conv_contrav conv_one conv_times inf.commute le_iff_inf mult_assoc)
by (metis conv_compl conv_contrav conv_invol conv_one conv_times inf.commute le_iff_inf mult_assoc)

lemma conv_backward_finite:
  "backward_finite x ⟷ forward_finite (xT)"
by (metis comp_assoc conv_add conv_compl conv_contrav conv_iso conv_one star_conv)

lemma conv_finite:
  "finite x ⟷ finite (xT)"
by (metis finite_iff conv_backward_finite conv_invol)

lemma conv_no_start_points_path:
  "no_start_points_path x ⟷ no_end_points_path (xT)"
using conv_path by fastforce

lemma conv_no_start_end_points_path:
  "no_start_end_points_path x ⟷ no_start_end_points_path (xT)"
using conv_path by fastforce

lemma conv_has_start_points_path:
  "has_start_points_path x ⟷ has_end_points_path (xT)"
using conv_has_start_points conv_path by fastforce

lemma conv_has_start_end_points_path:
  "has_start_end_points_path x ⟷ has_start_end_points_path (xT)"
using conv_has_start_end_points conv_path by fastforce

lemma conv_backward_terminating_path:
  "backward_terminating_path x ⟷ forward_terminating_path (xT)"
using conv_backward_terminating conv_path by fastforce

lemma conv_terminating_path:
  "terminating_path x ⟷ terminating_path (xT)"
using conv_path conv_terminating by fastforce

lemma conv_backward_finite_path:
  "backward_finite_path x ⟷ forward_finite_path (xT)"
using conv_backward_finite conv_path by fastforce

lemma conv_finite_path:
  "finite_path x ⟷ finite_path (xT)"
using conv_finite conv_path by blast

text ‹Equivalences for ‹connected››

lemma connected_iff2:
  assumes "is_inj x"
      and "is_p_fun x"
    shows "connected x ⟷ x;1;xT ≤ x⋆ + xT⋆"
proof
  assume 1: "connected x"
  have "x;1;xT ≤ x;1;x;xT"
    by (metis conv_invol modular_var_3 vector_meet_comp_x')
  also have "... ≤ (x+ + xT⋆);xT"
    using 1 mult_isor star_star_plus by fastforce
  also have "... ≤ x⋆;x;xT + xT⋆"
    using join_isol star_slide_var by simp
  also from assms(1) have "... ≤ x⋆ + xT⋆"
    by (metis is_inj_def comp_assoc join_iso mult_1_right mult_isol)
  finally show "x;1;xT ≤ x⋆ + xT⋆" .
next
  assume 2: "x;1;xT ≤ x⋆ + xT⋆"
  have "x;1;x ≤ x;1;xT;x"
    by (simp add: modular_var_3 vector_meet_comp_x)
  also have "... ≤ (x⋆ + xT+);x"
    using 2 by (metis mult_isor star_star_plus sup_commute)
  also have "... ≤ x⋆ + xT⋆;xT;x"
    using join_iso star_slide_var by simp
  also from assms(2) have "... ≤ x⋆ + xT⋆"
    by (metis comp_assoc is_p_fun_def join_isol mult_1_right mult_isol)
  finally show "connected x" .
qed

lemma connected_iff3:
  assumes "is_inj x"
      and "is_p_fun x"
    shows "connected x ⟷ xT;1;x ≤ x⋆ + xT⋆"
by (metis assms connected_conv connected_iff2 inj_p_fun p_fun_inj conv_invol add_commute)

lemma connected_iff4:
  "connected x ⟷ xT;1;xT ≤ x⋆ + xT⋆"
by (metis connected_conv conv_invol add_commute)

lemma connected_iff5:
  "connected x ⟷ x+;1;x+ ≤ x⋆ + xT⋆"
using comp_assoc plus_top top_plus by fastforce

lemma connected_iff6:
  assumes "is_inj x"
      and "is_p_fun x"
    shows "connected x ⟷ x+;1;(x+)T ≤ x⋆ + xT⋆"
using assms connected_iff2 comp_assoc plus_conv plus_top top_plus by fastforce

lemma connected_iff7:
  assumes "is_inj x"
      and "is_p_fun x"
    shows "connected x ⟷ (x+)T;1;x+ ≤ x⋆ + xT⋆"
by (metis assms connected_iff3 conv_contrav conv_invol conv_one top_plus vector_meet_comp_x)

lemma connected_iff8:
  "connected x ⟷ (x+)T;1;(x+)T ≤ x⋆ + xT⋆"
by (metis connected_iff4 comp_assoc conv_contrav conv_invol conv_one plus_conv star_conv top_plus)

text ‹Equivalences and implications for ‹many_strongly_connected››

lemma many_strongly_connected_iff_1:
  "many_strongly_connected x ⟷ xT ≤ x⋆"
 apply (rule iffI,simp)
by (metis conv_invol conv_iso order.eq_iff star_conv star_invol star_iso)

lemma many_strongly_connected_iff_2:
  "many_strongly_connected x ⟷ xT ≤ x+"
proof
  assume as: "many_strongly_connected x"
  hence "xT ≤ x⋆ ⋅ (-(1') + x)"
    by (metis many_strongly_connected_iff_1 loop_backward_forward inf_greatest)
  also have "... ≤ (x⋆ ⋅ -(1')) + (x⋆ ⋅ x)"
    by (simp add: inf_sup_distrib1)
  also have "... ≤ x+"
    by (metis as order.eq_iff mult_1_right mult_isol star_ref sup.absorb1 conv_invol eq_refl galois_1
              inf.absorb_iff1 inf.commute star_unfoldl_eq sup_mono many_strongly_connected_iff_1)
  finally show "xT ≤ x+" .
next
  show "xT ≤ x+ ⟹ many_strongly_connected x"
    using order_trans star_1l many_strongly_connected_iff_1 by blast
qed

lemma many_strongly_connected_iff_3:
  "many_strongly_connected x ⟷ x ≤ xT⋆"
by (metis conv_invol many_strongly_connected_iff_1)

lemma many_strongly_connected_iff_4:
  "many_strongly_connected x ⟷ x ≤ xT+"
by (metis conv_invol many_strongly_connected_iff_2)

lemma many_strongly_connected_iff_5:
  "many_strongly_connected x ⟷ x⋆;xT ≤ x+"
by (metis comp_assoc conv_contrav conway.dagger_unfoldr_distr star_conv star_denest_var_2
          star_invol star_trans_eq star_unfoldl_eq sup.boundedE many_strongly_connected_iff_2)

lemma many_strongly_connected_iff_6:
  "many_strongly_connected x ⟷ xT;x⋆ ≤ x+"
by (metis dual_order.trans star_1l star_conv star_inductl_star star_invol star_slide_var
          many_strongly_connected_iff_1 many_strongly_connected_iff_5)

lemma many_strongly_connected_iff_7:
  "many_strongly_connected x ⟷ xT+ = x+"
by (metis order.antisym conv_invol star_slide_var star_unfoldl_eq many_strongly_connected_iff_5)

lemma many_strongly_connected_iff_5_eq:
  "many_strongly_connected x ⟷ x⋆;xT = x+"
by (metis order.refl star_slide_var many_strongly_connected_iff_5 many_strongly_connected_iff_7)

lemma many_strongly_connected_iff_6_eq:
  "many_strongly_connected x ⟷ xT;x⋆ = x+"
using many_strongly_connected_iff_6 many_strongly_connected_iff_7 by force

lemma many_strongly_connected_implies_no_start_end_points:
  assumes "many_strongly_connected x"
    shows "no_start_end_points x"
by (metis assms conway.dagger_unfoldl_distr mult_assoc sup_top_left conv_invol
        many_strongly_connected_iff_7)

lemma many_strongly_connected_implies_8:
  assumes "many_strongly_connected x"
    shows "x;xT ≤ x+"
by (simp add: assms mult_isol)

lemma many_strongly_connected_implies_9:
  assumes "many_strongly_connected x"
    shows "xT;x ≤ x+"
by (metis assms eq_refl phl_cons1 star_ext star_slide_var)

lemma many_strongly_connected_implies_10:
  assumes "many_strongly_connected x"
    shows "x;xT;x⋆ ≤ x+"
by (simp add: assms comp_assoc mult_isol)

lemma many_strongly_connected_implies_10_eq:
  assumes "many_strongly_connected x"
    shows "x;xT;x⋆ = x+"
proof (rule order.antisym)
  show "x;xT;x⋆ ≤ x+"
    by (simp add: assms comp_assoc mult_isol)
next
  have "x+ ≤ x;xT;x;x⋆"
    using mult_isor x_leq_triple_x by blast
  thus "x+ ≤ x;xT;x⋆"
    by (simp add: comp_assoc mult_isol order_trans)
qed

lemma many_strongly_connected_implies_11:
  assumes "many_strongly_connected x"
    shows "x⋆;xT;x ≤ x+"
by (metis assms conv_contrav conv_iso mult_isol star_1l star_slide_var)

lemma many_strongly_connected_implies_11_eq:
  assumes "many_strongly_connected x"
    shows "x⋆;xT;x = x+"
by (metis assms comp_assoc conv_invol many_strongly_connected_iff_5_eq
          many_strongly_connected_implies_10_eq)

lemma many_strongly_connected_implies_12:
  assumes "many_strongly_connected x"
    shows "x⋆;x;xT ≤ x+"
by (metis assms comp_assoc mult_isol star_1l star_slide_var)

lemma many_strongly_connected_implies_12_eq:
  assumes "many_strongly_connected x"
    shows "x⋆;x;xT = x+"
by (metis assms comp_assoc star_slide_var many_strongly_connected_implies_10_eq)

lemma many_strongly_connected_implies_13:
  assumes "many_strongly_connected x"
    shows "xT;x;x⋆ ≤ x+"
by (metis assms star_slide_var many_strongly_connected_implies_11 mult.assoc)

lemma many_strongly_connected_implies_13_eq:
  assumes "many_strongly_connected x"
    shows "xT;x;x⋆ = x+"
by (metis assms conv_invol many_strongly_connected_iff_7 many_strongly_connected_implies_10_eq)

lemma many_strongly_connected_iff_8:
  assumes "is_p_fun x"
    shows "many_strongly_connected x ⟷ x;xT ≤ x+"
 apply (rule iffI)
  apply (simp add: mult_isol)
 apply (simp add: many_strongly_connected_iff_1)
by (metis comp_assoc conv_invol dual_order.trans mult_isol x_leq_triple_x assms comp_assoc
          dual_order.trans is_p_fun_def order.refl prod_star_closure star_ref)

lemma many_strongly_connected_iff_9:
  assumes "is_inj x"
    shows "many_strongly_connected x ⟷ xT;x ≤ x+"
by (metis assms conv_contrav conv_iso inj_p_fun star_conv star_slide_var
          many_strongly_connected_iff_1 many_strongly_connected_iff_8)

lemma many_strongly_connected_iff_10:
  assumes "is_p_fun x"
    shows "many_strongly_connected x ⟷ x;xT;x⋆ ≤ x+"
 apply (rule iffI)
 apply (simp add: comp_assoc mult_isol)
by (metis assms mult_isol mult_oner order_trans star_ref many_strongly_connected_iff_8)

lemma many_strongly_connected_iff_10_eq:
  assumes "is_p_fun x"
    shows "many_strongly_connected x ⟷ x;xT;x⋆ = x+"
using assms many_strongly_connected_iff_10 many_strongly_connected_implies_10_eq by fastforce

lemma many_strongly_connected_iff_11:
  assumes "is_inj x"
    shows "many_strongly_connected x ⟷ x⋆;xT;x ≤ x+"
by (metis assms comp_assoc conv_contrav conv_iso inj_p_fun plus_conv star_conv
          many_strongly_connected_iff_10 many_strongly_connected_iff_2)

lemma many_strongly_connected_iff_11_eq:
  assumes "is_inj x"
    shows "many_strongly_connected x ⟷ x⋆;xT;x = x+"
using assms many_strongly_connected_iff_11 many_strongly_connected_implies_11_eq by fastforce

lemma many_strongly_connected_iff_12:
  assumes "is_p_fun x"
    shows "many_strongly_connected x ⟷ x⋆;x;xT ≤ x+"
by (metis assms dual_order.trans mult_double_iso mult_oner star_ref star_slide_var
          many_strongly_connected_iff_8 many_strongly_connected_implies_12)

lemma many_strongly_connected_iff_12_eq:
  assumes "is_p_fun x"
    shows "many_strongly_connected x ⟷ x⋆;x;xT = x+"
using assms many_strongly_connected_iff_12 many_strongly_connected_implies_12_eq by fastforce

lemma many_strongly_connected_iff_13:
  assumes "is_inj x"
    shows "many_strongly_connected x ⟷ xT;x;x⋆ ≤ x+"
by (metis assms comp_assoc conv_contrav conv_iso inj_p_fun star_conv star_slide_var
          many_strongly_connected_iff_1 many_strongly_connected_iff_12)

lemma many_strongly_connected_iff_13_eq:
  assumes "is_inj x"
    shows "many_strongly_connected x ⟷ xT;x;x⋆ = x+"
using assms many_strongly_connected_iff_13 many_strongly_connected_implies_13_eq by fastforce

text ‹Equivalences and implications for ‹one_strongly_connected››

lemma one_strongly_connected_iff:
  "one_strongly_connected x ⟷ connected x ∧ many_strongly_connected x"
  apply (rule iffI)
 apply (metis top_greatest x_leq_triple_x mult_double_iso top_greatest dual_order.trans
              many_strongly_connected_iff_1 comp_assoc conv_contrav conv_invol conv_iso le_supI2
              star_conv)
by (metis comp_assoc conv_contrav conv_iso conv_one conway.dagger_denest star_conv star_invol
          star_sum_unfold star_trans_eq)

lemma one_strongly_connected_iff_1:
  "one_strongly_connected x ⟷ xT;1;xT ≤ x+"
proof
  assume 1: "one_strongly_connected x"
  have "xT;1;xT ≤ xT;x;xT;1;xT"
    by (metis conv_invol mult_isor x_leq_triple_x)
  also from 1 have "... ≤ xT;x;x⋆"
    by (metis distrib_left mult_assoc sup.absorb_iff1)
  also from 1 have "... ≤ x+"
    using many_strongly_connected_implies_13 one_strongly_connected_iff by blast
  finally show "xT;1;xT ≤ x+"
    .
next
  assume "xT;1;xT ≤ x+"
  thus "one_strongly_connected x"
    using dual_order.trans star_1l by blast
qed

lemma one_strongly_connected_iff_1_eq:
  "one_strongly_connected x ⟷ xT;1;xT = x+"
  apply (rule iffI, simp_all)
by (metis comp_assoc conv_contrav conv_invol mult_double_iso plus_conv star_slide_var top_greatest
          top_plus many_strongly_connected_implies_10_eq one_strongly_connected_iff order.eq_iff
          one_strongly_connected_iff_1)

lemma one_strongly_connected_iff_2:
  "one_strongly_connected x ⟷ x;1;x ≤ xT⋆"
by (metis conv_invol eq_refl less_eq_def one_strongly_connected_iff)

lemma one_strongly_connected_iff_3:
  "one_strongly_connected x ⟷ x;1;x ≤ xT+"
by (metis comp_assoc conv_contrav conv_invol conv_iso conv_one star_conv
          one_strongly_connected_iff_1)

lemma one_strongly_connected_iff_3_eq:
  "one_strongly_connected x ⟷ x;1;x = xT+"
by (metis conv_invol one_strongly_connected_iff_1_eq one_strongly_connected_iff_2)

lemma one_strongly_connected_iff_4_eq:
  "one_strongly_connected x ⟷ xT;1;x = x+"
  apply (rule iffI)
 apply (metis comp_assoc top_plus many_strongly_connected_iff_7 one_strongly_connected_iff
              one_strongly_connected_iff_1_eq)
by (metis comp_assoc conv_contrav conv_invol conv_one plus_conv top_plus
          one_strongly_connected_iff_1_eq)

lemma one_strongly_connected_iff_5_eq:
  "one_strongly_connected x ⟷ x;1;xT = x+"
using comp_assoc conv_contrav conv_invol conv_one plus_conv top_plus many_strongly_connected_iff_7
      one_strongly_connected_iff one_strongly_connected_iff_3_eq by metis

lemma one_strongly_connected_iff_6_aux:
  "x;x+ ≤ x;1;x"
by (metis comp_assoc maddux_21 mult_isol top_plus)

lemma one_strongly_connected_implies_6_eq:
  assumes "one_strongly_connected x"
    shows "x;1;x = x;x+"
by (metis assms comp_assoc many_strongly_connected_iff_7 many_strongly_connected_implies_10_eq
          one_strongly_connected_iff one_strongly_connected_iff_3_eq)

lemma one_strongly_connected_iff_7_aux:
  "x+ ≤ x;1;x"
by (metis le_infI maddux_20 maddux_21 plus_top top_plus vector_meet_comp_x')

lemma one_strongly_connected_implies_7_eq:
  assumes "one_strongly_connected x"
    shows "x;1;x = x+"
using assms many_strongly_connected_iff_7 one_strongly_connected_iff one_strongly_connected_iff_3_eq
by force

lemma one_strongly_connected_implies_8:
  assumes "one_strongly_connected x"
    shows "x;1;x ≤ x⋆"
using assms one_strongly_connected_iff by fastforce

lemma one_strongly_connected_iff_4:
  assumes "is_inj x"
    shows "one_strongly_connected x ⟷ xT;1;x ≤ x+"
proof
  assume "one_strongly_connected x"
  thus "xT;1;x ≤ x+"
    by (simp add: one_strongly_connected_iff_4_eq)
next
  assume 1: "xT;1;x ≤ x+"
  hence "xT;1;xT ≤ x⋆;x;xT"
    by (metis mult_isor star_slide_var comp_assoc conv_invol modular_var_3 vector_meet_comp_x
              order.trans)
  also from assms have "... ≤ x⋆"
    using comp_assoc is_inj_def mult_isol mult_oner by fastforce
  finally show "one_strongly_connected x"
    using dual_order.trans star_1l by fastforce
qed

lemma one_strongly_connected_iff_5:
  assumes "is_p_fun x"
    shows "one_strongly_connected x ⟷ x;1;xT ≤ x+"
  apply (rule iffI)
 using one_strongly_connected_iff_5_eq apply simp
by (metis assms comp_assoc mult_double_iso order.trans star_slide_var top_greatest top_plus
          many_strongly_connected_iff_12 many_strongly_connected_iff_7 one_strongly_connected_iff_3)

lemma one_strongly_connected_iff_6:
  assumes "is_p_fun x"
      and "is_inj x"
    shows "one_strongly_connected x ⟷ x;1;x ≤ x;x+"
proof
  assume "one_strongly_connected x"
  thus "x;1;x ≤ x;x+"
   by (simp add: one_strongly_connected_implies_6_eq)
next
  assume 1: "x;1;x ≤ x;x+"
  have "xT;1;x ≤ xT;x;xT;1;x"
    by (metis conv_invol mult_isor x_leq_triple_x)
  also have "... ≤ xT;x;1;x"
    by (metis comp_assoc mult_double_iso top_greatest)
  also from 1 have "... ≤ xT;x;x+"
    by (simp add: comp_assoc mult_isol)
  also from assms(1) have "... ≤ x+"
    by (metis comp_assoc is_p_fun_def mult_isor mult_onel)
  finally show "one_strongly_connected x"
    using assms(2) one_strongly_connected_iff_4 by blast
qed

lemma one_strongly_connected_iff_6_eq:
  assumes "is_p_fun x"
      and "is_inj x"
    shows "one_strongly_connected x ⟷ x;1;x = x;x+"
  apply (rule iffI)
 using one_strongly_connected_implies_6_eq apply blast
by (simp add: assms one_strongly_connected_iff_6)

text ‹Start points and end points›

lemma start_end_implies_terminating:
  assumes "has_start_points x"
      and "has_end_points x"
    shows "terminating x"
using assms by simp

lemma start_points_end_points_conv:
  "start_points x = end_points (xT)"
by simp

lemma start_point_at_most_one:
  assumes "path x"
    shows "is_inj (start_points x)"
proof -
  have isvec: "is_vector (x;1 ⋅ -(xT;1))"
    by (simp add: comp_assoc is_vector_def one_compl vector_1)

  have "x;1 ⋅ 1;xT ≤ x;1;x;xT"
    by (metis comp_assoc conv_contrav conv_one inf.cobounded2 mult_1_right mult_isol one_conv ra_2)
  also have "... ≤ (x⋆ + xT⋆);xT"
    using ‹path x› by (metis path_def mult_isor)
  also have "... = xT + x+;xT + xT+"
    by (simp add: star_slide_var)
  also have "... ≤ xT+ + x+;xT + xT+"
    by (metis add_iso mult_1_right star_unfoldl_eq subdistl)
  also have "... ≤ x⋆;x;xT + xT+"
    by (simp add: star_slide_var add_comm)
  also have "... ≤ x⋆;1' + xT+"
    using ‹path x› by (metis path_def is_inj_def comp_assoc distrib_left join_iso less_eq_def)
  also have "... = 1' + x⋆;x + xT;xT⋆"
    by simp
  also have "... ≤ 1' + 1;x + xT;1"
    by (metis join_isol mult_isol mult_isor sup.mono top_greatest)
  finally have aux: "x;1 ⋅ 1;xT ≤ 1' + 1;x + xT;1" .

  from aux have "x;1 ⋅ 1;xT ⋅ -(xT;1) ⋅ -(1;x) ≤ 1'"
    by (simp add: galois_1 sup_commute)
  hence "(x;1 ⋅ -(xT;1)) ⋅ (x;1 ⋅ -(xT;1))T ≤ 1'"
    by (simp add: conv_compl inf.assoc inf.left_commute)
  with isvec have "(x;1 ⋅ -(xT;1)) ; (x;1 ⋅ -(xT;1))T ≤ 1'"
    by (metis vector_meet_comp')
  thus "is_inj (start_points x)"
    by (simp add: conv_compl is_inj_def)
qed

lemma start_point_zero_point:
  assumes "path x"
    shows "start_points x = 0 ∨ is_point (start_points x)"
using assms start_point_at_most_one comp_assoc is_point_def is_vector_def vector_compl vector_mult
by simp

lemma start_point_iff1:
  assumes "path x"
    shows "is_point (start_points x) ⟷ ¬(no_start_points x)"
using assms start_point_zero_point galois_aux2 is_point_def by blast

lemma end_point_at_most_one:
  assumes "path x"
    shows "is_inj (end_points x)"
by (metis assms conv_path compl_bot_eq conv_invol inj_def_var1 is_point_def top_greatest
          start_point_zero_point)

lemma end_point_zero_point:
  assumes "path x"
    shows "end_points x = 0 ∨ is_point (end_points x)"
using assms conv_path start_point_zero_point by fastforce

lemma end_point_iff1:
  assumes "path x"
    shows "is_point (end_points x) ⟷ ¬(no_end_points x)"
using assms end_point_zero_point galois_aux2 is_point_def by blast

lemma predecessor_point':
  assumes "path x"
      and "point s"
      and "point e"
      and "e;sT ≤ x"
    shows "x;s = e"
proof (rule order.antisym)
  show 1: "e ≤ x ; s"
    using assms(2,4) point_def ss423bij by blast
  show "x ; s ≤ e"
  proof -
    have "eT ; (x ; s) = 1"
      using 1 by (metis assms(3) order.eq_iff is_vector_def point_def ss423conv top_greatest)
    thus ?thesis
      by (metis assms(1-3) comp_assoc conv_contrav conv_invol order.eq_iff inj_compose is_vector_def
                mult_isol path_def point_def ss423conv sur_def_var1 top_greatest)
  qed
qed

lemma predecessor_point:
  assumes "path x"
      and "point s"
      and "point e"
      and "e;sT ≤ x"
    shows "point(x;s)"
using predecessor_point' assms by blast

lemma points_of_path_iff:
  shows "(x + xT);1 = xT;1 + start_points(x)"
    and "(x + xT);1 = x;1 + end_points(x)"
using aux9 inf.commute sup.commute by auto

text ‹Path concatenation preliminaries›

lemma path_concat_aux_1:
  assumes "x;1 ⋅ y;1 ⋅ yT;1 = 0"
      and "end_points x = start_points y"
    shows "x;1 ⋅ y;1 = 0"
proof -
  have "x;1 ⋅ y;1 = (x;1 ⋅ y;1 ⋅ yT;1) + (x;1 ⋅ y;1 ⋅ -(yT;1))"
    by simp
  also from assms(1) have "... = x;1 ⋅ y;1 ⋅ -(yT;1)"
    by (metis aux6_var de_morgan_3 inf.left_commute inf_compl_bot inf_sup_absorb)
  also from assms(2) have "... = x;1 ⋅ xT;1 ⋅ -(x;1)"
    by (simp add: inf.assoc)
  also have "... = 0"
    by (simp add: inf.commute inf.assoc)
  finally show ?thesis .
qed

lemma path_concat_aux_2:
  assumes "x;1 ⋅ xT;1 ⋅ yT;1 = 0"
      and "end_points x = start_points y"
    shows "xT;1 ⋅ yT;1 = 0"
proof -
  have "yT;1 ⋅ xT;1 ⋅ (xT)T;1 = 0"
    using assms(1) inf.assoc inf.commute by force
  thus ?thesis
    by (metis assms(2) conv_invol inf.commute path_concat_aux_1)
qed

lemma path_concat_aux3_1:
  assumes "path x"
    shows "x;1;xT ≤ x⋆ + xT⋆"
proof -
  have "x;1;xT ≤ x;1;xT;x;xT"
    by (metis comp_assoc conv_invol mult_isol x_leq_triple_x)
  also have "... ≤ x;1;x;xT"
    by (metis mult_isol mult_isor mult_assoc top_greatest)
  also from assms have "... ≤ (x⋆ + xT⋆);xT"
    using path_def comp_assoc mult_isor by blast
  also have "... = x⋆;x;xT + xT⋆;xT"
    by (simp add: star_slide_var star_star_plus)
  also have "... ≤ x⋆;1' + xT⋆;xT"
    by (metis assms path_def is_inj_def join_iso mult_isol mult_assoc)
  also have "... ≤ x⋆ + xT⋆"
    using join_isol by simp
  finally show ?thesis .
qed

lemma path_concat_aux3_2:
  assumes "path x"
    shows "xT;1;x ≤ x⋆ + xT⋆"
proof -
  have "xT;1;x ≤ xT;x;xT;1;x"
    by (metis comp_assoc conv_invol mult_isor x_leq_triple_x)
  also have "... ≤ xT;x;1;x"
    by (metis mult_isol mult_isor mult_assoc top_greatest)
  also from assms have "... ≤ xT;(x⋆ + xT⋆)"
    by (simp add: comp_assoc mult_isol path_def)
  also have "... = xT;x;x⋆ + xT;xT⋆"
    by (simp add: comp_assoc distrib_left star_star_plus)
  also have "... ≤ 1';x⋆ + xT;xT⋆"
    by (metis assms path_def is_p_fun_def join_iso mult_isor mult_assoc)
  also have "... ≤ x⋆ + xT⋆"
    using join_isol by simp
  finally show ?thesis .
qed

lemma path_concat_aux3_3:
  assumes "path x"
    shows "xT;1;xT ≤ x⋆ + xT⋆"
proof -
  have "xT;1;xT ≤ xT;x;xT;1;xT"
    by (metis comp_assoc conv_invol mult_isor x_leq_triple_x)
  also have "... ≤ xT;x;1;xT"
    by (metis mult_isol mult_isor mult_assoc top_greatest)
  also from assms have "... ≤ xT;(x⋆ + xT⋆)"
    using path_concat_aux3_1 by (simp add: mult_assoc mult_isol)
  also have "... = xT;x;x⋆ + xT;xT⋆"
    by (simp add: comp_assoc distrib_left star_star_plus)
  also have "... ≤ 1';x⋆ + xT;xT⋆"
    by (metis assms path_def is_p_fun_def join_iso mult_isor mult_assoc)
  also have "... ≤ x⋆ + xT⋆"
    using join_isol by simp
  finally show ?thesis .
qed

lemma path_concat_aux_3:
  assumes "path x"
      and "y ≤ x+ + xT+"
      and "z ≤ x+ + xT+"
    shows "y;1;z ≤ x⋆ + xT⋆"
proof -
  from assms(2,3) have "y;1;z ≤ (x+ + xT+);1;(x+ + xT+)"
    using mult_isol_var mult_isor by blast
  also have "... = x+;1;x+ + x+;1;xT+ + xT+;1;x+ + xT+;1;xT+"
    by (simp add: distrib_left sup_commute sup_left_commute)
  also have "... = x;x⋆;1;x⋆;x + x;x⋆;1;xT⋆;xT + xT;xT⋆;1;x⋆;x + xT;xT⋆;1;xT⋆;xT"
    by (simp add: comp_assoc star_slide_var)
  also have "... ≤ x;1;x + x;x⋆;1;xT⋆;xT + xT;xT⋆;1;x⋆;x + xT;xT⋆;1;xT⋆;xT"
    by (metis comp_assoc mult_double_iso top_greatest join_iso)
  also have "... ≤ x;1;x + x;1;xT + xT;xT⋆;1;x⋆;x + xT;xT⋆;1;xT⋆;xT"
    by (metis comp_assoc mult_double_iso top_greatest join_iso join_isol)
  also have "... ≤ x;1;x + x;1;xT + xT;1;x + xT;xT⋆;1;xT⋆;xT"
    by (metis comp_assoc mult_double_iso top_greatest join_iso join_isol)
  also have "... ≤ x;1;x + x;1;xT + xT;1;x + xT;1;xT"
    by (metis comp_assoc mult_double_iso top_greatest join_isol)
  also have "... ≤ x⋆ + xT⋆"
    using assms(1) path_def path_concat_aux3_1 path_concat_aux3_2 path_concat_aux3_3 join_iso join_isol
    by simp
  finally show ?thesis .
qed

lemma path_concat_aux_4:
  "x⋆ + xT⋆ ≤ x⋆ + xT;1"
by (metis star_star_plus add_comm join_isol mult_isol top_greatest)

lemma path_concat_aux_5:
  assumes "path x"
      and "y ≤ start_points x"
      and "z ≤ x + xT"
    shows "y;1;z ≤ x⋆"
proof -
  from assms(1) have "x;1;x ≤ x⋆ + xT;1"
    using path_def path_concat_aux_4 dual_order.trans by blast
  hence aux1: "x;1;x ⋅ -(xT;1) ≤ x⋆"
    by (simp add: galois_1 sup_commute)

  from assms(1) have "x;1;xT ≤ x⋆ + xT;1"
    using dual_order.trans path_concat_aux3_1 path_concat_aux_4 by blast
  hence aux2: "x;1;xT ⋅ -(xT;1) ≤ x⋆"
    by (simp add: galois_1 sup_commute)

  from assms(2,3) have "y;1;z ≤ (x;1 ⋅ -(xT;1));1;(x + xT)"
    by (simp add: mult_isol_var mult_isor)
  also have "... = (x;1 ⋅ -(xT;1));1;x + (x;1 ⋅ -(xT;1));1;xT"
    using distrib_left by blast
  also have "... = (x;1 ⋅ -(xT;1) ⋅ 1;x) + (x;1 ⋅ -(xT;1));1;xT"
    by (metis comp_assoc inf_top_right is_vector_def one_idem_mult vector_1 vector_compl)
  also have "... = (x;1 ⋅ -(xT;1) ⋅ 1;x) + (x;1 ⋅ -(xT;1) ⋅ 1;xT)"
    by (metis comp_assoc inf_top_right is_vector_def one_idem_mult vector_1 vector_compl)
  also have "... = (x;1;x ⋅ -(xT;1)) + (x;1;xT -(xT;1))"
    using vector_meet_comp_x vector_meet_comp_x' diff_eq inf.assoc inf.commute by simp
  also from aux1 aux2 have "... ≤ x⋆"
    by (simp add: diff_eq join_iso)
  finally show ?thesis .
qed

lemma path_conditions_disjoint_points_iff:
  "x;1 ⋅ (xT;1 + y;1) ⋅ yT;1 = 0 ∧ start_points x ⋅ end_points y = 0 ⟷ x;1 ⋅ yT;1 = 0"
proof
  assume 1: "x ; 1 ⋅ yT ; 1 = 0"
  hence g1: "x ; 1 ⋅ (xT ; 1 + y ; 1) ⋅ yT ; 1 = 0"
    by (metis inf.left_commute inf_bot_right inf_commute)
  have g2: "start_points x ⋅ end_points y = 0"
    using 1 by (metis compl_inf_bot inf.assoc inf.commute inf.left_idem)
  show "x;1 ⋅ (xT;1 + y;1) ⋅ yT;1 = 0 ∧ start_points x ⋅ end_points y = 0"
    using g1 and g2 by simp
next
  assume a: "x;1 ⋅ (xT;1 + y;1) ⋅ yT;1 = 0 ∧ start_points x ⋅ end_points y = 0"
  from a have a1: "x;1 ⋅ xT;1 ⋅ yT;1 = 0"
    by (simp add: inf.commute inf_sup_distrib1)
  from a have a2: "x;1 ⋅ y;1 ⋅ yT;1 = 0"
    by (simp add: inf.commute inf_sup_distrib1)
  from a have a3: "start_points x ⋅ end_points y = 0"
    by blast

  have "x;1 ⋅ yT;1 = x;1 ⋅ xT;1 ⋅ yT;1 + x;1 ⋅ -(xT;1) ⋅ yT;1"
    by (metis aux4 inf_sup_distrib2)
  also from a1 have "... = x;1 ⋅ -(xT;1) ⋅ yT;1"
    using sup_bot_left by blast
  also have "... = x;1 ⋅ -(xT;1) ⋅ y;1 ⋅ yT;1 + x;1 ⋅ -(xT;1) ⋅ -(y;1) ⋅ yT;1"
    by (metis aux4 inf_sup_distrib2)
  also have "... ≤ x;1 ⋅ y;1 ⋅ yT;1 + x;1 ⋅ -(xT;1) ⋅ -(y;1) ⋅ yT;1"
    using join_iso meet_iso by simp
  also from a2 have "... = start_points x ⋅ end_points y"
    using sup_bot_left inf.commute inf.left_commute by simp
  also from a3 have "... = 0"
    by blast
  finally show "x;1 ⋅ yT;1 = 0"
    using le_bot by blast
qed

end (* end relation_algebra_rtc *)

subsection ‹Consequences with the Tarski rule›

context relation_algebra_rtc_tarski
begin

text ‹General theorems›

lemma reachable_implies_predecessor:
  assumes "p ≠ q"
      and "point p"
      and "point q"
      and "x⋆;q ≤ xT⋆;p"
    shows "x;q ≠ 0"
proof
  assume contra: "x;q=0"
  with assms(4) have "q ≤ xT⋆;p"
    by (simp add: independence1)
  hence "p ≤ x⋆;q"
    by (metis assms(2,3) point_swap star_conv)
  with contra assms(2,3) have "p=q"
    by (simp add: independence1 is_point_def point_singleton point_is_point)
  with assms(1) show False
    by simp
qed

lemma acyclic_imp_one_step_different_points:
  assumes "is_acyclic x"
      and "point p"
      and "point q"
      and "p ≤ x;q"
    shows "p ≤ -q" and "p ≠ q"
using acyclic_reachable_points assms point_is_point point_not_equal(1) by auto

text ‹Start points and end points›

lemma start_point_iff2:
  assumes "path x"
    shows "is_point (start_points x) ⟷ has_start_points x"
proof -
  have "has_start_points x ⟷ 1 ≤ -(1;x);x;1"
    by (simp add: order.eq_iff)
  also have "... ⟷ 1 ≤ 1;xT;-(xT;1)"
    by (metis comp_assoc conv_compl conv_contrav conv_iso conv_one)
  also have "... ⟷ 1 ≤ 1;(x;1 ⋅ -(xT;1))"
    by (metis (no_types) conv_contrav conv_one inf.commute is_vector_def one_idem_mult ra_2 vector_1
              vector_meet_comp_x)
  also have "... ⟷ 1 = 1;(x;1 ⋅ -(xT;1))"
    by (simp add: order.eq_iff)
  also have "... ⟷ x;1 ⋅ -(xT;1) ≠ 0"
    by (metis tarski comp_assoc one_compl ra_1 ss_p18)
  also have "... ⟷ is_point (start_points x)"
    using assms is_point_def start_point_zero_point by blast
  finally show ?thesis ..
qed

lemma end_point_iff2:
  assumes "path x"
    shows "is_point (end_points x) ⟷ has_end_points x"
by (metis assms conv_invol conv_has_start_points conv_path start_point_iff2)

lemma edge_is_path:
  assumes "is_point p"
      and "is_point q"
    shows "path (p;qT)"
  apply (unfold path_def; intro conjI)
    apply (metis assms comp_assoc is_point_def le_supI1 star_ext vector_rectangle point_equations(3))
   apply (metis is_p_fun_def assms comp_assoc conv_contrav conv_invol is_inj_def is_point_def
                vector_2_var vector_meet_comp_x' point_equations)
  by (metis is_inj_def assms conv_invol conv_times is_point_def p_fun_mult_var vector_meet_comp)

lemma edge_start:
  assumes "is_point p"
      and "is_point q"
      and "p ≠ q"
    shows "start_points (p;qT) = p"
using assms by (simp add: comp_assoc point_equations(1,3) point_not_equal inf.absorb1)

lemma edge_end:
  assumes "is_point p"
      and "is_point q"
      and "p ≠ q"
    shows "end_points (p;qT) = q"
using assms edge_start by simp

lemma loop_no_start:
  assumes "is_point p"
    shows "start_points (p;pT) = 0"
by simp

lemma loop_no_end:
  assumes "is_point p"
    shows "end_points (p;pT) = 0"
by simp

lemma start_point_no_predecessor:
  "x;start_points(x) = 0"
by (metis inf_top.right_neutral modular_1_aux')

lemma end_point_no_successor:
  "xT;end_points(x) = 0"
by (metis conv_invol start_point_no_predecessor)

lemma start_to_end:
  assumes "path x"
    shows "start_points(x);end_points(x)T ≤ x⋆"
proof (cases "end_points(x) = 0")
  assume "end_points(x) = 0"
  thus ?thesis
    by simp
next
  assume ass: "end_points(x) ≠ 0"
  hence nz: "x;end_points(x) ≠ 0"
    by (metis comp_res_aux compl_bot_eq inf.left_idem)
  have a: "x;end_points(x);end_points(x)T ≤ x + xT"
    by (metis end_point_at_most_one assms(1) is_inj_def comp_assoc mult_isol mult_oner le_supI1)

  have "start_points(x);end_points(x)T = start_points(x);1;end_points(x)T"
    using ass by (simp add: comp_assoc is_vector_def one_compl vector_1)
  also have "... = start_points(x);1;x;end_points(x);1;end_points(x)T"
    using nz tarski by (simp add: comp_assoc)
  also have "... = start_points(x);1;x;end_points(x);end_points(x)T"
    using ass by (simp add: comp_assoc is_vector_def one_compl vector_1)
  also with a assms(1) have "... ≤ x⋆"
    using path_concat_aux_5 comp_assoc eq_refl by simp
  finally show ?thesis .
qed

lemma path_acyclic:
  assumes "has_start_points_path x"
    shows "is_acyclic x"
proof -
  let ?r = "start_points(x)"
  have pt: "point(?r)"
    using assms point_is_point start_point_iff2 by blast
  have "x+⋅1' = (x+)T⋅x+⋅1'"
    by (metis conv_e conv_times inf.assoc inf.left_idem inf_le2 many_strongly_connected_iff_7
              mult_oner star_subid)
  also have "... ≤ xT;1⋅x+⋅1'"
    by (metis conv_contrav inf.commute maddux_20 meet_double_iso plus_top star_conv star_slide_var)
  finally have "?r;(x+⋅1') ≤ ?r;(xT;1⋅x+⋅1')"
    using mult_isol by blast
  also have "... = (?r⋅1;x);(x+⋅1')"
    by (metis (no_types, lifting) comp_assoc conv_contrav conv_invol conv_one inf.assoc
              is_vector_def one_idem_mult vector_2)
  also have "... = ?r;x;(x+⋅1')"
    by (metis comp_assoc inf_top.right_neutral is_vector_def one_compl one_idem_mult vector_1)
  also have "... ≤ (x⋆ + xT⋆);(x+⋅1')"
    using assms(1) mult_isor
    by (meson connected_iff4 dual_order.trans mult_subdistr path_concat_aux3_3)
  also have "... = x⋆;(x+⋅1') + xT+;(x+⋅1')"
    by (metis distrib_right star_star_plus sup.commute)
  also have "... ≤ x⋆;(x+⋅1') + xT;1"
    by (metis join_isol mult_isol plus_top top_greatest)
  finally have "?r;(x+⋅1');1 ≤ x⋆;(x+⋅1');1 + xT;1"
    by (metis distrib_right inf_absorb2 mult_assoc mult_subdistr one_idem_mult)
  hence 1: "?r;(x+⋅1');1 ≤ xT;1"
    using assms(1) path_def inj_implies_step_forwards_backwards sup_absorb2 by simp
  have "x+⋅1' ≤ (x+⋅1');1"
    by (simp add: maddux_20)
  also have "... ≤ ?rT;?r;(x+⋅1');1"
    using pt comp_assoc point_def ss423conv by fastforce
  also have "... ≤ ?rT;xT;1"
    using 1 by (simp add: comp_assoc mult_isol)
  also have "... = 0"
    by (metis start_point_no_predecessor annil conv_contrav conv_zero)
  finally show ?thesis
    using galois_aux le_bot by blast
qed

text ‹Equivalences for ‹terminating››

lemma backward_terminating_iff1:
  assumes "path x"
    shows "backward_terminating x ⟷ has_start_points x ∨ x = 0"
proof
  assume "backward_terminating x"
  hence "1;x;1 ≤ 1;-(1;x);x;1;1"
    by (metis mult_isor mult_isol comp_assoc)
  also have "... = -(1;x);x;1"
    by (metis conv_compl conv_contrav conv_invol conv_one mult_assoc one_compl one_idem_mult)
  finally have "1;x;1 ≤ -(1;x);x;1" .

  with tarski show "has_start_points x ∨ x = 0"
    by (metis top_le)
next
  show "has_start_points x ∨ x = 0 ⟹ backward_terminating x"
    by fastforce
qed

lemma backward_terminating_iff2_aux:
  assumes "path x"
    shows "x;1 ⋅ 1;xT ⋅ -(1;x) ≤ xT⋆"
proof -
  have "x;1 ⋅ 1;xT ≤ x;1;x;xT"
    by (metis conv_invol modular_var_3 vector_meet_comp_x vector_meet_comp_x')
  also from assms have "... ≤ (x⋆ + xT⋆);xT"
    using path_def mult_isor by blast
  also have "... ≤ x⋆;x;xT + xT⋆;xT"
    by (simp add: star_star_plus star_slide_var add_comm)
  also from assms have "... ≤ x⋆;1' + xT⋆;xT"
    by (metis path_def is_inj_def join_iso mult_assoc mult_isol)
  also have "... = x+ + xT⋆"
    by (metis mult_1_right star_slide_var star_star_plus sup.commute)
  also have "... ≤ xT⋆ + 1;x"
    by (metis join_iso mult_isor star_slide_var top_greatest add_comm)
  finally have "x;1 ⋅ 1;xT ≤ xT⋆ + 1;x" .
  thus ?thesis
    by (simp add: galois_1 sup.commute)
qed

lemma backward_terminating_iff2:
  assumes "path x"
    shows "backward_terminating x ⟷ x ≤ xT⋆;-(xT;1)"
proof
  assume "backward_terminating x"
  with assms have "has_start_points x ∨ x = 0"
    by (simp add: backward_terminating_iff1)
  thus "x ≤ xT⋆;-(xT;1)"
  proof
    assume "x = 0"
    thus ?thesis
      by simp
  next
    assume "has_start_points x"
    hence aux1: "1 = 1;xT;-(xT;1)"
      by (metis comp_assoc conv_compl conv_contrav conv_one)
    have "x = x ⋅ 1"
      by simp
    also have "... ≤ (x;-(1;x) ⋅ 1;xT);-(xT;1)"
      by (metis inf.commute aux1 conv_compl conv_contrav conv_invol conv_one modular_2_var)
    also have "... = (x;1 ⋅ -(1;x) ⋅ 1;xT);-(xT;1)"
      by (metis comp_assoc conv_compl conv_contrav conv_invol conv_one inf.commute inf_top_left
                one_compl ra_1)
    also from assms have "... ≤ xT⋆;-(xT;1)"
      using backward_terminating_iff2_aux inf.commute inf.assoc mult_isor by fastforce
    finally show "x ≤ xT⋆;-(xT;1)" .
  qed
next
  assume "x ≤ xT⋆;-(xT;1)"
  hence"x ≤ xT⋆;-(xT;1) ⋅ x"
    by simp
  also have "... = (xT⋆ ⋅ -(1;x));1 ⋅ x"
    by (metis one_compl conv_compl conv_contrav conv_invol conv_one inf_top_left ra_2)
  also have "... ≤ (xT⋆ ⋅ -(1;x)) ; (1 ⋅ (x⋆ ⋅ -(1;x)T);x)"
    by (metis (mono_tags) conv_compl conv_invol conv_times modular_1_var star_conv)
  also have "... ≤ -(1;x);x⋆;x"
    by (simp add: mult_assoc mult_isol_var)
  also have "... ≤ -(1;x);x;1"
    by (simp add: mult_assoc mult_isol star_slide_var)
  finally show "backward_terminating x" .
qed

lemma backward_terminating_iff3_aux:
  assumes "path x"
    shows "xT;1 ⋅ 1;xT ⋅ -(1;x) ≤ xT⋆"
proof -
  have "xT;1 ⋅ 1;xT ≤ xT;1;x;xT"
    by (metis conv_invol modular_var_3 vector_meet_comp_x vector_meet_comp_x')
  also from assms have "... ≤ (x⋆ + xT⋆);xT"
    using mult_isor path_concat_aux3_2 by blast
  also have "... ≤ x⋆;x;xT + xT⋆;xT"
    by (simp add: star_star_plus star_slide_var add_comm)
  also from assms have "... ≤ x⋆;1' + xT⋆;xT"
    by (metis path_def is_inj_def join_iso mult_assoc mult_isol)
  also have "... = x+ + xT⋆"
    by (metis mult_1_right star_slide_var star_star_plus sup.commute)
  also have "... ≤ xT⋆ + 1;x"
    by (metis join_iso mult_isor star_slide_var top_greatest add_comm)
  finally have "xT;1 ⋅ 1;xT ≤ xT⋆ + 1;x" .
  thus ?thesis
    by (simp add: galois_1 sup.commute)
qed

lemma backward_terminating_iff3:
  assumes "path x"
    shows "backward_terminating x ⟷ xT ≤ xT⋆;-(xT;1)"
proof
  assume "backward_terminating x"
  with assms have "has_start_points x ∨ x = 0"
    by (simp add: backward_terminating_iff1)
  thus "xT ≤ xT⋆;-(xT;1)"
  proof
    assume "x = 0"
    thus ?thesis
      by simp
  next
    assume "has_start_points x"
    hence aux1: "1 = 1;xT;-(xT;1)"
      by (metis comp_assoc conv_compl conv_contrav conv_one)
    have "xT = xT ⋅ 1"
      by simp
    also have "... ≤ (xT;-(1;x) ⋅ 1;xT);-(xT;1)"
      by (metis inf.commute aux1 conv_compl conv_contrav conv_invol conv_one modular_2_var)
    also have "... = (xT;1 ⋅ -(1;x) ⋅ 1;xT);-(xT;1)"
      by (metis comp_assoc conv_compl conv_contrav conv_invol conv_one inf.commute inf_top_left one_compl ra_1)
    also from assms have "... ≤ xT⋆;-(xT;1)"
      using backward_terminating_iff3_aux inf.commute inf.assoc mult_isor by fastforce
    finally show "xT ≤ xT⋆;-(xT;1)" .
  qed
next
  have 1: "-(1;x) ⋅ x = 0"
    by (simp add: galois_aux2 inf.commute maddux_21)
  assume "xT ≤ xT⋆;-(xT;1)"
  hence "x = -(1;x);x⋆ ⋅ x"
    by (metis (mono_tags, lifting) conv_compl conv_contrav conv_iso conv_one inf.absorb2 star_conv)
  also have "... = (-(1;x);x+ + -(1;x);1') ⋅ x"
    by (metis distrib_left star_unfoldl_eq sup_commute)
  also have "... = -(1;x);x+ ⋅ x + -(1;x) ⋅ x"
    by (simp add: inf_sup_distrib2)
  also have "... ≤ -(1;x);x+"
    using 1 by simp
  also have "... ≤ -(1;x);x;1"
    by (simp add: mult_assoc mult_isol star_slide_var)
  finally show "backward_terminating x" .
qed

lemma backward_terminating_iff4:
  assumes "path x"
    shows "backward_terminating x ⟷ x ≤ -(1;x);x⋆"
 apply (subst backward_terminating_iff3)
  apply (rule assms)
 by (metis (mono_tags, lifting) conv_compl conv_iso star_conv conv_contrav conv_one)

lemma forward_terminating_iff1:
  assumes "path x"
    shows "forward_terminating x ⟷ has_end_points x ∨ x = 0"
by (metis comp_assoc eq_refl le_bot one_compl tarski top_greatest)

lemma forward_terminating_iff2:
  assumes "path x"
    shows "forward_terminating x ⟷ xT ≤ x⋆;-(x;1)"
by (metis assms backward_terminating_iff1 backward_terminating_iff2 end_point_iff2
          forward_terminating_iff1 compl_bot_eq conv_compl conv_invol conv_one conv_path
          double_compl start_point_iff2)

lemma forward_terminating_iff3:
  assumes "path x"
    shows "forward_terminating x ⟷ x ≤ x⋆;-(x;1)"
by (metis assms backward_terminating_iff1 backward_terminating_iff3 end_point_iff2
          forward_terminating_iff1 compl_bot_eq conv_compl conv_invol conv_one conv_path
          double_compl start_point_iff2)

lemma forward_terminating_iff4:
  assumes "path x"
    shows "forward_terminating x ⟷ x ≤ -(1;xT);xT⋆"
using forward_terminating_iff2 conv_contrav conv_iso star_conv assms conv_compl by force

lemma terminating_iff1:
  assumes "path x"
    shows "terminating x ⟷ has_start_end_points x ∨ x = 0"
using assms backward_terminating_iff1 forward_terminating_iff1 by fastforce

lemma terminating_iff2:
  assumes "path x"
    shows "terminating x ⟷ x ≤ xT⋆;-(xT;1) ⋅ -(1;xT);xT⋆"
using assms backward_terminating_iff2 forward_terminating_iff2 conv_compl conv_iso star_conv
by force

lemma terminating_iff3:
  assumes "path x"
    shows "terminating x ⟷ x ≤ x⋆;-(x;1) ⋅ -(1;x);x⋆"
using assms backward_terminating_iff4 forward_terminating_iff3 by fastforce

lemma backward_terminating_path_irreflexive:
  assumes "backward_terminating_path x"
    shows "x ≤ -1'"
proof -
  have 1: "x;xT ≤ 1'"
    using assms is_inj_def path_def by blast
  have "x;(xT ⋅ 1') ≤ x;xT ⋅ x"
    by (metis inf.bounded_iff inf.commute mult_1_right mult_subdistl)
  also have "... ≤ 1' ⋅ x"
    using 1 meet_iso by blast
  also have "... = 1' ⋅ xT"
    by (metis conv_e conv_times inf.cobounded1 is_test_def test_eq_conv)
  finally have 2: "xT;-(xT ⋅ 1') ≤ -(xT ⋅ 1')"
    by (metis compl_le_swap1 conv_galois_1 inf.commute)
  have "xT ⋅ 1' ≤ xT;1"
    by (simp add: le_infI1 maddux_20)
  hence "-(xT;1) ≤ -(xT ⋅ 1')"
    using compl_mono by blast
  hence "xT;-(xT ⋅ 1') + -(xT;1) ≤ -(xT ⋅ 1')"
    using 2 by (simp add: le_supI)
  hence "xT⋆;-(xT;1) ≤ -(xT ⋅ 1')"
    by (simp add: rtc_inductl)
  hence "xT ⋅ 1' ⋅ xT⋆;-(xT;1) = 0"
    by (simp add: compl_le_swap1 galois_aux)
  hence "xT ⋅ 1' = 0"
    using assms backward_terminating_iff3 inf.order_iff le_infI1 by blast
  hence "x ⋅ 1' = 0"
    by (simp add: conv_self_conjugate)
  thus ?thesis
    by (simp add: galois_aux)
qed

lemma forward_terminating_path_end_points_1:
  assumes "forward_terminating_path x"
    shows "x ≤ x+;end_points x"
proof -
  have 1: "-(x;1) ⋅ x = 0"
    by (simp add: galois_aux maddux_20)
  have "x = x⋆;-(x;1) ⋅ x"
    using assms forward_terminating_iff3 inf.absorb2 by fastforce
  also have "... = (x+;-(x;1) + 1';-(x;1)) ⋅ x"
    by (simp add: sup.commute)
  also have "... =