Theory First_Order_Superposition

theory First_Order_Superposition
  imports
    Saturation_Framework.Lifting_to_Non_Ground_Calculi
    Ground_Superposition
    First_Order_Select
    First_Order_Ordering
    First_Order_Type_System
begin

hide_type Inference_System.inference
hide_const
  Inference_System.Infer
  Inference_System.prems_of
  Inference_System.concl_of
  Inference_System.main_prem_of

(* Hide as much of Restricted_Predicates.wfp_on as possible *)
hide_fact
  Restricted_Predicates.wfp_on_imp_minimal
  Restricted_Predicates.wfp_on_imp_inductive_on
  Restricted_Predicates.inductive_on_imp_wfp_on
  Restricted_Predicates.wfp_on_iff_inductive_on
  Restricted_Predicates.wfp_on_iff_minimal
  Restricted_Predicates.wfp_on_imp_has_min_elt
  Restricted_Predicates.wfp_on_induct
  Restricted_Predicates.wfp_on_UNIV
  Restricted_Predicates.wfp_less
  Restricted_Predicates.wfp_on_measure_on
  Restricted_Predicates.wfp_on_mono
  Restricted_Predicates.wfp_on_subset
  Restricted_Predicates.wfp_on_restrict_to
  Restricted_Predicates.wfp_on_imp_irreflp_on
  Restricted_Predicates.accessible_on_imp_wfp_on
  Restricted_Predicates.wfp_on_tranclp_imp_wfp_on
  Restricted_Predicates.wfp_on_imp_accessible_on
  Restricted_Predicates.wfp_on_accessible_on_iff
  Restricted_Predicates.wfp_on_restrict_to_tranclp
  Restricted_Predicates.wfp_on_restrict_to_tranclp'
  Restricted_Predicates.wfp_on_restrict_to_tranclp_wfp_on_conv

section ‹First-Order Layer›

locale first_order_superposition_calculus =
  first_order_select select +
  first_order_ordering less⇩t
  for 
    select :: "('f, ('v :: infinite)) select" and
    less⇩t :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "≺⇩t" 50) +
  fixes
    tiebreakers :: "'f gatom clause  ⇒ ('f, 'v) atom clause ⇒ ('f, 'v) atom clause ⇒ bool" and
    typeof_fun :: "('f, 'ty) fun_types"
  assumes
    wellfounded_tiebreakers: 
      "⋀clause⇩G. wfP (tiebreakers clause⇩G) ∧ 
               transp (tiebreakers clause⇩G) ∧ 
               asymp (tiebreakers clause⇩G)" and
    function_symbols: "⋀τ. ∃f. typeof_fun f = ([], τ)" and
    ground_critical_pair_theorem: "⋀(R :: 'f gterm rel). ground_critical_pair_theorem R" and
    variables: "|UNIV :: 'ty set| ≤o |UNIV :: 'v set|"
begin

abbreviation typed_tiebreakers :: 
      "'f gatom clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool" where 
    "typed_tiebreakers clause⇩G clause⇩1 clause⇩2 ≡ tiebreakers clause⇩G (fst clause⇩1) (fst clause⇩2)"

lemma wellfounded_typed_tiebreakers: 
      "wfP (typed_tiebreakers clause⇩G) ∧ 
       transp (typed_tiebreakers clause⇩G) ∧
      asymp (typed_tiebreakers clause⇩G)"
proof(intro conjI)

  show "wfp (typed_tiebreakers clause⇩G)"
    using wellfounded_tiebreakers
    by (meson wfp_if_convertible_to_wfp)

  show "transp (typed_tiebreakers clause⇩G)"
    using wellfounded_tiebreakers
    by (smt (verit, ccfv_threshold) transpD transpI)

  show "asymp (typed_tiebreakers clause⇩G)"
    using wellfounded_tiebreakers
    by (meson asympD asympI)
qed

definition is_merged_var_type_env where
  "is_merged_var_type_env 𝒱 X 𝒱⇩X ρ⇩X Y 𝒱⇩Y ρ⇩Y ≡
    (∀x ∈ X. welltyped typeof_fun 𝒱 (ρ⇩X x) (𝒱⇩X x)) ∧
    (∀y ∈ Y. welltyped typeof_fun 𝒱 (ρ⇩Y y) (𝒱⇩Y y))"

inductive eq_resolution :: "('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool" where
  eq_resolutionI: 
   "premise = add_mset literal premise' ⟹
    literal = term !≈ term' ⟹
    term_subst.is_imgu μ {{ term, term' }} ⟹
    welltyped_imgu' typeof_fun 𝒱 term term' μ ⟹
    select premise = {#} ∧ is_maximal⇩l (literal ⋅l μ) (premise ⋅ μ) ∨ 
      is_maximal⇩l (literal ⋅l μ) ((select premise) ⋅ μ) ⟹
    conclusion = premise' ⋅ μ ⟹
    eq_resolution (premise, 𝒱) (conclusion, 𝒱)"

inductive eq_factoring :: "('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool" where
  eq_factoringI: "
    premise = add_mset literal⇩1 (add_mset literal⇩2 premise') ⟹
    literal⇩1 = term⇩1 ≈ term⇩1' ⟹
    literal⇩2 = term⇩2 ≈ term⇩2' ⟹
    select premise = {#} ⟹ 
    is_maximal⇩l (literal⇩1 ⋅l μ) (premise ⋅ μ) ⟹
    ¬ (term⇩1 ⋅t μ ≼⇩t term⇩1' ⋅t μ) ⟹
    term_subst.is_imgu μ {{ term⇩1, term⇩2 }} ⟹
    welltyped_imgu' typeof_fun 𝒱 term⇩1 term⇩2 μ ⟹
    conclusion = add_mset (term⇩1 ≈ term⇩2') (add_mset (term⇩1' !≈ term⇩2') premise') ⋅ μ ⟹
    eq_factoring (premise, 𝒱) (conclusion, 𝒱)"

inductive superposition ::
  "('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool"
where
  superpositionI:
   "term_subst.is_renaming ρ⇩1 ⟹
    term_subst.is_renaming ρ⇩2 ⟹
    clause.vars (premise⇩1 ⋅ ρ⇩1) ∩  clause.vars (premise⇩2 ⋅ ρ⇩2) = {} ⟹
    premise⇩1 = add_mset literal⇩1 premise⇩1' ⟹
    premise⇩2 = add_mset literal⇩2 premise⇩2' ⟹
    𝒫 ∈ {Pos, Neg} ⟹
    literal⇩1 = 𝒫 (Upair context⇩1⟨term⇩1⟩ term⇩1') ⟹
    literal⇩2 = term⇩2 ≈ term⇩2' ⟹
    ¬ is_Var term⇩1 ⟹
    term_subst.is_imgu μ {{term⇩1 ⋅t ρ⇩1, term⇩2 ⋅t ρ⇩2}} ⟹
    welltyped_imgu' typeof_fun 𝒱⇩3 (term⇩1 ⋅t ρ⇩1) (term⇩2 ⋅t ρ⇩2) μ ⟹
    ∀x ∈ clause.vars (premise⇩1 ⋅ ρ⇩1). 𝒱⇩1 (the_inv ρ⇩1 (Var x)) = 𝒱⇩3 x ⟹
    ∀x ∈ clause.vars (premise⇩2 ⋅ ρ⇩2). 𝒱⇩2 (the_inv ρ⇩2 (Var x)) = 𝒱⇩3 x ⟹
    welltyped⇩σ_on (clause.vars premise⇩1) typeof_fun 𝒱⇩1 ρ⇩1 ⟹
    welltyped⇩σ_on (clause.vars premise⇩2) typeof_fun 𝒱⇩2 ρ⇩2 ⟹
    (⋀τ τ'. has_type typeof_fun 𝒱⇩2 term⇩2 τ ⟹ has_type typeof_fun 𝒱⇩2 term⇩2' τ' ⟹ τ = τ') ⟹
    ¬ (premise⇩1 ⋅ ρ⇩1 ⋅ μ ≼⇩c premise⇩2 ⋅ ρ⇩2 ⋅ μ) ⟹
    (𝒫 = Pos 
      ∧ select premise⇩1 = {#} 
      ∧ is_strictly_maximal⇩l (literal⇩1 ⋅l ρ⇩1 ⋅l μ) (premise⇩1 ⋅ ρ⇩1 ⋅ μ)) ∨
    (𝒫 = Neg 
      ∧ (select premise⇩1 = {#} ∧ is_maximal⇩l (literal⇩1 ⋅l ρ⇩1 ⋅l μ) (premise⇩1 ⋅ ρ⇩1 ⋅ μ) 
          ∨ is_maximal⇩l (literal⇩1 ⋅l ρ⇩1 ⋅l μ) ((select premise⇩1) ⋅ ρ⇩1 ⋅ μ))) ⟹
    select premise⇩2 = {#} ⟹
    is_strictly_maximal⇩l (literal⇩2 ⋅l ρ⇩2 ⋅l μ) (premise⇩2 ⋅ ρ⇩2 ⋅ μ) ⟹
    ¬ (context⇩1⟨term⇩1⟩ ⋅t ρ⇩1 ⋅t μ ≼⇩t term⇩1' ⋅t ρ⇩1 ⋅t μ) ⟹
    ¬ (term⇩2 ⋅t ρ⇩2 ⋅t μ ≼⇩t term⇩2' ⋅t ρ⇩2 ⋅t μ) ⟹
    conclusion = add_mset (𝒫 (Upair (context⇩1 ⋅t⇩c ρ⇩1)⟨term⇩2' ⋅t ρ⇩2⟩ (term⇩1' ⋅t ρ⇩1))) 
          (premise⇩1' ⋅ ρ⇩1 + premise⇩2' ⋅ ρ⇩2) ⋅ μ ⟹
    all_types 𝒱⇩1 ⟹ all_types 𝒱⇩2 ⟹
    superposition (premise⇩2, 𝒱⇩2) (premise⇩1, 𝒱⇩1) (conclusion, 𝒱⇩3)"

abbreviation eq_factoring_inferences where
  "eq_factoring_inferences ≡ 
    { Infer [premise] conclusion | premise conclusion. eq_factoring premise conclusion }"

abbreviation eq_resolution_inferences where
  "eq_resolution_inferences ≡ 
    { Infer [premise] conclusion | premise conclusion. eq_resolution premise conclusion }"

abbreviation superposition_inferences where
  "superposition_inferences ≡ { Infer [premise⇩2, premise⇩1] conclusion 
    |  premise⇩2 premise⇩1 conclusion. superposition premise⇩2 premise⇩1 conclusion}"

definition inferences :: "('f, 'v, 'ty) typed_clause inference set" where
  "inferences ≡ superposition_inferences ∪ eq_resolution_inferences ∪ eq_factoring_inferences"

abbreviation bottom⇩F :: "('f, 'v, 'ty) typed_clause set" ("⊥⇩F") where
  "bottom⇩F ≡ {({#}, 𝒱) | 𝒱. all_types 𝒱 }"

subsubsection ‹Alternative Specification of the Superposition Rule›

inductive pos_superposition ::
  "('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool"
where
  pos_superpositionI: "
    term_subst.is_renaming ρ⇩1 ⟹
    term_subst.is_renaming ρ⇩2 ⟹
    clause.vars (P⇩1 ⋅ ρ⇩1) ∩ clause.vars (P⇩2 ⋅ ρ⇩2) = {} ⟹
    P⇩1 = add_mset L⇩1 P⇩1' ⟹
    P⇩2 = add_mset L⇩2 P⇩2' ⟹
    L⇩1 = s⇩1⟨u⇩1⟩ ≈ s⇩1' ⟹
    L⇩2 = t⇩2 ≈ t⇩2' ⟹
    ¬ is_Var u⇩1 ⟹
    term_subst.is_imgu μ {{u⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}} ⟹
    welltyped_imgu' typeof_fun 𝒱⇩3 (u⇩1 ⋅t ρ⇩1) (t⇩2 ⋅t ρ⇩2) μ ⟹
    ∀x ∈ clause.vars (P⇩1 ⋅ ρ⇩1). 𝒱⇩1 (the_inv ρ⇩1 (Var x)) = 𝒱⇩3 x ⟹
    ∀x ∈ clause.vars (P⇩2 ⋅ ρ⇩2). 𝒱⇩2 (the_inv ρ⇩2 (Var x)) = 𝒱⇩3 x ⟹
    welltyped⇩σ_on (clause.vars P⇩1) typeof_fun 𝒱⇩1 ρ⇩1 ⟹
    welltyped⇩σ_on (clause.vars P⇩2) typeof_fun 𝒱⇩2 ρ⇩2 ⟹
    (⋀τ τ'. has_type typeof_fun 𝒱⇩2 t⇩2 τ ⟹ has_type typeof_fun 𝒱⇩2 t⇩2' τ' ⟹ τ = τ') ⟹
    ¬ (P⇩1 ⋅ ρ⇩1 ⋅ μ ≼⇩c P⇩2 ⋅ ρ⇩2 ⋅ μ) ⟹
    select P⇩1 = {#} ⟹
    is_strictly_maximal⇩l  (L⇩1 ⋅l ρ⇩1 ⋅l μ) (P⇩1 ⋅ ρ⇩1 ⋅ μ) ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal⇩l  (L⇩2 ⋅l ρ⇩2 ⋅l μ) (P⇩2 ⋅ ρ⇩2 ⋅ μ) ⟹
    ¬ (s⇩1⟨u⇩1⟩ ⋅t ρ⇩1 ⋅t μ ≼⇩t s⇩1' ⋅t ρ⇩1 ⋅t μ) ⟹
    ¬ (t⇩2 ⋅t ρ⇩2 ⋅t μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⋅t μ) ⟹
    C = add_mset ((s⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ ≈ (s⇩1' ⋅t ρ⇩1)) (P⇩1' ⋅ ρ⇩1 + P⇩2' ⋅ ρ⇩2) ⋅ μ ⟹
    all_types 𝒱⇩1 ⟹ all_types 𝒱⇩2 ⟹
    pos_superposition (P⇩2, 𝒱⇩2) (P⇩1, 𝒱⇩1) (C, 𝒱⇩3)"

lemma superposition_if_pos_superposition:
  assumes "pos_superposition P⇩2 P⇩1 C"
  shows "superposition P⇩2 P⇩1 C"
  using assms
proof (cases rule: pos_superposition.cases)
  case (pos_superpositionI ρ⇩1 ρ⇩2 P⇩1 P⇩2 L⇩1 P⇩1' L⇩2 P⇩2' s⇩1 u⇩1 s⇩1' t⇩2 t⇩2' μ 𝒱⇩3 𝒱⇩1 𝒱⇩2 C)
  then show ?thesis
    using superpositionI[of ρ⇩1 ρ⇩2 P⇩1 P⇩2]
    by blast
qed

inductive neg_superposition ::
  "('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ ('f, 'v, 'ty) typed_clause ⇒ bool"
where
  neg_superpositionI: "
    term_subst.is_renaming ρ⇩1 ⟹
    term_subst.is_renaming ρ⇩2 ⟹
    clause.vars (P⇩1 ⋅ ρ⇩1) ∩ clause.vars (P⇩2 ⋅ ρ⇩2) = {} ⟹
    P⇩1 = add_mset L⇩1 P⇩1' ⟹
    P⇩2 = add_mset L⇩2 P⇩2' ⟹
    L⇩1 = s⇩1⟨u⇩1⟩ !≈ s⇩1' ⟹
    L⇩2 = t⇩2 ≈ t⇩2' ⟹
    ¬ is_Var u⇩1 ⟹
    term_subst.is_imgu μ {{u⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}} ⟹
    welltyped_imgu' typeof_fun 𝒱⇩3 (u⇩1 ⋅t ρ⇩1) (t⇩2 ⋅t ρ⇩2) μ ⟹
    ∀x ∈ clause.vars (P⇩1 ⋅ ρ⇩1). 𝒱⇩1 (the_inv ρ⇩1 (Var x)) = 𝒱⇩3 x ⟹
    ∀x ∈ clause.vars (P⇩2 ⋅ ρ⇩2). 𝒱⇩2 (the_inv ρ⇩2 (Var x)) = 𝒱⇩3 x ⟹
    welltyped⇩σ_on (clause.vars P⇩1) typeof_fun 𝒱⇩1 ρ⇩1 ⟹
    welltyped⇩σ_on (clause.vars P⇩2) typeof_fun 𝒱⇩2 ρ⇩2 ⟹
    (⋀τ τ'. has_type typeof_fun 𝒱⇩2 t⇩2 τ ⟹ has_type typeof_fun 𝒱⇩2 t⇩2' τ' ⟹ τ = τ') ⟹
    ¬ (P⇩1 ⋅ ρ⇩1 ⋅ μ ≼⇩c P⇩2 ⋅ ρ⇩2 ⋅ μ) ⟹
    select P⇩1 = {#} ∧ 
      is_maximal⇩l (L⇩1 ⋅l ρ⇩1 ⋅l μ) (P⇩1 ⋅ ρ⇩1 ⋅ μ) ∨ is_maximal⇩l (L⇩1 ⋅l ρ⇩1 ⋅l μ) ((select P⇩1) ⋅ ρ⇩1 ⋅ μ) ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal⇩l  (L⇩2 ⋅l ρ⇩2 ⋅l μ) (P⇩2 ⋅ ρ⇩2 ⋅ μ) ⟹
    ¬ (s⇩1⟨u⇩1⟩ ⋅t ρ⇩1 ⋅t μ ≼⇩t s⇩1' ⋅t ρ⇩1 ⋅t μ) ⟹
    ¬ (t⇩2 ⋅t ρ⇩2 ⋅t μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⋅t μ) ⟹
    C = add_mset (Neg (Upair (s⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩  (s⇩1' ⋅t ρ⇩1))) (P⇩1' ⋅ ρ⇩1 + P⇩2' ⋅ ρ⇩2) ⋅ μ ⟹
    all_types 𝒱⇩1 ⟹ all_types 𝒱⇩2 ⟹
    neg_superposition (P⇩2, 𝒱⇩2) (P⇩1, 𝒱⇩1) (C, 𝒱⇩3)"

lemma superposition_if_neg_superposition:
  assumes "neg_superposition  P⇩2 P⇩1 C"
  shows "superposition P⇩2 P⇩1 C"
  using assms
proof (cases P⇩2 P⇩1 C rule: neg_superposition.cases)
  case (neg_superpositionI ρ⇩1 ρ⇩2 P⇩1 L⇩1 P⇩1' P⇩2 L⇩2 P⇩2' s⇩1 u⇩1 s⇩1' t⇩2 t⇩2' μ 𝒱⇩3 𝒱⇩1 𝒱⇩2 C)
  then show ?thesis
    using superpositionI[of ρ⇩1 ρ⇩2 P⇩1 L⇩1 P⇩1' P⇩2 L⇩2 P⇩2']
    by blast
qed

lemma superposition_iff_pos_or_neg:
  "superposition P⇩2 P⇩1 C ⟷ pos_superposition P⇩2 P⇩1 C ∨ neg_superposition P⇩2  P⇩1 C"
proof (rule iffI)
  assume "superposition P⇩2 P⇩1 C"
  thus "pos_superposition  P⇩2 P⇩1 C ∨ neg_superposition P⇩2 P⇩1 C"
  proof (cases P⇩2 P⇩1 C rule: superposition.cases)
    case (superpositionI ρ⇩1 ρ⇩2 premise⇩1 premise⇩2 literal⇩1 premise⇩1' literal⇩2 premise⇩2' 𝒫 context⇩1 
          term⇩1 term⇩1' term⇩2 term⇩2' μ)
    then show ?thesis
      using
        pos_superpositionI[of ρ⇩1 ρ⇩2 premise⇩1 premise⇩2 literal⇩1 premise⇩1' literal⇩2 premise⇩2' context⇩1 
                              term⇩1 term⇩1' term⇩2 term⇩2' μ]
        neg_superpositionI[of ρ⇩1 ρ⇩2 premise⇩1 premise⇩2 literal⇩1 premise⇩1' literal⇩2 premise⇩2' context⇩1 
                              term⇩1 term⇩1' term⇩2 term⇩2' μ] 
      by blast
  qed
next
  assume "pos_superposition P⇩2 P⇩1 C ∨ neg_superposition P⇩2 P⇩1 C"
  thus "superposition P⇩2 P⇩1 C"
    using superposition_if_neg_superposition superposition_if_pos_superposition by metis
qed

lemma eq_resolution_preserves_typing:
  assumes
    step: "eq_resolution (D, 𝒱) (C, 𝒱)" and
    wt_D: "welltyped⇩c typeof_fun 𝒱 D"
  shows "welltyped⇩c typeof_fun 𝒱 C"
  using step
proof (cases "(D, 𝒱)" "(C, 𝒱)" rule: eq_resolution.cases)
  case (eq_resolutionI literal premise' "term" term' μ)
  obtain τ where τ:
    "welltyped typeof_fun 𝒱 term τ"
    "welltyped typeof_fun 𝒱 term' τ"
    using wt_D
    unfolding 
      eq_resolutionI 
      welltyped⇩c_add_mset 
      welltyped⇩l_def 
      welltyped⇩a_def
    by clause_simp

  then have "welltyped⇩c typeof_fun 𝒱 (D  ⋅ μ)"
    using wt_D welltyped⇩σ_welltyped⇩c eq_resolutionI(4)
    by blast
    
  then show ?thesis
    unfolding eq_resolutionI subst_clause_add_mset welltyped⇩c_add_mset
    by clause_simp
qed

lemma has_type_welltyped:
  assumes "has_type typeof_fun 𝒱 term τ" "welltyped typeof_fun 𝒱 term τ'"
  shows "welltyped typeof_fun 𝒱 term τ"
  using assms
  by (smt (verit, best) welltyped.simps has_type.simps has_type_right_unique right_uniqueD)

lemma welltyped_has_type: 
  assumes "welltyped typeof_fun 𝒱 term τ"
  shows "has_type typeof_fun 𝒱 term τ"
  using assms welltyped.cases has_type.simps by fastforce

lemma eq_factoring_preserves_typing:
  assumes
    step: "eq_factoring (D, 𝒱) (C, 𝒱)" and
    wt_D: "welltyped⇩c typeof_fun 𝒱 D"
  shows "welltyped⇩c typeof_fun 𝒱 C"
  using step
proof (cases "(D, 𝒱)" "(C, 𝒱)" rule: eq_factoring.cases)
  case (eq_factoringI literal⇩1 literal⇩2 premise' term⇩1 term⇩1' term⇩2 term⇩2' μ)
  
  have wt_Dμ: "welltyped⇩c typeof_fun 𝒱 (D ⋅ μ)"
    using wt_D welltyped⇩σ_welltyped⇩c eq_factoringI
    by blast

  show ?thesis
  proof-
    have "⋀τ τ'.
       ⟦∀L∈#premise' ⋅ μ.
           ∃τ. ∀t∈set_uprod (atm_of L). First_Order_Type_System.welltyped typeof_fun 𝒱 t τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩1 ⋅t μ) τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩1' ⋅t μ) τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩2 ⋅t μ) τ';
        First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩2' ⋅t μ) τ'⟧
       ⟹ ∃τ. First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩1 ⋅t μ) τ ∧
               First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩2' ⋅t μ) τ"
       by (metis welltyped_right_unique eq_factoringI(8) right_uniqueD welltyped⇩σ_welltyped)

     moreover have "⋀τ τ'.
       ⟦∀L∈#premise' ⋅ μ.
           ∃τ. ∀t∈set_uprod (atm_of L). First_Order_Type_System.welltyped typeof_fun 𝒱 t τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩1 ⋅t μ) τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩1' ⋅t μ) τ;
        First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩2 ⋅t μ) τ';
        First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩2' ⋅t μ) τ'⟧
       ⟹ ∃τ. First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩1' ⋅t μ) τ ∧
               First_Order_Type_System.welltyped typeof_fun 𝒱 (term⇩2' ⋅t μ) τ"
       by (metis welltyped_right_unique eq_factoringI(8) right_uniqueD welltyped⇩σ_welltyped)

     ultimately show ?thesis
       using wt_Dμ
       unfolding welltyped⇩c_def welltyped⇩l_def welltyped⇩a_def eq_factoringI subst_clause_add_mset 
         subst_literal subst_atom
       by auto
   qed
qed

lemma superposition_preserves_typing:
  assumes
    step: "superposition (D, 𝒱⇩2) (C, 𝒱⇩1) (E, 𝒱⇩3)" and
    wt_C: "welltyped⇩c typeof_fun 𝒱⇩1 C" and
    wt_D: "welltyped⇩c typeof_fun 𝒱⇩2 D"
  shows "welltyped⇩c typeof_fun 𝒱⇩3 E"
  using step
proof (cases "(D, 𝒱⇩2)" "(C, 𝒱⇩1)" "(E, 𝒱⇩3)" rule: superposition.cases)
  case (superpositionI ρ⇩1 ρ⇩2 literal⇩1 premise⇩1' literal⇩2 premise⇩2' 𝒫 context⇩1 term⇩1 term⇩1' term⇩2 
         term⇩2' μ)

  have welltyped_μ: "welltyped⇩σ typeof_fun 𝒱⇩3 μ"
    using superpositionI(11)
    by blast

  have "welltyped⇩c typeof_fun 𝒱⇩3 (C ⋅ ρ⇩1)"
    using wt_C welltyped⇩c_renaming_weaker[OF superpositionI(1, 12)] 
    by blast

  then have wt_Cμ: "welltyped⇩c typeof_fun 𝒱⇩3 (C ⋅ ρ⇩1 ⋅ μ)"
    using welltyped⇩σ_welltyped⇩c[OF welltyped_μ]
    by blast

  have "welltyped⇩c typeof_fun 𝒱⇩3 (D ⋅ ρ⇩2)"
    using wt_D welltyped⇩c_renaming_weaker[OF superpositionI(2, 13)]
    by blast    

  then have wt_Dμ: "welltyped⇩c typeof_fun 𝒱⇩3 (D ⋅ ρ⇩2 ⋅ μ)"
    using welltyped⇩σ_welltyped⇩c[OF welltyped_μ]
    by blast

  note imgu = term_subst.subst_imgu_eq_subst_imgu[OF superpositionI(10)]

  show ?thesis
    using literal_cases[OF superpositionI(6)] wt_Cμ wt_Dμ
    by cases (clause_simp simp: superpositionI imgu)
qed

end

end