Theory Typed_Tiebreakers

theory Typed_Tiebreakers
  imports Tiebreakers
begin

context tiebreakers
begin

abbreviation typed_tiebreakers :: "'g clause ⇒ '𝒱 × 'a clause  ⇒ '𝒱 × 'a clause ⇒ bool" where
  "typed_tiebreakers C⇩G C⇩1 C⇩2 ≡ tiebreakers C⇩G (snd C⇩1) (snd C⇩2)"

sublocale typed_tiebreakers: wellfounded_strict_order "typed_tiebreakers C⇩G"
proof unfold_locales

  show "wfp (typed_tiebreakers C⇩G)"
    by (meson wfp wfp_if_convertible_to_wfp)

qed (auto simp: transp_on_def asympI)
 
end

end