[STATEMENT]
lemma vars_clause_hd_partitioned_from_tl:
  assumes "Cs \<noteq>[]"
  shows "vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs)))
    \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Cs \<noteq> []

goal (1 subgoal):
 1. vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}
[PROOF STEP]
proof (induction Cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
case (Cons C Cs)
[PROOF STATE]
proof (state)
this:
Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}
C # Cs \<noteq> []

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
define \<sigma>' :: "nat \<Rightarrow> nat"
    where "\<sigma>' = (\<lambda>v. (Suc (v + Max ((vars_clause_list (subst_cls_lists Cs
                        (renamings_apart Cs))) \<union> {0}))))"
[PROOF STATE]
proof (state)
this:
\<sigma>' = (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0})))

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
define \<sigma> :: "nat \<Rightarrow> ('a, nat) term"
    where "\<sigma> = (\<lambda>v. Var (\<sigma>' v))"
[PROOF STATE]
proof (state)
this:
\<sigma> = (\<lambda>v. Var (\<sigma>' v))

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
have "vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (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]
using vars_in_instance_in_range_cls[of C "hd (renamings_apart (C # Cs))"] \<sigma>_def \<sigma>'_def
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C (hd (renamings_apart (C # Cs)))) \<subseteq> \<Union> (vars_term ` range (hd (renamings_apart (C # Cs))))
\<sigma> = (\<lambda>v. Var (\<sigma>' v))
\<sigma>' = (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0})))

goal (1 subgoal):
 1. vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
have "\<Union> (vars_term ` range \<sigma>)
    \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
have "range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
unfolding \<sigma>'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
using Suc_Max_notin_set
[PROOF STATE]
proof (prove)
using this:
finite ?X \<Longrightarrow> Suc (?v + Max (insert 0 ?X)) \<notin> ?X

goal (1 subgoal):
 1. range (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. \<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. \<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
unfolding \<sigma>_def \<sigma>'_def
[PROOF STATE]
proof (prove)
using this:
range (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. \<Union> (vars_term ` range (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
\<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
have "vars_clause (subst_cls C \<sigma>)
     \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
\<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

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

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars_clause (subst_cls C \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. 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)))) = {}
[PROOF STEP]
unfolding \<sigma>_def \<sigma>'_def
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. 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)))) = {}
[PROOF STEP]
unfolding subst_cls_lists_def
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C (\<lambda>v. Var (Suc (v + Max (vars_clause_list (Map2.map2 subst_cls Cs (renamings_apart Cs)) \<union> {0}))))) \<inter> vars_clause_list (Map2.map2 subst_cls Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. vars_clause (hd (Map2.map2 subst_cls (C # Cs) (renamings_apart (C # Cs)))) \<inter> vars_clause_list (tl (Map2.map2 subst_cls (C # Cs) (renamings_apart (C # Cs)))) = {}
[PROOF STEP]
by (simp add: Let_def subst_cls_lists_def)
[PROOF STATE]
proof (state)
this:
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. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
[PROOF STEP]
qed auto