Theory Ground_Critical_Pairs

theory Ground_Critical_Pairs
  imports Term_Rewrite_System
begin

definition ground_critical_pairs :: "'f gterm rel ⇒ 'f gterm rel" where
  "ground_critical_pairs R = {(ctxt⟨r⇩2⟩⇩G, r⇩1) | ctxt l r⇩1 r⇩2. (ctxt⟨l⟩⇩G, r⇩1) ∈ R ∧ (l, r⇩2) ∈ R}"

abbreviation ground_critical_pair_theorem :: "'f gterm rel ⇒ bool" where
  "ground_critical_pair_theorem (R :: 'f gterm rel) ≡
    WCR (rewrite_inside_gctxt R) ⟷ ground_critical_pairs R ⊆ (rewrite_inside_gctxt R)⇧↓"

end