Theory First_Order_Clause.Ground_Critical_Peaks

theory Ground_Critical_Peaks
  imports Ground_Critical_Pairs
begin

context ground_term_rewrite_system
begin

definition ground_critical_peaks ::"'t rel ⇒ ('t × 't × 't) set" where
  "ground_critical_peaks R = { (c⟨r'⟩, c⟨l⟩, r) | l r r' c. (c⟨l⟩, r) ∈ R ∧ (l, r') ∈ R }"

lemma ground_critical_peak_to_pair: 
  assumes "(l, m, r) ∈ ground_critical_peaks R" 
  shows "(l, r) ∈ ground_critical_pairs R" 
  using assms 
  unfolding ground_critical_peaks_def ground_critical_pairs_def 
  by blast

end

locale ground_critical_peaks = ground_term_rewrite_system +
  assumes ground_critical_peaks_main: 
    "⋀R t u s.
      (t, u) ∈ rewrite_in_context R ⟹
      (t, s) ∈ rewrite_in_context R ⟹
      (s, u) ∈ join (rewrite_in_context R) ∨
      (∃c l m r. s = c⟨l⟩ ∧ t = c⟨m⟩ ∧ u = c⟨r⟩ ∧
        ((l, m, r) ∈ ground_critical_peaks R ∨ (r, m, l) ∈ ground_critical_peaks R))"
begin

sublocale ground_critical_pairs
  using ground_critical_peaks_main ground_critical_peak_to_pair
  by unfold_locales meson

end

end