Theory Superposition_Completeness

theory Superposition_Completeness
  imports
    Grounded_Superposition
    Ground_Superposition_Completeness
    Superposition_Welltypedness_Preservation

    First_Order_Clause.Nonground_Entailment
begin

section ‹Completeness›

context grounded_superposition_calculus
begin

subsection ‹Liftings›

lemma eq_resolution_lifting:
  fixes
    D⇩G C⇩G :: "'f ground_atom clause" and
    D C :: "('f, 'v) atom clause" and
    γ :: "('f, 'v) subst"
  defines
    [simp]: "D⇩G ≡ clause.to_ground (D ⋅ γ)" and
    [simp]: "C⇩G ≡ clause.to_ground (C ⋅ γ)"
  assumes
    ground_eq_resolution: "ground.eq_resolution D⇩G C⇩G" and
    D_grounding: "clause.is_ground (D ⋅ γ)" and
    C_grounding: "clause.is_ground (C ⋅ γ)" and
    select: "clause.from_ground (select⇩G D⇩G) = (select D) ⋅ γ" and
    D_is_welltyped: "clause.is_welltyped 𝒱 D" and
    γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱 γ" and
    𝒱: "infinite_variables_per_type 𝒱"
  obtains C'
  where
    "eq_resolution (D, 𝒱) (C', 𝒱)"
    "Infer [D⇩G] C⇩G ∈ inference_ground_instances (Infer [(D, 𝒱)] (C', 𝒱))"
    "C' ⋅ γ = C ⋅ γ"
  using ground_eq_resolution
proof(cases D⇩G C⇩G rule: ground.eq_resolution.cases)
  case ground_eq_resolutionI: (eq_resolutionI l⇩G D⇩G' t⇩G)

  let ?select⇩G_empty = "select⇩G D⇩G = {#}"
  let ?select⇩G_not_empty = "select⇩G D⇩G ≠ {#}"

  obtain l where
    l_γ: "l ⋅l γ = term.from_ground t⇩G !≈ term.from_ground t⇩G" and
    l_in_D: "l ∈# D" and
    l_selected: "?select⇩G_not_empty ⟹ is_maximal l (select D)" and
    l_γ_selected: "?select⇩G_not_empty ⟹ is_maximal (l ⋅l γ) (select D ⋅ γ)" and
    l_is_maximal: "?select⇩G_empty ⟹ is_maximal l D" and
    l_γ_is_maximal: "?select⇩G_empty ⟹ is_maximal (l ⋅l γ) (D ⋅ γ)"
  proof-
    obtain max_l where
      "is_maximal max_l D" and
      is_max_in_D_γ: "is_maximal (max_l ⋅l γ) (D ⋅ γ)"
    proof-
      have "D ≠ {#}"
        using ground_eq_resolutionI(1)
        by auto

      then show ?thesis
        using that D_grounding obtain_maximal_literal
        by blast
    qed

    moreover then have "max_l ∈# D"
      unfolding is_maximal_def
      by blast

    moreover have "max_l ⋅l γ = term.from_ground t⇩G !≈ term.from_ground t⇩G" if ?select⇩G_empty
    proof(rule unique_maximal_in_ground_clause[OF D_grounding is_max_in_D_γ])
      have "ground_is_maximal l⇩G D⇩G"
        using ground_eq_resolutionI(3) that
        unfolding is_maximal_def
        by simp

      then show "is_maximal (term.from_ground t⇩G !≈ term.from_ground t⇩G) (D ⋅ γ)"
        using D_grounding
        unfolding ground_eq_resolutionI(2)
        by simp
    qed

    moreover obtain selected_l where
      "selected_l ⋅l γ = term.from_ground t⇩G !≈ term.from_ground t⇩G" and
      "is_maximal selected_l (select D)"
      "is_maximal (selected_l ⋅l γ) (select D ⋅ γ)"
    if ?select⇩G_not_empty
    proof-
      have "is_maximal (term.from_ground t⇩G !≈ term.from_ground t⇩G) (select D ⋅ γ)"
        if ?select⇩G_not_empty
        using ground_eq_resolutionI(3) that select
        unfolding ground_eq_resolutionI(2)
        by simp

      then show ?thesis
        using
          that
          obtain_maximal_literal[OF _ select_ground_subst[OF D_grounding]]
          unique_maximal_in_ground_clause[OF select_ground_subst[OF D_grounding]]
        by (metis is_maximal_not_empty clause.magma_subst_empty)
    qed

    moreover then have "selected_l ∈# D" if ?select⇩G_not_empty
      by (meson that maximal_in_clause mset_subset_eqD select_subset)

    ultimately show ?thesis
      using that
      by blast
  qed

  obtain C' where D: "D = add_mset l C'"
    using multi_member_split[OF l_in_D]
    by blast

  obtain t t' where l: "l = t !≈ t'"
    using l_γ obtain_from_neg_literal_subst
    by meson

  obtain μ σ where γ: "γ = μ ⊙ σ" and imgu: "welltyped_imgu_on (clause.vars D) 𝒱 t t' μ"
  proof-
    have unified: "t ⋅t γ = t' ⋅t γ"
      using l_γ
      unfolding l
      by simp

    moreover obtain τ where welltyped: "welltyped 𝒱 t τ" "welltyped 𝒱 t' τ"
      using D_is_welltyped
      unfolding D l
      by auto

    show ?thesis
      using obtain_welltyped_imgu_on[OF unified welltyped] that
      by metis
  qed

  show ?thesis
  proof(rule that)

    show eq_resolution: "eq_resolution (D, 𝒱) (C' ⋅ μ, 𝒱)"
    proof (rule eq_resolutionI, rule imgu)

      show "select D = {#} ⟹ is_maximal (l ⋅l μ) (D ⋅ μ)"
      proof -
        assume "select D = {#}"

        then have "?select⇩G_empty"
          using select 
          by auto

        moreover have "l ⋅l μ ∈# D ⋅ μ"
          using l_in_D
          by blast

        ultimately show "is_maximal (l ⋅l μ) (D ⋅ μ)"
          using l_γ_is_maximal is_maximal_if_grounding_is_maximal D_grounding
          unfolding γ
          by simp
      qed

      show "select D ≠ {#} ⟹ is_maximal (l ⋅l μ) (select D ⋅ μ)"
      proof -
        assume "select D ≠ {#}"

        then have "¬?select⇩G_empty"
          using select 
          by auto

        moreover then have "l ⋅l μ ∈# select D ⋅ μ"
          using l_selected maximal_in_clause
          by blast

        ultimately show ?thesis
          using
            select_ground_subst[OF D_grounding]
            l_γ_selected
            is_maximal_if_grounding_is_maximal
          unfolding γ
          by auto
      qed
    qed (rule D, rule l, rule refl)

    show C'_μ_γ: "C' ⋅ μ ⋅ γ = C ⋅ γ"
    proof-
      have "term.is_idem μ"
        using imgu
        unfolding term_subst.is_imgu_iff_is_idem_and_is_mgu
        by blast

      then have μ_γ: "μ ⊙ γ = γ"
        unfolding γ term_subst.is_idem_def subst_compose_assoc[symmetric]
        by argo

      have "D ⋅ γ = add_mset (l ⋅l γ) (C ⋅ γ)"
      proof-
        have "clause.to_ground (D ⋅ γ) = clause.to_ground (add_mset (l ⋅l γ) (C ⋅ γ))"
          using ground_eq_resolutionI(1)
          unfolding ground_eq_resolutionI(2) l_γ ground_eq_resolutionI(4)[symmetric]
          by simp

        moreover have "clause.is_ground (add_mset (l ⋅l γ) (C ⋅ γ))"
          using C_grounding clause.to_set_is_ground_subst[OF l_in_D D_grounding]
          by simp

        ultimately show ?thesis
          using clause.to_ground_eq[OF D_grounding]
          by blast
      qed

      then have "C' ⋅ γ = C ⋅ γ"
        unfolding D
        by simp

      then show ?thesis
        unfolding clause.subst_comp_subst[symmetric] μ_γ.
    qed

    show "Infer [D⇩G] C⇩G ∈ inference_ground_instances (Infer [(D, 𝒱)] (C' ⋅ μ, 𝒱))"
    proof (rule is_inference_ground_instance_one_premise)

      show "is_inference_ground_instance_one_premise (D, 𝒱) (C' ⋅ μ, 𝒱) (Infer [D⇩G] C⇩G) γ"
      proof(unfold split, intro conjI; (rule D_is_welltyped refl 𝒱)?)
        show "inference.is_ground (Infer [D] (C' ⋅ μ) ⋅ι γ)"
          using D_grounding C_grounding C'_μ_γ
          by auto
      next
        show "Infer [D⇩G] C⇩G = inference.to_ground (Infer [D] (C' ⋅ μ) ⋅ι γ)"
          using C'_μ_γ
          by simp
      next
        have "clause.vars (C' ⋅ μ) ⊆ clause.vars D"
          using clause.variables_in_base_imgu imgu
          unfolding D l
          by auto

        then show "term.subst.is_welltyped_on (clause.vars (C' ⋅ μ)) 𝒱 γ"
          using D_is_welltyped γ_is_welltyped
          by blast
      next
        show "clause.is_welltyped 𝒱 (C' ⋅ μ)"
          using D_is_welltyped eq_resolution eq_resolution_preserves_typing
          by blast
      qed

      show "Infer [D⇩G] C⇩G ∈ ground.G_Inf"
        unfolding ground.G_Inf_def
        using ground_eq_resolution
        by blast
    qed
  qed
qed

lemma eq_factoring_lifting:
  fixes
    D⇩G C⇩G :: "'f ground_atom clause" and
    D C :: "('f, 'v) atom clause" and
    γ :: "('f, 'v) subst"
  defines
    [simp]: "D⇩G ≡ clause.to_ground (D ⋅ γ)" and
    [simp]: "C⇩G ≡ clause.to_ground (C ⋅ γ)"
  assumes
    ground_eq_factoring: "ground.eq_factoring D⇩G C⇩G" and
    D_grounding: "clause.is_ground (D ⋅ γ)" and
    C_grounding: "clause.is_ground (C ⋅ γ)" and
    select: "clause.from_ground (select⇩G D⇩G) = (select D) ⋅ γ" and
    D_is_welltyped: "clause.is_welltyped 𝒱 D" and
    γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱 γ" and
    𝒱: "infinite_variables_per_type 𝒱"
  obtains C'
  where
    "eq_factoring (D, 𝒱) (C', 𝒱)"
    "Infer [D⇩G] C⇩G ∈ inference_ground_instances (Infer [(D, 𝒱)] (C', 𝒱))"
    "C' ⋅ γ = C ⋅ γ"
  using ground_eq_factoring
proof(cases D⇩G C⇩G rule: ground.eq_factoring.cases)
  case ground_eq_factoringI: (eq_factoringI l⇩G⇩1 l⇩G⇩2 D⇩G' t⇩G⇩1 t⇩G⇩2 t⇩G⇩3)

  have "D ≠ {#}"
    using ground_eq_factoringI(1)
    by auto

  then obtain l⇩1 where
    l⇩1_is_maximal: "is_maximal l⇩1 D" and
    l⇩1_γ_is_maximal: "is_maximal (l⇩1 ⋅l γ) (D ⋅ γ)"
    using that obtain_maximal_literal D_grounding
    by blast

  obtain t⇩1 t⇩1' where
    l⇩1: "l⇩1 = t⇩1 ≈ t⇩1'" and
    l⇩1_γ: "l⇩1 ⋅l γ = term.from_ground t⇩G⇩1 ≈ term.from_ground t⇩G⇩2" and
    t⇩1_γ: "t⇩1 ⋅t γ = term.from_ground t⇩G⇩1" and
    t⇩1'_γ: "t⇩1' ⋅t γ = term.from_ground t⇩G⇩2"
  proof-
    have "is_maximal (literal.from_ground l⇩G⇩1) (D ⋅ γ)"
      using ground_eq_factoringI(5) D_grounding
      by simp

    then have "l⇩1 ⋅l γ = term.from_ground t⇩G⇩1 ≈ term.from_ground t⇩G⇩2"
      unfolding  ground_eq_factoringI(2)
      using unique_maximal_in_ground_clause[OF D_grounding l⇩1_γ_is_maximal]
      by simp

    then show ?thesis
      using that
      unfolding ground_eq_factoringI(2)
      by (metis obtain_from_pos_literal_subst)
  qed

  obtain l⇩2 D' where
    l⇩2_γ: "l⇩2 ⋅l γ = term.from_ground t⇩G⇩1 ≈ term.from_ground t⇩G⇩3" and
    D: "D = add_mset l⇩1 (add_mset l⇩2 D')"
  proof-
    obtain D'' where D: "D = add_mset l⇩1 D''"
      using maximal_in_clause[OF l⇩1_is_maximal]
      by (meson multi_member_split)

    moreover have "D ⋅ γ = clause.from_ground (add_mset l⇩G⇩1 (add_mset l⇩G⇩2 D⇩G'))"
      using ground_eq_factoringI(1) D⇩G_def
      by (metis D_grounding clause.to_ground_inverse)

    ultimately have "D'' ⋅ γ =  add_mset (literal.from_ground l⇩G⇩2) (clause.from_ground D⇩G')"
      using  l⇩1_γ
      by (simp add: ground_eq_factoringI(2))

    then obtain l⇩2 where "l⇩2 ⋅l γ = term.from_ground t⇩G⇩1 ≈ term.from_ground t⇩G⇩3" "l⇩2 ∈# D''"
      unfolding clause.subst_def ground_eq_factoringI
      using msed_map_invR
      by force

    then show ?thesis
      using that
      unfolding D
      by (metis mset_add)
  qed

  then obtain t⇩2 t⇩2' where
    l⇩2: "l⇩2 = t⇩2 ≈ t⇩2'" and
    t⇩2_γ: "t⇩2 ⋅t γ = term.from_ground t⇩G⇩1" and
    t⇩2'_γ: "t⇩2' ⋅t γ = term.from_ground t⇩G⇩3"
    unfolding ground_eq_factoringI(3)
    using obtain_from_pos_literal_subst
    by metis

  have D'_γ: "D' ⋅ γ = clause.from_ground D⇩G'"
    using D D_grounding ground_eq_factoringI(1,2,3) l⇩1_γ l⇩2_γ
    by force

  obtain μ σ where γ: "γ = μ ⊙ σ" and imgu: "welltyped_imgu_on (clause.vars D) 𝒱 t⇩1 t⇩2 μ"
  proof-
    have unified: "t⇩1 ⋅t γ = t⇩2 ⋅t γ"
      unfolding t⇩1_γ t⇩2_γ ..

    then obtain τ where "welltyped 𝒱 (t⇩1 ⋅t γ) τ" "welltyped 𝒱 (t⇩2 ⋅t γ) τ"
      using D_is_welltyped γ_is_welltyped
      unfolding D l⇩1 l⇩2
      by auto

    then have welltyped: "welltyped 𝒱 t⇩1 τ" "welltyped 𝒱 t⇩2 τ"
      using γ_is_welltyped
      unfolding D l⇩1 l⇩2
      by simp_all

    then show ?thesis
      using obtain_welltyped_imgu_on[OF unified welltyped] that
      by metis
  qed

  let ?C'' = "add_mset (t⇩1 ≈ t⇩2') (add_mset (t⇩1' !≈ t⇩2') D')"
  let ?C' = "?C'' ⋅ μ"

  show ?thesis
  proof(rule that)

    show eq_factoring: "eq_factoring (D, 𝒱) (?C', 𝒱)"
    proof (rule eq_factoringI; (rule D l⇩1 l⇩2 imgu refl 𝒱)?)
      show "select D = {#}"
        using ground_eq_factoringI(4) select
        by simp
    next
      have "l⇩1 ⋅l μ ∈# D ⋅ μ"
        using l⇩1_is_maximal clause.subst_in_to_set_subst maximal_in_clause
        by blast

      then show "is_maximal (l⇩1 ⋅l μ) (D ⋅ μ)"
        using is_maximal_if_grounding_is_maximal D_grounding l⇩1_γ_is_maximal
        unfolding γ
        by auto
    next
      have groundings: "term.is_ground (t⇩1' ⋅t μ ⋅t σ)" "term.is_ground (t⇩1 ⋅t μ ⋅t σ)"
        using t⇩1'_γ t⇩1_γ
        unfolding γ
        by simp_all

      have "t⇩1' ⋅t γ ≺⇩t t⇩1 ⋅t γ"
        using ground_eq_factoringI(6)
        unfolding t⇩1'_γ t⇩1_γ term.order.less⇩G_def.

      then show "¬ t⇩1 ⋅t μ ≼⇩t t⇩1' ⋅t μ"
        unfolding γ
        using term.order.ground_less_not_less_eq[OF groundings]
        by simp
    qed

    show C'_γ: "?C' ⋅ γ = C ⋅ γ"
    proof-
      have "term.is_idem μ"
        using imgu
        unfolding term_subst.is_imgu_iff_is_idem_and_is_mgu
        by blast

      then have μ_γ: "μ ⊙ γ = γ"
        unfolding γ term_subst.is_idem_def subst_compose_assoc[symmetric]
        by argo

      have "C ⋅ γ = clause.from_ground (add_mset (t⇩G⇩2 !≈ t⇩G⇩3) (add_mset (t⇩G⇩1 ≈ t⇩G⇩3) D⇩G'))"
        using ground_eq_factoringI(7) clause.to_ground_eq[OF C_grounding clause.ground_is_ground]
        unfolding C⇩G_def
        by (metis clause.from_ground_inverse)

      also have "... = ?C'' ⋅ γ"
        using t⇩1_γ t⇩1'_γ t⇩2'_γ D'_γ
        by simp

      also have "... = ?C' ⋅ γ"
        unfolding clause.subst_comp_subst[symmetric] μ_γ ..

      finally show ?thesis ..
    qed

    show "Infer [D⇩G] C⇩G ∈ inference_ground_instances (Infer [(D, 𝒱)] (?C', 𝒱))"
    proof (rule is_inference_ground_instance_one_premise)

      show "is_inference_ground_instance_one_premise (D, 𝒱) (?C', 𝒱) (Infer [D⇩G] C⇩G) γ"
      proof(unfold split, intro conjI; (rule D_is_welltyped refl 𝒱)?)

        show "inference.is_ground (Infer [D] ?C' ⋅ι γ)"
          using C_grounding D_grounding C'_γ
          by auto
      next

        show "Infer [D⇩G] C⇩G = inference.to_ground (Infer [D] ?C' ⋅ι γ)"
          using C'_γ
          by simp
      next

        have imgu: "term.is_imgu μ {{t⇩1, t⇩2}}"
          using imgu
          by blast

        have "clause.vars ?C' ⊆ clause.vars D"
          using clause.variables_in_base_imgu[OF imgu, of ?C'']
          unfolding D l⇩1 l⇩2
          by auto

        then show "term.subst.is_welltyped_on (clause.vars ?C') 𝒱 γ"
          using D_is_welltyped γ_is_welltyped
          by blast
      next

        show "clause.is_welltyped 𝒱 ?C'"
          using D_is_welltyped eq_factoring eq_factoring_preserves_typing
          by blast
      qed

      show "Infer [D⇩G] C⇩G ∈ ground.G_Inf"
        unfolding ground.G_Inf_def
        using ground_eq_factoring
        by blast
    qed
  qed
qed

lemma superposition_lifting:
  fixes
    E⇩G D⇩G C⇩G :: "'f ground_atom clause" and
    E D C :: "('f, 'v) atom clause" and
    γ ρ⇩1 ρ⇩2 :: "('f, 'v) subst" and
    𝒱⇩1 𝒱⇩2 :: "('v, 'ty) var_types"
  defines
    [simp]: "E⇩G ≡ clause.to_ground (E ⋅ ρ⇩1 ⊙ γ)" and
    [simp]: "D⇩G ≡ clause.to_ground (D ⋅ ρ⇩2 ⊙ γ)" and
    [simp]: "C⇩G ≡ clause.to_ground (C ⋅ γ)" and
    [simp]: "N⇩G ≡ clause.welltyped_ground_instances (E, 𝒱⇩1) ∪
                    clause.welltyped_ground_instances (D, 𝒱⇩2)" and
    [simp]: "ι⇩G ≡ Infer [D⇩G, E⇩G] C⇩G"
  assumes
    ground_superposition: "ground.superposition D⇩G E⇩G C⇩G" and
    ρ⇩1: "term_subst.is_renaming ρ⇩1" and
    ρ⇩2: "term_subst.is_renaming ρ⇩2" and
    rename_apart: "clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {}" and
    E_grounding: "clause.is_ground (E ⋅ ρ⇩1 ⊙ γ)" and
    D_grounding: "clause.is_ground (D ⋅ ρ⇩2 ⊙ γ)" and
    C_grounding: "clause.is_ground (C ⋅ γ)" and
    select_from_E: "clause.from_ground (select⇩G E⇩G) = (select E) ⋅ ρ⇩1 ⊙ γ" and
    select_from_D: "clause.from_ground (select⇩G D⇩G) = (select D) ⋅ ρ⇩2 ⊙ γ" and
    E_is_welltyped: "clause.is_welltyped 𝒱⇩1 E" and
    D_is_welltyped: "clause.is_welltyped 𝒱⇩2 D" and
    ρ⇩1_γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 (ρ⇩1 ⊙ γ)" and
    ρ⇩2_γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 (ρ⇩2 ⊙ γ)" and
    ρ⇩1_is_welltyped: "term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 ρ⇩1" and
    ρ⇩2_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 ρ⇩2" and
    𝒱⇩1: "infinite_variables_per_type 𝒱⇩1" and
    𝒱⇩2: "infinite_variables_per_type 𝒱⇩2" and
    not_redundant: "ι⇩G ∉ ground.Red_I N⇩G"
  obtains C' 𝒱⇩3
  where
    "superposition (D, 𝒱⇩2) (E, 𝒱⇩1) (C', 𝒱⇩3)"
    "ι⇩G ∈ inference_ground_instances (Infer [(D, 𝒱⇩2), (E, 𝒱⇩1)] (C', 𝒱⇩3))"
    "C' ⋅ γ = C ⋅ γ"
  using ground_superposition
proof(cases D⇩G E⇩G C⇩G rule: ground.superposition.cases)
  case ground_superpositionI: (superpositionI l⇩G⇩1 E⇩G' l⇩G⇩2 D⇩G' 𝒫⇩G c⇩G t⇩G⇩1 t⇩G⇩2 t⇩G⇩3)

  have E_γ: "E ⋅ ρ⇩1 ⊙ γ = clause.from_ground (add_mset l⇩G⇩1 E⇩G')"
    using ground_superpositionI(1)
    unfolding E⇩G_def
    by (metis E_grounding clause.to_ground_inverse)

  have D_γ: "D ⋅ ρ⇩2 ⊙ γ = clause.from_ground (add_mset l⇩G⇩2 D⇩G')"
    using ground_superpositionI(2) D⇩G_def
    by (metis D_grounding clause.to_ground_inverse)

  let ?select⇩G_empty = "select⇩G (clause.to_ground (E ⋅ ρ⇩1 ⊙ γ)) = {#}"
  let ?select⇩G_not_empty = "select⇩G (clause.to_ground (E ⋅ ρ⇩1 ⊙ γ)) ≠ {#}"

  obtain l⇩1 where
    l⇩1_γ: "l⇩1 ⋅l ρ⇩1 ⊙ γ = literal.from_ground l⇩G⇩1" and
    l⇩1_is_strictly_maximal: "𝒫⇩G = Pos ⟹ is_strictly_maximal l⇩1 E" and
    l⇩1_is_maximal: "𝒫⇩G = Neg ⟹ ?select⇩G_empty ⟹ is_maximal l⇩1 E" and
    l⇩1_selected: "𝒫⇩G = Neg ⟹ ?select⇩G_not_empty ⟹ is_maximal l⇩1 (select E)" and
    l⇩1_in_E: "l⇩1 ∈# E"
  proof-

    have E_not_empty: "E ≠ {#}"
      using ground_superpositionI(1)
      by auto

    have "is_strictly_maximal (literal.from_ground l⇩G⇩1) (E ⋅ ρ⇩1 ⊙ γ)" if "𝒫⇩G = Pos"
      using ground_superpositionI(9) that E_grounding
      by simp

    then obtain positive_l⇩1 where
      "is_strictly_maximal positive_l⇩1 E"
      "positive_l⇩1 ⋅l ρ⇩1 ⊙ γ = literal.from_ground l⇩G⇩1"
    if "𝒫⇩G = Pos"
      using obtain_strictly_maximal_literal[OF E_grounding]
      by metis

    moreover then have "positive_l⇩1 ∈# E" if "𝒫⇩G = Pos"
      using that strictly_maximal_in_clause
      by blast

    moreover then have "is_maximal (literal.from_ground l⇩G⇩1) (E ⋅ ρ⇩1 ⊙ γ)" if ?select⇩G_empty
      using that ground_superpositionI(9) is_maximal_not_empty E_grounding
      by auto

    then obtain negative_maximal_l⇩1 where
      "is_maximal negative_maximal_l⇩1 E"
      "negative_maximal_l⇩1 ⋅l ρ⇩1 ⊙ γ = literal.from_ground l⇩G⇩1"
    if "𝒫⇩G = Neg" ?select⇩G_empty
      using
        obtain_maximal_literal[OF E_not_empty E_grounding[folded clause.subst_comp_subst]]
        unique_maximal_in_ground_clause[OF E_grounding[folded clause.subst_comp_subst]]
      by metis

    moreover then have "negative_maximal_l⇩1 ∈# E" if "𝒫⇩G = Neg" ?select⇩G_empty
      using that maximal_in_clause
      by blast

    moreover have "ground_is_maximal l⇩G⇩1 (select⇩G E⇩G)" if "𝒫⇩G = Neg" ?select⇩G_not_empty
      using ground_superpositionI(9) that
      by simp

    then obtain negative_selected_l⇩1 where
      "is_maximal negative_selected_l⇩1 (select E)"
      "negative_selected_l⇩1 ⋅l ρ⇩1 ⊙ γ = literal.from_ground l⇩G⇩1"
    if "𝒫⇩G = Neg" ?select⇩G_not_empty
      using
        select_from_E
        unique_maximal_in_ground_clause
        obtain_maximal_literal
      unfolding E⇩G_def
      by (metis (no_types, lifting) clause.ground_is_ground clause.from_ground_empty'
          clause.magma_subst_empty)

    moreover then have "negative_selected_l⇩1 ∈# E" if "𝒫⇩G = Neg" ?select⇩G_not_empty
      using that
      by (meson maximal_in_clause mset_subset_eqD select_subset)

    ultimately show ?thesis
      using that ground_superpositionI(9)
      by (metis literals_distinct(1))
  qed

  obtain E' where E: "E = add_mset l⇩1 E'"
    by (meson l⇩1_in_E multi_member_split)

  then have E'_γ: "E' ⋅ ρ⇩1 ⊙ γ = clause.from_ground E⇩G'"
    using l⇩1_γ E_γ
    by auto

  let ?𝒫 = "if 𝒫⇩G = Pos then Pos else Neg"

  have [simp]: "𝒫⇩G ≠ Pos ⟷ 𝒫⇩G = Neg" "𝒫⇩G ≠ Neg ⟷ 𝒫⇩G = Pos"
    using ground_superpositionI(4)
    by auto

  have [simp]: "⋀a σ. ?𝒫 a ⋅l σ = ?𝒫 (a ⋅a σ)"
    by auto

  have [simp]: "⋀𝒱 a. literal.is_welltyped 𝒱 (?𝒫 a) ⟷ atom.is_welltyped 𝒱 a"
    by (auto simp: literal_is_welltyped_iff_atm_of)

  have [simp]: "⋀a. literal.vars (?𝒫 a) = atom.vars a"
    by auto

  have l⇩1_γ:
    "l⇩1 ⋅l ρ⇩1 ⊙ γ = ?𝒫 (Upair (context.from_ground c⇩G)⟨term.from_ground t⇩G⇩1⟩ (term.from_ground t⇩G⇩2))"
    unfolding ground_superpositionI l⇩1_γ
    by simp

  obtain c⇩1 t⇩1 t⇩1' where
    l⇩1: "l⇩1 = ?𝒫 (Upair c⇩1⟨t⇩1⟩ t⇩1')" and
    t⇩1'_γ: "t⇩1' ⋅t ρ⇩1 ⊙ γ = term.from_ground t⇩G⇩2" and
    t⇩1_γ: "t⇩1 ⋅t ρ⇩1 ⊙ γ = term.from_ground t⇩G⇩1" and
    c⇩1_γ: "c⇩1 ⋅t⇩c ρ⇩1 ⊙ γ = context.from_ground c⇩G" and
    t⇩1_is_Fun: "is_Fun t⇩1"
  proof-

    obtain c⇩1_t⇩1 t⇩1' where
      l⇩1: "l⇩1 = ?𝒫 (Upair c⇩1_t⇩1 t⇩1')" and
      t⇩1'_γ: "t⇩1' ⋅t ρ⇩1 ⊙ γ = term.from_ground t⇩G⇩2" and
      c⇩1_t⇩1_γ: "c⇩1_t⇩1 ⋅t ρ⇩1 ⊙ γ = (context.from_ground c⇩G)⟨term.from_ground t⇩G⇩1⟩"
      using l⇩1_γ
      by (smt (verit) obtain_from_literal_subst)

    let ?inference_into_Fun =
      "∃c⇩1 t⇩1.
        c⇩1_t⇩1 = c⇩1⟨t⇩1⟩ ∧
        t⇩1 ⋅t ρ⇩1 ⊙ γ = term.from_ground t⇩G⇩1 ∧
        c⇩1 ⋅t⇩c ρ⇩1 ⊙ γ = context.from_ground c⇩G ∧
        is_Fun t⇩1"

    have "¬ ?inference_into_Fun ⟹ ground.redundant_infer N⇩G ι⇩G"
    proof-
      assume "¬ ?inference_into_Fun"

      with c⇩1_t⇩1_γ
      obtain t⇩1 c⇩1 c⇩G' where
        c⇩1_t⇩1: "c⇩1_t⇩1 = c⇩1⟨t⇩1⟩" and
        t⇩1_is_Var: "is_Var t⇩1" and
        c⇩G: "c⇩G = context.to_ground (c⇩1 ⋅t⇩c ρ⇩1 ⊙ γ) ∘⇩c c⇩G'"
      proof(induction c⇩1_t⇩1 arbitrary: c⇩G thesis)
        case (Var x)

        show ?case
        proof(rule Var.prems)
          show "Var x = □⟨Var x⟩"
            by simp

          show "is_Var (Var x)"
            by simp

          show "c⇩G = context.to_ground (□ ⋅t⇩c ρ⇩1 ⊙ γ) ∘⇩c c⇩G"
            by (simp add: context.to_ground_def)
        qed
      next
        case (Fun f ts)

        have "c⇩G ≠ □"
          using Fun.prems(2,3)
          unfolding context.from_ground_def
          by (metis actxt.simps(8) intp_actxt.simps(1) is_FunI)

        then obtain ts⇩G⇩1 c⇩G' ts⇩G⇩2 where
          c⇩G: "c⇩G = More f ts⇩G⇩1 c⇩G' ts⇩G⇩2"
          using Fun.prems
          by (cases c⇩G) (auto simp: context.from_ground_def)

        have
          "map (λt. t ⋅t ρ⇩1 ⊙ γ) ts =
            map term.from_ground ts⇩G⇩1 @ (context.from_ground c⇩G')⟨term.from_ground t⇩G⇩1⟩ #
            map term.from_ground ts⇩G⇩2"
          using Fun(3)
          unfolding c⇩G context.from_ground_def
          by simp

        moreover then obtain ts⇩1 t ts⇩2 where
          ts: "ts = ts⇩1 @ t # ts⇩2" and
          ts⇩1_γ: "map (λterm. term ⋅t ρ⇩1 ⊙ γ) ts⇩1 = map term.from_ground ts⇩G⇩1" and
          ts⇩2_γ: "map (λterm. term ⋅t ρ⇩1 ⊙ γ) ts⇩2 = map term.from_ground ts⇩G⇩2"
          by (smt append_eq_map_conv map_eq_Cons_D)

        ultimately have t_γ: "t ⋅t ρ⇩1 ⊙ γ = (context.from_ground c⇩G')⟨term.from_ground t⇩G⇩1⟩"
          by simp

        obtain t⇩1 c⇩1 c⇩G'' where
          "t = c⇩1⟨t⇩1⟩" and
          "is_Var t⇩1" and
          "c⇩G' = context.to_ground (c⇩1 ⋅t⇩c ρ⇩1 ⊙ γ) ∘⇩c c⇩G''"
        proof-
          have "t ∈ set ts"
            by (simp add: ts)

          moreover have
            "∄c⇩1 t⇩1. t = c⇩1⟨t⇩1⟩ ∧
                t⇩1 ⋅t ρ⇩1 ⊙ γ = term.from_ground t⇩G⇩1 ∧
                c⇩1 ⋅t⇩c ρ⇩1 ⊙ γ = context.from_ground c⇩G' ∧
                is_Fun t⇩1"
          proof(rule notI, elim exE conjE)
            fix c⇩1 t⇩1
            assume
              "t = c⇩1⟨t⇩1⟩"
              "t⇩1 ⋅t ρ⇩1 ⊙ γ = term.from_ground t⇩G⇩1"
              "c⇩1 ⋅t⇩c ρ⇩1 ⊙ γ = context.from_ground c⇩G'"
              "is_Fun t⇩1"

            moreover then have
              "Fun f ts = (More f ts⇩1 c⇩1 ts⇩2)⟨t⇩1⟩"
              "(More f ts⇩1 c⇩1 ts⇩2) ⋅t⇩c ρ⇩1 ⊙ γ = context.from_ground c⇩G"
              unfolding context.from_ground_def c⇩G ts
              using ts⇩1_γ ts⇩2_γ
              by auto

            ultimately show False
              using Fun.prems(3)
              by blast
          qed

          ultimately show ?thesis
            using Fun(1) t_γ that
            by blast
        qed

        moreover then have
          "Fun f ts = (More f ts⇩1 c⇩1 ts⇩2)⟨t⇩1⟩"
          "c⇩G = context.to_ground (More f ts⇩1 c⇩1 ts⇩2 ⋅t⇩c ρ⇩1 ⊙ γ) ∘⇩c c⇩G''"
          using ts⇩1_γ ts⇩2_γ
          unfolding context.to_ground_def c⇩G ts
          by auto

        ultimately show ?case
          using Fun.prems(1)
          by blast
      qed

      obtain x where t⇩1_ρ⇩1: "t⇩1 ⋅t ρ⇩1 = Var x"
        using t⇩1_is_Var term.id_subst_rename[OF ρ⇩1]
        unfolding is_Var_def
        by auto

      have ι⇩G_parts:
        "set (side_prems_of ι⇩G) = {D⇩G}"
        "main_prem_of ι⇩G = E⇩G"
        "concl_of ι⇩G = C⇩G"
        by simp_all

      show ?thesis
      proof(rule ground.redundant_infer_singleton, unfold ι⇩G_parts, intro bexI conjI)

        let ?t⇩G = "(context.from_ground c⇩G')⟨term.from_ground t⇩G⇩3⟩"

        define γ' where
          "γ' ≡ γ(x := ?t⇩G)"

        let ?E⇩G' = "clause.to_ground (E ⋅ ρ⇩1 ⊙ γ')"

        have t⇩1_γ: "t⇩1 ⋅t ρ⇩1 ⊙ γ = (context.from_ground c⇩G')⟨term.from_ground t⇩G⇩1⟩"
        proof -

          have "context.is_ground (c⇩1 ⋅t⇩c ρ⇩1 ⊙ γ)"
            using c⇩1_t⇩1_γ
            unfolding c⇩1_t⇩1 context.safe_unfolds
            by (metis context.ground_is_ground context.term_with_context_is_ground
                term.ground_is_ground)

          then show ?thesis
            using c⇩1_t⇩1_γ
            unfolding c⇩1_t⇩1 c⇩1_t⇩1_γ c⇩G
            by auto
        qed

        have t⇩1_γ': "t⇩1 ⋅t ρ⇩1 ⊙ γ' = (context.from_ground c⇩G')⟨term.from_ground t⇩G⇩3⟩"
          unfolding γ'_def
          using t⇩1_ρ⇩1
          by simp

        show "?E⇩G' ∈ N⇩G"
        proof-

          have "?E⇩G' ∈ clause.welltyped_ground_instances (E, 𝒱⇩1)"
          proof(unfold clause.welltyped_ground_instances_def mem_Collect_eq fst_conv snd_conv,
              intro exI conjI E_is_welltyped 𝒱⇩1,
              rule refl)

            show "clause.is_ground (E ⋅ ρ⇩1 ⊙ γ')"
              unfolding γ'_def
              using E_grounding
              by simp

            show "term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 (ρ⇩1 ⊙ γ')"
            proof(intro term.welltyped.typed_subst_compose ρ⇩1_is_welltyped)

              have "welltyped 𝒱⇩1 ?t⇩G (𝒱⇩1 x)"
              proof-

                have "welltyped 𝒱⇩1 (context.from_ground c⇩G')⟨term.from_ground t⇩G⇩1⟩ (𝒱⇩1 x)"
                proof-

                  have "welltyped 𝒱⇩1 (t⇩1 ⋅t ρ⇩1) (𝒱⇩1 x)"
                    using t⇩1_ρ⇩1
                    by auto

                  then have "welltyped 𝒱⇩1 (t⇩1 ⋅t ρ⇩1 ⊙ γ) (𝒱⇩1 x)"
                    using ρ⇩1_is_welltyped ρ⇩1_γ_is_welltyped
                    unfolding E c⇩1_t⇩1 l⇩1 subst_compose_def
                    by simp

                  moreover have "context.is_ground (c⇩1 ⋅t⇩c ρ⇩1 ⊙ γ)"
                    using c⇩1_t⇩1_γ
                    unfolding c⇩1_t⇩1 context.safe_unfolds
                    by (metis context.ground_is_ground context.term_with_context_is_ground
                        term.ground_is_ground)

                  then have "t⇩1 ⋅t ρ⇩1 ⊙ γ = (context.from_ground c⇩G')⟨term.from_ground t⇩G⇩1⟩"
                    using c⇩1_t⇩1_γ
                    unfolding c⇩1_t⇩1 c⇩1_t⇩1_γ c⇩G
                    by auto

                  ultimately show ?thesis
                    by argo
                qed

                moreover obtain τ where
                  "welltyped 𝒱⇩1 (term.from_ground t⇩G⇩1) τ"
                  "welltyped 𝒱⇩1 (term.from_ground t⇩G⇩3) τ"
                proof-
                  have "clause.is_welltyped 𝒱⇩2 (clause.from_ground D⇩G)"
                    using D_is_welltyped
                    unfolding
                      D⇩G_def
                      clause.to_ground_inverse[OF D_grounding]
                      clause.is_welltyped.subst_stability[OF ρ⇩2_γ_is_welltyped].

                  then obtain τ where
                    "welltyped 𝒱⇩2 (term.from_ground t⇩G⇩1) τ"
                    "welltyped 𝒱⇩2 (term.from_ground t⇩G⇩3) τ"
                    unfolding ground_superpositionI
                    by auto

                  then show ?thesis
                    using that term.welltyped.explicit_replace_𝒱_iff[of _ 𝒱⇩2 𝒱⇩1]
                    by simp
                qed

                 ultimately show ?thesis
                  by auto
              qed

              moreover have "term.subst.is_welltyped_on (⋃ (term.vars ` ρ⇩1 ` clause.vars E)) 𝒱⇩1 γ"
                by (intro term.welltyped.renaming_subst_compose ρ⇩1_γ_is_welltyped ρ⇩1_is_welltyped ρ⇩1)

              ultimately show
                "term.subst.is_welltyped_on (⋃ (term.vars ` ρ⇩1 ` clause.vars E)) 𝒱⇩1 γ'"
                unfolding γ'_def
                by simp
            qed
          qed

          then show ?thesis
            by simp
        qed

        show "ground.G_entails {?E⇩G', D⇩G} {C⇩G}"
        proof(unfold ground.G_entails_def, intro allI impI)
          fix I :: "'f gterm rel"
          let ?I = "upair ` I"

          assume
            refl_I: "refl I" and
            trans_I: "trans I" and
            sym_I: "sym I" and
            compatible_with_gctxt_I: "compatible_with_gctxt I" and
            premise: "?I ⊫s {?E⇩G', D⇩G}"

           then interpret clause_entailment I
             by unfold_locales

          have γ_x_is_ground: "term.is_ground (γ x)"
            using t⇩1_γ t⇩1_ρ⇩1
            by auto

          show "?I ⊫s {C⇩G}"
          proof(cases "?I ⊫ D⇩G'")
            case True

            then show ?thesis
              unfolding ground_superpositionI
              by auto
          next
            case False

            then have t⇩G⇩1_t⇩G⇩3: "Upair t⇩G⇩1 t⇩G⇩3 ∈ ?I"
              using premise sym
              unfolding ground_superpositionI
              by auto

            have "?I ⊫l c⇩G'⟨t⇩G⇩1⟩⇩G ≈ c⇩G'⟨t⇩G⇩3⟩⇩G"
              using upair_compatible_with_gctxtI[OF t⇩G⇩1_t⇩G⇩3]
              by auto

            then have "?I ⊫l term.to_ground (t⇩1 ⋅t ρ⇩1 ⊙ γ) ≈ term.to_ground (t⇩1 ⋅t ρ⇩1 ⊙ γ')"
              unfolding t⇩1_γ t⇩1_γ'
              by simp

            then have "(term.to_ground (γ x), c⇩G'⟨t⇩G⇩3⟩⇩G) ∈ I"
              unfolding γ'_def
              using t⇩1_ρ⇩1
              by (auto simp: sym)

            moreover have "?I ⊫ ?E⇩G'"
              using premise
              by simp

            ultimately have "?I ⊫ E⇩G"
              unfolding γ'_def
              using
                clause.symmetric_congruence[of _ γ, OF _ γ_x_is_ground]
                E_grounding
              by simp

            then have "?I ⊫ add_mset (𝒫⇩G (Upair c⇩G⟨t⇩G⇩3⟩⇩G t⇩G⇩2)) E⇩G'"
              unfolding ground_superpositionI
              using symmetric_literal_context_congruence[OF t⇩G⇩1_t⇩G⇩3]
              by (cases "𝒫⇩G = Pos") simp_all

            then show ?thesis
              unfolding ground_superpositionI
              by blast
          qed
        qed

        show "?E⇩G' ≺⇩c⇩G E⇩G"
        proof-

          have "γ x = t⇩1 ⋅t ρ⇩1 ⊙ γ"
            using t⇩1_ρ⇩1
            by simp

          then have t⇩G_smaller: "?t⇩G ≺⇩t γ x"
            using ground_superpositionI(8)
            unfolding t⇩1_γ term.order.less⇩G_def
            by simp

          have "add_mset (l⇩1 ⋅l ρ⇩1 ⊙ γ') (E' ⋅ ρ⇩1 ⊙ γ') ≺⇩c add_mset (l⇩1 ⋅l ρ⇩1 ⊙ γ) (E' ⋅ ρ⇩1 ⊙ γ)"
          proof(rule less⇩c_add_mset)

            have "x ∈ literal.vars (l⇩1 ⋅l ρ⇩1)"
              unfolding l⇩1 c⇩1_t⇩1 literal.vars_def atom.vars_def
              using t⇩1_ρ⇩1
              by auto

            moreover have "literal.is_ground (l⇩1 ⋅l ρ⇩1 ⊙ γ)"
              using E_grounding
              unfolding E
              by simp

            ultimately show "l⇩1 ⋅l ρ⇩1 ⊙ γ' ≺⇩l l⇩1 ⋅l ρ⇩1 ⊙ γ"
              unfolding γ'_def
              using literal.order.subst_update_stability t⇩G_smaller
              by simp
          next

            have "clause.is_ground (E' ⋅ ρ⇩1 ⊙ γ)"
              using E'_γ
              by simp

            then show "E' ⋅ ρ⇩1 ⊙ γ' ≼⇩c E' ⋅ ρ⇩1 ⊙ γ"
              unfolding γ'_def
              using clause.order.subst_update_stability t⇩G_smaller
              by (cases "x ∈ clause.vars (E' ⋅ ρ⇩1)") simp_all
          qed

          then have "E ⋅ ρ⇩1 ⊙ γ' ≺⇩c E ⋅ ρ⇩1 ⊙ γ"
            unfolding E
            by simp

          moreover have "clause.is_ground (E ⋅ ρ⇩1 ⊙ γ')"
            unfolding γ'_def
            using E_grounding
            by simp

          ultimately show ?thesis
            using E_grounding
            unfolding clause.order.less⇩G_def
            by simp
        qed
      qed
    qed

    then show ?thesis
      using not_redundant ground_superposition that l⇩1 t⇩1'_γ c⇩1_t⇩1_γ
      unfolding ground.Red_I_def ground.G_Inf_def
      by auto
  qed

  obtain l⇩2 where
    l⇩2_γ: "l⇩2 ⋅l ρ⇩2 ⊙ γ = literal.from_ground l⇩G⇩2" and
    l⇩2_is_strictly_maximal: "is_strictly_maximal l⇩2 D"
  proof-
    have "is_strictly_maximal (literal.from_ground l⇩G⇩2) (D ⋅ ρ⇩2 ⊙ γ)"
      using ground_superpositionI(11) D_grounding
      by simp

    then show ?thesis
      using obtain_strictly_maximal_literal[OF D_grounding] that
      by metis
  qed

  then have l⇩2_in_D: "l⇩2 ∈# D"
    using strictly_maximal_in_clause
    by blast

  from l⇩2_γ have l⇩2_γ: "l⇩2 ⋅l ρ⇩2 ⊙ γ = term.from_ground t⇩G⇩1 ≈ term.from_ground t⇩G⇩3"
    unfolding ground_superpositionI
    by simp

  then obtain t⇩2 t⇩2' where
    l⇩2: "l⇩2 = t⇩2 ≈ t⇩2'" and
    t⇩2_γ: "t⇩2 ⋅t ρ⇩2 ⊙ γ = term.from_ground t⇩G⇩1" and
    t⇩2'_γ: "t⇩2' ⋅t ρ⇩2 ⊙ γ = term.from_ground t⇩G⇩3"
    using obtain_from_pos_literal_subst
    by metis

  obtain D' where D: "D = add_mset l⇩2 D'"
    by (meson l⇩2_in_D multi_member_split)

  then have D'_γ: "D' ⋅ ρ⇩2 ⊙ γ = clause.from_ground D⇩G'"
    using D_γ l⇩2_γ
    unfolding ground_superpositionI
    by auto

  obtain 𝒱⇩3 where
    𝒱⇩3: "infinite_variables_per_type 𝒱⇩3" and
    𝒱⇩1_𝒱⇩3: "∀x∈clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x)" and
    𝒱⇩2_𝒱⇩3: "∀x∈clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x)"
    using clause.obtain_merged_𝒱[OF ρ⇩1 ρ⇩2 rename_apart clause.finite_vars clause.finite_vars 
                                 infinite_UNIV] .

  have γ_is_welltyped:
    "term.subst.is_welltyped_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 γ"
  proof(unfold Set.ball_Un, intro conjI)

    show "term.subst.is_welltyped_on (clause.vars (E ⋅ ρ⇩1)) 𝒱⇩3 γ"
      using clause.is_welltyped.renaming_grounding[OF ρ⇩1 ρ⇩1_γ_is_welltyped E_grounding 𝒱⇩1_𝒱⇩3].
  next

    show "term.subst.is_welltyped_on (clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 γ"
      using clause.is_welltyped.renaming_grounding[OF ρ⇩2 ρ⇩2_γ_is_welltyped D_grounding 𝒱⇩2_𝒱⇩3].
  qed

  obtain μ σ where
    γ: "γ = μ ⊙ σ" and
    imgu: "welltyped_imgu_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 (t⇩1 ⋅t ρ⇩1) (t⇩2 ⋅t ρ⇩2) μ"
  proof-

    have unified: "t⇩1 ⋅t ρ⇩1 ⋅t γ = t⇩2 ⋅t ρ⇩2 ⋅t γ"
      using t⇩1_γ t⇩2_γ
      by simp

    obtain τ where welltyped: "welltyped 𝒱⇩3 (t⇩1 ⋅t ρ⇩1) τ" "welltyped 𝒱⇩3 (t⇩2 ⋅t ρ⇩2) τ"
    proof-
      have "clause.is_welltyped 𝒱⇩2 (D ⋅ ρ⇩2 ⊙ γ)"
        using ρ⇩2_γ_is_welltyped D_is_welltyped
        by (metis clause.is_welltyped.subst_stability)

      then obtain τ where
        "welltyped 𝒱⇩2 (term.from_ground t⇩G⇩1) τ"
        unfolding D_γ ground_superpositionI
        by auto

      then have "welltyped 𝒱⇩3 (term.from_ground t⇩G⇩1) τ"
        using term.welltyped.is_ground_typed
        by (meson term.ground_is_ground term.welltyped.explicit_is_ground_typed)

      then have "welltyped 𝒱⇩3 (t⇩1 ⋅t ρ⇩1 ⊙ γ) τ" "welltyped 𝒱⇩3 (t⇩2 ⋅t ρ⇩2 ⊙ γ) τ"
        using t⇩1_γ t⇩2_γ
        by presburger+

      moreover have
        "term.vars (t⇩1 ⋅t ρ⇩1) ⊆ clause.vars (E ⋅ ρ⇩1)"
        "term.vars (t⇩2 ⋅t ρ⇩2) ⊆ clause.vars (D ⋅ ρ⇩2)"
        unfolding E l⇩1 clause.add_subst D l⇩2
        by auto

      ultimately have "welltyped 𝒱⇩3 (t⇩1 ⋅t ρ⇩1) τ" "welltyped 𝒱⇩3 (t⇩2 ⋅t ρ⇩2) τ"
        using γ_is_welltyped
        by (simp_all add: subsetD)

      then show ?thesis
        using that
        by blast
    qed

    show ?thesis
      using obtain_welltyped_imgu_on[OF unified welltyped] that
      by metis
  qed

  define C' where
    C': "C' = add_mset (?𝒫 (Upair (c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ (t⇩1' ⋅t ρ⇩1))) (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ"

  show ?thesis
  proof(rule that)

    show superposition: "superposition (D, 𝒱⇩2) (E, 𝒱⇩1) (C', 𝒱⇩3)"
    proof(rule superpositionI;
           ((rule ρ⇩1 ρ⇩2 E D l⇩1 l⇩2 t⇩1_is_Fun imgu rename_apart ρ⇩1_is_welltyped ρ⇩2_is_welltyped 𝒱⇩1 𝒱⇩2 C'
               𝒱⇩1_𝒱⇩3 𝒱⇩2_𝒱⇩3)+)?)

      show "?𝒫 ∈ {Pos, Neg}"
        by simp
    next

      show "¬ E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ"
      proof(rule clause.order.ground_less_not_less_eq)

        show "clause.vars (D ⋅ ρ⇩2 ⊙ μ ⋅ σ) = {}"
          using D_grounding
          unfolding γ
          by simp

        show "clause.vars (E ⋅ ρ⇩1 ⊙ μ ⋅ σ) = {}"
          using E_grounding
          unfolding γ
          by simp

        show "D ⋅ ρ⇩2 ⊙ μ ⋅ σ ≺⇩c E ⋅ ρ⇩1 ⊙ μ ⋅ σ"
          using ground_superpositionI(3) D_grounding E_grounding
          unfolding E⇩G_def D⇩G_def clause.order.less⇩G_def γ
          by simp
      qed
    next
      assume "?𝒫 = Pos"

      then show "select E = {#}"
        using ground_superpositionI(9) select_from_E
        by fastforce

    next
      assume Pos: "?𝒫 = Pos"

      show "is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)"
      proof(rule is_strictly_maximal_if_grounding_is_strictly_maximal)

        show "l⇩1 ⋅l ρ⇩1 ⊙ μ ∈# E ⋅ ρ⇩1 ⊙ μ"
          using l⇩1_in_E
          by blast

        show "clause.is_ground (E ⋅ ρ⇩1 ⊙ μ ⋅ σ)"
          using E_grounding[unfolded γ]
          by simp

        show "is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ ⋅l σ) (E ⋅ ρ⇩1 ⊙ μ ⋅ σ)"
          using Pos l⇩1_γ E_γ ground_superpositionI(9)
          unfolding γ ground_superpositionI
          by fastforce
      qed
    next
      assume Neg: "?𝒫 = Neg" "select E = {#}"

      show "is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)"
      proof(rule is_maximal_if_grounding_is_maximal)

          show "l⇩1 ⋅l ρ⇩1 ⊙ μ ∈# E ⋅ ρ⇩1 ⊙ μ"
            using l⇩1_in_E
            by blast
        next

          show "clause.is_ground (E ⋅ ρ⇩1 ⊙ μ ⋅ σ)"
            using E_grounding γ
            by auto
        next

          show "is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ ⋅l σ) (E ⋅ ρ⇩1 ⊙ μ ⋅ σ) "
            using l⇩1_γ γ E_γ ground_superpositionI(5,9) is_maximal_not_empty Neg select_from_E
            by auto
        qed
    next
      assume Neg: "?𝒫 = Neg" "select E ≠ {#}"

      show "is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) ((select E) ⋅ ρ⇩1 ⊙ μ)"
      proof(rule is_maximal_if_grounding_is_maximal)

        show "l⇩1 ⋅l ρ⇩1 ⊙ μ ∈# select E ⋅ ρ⇩1 ⊙ μ"
          using ground_superpositionI(9) l⇩1_selected maximal_in_clause Neg select_from_E
          by force
      next

        show "clause.is_ground (select E ⋅ ρ⇩1 ⊙ μ ⋅ σ)"
          using select_ground_subst[OF E_grounding]
          unfolding γ
          by simp
      next
        show "is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ ⋅l σ) (select E ⋅ ρ⇩1 ⊙ μ ⋅ σ)"
          using γ ground_superpositionI(5,9) l⇩1_γ that select_from_E Neg
          by fastforce
      qed
    next

      show "select D = {#}"
        using ground_superpositionI(10) select_from_D
        by simp
    next

      show "is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ)"
      proof(rule is_strictly_maximal_if_grounding_is_strictly_maximal)

        show "l⇩2 ⋅l ρ⇩2 ⊙ μ ∈# D ⋅ ρ⇩2 ⊙ μ"
          using l⇩2_in_D
          by blast
      next

        show "clause.is_ground (D ⋅ ρ⇩2 ⊙ μ ⋅ σ)"
          using D_grounding
          unfolding γ
          by simp
      next

        show "is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ ⋅l σ) (D ⋅ ρ⇩2 ⊙ μ ⋅ σ)"
          using l⇩2_γ γ D_γ ground_superpositionI(6,11)
          by auto
      qed
    next

      show "¬ c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ"
      proof(rule term.order.ground_less_not_less_eq)

        show "term.is_ground (t⇩1' ⋅t ρ⇩1 ⊙ μ ⋅t σ)"
          using t⇩1'_γ γ
          by simp
      next

        show "term.is_ground (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ⋅t σ)"
          using t⇩1_γ c⇩1_γ γ
          by simp
      next

        show "t⇩1' ⋅t ρ⇩1 ⊙ μ ⋅t σ ≺⇩t c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ⋅t σ"
          using ground_superpositionI(7) c⇩1_γ t⇩1'_γ t⇩1_γ
          unfolding term.order.less⇩G_def γ
          by auto
      qed
    next

      show "¬ t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ"
      proof(rule term.order.ground_less_not_less_eq)

        show "term.is_ground (t⇩2' ⋅t ρ⇩2 ⊙ μ ⋅t σ)"
          using t⇩2'_γ γ
          by simp
      next

        show "term.is_ground (t⇩2 ⋅t ρ⇩2 ⊙ μ ⋅t σ)"
          using t⇩2_γ γ
          by simp
      next

        show "t⇩2' ⋅t ρ⇩2 ⊙ μ ⋅t σ ≺⇩t t⇩2 ⋅t ρ⇩2 ⊙ μ ⋅t σ"
          using ground_superpositionI(8) t⇩2_γ t⇩2'_γ
          unfolding γ term.order.less⇩G_def
          by simp
      qed
    next

      have "∃τ. welltyped 𝒱⇩2 t⇩2 τ ∧ welltyped 𝒱⇩2 t⇩2' τ"
        using D_is_welltyped
        unfolding D l⇩2
        by auto

      then show "⋀τ τ'. ⟦typed 𝒱⇩2 t⇩2 τ; typed 𝒱⇩2 t⇩2' τ'⟧ ⟹ τ = τ'"
        using term.typed_if_welltyped
        by blast
    qed

    show C'_γ: "C' ⋅ γ = C ⋅ γ"
    proof-

      have "term_subst.is_idem μ"
        using imgu term.is_imgu_iff_is_idem_and_is_mgu
        by blast

      then have μ_γ: "μ ⊙ γ = γ"
        unfolding γ term_subst.is_idem_def
        by (metis subst_compose_assoc)

      have "C ⋅ γ =
              add_mset
                (?𝒫 (Upair (context.from_ground c⇩G)⟨term.from_ground t⇩G⇩3⟩ (term.from_ground t⇩G⇩2)))
                  (clause.from_ground E⇩G' + clause.from_ground D⇩G')"
        using ground_superpositionI(4, 12) clause.to_ground_inverse[OF C_grounding]
        by auto

      then show ?thesis
        unfolding
          C'
          E'_γ[symmetric]
          D'_γ[symmetric]
          t⇩1'_γ[symmetric]
          t⇩2'_γ[symmetric]
          c⇩1_γ[symmetric]
          clause.subst_comp_subst[symmetric]
          μ_γ
        by simp
    qed

    show "ι⇩G ∈ inference_ground_instances (Infer [(D, 𝒱⇩2), (E, 𝒱⇩1)] (C', 𝒱⇩3))"
    proof (rule is_inference_ground_instance_two_premises)

      show "is_inference_ground_instance_two_premises (D, 𝒱⇩2) (E, 𝒱⇩1) (C', 𝒱⇩3) ι⇩G γ ρ⇩1 ρ⇩2"
      proof(unfold split, intro conjI;
            (rule ρ⇩1 ρ⇩2 rename_apart D_is_welltyped E_is_welltyped refl 𝒱⇩1 𝒱⇩2 𝒱⇩3)?)

        show "inference.is_ground (Infer [D ⋅ ρ⇩2, E ⋅ ρ⇩1] C' ⋅ι γ)"
          using  D_grounding E_grounding C_grounding C'_γ
          by auto
      next

        show "ι⇩G = inference.to_ground (Infer [D ⋅ ρ⇩2, E ⋅ ρ⇩1] C' ⋅ι γ)"
          using C'_γ
          by simp
      next

        show "clause.is_welltyped 𝒱⇩3 C'"
          using superposition superposition_preserves_typing E_is_welltyped D_is_welltyped
          by blast
      next

        show "term.subst.is_welltyped_on (clause.vars C') 𝒱⇩3 γ"
        proof(rule term.is_welltyped_on_subset[OF γ_is_welltyped])

          show "clause.vars C' ⊆ clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)"
          proof (unfold subset_eq, intro ballI)
            fix x

            have is_imgu: "term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}}"
              using imgu
              by blast

            assume "x ∈ clause.vars C'"

            then consider
              (t⇩2') "x ∈ term.vars (t⇩2' ⋅t ρ⇩2 ⊙ μ)" |
              (c⇩1) "x ∈ context.vars (c⇩1 ⋅t⇩c ρ⇩1 ⊙ μ)" |
              (t⇩1') "x ∈ term.vars (t⇩1' ⋅t ρ⇩1 ⊙ μ)" |
              (E') "x ∈ clause.vars (E' ⋅ ρ⇩1 ⊙ μ)" |
              (D') "x ∈ clause.vars (D' ⋅ ρ⇩2 ⊙ μ)"
              unfolding C'
              by auto

            then show "x ∈ clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)"
            proof cases
              case t⇩2'

              then show ?thesis
                using term.variables_in_base_imgu[OF is_imgu]
                unfolding E l⇩1 D l⇩2
                by auto
            next
              case c⇩1

              then show ?thesis
                using context.variables_in_base_imgu[OF is_imgu]
                unfolding E l⇩1 D l⇩2
                by force
            next
              case t⇩1'

              then show ?thesis
                using term.variables_in_base_imgu[OF is_imgu]
                unfolding E clause.add_subst l⇩1 D l⇩2
                by auto
            next
              case E'

              then show ?thesis
                using clause.variables_in_base_imgu[OF is_imgu]
                unfolding E l⇩1 D l⇩2
                by auto
            next
              case D'

              then show ?thesis
                using clause.variables_in_base_imgu[OF is_imgu]
                unfolding E l⇩1 D l⇩2
                by auto
            qed
          qed
        qed
      qed

      show "ι⇩G ∈ ground.G_Inf"
        unfolding ground.G_Inf_def
        using ground_superposition
        by simp
    qed
  qed
qed

subsection ‹Ground instances›

context
  fixes ι⇩G N
  assumes
    subst_stability: "subst_stability_on N" and
    ι⇩G_Inf_from: "ι⇩G ∈ ground.Inf_from_q select⇩G (⋃(clause.welltyped_ground_instances ` N))"
begin

lemma single_premise_ground_instance:
  assumes
    ground_inference: "ι⇩G ∈  {Infer [D] C | D C. ground_inference D C}" and
    lifting: "⋀D γ C 𝒱 thesis. ⟦
    ground_inference (clause.to_ground (D ⋅ γ)) (clause.to_ground (C ⋅ γ));
    clause.is_ground (D ⋅ γ);
    clause.is_ground (C ⋅ γ);
    clause.from_ground (select⇩G (clause.to_ground (D ⋅ γ))) = select D ⋅ γ;
    clause.is_welltyped 𝒱 D; 
    term.subst.is_welltyped_on (clause.vars D) 𝒱 γ;
    infinite_variables_per_type 𝒱;
    ⋀C'. ⟦
        inference (D, 𝒱) (C', 𝒱);
        Infer [clause.to_ground (D ⋅ γ)] (clause.to_ground (C ⋅ γ))
        ∈ inference_ground_instances (Infer [(D, 𝒱)] (C', 𝒱));
        C' ⋅ γ = C ⋅ γ⟧ ⟹ thesis⟧
       ⟹ thesis" and
    inference_eq: "inference = eq_factoring ∨ inference = eq_resolution"
  obtains ι where
    "ι ∈ Inf_from N"
    "ι⇩G ∈ inference_ground_instances ι"
proof-
  obtain D⇩G C⇩G where
    ι⇩G: "ι⇩G = Infer [D⇩G] C⇩G" and
    ground_inference: "ground_inference D⇩G C⇩G"
    using ground_inference
    by blast

  have D⇩G_in_groundings: "D⇩G ∈ ⋃(clause.welltyped_ground_instances ` N)"
    using ι⇩G_Inf_from
    unfolding ι⇩G ground.Inf_from_q_def ground.Inf_from_def
    by simp

  obtain D γ 𝒱 where
    D_grounding: "clause.is_ground (D ⋅ γ)" and
    D_is_welltyped: "clause.is_welltyped 𝒱 D" and
    γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱 γ" and
    𝒱: "infinite_variables_per_type 𝒱" and
    D_in_N: "(D, 𝒱)∈N" and
    "select⇩G D⇩G = clause.to_ground (select D ⋅ γ)"
    "D ⋅ γ = clause.from_ground D⇩G"
    using subst_stability[rule_format, OF D⇩G_in_groundings]
    by blast

  then have
    D⇩G: "D⇩G = clause.to_ground (D ⋅ γ)" and
    select: "clause.from_ground (select⇩G D⇩G) = select D ⋅ γ"
    by (simp_all add: select_ground_subst)

  obtain C where
    C⇩G: "C⇩G = clause.to_ground (C ⋅ γ)" and
    C_grounding: "clause.is_ground (C ⋅ γ)"
    by (metis clause.all_subst_ident_iff_ground clause.from_ground_inverse
        clause.ground_is_ground)

  obtain C' where
    inference: "inference (D, 𝒱) (C', 𝒱)" and
    inference_ground_instances: "ι⇩G ∈ inference_ground_instances (Infer [(D, 𝒱)] (C', 𝒱))" and
    C'_C: "C' ⋅ γ = C ⋅ γ"
    using
      lifting[OF
        ground_inference[unfolded D⇩G C⇩G]
        D_grounding
        C_grounding
        select[unfolded D⇩G]
        D_is_welltyped
        γ_is_welltyped
        𝒱]
    unfolding D⇩G C⇩G ι⇩G.

  let ?ι = "Infer [(D, 𝒱)] (C', 𝒱)"

  show ?thesis
  proof(rule that[OF _ inference_ground_instances])

    show "?ι ∈ Inf_from N"
      using D_in_N inference inference_eq
      unfolding Inf_from_def inferences_def inference_system.Inf_from_def
      by auto
  qed
qed

lemma eq_resolution_ground_instance:
  assumes ground_eq_resolution: "ι⇩G ∈ ground.eq_resolution_inferences"
  obtains ι where
    "ι ∈ Inf_from N"
    "ι⇩G ∈ inference_ground_instances ι"
  using eq_resolution_lifting single_premise_ground_instance[OF ground_eq_resolution]
  by blast

lemma eq_factoring_ground_instance:
  assumes ground_eq_factoring: "ι⇩G ∈ ground.eq_factoring_inferences"
  obtains ι where
    "ι ∈ Inf_from N"
    "ι⇩G ∈ inference_ground_instances ι"
  using eq_factoring_lifting single_premise_ground_instance[OF ground_eq_factoring]
  by blast

lemma superposition_ground_instance:
  assumes
    ground_superposition: "ι⇩G ∈ ground.superposition_inferences" and
    not_redundant: "ι⇩G ∉ ground.GRed_I (⋃ (clause.welltyped_ground_instances ` N))"
  obtains ι where
    "ι ∈ Inf_from N"
    "ι⇩G ∈ inference_ground_instances ι"
proof-
  obtain E⇩G D⇩G C⇩G where
    ι⇩G : "ι⇩G = Infer [D⇩G, E⇩G] C⇩G" and
    ground_superposition: "ground.superposition D⇩G E⇩G C⇩G"
    using assms(1)
    by blast

  have
    E⇩G_in_groundings: "E⇩G ∈ ⋃ (clause.welltyped_ground_instances ` N)" and
    D⇩G_in_groundings: "D⇩G ∈ ⋃ (clause.welltyped_ground_instances ` N)"
    using ι⇩G_Inf_from
    unfolding ι⇩G ground.Inf_from_q_def ground.Inf_from_def
    by simp_all

  obtain E 𝒱⇩1 γ⇩1 where
    E_grounding: "clause.is_ground (E ⋅ γ⇩1)" and
    E_is_welltyped: "clause.is_welltyped 𝒱⇩1 E" and
    γ⇩1_is_welltyped: "term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 γ⇩1" and
    𝒱⇩1: "infinite_variables_per_type 𝒱⇩1" and
    E_in_N: "(E, 𝒱⇩1)∈N" and
    "select⇩G E⇩G = clause.to_ground (select E ⋅ γ⇩1)"
    "E ⋅ γ⇩1 = clause.from_ground E⇩G"
    using subst_stability[rule_format, OF E⇩G_in_groundings]
    by blast

  then have
    E⇩G: "E⇩G = clause.to_ground (E ⋅ γ⇩1)" and
    select_from_E: "clause.from_ground (select⇩G E⇩G) = select E ⋅ γ⇩1"
    by (simp_all add: select_ground_subst)

  obtain D 𝒱⇩2 γ⇩2 where
    D_grounding: "clause.is_ground (D ⋅ γ⇩2)" and
    D_is_welltyped: "clause.is_welltyped 𝒱⇩2 D" and
    γ⇩2_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 γ⇩2" and
    𝒱⇩2: "infinite_variables_per_type 𝒱⇩2" and
    D_in_N: "(D, 𝒱⇩2)∈N" and
    "select⇩G D⇩G = clause.to_ground (select D ⋅ γ⇩2)"
    "D ⋅ γ⇩2 = clause.from_ground D⇩G"
    using subst_stability[rule_format, OF D⇩G_in_groundings]
    by blast

  then have
    D⇩G: "D⇩G = clause.to_ground (D ⋅ γ⇩2)" and
    select_from_D: "clause.from_ground (select⇩G D⇩G) = select D ⋅ γ⇩2"
    by (simp_all add: select_ground_subst)

  obtain ρ⇩1 ρ⇩2 γ :: "('f, 'v) subst" where
    ρ⇩1: "term_subst.is_renaming ρ⇩1" and
    ρ⇩2: "term_subst.is_renaming ρ⇩2" and
    rename_apart: "clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {}" and
    ρ⇩1_is_welltyped: "term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 ρ⇩1" and
    ρ⇩2_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 ρ⇩2" and
    γ⇩1_γ: "∀x ∈ clause.vars E. γ⇩1 x = (ρ⇩1 ⊙ γ) x" and
    γ⇩2_γ: "∀x ∈ clause.vars D. γ⇩2 x = (ρ⇩2 ⊙ γ) x"
    using clause.is_welltyped.obtain_merged_grounding[OF
            γ⇩1_is_welltyped γ⇩2_is_welltyped E_grounding D_grounding 𝒱⇩2 clause.finite_vars].

  have E_grounding: "clause.is_ground (E ⋅ ρ⇩1 ⊙ γ)"
    using clause.subst_eq γ⇩1_γ E_grounding
    by fastforce

  have E⇩G: "E⇩G = clause.to_ground (E ⋅ ρ⇩1 ⊙ γ)"
    using clause.subst_eq γ⇩1_γ E⇩G
    by fastforce

  have D_grounding: "clause.is_ground (D ⋅ ρ⇩2 ⊙ γ)"
    using clause.subst_eq γ⇩2_γ D_grounding
    by fastforce

  have D⇩G: "D⇩G = clause.to_ground (D ⋅ ρ⇩2 ⊙ γ)"
    using clause.subst_eq γ⇩2_γ D⇩G
    by fastforce

  have ρ⇩1_γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars E) 𝒱⇩1 (ρ⇩1 ⊙ γ)"
    using γ⇩1_is_welltyped γ⇩1_γ
    by fastforce

  have ρ⇩2_γ_is_welltyped: "term.subst.is_welltyped_on (clause.vars D) 𝒱⇩2 (ρ⇩2 ⊙ γ)"
    using γ⇩2_is_welltyped γ⇩2_γ
    by fastforce

  have select_from_E:
    "clause.from_ground (select⇩G (clause.to_ground (E ⋅ ρ⇩1 ⊙ γ))) = select E ⋅ ρ⇩1 ⊙ γ"
  proof-
    have "E ⋅ γ⇩1 = E ⋅ ρ⇩1 ⊙ γ"
      using γ⇩1_γ clause.subst_eq
      by fast

    moreover have "select E ⋅ γ⇩1 = select E ⋅ ρ⇩1 ⋅ γ"
      using clause.subst_eq γ⇩1_γ select_vars_subset
      by (metis (no_types, lifting) clause.comp_subst.left.monoid_action_compatibility in_mono)

    ultimately show ?thesis
      using select_from_E
      unfolding E⇩G
      by simp
  qed

  have select_from_D:
    "clause.from_ground (select⇩G (clause.to_ground (D ⋅ ρ⇩2 ⊙ γ))) = select D ⋅ ρ⇩2 ⊙ γ"
  proof-
    have "D ⋅ γ⇩2 = D ⋅ ρ⇩2 ⊙ γ"
      using γ⇩2_γ clause.subst_eq
      by fast

    moreover have "select D ⋅ γ⇩2 = select D ⋅ ρ⇩2 ⋅ γ"
      using clause.subst_eq γ⇩2_γ select_vars_subset[of D]
      by (metis (no_types, lifting) clause.comp_subst.left.monoid_action_compatibility in_mono)

    ultimately show ?thesis
      using select_from_D
      unfolding D⇩G
      by simp
  qed

  obtain C where
    C_grounding: "clause.is_ground (C ⋅ γ)" and
    C⇩G: "C⇩G = clause.to_ground (C ⋅ γ)"
    by (metis clause.all_subst_ident_if_ground clause.from_ground_inverse clause.ground_is_ground)

  have "clause.welltyped_ground_instances (E, 𝒱⇩1) ∪ clause.welltyped_ground_instances (D, 𝒱⇩2) ⊆
          ⋃ (clause.welltyped_ground_instances ` N)"
    using E_in_N D_in_N
    by blast

  then have ι⇩G_not_redundant:
    "ι⇩G ∉ ground.GRed_I
          (clause.welltyped_ground_instances (E, 𝒱⇩1) ∪ clause.welltyped_ground_instances (D, 𝒱⇩2))"
    using not_redundant ground.Red_I_of_subset
    by blast

  obtain C' 𝒱⇩3 where
    superposition: "superposition (D, 𝒱⇩2) (E, 𝒱⇩1) (C', 𝒱⇩3)" and
    inference_groundings: "ι⇩G ∈ inference_ground_instances (Infer [(D, 𝒱⇩2), (E, 𝒱⇩1)] (C', 𝒱⇩3))" and
    C'_γ_C_γ: "C' ⋅ γ = C ⋅ γ"
    using
      superposition_lifting[OF
        ground_superposition[unfolded D⇩G E⇩G C⇩G]
        ρ⇩1 ρ⇩2
        rename_apart
        E_grounding D_grounding C_grounding
        select_from_E select_from_D
        E_is_welltyped D_is_welltyped
        ρ⇩1_γ_is_welltyped ρ⇩2_γ_is_welltyped
        ρ⇩1_is_welltyped ρ⇩2_is_welltyped
        𝒱⇩1 𝒱⇩2
        ι⇩G_not_redundant[unfolded ι⇩G D⇩G E⇩G C⇩G]]
    unfolding ι⇩G C⇩G E⇩G D⇩G .

  let ?ι = "Infer [(D, 𝒱⇩2), (E, 𝒱⇩1)] (C', 𝒱⇩3)"

  show ?thesis
  proof(rule that[OF _ inference_groundings])

    show "?ι ∈ Inf_from N"
      using E_in_N D_in_N superposition
      unfolding Inf_from_def inferences_def inference_system.Inf_from_def
      by auto
  qed
qed

lemma ground_instances:
  assumes not_redundant: "ι⇩G ∉ ground.Red_I (⋃ (clause.welltyped_ground_instances ` N))"
  obtains ι where
    "ι ∈ Inf_from N"
    "ι⇩G ∈ inference_ground_instances ι"
proof-
  consider
    (superposition) "ι⇩G ∈ ground.superposition_inferences" |
    (eq_resolution) "ι⇩G ∈ ground.eq_resolution_inferences" |
    (eq_factoring) "ι⇩G ∈ ground.eq_factoring_inferences"
    using ι⇩G_Inf_from
    unfolding
      ground.Inf_from_q_def
      ground.G_Inf_def
      inference_system.Inf_from_def
    by fastforce

  then show ?thesis
  proof cases
    case superposition

    then show ?thesis
      using that superposition_ground_instance not_redundant
      by blast
  next
    case eq_resolution

    then show ?thesis
      using that eq_resolution_ground_instance
      by blast
  next
    case eq_factoring

    then show ?thesis
      using that eq_factoring_ground_instance
      by blast
  qed
qed

end

end

context superposition_calculus
begin

lemma overapproximation:
  obtains select⇩G where
    "ground_Inf_overapproximated select⇩G premises"
    "is_grounding select⇩G"
proof-
  obtain select⇩G where
    subst_stability: "select_subst_stability_on select select⇩G premises" and
    "is_grounding select⇩G"
    using obtain_subst_stable_on_select_grounding
    by blast

  then interpret grounded_superposition_calculus
    where select⇩G = select⇩G
    by unfold_locales

  show thesis
  proof(rule that[OF _ select⇩G])

    show "ground_Inf_overapproximated select⇩G premises"
      using ground_instances[OF subst_stability]
      by auto
  qed
qed

sublocale statically_complete_calculus "⊥⇩F" inferences entails_𝒢 Red_I_𝒢 Red_F_𝒢
proof(unfold static_empty_ord_inter_equiv_static_inter,
    rule stat_ref_comp_to_non_ground_fam_inter,
    rule ballI)
  fix select⇩G
  assume "select⇩G ∈ select⇩G⇩s"
  then interpret grounded_superposition_calculus
    where select⇩G = select⇩G
    by unfold_locales (simp add: select⇩G⇩s_def)

  show "statically_complete_calculus
          ground.G_Bot
          ground.G_Inf
          ground.G_entails
          ground.Red_I
          ground.Red_F"
    by unfold_locales
next

  show "⋀N. ∃select⇩G ∈ select⇩G⇩s. ground_Inf_overapproximated select⇩G N"
    using overapproximation
    unfolding select⇩G⇩s_def
    by (smt (verit, best) mem_Collect_eq)
qed

end

end