Theory Ground_Critical_Pairs

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 = {(ctxtr2G, r1) | ctxt l r1 r2. (ctxtlG, r1)  R  (l, r2)  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