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))"
  by (simp add: wf_on_def)

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"
  by (simp add: wf_on_def Wellfounded.wf_def)

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"
  by (simp add: wfp_on_def wf_on_def)


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))"
  by (simp add: wfp_on_iff_minimal) 

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"
  by (simp add: wf_eq_minimal) fast

lemmas wfP_subset = wf_subset [to_pred]

text ‹Well-foundedness of the empty relation›

lemma wf_empty [iff]: "wf {}"
  by (simp add: wf_def)

lemma wfP_empty [iff]: "wfp (λx y. False)"
proof -
  have "wfp bot"
    by (simp add: wfp_on_def)
  then show ?thesis
    by (simp add: bot_fun_def)
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
    by (auto simp add: lex_prodp_def)
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]
    by (simp add: Suc_ile_eq)
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)"
    by (simp add: wfp_iff_wfP)
  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