[STATEMENT]
lemma same_on_vars_lit:
  assumes "\<forall>v \<in> vars_lit L. \<sigma> v = \<tau> v"
  shows "subst_lit L \<sigma> = subst_lit L \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_lit L \<sigma> = subst_lit L \<tau>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_lit L. \<sigma> v = \<tau> v

goal (1 subgoal):
 1. subst_lit L \<sigma> = subst_lit L \<tau>
[PROOF STEP]
proof (induction L)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<forall>v\<in>vars_lit (Pos x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Pos x) \<sigma> = subst_lit (Pos x) \<tau>
 2. \<And>x. \<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>
[PROOF STEP]
case (Pos x)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>vars_lit (Pos x). \<sigma> v = \<tau> v

goal (2 subgoals):
 1. \<And>x. \<forall>v\<in>vars_lit (Pos x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Pos x) \<sigma> = subst_lit (Pos x) \<tau>
 2. \<And>x. \<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>vars_lit (Pos x). \<sigma> v = \<tau> v
[PROOF STEP]
have "\<forall>v \<in> vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_lit (Pos x). \<sigma> v = \<tau> v

goal (1 subgoal):
 1. \<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>
[PROOF STEP]
using term_subst_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_lit (Pos x). \<sigma> v = \<tau> v
(\<And>x. x \<in> vars_term ?t \<Longrightarrow> ?\<sigma> x = ?\<tau> x) \<Longrightarrow> ?t \<cdot> ?\<sigma> = ?t \<cdot> ?\<tau>

goal (1 subgoal):
 1. \<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>

goal (2 subgoals):
 1. \<And>x. \<forall>v\<in>vars_lit (Pos x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Pos x) \<sigma> = subst_lit (Pos x) \<tau>
 2. \<And>x. \<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>

goal (1 subgoal):
 1. subst_lit (Pos x) \<sigma> = subst_lit (Pos x) \<tau>
[PROOF STEP]
unfolding subst_lit_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>

goal (1 subgoal):
 1. Pos x \<cdot>lit \<sigma> = Pos x \<cdot>lit \<tau>
[PROOF STEP]
using Pos
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>
\<forall>v\<in>vars_lit (Pos x). \<sigma> v = \<tau> v

goal (1 subgoal):
 1. Pos x \<cdot>lit \<sigma> = Pos x \<cdot>lit \<tau>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_lit (Pos x) \<sigma> = subst_lit (Pos x) \<tau>

goal (1 subgoal):
 1. \<And>x. \<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>
[PROOF STEP]
case (Neg x)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v

goal (1 subgoal):
 1. \<And>x. \<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v
[PROOF STEP]
have "\<forall>v \<in> vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v

goal (1 subgoal):
 1. \<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>
[PROOF STEP]
using term_subst_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v
(\<And>x. x \<in> vars_term ?t \<Longrightarrow> ?\<sigma> x = ?\<tau> x) \<Longrightarrow> ?t \<cdot> ?\<sigma> = ?t \<cdot> ?\<tau>

goal (1 subgoal):
 1. \<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>

goal (1 subgoal):
 1. \<And>x. \<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v \<Longrightarrow> subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>

goal (1 subgoal):
 1. subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>
[PROOF STEP]
unfolding subst_lit_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>

goal (1 subgoal):
 1. Neg x \<cdot>lit \<sigma> = Neg x \<cdot>lit \<tau>
[PROOF STEP]
using Neg
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>
\<forall>v\<in>vars_lit (Neg x). \<sigma> v = \<tau> v

goal (1 subgoal):
 1. Neg x \<cdot>lit \<sigma> = Neg x \<cdot>lit \<tau>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_lit (Neg x) \<sigma> = subst_lit (Neg x) \<tau>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_list_of_mset_in_S:
  assumes "i < length (list_of_mset S)"
  shows "list_of_mset S ! i \<in># S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_of_mset S ! i \<in># S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_of_mset S ! i \<in># S
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < length (list_of_mset S)
[PROOF STEP]
have "list_of_mset S ! i \<in> set (list_of_mset S)"
[PROOF STATE]
proof (prove)
using this:
i < length (list_of_mset S)

goal (1 subgoal):
 1. list_of_mset S ! i \<in> set (list_of_mset S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_of_mset S ! i \<in> set (list_of_mset S)

goal (1 subgoal):
 1. list_of_mset S ! i \<in># S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_of_mset S ! i \<in> set (list_of_mset S)
[PROOF STEP]
have "list_of_mset S ! i \<in># mset (list_of_mset S)"
[PROOF STATE]
proof (prove)
using this:
list_of_mset S ! i \<in> set (list_of_mset S)

goal (1 subgoal):
 1. list_of_mset S ! i \<in># mset (list_of_mset S)
[PROOF STEP]
by (meson in_multiset_in_set)
[PROOF STATE]
proof (state)
this:
list_of_mset S ! i \<in># mset (list_of_mset S)

goal (1 subgoal):
 1. list_of_mset S ! i \<in># S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_of_mset S ! i \<in># mset (list_of_mset S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
list_of_mset S ! i \<in># mset (list_of_mset S)

goal (1 subgoal):
 1. list_of_mset S ! i \<in># S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_of_mset S ! i \<in># S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma same_on_vars_clause:
  assumes "\<forall>v \<in> vars_clause S. \<sigma> v = \<tau> v"
  shows "subst_cls S \<sigma> = subst_cls S \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cls S \<sigma> = subst_cls S \<tau>
[PROOF STEP]
by (smt assms image_eqI image_mset_cong2 mem_simps(9) same_on_vars_lit set_image_mset
      subst_cls_def vars_clause_def)


[STATEMENT]
lemma vars_partitioned_var_disjoint:
  assumes "vars_partitioned Cs"
  shows "var_disjoint Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var_disjoint Cs
[PROOF STEP]
unfolding var_disjoint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>s. length \<sigma>s = length Cs \<longrightarrow> (\<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>)
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>s. length \<sigma>s = length Cs \<Longrightarrow> \<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>
[PROOF STEP]
fix \<sigma>s :: \<open>('b \<Rightarrow> ('a, 'b) term) list\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>s. length \<sigma>s = length Cs \<Longrightarrow> \<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>
[PROOF STEP]
assume "length \<sigma>s = length Cs"
[PROOF STATE]
proof (state)
this:
length \<sigma>s = length Cs

goal (1 subgoal):
 1. \<And>\<sigma>s. length \<sigma>s = length Cs \<Longrightarrow> \<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>
[PROOF STEP]
with assms[unfolded vars_partitioned_def] Fun_More.fun_merge[of "map vars_clause Cs" "nth \<sigma>s"]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length Cs. \<forall>j<length Cs. i \<noteq> j \<longrightarrow> vars_clause (Cs ! i) \<inter> vars_clause (Cs ! j) = {}
\<forall>i<length (map vars_clause Cs). \<forall>j<length (map vars_clause Cs). i \<noteq> j \<longrightarrow> map vars_clause Cs ! i \<inter> map vars_clause Cs ! j = {} \<Longrightarrow> \<exists>\<sigma>. \<forall>i<length (map vars_clause Cs). \<forall>x\<in>map vars_clause Cs ! i. \<sigma> x = (\<sigma>s ! i) x
length \<sigma>s = length Cs
[PROOF STEP]
obtain \<sigma> where
    \<sigma>_p: "\<forall>i < length (map vars_clause Cs). \<forall>x \<in> map vars_clause Cs ! i. \<sigma> x = (\<sigma>s ! i) x"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length Cs. \<forall>j<length Cs. i \<noteq> j \<longrightarrow> vars_clause (Cs ! i) \<inter> vars_clause (Cs ! j) = {}
\<forall>i<length (map vars_clause Cs). \<forall>j<length (map vars_clause Cs). i \<noteq> j \<longrightarrow> map vars_clause Cs ! i \<inter> map vars_clause Cs ! j = {} \<Longrightarrow> \<exists>\<sigma>. \<forall>i<length (map vars_clause Cs). \<forall>x\<in>map vars_clause Cs ! i. \<sigma> x = (\<sigma>s ! i) x
length \<sigma>s = length Cs

goal (1 subgoal):
 1. (\<And>\<sigma>. \<forall>i<length (map vars_clause Cs). \<forall>x\<in>map vars_clause Cs ! i. \<sigma> x = (\<sigma>s ! i) x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length (map vars_clause Cs). \<forall>x\<in>map vars_clause Cs ! i. \<sigma> x = (\<sigma>s ! i) x

goal (1 subgoal):
 1. \<And>\<sigma>s. length \<sigma>s = length Cs \<Longrightarrow> \<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>
[PROOF STEP]
have "\<forall>i < length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>
[PROOF STEP]
proof (rule, rule, rule, rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i S. \<lbrakk>i < length Cs; S \<subseteq># Cs ! i\<rbrakk> \<Longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>
[PROOF STEP]
fix i :: nat and S :: "('a, 'b) term literal multiset"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i S. \<lbrakk>i < length Cs; S \<subseteq># Cs ! i\<rbrakk> \<Longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>
[PROOF STEP]
assume
      "i < length Cs" and
      "S \<subseteq># Cs ! i"
[PROOF STATE]
proof (state)
this:
i < length Cs
S \<subseteq># Cs ! i

goal (1 subgoal):
 1. \<And>i S. \<lbrakk>i < length Cs; S \<subseteq># Cs ! i\<rbrakk> \<Longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
S \<subseteq># Cs ! i
[PROOF STEP]
have "\<forall>v \<in> vars_clause S. (\<sigma>s ! i) v = \<sigma> v"
[PROOF STATE]
proof (prove)
using this:
i < length Cs
S \<subseteq># Cs ! i

goal (1 subgoal):
 1. \<forall>v\<in>vars_clause S. (\<sigma>s ! i) v = \<sigma> v
[PROOF STEP]
using vars_clause_mono[of S "Cs ! i"] \<sigma>_p
[PROOF STATE]
proof (prove)
using this:
i < length Cs
S \<subseteq># Cs ! i
S \<subseteq># Cs ! i \<Longrightarrow> vars_clause S \<subseteq> vars_clause (Cs ! i)
\<forall>i<length (map vars_clause Cs). \<forall>x\<in>map vars_clause Cs ! i. \<sigma> x = (\<sigma>s ! i) x

goal (1 subgoal):
 1. \<forall>v\<in>vars_clause S. (\<sigma>s ! i) v = \<sigma> v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>vars_clause S. (\<sigma>s ! i) v = \<sigma> v

goal (1 subgoal):
 1. \<And>i S. \<lbrakk>i < length Cs; S \<subseteq># Cs ! i\<rbrakk> \<Longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>vars_clause S. (\<sigma>s ! i) v = \<sigma> v
[PROOF STEP]
show "subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_clause S. (\<sigma>s ! i) v = \<sigma> v

goal (1 subgoal):
 1. subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>
[PROOF STEP]
using same_on_vars_clause
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_clause S. (\<sigma>s ! i) v = \<sigma> v
\<forall>v\<in>vars_clause ?S. ?\<sigma> v = ?\<tau> v \<Longrightarrow> subst_cls ?S ?\<sigma> = subst_cls ?S ?\<tau>

goal (1 subgoal):
 1. subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma>s. length \<sigma>s = length Cs \<Longrightarrow> \<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>
[PROOF STEP]
show "\<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>

goal (1 subgoal):
 1. \<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vars_in_instance_in_range_term:
  "vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
by (induction A) auto


[STATEMENT]
lemma vars_in_instance_in_range_lit: "vars_lit (subst_lit L \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_lit (subst_lit L \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
proof (induction L)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. vars_lit (subst_lit (Pos x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
 2. \<And>x. vars_lit (subst_lit (Neg x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
case (Pos A)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. vars_lit (subst_lit (Pos x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
 2. \<And>x. vars_lit (subst_lit (Neg x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
have "vars_term (A \<cdot> \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
using vars_in_instance_in_range_term[of A \<sigma>]
[PROOF STATE]
proof (prove)
using this:
vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (1 subgoal):
 1. vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (2 subgoals):
 1. \<And>x. vars_lit (subst_lit (Pos x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
 2. \<And>x. vars_lit (subst_lit (Neg x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (1 subgoal):
 1. vars_lit (subst_lit (Pos A) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_lit (subst_lit (Pos A) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (1 subgoal):
 1. \<And>x. vars_lit (subst_lit (Neg x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. vars_lit (subst_lit (Neg x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
case (Neg A)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>x. vars_lit (subst_lit (Neg x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
have "vars_term (A \<cdot> \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
using vars_in_instance_in_range_term[of A \<sigma>]
[PROOF STATE]
proof (prove)
using this:
vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (1 subgoal):
 1. vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (1 subgoal):
 1. \<And>x. vars_lit (subst_lit (Neg x) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (1 subgoal):
 1. vars_lit (subst_lit (Neg A) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_lit (subst_lit (Neg A) \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vars_in_instance_in_range_cls:
  "vars_clause (subst_cls C \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
unfolding vars_clause_def subst_cls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set_mset (image_mset vars_lit {#subst_lit A \<sigma>. A \<in># C#})) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
using vars_in_instance_in_range_lit[of _ \<sigma>]
[PROOF STATE]
proof (prove)
using this:
vars_lit (subst_lit ?L \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (1 subgoal):
 1. \<Union> (set_mset (image_mset vars_lit {#subst_lit A \<sigma>. A \<in># C#})) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
by auto


[STATEMENT]
lemma len_renamings_apart: "length (renamings_apart Cs) = length Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (renamings_apart Cs) = length Cs
[PROOF STEP]
by (induction Cs) (auto simp: Let_def)


[STATEMENT]
lemma renamings_apart_is_Var: "\<forall>\<sigma> \<in> set (renamings_apart Cs). \<forall>x. is_Var (\<sigma> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>\<in>set (renamings_apart Cs). \<forall>x. is_Var (\<sigma> x)
[PROOF STEP]
by (induction Cs) (auto simp: Let_def)


[STATEMENT]
lemma renamings_apart_inj: "\<forall>\<sigma> \<in> set (renamings_apart Cs). inj \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>\<in>set (renamings_apart Cs). inj \<sigma>
[PROOF STEP]
proof (induction Cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<sigma>\<in>set (renamings_apart []). inj \<sigma>
 2. \<And>a Cs. \<forall>\<sigma>\<in>set (renamings_apart Cs). inj \<sigma> \<Longrightarrow> \<forall>\<sigma>\<in>set (renamings_apart (a # Cs)). inj \<sigma>
[PROOF STEP]
case (Cons a Cs)
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>\<in>set (renamings_apart Cs). inj \<sigma>

goal (2 subgoals):
 1. \<forall>\<sigma>\<in>set (renamings_apart []). inj \<sigma>
 2. \<And>a Cs. \<forall>\<sigma>\<in>set (renamings_apart Cs). inj \<sigma> \<Longrightarrow> \<forall>\<sigma>\<in>set (renamings_apart (a # Cs)). inj \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<sigma>\<in>set (renamings_apart Cs). inj \<sigma>
[PROOF STEP]
have "inj (\<lambda>v. Var (Suc (v + Max (vars_clause_list
               (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<sigma>\<in>set (renamings_apart Cs). inj \<sigma>

goal (1 subgoal):
 1. inj (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))
[PROOF STEP]
by (meson add_right_imp_eq injI nat.inject term.inject(1))
[PROOF STATE]
proof (state)
this:
inj (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))

goal (2 subgoals):
 1. \<forall>\<sigma>\<in>set (renamings_apart []). inj \<sigma>
 2. \<And>a Cs. \<forall>\<sigma>\<in>set (renamings_apart Cs). inj \<sigma> \<Longrightarrow> \<forall>\<sigma>\<in>set (renamings_apart (a # Cs)). inj \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inj (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))

goal (1 subgoal):
 1. \<forall>\<sigma>\<in>set (renamings_apart (a # Cs)). inj \<sigma>
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
inj (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))
\<forall>\<sigma>\<in>set (renamings_apart Cs). inj \<sigma>

goal (1 subgoal):
 1. \<forall>\<sigma>\<in>set (renamings_apart (a # Cs)). inj \<sigma>
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>\<in>set (renamings_apart (a # Cs)). inj \<sigma>

goal (1 subgoal):
 1. \<forall>\<sigma>\<in>set (renamings_apart []). inj \<sigma>
[PROOF STEP]
qed auto


[STATEMENT]
lemma finite_vars_clause[simp]: "finite (vars_clause x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars_clause x)
[PROOF STEP]
unfolding vars_clause_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union> (set_mset (image_mset vars_lit x)))
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_vars_clause_list[simp]: "finite (vars_clause_list Cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars_clause_list Cs)
[PROOF STEP]
unfolding vars_clause_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union> (vars_clause ` set Cs))
[PROOF STEP]
by (induction Cs) auto


[STATEMENT]
lemma Suc_Max_notin_set: "finite X \<Longrightarrow> Suc (v + Max (insert 0 X)) \<notin> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X \<Longrightarrow> Suc (v + Max (insert 0 X)) \<notin> X
[PROOF STEP]
by (metis Max.boundedE Suc_n_not_le_n empty_iff finite.insertI le_add2 vimageE vimageI
      vimage_Suc_insert_0)


[STATEMENT]
lemma vars_partitioned_Nil[simp]: "vars_partitioned []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_partitioned []
[PROOF STEP]
unfolding vars_partitioned_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length []. \<forall>j<length []. i \<noteq> j \<longrightarrow> vars_clause ([] ! i) \<inter> vars_clause ([] ! j) = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma subst_cls_lists_Nil[simp]: "subst_cls_lists Cs [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cls_lists Cs [] = []
[PROOF STEP]
unfolding subst_cls_lists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Map2.map2 subst_cls Cs [] = []
[PROOF STEP]
by auto


[STATEMENT]
lemma vars_partitioned_renamings_apart: "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))
[PROOF STEP]
proof (induction Cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vars_partitioned (subst_cls_lists [] (renamings_apart []))
 2. \<And>a Cs. vars_partitioned (subst_cls_lists Cs (renamings_apart Cs)) \<Longrightarrow> vars_partitioned (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))
[PROOF STEP]
case (Cons C Cs)
[PROOF STATE]
proof (state)
this:
vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))

goal (2 subgoals):
 1. vars_partitioned (subst_cls_lists [] (renamings_apart []))
 2. \<And>a Cs. vars_partitioned (subst_cls_lists Cs (renamings_apart Cs)) \<Longrightarrow> vars_partitioned (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))

goal (2 subgoals):
 1. vars_partitioned (subst_cls_lists [] (renamings_apart []))
 2. \<And>a Cs. vars_partitioned (subst_cls_lists Cs (renamings_apart Cs)) \<Longrightarrow> vars_partitioned (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))
[PROOF STEP]
fix i :: nat and j :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vars_partitioned (subst_cls_lists [] (renamings_apart []))
 2. \<And>a Cs. vars_partitioned (subst_cls_lists Cs (renamings_apart Cs)) \<Longrightarrow> vars_partitioned (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))
[PROOF STEP]
assume ij:
      "i < Suc (length Cs)"
      "j < i"
[PROOF STATE]
proof (state)
this:
i < Suc (length Cs)
j < i

goal (2 subgoals):
 1. vars_partitioned (subst_cls_lists [] (renamings_apart []))
 2. \<And>a Cs. vars_partitioned (subst_cls_lists Cs (renamings_apart Cs)) \<Longrightarrow> vars_partitioned (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))
[PROOF STEP]
have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
proof (cases i; cases j)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = 0; j = Suc nat\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 4. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
fix j' :: nat
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = 0; j = Suc nat\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 4. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
assume i'j':
        "i = 0"
        "j = Suc j'"
[PROOF STATE]
proof (state)
this:
i = 0
j = Suc j'

goal (4 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = 0; j = Suc nat\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 4. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0
j = Suc j'
[PROOF STEP]
show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}"
[PROOF STATE]
proof (prove)
using this:
i = 0
j = Suc j'

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
i = 0
j = Suc j'
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
fix i' :: nat
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
assume i'j':
        "i = Suc i'"
        "j = 0"
[PROOF STATE]
proof (state)
this:
i = Suc i'
j = 0

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
have disjoin_C_Cs: "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter>
        vars_clause_list ((subst_cls_lists Cs (renamings_apart Cs))) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
using vars_clause_hd_partitioned_from_tl[of "C # Cs"]
[PROOF STATE]
proof (prove)
using this:
C # Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))) = {}

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
by (simp add: Let_def subst_cls_lists_def)
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
assume asm: "x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')"
[PROOF STATE]
proof (state)
this:
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
[PROOF STEP]
have "(subst_cls_lists Cs (renamings_apart Cs) ! i')
          \<in> set (subst_cls_lists Cs (renamings_apart Cs))"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')

goal (1 subgoal):
 1. subst_cls_lists Cs (renamings_apart Cs) ! i' \<in> set (subst_cls_lists Cs (renamings_apart Cs))
[PROOF STEP]
using i'j' ij
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
i = Suc i'
j = 0
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. subst_cls_lists Cs (renamings_apart Cs) ! i' \<in> set (subst_cls_lists Cs (renamings_apart Cs))
[PROOF STEP]
unfolding subst_cls_lists_def
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_clause (Map2.map2 subst_cls Cs (renamings_apart Cs) ! i')
i = Suc i'
j = 0
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. Map2.map2 subst_cls Cs (renamings_apart Cs) ! i' \<in> set (Map2.map2 subst_cls Cs (renamings_apart Cs))
[PROOF STEP]
by (metis Suc_less_SucD length_map len_renamings_apart length_zip min_less_iff_conj
              nth_mem)
[PROOF STATE]
proof (state)
this:
subst_cls_lists Cs (renamings_apart Cs) ! i' \<in> set (subst_cls_lists Cs (renamings_apart Cs))

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
subst_cls_lists Cs (renamings_apart Cs) ! i' \<in> set (subst_cls_lists Cs (renamings_apart Cs))

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
[PROOF STEP]
have
          "x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')

goal (1 subgoal):
 1. x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
[PROOF STEP]
using i'j' ij
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
i = Suc i'
j = 0
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
[PROOF STEP]
unfolding subst_cls_lists_def
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_clause (Map2.map2 subst_cls Cs (renamings_apart Cs) ! i')
i = Suc i'
j = 0
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. x \<in> vars_clause (Map2.map2 subst_cls Cs (renamings_apart Cs) ! i')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
subst_cls_lists Cs (renamings_apart Cs) ! i' \<in> set (subst_cls_lists Cs (renamings_apart Cs))
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
[PROOF STEP]
have "\<exists>D \<in> set (subst_cls_lists Cs (renamings_apart Cs)). x \<in> vars_clause D"
[PROOF STATE]
proof (prove)
using this:
subst_cls_lists Cs (renamings_apart Cs) ! i' \<in> set (subst_cls_lists Cs (renamings_apart Cs))
x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')

goal (1 subgoal):
 1. \<exists>D\<in>set (subst_cls_lists Cs (renamings_apart Cs)). x \<in> vars_clause D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>D\<in>set (subst_cls_lists Cs (renamings_apart Cs)). x \<in> vars_clause D

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<Longrightarrow> \<exists>D\<in>set (subst_cls_lists Cs (renamings_apart Cs)). ?x2 \<in> vars_clause D

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<Longrightarrow> \<exists>D\<in>set (subst_cls_lists Cs (renamings_apart Cs)). ?x2 \<in> vars_clause D
[PROOF STEP]
have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
        \<subseteq> Union (set (map vars_clause ((subst_cls_lists Cs (renamings_apart Cs)))))"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<Longrightarrow> \<exists>D\<in>set (subst_cls_lists Cs (renamings_apart Cs)). ?x2 \<in> vars_clause D

goal (1 subgoal):
 1. vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<subseteq> \<Union> (set (map vars_clause (subst_cls_lists Cs (renamings_apart Cs))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<subseteq> \<Union> (set (map vars_clause (subst_cls_lists Cs (renamings_apart Cs))))

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<subseteq> \<Union> (set (map vars_clause (subst_cls_lists Cs (renamings_apart Cs))))
[PROOF STEP]
have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter>
        vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') =
        {}"
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<subseteq> \<Union> (set (map vars_clause (subst_cls_lists Cs (renamings_apart Cs))))

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}
[PROOF STEP]
using disjoin_C_Cs
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<subseteq> \<Union> (set (map vars_clause (subst_cls_lists Cs (renamings_apart Cs))))
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}
[PROOF STEP]
unfolding vars_clause_list_def
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<subseteq> \<Union> (set (map vars_clause (subst_cls_lists Cs (renamings_apart Cs))))
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> \<Union> (vars_clause ` set (subst_cls_lists Cs (renamings_apart Cs))) = {}

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
have "subst_cls_lists Cs (renamings_apart Cs) ! i' =
        subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cls_lists Cs (renamings_apart Cs) ! i' = subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i
[PROOF STEP]
using i'j' ij
[PROOF STATE]
proof (prove)
using this:
i = Suc i'
j = 0
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. subst_cls_lists Cs (renamings_apart Cs) ! i' = subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i
[PROOF STEP]
unfolding subst_cls_lists_def
[PROOF STATE]
proof (prove)
using this:
i = Suc i'
j = 0
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. Map2.map2 subst_cls Cs (renamings_apart Cs) ! i' = Map2.map2 subst_cls (C # Cs) (renamings_apart (C # Cs)) ! i
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
subst_cls_lists Cs (renamings_apart Cs) ! i' = subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i

goal (3 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat. \<lbrakk>i = Suc nat; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 3. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}
subst_cls_lists Cs (renamings_apart Cs) ! i' = subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i
[PROOF STEP]
show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}"
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}
subst_cls_lists Cs (renamings_apart Cs) ! i' = subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
using i'j'
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') = {}
subst_cls_lists Cs (renamings_apart Cs) ! i' = subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i
i = Suc i'
j = 0

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
by (simp add: Int_commute)
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}

goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
fix i' :: nat and j' :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
assume i'j':
        "i = Suc i'"
        "j = Suc j'"
[PROOF STATE]
proof (state)
this:
i = Suc i'
j = Suc j'

goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
have "i'<length (subst_cls_lists Cs (renamings_apart Cs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < length (subst_cls_lists Cs (renamings_apart Cs))
[PROOF STEP]
using ij i'j'
[PROOF STATE]
proof (prove)
using this:
i < Suc (length Cs)
j < i
i = Suc i'
j = Suc j'

goal (1 subgoal):
 1. i' < length (subst_cls_lists Cs (renamings_apart Cs))
[PROOF STEP]
unfolding subst_cls_lists_def
[PROOF STATE]
proof (prove)
using this:
i < Suc (length Cs)
j < i
i = Suc i'
j = Suc j'

goal (1 subgoal):
 1. i' < length (Map2.map2 subst_cls Cs (renamings_apart Cs))
[PROOF STEP]
by (auto simp: len_renamings_apart)
[PROOF STATE]
proof (state)
this:
i' < length (subst_cls_lists Cs (renamings_apart Cs))

goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i' < length (subst_cls_lists Cs (renamings_apart Cs))

goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
have "j'<length (subst_cls_lists Cs (renamings_apart Cs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j' < length (subst_cls_lists Cs (renamings_apart Cs))
[PROOF STEP]
using ij i'j'
[PROOF STATE]
proof (prove)
using this:
i < Suc (length Cs)
j < i
i = Suc i'
j = Suc j'

goal (1 subgoal):
 1. j' < length (subst_cls_lists Cs (renamings_apart Cs))
[PROOF STEP]
unfolding subst_cls_lists_def
[PROOF STATE]
proof (prove)
using this:
i < Suc (length Cs)
j < i
i = Suc i'
j = Suc j'

goal (1 subgoal):
 1. j' < length (Map2.map2 subst_cls Cs (renamings_apart Cs))
[PROOF STEP]
by (auto simp: len_renamings_apart)
[PROOF STATE]
proof (state)
this:
j' < length (subst_cls_lists Cs (renamings_apart Cs))

goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j' < length (subst_cls_lists Cs (renamings_apart Cs))

goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
have "i' \<noteq> j'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<noteq> j'
[PROOF STEP]
using \<open>i = Suc i'\<close> \<open>j = Suc j'\<close> ij
[PROOF STATE]
proof (prove)
using this:
i = Suc i'
j = Suc j'
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. i' \<noteq> j'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i' \<noteq> j'

goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i' < length (subst_cls_lists Cs (renamings_apart Cs))
j' < length (subst_cls_lists Cs (renamings_apart Cs))
i' \<noteq> j'
[PROOF STEP]
have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter>
          vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') =
          {}"
[PROOF STATE]
proof (prove)
using this:
i' < length (subst_cls_lists Cs (renamings_apart Cs))
j' < length (subst_cls_lists Cs (renamings_apart Cs))
i' \<noteq> j'

goal (1 subgoal):
 1. vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
i' < length (subst_cls_lists Cs (renamings_apart Cs))
j' < length (subst_cls_lists Cs (renamings_apart Cs))
i' \<noteq> j'
vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))

goal (1 subgoal):
 1. vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}
[PROOF STEP]
unfolding vars_partitioned_def
[PROOF STATE]
proof (prove)
using this:
i' < length (subst_cls_lists Cs (renamings_apart Cs))
j' < length (subst_cls_lists Cs (renamings_apart Cs))
i' \<noteq> j'
\<forall>i<length (subst_cls_lists Cs (renamings_apart Cs)). \<forall>j<length (subst_cls_lists Cs (renamings_apart Cs)). i \<noteq> j \<longrightarrow> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i) \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j) = {}

goal (1 subgoal):
 1. vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}

goal (2 subgoals):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
 2. \<And>nat nata. \<lbrakk>i = Suc nat; j = Suc nata\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}
[PROOF STEP]
show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}"
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
unfolding i'j'
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') = {}

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! Suc i') \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! Suc j') = {}
[PROOF STEP]
by (simp add: subst_cls_lists_def Let_def)
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}

goal (1 subgoal):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
assume
        \<open>i = 0\<close> and
        \<open>j = 0\<close>
[PROOF STATE]
proof (state)
this:
i = 0
j = 0

goal (1 subgoal):
 1. \<lbrakk>i = 0; j = 0\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0
j = 0
[PROOF STEP]
show \<open>vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}\<close>
[PROOF STATE]
proof (prove)
using this:
i = 0
j = 0

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
i = 0
j = 0
i < Suc (length Cs)
j < i

goal (1 subgoal):
 1. vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}

goal (2 subgoals):
 1. vars_partitioned (subst_cls_lists [] (renamings_apart []))
 2. \<And>a Cs. vars_partitioned (subst_cls_lists Cs (renamings_apart Cs)) \<Longrightarrow> vars_partitioned (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < Suc (length Cs); ?j2 < ?i2\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! ?i2) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! ?j2) = {}

goal (2 subgoals):
 1. vars_partitioned (subst_cls_lists [] (renamings_apart []))
 2. \<And>a Cs. vars_partitioned (subst_cls_lists Cs (renamings_apart Cs)) \<Longrightarrow> vars_partitioned (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i2 < Suc (length Cs); ?j2 < ?i2\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! ?i2) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! ?j2) = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i2 < Suc (length Cs); ?j2 < ?i2\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! ?i2) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! ?j2) = {}

goal (1 subgoal):
 1. vars_partitioned (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))
[PROOF STEP]
unfolding vars_partitioned_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i2 < Suc (length Cs); ?j2 < ?i2\<rbrakk> \<Longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! ?i2) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! ?j2) = {}

goal (1 subgoal):
 1. \<forall>i<length (subst_cls_lists (C # Cs) (renamings_apart (C # Cs))). \<forall>j<length (subst_cls_lists (C # Cs) (renamings_apart (C # Cs))). i \<noteq> j \<longrightarrow> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter> vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) = {}
[PROOF STEP]
by (metis (no_types, lifting) Int_commute Suc_lessI len_renamings_apart length_map
        length_nth_simps(2) length_zip min.idem nat.inject not_less_eq subst_cls_lists_def)
[PROOF STATE]
proof (state)
this:
vars_partitioned (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))

goal (1 subgoal):
 1. vars_partitioned (subst_cls_lists [] (renamings_apart []))
[PROOF STEP]
qed auto


[STATEMENT]
lemma class_linorder_compare: "class.linorder (le_of_comp compare) (lt_of_comp compare)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder (le_of_comp compare) (lt_of_comp compare)
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y. lt_of_comp compare x y = strict (le_of_comp compare) x y
 2. \<And>x. le_of_comp compare x x
 3. \<And>x y z. \<lbrakk>le_of_comp compare x y; le_of_comp compare y z\<rbrakk> \<Longrightarrow> le_of_comp compare x z
 4. \<And>x y. \<lbrakk>le_of_comp compare x y; le_of_comp compare y x\<rbrakk> \<Longrightarrow> x = y
 5. \<And>x y. le_of_comp compare x y \<or> le_of_comp compare y x
[PROOF STEP]
apply (simp_all add: lt_of_comp_def le_of_comp_def split: order.splits)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y. compare y x = Lt \<longrightarrow> compare x y \<noteq> Lt
 2. \<And>x y z. \<lbrakk>compare x y = Lt; compare y z = Lt\<rbrakk> \<Longrightarrow> compare x z \<noteq> Gt
 3. \<And>x y. \<lbrakk>compare x y = Lt; compare y x = Lt\<rbrakk> \<Longrightarrow> x = y
 4. \<And>x y. compare x y = Gt \<longrightarrow> compare y x \<noteq> Gt
[PROOF STEP]
apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>compare x y = Lt; compare y z = Lt\<rbrakk> \<Longrightarrow> compare x z \<noteq> Gt
 2. \<And>x y. \<lbrakk>compare x y = Lt; compare y x = Lt\<rbrakk> \<Longrightarrow> x = y
 3. \<And>x y. compare x y = Gt \<longrightarrow> compare y x \<noteq> Gt
[PROOF STEP]
apply (metis comparator_compare comparator_def order.distinct(5))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>compare x y = Lt; compare y x = Lt\<rbrakk> \<Longrightarrow> x = y
 2. \<And>x y. compare x y = Gt \<longrightarrow> compare y x \<noteq> Gt
[PROOF STEP]
apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. compare x y = Gt \<longrightarrow> compare y x \<noteq> Gt
[PROOF STEP]
by (metis comparator.sym comparator_compare invert_order.simps(2) order.distinct(5))


[STATEMENT]
lemma unifies_all_pairs_iff:
  "(\<forall>p \<in> set (pairs xs). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) \<longleftrightarrow> (\<forall>a \<in> set xs. \<forall>b \<in> set xs. a \<cdot> \<sigma> = b \<cdot> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p\<in>set (pairs xs). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set xs. \<forall>b\<in>set xs. a \<cdot> \<sigma> = b \<cdot> \<sigma>)
[PROOF STEP]
proof (induct xs rule: pairs.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y xs. (\<forall>p\<in>set (pairs (y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (y # xs). \<forall>b\<in>set (y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>) \<Longrightarrow> (\<forall>p\<in>set (pairs (x # y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (x # y # xs). \<forall>b\<in>set (x # y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>)
 2. (\<forall>p\<in>set (pairs []). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set []. \<forall>b\<in>set []. a \<cdot> \<sigma> = b \<cdot> \<sigma>)
 3. \<And>v. (\<forall>p\<in>set (pairs [v]). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set [v]. \<forall>b\<in>set [v]. a \<cdot> \<sigma> = b \<cdot> \<sigma>)
[PROOF STEP]
case (1 x y xs)
[PROOF STATE]
proof (state)
this:
(\<forall>p\<in>set (pairs (y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (y # xs). \<forall>b\<in>set (y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>)

goal (3 subgoals):
 1. \<And>x y xs. (\<forall>p\<in>set (pairs (y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (y # xs). \<forall>b\<in>set (y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>) \<Longrightarrow> (\<forall>p\<in>set (pairs (x # y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (x # y # xs). \<forall>b\<in>set (x # y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>)
 2. (\<forall>p\<in>set (pairs []). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set []. \<forall>b\<in>set []. a \<cdot> \<sigma> = b \<cdot> \<sigma>)
 3. \<And>v. (\<forall>p\<in>set (pairs [v]). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set [v]. \<forall>b\<in>set [v]. a \<cdot> \<sigma> = b \<cdot> \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>p\<in>set (pairs (y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (y # xs). \<forall>b\<in>set (y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<forall>p\<in>set (pairs (y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (y # xs). \<forall>b\<in>set (y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>)

goal (1 subgoal):
 1. (\<forall>p\<in>set (pairs (x # y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (x # y # xs). \<forall>b\<in>set (x # y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>)
[PROOF STEP]
unfolding pairs.simps list.set ball_Un ball_simps simp_thms fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
(\<forall>p\<in>set (pairs (y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = ((\<forall>b\<in>set xs. y \<cdot> \<sigma> = b \<cdot> \<sigma>) \<and> (\<forall>a\<in>set xs. a \<cdot> \<sigma> = y \<cdot> \<sigma> \<and> (\<forall>b\<in>set xs. a \<cdot> \<sigma> = b \<cdot> \<sigma>)))

goal (1 subgoal):
 1. (x \<cdot> \<sigma> = y \<cdot> \<sigma> \<and> (\<forall>p\<in>set (pairs (y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>)) = ((x \<cdot> \<sigma> = y \<cdot> \<sigma> \<and> (\<forall>b\<in>set xs. x \<cdot> \<sigma> = b \<cdot> \<sigma>)) \<and> (y \<cdot> \<sigma> = x \<cdot> \<sigma> \<and> (\<forall>b\<in>set xs. y \<cdot> \<sigma> = b \<cdot> \<sigma>)) \<and> (\<forall>a\<in>set xs. a \<cdot> \<sigma> = x \<cdot> \<sigma> \<and> a \<cdot> \<sigma> = y \<cdot> \<sigma> \<and> (\<forall>b\<in>set xs. a \<cdot> \<sigma> = b \<cdot> \<sigma>)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<forall>p\<in>set (pairs (x # y # xs)). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set (x # y # xs). \<forall>b\<in>set (x # y # xs). a \<cdot> \<sigma> = b \<cdot> \<sigma>)

goal (2 subgoals):
 1. (\<forall>p\<in>set (pairs []). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set []. \<forall>b\<in>set []. a \<cdot> \<sigma> = b \<cdot> \<sigma>)
 2. \<And>v. (\<forall>p\<in>set (pairs [v]). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) = (\<forall>a\<in>set [v]. \<forall>b\<in>set [v]. a \<cdot> \<sigma> = b \<cdot> \<sigma>)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma in_pair_in_set:
  assumes "(A,B) \<in> set ((pairs As))"
  shows "A \<in> set As \<and> B \<in> set As"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> set As \<and> B \<in> set As
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(A, B) \<in> set (pairs As)

goal (1 subgoal):
 1. A \<in> set As \<and> B \<in> set As
[PROOF STEP]
proof (induction As)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (A, B) \<in> set (pairs []) \<Longrightarrow> A \<in> set [] \<and> B \<in> set []
 2. \<And>a As. \<lbrakk>(A, B) \<in> set (pairs As) \<Longrightarrow> A \<in> set As \<and> B \<in> set As; (A, B) \<in> set (pairs (a # As))\<rbrakk> \<Longrightarrow> A \<in> set (a # As) \<and> B \<in> set (a # As)
[PROOF STEP]
case (Cons A As)
[PROOF STATE]
proof (state)
this:
(A, B) \<in> set (pairs As) \<Longrightarrow> A \<in> set As \<and> B \<in> set As
(A, B) \<in> set (pairs (A # As))

goal (2 subgoals):
 1. (A, B) \<in> set (pairs []) \<Longrightarrow> A \<in> set [] \<and> B \<in> set []
 2. \<And>a As. \<lbrakk>(A, B) \<in> set (pairs As) \<Longrightarrow> A \<in> set As \<and> B \<in> set As; (A, B) \<in> set (pairs (a # As))\<rbrakk> \<Longrightarrow> A \<in> set (a # As) \<and> B \<in> set (a # As)
[PROOF STEP]
note Cons_outer = this
[PROOF STATE]
proof (state)
this:
(A, B) \<in> set (pairs As) \<Longrightarrow> A \<in> set As \<and> B \<in> set As
(A, B) \<in> set (pairs (A # As))

goal (2 subgoals):
 1. (A, B) \<in> set (pairs []) \<Longrightarrow> A \<in> set [] \<and> B \<in> set []
 2. \<And>a As. \<lbrakk>(A, B) \<in> set (pairs As) \<Longrightarrow> A \<in> set As \<and> B \<in> set As; (A, B) \<in> set (pairs (a # As))\<rbrakk> \<Longrightarrow> A \<in> set (a # As) \<and> B \<in> set (a # As)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
proof (cases As)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. As = [] \<Longrightarrow> A \<in> set (A # As) \<and> B \<in> set (A # As)
 2. \<And>a list. As = a # list \<Longrightarrow> A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
As = []

goal (2 subgoals):
 1. As = [] \<Longrightarrow> A \<in> set (A # As) \<and> B \<in> set (A # As)
 2. \<And>a list. As = a # list \<Longrightarrow> A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
As = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
As = []

goal (1 subgoal):
 1. A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
using Cons_outer
[PROOF STATE]
proof (prove)
using this:
As = []
(A, B) \<in> set (pairs As) \<Longrightarrow> A \<in> set As \<and> B \<in> set As
(A, B) \<in> set (pairs (A # As))

goal (1 subgoal):
 1. A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> set (A # As) \<and> B \<in> set (A # As)

goal (1 subgoal):
 1. \<And>a list. As = a # list \<Longrightarrow> A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. As = a # list \<Longrightarrow> A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
case (Cons B As')
[PROOF STATE]
proof (state)
this:
As = B # As'

goal (1 subgoal):
 1. \<And>a list. As = a # list \<Longrightarrow> A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
As = B # As'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
As = B # As'

goal (1 subgoal):
 1. A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
using Cons_outer
[PROOF STATE]
proof (prove)
using this:
As = B # As'
(A, B) \<in> set (pairs As) \<Longrightarrow> A \<in> set As \<and> B \<in> set As
(A, B) \<in> set (pairs (A # As))

goal (1 subgoal):
 1. A \<in> set (A # As) \<and> B \<in> set (A # As)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> set (A # As) \<and> B \<in> set (A # As)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<in> set (A # As) \<and> B \<in> set (A # As)

goal (1 subgoal):
 1. (A, B) \<in> set (pairs []) \<Longrightarrow> A \<in> set [] \<and> B \<in> set []
[PROOF STEP]
qed auto


[STATEMENT]
lemma in_pairs_sorted_list_of_set_in_set:
  assumes
    "finite AAA"
    "\<forall>AA \<in> AAA. finite AA"
    "AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA" and
    "(A :: _ :: compare, B) \<in> set AB_pairs"
  shows "\<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite AAA
\<forall>AA\<in>AAA. finite AA
AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA
(A, B) \<in> set AB_pairs
[PROOF STEP]
have "AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA"
[PROOF STATE]
proof (prove)
using this:
finite AAA
\<forall>AA\<in>AAA. finite AA
AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA
(A, B) \<in> set AB_pairs

goal (1 subgoal):
 1. AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA

goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA
[PROOF STEP]
obtain AA where
    AA_p: "AA \<in> AAA \<and> (pairs \<circ> compare_linorder.sorted_list_of_set) AA = AB_pairs"
[PROOF STATE]
proof (prove)
using this:
AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA

goal (1 subgoal):
 1. (\<And>AA. AA \<in> AAA \<and> (pairs \<circ> compare_linorder.sorted_list_of_set) AA = AB_pairs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AA \<in> AAA \<and> (pairs \<circ> compare_linorder.sorted_list_of_set) AA = AB_pairs

goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
have "(A, B) \<in> set (pairs (compare_linorder.sorted_list_of_set AA))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, B) \<in> set (pairs (compare_linorder.sorted_list_of_set AA))
[PROOF STEP]
using AA_p[] assms(4)
[PROOF STATE]
proof (prove)
using this:
AA \<in> AAA \<and> (pairs \<circ> compare_linorder.sorted_list_of_set) AA = AB_pairs
(A, B) \<in> set AB_pairs

goal (1 subgoal):
 1. (A, B) \<in> set (pairs (compare_linorder.sorted_list_of_set AA))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A, B) \<in> set (pairs (compare_linorder.sorted_list_of_set AA))

goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(A, B) \<in> set (pairs (compare_linorder.sorted_list_of_set AA))
[PROOF STEP]
have "A \<in> set (compare_linorder.sorted_list_of_set AA)" and
    "B \<in> set (compare_linorder.sorted_list_of_set AA)"
[PROOF STATE]
proof (prove)
using this:
(A, B) \<in> set (pairs (compare_linorder.sorted_list_of_set AA))

goal (1 subgoal):
 1. A \<in> set (compare_linorder.sorted_list_of_set AA) &&& B \<in> set (compare_linorder.sorted_list_of_set AA)
[PROOF STEP]
using in_pair_in_set[of A]
[PROOF STATE]
proof (prove)
using this:
(A, B) \<in> set (pairs (compare_linorder.sorted_list_of_set AA))
(A, ?B) \<in> set (pairs ?As) \<Longrightarrow> A \<in> set ?As \<and> ?B \<in> set ?As

goal (1 subgoal):
 1. A \<in> set (compare_linorder.sorted_list_of_set AA) &&& B \<in> set (compare_linorder.sorted_list_of_set AA)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> set (compare_linorder.sorted_list_of_set AA)
B \<in> set (compare_linorder.sorted_list_of_set AA)

goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> set (compare_linorder.sorted_list_of_set AA)
B \<in> set (compare_linorder.sorted_list_of_set AA)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<in> set (compare_linorder.sorted_list_of_set AA)
B \<in> set (compare_linorder.sorted_list_of_set AA)

goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
using assms(2) AA_p
[PROOF STATE]
proof (prove)
using this:
A \<in> set (compare_linorder.sorted_list_of_set AA)
B \<in> set (compare_linorder.sorted_list_of_set AA)
\<forall>AA\<in>AAA. finite AA
AA \<in> AAA \<and> (pairs \<circ> compare_linorder.sorted_list_of_set) AA = AB_pairs

goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA

goal:
No subgoals!
[PROOF STEP]
qed