# 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;v⇧T ≤ x"
and "v;z ≤ y"
shows "w;1;z ≤ x;y"
proof -
from tarski assms(1,2) have "1 = 1;v⇧T;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;v⇧T;v;1;z"
by (simp add: mult_isor mult_isol mult_assoc)
also from assms(1) have "... = w;v⇧T;v;z"
by (metis is_vector_def comp_assoc conv_contrav conv_one)
also from assms(3) have "... ≤ x;v;z"
also from assms(4) have "... ≤ x;y"
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⇧⋆ + x⇧T⇧⋆"

abbreviation many_strongly_connected
where "many_strongly_connected x ≡ x⇧⋆ = x⇧T⇧⋆"

abbreviation one_strongly_connected
where "one_strongly_connected x ≡ x⇧T;1;x⇧T ≤ 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 ⋅ -(x⇧T;1)"

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

abbreviation no_start_points
where "no_start_points x ≡ x;1 ≤ x⇧T;1"

abbreviation no_end_points
where "no_end_points x ≡ x⇧T;1 ≤ x;1"

abbreviation no_start_end_points
where "no_start_end_points x ≡ x;1 = x⇧T;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 ≤ x⇧T⇧⋆ + -(1;x);x;1"

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

abbreviation finite
where "finite x ≡ x ≤ x⇧T⇧⋆ + (-(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 ≤ p⇧T⇧⋆;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"

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 (x⇧T)"
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 (x⇧T)"
by fastforce

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

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

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

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

lemma conv_no_start_end_points:
"no_start_end_points x ⟷ no_start_end_points (x⇧T)"
by fastforce

lemma conv_has_start_points:
"has_start_points x ⟷ has_end_points (x⇧T)"
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 (x⇧T)"
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 (x⇧T)"
by (metis comp_assoc conv_compl conv_contrav conv_iso conv_one)

lemma conv_terminating:
"terminating x ⟷ terminating (x⇧T)"
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 (x⇧T)"
by (metis comp_assoc conv_add conv_compl conv_contrav conv_iso conv_one star_conv)

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

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

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

lemma conv_has_start_points_path:
"has_start_points_path x ⟷ has_end_points_path (x⇧T)"
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 (x⇧T)"
using conv_has_start_end_points conv_path by fastforce

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

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

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

lemma conv_finite_path:
"finite_path x ⟷ finite_path (x⇧T)"
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;x⇧T ≤ x⇧⋆ + x⇧T⇧⋆"
proof
assume 1: "connected x"
have "x;1;x⇧T ≤ x;1;x;x⇧T"
by (metis conv_invol modular_var_3 vector_meet_comp_x')
also have "... ≤ (x⇧+ + x⇧T⇧⋆);x⇧T"
using 1 mult_isor star_star_plus by fastforce
also have "... ≤ x⇧⋆;x;x⇧T + x⇧T⇧⋆"
using join_isol star_slide_var by simp
also from assms(1) have "... ≤ x⇧⋆ + x⇧T⇧⋆"
by (metis is_inj_def comp_assoc join_iso mult_1_right mult_isol)
finally show "x;1;x⇧T ≤ x⇧⋆ + x⇧T⇧⋆" .
next
assume 2: "x;1;x⇧T ≤ x⇧⋆ + x⇧T⇧⋆"
have "x;1;x ≤ x;1;x⇧T;x"
also have "... ≤ (x⇧⋆ + x⇧T⇧+);x"
using 2 by (metis mult_isor star_star_plus sup_commute)
also have "... ≤ x⇧⋆ + x⇧T⇧⋆;x⇧T;x"
using join_iso star_slide_var by simp
also from assms(2) have "... ≤ x⇧⋆ + x⇧T⇧⋆"
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 ⟷ x⇧T;1;x ≤ x⇧⋆ + x⇧T⇧⋆"
by (metis assms connected_conv connected_iff2 inj_p_fun p_fun_inj conv_invol add_commute)

lemma connected_iff4:
"connected x ⟷ x⇧T;1;x⇧T ≤ x⇧⋆ + x⇧T⇧⋆"

lemma connected_iff5:
"connected x ⟷ x⇧+;1;x⇧+ ≤ x⇧⋆ + x⇧T⇧⋆"
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⇧⋆ + x⇧T⇧⋆"
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⇧⋆ + x⇧T⇧⋆"
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⇧⋆ + x⇧T⇧⋆"
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 ⟷ x⇧T ≤ 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 ⟷ x⇧T ≤ x⇧+"
proof
assume as: "many_strongly_connected x"
hence "x⇧T ≤ x⇧⋆ ⋅ (-(1') + x)"
by (metis many_strongly_connected_iff_1 loop_backward_forward inf_greatest)
also have "... ≤ (x⇧⋆ ⋅ -(1')) + (x⇧⋆ ⋅ x)"
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 "x⇧T ≤ x⇧+" .
next
show "x⇧T ≤ 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 ≤ x⇧T⇧⋆"
by (metis conv_invol many_strongly_connected_iff_1)

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

lemma many_strongly_connected_iff_5:
"many_strongly_connected x ⟷ x⇧⋆;x⇧T ≤ 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 ⟷ x⇧T;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 ⟷ x⇧T⇧+ = 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⇧⋆;x⇧T = 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 ⟷ x⇧T;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;x⇧T ≤ x⇧+"

lemma many_strongly_connected_implies_9:
assumes "many_strongly_connected x"
shows "x⇧T;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;x⇧T;x⇧⋆ ≤ x⇧+"
by (simp add: assms comp_assoc mult_isol)

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

lemma many_strongly_connected_implies_11:
assumes "many_strongly_connected x"
shows "x⇧⋆;x⇧T;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⇧⋆;x⇧T;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;x⇧T ≤ 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;x⇧T = 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 "x⇧T;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 "x⇧T;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;x⇧T ≤ x⇧+"
apply (rule iffI)
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 ⟷ x⇧T;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;x⇧T;x⇧⋆ ≤ x⇧+"
apply (rule iffI)
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;x⇧T;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⇧⋆;x⇧T;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⇧⋆;x⇧T;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;x⇧T ≤ 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;x⇧T = 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 ⟷ x⇧T;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 ⟷ x⇧T;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 ⟷ x⇧T;1;x⇧T ≤ x⇧+"
proof
assume 1: "one_strongly_connected x"
have "x⇧T;1;x⇧T ≤ x⇧T;x;x⇧T;1;x⇧T"
by (metis conv_invol mult_isor x_leq_triple_x)
also from 1 have "... ≤ x⇧T;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 "x⇧T;1;x⇧T ≤ x⇧+"
.
next
assume "x⇧T;1;x⇧T ≤ 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 ⟷ x⇧T;1;x⇧T = 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 ≤ x⇧T⇧⋆"
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 ≤ x⇧T⇧+"
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 = x⇧T⇧+"
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 ⟷ x⇧T;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;x⇧T = 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"

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 ⟷ x⇧T;1;x ≤ x⇧+"
proof
assume "one_strongly_connected x"
thus "x⇧T;1;x ≤ x⇧+"
next
assume 1: "x⇧T;1;x ≤ x⇧+"
hence "x⇧T;1;x⇧T ≤ x⇧⋆;x;x⇧T"
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;x⇧T ≤ 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⇧+"
next
assume 1: "x;1;x ≤ x;x⇧+"
have "x⇧T;1;x ≤ x⇧T;x;x⇧T;1;x"
by (metis conv_invol mult_isor x_leq_triple_x)
also have "... ≤ x⇧T;x;1;x"
by (metis comp_assoc mult_double_iso top_greatest)
also from 1 have "... ≤ x⇧T;x;x⇧+"
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

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 (x⇧T)"
by simp

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

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

from aux have "x;1 ⋅ 1;x⇧T ⋅ -(x⇧T;1) ⋅ -(1;x) ≤ 1'"
hence "(x;1 ⋅ -(x⇧T;1)) ⋅ (x;1 ⋅ -(x⇧T;1))⇧T ≤ 1'"
by (simp add: conv_compl inf.assoc inf.left_commute)
with isvec have "(x;1 ⋅ -(x⇧T;1)) ; (x;1 ⋅ -(x⇧T;1))⇧T ≤ 1'"
by (metis vector_meet_comp')
thus "is_inj (start_points x)"
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;s⇧T ≤ 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 "e⇧T ; (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;s⇧T ≤ x"
shows "point(x;s)"
using predecessor_point' assms by blast

lemma points_of_path_iff:
shows "(x + x⇧T);1 = x⇧T;1 + start_points(x)"
and "(x + x⇧T);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 ⋅ y⇧T;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 ⋅ y⇧T;1) + (x;1 ⋅ y;1 ⋅ -(y⇧T;1))"
by simp
also from assms(1) have "... = x;1 ⋅ y;1 ⋅ -(y⇧T;1)"
by (metis aux6_var de_morgan_3 inf.left_commute inf_compl_bot inf_sup_absorb)
also from assms(2) have "... = x;1 ⋅ x⇧T;1 ⋅ -(x;1)"
also have "... = 0"
finally show ?thesis .
qed

lemma path_concat_aux_2:
assumes "x;1 ⋅ x⇧T;1 ⋅ y⇧T;1 = 0"
and "end_points x = start_points y"
shows "x⇧T;1 ⋅ y⇧T;1 = 0"
proof -
have "y⇧T;1 ⋅ x⇧T;1 ⋅ (x⇧T)⇧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;x⇧T ≤ x⇧⋆ + x⇧T⇧⋆"
proof -
have "x;1;x⇧T ≤ x;1;x⇧T;x;x⇧T"
by (metis comp_assoc conv_invol mult_isol x_leq_triple_x)
also have "... ≤ x;1;x;x⇧T"
by (metis mult_isol mult_isor mult_assoc top_greatest)
also from assms have "... ≤ (x⇧⋆ + x⇧T⇧⋆);x⇧T"
using path_def comp_assoc mult_isor by blast
also have "... = x⇧⋆;x;x⇧T + x⇧T⇧⋆;x⇧T"
also have "... ≤ x⇧⋆;1' + x⇧T⇧⋆;x⇧T"
by (metis assms path_def is_inj_def join_iso mult_isol mult_assoc)
also have "... ≤ x⇧⋆ + x⇧T⇧⋆"
using join_isol by simp
finally show ?thesis .
qed

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

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

lemma path_concat_aux_3:
assumes "path x"
and "y ≤ x⇧+ + x⇧T⇧+"
and "z ≤ x⇧+ + x⇧T⇧+"
shows "y;1;z ≤ x⇧⋆ + x⇧T⇧⋆"
proof -
from assms(2,3) have "y;1;z ≤ (x⇧+ + x⇧T⇧+);1;(x⇧+ + x⇧T⇧+)"
using mult_isol_var mult_isor by blast
also have "... = x⇧+;1;x⇧+ + x⇧+;1;x⇧T⇧+ + x⇧T⇧+;1;x⇧+ + x⇧T⇧+;1;x⇧T⇧+"
by (simp add: distrib_left sup_commute sup_left_commute)
also have "... = x;x⇧⋆;1;x⇧⋆;x + x;x⇧⋆;1;x⇧T⇧⋆;x⇧T + x⇧T;x⇧T⇧⋆;1;x⇧⋆;x + x⇧T;x⇧T⇧⋆;1;x⇧T⇧⋆;x⇧T"
also have "... ≤ x;1;x + x;x⇧⋆;1;x⇧T⇧⋆;x⇧T + x⇧T;x⇧T⇧⋆;1;x⇧⋆;x + x⇧T;x⇧T⇧⋆;1;x⇧T⇧⋆;x⇧T"
by (metis comp_assoc mult_double_iso top_greatest join_iso)
also have "... ≤ x;1;x + x;1;x⇧T + x⇧T;x⇧T⇧⋆;1;x⇧⋆;x + x⇧T;x⇧T⇧⋆;1;x⇧T⇧⋆;x⇧T"
by (metis comp_assoc mult_double_iso top_greatest join_iso join_isol)
also have "... ≤ x;1;x + x;1;x⇧T + x⇧T;1;x + x⇧T;x⇧T⇧⋆;1;x⇧T⇧⋆;x⇧T"
by (metis comp_assoc mult_double_iso top_greatest join_iso join_isol)
also have "... ≤ x;1;x + x;1;x⇧T + x⇧T;1;x + x⇧T;1;x⇧T"
by (metis comp_assoc mult_double_iso top_greatest join_isol)
also have "... ≤ x⇧⋆ + x⇧T⇧⋆"
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⇧⋆ + x⇧T⇧⋆ ≤ x⇧⋆ + x⇧T;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 + x⇧T"
shows "y;1;z ≤ x⇧⋆"
proof -
from assms(1) have "x;1;x ≤ x⇧⋆ + x⇧T;1"
using path_def path_concat_aux_4 dual_order.trans by blast
hence aux1: "x;1;x ⋅ -(x⇧T;1) ≤ x⇧⋆"

from assms(1) have "x;1;x⇧T ≤ x⇧⋆ + x⇧T;1"
using dual_order.trans path_concat_aux3_1 path_concat_aux_4 by blast
hence aux2: "x;1;x⇧T ⋅ -(x⇧T;1) ≤ x⇧⋆"

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

lemma path_conditions_disjoint_points_iff:
"x;1 ⋅ (x⇧T;1 + y;1) ⋅ y⇧T;1 = 0 ∧ start_points x ⋅ end_points y = 0 ⟷ x;1 ⋅ y⇧T;1 = 0"
proof
assume 1: "x ; 1 ⋅ y⇧T ; 1 = 0"
hence g1: "x ; 1 ⋅ (x⇧T ; 1 + y ; 1) ⋅ y⇧T ; 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 ⋅ (x⇧T;1 + y;1) ⋅ y⇧T;1 = 0 ∧ start_points x ⋅ end_points y = 0"
using g1 and g2 by simp
next
assume a: "x;1 ⋅ (x⇧T;1 + y;1) ⋅ y⇧T;1 = 0 ∧ start_points x ⋅ end_points y = 0"
from a have a1: "x;1 ⋅ x⇧T;1 ⋅ y⇧T;1 = 0"
from a have a2: "x;1 ⋅ y;1 ⋅ y⇧T;1 = 0"
from a have a3: "start_points x ⋅ end_points y = 0"
by blast

have "x;1 ⋅ y⇧T;1 = x;1 ⋅ x⇧T;1 ⋅ y⇧T;1 + x;1 ⋅ -(x⇧T;1) ⋅ y⇧T;1"
by (metis aux4 inf_sup_distrib2)
also from a1 have "... = x;1 ⋅ -(x⇧T;1) ⋅ y⇧T;1"
using sup_bot_left by blast
also have "... = x;1 ⋅ -(x⇧T;1) ⋅ y;1 ⋅ y⇧T;1 + x;1 ⋅ -(x⇧T;1) ⋅ -(y;1) ⋅ y⇧T;1"
by (metis aux4 inf_sup_distrib2)
also have "... ≤ x;1 ⋅ y;1 ⋅ y⇧T;1 + x;1 ⋅ -(x⇧T;1) ⋅ -(y;1) ⋅ y⇧T;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 ⋅ y⇧T;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 ≤ x⇧T⇧⋆;p"
shows "x;q ≠ 0"
proof
assume contra: "x;q=0"
with assms(4) have "q ≤ x⇧T⇧⋆;p"
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"
also have "... ⟷ 1 ≤ 1;x⇧T;-(x⇧T;1)"
by (metis comp_assoc conv_compl conv_contrav conv_iso conv_one)
also have "... ⟷ 1 ≤ 1;(x;1 ⋅ -(x⇧T;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 ⋅ -(x⇧T;1))"
also have "... ⟷ x;1 ⋅ -(x⇧T;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;q⇧T)"
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;q⇧T) = 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;q⇧T) = q"
using assms edge_start by simp

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

lemma loop_no_end:
assumes "is_point p"
shows "end_points (p;p⇧T) = 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:
"x⇧T;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 + x⇧T"
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 "... ≤ x⇧T;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;(x⇧T;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⇧⋆ + x⇧T⇧⋆);(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') + x⇧T⇧+;(x⇧+⋅1')"
by (metis distrib_right star_star_plus sup.commute)
also have "... ≤ x⇧⋆;(x⇧+⋅1') + x⇧T;1"
by (metis join_isol mult_isol plus_top top_greatest)
finally have "?r;(x⇧+⋅1');1 ≤ x⇧⋆;(x⇧+⋅1');1 + x⇧T;1"
by (metis distrib_right inf_absorb2 mult_assoc mult_subdistr one_idem_mult)
hence 1: "?r;(x⇧+⋅1');1 ≤ x⇧T;1"
using assms(1) path_def inj_implies_step_forwards_backwards sup_absorb2 by simp
have "x⇧+⋅1' ≤ (x⇧+⋅1');1"
also have "... ≤ ?r⇧T;?r;(x⇧+⋅1');1"
using pt comp_assoc point_def ss423conv by fastforce
also have "... ≤ ?r⇧T;x⇧T;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;x⇧T ⋅ -(1;x) ≤ x⇧T⇧⋆"
proof -
have "x;1 ⋅ 1;x⇧T ≤ x;1;x;x⇧T"
by (metis conv_invol modular_var_3 vector_meet_comp_x vector_meet_comp_x')
also from assms have "... ≤ (x⇧⋆ + x⇧T⇧⋆);x⇧T"
using path_def mult_isor by blast
also have "... ≤ x⇧⋆;x;x⇧T + x⇧T⇧⋆;x⇧T"
also from assms have "... ≤ x⇧⋆;1' + x⇧T⇧⋆;x⇧T"
by (metis path_def is_inj_def join_iso mult_assoc mult_isol)
also have "... = x⇧+ + x⇧T⇧⋆"
by (metis mult_1_right star_slide_var star_star_plus sup.commute)
also have "... ≤ x⇧T⇧⋆ + 1;x"
by (metis join_iso mult_isor star_slide_var top_greatest add_comm)
finally have "x;1 ⋅ 1;x⇧T ≤ x⇧T⇧⋆ + 1;x" .
thus ?thesis
qed

lemma backward_terminating_iff2:
assumes "path x"
shows "backward_terminating x ⟷ x ≤ x⇧T⇧⋆;-(x⇧T;1)"
proof
assume "backward_terminating x"
with assms have "has_start_points x ∨ x = 0"
thus "x ≤ x⇧T⇧⋆;-(x⇧T;1)"
proof
assume "x = 0"
thus ?thesis
by simp
next
assume "has_start_points x"
hence aux1: "1 = 1;x⇧T;-(x⇧T;1)"
by (metis comp_assoc conv_compl conv_contrav conv_one)
have "x = x ⋅ 1"
by simp
also have "... ≤ (x;-(1;x) ⋅ 1;x⇧T);-(x⇧T;1)"
by (metis inf.commute aux1 conv_compl conv_contrav conv_invol conv_one modular_2_var)
also have "... = (x;1 ⋅ -(1;x) ⋅ 1;x⇧T);-(x⇧T;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 "... ≤ x⇧T⇧⋆;-(x⇧T;1)"
using backward_terminating_iff2_aux inf.commute inf.assoc mult_isor by fastforce
finally show "x ≤ x⇧T⇧⋆;-(x⇧T;1)" .
qed
next
assume "x ≤ x⇧T⇧⋆;-(x⇧T;1)"
hence"x ≤ x⇧T⇧⋆;-(x⇧T;1) ⋅ x"
by simp
also have "... = (x⇧T⇧⋆ ⋅ -(1;x));1 ⋅ x"
by (metis one_compl conv_compl conv_contrav conv_invol conv_one inf_top_left ra_2)
also have "... ≤ (x⇧T⇧⋆ ⋅ -(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"
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 "x⇧T;1 ⋅ 1;x⇧T ⋅ -(1;x) ≤ x⇧T⇧⋆"
proof -
have "x⇧T;1 ⋅ 1;x⇧T ≤ x⇧T;1;x;x⇧T"
by (metis conv_invol modular_var_3 vector_meet_comp_x vector_meet_comp_x')
also from assms have "... ≤ (x⇧⋆ + x⇧T⇧⋆);x⇧T"
using mult_isor path_concat_aux3_2 by blast
also have "... ≤ x⇧⋆;x;x⇧T + x⇧T⇧⋆;x⇧T"
also from assms have "... ≤ x⇧⋆;1' + x⇧T⇧⋆;x⇧T"
by (metis path_def is_inj_def join_iso mult_assoc mult_isol)
also have "... = x⇧+ + x⇧T⇧⋆"
by (metis mult_1_right star_slide_var star_star_plus sup.commute)
also have "... ≤ x⇧T⇧⋆ + 1;x"
by (metis join_iso mult_isor star_slide_var top_greatest add_comm)
finally have "x⇧T;1 ⋅ 1;x⇧T ≤ x⇧T⇧⋆ + 1;x" .
thus ?thesis
qed

lemma backward_terminating_iff3:
assumes "path x"
shows "backward_terminating x ⟷ x⇧T ≤ x⇧T⇧⋆;-(x⇧T;1)"
proof
assume "backward_terminating x"
with assms have "has_start_points x ∨ x = 0"
thus "x⇧T ≤ x⇧T⇧⋆;-(x⇧T;1)"
proof
assume "x = 0"
thus ?thesis
by simp
next
assume "has_start_points x"
hence aux1: "1 = 1;x⇧T;-(x⇧T;1)"
by (metis comp_assoc conv_compl conv_contrav conv_one)
have "x⇧T = x⇧T ⋅ 1"
by simp
also have "... ≤ (x⇧T;-(1;x) ⋅ 1;x⇧T);-(x⇧T;1)"
by (metis inf.commute aux1 conv_compl conv_contrav conv_invol conv_one modular_2_var)
also have "... = (x⇧T;1 ⋅ -(1;x) ⋅ 1;x⇧T);-(x⇧T;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 "... ≤ x⇧T⇧⋆;-(x⇧T;1)"
using backward_terminating_iff3_aux inf.commute inf.assoc mult_isor by fastforce
finally show "x⇧T ≤ x⇧T⇧⋆;-(x⇧T;1)" .
qed
next
have 1: "-(1;x) ⋅ x = 0"
assume "x⇧T ≤ x⇧T⇧⋆;-(x⇧T;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"
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 ⟷ x⇧T ≤ 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;x⇧T);x⇧T⇧⋆"
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 ≤ x⇧T⇧⋆;-(x⇧T;1) ⋅ -(1;x⇧T);x⇧T⇧⋆"
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;x⇧T ≤ 1'"
using assms is_inj_def path_def by blast
have "x;(x⇧T ⋅ 1') ≤ x;x⇧T ⋅ 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' ⋅ x⇧T"
by (metis conv_e conv_times inf.cobounded1 is_test_def test_eq_conv)
finally have 2: "x⇧T;-(x⇧T ⋅ 1') ≤ -(x⇧T ⋅ 1')"
by (metis compl_le_swap1 conv_galois_1 inf.commute)
have "x⇧T ⋅ 1' ≤ x⇧T;1"
hence "-(x⇧T;1) ≤ -(x⇧T ⋅ 1')"
using compl_mono by blast
hence "x⇧T;-(x⇧T ⋅ 1') + -(x⇧T;1) ≤ -(x⇧T ⋅ 1')"
using 2 by (simp add: le_supI)
hence "x⇧T⇧⋆;-(x⇧T;1) ≤ -(x⇧T ⋅ 1')"
hence "x⇧T ⋅ 1' ⋅ x⇧T⇧⋆;-(x⇧T;1) = 0"
hence "x⇧T ⋅ 1' = 0"
using assms backward_terminating_iff3 inf.order_iff le_infI1 by blast
hence "x ⋅ 1' = 0"
thus ?thesis