[STATEMENT]
lemma ptrm_prm_agreement_equiv:
  assumes "\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M"
  shows "\<pi> \<bullet> M \<approx> \<sigma> \<bullet> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs M

goal (1 subgoal):
 1. \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M
[PROOF STEP]
proof(induction M arbitrary: \<pi> \<sigma>)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs PUnit) \<Longrightarrow> \<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit
 2. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 4. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 5. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 7. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PUnit)
[PROOF STATE]
proof (state)
this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs PUnit

goal (7 subgoals):
 1. \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs PUnit) \<Longrightarrow> \<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit
 2. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 4. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 5. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 7. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs PUnit

goal (1 subgoal):
 1. \<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit
[PROOF STEP]
using ptrm_alpha_equiv.unit
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs PUnit
PUnit \<approx> PUnit

goal (1 subgoal):
 1. \<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PUnit \<approx> \<sigma> \<bullet> PUnit

goal (6 subgoals):
 1. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 3. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 4. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 3. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 4. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PVar x)
[PROOF STATE]
proof (state)
this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PVar x)

goal (6 subgoals):
 1. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 3. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 4. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
consider "x \<in> ds \<pi> \<sigma>" | "x \<notin> ds \<pi> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> ds \<pi> \<sigma> \<Longrightarrow> thesis; x \<notin> ds \<pi> \<sigma> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<in> ds \<pi> \<sigma> \<Longrightarrow> ?thesis; x \<notin> ds \<pi> \<sigma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (6 subgoals):
 1. \<And>x \<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PVar x)) \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 3. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 4. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 6. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> ds \<pi> \<sigma> \<Longrightarrow> ?thesis; x \<notin> ds \<pi> \<sigma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x \<in> ds \<pi> \<sigma>

goal (2 subgoals):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
hence "x \<notin> ptrm_fvs (PVar x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. x \<notin> ptrm_fvs (PVar x)
[PROOF STEP]
using PVar.prems
[PROOF STATE]
proof (prove)
using this:
x \<in> ds \<pi> \<sigma>
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PVar x)

goal (1 subgoal):
 1. x \<notin> ptrm_fvs (PVar x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<notin> ptrm_fvs (PVar x)

goal (2 subgoals):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
 2. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> ptrm_fvs (PVar x)

goal (1 subgoal):
 1. \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x

goal (1 subgoal):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x \<notin> ds \<pi> \<sigma>

goal (1 subgoal):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
hence "\<pi> $ x = \<sigma> $ x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<pi> $ x = \<sigma> $ x
[PROOF STEP]
using prm_disagreement_ext
[PROOF STATE]
proof (prove)
using this:
x \<notin> ds \<pi> \<sigma>
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x

goal (1 subgoal):
 1. \<pi> $ x = \<sigma> $ x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi> $ x = \<sigma> $ x

goal (1 subgoal):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x = \<sigma> $ x

goal (1 subgoal):
 1. \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
using ptrm_alpha_equiv.var
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x = \<sigma> $ x
PVar ?x \<approx> PVar ?x

goal (1 subgoal):
 1. \<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PVar x \<approx> \<sigma> \<bullet> PVar x

goal (5 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 2. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 2. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PApp A B)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs B) \<Longrightarrow> ?\<pi> \<bullet> B \<approx> ?\<sigma> \<bullet> B
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PApp A B)

goal (5 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 2. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
hence "\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A" and "\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B"
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs B) \<Longrightarrow> ?\<pi> \<bullet> B \<approx> ?\<sigma> \<bullet> B
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PApp A B)

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> \<sigma> \<bullet> A &&& \<pi> \<bullet> B \<approx> \<sigma> \<bullet> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B

goal (5 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PApp M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PApp M1 M2 \<approx> \<sigma> \<bullet> PApp M1 M2
 2. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 3. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 5. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B

goal (1 subgoal):
 1. \<pi> \<bullet> PApp A B \<approx> \<sigma> \<bullet> PApp A B
[PROOF STEP]
using ptrm_alpha_equiv.app
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B
\<lbrakk>?A \<approx> ?B; ?C \<approx> ?D\<rbrakk> \<Longrightarrow> PApp ?A ?C \<approx> PApp ?B ?D

goal (1 subgoal):
 1. \<pi> \<bullet> PApp A B \<approx> \<sigma> \<bullet> PApp A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PApp A B \<approx> \<sigma> \<bullet> PApp A B

goal (4 subgoals):
 1. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PFn x T A)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)

goal (4 subgoals):
 1. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
consider "x \<notin> ds \<pi> \<sigma>" | "x \<in> ds \<pi> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> ds \<pi> \<sigma> \<Longrightarrow> thesis; x \<in> ds \<pi> \<sigma> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<notin> ds \<pi> \<sigma> \<Longrightarrow> ?thesis; x \<in> ds \<pi> \<sigma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (4 subgoals):
 1. \<And>x1 x2a M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFn x1 x2a M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFn x1 x2a M \<approx> \<sigma> \<bullet> PFn x1 x2a M
 2. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 4. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<notin> ds \<pi> \<sigma> \<Longrightarrow> ?thesis; x \<in> ds \<pi> \<sigma> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
 2. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x \<notin> ds \<pi> \<sigma>

goal (2 subgoals):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
 2. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
hence *: "\<pi> $ x = \<sigma> $ x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<pi> $ x = \<sigma> $ x
[PROOF STEP]
using prm_disagreement_ext
[PROOF STATE]
proof (prove)
using this:
x \<notin> ds \<pi> \<sigma>
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x

goal (1 subgoal):
 1. \<pi> $ x = \<sigma> $ x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi> $ x = \<sigma> $ x

goal (2 subgoals):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
 2. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
have "\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
assume "a \<in> ds \<pi> \<sigma>"
[PROOF STATE]
proof (state)
this:
a \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
hence "a \<notin> ptrm_fvs (PFn x T A)"
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. a \<notin> ptrm_fvs (PFn x T A)
[PROOF STEP]
using PFn.prems
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> \<sigma>
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. a \<notin> ptrm_fvs (PFn x T A)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
hence "a = x \<or> a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
using this:
a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. a = x \<or> a \<notin> ptrm_fvs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = x \<or> a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
thus "a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
using this:
a = x \<or> a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. a \<notin> ptrm_fvs A
[PROOF STEP]
using \<open>a \<in> ds \<pi> \<sigma>\<close> \<open>x \<notin> ds \<pi> \<sigma>\<close>
[PROOF STATE]
proof (prove)
using this:
a = x \<or> a \<notin> ptrm_fvs A
a \<in> ds \<pi> \<sigma>
x \<notin> ds \<pi> \<sigma>

goal (1 subgoal):
 1. a \<notin> ptrm_fvs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> ptrm_fvs A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs A

goal (2 subgoals):
 1. x \<notin> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
 2. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
using PFn.IH * ptrm_alpha_equiv.fn1 ptrm_apply_prm.simps(3)
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
\<pi> $ x = \<sigma> $ x
?A \<approx> ?B \<Longrightarrow> PFn ?x ?T ?A \<approx> PFn ?x ?T ?B
?\<pi> \<bullet> PApp ?A ?B = PApp (?\<pi> \<bullet> ?A) (?\<pi> \<bullet> ?B)

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
hence "\<pi> $ x \<noteq> \<sigma> $ x"
[PROOF STATE]
proof (prove)
using this:
x \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<pi> $ x \<noteq> \<sigma> $ x
[PROOF STEP]
using prm_disagreement_def CollectD
[PROOF STATE]
proof (prove)
using this:
x \<in> ds \<pi> \<sigma>
ds ?\<pi> ?\<sigma> \<equiv> {x. ?\<pi> $ x \<noteq> ?\<sigma> $ x}
?a \<in> {x. ?P x} \<Longrightarrow> ?P ?a

goal (1 subgoal):
 1. \<pi> $ x \<noteq> \<sigma> $ x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<noteq> \<sigma> $ x

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<noteq> \<sigma> $ x

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
have "\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
have "y \<in> (ptrm_fvs A) \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ y" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ y
[PROOF STEP]
using PFn \<open>\<pi> $ x \<noteq> \<sigma> $ x\<close> prm_apply_unequal prm_disagreement_ext ptrm_fvs.simps(4)
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)
\<pi> $ x \<noteq> \<sigma> $ x
?x \<noteq> ?y \<Longrightarrow> ?\<pi> $ ?x \<noteq> ?\<pi> $ ?y
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x
ptrm_fvs (PFn ?x ?uu ?A) = ptrm_fvs ?A - {?x}

goal (1 subgoal):
 1. y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ y
[PROOF STEP]
by (metis Diff_iff empty_iff insert_iff)
[PROOF STATE]
proof (state)
this:
?y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ ?y

goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
hence "\<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A"
[PROOF STATE]
proof (prove)
using this:
?y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ ?y

goal (1 subgoal):
 1. \<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A
[PROOF STEP]
unfolding prm_set_def
[PROOF STATE]
proof (prove)
using this:
?y \<in> ptrm_fvs A \<Longrightarrow> \<pi> $ x \<noteq> \<sigma> $ ?y

goal (1 subgoal):
 1. \<pi> $ x \<notin> ($) \<sigma> ` ptrm_fvs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A

goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A

goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
using ptrm_prm_fvs
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x \<notin> \<sigma> {$} ptrm_fvs A
ptrm_fvs (?\<pi> \<bullet> ?X) = ?\<pi> {$} ptrm_fvs ?X

goal (1 subgoal):
 1. \<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
have "\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
have "\<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
assume *: "a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)"
[PROOF STATE]
proof (state)
this:
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
hence "a \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)

goal (1 subgoal):
 1. a \<noteq> x
[PROOF STEP]
using \<open>\<pi> $ x \<noteq> \<sigma> $ x\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)
\<pi> $ x \<noteq> \<sigma> $ x

goal (1 subgoal):
 1. a \<noteq> x
[PROOF STEP]
using prm_apply_composition prm_disagreement_ext prm_unit_action prm_unit_commutes
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)
\<pi> $ x \<noteq> \<sigma> $ x
?f \<diamondop> ?g $ ?x = ?f $ (?g $ ?x)
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x
[?a \<leftrightarrow> ?b] $ ?a = ?b
[?a \<leftrightarrow> ?b] = [?b \<leftrightarrow> ?a]

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

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
hence "a \<in> ds \<pi> \<sigma>"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> x

goal (1 subgoal):
 1. a \<in> ds \<pi> \<sigma>
[PROOF STEP]
using * prm_apply_composition prm_apply_unequal prm_disagreement_ext prm_unit_inaction
[PROOF STATE]
proof (prove)
using this:
a \<noteq> x
a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>)
?f \<diamondop> ?g $ ?x = ?f $ (?g $ ?x)
?x \<noteq> ?y \<Longrightarrow> ?\<pi> $ ?x \<noteq> ?\<pi> $ ?y
?x \<in> ds ?\<pi> ?\<sigma> \<equiv> ?\<pi> $ ?x \<noteq> ?\<sigma> $ ?x
\<lbrakk>?x \<noteq> ?a; ?x \<noteq> ?b\<rbrakk> \<Longrightarrow> [?a \<leftrightarrow> ?b] $ ?x = ?x

goal (1 subgoal):
 1. a \<in> ds \<pi> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. \<And>a. a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> a \<notin> ptrm_fvs A
[PROOF STEP]
thus "a \<notin> ptrm_fvs A"
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> \<sigma>

goal (1 subgoal):
 1. a \<notin> ptrm_fvs A
[PROOF STEP]
using \<open>a \<noteq> x\<close> PFn.prems
[PROOF STATE]
proof (prove)
using this:
a \<in> ds \<pi> \<sigma>
a \<noteq> x
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. a \<notin> ptrm_fvs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> ptrm_fvs A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> ?a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> ?a \<notin> ptrm_fvs A

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
using PFn
[PROOF STATE]
proof (prove)
using this:
?a \<in> ds \<pi> ([\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<diamondop> \<sigma>) \<Longrightarrow> ?a \<notin> ptrm_fvs A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFn x T A)

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
by (simp add: ptrm_prm_apply_compose)
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A

goal (1 subgoal):
 1. x \<in> ds \<pi> \<sigma> \<Longrightarrow> \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> $ x \<noteq> \<sigma> $ x
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x \<noteq> \<sigma> $ x
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
using ptrm_alpha_equiv.fn2
[PROOF STATE]
proof (prove)
using this:
\<pi> $ x \<noteq> \<sigma> $ x
\<pi> $ x \<notin> ptrm_fvs (\<sigma> \<bullet> A)
\<pi> \<bullet> A \<approx> [\<pi> $ x \<leftrightarrow> \<sigma> $ x] \<bullet> \<sigma> \<bullet> A
\<lbrakk>?a \<noteq> ?b; ?A \<approx> [?a \<leftrightarrow> ?b] \<bullet> ?B; ?a \<notin> ptrm_fvs ?B\<rbrakk> \<Longrightarrow> PFn ?a ?T ?A \<approx> PFn ?b ?T ?B

goal (1 subgoal):
 1. \<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PFn x T A \<approx> \<sigma> \<bullet> PFn x T A

goal (3 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PPair A B)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs B) \<Longrightarrow> ?\<pi> \<bullet> B \<approx> ?\<sigma> \<bullet> B
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PPair A B)

goal (3 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
hence "\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A" and "\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B"
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs A) \<Longrightarrow> ?\<pi> \<bullet> A \<approx> ?\<sigma> \<bullet> A
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs B) \<Longrightarrow> ?\<pi> \<bullet> B \<approx> ?\<sigma> \<bullet> B
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PPair A B)

goal (1 subgoal):
 1. \<pi> \<bullet> A \<approx> \<sigma> \<bullet> A &&& \<pi> \<bullet> B \<approx> \<sigma> \<bullet> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B

goal (3 subgoals):
 1. \<And>M1 M2 \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M1) \<Longrightarrow> \<pi> \<bullet> M1 \<approx> \<sigma> \<bullet> M1; \<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M2) \<Longrightarrow> \<pi> \<bullet> M2 \<approx> \<sigma> \<bullet> M2; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PPair M1 M2)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PPair M1 M2 \<approx> \<sigma> \<bullet> PPair M1 M2
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 3. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B

goal (1 subgoal):
 1. \<pi> \<bullet> PPair A B \<approx> \<sigma> \<bullet> PPair A B
[PROOF STEP]
using ptrm_alpha_equiv.pair
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> A \<approx> \<sigma> \<bullet> A
\<pi> \<bullet> B \<approx> \<sigma> \<bullet> B
\<lbrakk>?A \<approx> ?B; ?C \<approx> ?D\<rbrakk> \<Longrightarrow> PPair ?A ?C \<approx> PPair ?B ?D

goal (1 subgoal):
 1. \<pi> \<bullet> PPair A B \<approx> \<sigma> \<bullet> PPair A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PPair A B \<approx> \<sigma> \<bullet> PPair A B

goal (2 subgoals):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PFst P)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs P) \<Longrightarrow> ?\<pi> \<bullet> P \<approx> ?\<sigma> \<bullet> P
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFst P)

goal (2 subgoals):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
hence "\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P"
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs P) \<Longrightarrow> ?\<pi> \<bullet> P \<approx> ?\<sigma> \<bullet> P
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PFst P)

goal (1 subgoal):
 1. \<pi> \<bullet> P \<approx> \<sigma> \<bullet> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P

goal (2 subgoals):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PFst M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PFst M \<approx> \<sigma> \<bullet> PFst M
 2. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P

goal (1 subgoal):
 1. \<pi> \<bullet> PFst P \<approx> \<sigma> \<bullet> PFst P
[PROOF STEP]
using ptrm_alpha_equiv.fst
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P
?A \<approx> ?B \<Longrightarrow> PFst ?A \<approx> PFst ?B

goal (1 subgoal):
 1. \<pi> \<bullet> PFst P \<approx> \<sigma> \<bullet> PFst P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PFst P \<approx> \<sigma> \<bullet> PFst P

goal (1 subgoal):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
case (PSnd P)
[PROOF STATE]
proof (state)
this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs P) \<Longrightarrow> ?\<pi> \<bullet> P \<approx> ?\<sigma> \<bullet> P
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PSnd P)

goal (1 subgoal):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
hence "\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P"
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ds ?\<pi> ?\<sigma> \<Longrightarrow> a \<notin> ptrm_fvs P) \<Longrightarrow> ?\<pi> \<bullet> P \<approx> ?\<sigma> \<bullet> P
?a \<in> ds \<pi> \<sigma> \<Longrightarrow> ?a \<notin> ptrm_fvs (PSnd P)

goal (1 subgoal):
 1. \<pi> \<bullet> P \<approx> \<sigma> \<bullet> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P

goal (1 subgoal):
 1. \<And>M \<pi> \<sigma>. \<lbrakk>\<And>\<pi> \<sigma>. (\<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs M) \<Longrightarrow> \<pi> \<bullet> M \<approx> \<sigma> \<bullet> M; \<And>a. a \<in> ds \<pi> \<sigma> \<Longrightarrow> a \<notin> ptrm_fvs (PSnd M)\<rbrakk> \<Longrightarrow> \<pi> \<bullet> PSnd M \<approx> \<sigma> \<bullet> PSnd M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P

goal (1 subgoal):
 1. \<pi> \<bullet> PSnd P \<approx> \<sigma> \<bullet> PSnd P
[PROOF STEP]
using ptrm_alpha_equiv.snd
[PROOF STATE]
proof (prove)
using this:
\<pi> \<bullet> P \<approx> \<sigma> \<bullet> P
?A \<approx> ?B \<Longrightarrow> PSnd ?A \<approx> PSnd ?B

goal (1 subgoal):
 1. \<pi> \<bullet> PSnd P \<approx> \<sigma> \<bullet> PSnd P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> \<bullet> PSnd P \<approx> \<sigma> \<bullet> PSnd P

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<R>\<^sub>3_sym: "sym (\<R>\<^sub>3 \<Gamma> \<S> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (\<R>\<^sub>3 \<Gamma> \<S> P)
[PROOF STEP]
unfolding sym_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> \<R>\<^sub>3 \<Gamma> \<S> P \<longrightarrow> (y, x) \<in> \<R>\<^sub>3 \<Gamma> \<S> P
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<langle>a, b, ba\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>aa, bb, bc\<rangle> \<Longrightarrow> \<langle>aa, bb, bc\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>a, b, ba\<rangle>
[PROOF STEP]
fix c\<^sub>1 mds mem\<^sub>1 c\<^sub>2 mds' mem\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<langle>a, b, ba\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>aa, bb, bc\<rangle> \<Longrightarrow> \<langle>aa, bb, bc\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>a, b, ba\<rangle>
[PROOF STEP]
assume asm: "\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>"
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<langle>a, b, ba\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>aa, bb, bc\<rangle> \<Longrightarrow> \<langle>aa, bb, bc\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>a, b, ba\<rangle>
[PROOF STEP]
hence [simp]: "mds' = mds"
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. mds' = mds
[PROOF STEP]
using \<R>\<^sub>3_elim'
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>
\<lbrakk>\<langle>?c\<^sub>1, ?mds, ?mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>?\<Gamma>,?\<S>,?P\<^esub> \<langle>?c\<^sub>2, ?mds\<^sub>2, ?mem\<^sub>2\<rangle>; \<And>c\<^sub>1 \<Gamma> \<S> P c\<^sub>2 c. \<lbrakk>?c\<^sub>1 = c\<^sub>1 ;; c; \<langle>c\<^sub>1, ?mds, ?mem\<^sub>1\<rangle> \<R>\<^sup>1\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, ?mds, ?mem\<^sub>2\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} ?\<Gamma>,?\<S>,?P; ?c\<^sub>2 = c\<^sub>2 ;; c; ?mds\<^sub>2 = ?mds\<rbrakk> \<Longrightarrow> ?Pa; \<And>c\<^sub>1 \<Gamma> \<S> P c\<^sub>2 c. \<lbrakk>?c\<^sub>1 = c\<^sub>1 ;; c; \<langle>c\<^sub>1, ?mds, ?mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, ?mds, ?mem\<^sub>2\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} ?\<Gamma>,?\<S>,?P; ?c\<^sub>2 = c\<^sub>2 ;; c; ?mds\<^sub>2 = ?mds\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. mds' = mds
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mds' = mds

goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<langle>a, b, ba\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>aa, bb, bc\<rangle> \<Longrightarrow> \<langle>aa, bb, bc\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>a, b, ba\<rangle>
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>
[PROOF STEP]
show "\<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. \<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<Longrightarrow> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>
[PROOF STEP]
apply (induct rule: \<R>\<^sub>3_aux.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c\<^sub>1 mds mem\<^sub>1 \<Gamma> \<S> P c\<^sub>2 mem\<^sub>2 c \<Gamma>' \<S>' P'. \<lbrakk>\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>1\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} \<Gamma>',\<S>',P'\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>2 ;; c, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>',\<S>',P'\<^esub> \<langle>c\<^sub>1 ;; c, mds, mem\<^sub>1\<rangle>
 2. \<And>c\<^sub>1 mds mem\<^sub>1 \<Gamma> \<S> P c\<^sub>2 mem\<^sub>2 c \<Gamma>' \<S>' P'. \<lbrakk>\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>; \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} \<Gamma>',\<S>',P'\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>2 ;; c, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>',\<S>',P'\<^esub> \<langle>c\<^sub>1 ;; c, mds, mem\<^sub>1\<rangle>
[PROOF STEP]
apply (metis (lifting) \<R>\<^sub>1_sym \<R>\<^sub>3_aux.intro\<^sub>1 symD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c\<^sub>1 mds mem\<^sub>1 \<Gamma> \<S> P c\<^sub>2 mem\<^sub>2 c \<Gamma>' \<S>' P'. \<lbrakk>\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>; \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>; \<turnstile> \<Gamma>,\<S>,P {c} \<Gamma>',\<S>',P'\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>2 ;; c, mds, mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>',\<S>',P'\<^esub> \<langle>c\<^sub>1 ;; c, mds, mem\<^sub>1\<rangle>
[PROOF STEP]
by (metis (lifting) \<R>\<^sub>3_aux.intro\<^sub>3)
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>2, mds', mem\<^sub>2\<rangle> \<R>\<^sup>3\<^bsub>\<Gamma>,\<S>,P\<^esub> \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PO_m2_inv9_M5_step3:
  "{m2_inv9_M5 \<inter> m2_inv2_keys_for} m2_step3 Rs A B Na Kab {> m2_inv9_M5}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m2_inv9_M5 \<inter> m2_inv2_keys_for} m2_step3 Rs A B Na Kab {> m2_inv9_M5}
[PROOF STEP]
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth (sesK (Rs $ sk)) (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<in> bad; B \<in> bad; aKey (sesK (Rs $ sk)) \<notin> extr (insert (aKey (sesK (Rs $ sk))) (insert (aAgt A) ik0)) (chan xa)\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]))
 2. \<And>Kaba Aa Ba Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth Kaba (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<in> bad; B \<in> bad; aKey Kaba \<notin> extr (insert (aKey (sesK (Rs $ sk))) (insert (aAgt A) ik0)) (chan xa); StatCh secure Sv Ba (Msg [aKey Kaba, aAgt Aa]) \<in> chan xa\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [Aa, Ba], [aKey Kaba, aNon Nb]))
 3. \<And>Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth (sesK (Rs $ sk)) (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<in> bad; B \<notin> bad; aKey (sesK (Rs $ sk)) \<notin> extr (insert (aKey (sesK (Rs $ sk))) ik0) (chan xa)\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]))
 4. \<And>Kaba Aa Ba Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth Kaba (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<in> bad; B \<notin> bad; aKey Kaba \<notin> extr (insert (aKey (sesK (Rs $ sk))) ik0) (chan xa); StatCh secure Sv Ba (Msg [aKey Kaba, aAgt Aa]) \<in> chan xa\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [Aa, Ba], [aKey Kaba, aNon Nb]))
 5. \<And>Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth (sesK (Rs $ sk)) (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<notin> bad; B \<in> bad; aKey (sesK (Rs $ sk)) \<notin> extr (insert (aKey (sesK (Rs $ sk))) (insert (aAgt A) ik0)) (chan xa)\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]))
 6. \<And>Kaba Aa Ba Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth Kaba (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<notin> bad; B \<in> bad; aKey Kaba \<notin> extr (insert (aKey (sesK (Rs $ sk))) (insert (aAgt A) ik0)) (chan xa); StatCh secure Sv Ba (Msg [aKey Kaba, aAgt Aa]) \<in> chan xa\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [Aa, Ba], [aKey Kaba, aNon Nb]))
 7. \<And>Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth (sesK (Rs $ sk)) (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<notin> bad; B \<notin> bad; aKey (sesK (Rs $ sk)) \<notin> extr ik0 (chan xa)\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]))
 8. \<And>Kaba Aa Ba Nb xa. \<lbrakk>xa \<in> m2_inv9_M5; xa \<in> m2_inv2_keys_for; Rs \<notin> dom (runs xa); Kab = sesK (Rs $ sk); Insec A B (Msg [aNon Na]) \<in> chan xa; dAuth Kaba (Msg [aNon Nb, aNon Nb]) \<in> chan xa; A \<notin> bad; B \<notin> bad; aKey Kaba \<notin> extr ik0 (chan xa); StatCh secure Sv Ba (Msg [aKey Kaba, aAgt Aa]) \<in> chan xa\<rbrakk> \<Longrightarrow> \<exists>Ra. Ra \<noteq> Rs \<and> (Ra \<noteq> Rs \<longrightarrow> runs xa Ra = Some (Init, [Aa, Ba], [aKey Kaba, aNon Nb]))
[PROOF STEP]
apply (auto simp add: m2_inv2_keys_for__extr_insert_key dest!: m2_inv9_M5D dest: dom_lemmas)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma register_tensor_id_update[simp]:
  assumes \<open>register F\<close>
  shows \<open>register (\<lambda>a::'a::type update. F a \<otimes>\<^sub>u Some)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register (\<lambda>a. F a \<otimes>\<^sub>u Some)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
register F

goal (1 subgoal):
 1. register (\<lambda>a. F a \<otimes>\<^sub>u Some)
[PROOF STEP]
apply (rule register_comp[unfolded o_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register (\<lambda>a. a \<otimes>\<^sub>u Some)
[PROOF STEP]
by simp


[STATEMENT]
lemma map_inv_f_f [simp]:
  "\<lbrakk> inj_on f (dom f); f x = Some y \<rbrakk> \<Longrightarrow> map_inv f y = Some x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f (dom f); f x = Some y\<rbrakk> \<Longrightarrow> map_inv f y = Some x
[PROOF STEP]
apply (auto simp add: map_inv_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj_on f (dom f); f x = Some y; y \<in> ran f\<rbrakk> \<Longrightarrow> (SOME x. f x = Some y) = x
 2. \<lbrakk>inj_on f (dom f); f x = Some y\<rbrakk> \<Longrightarrow> y \<in> ran f
[PROOF STEP]
apply (rule some_equality)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>inj_on f (dom f); f x = Some y; y \<in> ran f\<rbrakk> \<Longrightarrow> f x = Some y
 2. \<And>xa. \<lbrakk>inj_on f (dom f); f x = Some y; y \<in> ran f; f xa = Some y\<rbrakk> \<Longrightarrow> xa = x
 3. \<lbrakk>inj_on f (dom f); f x = Some y\<rbrakk> \<Longrightarrow> y \<in> ran f
[PROOF STEP]
apply (auto simp add:inj_on_def dom_def ran_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma determI[intro]:
  "\<lbrakk> additive t; maximal t \<rbrakk> \<Longrightarrow> determ t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Transformers.additive t; maximal t\<rbrakk> \<Longrightarrow> determ t
[PROOF STEP]
by(simp add:determ_def)


[STATEMENT]
lemma I_implies_IA:
"I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
assume I: "I \<V> Tr\<^bsub>ES\<^esub>"
[PROOF STATE]
proof (state)
this:
I \<V> Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
I \<V> Tr\<^bsub>ES\<^esub>

goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
fix \<alpha> \<beta> c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
assume "c \<in> C\<^bsub>\<V>\<^esub>"
      and  "\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>"
      and  "\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []"
      and  "Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c"
[PROOF STATE]
proof (state)
this:
c \<in> C\<^bsub>\<V>\<^esub>
\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []
Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c

goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
with I
[PROOF STATE]
proof (chain)
picking this:
I \<V> Tr\<^bsub>ES\<^esub>
c \<in> C\<^bsub>\<V>\<^esub>
\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []
Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c
[PROOF STEP]
have "\<exists> \<alpha>' \<beta>'. \<beta>' @ (c # \<alpha>') \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^esub>
                            \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []  \<and> \<beta>' \<upharpoonleft>(V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = \<beta> \<upharpoonleft>(V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) "
[PROOF STATE]
proof (prove)
using this:
I \<V> Tr\<^bsub>ES\<^esub>
c \<in> C\<^bsub>\<V>\<^esub>
\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []
Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c

goal (1 subgoal):
 1. \<exists>\<alpha>' \<beta>'. \<beta>' @ c # \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = \<beta> \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>)
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<alpha> \<beta>. \<forall>c\<in>C\<^bsub>\<V>\<^esub>. \<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<longrightarrow> (\<exists>\<alpha>' \<beta>'. \<beta>' @ [c] @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = \<beta> \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>))
c \<in> C\<^bsub>\<V>\<^esub>
\<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub>
\<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []
Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c

goal (1 subgoal):
 1. \<exists>\<alpha>' \<beta>'. \<beta>' @ c # \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = \<beta> \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha>' \<beta>'. \<beta>' @ c # \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = \<beta> \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>)

goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c2 \<in> C\<^bsub>\<V>\<^esub>; ?\<beta>2 @ ?\<alpha>2 \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []; Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> ?\<beta>2 ?c2\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<beta>' @ ?c2 # \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = ?\<alpha>2 \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = ?\<beta>2 \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>)

goal (1 subgoal):
 1. I \<V> Tr\<^bsub>ES\<^esub> \<Longrightarrow> IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c2 \<in> C\<^bsub>\<V>\<^esub>; ?\<beta>2 @ ?\<alpha>2 \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []; Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> ?\<beta>2 ?c2\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<beta>' @ ?c2 # \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = ?\<alpha>2 \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = ?\<beta>2 \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>)

goal (1 subgoal):
 1. IA \<rho> \<V> Tr\<^bsub>ES\<^esub>
[PROOF STEP]
unfolding I_def IA_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c2 \<in> C\<^bsub>\<V>\<^esub>; ?\<beta>2 @ ?\<alpha>2 \<in> Tr\<^bsub>ES\<^esub>; ?\<alpha>2 \<upharpoonleft> C\<^bsub>\<V>\<^esub> = []; Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> ?\<beta>2 ?c2\<rbrakk> \<Longrightarrow> \<exists>\<alpha>' \<beta>'. \<beta>' @ ?c2 # \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = ?\<alpha>2 \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = ?\<beta>2 \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>)

goal (1 subgoal):
 1. \<forall>\<alpha> \<beta>. \<forall>c\<in>C\<^bsub>\<V>\<^esub>. \<beta> @ \<alpha> \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha> \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> Adm \<V> \<rho> Tr\<^bsub>ES\<^esub> \<beta> c \<longrightarrow> (\<exists>\<alpha>' \<beta>'. \<beta>' @ [c] @ \<alpha>' \<in> Tr\<^bsub>ES\<^esub> \<and> \<alpha>' \<upharpoonleft> V\<^bsub>\<V>\<^esub> = \<alpha> \<upharpoonleft> V\<^bsub>\<V>\<^esub> \<and> \<alpha>' \<upharpoonleft> C\<^bsub>\<V>\<^esub> = [] \<and> \<beta>' \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>) = \<beta> \<upharpoonleft> (V\<^bsub>\<V>\<^esub> \<union> C\<^bsub>\<V>\<^esub>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
IA \<rho> \<V> Tr\<^bsub>ES\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed