[STATEMENT]
lemma reachable_constraints_fv_bvars_disj:
  fixes \<A>::"('fun,'atom,'sets,'lbl) prot_constr"
  assumes \<A>_reach: "\<A> \<in> reachable_constraints P"
    and P: "\<forall>S \<in> set P. admissible_transaction S"
  shows "fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}
[PROOF STEP]
let ?X = "\<Union>T \<in> set P. bvars_transaction T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}
[PROOF STEP]
note 0 = admissible_transactions_fv_bvars_disj[OF P]
[PROOF STATE]
proof (state)
this:
\<Union> (fv_transaction ` set P) \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}
[PROOF STEP]
have 1: "bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
using \<A>_reach
[PROOF STATE]
proof (prove)
using this:
\<A> \<in> reachable_constraints P

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
proof (induction \<A> rule: reachable_constraints.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
 2. \<And>\<A> T \<xi> \<sigma> \<alpha>. \<lbrakk>\<A> \<in> reachable_constraints P; bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P); T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \<A>; transaction_renaming_subst \<alpha> P \<A>\<rbrakk> \<Longrightarrow> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
case (step \<A> T \<xi> \<sigma> \<alpha>)
[PROOF STATE]
proof (state)
this:
\<A> \<in> reachable_constraints P
T \<in> set P
transaction_decl_subst \<xi> T
transaction_fresh_subst \<sigma> T \<A>
transaction_renaming_subst \<alpha> P \<A>
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P)

goal (2 subgoals):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
 2. \<And>\<A> T \<xi> \<sigma> \<alpha>. \<lbrakk>\<A> \<in> reachable_constraints P; bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P); T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \<A>; transaction_renaming_subst \<alpha> P \<A>\<rbrakk> \<Longrightarrow> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
have "bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T
[PROOF STEP]
using bvars\<^sub>s\<^sub>s\<^sub>t_subst[of "unlabel (transaction_strand T)" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            bvars\<^sub>s\<^sub>s\<^sub>t_unlabel_dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t_eq[of "transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            unlabel_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>s\<^sub>s\<^sub>t (unlabel (transaction_strand T) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) = bvars_transaction T
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) = dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T) \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>
unlabel (transaction_strand T) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha> = unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T

goal (2 subgoals):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
 2. \<And>\<A> T \<xi> \<sigma> \<alpha>. \<lbrakk>\<A> \<in> reachable_constraints P; bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P); T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \<A>; transaction_renaming_subst \<alpha> P \<A>\<rbrakk> \<Longrightarrow> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
hence "bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> ?X"
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
using step.hyps(2)
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T
T \<in> set P

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)

goal (2 subgoals):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
 2. \<And>\<A> T \<xi> \<sigma> \<alpha>. \<lbrakk>\<A> \<in> reachable_constraints P; bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P); T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \<A>; transaction_renaming_subst \<alpha> P \<A>\<rbrakk> \<Longrightarrow> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
using step.IH bvars\<^sub>s\<^sub>s\<^sub>t_append
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P)
bvars\<^sub>s\<^sub>s\<^sub>t (?A @ ?B) = bvars\<^sub>s\<^sub>s\<^sub>t ?A \<union> bvars\<^sub>s\<^sub>s\<^sub>t ?B

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
qed (simp add: unlabel_def)
[PROOF STATE]
proof (state)
this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P)

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}
[PROOF STEP]
have 2: "fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> ?X = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
using \<A>_reach
[PROOF STATE]
proof (prove)
using this:
\<A> \<in> reachable_constraints P

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
proof (induction \<A> rule: reachable_constraints.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
 2. \<And>\<A> T \<xi> \<sigma> \<alpha>. \<lbrakk>\<A> \<in> reachable_constraints P; fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}; T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \<A>; transaction_renaming_subst \<alpha> P \<A>\<rbrakk> \<Longrightarrow> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
case (step \<A> T \<xi> \<sigma> \<alpha>)
[PROOF STATE]
proof (state)
this:
\<A> \<in> reachable_constraints P
T \<in> set P
transaction_decl_subst \<xi> T
transaction_fresh_subst \<sigma> T \<A>
transaction_renaming_subst \<alpha> P \<A>
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (2 subgoals):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
 2. \<And>\<A> T \<xi> \<sigma> \<alpha>. \<lbrakk>\<A> \<in> reachable_constraints P; fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}; T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \<A>; transaction_renaming_subst \<alpha> P \<A>\<rbrakk> \<Longrightarrow> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
have "x \<noteq> y" when x: "x \<in> ?X" and y: "y \<in> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
obtain y' where y': "y' \<in> fv_transaction T" "y \<in> fv ((\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>y' \<in> fv_transaction T; y \<in> fv ((\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using y unlabel_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
[PROOF STATE]
proof (prove)
using this:
y \<in> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
unlabel (transaction_strand T) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha> = unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>y' \<in> fv_transaction T; y \<in> fv ((\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis fv\<^sub>s\<^sub>s\<^sub>t_subst_obtain_var)
[PROOF STATE]
proof (state)
this:
y' \<in> fv_transaction T
y \<in> fv ((\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y')

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
have "y \<notin> \<Union>(vars_transaction ` set P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> \<Union> (vars_transaction ` set P)
[PROOF STEP]
using transaction_decl_fresh_renaming_substs_range''[OF step.hyps(3-5) y'(2)]
              transaction_renaming_subst_range_notin_vars[OF step.hyps(5), of y']
[PROOF STATE]
proof (prove)
using this:
\<xi> y' = Var y'
\<sigma> y' = Var y'
\<alpha> y' = Var y
(\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y' = Var y
\<exists>y. \<alpha> y' = Var y \<and> y \<notin> \<Union> (vars_transaction ` set P) \<union> vars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A>

goal (1 subgoal):
 1. y \<notin> \<Union> (vars_transaction ` set P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<notin> \<Union> (vars_transaction ` set P)

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<notin> \<Union> (vars_transaction ` set P)

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
using x vars\<^sub>s\<^sub>s\<^sub>t_is_fv\<^sub>s\<^sub>s\<^sub>t_bvars\<^sub>s\<^sub>s\<^sub>t
[PROOF STATE]
proof (prove)
using this:
y \<notin> \<Union> (vars_transaction ` set P)
x \<in> \<Union> (bvars_transaction ` set P)
vars\<^sub>s\<^sub>s\<^sub>t ?S = fv\<^sub>s\<^sub>s\<^sub>t ?S \<union> bvars\<^sub>s\<^sub>s\<^sub>t ?S

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x24 \<in> \<Union> (bvars_transaction ` set P); ?y24 \<in> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)\<rbrakk> \<Longrightarrow> ?x24 \<noteq> ?y24

goal (2 subgoals):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
 2. \<And>\<A> T \<xi> \<sigma> \<alpha>. \<lbrakk>\<A> \<in> reachable_constraints P; fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}; T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \<A>; transaction_renaming_subst \<alpha> P \<A>\<rbrakk> \<Longrightarrow> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
hence "fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> ?X = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x24 \<in> \<Union> (bvars_transaction ` set P); ?y24 \<in> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)\<rbrakk> \<Longrightarrow> ?x24 \<noteq> ?y24

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (2 subgoals):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
 2. \<And>\<A> T \<xi> \<sigma> \<alpha>. \<lbrakk>\<A> \<in> reachable_constraints P; fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}; T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \<A>; transaction_renaming_subst \<alpha> P \<A>\<rbrakk> \<Longrightarrow> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
using step.IH
            fv\<^sub>s\<^sub>s\<^sub>t_unlabel_dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t_eq[of "transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            unlabel_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            fv\<^sub>s\<^sub>s\<^sub>t_append[of "unlabel \<A>" "unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)"]
            unlabel_append[of \<A> "transaction_strand T"]
[PROOF STATE]
proof (prove)
using this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> \<Union> (bvars_transaction ` set P) = {}
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) = dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T) \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>
unlabel (transaction_strand T) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha> = unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
fv\<^sub>s\<^sub>s\<^sub>t (unlabel \<A> @ unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<union> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
unlabel (\<A> @ transaction_strand T) = unlabel \<A> @ unlabel (transaction_strand T)

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A> @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
qed (simp add: unlabel_def)
[PROOF STATE]
proof (state)
this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}
[PROOF STEP]
using 0 1 2
[PROOF STATE]
proof (prove)
using this:
\<Union> (fv_transaction ` set P) \<inter> \<Union> (bvars_transaction ` set P) = {}
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<subseteq> \<Union> (bvars_transaction ` set P)
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> = {}

goal:
No subgoals!
[PROOF STEP]
qed