Theory First_Order_Clause.Tiebreakers

theory Tiebreakers
  imports Restricted_Order Nonground_Clause_Generic
begin

type_synonym ('g, 'a) tiebreakers = 
  "'g clause ⇒ 'a clause ⇒ 'a clause ⇒ bool"

locale tiebreakers =
  fixes tiebreakers :: "('g, 'a) tiebreakers"
  assumes "⋀C⇩G. wfp (tiebreakers C⇩G) ∧ transp (tiebreakers C⇩G)"
begin

sublocale wellfounded_strict_order "tiebreakers C⇩G"
  using tiebreakers_axioms tiebreakers_def wfp_imp_asymp
  by unfold_locales auto  

end

end