# HG changeset patch
# User desharna
# Date 1738576017 -3600
# Node ID ba32209092213c33523db9860a53de75ff5088e4
# Parent  361fbb3e21c8323a1207492cf98609a4aea21fa0
added lemmas ex_terminating_rtranclp_strong and ex_terminating_rtranclp

diff -r 361fbb3e21c8 -r ba3220909221 NEWS
--- a/NEWS	Mon Feb 03 10:04:59 2025 +0100
+++ b/NEWS	Mon Feb 03 10:46:57 2025 +0100
@@ -302,6 +302,8 @@
       wfP_wf_eq ~> wfp_wf_eq
       wf_acc_iff ~> wf_iff_acc
   - Added lemmas.
+      ex_terminating_rtranclp
+      ex_terminating_rtranclp_strong
       strict_partial_order_wfp_on_finite_set
       wf_on_antimono_stronger
       wfp_on_antimono_stronger
diff -r 361fbb3e21c8 -r ba3220909221 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Feb 03 10:04:59 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Feb 03 10:46:57 2025 +0100
@@ -395,6 +395,43 @@
 
 subsubsection \<open>Well-foundedness of transitive closure\<close>
 
+
+
+lemma ex_terminating_rtranclp_strong:
+  assumes wf: "wfp_on {x'. R\<^sup>*\<^sup>* x x'} R\<inverse>\<inverse>"
+  shows "\<exists>y. R\<^sup>*\<^sup>* x y \<and> (\<nexists>z. R y z)"
+proof (cases "\<exists>y. R x y")
+  case True
+  with wf show ?thesis
+  proof (induction rule: Wellfounded.wfp_on_induct)
+    case in_set
+    thus ?case
+      by simp
+  next
+    case (less y)
+    have "R\<^sup>*\<^sup>* x y"
+      using less.hyps mem_Collect_eq[of _ "R\<^sup>*\<^sup>* x"] by iprover
+
+    moreover obtain z where "R y z"
+      using less.prems by iprover
+
+    ultimately have "R\<^sup>*\<^sup>* x z"
+      using rtranclp.rtrancl_into_rtrancl[of R x y z] by iprover
+
+    show ?case
+      using \<open>R y z\<close> \<open>R\<^sup>*\<^sup>* x z\<close> less.IH[of z] rtranclp_trans[of R y z] by blast
+  qed
+next
+  case False
+  thus ?thesis
+    by blast
+qed
+
+lemma ex_terminating_rtranclp:
+  assumes wf: "wfp R\<inverse>\<inverse>"
+  shows "\<exists>y. R\<^sup>*\<^sup>* x y \<and> (\<nexists>z. R y z)"
+  using ex_terminating_rtranclp_strong[OF wfp_on_subset[OF wf subset_UNIV]] .
+
 lemma wf_trancl:
   assumes "wf r"
   shows "wf (r\<^sup>+)"