# Theory Wellfounded_Extra

```theory Wellfounded_Extra
imports
Main
"Ordered_Resolution_Prover.Lazy_List_Chain"
begin

definition wf_on :: "'a set ⇒ 'a rel ⇒ bool"
where "wf_on A r ⟷ (∀P. (∀x ∈ A. (∀y ∈ A. (y, x) ∈ r ⟶ P y) ⟶ P x) ⟶ (∀x ∈ A. P x))"

abbreviation wf :: "'a rel ⇒ bool" where
"wf ≡ wf_on UNIV"

definition wfp_on :: "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool" where
"wfp_on A R ⟷ (∀P. (∀x ∈ A. (∀y ∈ A. R y x ⟶ P y) ⟶ P x) ⟶ (∀x ∈ A. P x))"

abbreviation wfp :: "('a ⇒ 'a ⇒ bool) ⇒ bool" where
"wfp ≡ wfp_on UNIV"

lemma wf_def[no_atp]: "wf r ⟷ (∀P. (∀x. (∀y. (y, x) ∈ r ⟶ P y) ⟶ P x) ⟶ (∀x. P x))"

lemma wf_onI:
"(⋀P x. (⋀y. y ∈ A ⟹ (⋀z. z ∈ A ⟹ (z, y) ∈ r ⟹ P z) ⟹ P y) ⟹ x ∈ A ⟹ P x) ⟹ wf_on A r"
unfolding wf_on_def by metis

lemma wfI: "(⋀P x. (⋀y. (⋀z. (z, y) ∈ r ⟹ P z) ⟹ P y) ⟹ P x) ⟹ wf r"
by (auto simp: wf_on_def)

lemma wf_on_induct[consumes 1, case_names less in_dom]:
assumes
"wf_on A r" and
"⋀x. x ∈ A ⟹ (⋀y. y ∈ A ⟹ (y, x) ∈ r ⟹ P y) ⟹ P x" and
"x ∈ A"
shows "P x"
using assms unfolding wf_on_def by metis

lemma "wf_on UNIV r ⟷ Wellfounded.wf r"

lemma wfp_iff_wfP: "wfp R ⟷ Wellfounded.wfP R"
by (metis (no_types, opaque_lifting) UNIV_I wfPUNIVI wfP_induct_rule wfp_on_def)

lemma wfp_on_wf_on_iff[pred_set_conv]: "wfp_on A (λx y. (x, y) ∈ r) ⟷ wf_on A r"

subsection ‹Basic Results›

text ‹Point-free characterization of well-foundedness›

lemma wf_onE_pf:
assumes wf: "wf_on A r" and "B ⊆ A" and "B ⊆ r `` B"
shows "B = {}"
proof -
from wf have "x ∉ B" if "x ∈ A" for x
proof (induction x rule: wf_on_induct)
case (less x)
then show ?case
by (metis ImageE assms(2) assms(3) in_mono)
next
case in_dom
show ?case
using that .
qed
with ‹B ⊆ A› show ?thesis
by blast
qed

lemma wfE_pf: "wf R ⟹ A ⊆ R `` A ⟹ A = {}"
by (auto elim!: wf_onE_pf)

lemma wf_onI_pf:
assumes "⋀B. B ⊆ A ⟹ B ⊆ R `` B ⟹ B = {}"
shows "wf_on A R"
unfolding wf_on_def
proof (intro allI impI ballI)
fix P :: "'a ⇒ bool" and x :: 'a
let ?B = "{x ∈ A. ¬ P x}"
assume "∀x∈A. (∀y∈A. (y, x) ∈ R ⟶ P y) ⟶ P x"
hence "?B ⊆ R `` ?B" by blast
with assms(1)[of ?B] have "{x ∈ A. ¬ P x} = {}"
by simp
moreover assume "x ∈ A"
ultimately show "P x"
by simp
qed

lemma wfI_pf: "(⋀A. A ⊆ R `` A ⟹ A = {}) ⟹ wf R"
by (auto intro!: wf_onI_pf)

subsubsection ‹Minimal-element characterization of well-foundedness›

lemma minimal_if_wf_on:
assumes wf: "wf_on A R" and "B ⊆ A" and "B ≠ {}"
shows "∃z ∈ B. ∀y. (y, z) ∈ R ⟶ y ∉ B"
using wf_onE_pf[OF wf ‹B ⊆ A›]
by (metis Image_iff assms(3) subsetI)

lemma wfE_min:
assumes wf: "wf R" and Q: "x ∈ Q"
obtains z where "z ∈ Q" "⋀y. (y, z) ∈ R ⟹ y ∉ Q"
using Q wfE_pf[OF wf, of Q] by blast

lemma wfE_min':
"wf R ⟹ Q ≠ {} ⟹ (⋀z. z ∈ Q ⟹ (⋀y. (y, z) ∈ R ⟹ y ∉ Q) ⟹ thesis) ⟹ thesis"
using wfE_min[of R _ Q] by blast

lemma wf_on_if_minimal:
assumes "⋀B. B ⊆ A ⟹ B ≠ {} ⟹ ∃z ∈ B. ∀y. (y, z) ∈ R ⟶ y ∉ B"
shows "wf_on A R"
proof (rule wf_onI_pf)
fix B
show "B ⊆ A ⟹ B ⊆ R `` B ⟹ B = {}"
using assms by (metis ImageE subset_eq)
qed

lemma wfI_min:
assumes a: "⋀x Q. x ∈ Q ⟹ ∃z∈Q. ∀y. (y, z) ∈ R ⟶ y ∉ Q"
shows "wf R"
proof (rule wfI_pf)
fix A
assume b: "A ⊆ R `` A"
have False if "x ∈ A" for x
using a[OF that] b by blast
then show "A = {}" by blast
qed

lemma wf_on_iff_minimal: "wf_on A r ⟷ (∀B ⊆ A. B ≠ {} ⟶ (∃z ∈ B. ∀y. (y, z) ∈ r ⟶ y ∉ B))"
using minimal_if_wf_on wf_on_if_minimal by metis

lemma wf_iff_minimal: "wf r ⟷ (∀B. B ≠ {} ⟶ (∃z ∈ B. ∀y. (y, z) ∈ r ⟶ y ∉ B))"
using wf_on_iff_minimal[of UNIV, simplified] by metis

lemma wf_eq_minimal[no_atp]: "wf r ⟷ (∀Q x. x ∈ Q ⟶ (∃z∈Q. ∀y. (y, z) ∈ r ⟶ y ∉ Q))"
unfolding wf_iff_minimal by auto

lemma wfp_on_iff_minimal: "wfp_on A R ⟷ (∀B ⊆ A. B ≠ {} ⟶ (∃z ∈ B. ∀y. R y z ⟶ y ∉ B))"
using wf_on_iff_minimal[of A, to_pred] by simp

lemma wfp_iff_minimal: "wfp R ⟷ (∀B. B ≠ {} ⟶ (∃z ∈ B. ∀y. R y z ⟶ y ∉ B))"

lemmas wfP_eq_minimal[no_atp] = wf_eq_minimal[to_pred]

lemma ex_trans_min_element_if_wf_on:
assumes wf: "wf_on A r" and x_in: "x ∈ A"
shows "∃y ∈ A. (y, x) ∈ r⇧* ∧ ¬(∃z ∈ A. (z, y) ∈ r)"
using wf
proof (induction x rule: wf_on_induct)
case (less x)
thus ?case
by (metis rtrancl.rtrancl_into_rtrancl rtrancl.rtrancl_refl)
next
case in_dom
thus ?case
using x_in by metis
qed

lemma ex_trans_min_element_if_wfp_on: "wfp_on A R ⟹ x ∈ A ⟹ ∃y∈A. R⇧*⇧* y x ∧ ¬ (∃z∈A. R z y)"
by (rule ex_trans_min_element_if_wf_on[to_pred])

subsection ‹Bound Restriction and Monotonicity›

lemma wf_on_subset: "wf_on A r ⟹ B ⊆ A ⟹ wf_on B r"
unfolding wf_on_iff_minimal
by (meson order_trans)

lemma wfp_on_subset: "wfp_on A R ⟹ B ⊆ A ⟹ wfp_on B R"
by (rule wf_on_subset[of A _ B, to_pred])

lemma wf_on_mono_strong:
"wf_on A r ⟹ (⋀x y. x ∈ A ⟹ y ∈ A ⟹ (x, y) ∈ q ⟹ (x, y) ∈ r) ⟹ wf_on A q"
unfolding wf_on_iff_minimal
by (meson in_mono)

lemma wfp_on_mono_strong:
"wfp_on A R ⟹ (⋀x y. x ∈ A ⟹ y ∈ A ⟹ Q x y ⟹ R x y) ⟹ wfp_on A Q"
by (rule wf_on_mono_strong[to_pred])

text ‹Well-foundedness of subsets›

lemma wf_subset: "wf r ⟹ p ⊆ r ⟹ wf p"

lemmas wfP_subset = wf_subset [to_pred]

text ‹Well-foundedness of the empty relation›

lemma wf_empty [iff]: "wf {}"

lemma wfP_empty [iff]: "wfp (λx y. False)"
proof -
have "wfp bot"
then show ?thesis
qed

lemma wf_Int1: "wf r ⟹ wf (r ∩ r')"
by (erule wf_subset) (rule Int_lower1)

lemma wf_Int2: "wf r ⟹ wf (r' ∩ r)"
by (erule wf_subset) (rule Int_lower2)

definition inv_imagep_on :: "'a set ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where
"inv_imagep_on A R f = (λx y. x ∈ A ∧ y ∈ A ∧ R (f x) (f y))"

lemma wfp_on_inv_imagep:
assumes wf: "wfp_on (f ` A) R"
shows "wfp_on A (inv_imagep R f)"
unfolding wfp_on_iff_minimal
proof (intro allI impI)
fix B assume "B ⊆ A" and "B ≠ {}"
hence "∃z∈f ` B. ∀y. R y z ⟶ y ∉ f ` B"
using wf[unfolded wfp_on_iff_minimal, rule_format, of "f ` B"] by blast
thus "∃z∈B. ∀y. inv_imagep R f y z ⟶ y ∉ B"
unfolding inv_imagep_def
by (metis image_iff)
qed

lemma wfp_on_if_convertible_to_wfp:
assumes
wf: "wfp_on (f ` A) Q" and
convertible: "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ Q (f x) (f y))"
shows "wfp_on A R"
unfolding wfp_on_iff_minimal
proof (intro allI impI)
fix B assume "B ⊆ A" and "B ≠ {}"
moreover from wf have "wfp_on A (inv_imagep Q f)"
by (rule wfp_on_inv_imagep)
ultimately obtain y where "y ∈ B" and "⋀z. Q (f z) (f y) ⟹ z ∉ B"
unfolding wfp_on_iff_minimal in_inv_imagep by metis
thus "∃z ∈ B. ∀y. R y z ⟶ y ∉ B"
using ‹B ⊆ A› convertible by blast
qed

definition lex_prodp where
"lex_prodp R⇩A R⇩B x y ⟷ R⇩A (fst x) (fst y) ∨ fst x = fst y ∧ R⇩B (snd x) (snd y)"

lemma lex_prodp_lex_prod_iff[pred_set_conv]:
"lex_prodp R⇩A R⇩B x y ⟷ (x, y) ∈ lex_prod {(x, y). R⇩A x y} {(x, y). R⇩B x y}"
unfolding lex_prodp_def lex_prod_def by auto

lemma lex_prod_lex_prodp_iff:
"lex_prod {(x, y). R⇩A x y} {(x, y). R⇩B x y} = {(x, y). lex_prodp R⇩A R⇩B x y}"
unfolding lex_prodp_def lex_prod_def by auto

lemma wf_on_lex_prod:
assumes wfA: "wf_on A r⇩A" and wfB: "wf_on B r⇩B"
shows "wf_on (A × B) (r⇩A <*lex*> r⇩B)"
unfolding wf_on_iff_minimal
proof (intro allI impI)
fix AB assume "AB ⊆ A × B" and "AB ≠ {}"
hence "fst ` AB ⊆ A" and "snd ` AB ⊆ B"
by auto

from ‹fst ` AB ⊆ A› ‹AB ≠ {}› obtain a where
a_in: "a ∈ fst ` AB" and
a_minimal: "(∀y. (y, a) ∈ r⇩A ⟶ y ∉ fst ` AB)"
using wfA[unfolded wf_on_iff_minimal, rule_format, of "fst ` AB"]
by auto

from ‹snd ` AB ⊆ B› ‹AB ≠ {}› a_in obtain b where
b_in: "b ∈ snd ` {p ∈ AB. fst p = a}" and
b_minimal: "(∀y. (y, b) ∈ r⇩B ⟶ y ∉ snd ` {p ∈ AB. fst p = a})"
using wfB[unfolded wf_on_iff_minimal, rule_format, of "snd ` {p ∈ AB. fst p = a}"]
by blast

show "∃z∈AB. ∀y. (y, z) ∈ r⇩A <*lex*> r⇩B ⟶ y ∉ AB"
proof (rule bexI)
show "(a, b) ∈ AB"
using b_in by fastforce
next
show "∀y. (y, (a, b)) ∈ r⇩A <*lex*> r⇩B ⟶ y ∉ AB"
proof (intro allI impI)
fix p assume "(p, (a, b)) ∈ r⇩A <*lex*> r⇩B"
hence "(fst p, a) ∈ r⇩A ∨ fst p = a ∧ (snd p, b) ∈ r⇩B"
unfolding lex_prod_def by auto
then show "p ∉ AB"
proof (elim disjE conjE)
assume "(fst p, a) ∈ r⇩A"
hence "fst p ∉ fst ` AB"
using a_minimal by simp
thus ?thesis
by auto
next
assume "fst p = a" and "(snd p, b) ∈ r⇩B"
hence "snd p ∉ snd ` {p ∈ AB. fst p = a}"
using b_minimal by simp
thus "p ∉ AB"
using ‹fst p = a› by auto
qed
qed
qed
qed

lemma wfp_on_lex_prodp: "wfp_on A R⇩A ⟹ wfp_on B R⇩B ⟹ wfp_on (A × B) (lex_prodp R⇩A R⇩B)"
by (rule wf_on_lex_prod[to_pred, unfolded lex_prod_lex_prodp_iff, to_pred])

corollary wfp_lex_prodp: "wfp R⇩A ⟹ wfp R⇩B ⟹ wfp (lex_prodp R⇩A R⇩B)"
by (rule wfp_on_lex_prodp[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])

lemma wfp_on_sup_if_convertible_to_wfp:
includes lattice_syntax
assumes
wf_S: "wfp_on A S" and
wf_Q: "wfp_on (f ` A) Q" and
convertible_R: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ Q (f x) (f y)" and
convertible_S: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ S x y ⟹ Q (f x) (f y) ∨ f x = f y"
shows "wfp_on A (R ⊔ S)"
proof (rule wfp_on_if_convertible_to_wfp)
show "wfp_on ((λx. (f x, x)) ` A) (lex_prodp Q S)"
proof (rule wfp_on_subset)
show "wfp_on (f ` A × A) (lex_prodp Q S)"
by (rule wfp_on_lex_prodp[OF wf_Q wf_S])
next
show "(λx. (f x, x)) ` A ⊆ f ` A × A"
by auto
qed
next
fix x y
show "x ∈ A ⟹ y ∈ A ⟹ (R ⊔ S) x y ⟹ lex_prodp Q S (f x, x) (f y, y)"
using convertible_R convertible_S
qed

lemma wf_on_iff_wf: "wf_on A r ⟷ wf {(x, y) ∈ r. x ∈ A ∧ y ∈ A}"
proof (rule iffI)
assume wf: "wf_on A r"
show "wf {(x, y) ∈ r. x ∈ A ∧ y ∈ A}"
unfolding wf_def
proof (intro allI impI ballI)
fix P x
assume IH: "∀x. (∀y. (y, x) ∈ {(x, y). (x, y) ∈ r ∧ x ∈ A ∧ y ∈ A} ⟶ P y) ⟶ P x"
show "P x"
proof (cases "x ∈ A")
case True
from wf show ?thesis
proof (induction x rule: wf_on_induct)
case (less x)
then show ?case
by (auto intro: IH[rule_format])
next
case in_dom
show ?case
using True .
qed
next
case False
then show ?thesis
by (auto intro: IH[rule_format])
qed
qed
next
assume wf: "wf {(x, y). (x, y) ∈ r ∧ x ∈ A ∧ y ∈ A}"
show "wf_on A r"
unfolding wf_on_def
proof (intro allI impI ballI)
fix P x
assume IH: "∀x∈A. (∀y∈A. (y, x) ∈ r ⟶ P y) ⟶ P x" and "x ∈ A"
show "P x"
using wf ‹x ∈ A›
proof (induction x rule: wf_on_induct)
case (less y)
hence "⋀z. (z, y) ∈ r ⟹ z ∈ A ⟹ P z"
by simp
thus ?case
using IH[rule_format, OF ‹y ∈ A›] by simp
next
case in_dom
show ?case
by simp
qed
qed
qed

lemma wfp_on_iff_wfp: "wfp_on A R ⟷ wfp (λx y. R x y ∧  x ∈ A ∧ y ∈ A)"
by (smt (verit, del_insts) UNIV_I subsetI wfp_on_def wfp_on_mono_strong wfp_on_subset)

lemma chain_lnth_rtranclp:
assumes
chain: "Lazy_List_Chain.chain R xs" and
len: "enat j < llength xs"
shows "R⇧*⇧* (lhd xs) (lnth xs j)"
using len
proof (induction j)
case 0
from chain obtain x xs' where "xs = LCons x xs'"
by (auto elim: chain.cases)
thus ?case
by simp
next
case (Suc j)
then show ?case
by (metis Suc_ile_eq chain chain_lnth_rel less_le_not_le rtranclp.simps)
qed

lemma chain_conj_rtranclpI:
fixes xs :: "'a llist"
assumes "Lazy_List_Chain.chain (λx y. R x y) (LCons init xs)"
shows "Lazy_List_Chain.chain (λx y. R x y ∧ R⇧*⇧* init x) (LCons init xs)"
proof (intro lnth_rel_chain allI impI conjI)
show "¬ lnull (LCons init xs)"
by simp
next
fix j
assume hyp: "enat (j + 1) < llength (LCons init xs)"

from hyp show "R (lnth (LCons init xs) j) (lnth (LCons init xs) (j + 1))"
using assms[THEN chain_lnth_rel, of j] by simp

from hyp show "R⇧*⇧* init (lnth (LCons init xs) j)"
using assms[THEN chain_lnth_rtranclp, of j]
qed

lemma rtranclp_implies_ex_lfinite_chain:
assumes run: "R⇧*⇧* x⇩0 x"
shows "∃xs. lfinite xs ∧ chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 xs) ∧ llast (LCons x⇩0 xs) = x"
using run
proof (induction x rule: rtranclp_induct)
case base
then show ?case
by (meson chain.chain_singleton lfinite_code(1) llast_singleton)
next
case (step y z)
from step.IH obtain xs where
"lfinite xs" and "chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 xs)" and "llast (LCons x⇩0 xs) = y"
by auto
let ?xs = "lappend xs (LCons z LNil)"
show ?case
proof (intro exI conjI)
show "lfinite ?xs"
using ‹lfinite xs› by simp
next
show "chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 ?xs)"
using ‹chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 xs)› ‹llast (LCons x⇩0 xs) = y›
chain.chain_singleton chain_lappend step.hyps(1) step.hyps(2)
by fastforce
next
show "llast (LCons x⇩0 ?xs) = z"
by (simp add: ‹lfinite xs› llast_LCons)
qed
qed

lemma chain_conj_rtranclpD:
fixes xs :: "'a llist"
assumes inf: "¬ lfinite xs" and chain: "chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) xs"
shows "∃ys. lfinite ys ∧ chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (lappend ys xs) ∧ lhd (lappend ys xs) = x⇩0"
using chain
proof (cases "λy z. R y z ∧ R⇧*⇧* x⇩0 y" xs rule: chain.cases)
case (chain_singleton x)
with inf have False
by simp
thus ?thesis ..
next
case (chain_cons xs' x)
hence "R⇧*⇧* x⇩0 x"
by auto
thus ?thesis
proof (cases R x⇩0 x rule: rtranclp.cases)
case rtrancl_refl
then show ?thesis
using chain local.chain_cons(1) by force
next
case (rtrancl_into_rtrancl x⇩n)
then obtain ys where
lfin_ys: "lfinite ys" and
chain_ys: "chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 ys)" and
llast_ys: "llast (LCons x⇩0 ys) = x⇩n"
by (auto dest: rtranclp_implies_ex_lfinite_chain)
show ?thesis
proof (intro exI conjI)
show "lfinite (LCons x⇩0 ys)"
using lfin_ys
by simp
next
have "R (llast (LCons x⇩0 ys)) (lhd xs)"
using rtrancl_into_rtrancl(2) chain_cons(1) llast_ys
by simp
moreover have "R⇧*⇧* x⇩0 (llast (LCons x⇩0 ys))"
using rtrancl_into_rtrancl(1,2)
using lappend_code(2)[of x⇩0 ys xs]
lhd_LCons[of x⇩0 "(lappend ys xs)"] local.chain_cons(1)
using llast_ys
by fastforce
ultimately show "chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (lappend (LCons x⇩0 ys) xs)"
using chain_lappend[OF chain_ys chain]
by metis
next
show "lhd (lappend (LCons x⇩0 ys) xs) = x⇩0"
by simp
qed
qed
qed

lemma wfp_on_rtranclp_conversep_iff_no_infinite_down_chain_llist:
fixes R x⇩0
shows "wfp_on {x. R⇧*⇧* x⇩0 x} R¯¯ ⟷ (∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain R (LCons x⇩0 xs))"
proof (rule iffI)
assume "wfp_on {x. R⇧*⇧* x⇩0 x} R¯¯"
hence "wfp (λz y. R¯¯ z y ∧ z ∈ {x. R⇧*⇧* x⇩0 x} ∧ y ∈ {x. R⇧*⇧* x⇩0 x})"
using wfp_on_iff_wfp by blast
hence "wfp (λz y. R y z ∧ R⇧*⇧* x⇩0 y)"
by (auto elim: wfp_on_mono_strong)
hence "Wellfounded.wfP (λz y. R y z ∧ R⇧*⇧* x⇩0 y)"
hence "∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) xs"
unfolding wfP_iff_no_infinite_down_chain_llist
by (metis (no_types, lifting) Lazy_List_Chain.chain_mono conversepI)
hence "∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 xs)"
by (meson lfinite_LCons)
thus "∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain R (LCons x⇩0 xs)"
using chain_conj_rtranclpI
by fastforce
next
assume "∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain R (LCons x⇩0 xs)"
hence no_inf_chain: "∄xs. ¬ lfinite xs ∧ chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 xs)"
by (metis (mono_tags, lifting) Lazy_List_Chain.chain_mono)
have "∄xs. ¬ lfinite xs ∧ chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) xs"
proof (rule notI, elim exE conjE)
fix xs assume "¬ lfinite xs" and "chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) xs"
then obtain ys where
"lfinite ys" and "chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (lappend ys xs)" and "lhd (lappend ys xs) = x⇩0"
by (auto dest: chain_conj_rtranclpD)
hence "∃xs. ¬ lfinite xs ∧ chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 xs)"
proof (intro exI conjI)
show "¬ lfinite (ltl (lappend ys xs))"
using ‹¬ lfinite xs› lfinite_lappend lfinite_ltl
by blast
next
show "chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (LCons x⇩0 (ltl (lappend ys xs)))"
using ‹chain (λy z. R y z ∧ R⇧*⇧* x⇩0 y) (lappend ys xs)› ‹lhd (lappend ys xs) = x⇩0›
chain_not_lnull lhd_LCons_ltl
by fastforce
qed
with no_inf_chain show False
by argo
qed
hence "Wellfounded.wfP (λz y. R y z ∧ y ∈ {x. R⇧*⇧* x⇩0 x})"
unfolding wfP_iff_no_infinite_down_chain_llist
using Lazy_List_Chain.chain_mono by fastforce
hence "wfp (λz y. R y z ∧ y ∈ {x. R⇧*⇧* x⇩0 x})"
unfolding wfp_iff_wfP by argo
hence "wfp (λz y. R¯¯ z y ∧ z ∈ {x. R⇧*⇧* x⇩0 x} ∧ y ∈ {x. R⇧*⇧* x⇩0 x})"
by (auto elim: wfp_on_mono_strong)
thus "wfp_on {x. R⇧*⇧* x⇩0 x} R¯¯"
unfolding wfp_on_iff_wfp[of "{x. R⇧*⇧* x⇩0 x}" "R¯¯"] by argo
qed

end
```