theory Ground_Critical_Pairs imports First_Order_Clause.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}" locale ground_critical_pair_theorem = fixes f_type :: "'f itself" assumes ground_critical_pair_theorem: "⋀R :: 'f gterm rel. WCR (rewrite_inside_gctxt R) ⟷ ground_critical_pairs R ⊆ (rewrite_inside_gctxt R)⇧↓" end