Theory Untyped_Ordered_Resolution_Completeness

theory Untyped_Ordered_Resolution_Completeness
  imports 
    Untyped_Ordered_Resolution_Inference_System
    Ordered_Resolution_Completeness
begin

context untyped_ordered_resolution_calculus
begin

(* TODO: Write own *)
abbreviation Red_F where 
  "Red_F N ≡ snd ` typed.Red_F_𝒢 (empty_typed ` N)" 

abbreviation Red_I where
  "Red_I N ≡ remove_types ` typed.Red_I_𝒢 (empty_typed ` N)"

sublocale untyped_complete_calculus where 
  typed_bottom = "⊥⇩F" and typed_entails = typed.entails_𝒢 and
  typed_inferences = typed.inferences and typed_Red_I = typed.Red_I_𝒢 and
  typed_Red_F = typed.Red_F_𝒢 and bottom = bottom and inferences = inferences and Red_F = Red_F and
  Red_I = Red_I and entails = entails
  by unfold_locales

end

end