Theory Set_Proc

theory Set_Proc                
  imports Realisation HF_Extras Set_Semantics Typing
begin

chapter ‹A Decision Procedure for MLSS›
text ‹
  This theory proves the soundness and completeness of the
  tableau calculus defined in 🗏‹./Set_Calculus.thy›
  It then lifts those properties to a recursive procedure
  that applies the rules of the calculus exhaustively.
  To obtain a decision procedure, we also prove termination.
›

section ‹Basic Definitions›

definition "lin_sat b ≡ ∀b'. lexpands b' b ⟶ set b' ⊆ set b"

lemma lin_satD:
  assumes "lin_sat b"
  assumes "lexpands b' b"
  assumes "x ∈ set b'"
  shows "x ∈ set b"
  using assms unfolding lin_sat_def by auto

lemma not_lin_satD: "¬ lin_sat b ⟹ ∃b'. lexpands b' b ∧ set b ⊂ set (b' @ b)"
  unfolding lin_sat_def by auto

definition "sat b ≡ lin_sat b ∧ (∄bs'. bexpands bs' b)"

lemma satD:
  assumes "sat b"
  shows "lin_sat b" "∄bs'. bexpands bs' b"
  using assms unfolding sat_def by auto
                            
definition wits :: "'a branch ⇒ 'a set" where
  "wits b ≡ vars b - vars (last b)"

definition pwits :: "'a branch ⇒ 'a set" where
  "pwits b ≡ {c ∈ wits b. ∀t ∈ subterms (last b).
                  AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b}"

lemma wits_singleton[simp]: "wits [φ] = {}"
  unfolding wits_def vars_branch_simps by simp

lemma pwits_singleton[simp]: "pwits [φ] = {}"
  unfolding pwits_def by auto

lemma pwitsD:
  assumes "c ∈ pwits b"
  shows "c ∈ wits b"
        "t ∈ subterms (last b) ⟹ AT (Var c =⇩s t) ∉ set b"
        "t ∈ subterms (last b) ⟹ AT (t =⇩s Var c) ∉ set b"
  using assms unfolding pwits_def by auto

lemma pwitsI:
  assumes "c ∈ wits b"
  assumes "⋀t. t ∈ subterms (last b) ⟹ AT (Var c =⇩s t) ∉ set b"
  assumes "⋀t. t ∈ subterms (last b) ⟹ AT (t =⇩s Var c) ∉ set b"
  shows "c ∈ pwits b"
  using assms unfolding pwits_def by blast

lemma finite_wits: "finite (wits b)"
  unfolding wits_def using finite_vars_branch by auto

lemma finite_pwits: "finite (pwits b)"
proof -
  have "pwits b ⊆ wits b"
    unfolding pwits_def by simp
  then show ?thesis using finite_wits finite_subset by blast
qed

lemma lexpands_subterms_branch_eq:
  "lexpands b' b ⟹ b ≠ [] ⟹ subterms (b' @ b) = subterms b"
proof(induction rule: lexpands.induct)
  case (1 b' b)
  then show ?case
    apply(induction rule: lexpands_fm.induct)
         apply(auto simp: subterms_branch_def)
    done
next
  case (2 b' b)
  then show ?case
    apply(induction rule: lexpands_un.induct)
    using subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
         apply(auto simp: subterms_branch_simps 
          intro: subterms_term_subterms_branch_trans
          dest: subterms_branchD AT_mem_subterms_branchD AF_mem_subterms_branchD)
    done
next
  case (3 b' b)
  then show ?case
    apply(induction rule: lexpands_int.induct)
    using subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
         apply(auto simp: subterms_branch_simps 
          intro: subterms_term_subterms_branch_trans
          dest: subterms_branchD AT_mem_subterms_branchD AF_mem_subterms_branchD)
    done
next
  case (4 b' b)
  then show ?case
    apply(induction rule: lexpands_diff.induct)
    using subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
         apply(auto simp: subterms_branch_simps 
          intro: subterms_term_subterms_branch_trans
          dest: subterms_branchD AT_mem_subterms_branchD AF_mem_subterms_branchD)
    done
next
  case (5 b' b)
  then show ?case
  proof(induction rule: lexpands_single.induct)
    case (1 t1 b)
    then show ?case
      using subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]
      apply(auto simp: subterms_branch_simps
            dest: subterms_fmD intro: subterms_term_subterms_branch_trans)
      done
  qed (auto simp: subterms_branch_simps subterms_term_subterms_atom_Atom_trans
       dest: subterms_branchD AF_mem_subterms_branchD 
       intro: subterms_term_subterms_branch_trans)
next
  case (6 b' b)
  have *: "subterms_atom (subst_tlvl t1 t2 a) ⊆ subterms t2 ∪ subterms_atom a"
    for t1 t2 and a :: "'a pset_atom"
    by (cases "(t1, t2, a)" rule: subst_tlvl.cases) auto
  from 6 show ?case
  by (induction rule: lexpands_eq.induct)
     (auto simp: subterms_branch_def subterms_term_subterms_atom_Atom_trans
            dest!: subsetD[OF *])
qed

lemma lexpands_vars_branch_eq:
  "lexpands b' b ⟹ b ≠ [] ⟹ vars (b' @ b) = vars b"
  using lexpands_subterms_branch_eq subterms_branch_eq_if_vars_branch_eq by metis

lemma bexpands_nowit_subterms_branch_eq:
  "bexpands_nowit bs' b ⟹ b' ∈ bs' ⟹ b ≠ [] ⟹ subterms (b' @ b) = subterms b"
proof(induction rule: bexpands_nowit.induct)
  case (3 s t1 t2 b)
  then show ?case
    by (auto simp: subterms_term_subterms_atom_Atom_trans subterms_branch_simps)
next
  case (4 s t1 b t2)
  then show ?case
    using subterms_branch_subterms_subterms_fm_trans[OF _ _ "4"(2)]
    by (auto simp: subterms_term_subterms_atom_Atom_trans subterms_branch_simps)
next
  case (5 s t1 b t2)
  then show ?case
    using subterms_branch_subterms_subterms_fm_trans[OF _ _ "5"(2)]
    by (auto simp: subterms_term_subterms_atom_Atom_trans subterms_branch_simps)
qed (use subterms_branch_def in ‹(fastforce simp: subterms_branch_simps)+›)


lemma bexpands_nowit_vars_branch_eq:
  "bexpands_nowit bs' b ⟹ b' ∈ bs' ⟹ b ≠ [] ⟹ vars (b' @ b) = vars b"
  using bexpands_nowit_subterms_branch_eq subterms_branch_eq_if_vars_branch_eq by metis

lemma lexpands_wits_eq:
  "lexpands b' b ⟹ b ≠ [] ⟹ wits (b' @ b) = wits b"
  using lexpands_vars_branch_eq unfolding wits_def by force

lemma bexpands_nowit_wits_eq:
  assumes "bexpands_nowit bs' b" "b' ∈ bs'" "b ≠ []" 
  shows "wits (b' @ b) = wits b"
  using bexpands_nowit_vars_branch_eq[OF assms] assms(3)
  unfolding wits_def by simp

lemma bexpands_wit_vars_branch_eq:
  assumes "bexpands_wit t1 t2 x bs' b" "b' ∈ bs'" "b ≠ []"
  shows "vars (b' @ b) = insert x (vars b)"
  using assms bexpands_witD[OF assms(1)]
  by (auto simp: mem_vars_fm_if_mem_subterms_fm vars_branch_simps vars_fm_vars_branchI)

lemma bexpands_wit_wits_eq:
  assumes "bexpands_wit t1 t2 x bs' b" "b' ∈ bs'" "b ≠ []"
  shows "wits (b' @ b) = insert x (wits b)"
  using assms bexpands_witD[OF assms(1)]
  unfolding wits_def
  by (auto simp: mem_vars_fm_if_mem_subterms_fm vars_branch_simps vars_branch_def)

lemma lexpands_pwits_subs:
  assumes "lexpands b' b" "b ≠ []"
  shows "pwits (b' @ b) ⊆ pwits b"
  using assms lexpands_wits_eq[OF assms]
  by (induction rule: lexpands_induct) (auto simp: pwits_def)

subsection ‹‹no_new_subterms››

definition "no_new_subterms b ≡
   ∀t ∈ subterms b. t ∉ Var ` wits b ⟶ t ∈ subterms (last b)"

lemma no_new_subtermsI:
  assumes "⋀t. t ∈ subterms b ⟹ t ∉ Var ` wits b ⟹ t ∈ subterms (last b)"
  shows "no_new_subterms b"
  using assms unfolding no_new_subterms_def by blast

lemma Var_mem_subterms_branch_and_not_in_wits:
  assumes "Var v ∈ subterms b" "v ∉ wits b"
  shows "v ∈ vars (last b)"
  using assms unfolding wits_def no_new_subterms_def
  by (auto simp: image_set_diff[unfolded inj_on_def] image_UN
                 Un_vars_term_subterms_branch_eq_vars_branch[symmetric])

lemma subterms_branch_cases:
  assumes "t ∈ subterms b" "t ∉ Var ` wits b"
  obtains
    (Empty) n where "t = ∅ n"
  | (Union) t1 t2 where "t = t1 ⊔⇩s t2"
  | (Inter) t1 t2 where "t = t1 ⊓⇩s t2"
  | (Diff) t1 t2 where "t = t1 -⇩s t2"
  | (Single) t1 where "t = Single t1"
  | (Var) v where "t = Var v" "v ∈ vars (last b)"
proof(cases t)
  case (Var x)
  with assms have "x ∈ vars (last b)"
    using Var_mem_subterms_branch_and_not_in_wits by (metis imageI)
  with Var that show ?thesis by blast
qed (use assms that in auto)

lemma no_new_subterms_casesI[case_names Empty Union Inter Diff Single]:
  assumes "⋀n. ∅ n ∈ subterms b ⟹ ∅ n ∈ subterms (last b)"
  assumes "⋀t1 t2. t1 ⊔⇩s t2 ∈ subterms b ⟹ t1 ⊔⇩s t2 ∈ subterms (last b)"
  assumes "⋀t1 t2. t1 ⊓⇩s t2 ∈ subterms b ⟹ t1 ⊓⇩s t2 ∈ subterms (last b)"
  assumes "⋀t1 t2. t1 -⇩s t2 ∈ subterms b ⟹ t1 -⇩s t2 ∈ subterms (last b)"
  assumes "⋀t. Single t ∈ subterms b ⟹ Single t ∈ subterms (last b)"
  shows "no_new_subterms b"
proof(intro no_new_subtermsI)
  fix t assume "t ∈ subterms b" "t ∉ Var ` wits b"
  with this assms show "t ∈ subterms (last b)"
    by (cases t rule: subterms_branch_cases) (auto simp: vars_fm_subs_subterms_fm)
qed

lemma no_new_subtermsD:
  assumes "no_new_subterms b"
  shows "⋀n. ∅ n ∈ subterms b ⟹ ∅ n ∈ subterms (last b)"
        "⋀t1 t2. t1 ⊔⇩s t2 ∈ subterms b ⟹ t1 ⊔⇩s t2 ∈ subterms (last b)"
        "⋀t1 t2. t1 ⊓⇩s t2 ∈ subterms b ⟹ t1 ⊓⇩s t2 ∈ subterms (last b)"
        "⋀t1 t2. t1 -⇩s t2 ∈ subterms b ⟹ t1 -⇩s t2 ∈ subterms (last b)"
        "⋀t. Single t ∈ subterms b ⟹ Single t ∈ subterms (last b)"
  using assms unfolding no_new_subterms_def by auto

lemma lexpands_no_new_subterms:
  assumes "lexpands b' b" "b ≠ []"
  assumes "no_new_subterms b"
  shows "no_new_subterms (b' @ b)"
  using assms unfolding no_new_subterms_def
  by (simp add: lexpands_wits_eq lexpands_subterms_branch_eq[OF assms(1,2)])

lemma subterms_branch_subterms_atomI:
  assumes "Atom l ∈ set b" "t ∈ subterms_atom l"
  shows "t ∈ subterms_branch b"
  using assms unfolding subterms_branch_def  
  apply (cases l rule: subterms_atom.cases)
   apply (metis subterms_branch_def subterms_term_subterms_atom_Atom_trans subterms_refl)+
  done
  
lemma bexpands_nowit_no_new_subterms:
  assumes "bexpands_nowit bs' b" "b' ∈ bs'" "b ≠ []" 
  assumes "no_new_subterms b"
  shows "no_new_subterms (b' @ b)"
  using assms unfolding no_new_subterms_def
  by (simp add: bexpands_nowit_wits_eq bexpands_nowit_subterms_branch_eq[OF assms(1,2)])

lemma bexpands_wit_no_new_subterms:
  assumes "bexpands_wit t1 t2 x bs' b" "b ≠ []" "b' ∈ bs'"
  assumes "no_new_subterms b"
  shows "no_new_subterms (b' @ b)"
  using assms
  apply(induction rule: bexpands_wit.induct)
  apply(auto simp: subterms_branch_simps
                   subterms_term_subterms_atom_trans subterms_term_subterms_fm_trans
             elim: no_new_subtermsD
             intro!: no_new_subterms_casesI)
  done

lemma bexpands_no_new_subterms:
  assumes "bexpands bs' b" "b ≠ []" "b' ∈ bs'"
  assumes "no_new_subterms b"
  shows "no_new_subterms (b' @ b)"
  using assms
  apply(cases rule: bexpands.cases)
  using bexpands_nowit_no_new_subterms bexpands_wit_no_new_subterms by metis+

lemma expandss_no_new_subterms:
  assumes "expandss b' b" "b ≠ []" "no_new_subterms b"
  shows "no_new_subterms b'"
  using assms
  apply(induction b' b rule: expandss.induct)
  using expandss_suffix suffix_bot.extremum_uniqueI
  using lexpands_no_new_subterms bexpands_no_new_subterms
  by blast+

lemmas subterms_branch_subterms_fm_lastI =
  subterms_branch_subterms_subterms_fm_trans[OF _ subterms_refl]


subsection ‹‹wits_subterms››

definition wits_subterms :: "'a branch ⇒ 'a pset_term set" where
  "wits_subterms b ≡ Var ` wits b ∪ subterms (last b)"

lemma subterms_branch_eq_if_no_new_subterms:
  assumes "no_new_subterms b" "b ≠ []"
  shows "subterms_branch b = wits_subterms b"
  using assms no_new_subtermsD[OF assms(1)]
proof -
  note simps = wits_def no_new_subterms_def wits_subterms_def
    subterms_branch_simps vars_branch_simps
  with assms show ?thesis
    by (auto simp: simps vars_fm_subs_subterms_fm
                   vars_branch_subs_subterms_branch[unfolded image_subset_iff]
             intro: subterms_branch_subterms_fm_lastI)
qed

lemma wits_subterms_last_disjnt: "Var ` wits b ∩ subterms (last b) = {}"
  by (auto simp: wits_def intro!: mem_vars_fm_if_mem_subterms_fm)

section ‹Completeness of the Calculus›

subsection ‹Proof of Lemma 2›

fun is_literal :: "'a fm ⇒ bool" where
  "is_literal (Atom _) = True"
| "is_literal (Neg (Atom _)) = True"
| "is_literal _ = False"

lemma lexpands_no_wits_if_not_literal:
  defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
  assumes "lexpands b' b" "b ≠ []"
  assumes "P b"
  shows "P (b' @ b)"
  using assms(2-) lexpands_wits_eq[OF assms(2,3)]
  by (induction rule: lexpands_induct) (auto simp: disjoint_iff P_def)

lemma bexpands_nowit_no_wits_if_not_literal:
  defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
  assumes "bexpands_nowit bs' b" "b' ∈ bs'" "b ≠ []"
  assumes "P b"
  shows "P (b' @ b)"
  using assms(2-)
  by (induction rule: bexpands_nowit.induct)
     (auto simp: Int_def P_def wits_def vars_fm_vars_branchI)

lemma bexpands_wit_no_wits_if_not_literal:
  defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
  assumes "bexpands_wit t1 t2 x bs' b" "b' ∈ bs'" "b ≠ []"
  assumes "P b"
  shows "P (b' @ b)"
  using assms(2-)
  by (induction rule: bexpands_wit.induct)
     (auto simp: Int_def P_def wits_def vars_fm_vars_branchI)

lemma bexpands_no_wits_if_not_literal:
  defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
  assumes "bexpands bs' b" "b' ∈ bs'" "b ≠ []"
  assumes "P b"
  shows "P (b' @ b)"
  using assms(2-)
  apply(cases bs' b rule: bexpands_cases)
  using bexpands_wit_no_wits_if_not_literal bexpands_nowit_no_wits_if_not_literal
  using P_def by fast+

lemma expandss_no_wits_if_not_literal:
  defines "P ≡ (λb. ∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {})"
  assumes "expandss b' b" "b ≠ []"
  assumes "P b"
  shows "P b'"
  using assms(2-)
  apply (induction rule: expandss.induct)
  using lexpands_no_wits_if_not_literal bexpands_no_wits_if_not_literal
     apply (metis P_def expandss_suffix suffix_bot.extremum_uniqueI)+
  done

lemma lexpands_fm_pwits_eq:
  assumes "lexpands_fm b' b" "b ≠ []"
  assumes "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
  shows "pwits (b' @ b) = pwits b"
  using assms
  apply(induction rule: lexpands_fm.induct)
       apply(fastforce simp: pwits_def wits_def vars_branch_def)+
  done

lemma lexpands_un_pwits_eq:
  assumes "lexpands_un b' b" "b ≠ []"
  assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b.
    AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b"
  shows "pwits (b' @ b) = pwits b"
proof -
  note lexpands.intros(2)[OF assms(1)]
  note lexpands_wits_eq[OF this ‹b ≠ []›] 
  from assms this have "x ∈ pwits (b' @ b)" if "x ∈ pwits b" for x
    using that
    by (induction rule: lexpands_un.induct)
       (auto simp: wits_subterms_def pwitsD intro!: pwitsI)
  with lexpands_pwits_subs[OF ‹lexpands b' b› ‹b ≠ []›] show ?thesis
    by auto
qed

lemma lexpands_int_pwits_eq:
  assumes "lexpands_int b' b" "b ≠ []"
  assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b.
    AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b"
  shows "pwits (b' @ b) = pwits b"
proof -
  note lexpands.intros(3)[OF assms(1)]
  note lexpands_wits_eq[OF this ‹b ≠ []›] 
  from assms this have "x ∈ pwits (b' @ b)" if "x ∈ pwits b" for x
    using that
    by (induction rule: lexpands_int.induct)
       (auto simp: wits_subterms_def pwitsD intro!: pwitsI)
  with lexpands_pwits_subs[OF ‹lexpands b' b› ‹b ≠ []›] show ?thesis
    by auto
qed

lemma lexpands_diff_pwits_eq:
  assumes "lexpands_diff b' b" "b ≠ []"
  assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b.
    AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b"
  shows "pwits (b' @ b) = pwits b"
proof -
  note lexpands.intros(4)[OF assms(1)]
  note lexpands_wits_eq[OF this ‹b ≠ []›] 
  from assms this have "x ∈ pwits (b' @ b)" if "x ∈ pwits b" for x
    using that
    by (induction rule: lexpands_diff.induct)
       (auto simp: wits_subterms_def pwitsD intro!: pwitsI)
  with lexpands_pwits_subs[OF ‹lexpands b' b› ‹b ≠ []›] show ?thesis
    by auto
qed

lemma bexpands_nowit_pwits_eq:
  assumes "bexpands_nowit bs' b" "b' ∈ bs'" "b ≠ []"
  assumes "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
  shows "pwits (b' @ b) = pwits b"
  using assms
proof -
  from assms have "x ∈ pwits (b' @ b)" if "x ∈ pwits b" for x
    using that bexpands_nowit_wits_eq[OF assms(1-3)]
    by (induction rule: bexpands_nowit.induct)
       (intro pwitsI; fastforce simp: pwitsD)+
  moreover from assms have "pwits (b' @ b) ⊆ pwits b"
    unfolding pwits_def
    using bexpands_nowit_wits_eq by fastforce
  ultimately show ?thesis by blast
qed

lemma bexpands_wit_pwits_eq:
  assumes "bexpands_wit t1 t2 x bs' b" "b' ∈ bs'" "b ≠ []"
  shows "pwits (b' @ b) = insert x (pwits b)"
  using assms(2,3) bexpands_witD[OF assms(1)]
  unfolding pwits_def bexpands_wit_wits_eq[OF assms] 
  by (auto simp: vars_fm_vars_branchI)

lemma lemma_2_lexpands:
  defines "P ≡ (λb c t. AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b)"
  assumes "lexpands b' b" "b ≠ []"
  assumes "no_new_subterms b"
  assumes "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
  assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b. P b c t"
  shows "∀c ∈ pwits (b' @ b). ∀t ∈ wits_subterms (b' @ b). P (b' @ b) c t"
  using assms(2-6)
  using lexpands_wits_eq[OF assms(2,3)]
        lexpands_pwits_subs[OF assms(2,3)]
proof(induction rule: lexpands.induct)
  case (1 b' b)

  have "P (b' @ b) c t"
    if "∀φ ∈ set b'. vars φ ∩ wits (b' @ b) = {}"
    and "c ∈ pwits b" "t ∈ wits_subterms (b' @ b)" for c t
  proof -
    from that "1.prems"(5)
    have "∀φ ∈ set b'. φ ≠ AT (Var c =⇩s t) ∧ φ ≠ AT (t =⇩s Var c) ∧ φ ≠ AT (t ∈⇩s Var c)"
      by (auto simp: pwits_def disjoint_iff)
    with 1 that show ?thesis
      unfolding P_def wits_subterms_def
      by (metis Un_iff last_appendR set_append)
  qed
  moreover from "1"(1,4,6) have "∀φ ∈ set b'. vars φ ∩ wits (b' @ b) = {}"
    by (induction rule: lexpands_fm.induct) (auto simp: disjoint_iff)
  ultimately show ?case
    using 1 lexpands_fm_pwits_eq by blast
next
  case (2 b' b)
  then show ?case
    using lexpands_un_pwits_eq[OF "2"(1,2,5)[unfolded P_def]]
  proof(induction rule: lexpands_un.induct)
    case (4 s t1 t2 b)
    then have "t1 ⊔⇩s t2 ∈ subterms b"
      unfolding subterms_branch_def
      by (metis UN_iff UnI2 subterms_fm_simps(1) subterms_atom.simps(1) subterms_refl)
    with ‹no_new_subterms b› have "t1 ⊔⇩s t2 ∈ subterms (last b)"
      using no_new_subtermsD by blast
    then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 4 show ?case
      by (auto simp: wits_subterms_def P_def subterms_branch_simps pwitsD(1))
  next
    case (5 s t1 t2 b)
    then have "t1 ⊔⇩s t2 ∈ subterms b"
      unfolding subterms_branch_def
      by (metis UN_iff UnI2 subterms_fm_simps(1) subterms_atom.simps(1) subterms_refl)
    with ‹no_new_subterms b› have "t1 ⊔⇩s t2 ∈ subterms (last b)"
      using no_new_subtermsD by blast
    then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 5 show ?case
      by (auto simp: wits_subterms_def P_def subterms_branch_simps pwitsD(1))
  qed (auto simp: wits_subterms_def P_def)
next
  case (3 b' b)
  then show ?case
    using lexpands_int_pwits_eq[OF "3"(1,2,5)[unfolded P_def]]
  proof(induction rule: lexpands_int.induct)
    case (1 s t1 t2 b)
    then have "t1 ⊓⇩s t2 ∈ subterms b"
      unfolding subterms_branch_def
      by (metis UN_iff UnI2 subterms_fm_simps(1) subterms_atom.simps(1) subterms_refl)
    with ‹no_new_subterms b› have "t1 ⊓⇩s t2 ∈ subterms (last b)"
      using no_new_subtermsD by blast
    then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 1 show ?case
      by (auto simp: wits_subterms_def P_def subterms_branch_simps pwitsD(1))
  next
    case (6 s t1 b t2)
    then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 6 show ?case
      by (auto simp: wits_subterms_def P_def subterms_branch_simps pwitsD(1))
  qed (auto simp: wits_subterms_def P_def)
next
  case (4 b' b)
  then show ?case
    using lexpands_diff_pwits_eq[OF "4"(1,2,5)[unfolded P_def]]
  proof(induction rule: lexpands_diff.induct)
    case (1 s t1 t2 b)
    then have "t1 -⇩s t2 ∈ subterms b"
      unfolding subterms_branch_def
      by (metis UN_iff UnI2 subterms_fm_simps(1) subterms_atom.simps(1) subterms_refl)
    with ‹no_new_subterms b› have "t1 -⇩s t2 ∈ subterms (last b)"
      using no_new_subtermsD by blast
    then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 1 show ?case
      by (auto simp: wits_subterms_def P_def subterms_branch_simps dest: pwitsD(1))
  next
    case (4 s t1 t2 b)
    then have "t1 -⇩s t2 ∈ subterms b"
      unfolding subterms_branch_def
      by (metis AF_mem_subterms_branchD(2) subterms_branch_def)
    with ‹no_new_subterms b› have "t1 -⇩s t2 ∈ subterms (last b)"
      using no_new_subtermsD by blast
    then have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 4 show ?case
      by (auto simp: wits_subterms_def P_def subterms_branch_simps dest: pwitsD(1))
  qed (auto simp: wits_subterms_def P_def)
next
  case (5 b' b)
  then show ?case
  proof(induction rule: lexpands_single.induct)
    case (2 s t b)
    then have "Single t ∈ subterms b"
      by (auto intro: subterms_branch_subterms_atomI)
    with 2 have "t ∈ subterms (last b)"
      by (metis subterms_fmD(7) no_new_subtermsD(5))
    then have "∀c ∈ pwits b. Var c ≠ t"
      unfolding pwits_def wits_def
      using wits_def wits_subterms_last_disjnt by fastforce
    with ‹t ∈ subterms (last b)› show ?case
      using 2
      unfolding P_def
      by (auto simp: wits_subterms_last_disjnt[unfolded disjoint_iff] wits_subterms_def subsetD
               dest: pwitsD(2))
  qed (auto simp: wits_subterms_def P_def)
next
  case (6 b' b)
  then have "no_new_subterms (b' @ b)" "b' @ b ≠ []"
    using lexpands_no_new_subterms[OF lexpands.intros(6)] by blast+
  note subterms_branch_eq_if_no_new_subterms[OF this]
  with 6 show ?case
  proof(induction rule: lexpands_eq_induct')
    case (subst t1 t2 t1' t2' p l b)
    then have "t1' ∈ subterms b"
      using AT_eq_subterms_branchD by blast
    then show ?case unfolding P_def
    proof(safe, goal_cases)
      case (1 c x)
      with subst have [simp]: "p"
        by (cases p) (simp add: P_def wits_subterms_def; blast)+
      from 1 subst have "(Var c =⇩s x) = subst_tlvl t1' t2' l"
        by (simp add: P_def wits_subterms_def; blast)
      with 1 subst consider
        (refl) "l = (t1' =⇩s t1')" "t2' = Var c" "x = Var c"
        | (t1'_left) "l = (Var c =⇩s t1')" "t2' = x"
        | (t1'_right) "l = (t1' =⇩s x)" "t2' = Var c"
        apply(cases "(t1', t2', l)" rule: subst_tlvl.cases)
        by (auto split: if_splits)
      then show ?case
        apply(cases)
        by (use 1 subst subterms_branch_eq_if_no_new_subterms in ‹(simp add: P_def; blast)+›)
    next
      case (2 c x)
      with subst have [simp]: "p"
        by (cases p) (simp add: P_def wits_subterms_def; blast)+
      from 2 subst have "(x =⇩s Var c) = subst_tlvl t1' t2' l"
        by (simp add: P_def wits_subterms_def; blast)
      with 2 subst consider
        (refl) "l = (t1' =⇩s t1')" "t2' = Var c" "x = Var c"
        | (t1_left) "l = (t1' =⇩s Var c)" "t2' = x"
        | (t1_right) "l = (x =⇩s t1')" "t2' = Var c"
        apply(cases "(t1', t2', l)" rule: subst_tlvl.cases)
        by (auto split: if_splits)
      then show ?case
        apply(cases)
        by (use 2 subst subterms_branch_eq_if_no_new_subterms in ‹(simp add: P_def; blast)+›)
    next
      case (3 c x)
      with subst have [simp]: "p"
        by (cases p) (simp add: P_def wits_subterms_def; blast)+
      from 3 subst have "(x ∈⇩s Var c) = subst_tlvl t1' t2' l"
        by (simp add: P_def wits_subterms_def; blast)
      with 3 subst consider
        (refl) "l = (t1' ∈⇩s t1')" "t2' = Var c" "x = Var c"
        | (t1_left) "l = (t1' ∈⇩s Var c)" "t2' = x"
        | (t1_right) "l = (x ∈⇩s t1')" "t2' = Var c"
        apply(cases "(t1', t2', l)" rule: subst_tlvl.cases)
        by (auto split: if_splits)
      then show ?case
        apply(cases)
        by (use 3 subst subterms_branch_eq_if_no_new_subterms in ‹(simp add: P_def; blast)+›)
    qed
  next
    case (neq s t s' b)
    then show ?case
      using P_def by (simp add: wits_subterms_def) blast
  qed
qed

lemma lemma_2_bexpands:
  defines "P ≡ (λb c t. AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b
                      ∧ AT (t ∈⇩s Var c) ∉ set b)"
  assumes "bexpands bs' b" "b' ∈ bs'" "b ≠ []"
  assumes "no_new_subterms b"
  assumes "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
  assumes "∀c ∈ pwits b. ∀t ∈ wits_subterms b. P b c t"
  shows "∀c ∈ pwits (b' @ b). ∀t ∈ wits_subterms (b' @ b). P (b' @ b) c t"
  using assms(2-) bexpands_no_new_subterms[OF assms(2,4,3,5)]
proof(induction rule: bexpands.induct)
  case (1 bs' b)
  then show ?case
    using bexpands_nowit_wits_eq[OF "1"(1-3)] bexpands_nowit_pwits_eq[OF "1"(1-3,5)]
  proof(induction rule: bexpands_nowit.induct)
    case (1 p q b)
    then show ?case
      unfolding P_def wits_subterms_def
      by (fastforce dest: pwitsD)
  next
    case (2 p q b)
    then show ?case
      unfolding P_def wits_subterms_def
      by (fastforce dest: pwitsD)
  next
    case (3 s t1 t2 b)
    then have "t1 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 3 show ?case
      unfolding P_def wits_subterms_def
      by (fastforce simp: vars_branch_simps dest: pwitsD)
  next
    case (4 s t1 b t2)
    then have "t2 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 4 show ?case
      unfolding P_def wits_subterms_def
      by (fastforce simp: vars_branch_simps dest: pwitsD)
  next
    case (5 s t1 b t2)
    then have "t2 ∉ Var ` wits b"
      by (meson disjoint_iff wits_subterms_last_disjnt subterms_fmD)+
    with 5 show ?case
      unfolding P_def wits_subterms_def
      by (fastforce simp: vars_branch_simps dest: pwitsD)
  qed
next
  case (2 t1 t2 x bs b)
  from bexpands_witD[OF "2"(1)] have "t1 ∉ Var ` wits b" "t2 ∉ Var ` wits b"
    by (meson disjoint_iff_not_equal wits_subterms_last_disjnt)+
  then have not_in_pwits: "t1 ∉ Var ` pwits b" "t2 ∉ Var ` pwits b"
    unfolding pwits_def by auto
  with bexpands_witD[OF "2"(1)] "2"(2-) show ?case
    unfolding P_def wits_subterms_def
    unfolding bexpands_wit_pwits_eq[OF "2"(1-3)] bexpands_wit_wits_eq[OF "2"(1-3)]
    by safe (auto simp: vars_fm_vars_branchI[where ?x=x and ?b=b])
qed

lemma subterms_branch_eq_if_wf_branch:
  assumes "wf_branch b"
  shows "subterms_branch b = wits_subterms b"
proof -
  from assms obtain φ where "expandss b [φ]"
    unfolding wf_branch_def by blast
  then have "no_new_subterms [φ]"
    unfolding no_new_subterms_def wits_def
    by (simp add: subterms_branch_simps)
  with ‹expandss b [φ]› have "no_new_subterms b"
    using expandss_no_new_subterms by blast
  with ‹expandss b [φ]› assms show ?thesis
    by (intro subterms_branch_eq_if_no_new_subterms) simp_all
qed

lemma
  assumes "wf_branch b"
  shows no_new_subterms_if_wf_branch: "no_new_subterms b"
    and no_wits_if_not_literal_if_wf_branch:
          "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
proof -
  from assms obtain φ where "expandss b [φ]"
    unfolding wf_branch_def by blast
  then have "no_new_subterms [φ]"
    by (auto simp: no_new_subterms_def wits_def vars_branch_simps subterms_branch_simps)
  from expandss_no_new_subterms[OF ‹expandss b [φ]› _ this] show "no_new_subterms b"
    by simp
  from expandss_no_wits_if_not_literal[OF ‹expandss b [φ]›]
  show "∀φ ∈ set b. ¬ is_literal φ ⟶ vars φ ∩ wits b = {}"
    unfolding wits_def by simp
qed

lemma lemma_2:
  assumes "wf_branch b"
  assumes "c ∈ pwits b"
  shows "AT (Var c =⇩s t) ∉ set b" "AT (t =⇩s Var c) ∉ set b" "AT (t ∈⇩s Var c) ∉ set b"
proof -
  from ‹wf_branch b› obtain φ where "expandss b [φ]"
    using wf_branch_def by blast
  have no_wits_if_not_literal: "∀φ ∈ set b'. ¬ is_literal φ ⟶ vars φ ∩ wits b' = {}"
    if "expandss b' [φ]" for b'
    using no_wits_if_not_literal_if_wf_branch that unfolding wf_branch_def by blast
  have no_new_subterms: "no_new_subterms b'" if "expandss b' [φ]" for b'
    using no_new_subterms_if_wf_branch that unfolding wf_branch_def by blast
  have "AT (Var c =⇩s t) ∉ set b ∧ AT (t =⇩s Var c) ∉ set b ∧ AT (t ∈⇩s Var c) ∉ set b"
    using ‹expandss b [φ]› assms(2)
  proof(induction b "[φ]" arbitrary: c t rule: expandss.induct)
    case 1
    then show ?case by simp
  next
    case (2 b1 b2)
    note lemma_2_lexpands[OF this(1) _
        no_new_subterms[OF this(3)] no_wits_if_not_literal[OF this(3)]]
    with 2 show ?case
      using wf_branch_def wf_branch_not_Nil subterms_branch_eq_if_wf_branch
      by (metis AT_eq_subterms_branchD(1,2) AT_mem_subterms_branchD(1) expandss.intros(2))
  next
    case (3 bs b2 b1)
    note lemma_2_bexpands[OF "3"(1) _ _
        no_new_subterms[OF "3"(3)] no_wits_if_not_literal[OF "3"(3)]]
    with 3 show ?case
      using wf_branch_def wf_branch_not_Nil subterms_branch_eq_if_wf_branch
      by (metis AT_eq_subterms_branchD(1,2) AT_mem_subterms_branchD(1) expandss.intros(3))
  qed
  then show "AT (Var c =⇩s t) ∉ set b" "AT (t =⇩s Var c) ∉ set b" "AT (t ∈⇩s Var c) ∉ set b"
    by safe
qed

subsection ‹Urelements›
  
definition "urelems b ≡ {x ∈ subterms b. ∃v. ∀φ ∈ set b. urelem' v φ x}"

lemma finite_urelems: "finite (urelems b)"
proof -
  have "urelems b ⊆ subterms b"
    unfolding urelems_def urelem_def by blast
  with finite_subset finite_subterms_branch show ?thesis
    by blast
qed

lemma urelems_subs_subterms: "urelems b ⊆ subterms b"
  unfolding urelems_def by blast

lemma is_Var_if_mem_urelems: "t ∈ urelems b ⟹ is_Var t"
  unfolding urelems_def subterms_branch_def
  using is_Var_if_urelem' by auto

lemma urelems_subs_vars: "urelems b ⊆ Var ` vars b"
proof
  fix t assume "t ∈ urelems b"
  with urelems_subs_subterms have "t ∈ subterms b"
    by blast
  moreover note is_Var_if_mem_urelems[OF ‹t ∈ urelems b›]
  then obtain x where "t = Var x"
    by (meson is_Var_def)
  ultimately have "x ∈ vars b"
    unfolding Un_vars_term_subterms_branch_eq_vars_branch[symmetric]
    by force
  with ‹t = Var x› show "t ∈ Var ` vars b"
    by blast
qed

lemma types_term_inf:
  assumes "v1 ⊢ t : l1" "v2 ⊢ t : l2"
  shows "inf v1 v2 ⊢ t : inf l1 l2"
  using assms
  apply(induction t arbitrary: l1 l2)
       apply(auto simp: inf_min elim!: types_pset_term_cases
                  intro: types_pset_term_intros' types_pset_term.intros(4-))
  done

lemma types_pset_atom_inf:
  fixes a :: "'a pset_atom"
  assumes "v1 ⊢ a" "v2 ⊢ a"
  shows "inf v1 v2 ⊢ a"
  using assms
  by (auto simp: types_pset_atom.simps) (metis inf_min min_Suc_Suc types_term_inf)+

lemma types_pset_fm_inf:
  fixes φ :: "'a pset_fm"
  assumes "v1 ⊢ φ" "v2 ⊢ φ"
  shows "inf v1 v2 ⊢ φ"
  using assms types_pset_atom_inf
  unfolding types_pset_fm_def by blast

lemma types_urelems:
  fixes b :: "'a branch"
  assumes "wf_branch b" "v ⊢ last b"
  obtains v' where "∀φ ∈ set b. v' ⊢ φ" "∀u ∈ urelems b. v' ⊢ u : 0"
proof -
  from assms have "expandss b [last b]"
    unfolding wf_branch_def by force

  define V where "V ≡ {v. (∀φ ∈ set b. v ⊢ φ) ∧ (∀x. x ∉ vars b ⟶ v x = 0)}"
  have "V ≠ {}"
  proof -
    from types_expandss[OF ‹expandss b [last b]›, simplified] ‹v ⊢ last b›
    obtain v where v: "∀φ ∈ set b. v ⊢ φ"
      unfolding vars_branch_simps by metis
    define v' where "v' ≡ λx. if x ∈ vars b then v x else 0"
    have "v' ⊢ φ ⟷ v ⊢ φ" if "φ ∈ set b" for φ :: "'a pset_fm"
      apply(intro types_pset_fm_if_on_vars_eq)
      using that vars_fm_vars_branchI unfolding v'_def by metis
    with v have "∀φ ∈ set b. v' ⊢ φ"
      by blast
    then have "v' ∈ V"
      unfolding V_def v'_def by simp
    then show ?thesis
      by blast
  qed
    
  define m_x where "m_x ≡ λx. ARG_MIN (λv. v x) v. v ∈ V"
  with ‹V ≠ {}› have m_x: "∀v ∈ V. m_x x x ≤ v x" "m_x x ∈ V" for x
    using arg_min_nat_le arg_min_natI by (metis ex_in_conv)+

  define M where "M ≡ Finite_Set.fold inf (SOME v. v ∈ V) (m_x ` vars b)"
  note finite_imageI[where ?h=m_x, OF finite_vars_branch[of b]]
  note M_inf_eq = Inf_fin.eq_fold[symmetric, OF this, of "SOME v. v ∈ V"]
  have M_leq: "M x ≤ v x" if "x ∈ vars b" "v ∈ V" for x v
  proof -
    from that have "m_x x ∈ m_x ` vars b"
      by blast
    then have "M = inf (m_x x) (⨅⇩f⇩i⇩n insert (SOME v. v ∈ V) (m_x ` vars b))"
      unfolding M_def M_inf_eq
      by (simp add: Inf_fin.in_idem finite_vars_branch)
    with m_x that show ?thesis
      by (simp add: inf.coboundedI1)
  qed
  moreover have "M ∈ V"
    unfolding M_def M_inf_eq using finite_vars_branch[of b]
  proof(induction rule: finite_induct)
    case empty
    with ‹V ≠ {}› show ?case
      by (simp add: some_in_eq)
  next
    case (insert x F)
    then have M'_eq: "⨅⇩f⇩i⇩n insert (SOME v. v ∈ V) (m_x ` insert x F)
      = inf (m_x x) (⨅⇩f⇩i⇩n insert (SOME v. v ∈ V) (m_x ` F))" (is "_ = ?M'")
      by (simp add: insert_commute)
    from types_pset_fm_inf insert have "∀φ ∈ set b. ?M' ⊢ φ"
      using V_def m_x(2) by blast
    moreover have "(inf w v) x = 0" if "x ∉ vars b" "w ∈ V" "v ∈ V" for w v
      using that by (simp add: V_def)
    with "insert.IH" m_x(2) have "∀x. x ∉ vars b ⟶ ?M' x = 0"
      by (simp add: V_def)
    ultimately have "?M' ∈ V"
      using V_def by blast
    with M'_eq show ?case
      by metis
  qed
  moreover have "M ⊢ u : 0" if "u ∈ urelems b" for u
  proof -
    from that obtain v where v: "∀φ ∈ set b. urelem' v φ u"
      unfolding urelems_def by blast
    define v' where "v' ≡ λx. if x ∈ vars b then v x else 0"
    have "v' ⊢ φ ⟷ v ⊢ φ" if "φ ∈ set b" for φ :: "'a pset_fm"
      apply(intro types_pset_fm_if_on_vars_eq)
      using that vars_fm_vars_branchI unfolding v'_def by metis
    with v have "∀φ ∈ set b. v' ⊢ φ"
      by blast
    then have "v' ∈ V"
      unfolding V_def v'_def by auto
    moreover obtain uv where uv: "u = Var uv"
      using v is_Var_if_urelem' wf_branch_not_Nil[OF ‹wf_branch b›]
      by (metis is_Var_def last_in_set)
    then have "v' ⊢ u : 0"
      using v  wf_branch_not_Nil[OF ‹wf_branch b›, THEN last_in_set]
      unfolding v'_def
      by (auto elim!: types_pset_term_cases(2) intro!: types_pset_term_intros'(2))
    ultimately show "M ⊢ u : 0"
      using M_leq[where ?v=v'] ‹M ∈ V›[unfolded V_def] unfolding uv
      by (fastforce elim!: types_pset_term_cases(2) intro!: types_pset_term_intros'(2))
  qed
  ultimately show ?thesis
    using that unfolding V_def by auto
qed

lemma mem_urelems_if_urelem_last:
  assumes "wf_branch b"
  assumes "urelem (last b) x" "x ∈ subterms (last b)"
  shows "x ∈ urelems b"
proof -
  from assms have "x ∈ subterms b"
    unfolding subterms_branch_def by auto
  moreover note urelem_invar_if_wf_branch[OF assms]
  ultimately show ?thesis
    unfolding urelems_def urelem_def by blast
qed

lemma not_urelem_comps_if_compound:
  assumes "f t1 t2 ∈ subterms b" "f ∈ {(⊓⇩s), (⊔⇩s), (-⇩s)}"
  shows "t1 ∉ urelems b" "t2 ∉ urelems b"
proof -
  from assms obtain φ where "φ ∈ set b" "f t1 t2 ∈ subterms φ"
    unfolding subterms_branch_def by auto
  note not_urelem_comps_if_compound[of f t1 t2, OF this(2) assms(2)]
  with ‹φ ∈ set b› show "t1 ∉ urelems b" "t2 ∉ urelems b"
    unfolding urelems_def urelem_def by auto
qed

subsection ‹Realization of an Open Branch›

definition "base_vars b ≡ Var ` pwits b ∪ urelems b"

lemma finite_base_vars: "finite (base_vars b)"
  unfolding base_vars_def finite_Un
  using finite_pwits[THEN finite_imageI] finite_urelems by blast

lemma pwits_subs_base_vars:
  shows "Var ` pwits b ⊆ base_vars b"
  unfolding base_vars_def
  by blast

lemma base_vars_subs_vars: "base_vars b ⊆ Var ` vars b"
  unfolding base_vars_def pwits_def wits_def
  using urelems_subs_vars by blast

definition subterms' :: "'a branch ⇒ 'a pset_term set" where
  "subterms' b ≡ subterms b - base_vars b"

definition bgraph :: "'a branch ⇒ ('a pset_term, 'a pset_term × 'a pset_term) pre_digraph" where
  "bgraph b ≡
    let
      vs = base_vars b ∪ subterms' b
    in
      ⦇ verts = vs,
        arcs = {(s, t). AT (s ∈⇩s t) ∈ set b},
        tail = fst,
        head = snd ⦈"

lemma base_vars_Un_subterms'_eq_subterms:
  "base_vars b ∪ subterms' b = subterms b"
  unfolding subterms'_def
  using base_vars_subs_vars vars_branch_subs_subterms_branch by fastforce

lemma finite_base_vars_Un_subterms': "finite (base_vars b ∪ subterms' b)"
  unfolding base_vars_Un_subterms'_eq_subterms
  using finite_subterms_branch .

lemma verts_bgraph: "verts (bgraph b) = base_vars b ∪ subterms' b"
  unfolding bgraph_def Let_def by simp

lemma verts_bgraph_eq_subterms: "verts (bgraph b) = subterms b"
  unfolding verts_bgraph base_vars_Un_subterms'_eq_subterms ..

lemma finite_subterms': "finite (subterms' b)"
  unfolding subterms'_def using finite_base_vars finite_subterms_branch
  by auto

lemma base_vars_subterms'_disjnt: "base_vars b ∩ subterms' b = {}"
  unfolding subterms'_def by fastforce

lemma wits_subterms_eq_base_vars_Un_subterms':
  assumes "wf_branch b"
  shows "wits_subterms b = base_vars b ∪ subterms' b"
  unfolding subterms_branch_eq_if_wf_branch[OF assms, symmetric] subterms'_def
  using base_vars_subs_vars vars_branch_subs_subterms_branch
  by fastforce

lemma in_subterms'_if_AT_mem_in_branch:
  assumes "wf_branch b"
  assumes "AT (s ∈⇩s t) ∈ set b"
  shows "s ∈ base_vars b ∪ subterms' b"
    and "t ∈ base_vars b ∪ subterms' b"
  using assms
  using wits_subterms_eq_base_vars_Un_subterms' AT_mem_subterms_branchD
  using subterms_branch_eq_if_wf_branch
  by blast+

lemma in_subterms'_if_AF_mem_in_branch:
  assumes "wf_branch b"
  assumes "AF (s ∈⇩s t) ∈ set b"
  shows "s ∈ base_vars b ∪ subterms' b"
    and "t ∈ base_vars b ∪ subterms' b"
  using assms
  using wits_subterms_eq_base_vars_Un_subterms' AF_mem_subterms_branchD
  using subterms_branch_eq_if_wf_branch
  by blast+

lemma in_subterms'_if_AT_eq_in_branch:
  assumes "wf_branch b"
  assumes "AT (s =⇩s t) ∈ set b"
  shows "s ∈ base_vars b ∪ subterms' b"
    and "t ∈ base_vars b ∪ subterms' b"
  using assms
  using wits_subterms_eq_base_vars_Un_subterms' AT_eq_subterms_branchD
  using subterms_branch_eq_if_wf_branch
  by blast+

lemma in_subterms'_if_AF_eq_in_branch:
  assumes "wf_branch b"
  assumes "AF (s =⇩s t) ∈ set b"
  shows "s ∈ base_vars b ∪ subterms' b"
    and "t ∈ base_vars b ∪ subterms' b"
  using assms
  using wits_subterms_eq_base_vars_Un_subterms' AF_eq_subterms_branchD
  using subterms_branch_eq_if_wf_branch
  by blast+

lemma mem_subterms_fm_last_if_mem_subterms_branch:
  assumes "wf_branch b"
  assumes "t ∈ subterms b" "¬ is_Var t"
  shows "t ∈ subterms (last b)"
  using assms
  unfolding subterms_branch_eq_if_wf_branch[OF ‹wf_branch b›]
  unfolding subterms'_def wits_subterms_def by force

locale open_branch =
  fixes b :: "'a branch"
  assumes wf_branch: "wf_branch b" and bopen: "bopen b" and types: "∃v. v ⊢ last b"
      and infinite_vars: "infinite (UNIV :: 'a set)"
begin

sublocale fin_digraph_bgraph: fin_digraph "bgraph b"
proof
  show "finite (verts (bgraph b))"
    using finite_base_vars finite_subterms'
    by (auto simp: bgraph_def Let_def)

  show "finite (arcs (bgraph b))"
    using [[simproc add: finite_Collect]]
    by (auto simp: bgraph_def Let_def inj_on_def intro!: finite_vimageI)

qed (use in_subterms'_if_AT_mem_in_branch[OF wf_branch]
      in ‹(fastforce simp: bgraph_def Let_def)+›)

lemma member_seq_if_cas:
  "fin_digraph_bgraph.cas t1 is t2
  ⟹ member_seq t1 (map (λe. tail (bgraph b) e ∈⇩s head (bgraph b) e) is) t2"
  by (induction "is" arbitrary: t1 t2) auto

lemma member_cycle_if_cycle:
  "fin_digraph_bgraph.cycle c
  ⟹ member_cycle (map (λe. tail (bgraph b) e ∈⇩s head (bgraph b) e) c)"
  unfolding pre_digraph.cycle_def
  by (cases c) (auto simp: member_seq_if_cas)

sublocale dag_bgraph: dag "bgraph b"
proof(unfold_locales, goal_cases)
  case (1 e)
  show ?case
  proof
    assume "tail (bgraph b) e = head (bgraph b) e"
    then obtain t where "AT (t ∈⇩s t) ∈ set b"
      using 1 unfolding bgraph_def Let_def by auto
    then have "member_cycle [(t ∈⇩s t)]" "(t ∈⇩s t) ∈ Atoms (set b)"
      by (auto simp: Atoms_def)
    then have "bclosed b"
      using memberCycle by (metis empty_iff empty_set set_ConsD subsetI)
    with bopen show "False"
      by blast
  qed
next
  case (2 e1 e2)
  then show ?case
    by (auto simp: bgraph_def Let_def arc_to_ends_def)
next
  case 3
  show ?case
  proof
    assume "∃c. fin_digraph_bgraph.cycle c"
    then obtain c where "fin_digraph_bgraph.cycle c"
      by blast
    then have "member_cycle (map (λe. (tail (bgraph b) e ∈⇩s head (bgraph b) e)) c)"
      using member_cycle_if_cycle by blast
    moreover
    from ‹fin_digraph_bgraph.cycle c› have "set c ⊆ arcs (bgraph b)"
      by (meson fin_digraph_bgraph.cycle_def pre_digraph.awalk_def)
    then have "set (map (λe. (tail (bgraph b) e ∈⇩s head (bgraph b) e)) c) ⊆ Atoms (set b)"
      unfolding bgraph_def Let_def Atoms_def by auto
    ultimately have "bclosed b"
      using memberCycle by blast
    with bopen show False by blast
  qed
qed

definition I :: "'a pset_term ⇒ hf" where
  "I ≡ SOME f. inj_on f (subterms b)
             ∧ (∀p. hcard (f p) > 2 * card (base_vars b ∪ subterms' b))"


lemma (in -) Ex_set_family:
  assumes "finite P"
  shows "∃I. inj_on I P ∧ (∀p. hcard (I p) ≥ n)"
proof -
  from ‹finite P› obtain ip where ip: "bij_betw ip P {..<card P}"
    using to_nat_on_finite by blast
  let ?I = "ord_of o ((+) n) o ip"
  from ip have "inj_on ?I P"
    by (auto simp: inj_on_def bij_betw_def)
  moreover have "hcard (?I p) ≥ n" for p
    by simp
  ultimately show ?thesis
    by auto
qed

lemma
  shows inj_on_I: "inj_on I (subterms b)"
    and card_I: "hcard (I p) > 2 * card (base_vars b ∪ subterms' b)"
proof -
  have "∃f. inj_on f (subterms b)
    ∧ (∀p. hcard (f p) > 2 * card (base_vars b ∪ subterms' b))"
    using Ex_set_family finite_subterms_branch by (metis less_eq_Suc_le)
  from someI_ex[OF this]
  show "inj_on I (subterms b)"
       "hcard (I p) > 2 * card (base_vars b ∪ subterms' b)"
    unfolding I_def by blast+
qed

lemma
  shows inj_on_base_vars_I: "inj_on I (base_vars b)"
    and inj_on_subterms'_I: "inj_on I (subterms' b)"
proof -
  from base_vars_Un_subterms'_eq_subterms have
    "base_vars b ⊆ subterms b" "subterms' b ⊆ subterms b"
    using wf_branch_not_Nil[OF wf_branch] by blast+
  with inj_on_I show "inj_on I (base_vars b)" "inj_on I (subterms' b)"
    unfolding inj_on_def by blast+
qed

definition "eq ≡ symcl ({(s, t). AT (s =⇩s t) ∈ set b}⇧=)"

lemma refl_eq: "refl eq"
  unfolding eq_def symcl_def refl_on_def by auto

lemma trans_eq:
  assumes "lin_sat b" shows "trans eq"
proof
  fix s t u assume assms: "(s, t) ∈ eq" "(t, u) ∈ eq"
  have "(s, u) ∈ eq" if "s ≠ t" "t ≠ u"
  proof -
    from that assms have
      s_t: "AT (s =⇩s t) ∈ set b ∨ AT (t =⇩s s) ∈ set b" and
      t_u: "AT (t =⇩s u) ∈ set b ∨ AT (u =⇩s t) ∈ set b"
      unfolding eq_def symcl_def by fastforce+
    note intros = lexpands_eq.intros(1,3)[
        THEN lexpands.intros(6), THEN ‹lin_sat b›[THEN lin_satD]]
    note intros' = intros[where ?x="AT (s =⇩s u)"] intros[where ?x="AT (u =⇩s s)"]
    from s_t t_u that have "AT (s =⇩s u) ∈ set b ∨ AT (u =⇩s s) ∈ set b"
      by safe (simp_all add: intros')
    then show ?thesis
      unfolding eq_def symcl_def by auto
  qed
  with assms show "(s, u) ∈ eq"
    by (cases "s ≠ t ∧ t ≠ u") (auto simp: eq_def)
qed

lemma sym_eq: "sym eq"
  unfolding eq_def symcl_def sym_def by auto

lemma equiv_eq: "lin_sat b ⟹ equiv UNIV eq"
  by (rule equivI) (use refl_eq trans_eq sym_eq in safe)

lemma not_dominated_if_pwits:
  assumes "x ∈ Var ` pwits b" shows "¬ s →⇘bgraph b⇙ x"
proof -
  from assms obtain x' where "x = Var x'" "x' ∈ pwits b"
    by blast
  from lemma_2(3)[OF wf_branch this(2)] this(1) show "¬ s →⇘bgraph b⇙ x"
    unfolding arcs_ends_def arc_to_ends_def by (auto simp: bgraph_def)
qed

lemma parents_empty_if_pwits:
  assumes "x ∈ Var ` pwits b" shows "parents (bgraph b) x = {}"
  using not_dominated_if_pwits[OF assms] unfolding bgraph_def by simp

lemma not_AT_mem_if_urelem:
  assumes "t ∈ urelems b"
  shows "AT (s ∈⇩s t) ∉ set b"
proof
  assume "AT (s ∈⇩s t) ∈ set b"
  with assms urelem_invar_if_wf_branch[OF wf_branch] have "urelem (AT (s ∈⇩s t)) t"
    by (meson types types_urelems urelem_def wf_branch)
  then show False
    unfolding urelem_def
    by (auto dest!: types_fmD simp: types_pset_atom.simps dest: types_term_unique)
qed

lemma not_dominated_if_urelems:
  assumes "t ∈ urelems b"
  shows "¬ s →⇘bgraph b⇙ t"
  using not_AT_mem_if_urelem[OF assms] unfolding bgraph_def by auto

lemma parents_empty_if_urelems:
  assumes "t ∈ urelems b"
  shows "parents (bgraph b) t = {}"
  using not_dominated_if_urelems[OF assms] by simp

lemma not_dominated_if_base_vars:
  assumes "x ∈ base_vars b"
  shows "¬ s →⇘bgraph b⇙ x"
  using assms not_dominated_if_urelems not_dominated_if_pwits
  unfolding base_vars_def by blast

lemma parents_empty_if_base_vars:
  assumes "x ∈ base_vars b"
  shows "parents (bgraph b) x = {}"
  using not_dominated_if_base_vars[OF assms] by blast

lemma eq_class_subs_subterms: "eq `` {t} ⊆ {t} ∪ subterms b"
proof -
  have "eq - Id ⊆ subterms b × subterms b"
    by (auto simp: AT_eq_subterms_branchD eq_def symcl_def)
  then show "eq `` {t} ⊆ {t} ∪ subterms b"
    by blast
qed

lemma finite_eq_class: "finite (eq `` {x})"
  using eq_class_subs_subterms finite_subterms_branch
  using finite_subset by fastforce

lemma finite_I_image_eq_class: "finite (I ` eq `` {x})"
  using finite_eq_class by blast

context
begin

interpretation realisation "bgraph b" "base_vars b" "subterms' b" I eq
proof(unfold_locales)
  from base_vars_subterms'_disjnt show "base_vars b ∩ subterms' b = {}" .

  show "verts (bgraph b) = base_vars b ∪ subterms' b"
    unfolding bgraph_def by simp

  from not_dominated_if_base_vars show "⋀p t. p ∈ base_vars b ⟹ ¬ t →⇘bgraph b⇙ p" .
qed

lemmas realisation = realisation_axioms

lemma card_realisation:
  "hcard (realise t) ≤ 2 * card (subterms b)"
proof(induction t rule: realise.induct)
  case (1 x)
  then have "hcard (realise x) = card (realise ` parents (bgraph b) x ∪ I ` eq_class x)"
    using hcard_HF Zero_hf_def parents_empty_if_base_vars
    using finite_I_image_eq_class by force
  also have "… ≤ card (realise ` parents (bgraph b) x) + card (I ` eq_class x)"
    using card_Un_le by blast
  also have "… ≤ card (parents (bgraph b) x) + card (eq_class x)"
    using card_image_le[OF fin_digraph_bgraph.finite_parents]
    using card_image_le[OF finite_eq_class]
    by (metis add_le_mono)
  also have "… ≤ card (subterms b) + card (eq_class x)"
    using fin_digraph_bgraph.parents_subs_verts[unfolded verts_bgraph_eq_subterms]
    using card_mono[OF finite_subterms_branch]
    by (simp add: "1.hyps" not_dominated_if_base_vars)
  also have "… ≤ card (subterms b) + card ({x} ∪ subterms b)"
    apply (intro add_le_mono card_mono[where ?B="{x} ∪ subterms b"])
    using eq_class_subs_subterms finite_subterms_branch by auto
  also have "… ≤ 2 * card (subterms b)"
  proof -
    from 1 have "x ∈ subterms b"
      using "1.prems" verts_bgraph verts_bgraph_eq_subterms wf_branch_not_Nil[OF wf_branch]
      by blast
    then show ?thesis
      unfolding mult_2 by (metis insert_absorb insert_is_Un order_refl)
  qed
  finally show ?case .
next
  case (2 t)
  then have "hcard (realise t) = card (realise ` parents (bgraph b) t)"
    using hcard_HF[OF finite_realisation_parents] by simp
  also have "… ≤ card (parents (bgraph b) t)"
    using card_image_le by blast
  also have "… ≤ card (subterms b)"
    using fin_digraph_bgraph.parents_subs_verts wf_branch_not_Nil[OF wf_branch]
    unfolding verts_bgraph_eq_subterms
    by (metis card_mono fin_digraph_bgraph.finite_verts verts_bgraph_eq_subterms)
  finally show ?case
    unfolding base_vars_Un_subterms'_eq_subterms by auto
next
  case (3 t)
  then show ?case by simp
qed

lemma I_neq_realise: "I x ≠ realise y"
proof -
  note card_realisation[of y]
  moreover have "hcard (I x) > 2 * card (subterms b)"
    using card_I wf_branch
    by (simp add: subterms_branch_eq_if_wf_branch wits_subterms_eq_base_vars_Un_subterms')
  ultimately show ?thesis
    by (metis linorder_not_le)
qed

end

sublocale realisation "bgraph b" "base_vars b" "subterms' b" I eq
  rewrites "(⋀x y. I x ≠ realise y) ≡ Trueprop True"
       and "⋀P. (True ⟹ P) ≡ Trueprop P"
       and "⋀P Q. (True ⟹ PROP P ⟹ PROP Q) ≡ (PROP P ⟹ True ⟹ PROP Q)"
  using realisation I_neq_realise by simp_all

lemma eq_class_singleton_if_pwits:
  assumes "x ∈ Var ` pwits b" shows "eq_class x = {x}"
proof -
  from assms obtain x' where "x = Var x'" "x' ∈ pwits b"
    by blast
  have False if "eq_class x ≠ {x}"
  proof -
    have "x ∈ eq_class x"
      by (simp add: eq_def symcl_def)
    with that obtain y where "y ∈ eq_class x" "y ≠ x"
      by auto
    then have "AT (y =⇩s x) ∈ set b ∨ AT (x =⇩s y) ∈ set b"
      unfolding eq_def symcl_def by auto
    with lemma_2(1,2)[OF wf_branch ‹x' ∈ pwits b›] ‹x = Var x'› show False
      by blast
  qed
  with assms show ?thesis by blast
qed

lemma realise_pwits:
  "x ∈ Var ` pwits b ⟹ realise x = HF {I x}"
  unfolding realise.simps(1)[OF pwits_subs_base_vars[THEN subsetD]]
  by (auto simp: eq_class_singleton_if_pwits parents_empty_if_pwits)

lemma I_in_realise_if_base_vars[simp]:
  "s ∈ base_vars b ⟹ I s ❙∈ realise s"
  using refl_eq by (simp add: finite_I_image_eq_class refl_on_def)

lemma realise_neq_if_base_vars_and_subterms':
  assumes "s ∈ base_vars b" "t ∈ subterms' b"
  shows "realise s ≠ realise t"
proof -
  from assms have "I s ❙∉ realise t"
    using I_neq_realise by auto
  with I_in_realise_if_base_vars assms(1) show ?thesis
    by metis
qed

lemma AT_mem_branch_wits_subtermsD:
  assumes "AT (s ∈⇩s t) ∈ set b"
  shows "s ∈ wits_subterms b" "t ∈ wits_subterms b"
  using assms AT_mem_subterms_branchD subterms_branch_eq_if_wf_branch wf_branch by blast+

lemma AF_mem_branch_wits_subtermsD:
  assumes "AF (s ∈⇩s t) ∈ set b"
  shows "s ∈ wits_subterms b" "t ∈ wits_subterms b"
  using assms AF_mem_subterms_branchD subterms_branch_eq_if_wf_branch wf_branch by blast+

lemma AT_eq_branch_wits_subtermsD:
  assumes "AT (s =⇩s t) ∈ set b"
  shows "s ∈ wits_subterms b" "t ∈ wits_subterms b"
  using assms AT_eq_subterms_branchD subterms_branch_eq_if_wf_branch wf_branch by blast+

lemma AF_eq_branch_wits_subtermsD:
  assumes "AF (s =⇩s t) ∈ set b"
  shows "s ∈ wits_subterms b" "t ∈ wits_subterms b"
  using assms AF_eq_subterms_branchD subterms_branch_eq_if_wf_branch wf_branch by blast+

lemma realisation_if_AT_mem:
  assumes "AT (s ∈⇩s t) ∈ set b"
  shows "realise s ❙∈ realise t"
proof -
  from assms have "t ∈ base_vars b ∪ subterms' b"
    using in_subterms'_if_AT_mem_in_branch(2) wf_branch by blast
  moreover from assms have "s →⇘bgraph b⇙ t"
    unfolding arcs_ends_def arc_to_ends_def by (simp add: bgraph_def)
  ultimately show ?thesis
    by (cases t rule: realise.cases) auto
qed

lemma AT_eq_urelems_subterms'_cases:
  assumes "AT (s =⇩s t) ∈ set b"
  obtains (urelems) "s ∈ urelems b" "t ∈ urelems b" |
          (subterms') "s ∈ subterms' b" "t ∈ subterms' b"
proof -
  from types obtain v where "v ⊢ last b"
    by blast
  with types_urelems wf_branch obtain v'
    where v': "∀φ ∈ set b. v' ⊢ φ" "∀u ∈ urelems b. v' ⊢ u : 0"
    by blast
  with assms have "v' ⊢ AT (s =⇩s t)"
    by blast
  then obtain lst where lst: "v' ⊢ s : lst" "v' ⊢ t : lst"
    by (auto dest!: types_fmD(6) simp: types_pset_atom.simps)
  note mem_subterms = AT_eq_subterms_branchD[OF assms]
  with v' have "t ∈ urelems b" if "s ∈ urelems b"
    using that lst types_term_unique urelems_def by fastforce
  moreover from assms have "s ∉ Var ` pwits b" "t ∉ Var ` pwits b"
    using lemma_2(1,2)[OF wf_branch] by blast+
  moreover have "t ∈ subterms' b" if "s ∈ subterms' b"
  proof -
    have "s ∉ urelems b"
      using that B_T_partition_verts(1) unfolding base_vars_def by blast
    with v'(1) mem_subterms(1) have "¬ v' ⊢ s : 0"
      using urelems_def by blast
    with lst v'(2) have "t ∉ urelems b"
      using types_term_unique by metis
    with ‹t ∉ Var ` pwits b› ‹t ∈ subterms b› show "t ∈ subterms' b"
      by (simp add: base_vars_def subterms'_def)
  qed
  ultimately show ?thesis
    using that mem_subterms
    by (cases "s ∈ subterms' b") (auto simp: base_vars_def subterms'_def)
qed

lemma realisation_if_AT_eq:
  assumes "lin_sat b"
  assumes "AT (s =⇩s t) ∈ set b"
  shows "realise s = realise t"
proof -
  from assms(2) show ?thesis
  proof(cases rule: AT_eq_urelems_subterms'_cases)
    case urelems
    then have "s ∈ base_vars b" "t ∈ base_vars b"
      by (simp_all add: base_vars_def)
    moreover from assms have "(s, t) ∈ eq"
      unfolding eq_def symcl_def by blast
    then have "I ` eq_class s = I ` eq_class t"
      using equiv_eq[OF assms(1)] by (simp add: equiv_class_eq_iff)
    ultimately show ?thesis 
      using urelems by (simp add: parents_empty_if_urelems)
  next
    case subterms'
    have "False" if "realise s ≠ realise t"
    proof -
      from that have "hfset (realise s) ≠ hfset (realise t)"
        by (metis HF_hfset)
      then obtain a s' t' where
        a: "a ∈ realise ` parents (bgraph b) s'"
           "a ∉ realise ` parents (bgraph b) t'"
        and s'_t': "s' = s ∧ t' = t ∨ s' = t ∧ t' = s"
        using subterms' by auto blast+
      with subterms' have "s' ∈ subterms' b" "t' ∈ subterms' b"
        by auto
      with a obtain u where u: "a = realise u" "u →⇘bgraph b⇙ s'"
        using subterms' dominates_if_mem_realisation by auto
      then have "u ≠ s'"
        using dag_bgraph.adj_not_same by blast
      from u have "AT (u ∈⇩s s') ∈ set b"
        unfolding bgraph_def Let_def using dag_bgraph.adj_not_same by auto
      note lexpands_eq.intros(1,3)[OF assms(2) this, THEN lexpands.intros(6)]
      with ‹lin_sat b› s'_t' ‹u ≠ s'› have "AT (u ∈⇩s t') ∈ set b"
        unfolding lin_sat_def by (auto split: if_splits)
      from realisation_if_AT_mem[OF this] ‹a = realise u› have "a ❙∈ realise t'"
        by blast
      with a show False
        using ‹t' ∈ subterms' b› by simp
    qed
    then show ?thesis by blast
  qed
qed

lemma realise_base_vars_if_AF_eq:
  assumes "sat b"
  assumes "AF (x =⇩s y) ∈ set b"
  assumes "x ∈ base_vars b ∨ y ∈ base_vars b"
  shows "realise x ≠ realise y"
proof(cases "x ∈ base_vars b ∧ y ∈ base_vars b")
  case False
  with assms(3) show ?thesis
    using realise_neq_if_base_vars_and_subterms' I_in_realise_if_base_vars
    by (metis hempty_iff realise.elims)
next
  case True
  from assms bopen have "x ≠ y"
    using neqSelf by blast
  moreover from assms bopen have "AT (x =⇩s y) ∉ set b"
    using contr by blast
  moreover have "AT (y =⇩s x) ∉ set b"
  proof 
    assume "AT (y =⇩s x) ∈ set b"
    note lexpands_eq.intros(2)[OF this assms(2), THEN lexpands.intros(6)]
    with ‹sat b›[THEN satD(1), THEN lin_satD] have "AF (x =⇩s x) ∈ set b"
      by auto
    with bopen neqSelf show False
      by blast
  qed
  ultimately have "(x, y) ∉ eq"
    unfolding eq_def symcl_def by auto

  then have "x ∉ eq_class y"
    by (meson Image_singleton_iff symE sym_eq)
  then have "I x ∉ I ` eq_class y"
    using inj_on_I AF_eq_subterms_branchD[OF assms(2)]
    using eq_class_subs_subterms inj_onD by fastforce
  then have "I ` eq_class x ≠ I ` eq_class y"
    using refl_eq
    by (metis Image_singleton_iff UNIV_I imageI refl_onD)

  with ‹x ∈ base_vars b ∧ y ∈ base_vars b› show "realise x ≠ realise y"
    using hunion_hempty_left[unfolded Zero_hf_def]
    using inj_on_HF[THEN inj_onD] finite_I_image_eq_class
    by (force simp: parents_empty_if_base_vars)
qed

lemma Ex_AT_eq_mem_subterms_last_if_subterms':
  assumes "t ∈ subterms' b"
  obtains "t ∈ subterms (last b) - base_vars b"
  | t' where "t' ∈ subterms (last b) - base_vars b"
             "AT (t =⇩s t') ∈ set b ∨ AT (t' =⇩s t) ∈ set b"
proof(cases "t ∈ subterms (last b) - base_vars b")
  case False
  from assms have "t ∈ subterms b"
    using base_vars_Un_subterms'_eq_subterms by auto
  with False consider (t_base_vars) "t ∈ base_vars b" | (t_wits) "t ∈ Var ` wits b"
    using no_new_subterms_if_wf_branch[OF wf_branch]
    by (meson DiffI no_new_subterms_def)
  then show ?thesis
  proof cases
    case t_wits
    with ‹t ∈ subterms' b› have "t ∉ Var ` pwits b"
      unfolding subterms'_def base_vars_def by blast
    with t_wits obtain t' where t': "t' ∈ subterms (last b)"
      "AT (t =⇩s t') ∈ set b ∨ AT (t' =⇩s t) ∈ set b"
      unfolding pwits_def by blast
    with ‹t ∈ subterms' b› have "t' ∉ base_vars b"
      using AT_eq_urelems_subterms'_cases B_T_partition_verts(1)
      by (metis Un_iff base_vars_def disjoint_iff)
    with t' that show ?thesis
      by blast
  qed (use assms[unfolded subterms'_def] in blast)
qed
  

lemma realisation_if_AF_eq:
  assumes "sat b"
  assumes "AF (t1 =⇩s t2) ∈ set b"
  shows "realise t1 ≠ realise t2"
proof -
  note AF_eq_branch_wits_subtermsD[OF assms(2)]
  then consider
    (t1_base_vars) "t1 ∈ base_vars b" |
    (t2_base_vars) "t2 ∈ base_vars b" "t1 ∈ base_vars b ∪ subterms' b" |
    (subterms) "t1 ∈ subterms' b" "t2 ∈ subterms' b"
    by (metis UnE wf_branch wits_subterms_eq_base_vars_Un_subterms')
  then show ?thesis
  proof cases
    case t1_base_vars
    with assms show ?thesis
      using realise_base_vars_if_AF_eq by blast
  next
    case t2_base_vars
    with assms show ?thesis
      using realise_base_vars_if_AF_eq by blast
  next
    case subterms
    define Δ where "Δ ≡ {(t1, t2) ∈ subterms' b × subterms' b.
                            AF (t1 =⇩s t2) ∈ set b ∧ realise t1 = realise t2}"
    have "finite Δ"
    proof -
      have "Δ ⊆ subterms' b × subterms' b"
        unfolding Δ_def by auto
      moreover note finite_cartesian_product[OF finite_subterms' finite_subterms']
      ultimately show ?thesis
        using finite_subset by blast
    qed
    let ?h = "λ(t1, t2). min (height t1) (height t2)"
    have False if "Δ ≠ {}"
    proof -
      obtain t1 t2 where t1_t2: "(t1, t2) = arg_min_on ?h Δ"
        by (metis surj_pair)
      have "(t1, t2) ∈ Δ" "?h (t1, t2) = Min (?h ` Δ)"
      proof -
        from arg_min_if_finite(1)[OF ‹finite Δ› that] t1_t2 show "(t1, t2) ∈ Δ"
          by metis

        have "f (arg_min_on f S) = Min (f ` S)" if "finite S" "S ≠ {}"
          for f :: "('a pset_term × 'a pset_term) ⇒ nat" and S
          using arg_min_least[OF that] that
          by (auto intro!: Min_eqI[symmetric] intro: arg_min_if_finite(1)[OF that])
        from this[OF ‹finite Δ› that] t1_t2 show "?h (t1, t2) = Min (?h ` Δ)"
          by auto
      qed
      then have *: "t1 ∈ subterms' b" "t2 ∈ subterms' b"
        "AF (t1 =⇩s t2) ∈ set b" "realise t1 = realise t2"
        unfolding Δ_def by auto
      obtain t1' t2' where t1'_t2':
        "t1' ∈ subterms (last b) - base_vars b" "t2' ∈ subterms (last b) - base_vars b"
        "AF (t1' =⇩s t2') ∈ set b"
        "realise t1' = realise t1" "realise t2' = realise t2"
      proof -
        note Ex_AT_eq_mem_subterms_last_if_subterms'[OF ‹t1 ∈ subterms' b›]
        then obtain t1'' where
          "t1'' ∈ subterms (last b) - base_vars b" "AF (t1'' =⇩s t2) ∈ set b"
          "realise t1'' = realise t1"
        proof cases
          case (2 t1')
          from bopen neqSelf ‹AF (t1 =⇩s t2) ∈ set b› have "t1 ≠ t2"
            by blast
          with 2 ‹sat b›[THEN satD(1), THEN lin_satD] have "AF (t1' =⇩s t2) ∈ set b"
            using lexpands_eq.intros(2,4)[OF _ ‹AF (t1 =⇩s t2) ∈ set b›, THEN lexpands.intros(6)]
            by fastforce
          with that[OF _ this] "2"(1) ‹sat b›[unfolded sat_def] show ?thesis
            using realisation_if_AT_eq 2 by metis
        qed (use * that[of t1] in blast)
        moreover
        note Ex_AT_eq_mem_subterms_last_if_subterms'[OF ‹t2 ∈ subterms' b›]
        then obtain t2'' where
          "t2'' ∈ subterms (last b) - base_vars b" "AF (t1'' =⇩s t2'') ∈ set b"
          "realise t2'' = realise t2"
        proof cases
          case (2 t2')
          from bopen neqSelf ‹AF (t1'' =⇩s t2) ∈ set b› have "t1'' ≠ t2"
            by blast
          with 2 ‹sat b›[THEN satD(1), THEN lin_satD] have "AF (t1'' =⇩s t2') ∈ set b"
            using lexpands_eq.intros(2,4)[OF _ ‹AF (t1'' =⇩s t2) ∈ set b›, THEN lexpands.intros(6)]
            by fastforce
          with that[OF _ this] "2"(1) ‹sat b›[unfolded sat_def] show ?thesis
            using realisation_if_AT_eq 2 by metis
        qed (use ‹AF (t1'' =⇩s t2) ∈ set b› that[of t2] in blast)
        ultimately show ?thesis
          using that * by metis
      qed
      with ‹realise t1 = realise t2› have "(t1', t2') ∈ Δ"
        unfolding Δ_def subterms'_def
        by (simp add: AF_eq_subterms_branchD(1,2))
      then have t1'_t2'_subterms: "t1' ∈ subterms' b" "t2' ∈ subterms' b"
        unfolding Δ_def by blast+
      
      from t1'_t2' lemma1_2 "*"(3) have "?h (t1', t2') = ?h (t1, t2)"
        by (metis in_subterms'_if_AF_eq_in_branch(1,2)[OF wf_branch] case_prod_conv)

      from mem_urelems_if_urelem_last[OF wf_branch] t1'_t2'(1,2)
      have not_urelem: "¬ urelem (last b) t1'" "¬ urelem (last b) t2'"
        unfolding base_vars_def by auto
      from finite_vars_branch infinite_vars obtain x where "x ∉ vars b"
        using ex_new_if_finite by blast
      from bexpands_wit.intros[OF t1'_t2'(3) _ _ _ _ this not_urelem]
           t1'_t2'(1,2) ‹sat b›[unfolded sat_def] consider
        s1 where "AT (s1 ∈⇩s t1') ∈ set b" "AF (s1 ∈⇩s t2') ∈ set b" |
        s2 where "AF (s2 ∈⇩s t1') ∈ set b" "AT (s2 ∈⇩s t2') ∈ set b"
        using bexpands.intros(2-) by (metis Diff_iff)
      then show ?thesis
      proof cases
        case 1
        then have "realise s1 ❙∈ realise t2'"
          using realisation_if_AT_mem
          by (metis "*"(4) t1'_t2'(4) t1'_t2'(5))
        with 1 t1'_t2'(3,4) obtain s2 where
          "s2 →⇘bgraph b⇙ t2'" "realise s1 = realise s2"
          using dominates_if_mem_realisation in_subterms'_if_AT_mem_in_branch(1)[OF wf_branch] 
          by metis
        then have "AT (s2 ∈⇩s t2') ∈ set b"
          unfolding bgraph_def Let_def by auto
        with ‹AF (s1 ∈⇩s t2') ∈ set b› ‹sat b›[THEN satD(1), THEN lin_satD]
        have "AF (s2 =⇩s s1) ∈ set b"
          using lexpands_eq.intros(5)[THEN lexpands.intros(6)] by fastforce
        then have "s1 ≠ s2"
          using neqSelf bopen by blast
        from realise_base_vars_if_AF_eq[OF ‹sat b› ‹AF (s2 =⇩s s1) ∈ set b›]
             ‹realise s1 = realise s2›
        have "s1 ∈ subterms' b" "s2 ∈ subterms' b"
          by (metis Un_iff ‹AF (s2 =⇩s s1) ∈ set b› in_subterms'_if_AF_eq_in_branch wf_branch)+
   
        with ‹realise s1 = realise s2› have "(s2, s1) ∈ Δ"
          unfolding Δ_def using ‹AF (s2 =⇩s s1) ∈ set b› by auto
        moreover
        have "realise s1 ❙∈ realise t1'" "realise s2 ❙∈ realise t1'"
             "realise s1 ❙∈ realise t2'" "realise s2 ❙∈ realise t2'"
          using ‹realise s1 ❙∈ realise t2'› ‹realise s1 = realise s2›
          using "*"(4) t1'_t2'(4,5) by auto
        with lemma1_3 have "?h (s2, s1) < ?h (t1', t2')"
          using ‹s1 ∈ subterms' b› ‹s2 ∈ subterms' b› t1'_t2'_subterms
          by (auto simp: min_def)
        ultimately show ?thesis
          using arg_min_least[OF ‹finite Δ› ‹Δ ≠ {}›]
          using ‹(t1', t2') ∈ Δ› ‹?h (t1', t2') = ?h (t1, t2)› t1_t2
          by (metis (mono_tags, lifting) le_antisym le_eq_less_or_eq nat_neq_iff)
      next
        case 2
        then have "realise s2 ❙∈ realise t1'"
          using realisation_if_AT_mem
          by (metis "*"(4) t1'_t2'(4) t1'_t2'(5))
        with 2 t1'_t2'(3,4) obtain s1 where
          "s1 →⇘bgraph b⇙ t1'" "realise s1 = realise s2"
          using dominates_if_mem_realisation by metis
        then have "AT (s1 ∈⇩s t1') ∈ set b"
          unfolding bgraph_def Let_def by auto
        with ‹AF (s2 ∈⇩s t1') ∈ set b› ‹sat b›[unfolded sat_def]
        have "AF (s1 =⇩s s2) ∈ set b"
          using lexpands_eq.intros(5)[THEN lexpands.intros(6)]
          using lin_satD by fastforce
        then have "s1 ≠ s2"
          using neqSelf bopen by blast           
        from realise_base_vars_if_AF_eq[OF ‹sat b› ‹AF (s1 =⇩s s2) ∈ set b›]
             ‹realise s1 = realise s2›
        have "s1 ∈ subterms' b" "s2 ∈ subterms' b"
          by (metis Un_iff ‹AF (s1 =⇩s s2) ∈ set b› in_subterms'_if_AF_eq_in_branch wf_branch)+

        with ‹realise s1 = realise s2› have "(s1, s2) ∈ Δ"
          unfolding Δ_def using ‹AF (s1 =⇩s s2) ∈ set b› by auto
        moreover
        have "realise s1 ❙∈ realise t1'" "realise s2 ❙∈ realise t1'"
             "realise s1 ❙∈ realise t2'" "realise s2 ❙∈ realise t2'"
          using ‹realise s2 ❙∈ realise t1'› ‹realise s1 = realise s2›
          using "*"(4) t1'_t2'(4,5) by auto
        with lemma1_3 have "?h (s1, s2) < ?h (t1', t2')"
          using ‹s1 ∈ subterms' b› ‹s2 ∈ subterms' b› t1'_t2'_subterms
          by (auto simp: min_def)
        ultimately show ?thesis
          using arg_min_least[OF ‹finite Δ› ‹Δ ≠ {}›]
          using ‹(t1', t2') ∈ Δ› ‹?h (t1', t2') = ?h (t1, t2)› t1_t2
          by (metis (mono_tags, lifting) le_antisym le_eq_less_or_eq nat_neq_iff)
      qed
    qed
    with assms subterms show ?thesis
      unfolding Δ_def by blast
  qed
qed

lemma realisation_if_AF_mem:
  assumes "sat b"
  assumes "AF (s ∈⇩s t) ∈ set b"
  shows "realise s ❙∉ realise t"
proof
  assume "realise s ❙∈ realise t"
  from assms have "s ∈ base_vars b ∪ subterms' b"
                  "t ∈ base_vars b ∪ subterms' b"
    using in_subterms'_if_AF_mem_in_branch[OF wf_branch] by blast+
  from dominates_if_mem_realisation[OF ‹realise s ❙∈ realise t›]
  obtain s' where "s' →⇘bgraph b⇙ t" "realise s = realise s'"
    by blast
  then have "AT (s' ∈⇩s t) ∈ set b"
    unfolding bgraph_def Let_def by auto
  with assms lexpands_eq.intros(5)[THEN lexpands.intros(6)] have "AF (s' =⇩s s) ∈ set b"
    unfolding sat_def using lin_satD by fastforce
  from realisation_if_AF_eq[OF ‹sat b› this] ‹realise s = realise s'› show False
    by simp
qed

lemma realisation_Empty: "realise (∅ n) = 0"
proof -
  from bopen have "AT (s ∈⇩s ∅ n) ∉ set b" for s
    using bclosed.intros by blast
  then have "parents (bgraph b) (∅ n) = {}"
    unfolding bgraph_def Let_def by auto
  moreover
  have "(∅ n) ∉ base_vars b"
  proof -
    have "(∅ n) ∉ Var ` pwits b"
      using pwits_def wits_def by blast
    moreover have "(∅ n) ∉ urelems b"
      unfolding urelems_def using wf_branch[THEN wf_branch_not_Nil] last_in_set
      using is_Var_if_urelem' by fastforce
    ultimately show ?thesis
      unfolding base_vars_def by blast
  qed
  then have "(∅ n) ∈ subterms' b ∨ (∅ n) ∉ verts (bgraph b)"
    by (simp add: verts_bgraph)
  ultimately show "realise (∅ n) = 0"
    by (auto simp: verts_bgraph)
qed

lemma realisation_Union:
  assumes "sat b"
  assumes "t1 ⊔⇩s t2 ∈ subterms b"
  shows "realise (t1 ⊔⇩s t2) = realise t1 ⊔ realise t2"
  using assms
proof -
  from assms have mem_subterms_last: "t1 ⊔⇩s t2 ∈ subterms (last b)"
    using mem_subterms_fm_last_if_mem_subterms_branch[OF wf_branch]
    by simp
  note not_urelem_comps_if_compound[where ?f="(⊔⇩s)", OF assms(2), simplified]
  moreover note subterms_fmD(1,2)[OF mem_subterms_last]
  then have "t1 ∉ Var ` pwits b" "t2 ∉ Var ` pwits b"
    unfolding pwits_def wits_def 
    using pset_term.set_intros(1) mem_vars_fm_if_mem_subterms_fm by fastforce+
  ultimately have "t1 ∈ subterms' b" "t2 ∈ subterms' b"
    unfolding subterms'_def base_vars_def
    using assms(2) by (auto dest: subterms_branchD)

  from assms(2) have "t1 ⊔⇩s t2 ∈ subterms' b"
    using base_vars_subs_vars base_vars_Un_subterms'_eq_subterms by blast

  have "realise (t1 ⊔⇩s t2) ≤ realise t1 ⊔ realise t2"
  proof
    fix e assume "e ❙∈ realise (t1 ⊔⇩s t2)"
    then obtain s where s: "e = realise s" "s →⇘bgraph b⇙ (t1 ⊔⇩s t2)"
      using dominates_if_mem_realisation ‹t1 ⊔⇩s t2 ∈ subterms' b›
      by auto
    then have "AT (s ∈⇩s t1 ⊔⇩s t2) ∈ set b"
      unfolding bgraph_def Let_def by auto
    with ‹sat b› consider "AT (s ∈⇩s t1) ∈ set b" | "AF (s ∈⇩s t1) ∈ set b"
      unfolding sat_def using bexpands_nowit.intros(3)[OF _ mem_subterms_last, THEN bexpands.intros(1)]
      by blast
    then show "e ❙∈ realise t1 ⊔ realise t2"
    proof(cases)
      case 1
      with s show ?thesis using realisation_if_AT_mem by auto
    next
      case 2
      from ‹sat b› lexpands_un.intros(4)[OF ‹AT (s ∈⇩s t1 ⊔⇩s t2) ∈ set b› this]
      have "AT (s ∈⇩s t2) ∈ set b"
        unfolding sat_def using lin_satD lexpands.intros(2) by force
      with s show ?thesis using realisation_if_AT_mem by auto
    qed
  qed
  moreover have "realise t1 ⊔ realise t2 ≤ realise (t1 ⊔⇩s t2)"
  proof
    fix e assume "e ❙∈ realise t1 ⊔ realise t2"
    with ‹t1 ∈ subterms' b› ‹t2 ∈ subterms' b› consider
      s1 where "e = realise s1" "s1 →⇘bgraph b⇙ t1" |
      s2 where "e = realise s2" "s2 →⇘bgraph b⇙ t2"
      using dominates_if_mem_realisation by force
    then show "e ❙∈ realise (t1 ⊔⇩s t2)"
    proof(cases)
      case 1
      then have "AT (s1 ∈⇩s t1) ∈ set b"
        unfolding bgraph_def Let_def by auto
      from ‹sat b› lexpands_un.intros(2)[OF this mem_subterms_last, THEN lexpands.intros(2)]
      have "AT (s1 ∈⇩s t1 ⊔⇩s t2) ∈ set b"
        unfolding sat_def using lin_satD by force
      with 1 realisation_if_AT_mem[OF this] show ?thesis
        by blast
    next
      case 2
      then have "AT (s2 ∈⇩s t2) ∈ set b"
        unfolding bgraph_def Let_def by auto
      from ‹sat b› lexpands_un.intros(3)[OF this mem_subterms_last, THEN lexpands.intros(2)]
      have "AT (s2 ∈⇩s t1 ⊔⇩s t2) ∈ set b"
        unfolding sat_def using lin_satD by force
      with 2 realisation_if_AT_mem[OF this] show ?thesis
        by blast
    qed
  qed
  ultimately show ?thesis by blast
qed

lemma realisation_Inter:
  assumes "sat b"
  assumes "t1 ⊓⇩s t2 ∈ subterms b"
  shows "realise (t1 ⊓⇩s t2) = realise t1 ⊓ realise t2"
  using assms
proof -
  from assms have mem_subterms_last: "t1 ⊓⇩s t2 ∈ subterms (last b)"
    using mem_subterms_fm_last_if_mem_subterms_branch[OF wf_branch]
    by simp
  note not_urelem_comps_if_compound[where ?f="(⊓⇩s)", OF assms(2), simplified]
  moreover note subterms_fmD(3,4)[OF mem_subterms_last]
  then have "t1 ∉ Var ` pwits b" "t2 ∉ Var ` pwits b"
    unfolding pwits_def wits_def 
    using pset_term.set_intros(1) mem_vars_fm_if_mem_subterms_fm by fastforce+
  ultimately have t1_t2_subterms': "t1 ∈ subterms' b" "t2 ∈ subterms' b"
    unfolding subterms'_def base_vars_def
    using assms(2) by (auto dest: subterms_branchD)

  from assms(2) have "t1 ⊓⇩s t2 ∈ subterms' b"
    using base_vars_subs_vars base_vars_Un_subterms'_eq_subterms by blast

  have "realise (t1 ⊓⇩s t2) ≤ realise t1 ⊓ realise t2"
  proof
    fix e assume "e ❙∈ realise (t1 ⊓⇩s t2)"
    with ‹t1 ⊓⇩s t2 ∈ subterms' b› obtain s
      where s: "e = realise s" "s →⇘bgraph b⇙ (t1 ⊓⇩s t2)"
      using dominates_if_mem_realisation by auto
    then have "AT (s ∈⇩s t1 ⊓⇩s t2) ∈ set b"
      unfolding bgraph_def Let_def by auto
    with ‹sat b› lexpands_int.intros(1)[OF this, THEN lexpands.intros(3)]
    have "AT (s ∈⇩s t1) ∈ set b" "AT (s ∈⇩s t2) ∈ set b"
      unfolding sat_def using lin_satD by force+
    from this[THEN realisation_if_AT_mem] s show "e ❙∈ realise t1 ⊓ realise t2"
      by auto
  qed
  moreover have "realise t1 ⊓ realise t2 ≤ realise (t1 ⊓⇩s t2)"
  proof
    fix e assume "e ❙∈ realise t1 ⊓ realise t2"
    with ‹t1 ∈ subterms' b› ‹t2 ∈ subterms' b› obtain s1 s2 where s1_s2:
      "e = realise s1" "s1 →⇘bgraph b⇙ t1"
      "e = realise s2" "s2 →⇘bgraph b⇙ t2"
      using dominates_if_mem_realisation by auto metis
    then have "AT (s1 ∈⇩s t1) ∈ set b" "AT (s2 ∈⇩s t2) ∈ set b"
      unfolding bgraph_def Let_def by auto
    moreover have "AT (s1 ∈⇩s t2) ∈ set b"
    proof -
      from ‹sat b› have "AT (s1 ∈⇩s t2) ∈ set b ∨ AF (s1 ∈⇩s t2) ∈ set b"
        unfolding sat_def
        using bexpands_nowit.intros(4)[OF ‹AT (s1 ∈⇩s t1) ∈ set b› mem_subterms_last]
        using bexpands.intros(1) by blast
      moreover from ‹sat b› s1_s2 have False if "AF (s1 ∈⇩s t2) ∈ set b"
      proof -
        note lexpands_eq.intros(5)[OF ‹AT (s2 ∈⇩s t2) ∈ set b› that, THEN lexpands.intros(6)]
        with realisation_if_AF_eq[OF ‹sat b›, of s2 s1] have "realise s2 ≠ realise s1"
          using ‹sat b› by (auto simp: sat_def lin_satD)
        with ‹e = realise s1› ‹e = realise s2› show False by simp
      qed
      ultimately show "AT (s1 ∈⇩s t2) ∈ set b" by blast
    qed
    ultimately have "AT (s1 ∈⇩s t1 ⊓⇩s t2) ∈ set b"
      using ‹sat b› lexpands_int.intros(6)[OF _ _ mem_subterms_last, THEN lexpands.intros(3)]
      unfolding sat_def by (fastforce simp: lin_satD)
    from realisation_if_AT_mem[OF this] show "e ❙∈ realise (t1 ⊓⇩s t2)"
      unfolding ‹e = realise s1›
      by simp
  qed
  ultimately show ?thesis by blast
qed

lemma realisation_Diff:
  assumes "sat b"
  assumes "s -⇩s t ∈ subterms b"
  shows "realise (s -⇩s t) = realise s - realise t"
  using assms
proof -
  from assms have mem_subterms_last: "s -⇩s t ∈ subterms (last b)"
    using mem_subterms_fm_last_if_mem_subterms_branch[OF wf_branch]
    by simp
  note not_urelem_comps_if_compound[where ?f="(-⇩s)", OF assms(2), simplified]
  moreover note subterms_fmD(5,6)[OF mem_subterms_last]
  then have "s ∉ Var ` pwits b" "t ∉ Var ` pwits b"
    unfolding pwits_def wits_def 
    using pset_term.set_intros(1) mem_vars_fm_if_mem_subterms_fm by fastforce+
  ultimately have "s ∈ subterms' b" "t ∈ subterms' b"
    unfolding subterms'_def base_vars_def
    using assms(2) by (auto dest: subterms_branchD)

  from assms(2) have "s -⇩s t ∈ subterms' b"
    using base_vars_subs_vars base_vars_Un_subterms'_eq_subterms by blast

  have "realise (s -⇩s t) ≤ realise s - realise t"
  proof
    fix e assume "e ❙∈ realise (s -⇩s t)"
    then obtain u where u: "e = realise u" "u →⇘bgraph b⇙ (s -⇩s t)"
      using dominates_if_mem_realisation ‹s -⇩s t ∈ subterms' b› by auto
    then have "AT (u ∈⇩s s -⇩s t) ∈ set b"
      unfolding bgraph_def Let_def by auto
    with ‹sat b› lexpands_diff.intros(1)[OF this, THEN lexpands.intros(4)]
    have "AT (u ∈⇩s s) ∈ set b" "AF (u ∈⇩s t) ∈ set b"
      unfolding sat_def using lin_satD by force+
    with u show "e ❙∈ realise s - realise t"
      using ‹sat b› realisation_if_AT_mem realisation_if_AF_mem
      by auto
  qed
  moreover have "realise s - realise t ≤ realise (s -⇩s t)"
  proof
    fix e assume "e ❙∈ realise s - realise t"
    then obtain u where u:
      "e = realise u" "u →⇘bgraph b⇙ s" "¬ u →⇘bgraph b⇙ t"
      using dominates_if_mem_realisation ‹s ∈ subterms' b› ‹t ∈ subterms' b› by auto
    then have "AT (u ∈⇩s s) ∈ set b"
      unfolding bgraph_def Let_def by auto
    moreover have "AF (u ∈⇩s t) ∈ set b"
    proof -
      from ‹sat b› have "AT (u ∈⇩s t) ∈ set b ∨ AF (u ∈⇩s t) ∈ set b"
        unfolding sat_def using bexpands_nowit.intros(5)[OF ‹AT (u ∈⇩s s) ∈ set b› mem_subterms_last]
        using bexpands.intros(1) by blast
      moreover from u(3) have False if "AT (u ∈⇩s t) ∈ set b"
        using that unfolding Let_def bgraph_def by (auto simp: arcs_ends_def arc_to_ends_def)
      ultimately show "AF (u ∈⇩s t) ∈ set b"
        by blast
    qed
    ultimately have "AT (u ∈⇩s s -⇩s t) ∈ set b"
      using ‹sat b› lexpands_diff.intros(6)[OF _ _ mem_subterms_last, THEN lexpands.intros(4)]
      unfolding sat_def by (fastforce simp: lin_satD)
    from realisation_if_AT_mem[OF this] show "e ❙∈ realise (s -⇩s t)"
      unfolding ‹e = realise u›
      by simp
  qed
  ultimately show ?thesis by blast
qed

lemma realisation_Single:
  assumes "sat b"
  assumes "Single t ∈ subterms b"
  shows "realise (Single t) = HF {realise t}"
  using assms
proof -
  from assms have mem_subterms_last: "Single t ∈ subterms (last b)"
    using mem_subterms_fm_last_if_mem_subterms_branch[OF wf_branch]
    by simp
  have "Single t ∈ subterms' b"
    proof -
    from urelems_subs_vars have "Single t ∉ base_vars b"
      unfolding base_vars_def by blast
    then show ?thesis
      by (simp add: assms(2) subterms'_def)
  qed

  have "realise (Single t) ≤ HF {realise t}"
  proof
    fix e assume "e ❙∈ realise (Single t)"
    then obtain s where s: "e = realise s" "s →⇘bgraph b⇙ Single t"
      using dominates_if_mem_realisation ‹Single t ∈ subterms' b› by auto
    then have "AT (s ∈⇩s Single t) ∈ set b"
      unfolding bgraph_def Let_def by auto
    with ‹sat b› lexpands_single.intros(2)[OF this, THEN lexpands.intros(5)]
    have "AT (s =⇩s t) ∈ set b"
      unfolding sat_def using lin_satD by fastforce
    with s show "e ❙∈ HF {realise t}"
      using realisation_if_AT_eq ‹sat b›[unfolded sat_def]
      by auto
  qed
  moreover have "HF {realise t} ≤ realise (Single t)"
  proof
    fix e assume "e ❙∈ HF {realise t}"
    then have "e = realise t"
      by simp
    from lexpands_single.intros(1)[OF mem_subterms_last, THEN lexpands.intros(5)] ‹sat b›
    have "AT (t ∈⇩s Single t) ∈ set b"
      unfolding sat_def using lin_satD by fastforce
    from realisation_if_AT_mem[OF this] ‹e = realise t›
    show "e ❙∈ realise (Single t)"
      by simp
  qed
  ultimately show ?thesis by blast
qed

lemmas realisation_simps =
  realisation_Empty realisation_Union realisation_Inter realisation_Diff realisation_Single

end

subsection ‹Coherence›

lemma (in open_branch) I⇩s⇩t_realisation_eq_realisation:
  assumes "sat b" "t ∈ subterms b"
  shows "I⇩s⇩t (λx. realise (Var x)) t = realise t"
  using assms
  by (induction t) (force simp: realisation_simps dest: subterms_branchD)+

lemma (in open_branch) coherence:
  assumes "sat b" "φ ∈ set b"
  shows "interp I⇩s⇩a (λx. realise (Var x)) φ"
  using assms
proof(induction "size φ" arbitrary: φ rule: less_induct)
  case less
  then show ?case
  proof(cases φ)
    case (Atom a)
    then show ?thesis
    proof(cases a)
      case (Elem s t)
      with Atom less have "s ∈ subterms b" "t ∈ subterms b"
        using AT_mem_subterms_branchD by blast+
      with Atom Elem less show ?thesis
        using I⇩s⇩t_realisation_eq_realisation[OF ‹sat b›] realisation_if_AT_mem by auto
    next
      case (Equal s t)
      with Atom less have "s ∈ subterms b" "t ∈ subterms b"
        using AT_eq_subterms_branchD by blast+
      with Atom Equal less satD(1)[OF ‹sat b›] show ?thesis
        using I⇩s⇩t_realisation_eq_realisation[OF ‹sat b›] realisation_if_AT_eq by auto
    qed
  next
    case (And φ1 φ2)
    with ‹φ ∈ set b› ‹sat b›[THEN satD(1), THEN lin_satD] have "φ1 ∈ set b" "φ2 ∈ set b"
      using lexpands_fm.intros(1)[THEN lexpands.intros(1)] by fastforce+
    with And less show ?thesis by simp
  next
    case (Or φ1 φ2)
    with ‹φ ∈ set b› ‹sat b›[THEN satD(2)] have "φ1 ∈ set b ∨ Neg φ1 ∈ set b"
      using bexpands_nowit.intros(1)[THEN bexpands.intros(1)]
      by blast
    with less Or ‹sat b›[THEN satD(1), THEN lin_satD] have "φ1 ∈ set b ∨ φ2 ∈ set b"
      using lexpands_fm.intros(3)[THEN lexpands.intros(1)] by fastforce
    with Or less show ?thesis
      by force
  next
    case (Neg φ')
    show ?thesis
    proof(cases φ')
      case (Atom a)
      then show ?thesis
      proof(cases a)
        case (Elem s t)
        with Atom Neg less have "s ∈ subterms b" "t ∈ subterms b"
          using AF_mem_subterms_branchD by blast+
        with Neg Atom Elem less show ?thesis
          using I⇩s⇩t_realisation_eq_realisation realisation_if_AF_mem ‹sat b› by auto
      next
        case (Equal s t)
        with Atom Neg less have "s ∈ subterms b" "t ∈ subterms b"
          using AF_eq_subterms_branchD by blast+
        with Neg Atom Equal less show ?thesis
          using I⇩s⇩t_realisation_eq_realisation realisation_if_AF_eq ‹sat b› by auto
      qed
    next
      case (And φ1 φ2)
      with Neg ‹sat b›[THEN satD(2)] less have "φ1 ∈ set b ∨ Neg φ1 ∈ set b"
        using bexpands_nowit.intros(2)[THEN bexpands.intros(1)] by blast
      with ‹sat b›[THEN satD(1), THEN lin_satD] Neg And less
      have "Neg φ2 ∈ set b ∨ Neg φ1 ∈ set b"
        using lexpands_fm.intros(5)[THEN lexpands.intros(1)] by fastforce
      with Neg And less show ?thesis by force
    next
      case (Or φ1 φ2)
      with ‹φ ∈ set b› Neg ‹sat b›[THEN satD(1), THEN lin_satD]
      have "Neg φ1 ∈ set b" "Neg φ2 ∈ set b"
        using lexpands_fm.intros(2)[THEN lexpands.intros(1)] by fastforce+
      moreover have "size (Neg φ1) < size φ" "size (Neg φ2) < size φ"
        using Neg Or by simp_all
      ultimately show ?thesis using Neg Or less by force
    next
      case Neg': (Neg φ'')
      with ‹φ ∈ set b› Neg ‹sat b›[THEN satD(1), THEN lin_satD] have "φ'' ∈ set b"
        using lexpands_fm.intros(7)[THEN lexpands.intros(1)] by fastforce+
      with Neg Neg' less show ?thesis by simp
    qed
  qed
qed


section ‹Soundness of the Calculus›

subsection ‹Soundness of Closedness›

lemmas wf_trancl_hmem_rel = wf_trancl[OF wf_hmem_rel]

lemma trancl_hmem_rel_not_refl: "(x, x) ∉ hmem_rel⇧+"
  using wf_trancl_hmem_rel by simp

lemma mem_trancl_elts_rel_if_member_seq:
  assumes "member_seq s cs t"
  assumes "cs ≠ []"
  assumes "∀a ∈ set cs. I⇩s⇩a M a"
  shows "(I⇩s⇩t M s, I⇩s⇩t M t) ∈ hmem_rel⇧+"
  using assms
proof(induction rule: member_seq.induct)
  case (2 s s' u cs t)
  show ?case
  proof(cases cs)
    case Nil
    with 2 show ?thesis
      unfolding hmem_rel_def by auto
  next
    case (Cons c cs')
    with 2 have "(I⇩s⇩t M u, I⇩s⇩t M t) ∈ hmem_rel⇧+"
      by simp
    moreover from 2 have "I⇩s⇩a M (s ∈⇩s u)"
      by simp
    ultimately show ?thesis
      unfolding hmem_rel_def by (simp add: trancl_into_trancl2)
  qed
qed simp_all

lemma bclosed_sound:
  assumes "bclosed b"
  shows "∃φ ∈ set b. ¬ interp I⇩s⇩a M φ"
  using assms
proof -
  have False if "∀φ ∈ set b. interp I⇩s⇩a M φ"
    using assms that
  proof(induction rule: bclosed.induct)
    case (memberCycle cs b)
    then have "∀a ∈ set cs. I⇩s⇩a M a"
      unfolding Atoms_def by fastforce
    from memberCycle obtain s where "member_seq s cs s"
      using member_cycle.elims(2) by blast
    with memberCycle ‹∀a ∈ set cs. I⇩s⇩a M a› have "(I⇩s⇩t M s, I⇩s⇩t M s) ∈ hmem_rel⇧+"
      using mem_trancl_elts_rel_if_member_seq member_cycle.simps(2) by blast  
    with trancl_hmem_rel_not_refl show ?case
      by blast
  qed (use interp.simps(4) in ‹fastforce+›)
  then show ?thesis
    by blast
qed

lemma types_term_lt_if_member_seq:
  fixes cs :: "'a pset_atom list"
  assumes "∀a ∈ set cs. v ⊢ a"
  assumes "member_seq s cs t" "cs ≠ []"
  shows "∃ls lt. v ⊢ s : ls ∧ v ⊢ t : lt ∧ ls < lt"
  using assms
proof(induction s cs t rule: member_seq.induct)
  case (2 s s' u cs t)
  then show ?case
  proof(cases cs)
    case (Cons c cs')
    with 2 obtain lu lt where "v ⊢ u : lu" "v ⊢ t : lt" "lu < lt"
      by auto
    moreover from 2 obtain ls where "v ⊢ s : ls" "ls < lu"
      using ‹v ⊢ u : lu› by (auto simp: types_pset_atom.simps dest: types_term_unique)
    ultimately show ?thesis
      by fastforce
  qed (fastforce simp: types_pset_atom.simps)
qed auto

lemma no_member_cycle_if_types_last:
  fixes b :: "'a branch"
  assumes "wf_branch b"
  assumes "∃v. v ⊢ last b"
  shows "¬ (member_cycle cs ∧ set cs ⊆ Atoms (set b))"
proof
  presume "member_cycle cs" "set cs ⊆ Atoms (set b)"
  then obtain s where "member_seq s cs s" "cs ≠ []"
    using member_cycle.elims(2) by blast
  moreover from assms obtain v where "∀φ ∈ set b. v ⊢ φ"
    using types_urelems by blast
  with ‹set cs ⊆ Atoms (set b)› have "∀a ∈ set cs. v ⊢ a"
    unfolding Atoms_def by (auto dest!: types_fmD(6))
  ultimately show False
    using types_term_lt_if_member_seq types_term_unique by blast
qed simp_all

subsection ‹Soundness of the Expansion Rules›

lemma lexpands_sound:
  assumes "lexpands b' b"
  assumes "φ ∈ set b'"
  assumes "⋀ψ. ψ ∈ set b ⟹ interp I⇩s⇩a M ψ"
  shows "interp I⇩s⇩a M φ"
  using assms
proof(induction rule: lexpands.induct)
  case (1 b' b)
  then show ?case
    by (induction rule: lexpands_fm.induct)
       (metis empty_iff empty_set interp.simps(2,3,4) set_ConsD)+
next
  case (2 b' b)
  then show ?case
  proof(induction rule: lexpands_un.induct)
    case (4 s t1 t2 branch)
    with this(1)[THEN this(4)] show ?case
      by force
  next
    case (5 s t1 t2 branch)
    with this(1)[THEN this(4)] show ?case
      by force
  qed force+
next
  case (3 b' b)
  then show ?case
  proof(induction rule: lexpands_int.induct)
    case (4 s t1 t2 branch)
    with this(1)[THEN this(4)] show ?case
      by force
  next
    case (5 s t1 t2 branch)
    with this(1)[THEN this(4)] show ?case
      by force
  qed force+
next
  case (4 b' b)
  then show ?case
  proof(induction rule: lexpands_diff.induct)
    case (4 s t1 t2 branch)
    with this(1)[THEN this(4)] show ?case by force
  next
    case (5 s t1 t2 branch)
    with this(1)[THEN this(4)] show ?case by force
  qed force+
next
  case (5 b' b)
  then show ?case
    by (induction rule: lexpands_single.induct) force+
next
  case (6 b' b)
  then show ?case
  proof(induction rule: lexpands_eq_induct')
    case (subst t1 t2 t1' t2' p l b)
    with this(1,2)[THEN this(6)] show ?case
      by (cases l; cases p) auto
  next
    case (neq s t s' b)
    with this(1,2)[THEN this(4)] show ?case by force
  qed
qed

lemma bexpands_nowit_sound:
  assumes "bexpands_nowit bs' b"
  assumes "⋀ψ. ψ ∈ set b ⟹ interp I⇩s⇩a M ψ"
  shows "∃b' ∈ bs'. ∀ψ ∈ set b'. interp I⇩s⇩a M ψ"
  using assms
  by (induction rule: bexpands_nowit.induct) force+

lemma I⇩s⇩t_upd_eq_if_not_mem_vars_term:
  assumes "x ∉ vars t"
  shows "I⇩s⇩t (M(x := y)) t = I⇩s⇩t M t"
  using assms by (induction t) auto

lemma I⇩s⇩a_upd_eq_if_not_mem_vars_atom:
  assumes "x ∉ vars a"
  shows "I⇩s⇩a (M(x := y)) a = I⇩s⇩a M a"
  using assms
  by (cases a) (auto simp: I⇩s⇩t_upd_eq_if_not_mem_vars_term)

lemma interp_upd_eq_if_not_mem_vars_fm:
  assumes "x ∉ vars φ"
  shows "interp I⇩s⇩a (M(x := y)) φ = interp I⇩s⇩a M φ"
  using assms
  by (induction φ) (auto simp: I⇩s⇩a_upd_eq_if_not_mem_vars_atom)

lemma bexpands_wit_sound:
  assumes "bexpands_wit s t x bs' b"
  assumes "⋀ψ. ψ ∈ set b ⟹ interp I⇩s⇩a M ψ"
  shows "∃M. ∃b' ∈ bs'. ∀ψ ∈ set (b' @ b). interp I⇩s⇩a M ψ"
  using assms
proof (induction rule: bexpands_wit.induct)
  let ?bs'="{[AT (Var x ∈⇩s s), AF (Var x ∈⇩s t)],
             [AT (Var x ∈⇩s t), AF (Var x ∈⇩s s)]}"
  case (1 b)
  with this(1)[THEN this(9)] have "I⇩s⇩t M s ≠ I⇩s⇩t M t"
    by auto
  then obtain y where y:
    "y ❙∈ I⇩s⇩t M s ∧ y ❙∉ I⇩s⇩t M t ∨
     y ❙∈ I⇩s⇩t M t ∧ y ❙∉ I⇩s⇩t M s"
    by auto
  have "x ∉ vars s" "x ∉ vars t"
    using 1 by (auto simp: vars_fm_vars_branchI)
  then have "I⇩s⇩t (M(x := y)) s = I⇩s⇩t M s" "I⇩s⇩t (M(x := y)) t = I⇩s⇩t M t"
    using I⇩s⇩t_upd_eq_if_not_mem_vars_term by metis+
  then have "∃b' ∈ ?bs'. ∀ψ ∈ set b'. interp I⇩s⇩a (M(x := y)) ψ"
    using 1 y by auto
  moreover have "∀ψ ∈ set b. interp I⇩s⇩a (M(x := y)) ψ"
    using "1"(9) ‹x ∉ vars b› interp_upd_eq_if_not_mem_vars_fm
    by (metis vars_fm_vars_branchI)
  ultimately show ?case
    by auto (metis fun_upd_same)+
qed

lemma bexpands_sound:
  assumes "bexpands bs' b"
  assumes "⋀ψ. ψ ∈ set b ⟹ interp I⇩s⇩a M ψ"
  shows "∃M. ∃b' ∈ bs'. ∀ψ ∈ set (b' @ b). interp I⇩s⇩a M ψ"
  using assms
proof(induction rule: bexpands.induct)
  case (1 bs' b)
  with bexpands_nowit_sound[OF this(1)] have "∃b' ∈ bs'. ∀ψ ∈ set b'. interp I⇩s⇩a M ψ"
    by blast
  with 1 show ?case
    by auto
next
  case (2 t1 t2 x bs b)
  then show ?case using bexpands_wit_sound by metis
qed


section ‹Upper Bounding the Cardinality of a Branch›

lemma Ex_bexpands_wits_if_in_wits:
  assumes "wf_branch b"
  assumes "x ∈ wits b"
  obtains t1 t2 bs b2 b1 where
    "expandss b (b2 @ b1)" "bexpands_wit t1 t2 x bs b1" "b2 ∈ bs" "expandss b1 [last b]"
    "x ∉ wits b1" "wits (b2 @ b1) = insert x (wits b1)"
proof -
  from assms obtain φ where "expandss b [φ]"
    unfolding wf_branch_def by blast
  then have "last b = φ"
    by simp
  from ‹expandss b [φ]› ‹x ∈ wits b› that show ?thesis
    unfolding ‹last b = φ›
  proof(induction b "[φ]" rule: expandss.induct)
    case 1
    then show ?case by simp
  next
    case (2 b2 b1)
    with expandss_mono have "b1 ≠ []"
      by fastforce
    with lexpands_wits_eq[OF ‹lexpands b2 b1› this] 2 show ?case
      by (metis (no_types, lifting) expandss.intros(2))
  next
    case (3 bs _ b2)
    then show ?case
    proof(induction rule: bexpands.induct)
      case (1 bs b1)
      with expandss_mono have "b1 ≠ []"
        by fastforce
      with bexpands_nowit_wits_eq[OF ‹bexpands_nowit bs b1› ‹b2 ∈ bs› this] 1 show ?case
        by (metis bexpands.intros(1) expandss.intros(3))
    next
      case (2 t1 t2 y bs b1)
      show ?case
      proof(cases "x ∈ wits b1")
        case True
        from 2 have "expandss (b2 @ b1) b1"
          using expandss.intros(3)[OF _ "2.prems"(1)] bexpands.intros(2)[OF "2.hyps"]
          by (metis expandss.intros(1))
        with True 2 show ?thesis
          using expandss_trans by blast
      next
        case False
        from 2 have "b1 ≠ []"
          using expandss_mono by fastforce
        with bexpands_witD[OF "2"(1)] "2"(2-) have "wits (b2 @ b1) = insert y (wits b1)"
          unfolding wits_def
          by (metis "2.hyps" bexpands_wit_wits_eq wits_def)
        moreover from ‹y ∉ vars_branch b1› have "y ∉ wits b1"
          unfolding wits_def by simp
        moreover from calculation have "y = x"
          using False 2 by simp
        ultimately show ?thesis
          using 2 by (metis expandss.intros(1))
      qed
    qed
  qed
qed

lemma card_wits_ub_if_wf_branch:
  assumes "wf_branch b"
  shows "card (wits b) ≤ (card (subterms (last b)))⇧2"
proof -
  from assms obtain φ where "expandss b [φ]"
    unfolding wf_branch_def by blast
  with wf_branch_not_Nil[OF assms] have [simp]: "last b = φ"
    using expandss_last_eq by force
  have False if card_gt: "card (wits b) > (card (subterms φ))⇧2"
  proof -
    define ts where "ts ≡ (λx. SOME t1_t2. ∃bs b2 b1.
       expandss b (b2 @ b1) ∧ b2 ∈ bs ∧ bexpands_wit (fst t1_t2) (snd t1_t2) x bs b1  ∧ expandss b1 [φ])"
    from ‹expandss b [φ]› ‹last b = φ›
    have *: "∃t1_t2 bs b2 b1.
      expandss b (b2 @ b1) ∧ b2 ∈ bs ∧ bexpands_wit (fst t1_t2) (snd t1_t2) x bs b1 ∧ expandss b1 [φ]"
      if "x ∈ wits b" for x
      using that Ex_bexpands_wits_if_in_wits[OF ‹wf_branch b› that] by (metis fst_conv snd_conv)
    have ts_wd:
      "∃bs b2 b1. expandss b (b2 @ b1) ∧ b2 ∈ bs ∧ bexpands_wit t1 t2 x bs b1 ∧ expandss b1 [φ]"
      if "ts x = (t1, t2)" "x ∈ wits b" for t1 t2 x
      using exE_some[OF * that(1)[THEN eq_reflection, symmetric, unfolded ts_def], OF that(2)]
      by simp
    with ‹last b = φ› ‹expandss b [φ]› have in_subterms_fm:
      "t1 ∈ subterms φ" "t2 ∈ subterms φ"
      if "ts x = (t1, t2)" "x ∈ wits b" for t1 t2 x
      using that bexpands_witD
      by (metis expandss_last_eq list.discI)+
    have "¬ inj_on ts (wits b)"
    proof -
      from in_subterms_fm have "ts ` wits b ⊆ subterms φ × subterms φ"
        by (intro subrelI) (metis imageE mem_Sigma_iff)
      then have "card (ts ` wits b) ≤ card (subterms φ × subterms φ)"
        by (intro card_mono) (simp_all add: finite_subterms_fm)
      moreover have "card (subterms φ × subterms φ) = (card (subterms φ))⇧2"
        unfolding card_cartesian_product by algebra
      ultimately show "¬ inj_on ts (wits b)"
        using card_gt by (metis card_image linorder_not_less)
    qed
  
    from ‹¬ inj_on ts (wits b)› obtain x t1 t2 xb1 xbs2 xb2 y yb1 ybs2 yb2 where x_y:
      "x ≠ y" "x ∈ wits b" "y ∈ wits b"
      "expandss xb1 [φ]" "bexpands_wit t1 t2 x xbs2 xb1" "xb2 ∈ xbs2" "expandss b (xb2 @ xb1)"
      "expandss yb1 [φ]" "bexpands_wit t1 t2 y ybs2 yb1" "yb2 ∈ ybs2" "expandss b (yb2 @ yb1)"
      unfolding inj_on_def by (metis ts_wd prod.exhaust)
    have "xb2 ≠ yb2"
      using x_y(5)[THEN bexpands_witD(1)] x_y(9)[THEN bexpands_witD(1)] x_y(1,6,10) 
      by auto
    moreover from x_y have "suffix (xb2 @ xb1) (yb2 @ yb1) ∨ suffix (yb2 @ yb1) (xb2 @ xb1)"
      using expandss_suffix suffix_same_cases by blast 
    then have "suffix (xb2 @ xb1) yb1 ∨ suffix (yb2 @ yb1) xb1"
      using x_y(5)[THEN bexpands_witD(1)] x_y(9)[THEN bexpands_witD(1)] x_y(1,6,10)
      by (auto simp: suffix_Cons)
    ultimately show False
      using bexpands_witD(1,5,6)[OF x_y(5)] bexpands_witD(1,5,6)[OF x_y(9)] x_y(6,10)
      by (auto dest!: set_mono_suffix)
  qed
  then show ?thesis
    using linorder_not_le ‹last b = φ› by blast
qed

lemma card_subterms_branch_ub_if_wf_branch:
  assumes "wf_branch b"
  shows "card (subterms b) ≤ card (subterms (last b)) + card (wits b)"
  unfolding subterms_branch_eq_if_wf_branch[OF assms, unfolded wits_subterms_def]
  by (simp add: assms card_Un_disjoint card_image_le finite_wits finite_subterms_fm
                wits_subterms_last_disjnt)

lemma card_literals_branch_if_wf_branch:
  assumes "wf_branch b"
  shows "card {a ∈ set b. is_literal a}
       ≤ 2 * (2 * (card (subterms (last b)) + card (wits b))⇧2)"
proof -
  have "card {a ∈ set b. is_literal a}
      ≤ card (pset_atoms_branch b) + card (pset_atoms_branch b)" (is "card ?A ≤ _")
  proof -
    have "?A = {AT a |a. AT a ∈ set b}
             ∪ {AF a |a. AF a ∈ set b}" (is "_ = ?ATs ∪ ?AFs")
      by auto (metis is_literal.elims(2))
    moreover have
      "?ATs ⊆ AT ` pset_atoms_branch b" "?AFs ⊆ AF ` pset_atoms_branch b"
      by force+
    moreover from calculation have "finite ?ATs" "finite ?AFs"
      by (simp_all add: finite_surj[OF finite_pset_atoms_branch])
    moreover have "?ATs ∩ ?AFs = {}"
      by auto
    ultimately show ?thesis
      by (simp add: add_mono card_Un_disjoint finite_pset_atoms_branch surj_card_le)
  qed
  then have "card ?A ≤ 2 * card (pset_atoms_branch b)"
    by simp
  moreover
  have "atoms φ ⊆
    case_prod Elem ` (subterms φ × subterms φ)
    ∪ case_prod Equal ` (subterms φ × subterms φ)" for φ :: "'a pset_fm"
  proof(induction φ)
    case (Atom x)
    then show ?case by (cases x) auto
  qed auto
  then have "pset_atoms_branch b ⊆
    case_prod Elem ` (subterms b × subterms b)
    ∪ case_prod Equal ` (subterms b × subterms b)" (is "_ ⊆ ?Els ∪ ?Eqs")
    unfolding subterms_branch_def
    by force
  have "card (pset_atoms_branch b)
    ≤ (card (subterms b))⇧2 + (card (subterms b))⇧2"
  proof -
    from finite_subterms_branch have "finite (subterms b × subterms b)"
      using finite_cartesian_product by auto
    then have "finite ?Els" "finite ?Eqs"
      by blast+
    moreover have "inj_on (case_prod Elem) A" "inj_on (case_prod Equal) A"
      for A :: "('a pset_term × 'a pset_term) set"
      unfolding inj_on_def by auto
    ultimately have "card ?Els = (card (subterms b))⇧2" "card ?Eqs = (card (subterms b))⇧2"
      using card_image[where ?A="subterms b × subterms b"] card_cartesian_product
      unfolding power2_eq_square by metis+
    with card_mono[OF _ ‹pset_atoms_branch b ⊆ ?Els ∪ ?Eqs›] show ?thesis
      using ‹finite ?Els› ‹finite ?Eqs›
      by (metis card_Un_le finite_UnI sup.boundedE sup_absorb2)
  qed
  then have "card (pset_atoms_branch b) ≤ 2 * (card (subterms b))⇧2"
    by simp
  ultimately show ?thesis
    using card_subterms_branch_ub_if_wf_branch[OF assms]
    by (meson dual_order.trans mult_le_mono2 power2_nat_le_eq_le)
qed

lemma lexpands_not_literal_mem_subfms_last:
  defines "P ≡ (λb. ∀ψ ∈ set b. ¬ is_literal ψ
                          ⟶ ψ ∈ subfms (last b) ∨ ψ ∈ Neg ` subfms (last b))"
  assumes "lexpands b' b" "b ≠ []"
  assumes "P b"
  shows "P (b' @ b)"
  using assms(2-)
  by (induction b' b rule: lexpands_induct) (fastforce simp: P_def dest: subfmsD)+

lemma bexpands_not_literal_mem_subfms_last:
  defines "P ≡ (λb. ∀ψ ∈ set b. ¬ is_literal ψ
                          ⟶ ψ ∈ subfms (last b) ∨ ψ ∈ Neg ` subfms (last b))"
  assumes "bexpands bs b" "b' ∈ bs" "b ≠ []"
  assumes "P b"
  shows "P (b' @ b)"
  using assms(2-)
proof(induction bs b rule: bexpands.induct)
  case (1 bs' b)
  then show ?case
    apply(induction rule: bexpands_nowit.induct)
        apply(fastforce simp: P_def dest: subfmsD)+
    done
next
  case (2 t1 t2 x bs' b)
  then show ?case
    apply(induction rule: bexpands_wit.induct)
    apply(fastforce simp: P_def dest: subfmsD)+
    done
qed

lemma expandss_not_literal_mem_subfms_last:
  defines "P ≡ (λb. ∀ψ ∈ set b. ¬ is_literal ψ
                          ⟶ ψ ∈ subfms (last b) ∨ ψ ∈ Neg ` subfms (last b))"
  assumes "expandss b' b" "b ≠ []"
  assumes "P b"
  shows "P b'"
  using assms(2-)
proof(induction b' b rule: expandss.induct)
  case (2 b3 b2 b1)
  then have "b2 ≠ []"
    using expandss_suffix suffix_bot.extremum_uniqueI by blast
  with 2 show ?case
    using lexpands_not_literal_mem_subfms_last unfolding P_def by blast
next
  case (3 bs b2 b3 b1)
  then have "b2 ≠ []"
    using expandss_suffix suffix_bot.extremum_uniqueI by blast
  with 3 show ?case
    using bexpands_not_literal_mem_subfms_last unfolding P_def by blast
qed simp

lemma card_not_literal_branch_if_wf_branch:
  assumes "wf_branch b"
  shows "card {φ ∈ set b. ¬ is_literal φ} ≤ 2 * card (subfms (last b))"
proof -
  from assms obtain φ where "expandss b [φ]"
    unfolding wf_branch_def by blast
  then have [simp]: "last b = φ"
    by simp
  have "{ψ ∈ set b. ¬ is_literal ψ} ⊆ subfms φ ∪ Neg ` subfms φ"
    using expandss_not_literal_mem_subfms_last[OF ‹expandss b [φ]›]
    by auto
  from card_mono[OF _ this] have
    "card {ψ ∈ set b. ¬ is_literal ψ} ≤ card (subfms φ ∪ Neg ` subfms φ)"
    using finite_subfms finite_imageI by fast
  also have "… ≤ card (subfms φ) + card (Neg ` subfms φ)"
    using card_Un_le by blast
  also have "… ≤ 2 * card (subfms φ)"
    unfolding mult_2 by (simp add: card_image_le finite_subfms)
  finally show ?thesis
    by simp
qed

lemma card_wf_branch_ub:
  assumes "wf_branch b"
  shows "card (set b)
      ≤ 2 * card (subfms (last b)) + 16 * (card (subterms (last b)))^4"
proof -
  let ?csts = "card (subterms (last b))"
  have "set b = {ψ ∈ set b. ¬ is_literal ψ} ∪ {ψ ∈ set b. is_literal ψ}"
    by auto
  then have "card (set b)
    = card ({ψ ∈ set b. ¬ is_literal ψ}) + card ({ψ ∈ set b. is_literal ψ})"
    using card_Un_disjoint finite_Un
    by (metis (no_types, lifting) List.finite_set disjoint_iff mem_Collect_eq)
  also have "… ≤ 2 * card (subfms (last b)) + 4 * (?csts + card (wits b))⇧2"
    using assms card_literals_branch_if_wf_branch card_not_literal_branch_if_wf_branch
    by fastforce
  also have "… ≤ 2 * card (subfms (last b)) + 4 * (?csts + ?csts⇧2)⇧2"
    using assms card_wits_ub_if_wf_branch by auto
  also have "… ≤ 2 * card (subfms (last b)) + 16 * ?csts^4"
  proof -
    have "1 ≤ ?csts"
      using finite_subterms_fm[THEN card_0_eq]
      by (auto intro: Suc_leI)
    then have "(?csts + ?csts⇧2)⇧2 = ?csts⇧2 + 2 * ?csts^3 + ?csts^4"
      by algebra
    also have "… ≤ ?csts⇧2 + 2 * ?csts^4 + ?csts^4"
      using power_increasing[OF _ ‹1 ≤ ?csts›] by simp
    also have "… ≤ ?csts^4 + 2 * ?csts^4 + ?csts^4"
      using power_increasing[OF _ ‹1 ≤ ?csts›] by simp
    also have "… ≤ 4 * ?csts^4"
      by simp
    finally show ?thesis
      by simp
  qed
  finally show ?thesis .
qed


section ‹The Decision Procedure›

locale mlss_proc =
  fixes lexpand :: "'a branch ⇒ 'a branch"
  assumes lexpands_lexpand:
    "¬ lin_sat b ⟹ lexpands (lexpand b) b ∧ set b ⊂ set (lexpand b @ b)"
  fixes bexpand :: "'a branch ⇒ 'a branch set"
  assumes bexpands_bexpand:
    "¬ sat b ⟹ lin_sat b ⟹ bexpands (bexpand b) b"
begin

function (domintros) mlss_proc_branch :: "'a branch ⇒ bool" where
  "¬ lin_sat b
  ⟹ mlss_proc_branch b = mlss_proc_branch (lexpand b @ b)"
| "⟦ lin_sat b; bclosed b ⟧ ⟹ mlss_proc_branch b = True"
| "⟦ ¬ sat b; bopen b; lin_sat b ⟧
  ⟹ mlss_proc_branch b = (∀b' ∈ bexpand b. mlss_proc_branch (b' @ b))"
| "⟦ lin_sat b; sat b ⟧ ⟹ mlss_proc_branch b = bclosed b"
  by auto

lemma mlss_proc_branch_dom_if_wf_branch:
  assumes "wf_branch b"
  shows "mlss_proc_branch_dom b"
proof -
  define card_ub :: "'a branch ⇒ nat" where
    "card_ub ≡ λb. 2 * card (subfms (last b)) + 16 * (card (subterms (last b)))^4"
  from assms show ?thesis
  proof(induction "card_ub b - card (set b)"
      arbitrary: b rule: less_induct)
    case less
    have less': "mlss_proc_branch_dom b'" if "set b ⊂ set b'" "expandss b' b" for b'
    proof -
      note expandss_last_eq[OF ‹expandss b' b› wf_branch_not_Nil[OF ‹wf_branch b›]] 
      then have "card_ub b' = card_ub b"
        unfolding card_ub_def by simp
      moreover from that ‹wf_branch b› have "wf_branch b'"
        by (meson expandss_trans wf_branch_def)
      ultimately have "mlss_proc_branch_dom b'" if "card (set b') > card (set b)"
        using less(1)[OF _ ‹wf_branch b'›] card_wf_branch_ub that
        by (metis (no_types, lifting) card_ub_def diff_less_mono2 order_less_le_trans)
      with that show ?thesis
        by (simp add: psubset_card_mono)
    qed
    then show ?case
    proof(cases "sat b")
      case False
      then consider
        b' where  "¬ lin_sat b" "lexpands b' b" "set b ⊂ set (b' @ b)" |
        bs' where "lin_sat b" "¬ sat b" "bexpands bs' b" "bs' ≠ {}"
                  "∀b' ∈ bs'. set b ⊂ set (b' @ b)"
        unfolding sat_def lin_sat_def
        using bexpands_strict_mono bexpands_nonempty
        by (metis (no_types, opaque_lifting) inf_sup_aci(5) psubsetI set_append sup_ge1)
      then show ?thesis
      proof(cases)
        case 1
        with less' show ?thesis 
          using mlss_proc_branch.domintros(1)
          by (metis expandss.intros(1,2) lexpands_lexpand)
      next
        case 2
        then show ?thesis
          using less' bexpands_bexpand mlss_proc_branch.domintros(2,3)
          by (metis bexpands_strict_mono expandss.intros(1,3))
      qed
    qed (use mlss_proc_branch.domintros(4) sat_def in metis)
  qed
qed

definition mlss_proc :: "'a pset_fm ⇒ bool" where
  "mlss_proc φ ≡ mlss_proc_branch [φ]"

lemma mlss_proc_branch_complete:
  fixes b :: "'a branch"
  assumes "wf_branch b" "∃v. v ⊢ last b"
  assumes "¬ mlss_proc_branch b"
  assumes "infinite (UNIV :: 'a set)"
  shows "∃M. interp I⇩s⇩a M (last b)"
proof -
  from mlss_proc_branch_dom_if_wf_branch[OF assms(1)] assms(1,2,3)
  show ?thesis
  proof(induction rule: mlss_proc_branch.pinduct)
    case (1 b)
    let ?b' = "lexpand b"
    from 1 lexpands_lexpand have "wf_branch (?b' @ b)"
      using wf_branch_lexpands by blast
    moreover from 1 lexpands_lexpand have "¬ mlss_proc_branch (?b' @ b)"
      by (simp add: mlss_proc_branch.psimps)
    ultimately obtain M where "interp I⇩s⇩a M (last (?b' @ b))"
      using 1 by auto
    with 1 show ?case
      using wf_branch_not_Nil by auto
  next
    case (2 b)
    then show ?case by (simp add: mlss_proc_branch.psimps)
  next
    case (3 b)
    let ?bs' = "bexpand b"
    from 3 bexpands_bexpand obtain b' where b': "b' ∈ ?bs'" "¬ mlss_proc_branch (b' @ b)"
      using mlss_proc_branch.psimps(3) by metis
    with 3 bexpands_bexpand have "wf_branch (b' @ b)"
      using wf_branch_expandss[OF ‹wf_branch b› expandss.intros(3)]
      using expandss.intros(1) by blast
    with 3 b' obtain M where "interp I⇩s⇩a M (last (b' @ b))"
      by auto
    with 3 show ?case
      by auto
  next
    case (4 b)
    then have "bopen b"
      by (simp add: mlss_proc_branch.psimps)
    interpret open_branch b
      using ‹wf_branch b› ‹∃v. v ⊢ last b› ‹bopen b› ‹infinite UNIV›
      by unfold_locales assumption+
    from coherence[OF ‹sat b› last_in_set] show ?case
      using wf_branch wf_branch_not_Nil by blast
  qed
qed

lemma mlss_proc_branch_sound:
  assumes "wf_branch b"
  assumes "∀ψ ∈ set b. interp I⇩s⇩a M ψ"
  shows "¬ mlss_proc_branch b"
proof
  assume "mlss_proc_branch b"
  with mlss_proc_branch_dom_if_wf_branch[OF ‹wf_branch b›]
  have "∃b'. expandss b' b ∧ (∃M. ∀ψ ∈ set b'. interp I⇩s⇩a M ψ) ∧ bclosed b'"
    using assms
  proof(induction arbitrary: M rule: mlss_proc_branch.pinduct)
    case (1 b)
    let ?b' = "lexpand b"
    from 1 lexpands_lexpand ‹wf_branch b› have "wf_branch (?b' @ b)"
      using wf_branch_lexpands by metis
    with 1 lexpands_sound lexpands_lexpand obtain b'' where
      "expandss b'' (?b' @ b)" "∃M. ∀ψ ∈ set b''. interp I⇩s⇩a M ψ" "bclosed b''"
      by (fastforce simp: mlss_proc_branch.psimps)
    with 1 lexpands_lexpand show ?case
      using expandss_trans expandss.intros(1,2) by meson
  next
    case (3 b)
    let ?bs' = "bexpand b"
    from 3 ‹wf_branch b› bexpands_bexpand have wf_branch_b':
      "wf_branch (b' @ b)" if "b' ∈ ?bs'" for b'
      using that expandss.intros(3) wf_branch_def by metis
    from bexpands_sound bexpands_bexpand 3 obtain M' b' where
      "b' ∈ ?bs'" "∀ψ ∈ set (b' @ b). interp I⇩s⇩a M' ψ"
      by metis
    with "3.IH" ‹mlss_proc_branch b› wf_branch_b' obtain b'' where
      "b' ∈ ?bs'" "expandss b'' (b' @ b)"
      "∃M. ∀ψ ∈ set b''. interp I⇩s⇩a M ψ" "bclosed b''"
      using mlss_proc_branch.psimps(3)[OF "3.hyps"(2-4,1)] by blast
    with 3 bexpands_bexpand show ?case
      using expandss_trans expandss.intros(1,3) by metis
  qed (use expandss.intros(1) mlss_proc_branch.psimps(4) in ‹blast+›)
  with bclosed_sound show False by blast
qed

theorem mlss_proc_complete:
  fixes φ :: "'a pset_fm"
  assumes "¬ mlss_proc φ"
  assumes "∃v. v ⊢ φ"
  assumes "infinite (UNIV :: 'a set)"
  shows "∃M. interp I⇩s⇩a M φ"
  using assms mlss_proc_branch_complete[of "[φ]"]
  unfolding mlss_proc_def by simp

theorem mlss_proc_sound:
  assumes "interp I⇩s⇩a M φ"
  shows "¬ mlss_proc φ"
  using assms mlss_proc_branch_sound[of "[φ]"]
  unfolding mlss_proc_def by simp

end

end